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