Step | Hyp | Ref
| Expression |
1 | | xpcval.t |
. 2
⊢ 𝑇 = (𝐶 ×c 𝐷) |
2 | | df-xpc 17887 |
. . . 4
⊢
×c = (𝑟 ∈ V, 𝑠 ∈ V ↦
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
ℎ〉,
〈(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉}) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → ×c
= (𝑟 ∈ V, 𝑠 ∈ V ↦
⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
ℎ〉,
〈(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉})) |
4 | | fvex 6784 |
. . . . . 6
⊢
(Base‘𝑟)
∈ V |
5 | | fvex 6784 |
. . . . . 6
⊢
(Base‘𝑠)
∈ V |
6 | 4, 5 | xpex 7597 |
. . . . 5
⊢
((Base‘𝑟)
× (Base‘𝑠))
∈ V |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → ((Base‘𝑟) × (Base‘𝑠)) ∈ V) |
8 | | simprl 768 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → 𝑟 = 𝐶) |
9 | 8 | fveq2d 6775 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → (Base‘𝑟) = (Base‘𝐶)) |
10 | | xpcval.x |
. . . . . . 7
⊢ 𝑋 = (Base‘𝐶) |
11 | 9, 10 | eqtr4di 2798 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → (Base‘𝑟) = 𝑋) |
12 | | simprr 770 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → 𝑠 = 𝐷) |
13 | 12 | fveq2d 6775 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → (Base‘𝑠) = (Base‘𝐷)) |
14 | | xpcval.y |
. . . . . . 7
⊢ 𝑌 = (Base‘𝐷) |
15 | 13, 14 | eqtr4di 2798 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → (Base‘𝑠) = 𝑌) |
16 | 11, 15 | xpeq12d 5621 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → ((Base‘𝑟) × (Base‘𝑠)) = (𝑋 × 𝑌)) |
17 | | xpcval.b |
. . . . . 6
⊢ (𝜑 → 𝐵 = (𝑋 × 𝑌)) |
18 | 17 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → 𝐵 = (𝑋 × 𝑌)) |
19 | 16, 18 | eqtr4d 2783 |
. . . 4
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → ((Base‘𝑟) × (Base‘𝑠)) = 𝐵) |
20 | | vex 3435 |
. . . . . . 7
⊢ 𝑏 ∈ V |
21 | 20, 20 | mpoex 7913 |
. . . . . 6
⊢ (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) ∈ V |
22 | 21 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) ∈ V) |
23 | | simpr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
24 | | simplrl 774 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → 𝑟 = 𝐶) |
25 | 24 | fveq2d 6775 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (Hom ‘𝑟) = (Hom ‘𝐶)) |
26 | | xpcval.h |
. . . . . . . . . 10
⊢ 𝐻 = (Hom ‘𝐶) |
27 | 25, 26 | eqtr4di 2798 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (Hom ‘𝑟) = 𝐻) |
28 | 27 | oveqd 7288 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → ((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) = ((1st ‘𝑢)𝐻(1st ‘𝑣))) |
29 | | simplrr 775 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → 𝑠 = 𝐷) |
30 | 29 | fveq2d 6775 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (Hom ‘𝑠) = (Hom ‘𝐷)) |
31 | | xpcval.j |
. . . . . . . . . 10
⊢ 𝐽 = (Hom ‘𝐷) |
32 | 30, 31 | eqtr4di 2798 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (Hom ‘𝑠) = 𝐽) |
33 | 32 | oveqd 7288 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)) = ((2nd ‘𝑢)𝐽(2nd ‘𝑣))) |
34 | 28, 33 | xpeq12d 5621 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣))) = (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣)))) |
35 | 23, 23, 34 | mpoeq123dv 7344 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))) |
36 | | xpcval.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))) |
37 | 36 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1st ‘𝑢)𝐻(1st ‘𝑣)) × ((2nd ‘𝑢)𝐽(2nd ‘𝑣))))) |
38 | 35, 37 | eqtr4d 2783 |
. . . . 5
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → (𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) = 𝐾) |
39 | | simplr 766 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 𝑏 = 𝐵) |
40 | 39 | opeq2d 4817 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐵〉) |
41 | | simpr 485 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ℎ = 𝐾) |
42 | 41 | opeq2d 4817 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 〈(Hom ‘ndx), ℎ〉 = 〈(Hom ‘ndx),
𝐾〉) |
43 | 39, 39 | xpeq12d 5621 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
44 | 41 | oveqd 7288 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ((2nd ‘𝑥)ℎ𝑦) = ((2nd ‘𝑥)𝐾𝑦)) |
45 | 41 | fveq1d 6773 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (ℎ‘𝑥) = (𝐾‘𝑥)) |
46 | 24 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 𝑟 = 𝐶) |
47 | 46 | fveq2d 6775 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (comp‘𝑟) = (comp‘𝐶)) |
48 | | xpcval.o1 |
. . . . . . . . . . . . . 14
⊢ · =
(comp‘𝐶) |
49 | 47, 48 | eqtr4di 2798 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (comp‘𝑟) = · ) |
50 | 49 | oveqd 7288 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦)) = (〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))) |
51 | 50 | oveqd 7288 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)) = ((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓))) |
52 | 29 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 𝑠 = 𝐷) |
53 | 52 | fveq2d 6775 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (comp‘𝑠) = (comp‘𝐷)) |
54 | | xpcval.o2 |
. . . . . . . . . . . . . 14
⊢ ∙ =
(comp‘𝐷) |
55 | 53, 54 | eqtr4di 2798 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (comp‘𝑠) = ∙ ) |
56 | 55 | oveqd 7288 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦)) = (〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))) |
57 | 56 | oveqd 7288 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓)) = ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))) |
58 | 51, 57 | opeq12d 4818 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉 = 〈((1st
‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉) |
59 | 44, 45, 58 | mpoeq123dv 7344 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉) = (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉)) |
60 | 43, 39, 59 | mpoeq123dv 7344 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉)) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))) |
61 | | xpcval.o |
. . . . . . . . 9
⊢ (𝜑 → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))) |
62 | 61 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((2nd ‘𝑥)𝐾𝑦), 𝑓 ∈ (𝐾‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉 ·
(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉 ∙
(2nd ‘𝑦))(2nd ‘𝑓))〉))) |
63 | 60, 62 | eqtr4d 2783 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉)) = 𝑂) |
64 | 63 | opeq2d 4817 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → 〈(comp‘ndx), (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉 = 〈(comp‘ndx),
𝑂〉) |
65 | 40, 42, 64 | tpeq123d 4690 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) ∧ ℎ = 𝐾) → {〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
ℎ〉,
〈(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐾〉,
〈(comp‘ndx), 𝑂〉}) |
66 | 22, 38, 65 | csbied2 3877 |
. . . 4
⊢ (((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) ∧ 𝑏 = 𝐵) → ⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
ℎ〉,
〈(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐾〉,
〈(comp‘ndx), 𝑂〉}) |
67 | 7, 19, 66 | csbied2 3877 |
. . 3
⊢ ((𝜑 ∧ (𝑟 = 𝐶 ∧ 𝑠 = 𝐷)) → ⦋((Base‘𝑟) × (Base‘𝑠)) / 𝑏⦌⦋(𝑢 ∈ 𝑏, 𝑣 ∈ 𝑏 ↦ (((1st ‘𝑢)(Hom ‘𝑟)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑠)(2nd ‘𝑣)))) / ℎ⦌{〈(Base‘ndx), 𝑏〉, 〈(Hom ‘ndx),
ℎ〉,
〈(comp‘ndx), (𝑥
∈ (𝑏 × 𝑏), 𝑦 ∈ 𝑏 ↦ (𝑔 ∈ ((2nd ‘𝑥)ℎ𝑦), 𝑓 ∈ (ℎ‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑟)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑠)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐾〉,
〈(comp‘ndx), 𝑂〉}) |
68 | | xpcval.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
69 | 68 | elexd 3451 |
. . 3
⊢ (𝜑 → 𝐶 ∈ V) |
70 | | xpcval.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑊) |
71 | 70 | elexd 3451 |
. . 3
⊢ (𝜑 → 𝐷 ∈ V) |
72 | | tpex 7591 |
. . . 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 7419 |
. 2
⊢ (𝜑 → (𝐶 ×c 𝐷) = {〈(Base‘ndx),
𝐵〉, 〈(Hom
‘ndx), 𝐾〉,
〈(comp‘ndx), 𝑂〉}) |
75 | 1, 74 | eqtrid 2792 |
1
⊢ (𝜑 → 𝑇 = {〈(Base‘ndx), 𝐵〉, 〈(Hom ‘ndx),
𝐾〉,
〈(comp‘ndx), 𝑂〉}) |