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 16645 |
. 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 | | opelxpi 5072 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵)) |
11 | 8, 9, 10 | syl2anc 691 |
. . 3
⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐵 × 𝐵)) |
12 | | xpcco.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
13 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = ⟨𝑋, 𝑌⟩) → 𝑍 ∈ 𝐵) |
14 | | ovex 6577 |
. . . . 5
⊢
((2^{nd} ‘𝑥)𝐾𝑦) ∈ V |
15 | | fvex 6113 |
. . . . 5
⊢ (𝐾‘𝑥) ∈ V |
16 | 14, 15 | mpt2ex 7136 |
. . . 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 |
17 | 16 | 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) |
18 | | xpcco.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ (𝑌𝐾𝑍)) |
19 | 18 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝐺 ∈ (𝑌𝐾𝑍)) |
20 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝑥 = ⟨𝑋, 𝑌⟩) |
21 | 20 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (2^{nd} ‘𝑥) = (2^{nd}
‘⟨𝑋, 𝑌⟩)) |
22 | | op2ndg 7072 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (2^{nd} ‘⟨𝑋, 𝑌⟩) = 𝑌) |
23 | 8, 9, 22 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (2^{nd}
‘⟨𝑋, 𝑌⟩) = 𝑌) |
24 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (2^{nd} ‘⟨𝑋, 𝑌⟩) = 𝑌) |
25 | 21, 24 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (2^{nd} ‘𝑥) = 𝑌) |
26 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝑦 = 𝑍) |
27 | 25, 26 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → ((2^{nd} ‘𝑥)𝐾𝑦) = (𝑌𝐾𝑍)) |
28 | 19, 27 | eleqtrrd 2691 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝐺 ∈ ((2^{nd} ‘𝑥)𝐾𝑦)) |
29 | | xpcco.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝑋𝐾𝑌)) |
30 | 29 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝐹 ∈ (𝑋𝐾𝑌)) |
31 | 20 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (𝐾‘𝑥) = (𝐾‘⟨𝑋, 𝑌⟩)) |
32 | | df-ov 6552 |
. . . . . . 7
⊢ (𝑋𝐾𝑌) = (𝐾‘⟨𝑋, 𝑌⟩) |
33 | 31, 32 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (𝐾‘𝑥) = (𝑋𝐾𝑌)) |
34 | 30, 33 | eleqtrrd 2691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → 𝐹 ∈ (𝐾‘𝑥)) |
35 | 34 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ 𝑔 = 𝐺) → 𝐹 ∈ (𝐾‘𝑥)) |
36 | | opex 4859 |
. . . . 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 |
37 | 36 | 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) |
38 | 20 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (1^{st} ‘𝑥) = (1^{st}
‘⟨𝑋, 𝑌⟩)) |
39 | | op1stg 7071 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (1^{st} ‘⟨𝑋, 𝑌⟩) = 𝑋) |
40 | 8, 9, 39 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1^{st}
‘⟨𝑋, 𝑌⟩) = 𝑋) |
41 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (1^{st} ‘⟨𝑋, 𝑌⟩) = 𝑋) |
42 | 38, 41 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) → (1^{st} ‘𝑥) = 𝑋) |
43 | 42 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st} ‘𝑥) = 𝑋) |
44 | 43 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st}
‘(1^{st} ‘𝑥)) = (1^{st} ‘𝑋)) |
45 | 25 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd} ‘𝑥) = 𝑌) |
46 | 45 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st}
‘(2^{nd} ‘𝑥)) = (1^{st} ‘𝑌)) |
47 | 44, 46 | opeq12d 4348 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ =
⟨(1^{st} ‘𝑋), (1^{st} ‘𝑌)⟩) |
48 | | simplrr 797 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑦 = 𝑍) |
49 | 48 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st} ‘𝑦) = (1^{st} ‘𝑍)) |
50 | 47, 49 | oveq12d 6567 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩ ·
(1^{st} ‘𝑦))
= (⟨(1^{st} ‘𝑋), (1^{st} ‘𝑌)⟩ · (1^{st}
‘𝑍))) |
51 | | simprl 790 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑔 = 𝐺) |
52 | 51 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st} ‘𝑔) = (1^{st} ‘𝐺)) |
53 | | simprr 792 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹) |
54 | 53 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (1^{st} ‘𝑓) = (1^{st} ‘𝐹)) |
55 | 50, 52, 54 | oveq123d 6570 |
. . . . 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} ‘𝐹))) |
56 | 43 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd}
‘(1^{st} ‘𝑥)) = (2^{nd} ‘𝑋)) |
57 | 45 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd}
‘(2^{nd} ‘𝑥)) = (2^{nd} ‘𝑌)) |
58 | 56, 57 | opeq12d 4348 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → ⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ =
⟨(2^{nd} ‘𝑋), (2^{nd} ‘𝑌)⟩) |
59 | 48 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd} ‘𝑦) = (2^{nd} ‘𝑍)) |
60 | 58, 59 | oveq12d 6567 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩ ∙
(2^{nd} ‘𝑦))
= (⟨(2^{nd} ‘𝑋), (2^{nd} ‘𝑌)⟩ ∙ (2^{nd}
‘𝑍))) |
61 | 51 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd} ‘𝑔) = (2^{nd} ‘𝐺)) |
62 | 53 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = ⟨𝑋, 𝑌⟩ ∧ 𝑦 = 𝑍)) ∧ (𝑔 = 𝐺 ∧ 𝑓 = 𝐹)) → (2^{nd} ‘𝑓) = (2^{nd} ‘𝐹)) |
63 | 60, 61, 62 | oveq123d 6570 |
. . . . 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} ‘𝐹))) |
64 | 55, 63 | opeq12d 4348 |
. . . 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}
‘𝐹))⟩) |
65 | 28, 35, 37, 64 | ovmpt2dv2 6692 |
. . 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} ‘𝐹))⟩)) |
66 | 11, 13, 17, 65 | ovmpt2dv 6691 |
. 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} ‘𝐹))⟩)) |
67 | 7, 66 | mpi 20 |
1
⊢ (𝜑 → (𝐺(⟨𝑋, 𝑌⟩𝑂𝑍)𝐹) = ⟨((1^{st} ‘𝐺)(⟨(1^{st}
‘𝑋), (1^{st}
‘𝑌)⟩ ·
(1^{st} ‘𝑍))(1^{st} ‘𝐹)), ((2^{nd} ‘𝐺)(⟨(2^{nd}
‘𝑋), (2^{nd}
‘𝑌)⟩ ∙
(2^{nd} ‘𝑍))(2^{nd} ‘𝐹))⟩) |