Step | Hyp | Ref
| Expression |
1 | | xpccofval.t |
. . 3
⊢ 𝑇 = (𝐶 ×_{c} 𝐷) |
2 | | xpccofval.b |
. . 3
⊢ 𝐵 = (Base‘𝑇) |
3 | | xpccofval.k |
. . 3
⊢ 𝐾 = (Hom ‘𝑇) |
4 | | xpccofval.o1 |
. . 3
⊢ · =
(comp‘𝐶) |
5 | | xpccofval.o2 |
. . 3
⊢ ∙ =
(comp‘𝐷) |
6 | | xpccofval.o |
. . 3
⊢ 𝑂 = (comp‘𝑇) |
7 | 1, 2, 3, 4, 5, 6 | xpccofval 17694 |
. 2
⊢ 𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((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} ‘𝑓))⟩)) |
8 | | xpcco.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
9 | | xpcco.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
10 | 8, 9 | opelxpd 5594 |
. . 3
⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵)) |
11 | | xpcco.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
12 | 11 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = ⟨𝑋, 𝑌⟩) → 𝑍 ∈ 𝐵) |
13 | | ovex 7251 |
. . . . 5
⊢
((2^{nd} ‘𝑥)𝐾𝑦) ∈ V |
14 | | fvex 6735 |
. . . . 5
⊢ (𝐾‘𝑥) ∈ V |
15 | 13, 14 | mpoex 7855 |
. . . 4
⊢ (𝑔 ∈ ((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} ‘𝑓))⟩) ∈ V |
16 | 15 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (𝑔 ∈ ((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} ‘𝑓))⟩) ∈ V) |
17 | | xpcco.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (𝑌𝐾𝑍)) |
18 | 17 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝐺 ∈ (𝑌𝐾𝑍)) |
19 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝑥 = ⟨𝑋, 𝑌⟩) |
20 | 19 | fveq2d 6726 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (2^{nd} ‘𝑥) = (2^{nd}
‘⟨𝑋, 𝑌⟩)) |
21 | | op2ndg 7779 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (2^{nd} ‘⟨𝑋, 𝑌⟩) = 𝑌) |
22 | 8, 9, 21 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → (2^{nd}
‘⟨𝑋, 𝑌⟩) = 𝑌) |
23 | 22 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (2^{nd} ‘⟨𝑋, 𝑌⟩) = 𝑌) |
24 | 20, 23 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (2^{nd} ‘𝑥) = 𝑌) |
25 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝑦 = 𝑍) |
26 | 24, 25 | oveq12d 7236 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → ((2^{nd} ‘𝑥)𝐾𝑦) = (𝑌𝐾𝑍)) |
27 | 18, 26 | eleqtrrd 2841 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝐺 ∈ ((2^{nd} ‘𝑥)𝐾𝑦)) |
28 | | xpcco.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝑋𝐾𝑌)) |
29 | 28 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝐹 ∈ (𝑋𝐾𝑌)) |
30 | 19 | fveq2d 6726 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (𝐾‘𝑥) = (𝐾‘⟨𝑋, 𝑌⟩)) |
31 | | df-ov 7221 |
. . . . . . 7
⊢ (𝑋𝐾𝑌) = (𝐾‘⟨𝑋, 𝑌⟩) |
32 | 30, 31 | eqtr4di 2796 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (𝐾‘𝑥) = (𝑋𝐾𝑌)) |
33 | 29, 32 | eleqtrrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝐹 ∈ (𝐾‘𝑥)) |
34 | 33 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ 𝑔 = 𝐺) → 𝐹 ∈ (𝐾‘𝑥)) |
35 | | opex 5353 |
. . . . 5
⊢
⟨((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} ‘𝑓))⟩ ∈ V |
36 | 35 | a1i 11 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ⟨((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} ‘𝑓))⟩ ∈ V) |
37 | 19 | fveq2d 6726 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (1^{st} ‘𝑥) = (1^{st}
‘⟨𝑋, 𝑌⟩)) |
38 | | op1stg 7778 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (1^{st} ‘⟨𝑋, 𝑌⟩) = 𝑋) |
39 | 8, 9, 38 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1^{st}
‘⟨𝑋, 𝑌⟩) = 𝑋) |
40 | 39 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (1^{st} ‘⟨𝑋, 𝑌⟩) = 𝑋) |
41 | 37, 40 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (1^{st} ‘𝑥) = 𝑋) |
42 | 41 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st} ‘𝑥) = 𝑋) |
43 | 42 | fveq2d 6726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st}
‘(1^{st} ‘𝑥)) = (1^{st} ‘𝑋)) |
44 | 24 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd} ‘𝑥) = 𝑌) |
45 | 44 | fveq2d 6726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st}
‘(2^{nd} ‘𝑥)) = (1^{st} ‘𝑌)) |
46 | 43, 45 | opeq12d 4797 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ =
⟨(1^{st} ‘𝑋), (1^{st} ‘𝑌)⟩) |
47 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑦 = 𝑍) |
48 | 47 | fveq2d 6726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st} ‘𝑦) = (1^{st} ‘𝑍)) |
49 | 46, 48 | oveq12d 7236 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))
= (⟨(1^{st} ‘𝑋), (1^{st} ‘𝑌)⟩ · (1^{st}
‘𝑍))) |
50 | | simprl 771 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑔 = 𝐺) |
51 | 50 | fveq2d 6726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st} ‘𝑔) = (1^{st} ‘𝐺)) |
52 | | simprr 773 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹) |
53 | 52 | fveq2d 6726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st} ‘𝑓) = (1^{st} ‘𝐹)) |
54 | 49, 51, 53 | oveq123d 7239 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))(1^{st} ‘𝑓)) = ((1^{st} ‘𝐺)(⟨(1^{st}
‘𝑋), (1^{st}
‘𝑌)⟩ ·
(1^{st} ‘𝑍))(1^{st} ‘𝐹))) |
55 | 42 | fveq2d 6726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd}
‘(1^{st} ‘𝑥)) = (2^{nd} ‘𝑋)) |
56 | 44 | fveq2d 6726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd}
‘(2^{nd} ‘𝑥)) = (2^{nd} ‘𝑌)) |
57 | 55, 56 | opeq12d 4797 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ =
⟨(2^{nd} ‘𝑋), (2^{nd} ‘𝑌)⟩) |
58 | 47 | fveq2d 6726 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd} ‘𝑦) = (2^{nd} ‘𝑍)) |
59 | 57, 58 | oveq12d 7236 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))
= (⟨(2^{nd} ‘𝑋), (2^{nd} ‘𝑌)⟩ ∙ (2^{nd}
‘𝑍))) |
60 | 50 | fveq2d 6726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd} ‘𝑔) = (2^{nd} ‘𝐺)) |
61 | 52 | fveq2d 6726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd} ‘𝑓) = (2^{nd} ‘𝐹)) |
62 | 59, 60, 61 | oveq123d 7239 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) = ((2^{nd} ‘𝐺)(⟨(2^{nd}
‘𝑋), (2^{nd}
‘𝑌)⟩ ∙
(2^{nd} ‘𝑍))(2^{nd} ‘𝐹))) |
63 | 54, 62 | opeq12d 4797 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ⟨((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} ‘𝑓))⟩ = ⟨((1^{st}
‘𝐺)(⟨(1^{st} ‘𝑋), (1^{st} ‘𝑌)⟩ · (1^{st}
‘𝑍))(1^{st}
‘𝐹)),
((2^{nd} ‘𝐺)(⟨(2^{nd} ‘𝑋), (2^{nd} ‘𝑌)⟩ ∙ (2^{nd}
‘𝑍))(2^{nd}
‘𝐹))⟩) |
64 | 27, 34, 36, 63 | ovmpodv2 7372 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → ((⟨𝑋, 𝑌⟩𝑂𝑍) = (𝑔 ∈ ((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} ‘𝑓))⟩) → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = ⟨((1^{st} ‘𝐺)(⟨(1^{st}
‘𝑋), (1^{st}
‘𝑌)⟩ ·
(1^{st} ‘𝑍))(1^{st} ‘𝐹)), ((2^{nd} ‘𝐺)(⟨(2^{nd}
‘𝑋), (2^{nd}
‘𝑌)⟩ ∙
(2^{nd} ‘𝑍))(2^{nd} ‘𝐹))⟩)) |
65 | 10, 12, 16, 64 | ovmpodv 7371 |
. 2
⊢ (𝜑 → (𝑂 = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ 𝐵 ↦ (𝑔 ∈ ((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} ‘𝑓))⟩)) → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = ⟨((1^{st} ‘𝐺)(⟨(1^{st}
‘𝑋), (1^{st}
‘𝑌)⟩ ·
(1^{st} ‘𝑍))(1^{st} ‘𝐹)), ((2^{nd} ‘𝐺)(⟨(2^{nd}
‘𝑋), (2^{nd}
‘𝑌)⟩ ∙
(2^{nd} ‘𝑍))(2^{nd} ‘𝐹))⟩)) |
66 | 7, 65 | mpi 20 |
1
⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = ⟨((1^{st} ‘𝐺)(⟨(1^{st}
‘𝑋), (1^{st}
‘𝑌)⟩ ·
(1^{st} ‘𝑍))(1^{st} ‘𝐹)), ((2^{nd} ‘𝐺)(⟨(2^{nd}
‘𝑋), (2^{nd}
‘𝑌)⟩ ∙
(2^{nd} ‘𝑍))(2^{nd} ‘𝐹))⟩) |