Step | Hyp | Ref
| Expression |
1 | | xpcval.t |
. 2
⊢ 𝑇 = (𝐶 ×_{c} 𝐷) |
2 | | df-xpc 17293 |
. . . 4
⊢
×_{c} = (𝑟 ∈ V, 𝑠 ∈ V ↦
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx),
ℎ⟩,
⟨(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩}) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → ×_{c}
= (𝑟 ∈ V, 𝑠 ∈ V ↦
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx),
ℎ⟩,
⟨(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩})) |
4 | | fvex 6510 |
. . . . . 6
⊢
(Base‘𝑟)
∈ V |
5 | | fvex 6510 |
. . . . . 6
⊢
(Base‘𝑠)
∈ V |
6 | 4, 5 | xpex 7292 |
. . . . 5
⊢
((Base‘𝑟)
× (Base‘𝑠))
∈ V |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → ((Base‘𝑟) × (Base‘𝑠)) ∈ V) |
8 | | simprl 759 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → 𝑟 = 𝐶) |
9 | 8 | fveq2d 6501 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → (Base‘𝑟) = (Base‘𝐶)) |
10 | | xpcval.x |
. . . . . . 7
⊢ 𝑋 = (Base‘𝐶) |
11 | 9, 10 | syl6eqr 2827 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → (Base‘𝑟) = 𝑋) |
12 | | simprr 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → 𝑠 = 𝐷) |
13 | 12 | fveq2d 6501 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → (Base‘𝑠) = (Base‘𝐷)) |
14 | | xpcval.y |
. . . . . . 7
⊢ 𝑌 = (Base‘𝐷) |
15 | 13, 14 | syl6eqr 2827 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → (Base‘𝑠) = 𝑌) |
16 | 11, 15 | xpeq12d 5435 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → ((Base‘𝑟) × (Base‘𝑠)) = (𝑋 × 𝑌)) |
17 | | xpcval.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (𝑋 × 𝑌)) |
18 | 17 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → 𝐵 = (𝑋 × 𝑌)) |
19 | 16, 18 | eqtr4d 2812 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → ((Base‘𝑟) × (Base‘𝑠)) = 𝐵) |
20 | | vex 3413 |
. . . . . . 7
⊢ 𝑏 ∈ V |
21 | 20, 20 | mpoex 7584 |
. . . . . 6
⊢ (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) ∈ V |
22 | 21 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) ∈ V) |
23 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
24 | | simplrl 765 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → 𝑟 = 𝐶) |
25 | 24 | fveq2d 6501 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (Hom ‘𝑟) = (Hom ‘𝐶)) |
26 | | xpcval.h |
. . . . . . . . . 10
⊢ 𝐻 = (Hom ‘𝐶) |
27 | 25, 26 | syl6eqr 2827 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (Hom ‘𝑟) = 𝐻) |
28 | 27 | oveqd 6992 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → ((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) = ((1^{st} ‘𝑢)𝐻(1^{st} ‘𝑣))) |
29 | | simplrr 766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → 𝑠 = 𝐷) |
30 | 29 | fveq2d 6501 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (Hom ‘𝑠) = (Hom ‘𝐷)) |
31 | | xpcval.j |
. . . . . . . . . 10
⊢ 𝐽 = (Hom ‘𝐷) |
32 | 30, 31 | syl6eqr 2827 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (Hom ‘𝑠) = 𝐽) |
33 | 32 | oveqd 6992 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)) = ((2^{nd} ‘𝑢)𝐽(2^{nd} ‘𝑣))) |
34 | 28, 33 | xpeq12d 5435 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣))) = (((1^{st} ‘𝑢)𝐻(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)𝐽(2^{nd} ‘𝑣)))) |
35 | 23, 23, 34 | mpoeq123dv 7046 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1^{st} ‘𝑢)𝐻(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)𝐽(2^{nd} ‘𝑣))))) |
36 | | xpcval.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1^{st} ‘𝑢)𝐻(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)𝐽(2^{nd} ‘𝑣))))) |
37 | 36 | ad2antrr 714 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1^{st} ‘𝑢)𝐻(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)𝐽(2^{nd} ‘𝑣))))) |
38 | 35, 37 | eqtr4d 2812 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) = 𝐾) |
39 | | simplr 757 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 𝑏 = 𝐵) |
40 | 39 | opeq2d 4681 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ⟨(Base‘ndx), 𝑏⟩ = ⟨(Base‘ndx),
𝐵⟩) |
41 | | simpr 477 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ℎ = 𝐾) |
42 | 41 | opeq2d 4681 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ⟨(Hom ‘ndx), ℎ⟩ = ⟨(Hom ‘ndx),
𝐾⟩) |
43 | 39, 39 | xpeq12d 5435 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
44 | 41 | oveqd 6992 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ((2^{nd} ‘𝑥)ℎ𝑦) = ((2^{nd} ‘𝑥)𝐾𝑦)) |
45 | 41 | fveq1d 6499 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (ℎ‘𝑥) = (𝐾‘𝑥)) |
46 | 24 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 𝑟 = 𝐶) |
47 | 46 | fveq2d 6501 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (comp‘𝑟) = (comp‘𝐶)) |
48 | | xpcval.o1 |
. . . . . . . . . . . . . 14
⊢ · =
(comp‘𝐶) |
49 | 47, 48 | syl6eqr 2827 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (comp‘𝑟) = · ) |
50 | 49 | oveqd 6992 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦)) = (⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))) |
51 | 50 | oveqd 6992 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) = ((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓))) |
52 | 29 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 𝑠 = 𝐷) |
53 | 52 | fveq2d 6501 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (comp‘𝑠) = (comp‘𝐷)) |
54 | | xpcval.o2 |
. . . . . . . . . . . . . 14
⊢ ∙ =
(comp‘𝐷) |
55 | 53, 54 | syl6eqr 2827 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (comp‘𝑠) = ∙ ) |
56 | 55 | oveqd 6992 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦)) = (⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))) |
57 | 56 | oveqd 6992 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) = ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))) |
58 | 51, 57 | opeq12d 4682 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩ = ⟨((1^{st}
‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) |
59 | 44, 45, 58 | mpoeq123dv 7046 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) = (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) |
60 | 43, 39, 59 | mpoeq123dv 7046 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
61 | | xpcval.o |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
62 | 61 | ad3antrrr 718 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
63 | 60, 62 | eqtr4d 2812 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) = 𝑂) |
64 | 63 | opeq2d 4681 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ⟨(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩ = ⟨(comp‘ndx),
𝑂⟩) |
65 | 40, 42, 64 | tpeq123d 4555 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → {⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx),
ℎ⟩,
⟨(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} = {⟨(Base‘ndx),
𝐵⟩, ⟨(Hom
‘ndx), 𝐾⟩,
⟨(comp‘ndx), 𝑂⟩}) |
66 | 22, 38, 65 | csbied2 3811 |
. . . 4
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → ⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx),
ℎ⟩,
⟨(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} = {⟨(Base‘ndx),
𝐵⟩, ⟨(Hom
‘ndx), 𝐾⟩,
⟨(comp‘ndx), 𝑂⟩}) |
67 | 7, 19, 66 | csbied2 3811 |
. . 3
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1^{st} ‘𝑢)(Hom ‘𝑟)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑠)(2^{nd} ‘𝑣)))) / ℎ⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(Hom ‘ndx),
ℎ⟩,
⟨(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑟)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑠)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} = {⟨(Base‘ndx),
𝐵⟩, ⟨(Hom
‘ndx), 𝐾⟩,
⟨(comp‘ndx), 𝑂⟩}) |
68 | | xpcval.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
69 | 68 | elexd 3430 |
. . 3
⊢ (𝜑 → 𝐶 ∈ V) |
70 | | xpcval.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑊) |
71 | 70 | elexd 3430 |
. . 3
⊢ (𝜑 → 𝐷 ∈ V) |
72 | | tpex 7286 |
. . . 4
⊢
{⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx), 𝐾⟩, ⟨(comp‘ndx),
𝑂⟩} ∈
V |
73 | 72 | a1i 11 |
. . 3
⊢ (𝜑 → {⟨(Base‘ndx),
𝐵⟩, ⟨(Hom
‘ndx), 𝐾⟩,
⟨(comp‘ndx), 𝑂⟩} ∈ V) |
74 | 3, 67, 69, 71, 73 | ovmpod 7117 |
. 2
⊢ (𝜑 → (𝐶 ×_{c} 𝐷) = {⟨(Base‘ndx),
𝐵⟩, ⟨(Hom
‘ndx), 𝐾⟩,
⟨(comp‘ndx), 𝑂⟩}) |
75 | 1, 74 | syl5eq 2821 |
1
⊢ (𝜑 → 𝑇 = {⟨(Base‘ndx), 𝐵⟩, ⟨(Hom ‘ndx),
𝐾⟩,
⟨(comp‘ndx), 𝑂⟩}) |