Step | Hyp | Ref
| Expression |
1 | | hofval.m |
. . . 4
⊢ 𝑀 =
(HomF‘𝐶) |
2 | | hofval.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | hof1.b |
. . . 4
⊢ 𝐵 = (Base‘𝐶) |
4 | | hof1.h |
. . . 4
⊢ 𝐻 = (Hom ‘𝐶) |
5 | | hof2.o |
. . . 4
⊢ · =
(comp‘𝐶) |
6 | 1, 2, 3, 4, 5 | hofval 16892 |
. . 3
⊢ (𝜑 → 𝑀 = 〈(Homf
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))〉) |
7 | | fvex 6201 |
. . . 4
⊢
(Homf ‘𝐶) ∈ V |
8 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
9 | 3, 8 | eqeltri 2697 |
. . . . . 6
⊢ 𝐵 ∈ V |
10 | 9, 9 | xpex 6962 |
. . . . 5
⊢ (𝐵 × 𝐵) ∈ V |
11 | 10, 10 | mpt2ex 7247 |
. . . 4
⊢ (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓)))) ∈ V |
12 | 7, 11 | op2ndd 7179 |
. . 3
⊢ (𝑀 = 〈(Homf
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))〉 → (2nd
‘𝑀) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))) |
13 | 6, 12 | syl 17 |
. 2
⊢ (𝜑 → (2nd
‘𝑀) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))) |
14 | | simprr 796 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → 𝑦 = 〈𝑍, 𝑊〉) |
15 | 14 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (1st ‘𝑦) = (1st
‘〈𝑍, 𝑊〉)) |
16 | | hof2.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
17 | | hof2.w |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ 𝐵) |
18 | | op1stg 7180 |
. . . . . . 7
⊢ ((𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (1st ‘〈𝑍, 𝑊〉) = 𝑍) |
19 | 16, 17, 18 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝑍, 𝑊〉) = 𝑍) |
20 | 19 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (1st
‘〈𝑍, 𝑊〉) = 𝑍) |
21 | 15, 20 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (1st ‘𝑦) = 𝑍) |
22 | | simprl 794 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → 𝑥 = 〈𝑋, 𝑌〉) |
23 | 22 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (1st ‘𝑥) = (1st
‘〈𝑋, 𝑌〉)) |
24 | | hof1.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
25 | | hof1.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
26 | | op1stg 7180 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝑋, 𝑌〉) = 𝑋) |
27 | 24, 25, 26 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝑋, 𝑌〉) = 𝑋) |
28 | 27 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (1st
‘〈𝑋, 𝑌〉) = 𝑋) |
29 | 23, 28 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (1st ‘𝑥) = 𝑋) |
30 | 21, 29 | oveq12d 6668 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → ((1st
‘𝑦)𝐻(1st ‘𝑥)) = (𝑍𝐻𝑋)) |
31 | 22 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (2nd ‘𝑥) = (2nd
‘〈𝑋, 𝑌〉)) |
32 | | op2ndg 7181 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝑋, 𝑌〉) = 𝑌) |
33 | 24, 25, 32 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (2nd
‘〈𝑋, 𝑌〉) = 𝑌) |
34 | 33 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (2nd
‘〈𝑋, 𝑌〉) = 𝑌) |
35 | 31, 34 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (2nd ‘𝑥) = 𝑌) |
36 | 14 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (2nd ‘𝑦) = (2nd
‘〈𝑍, 𝑊〉)) |
37 | | op2ndg 7181 |
. . . . . . 7
⊢ ((𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (2nd ‘〈𝑍, 𝑊〉) = 𝑊) |
38 | 16, 17, 37 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (2nd
‘〈𝑍, 𝑊〉) = 𝑊) |
39 | 38 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (2nd
‘〈𝑍, 𝑊〉) = 𝑊) |
40 | 36, 39 | eqtrd 2656 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (2nd ‘𝑦) = 𝑊) |
41 | 35, 40 | oveq12d 6668 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → ((2nd
‘𝑥)𝐻(2nd ‘𝑦)) = (𝑌𝐻𝑊)) |
42 | 22 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (𝐻‘𝑥) = (𝐻‘〈𝑋, 𝑌〉)) |
43 | | df-ov 6653 |
. . . . 5
⊢ (𝑋𝐻𝑌) = (𝐻‘〈𝑋, 𝑌〉) |
44 | 42, 43 | syl6eqr 2674 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (𝐻‘𝑥) = (𝑋𝐻𝑌)) |
45 | 21, 29 | opeq12d 4410 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → 〈(1st
‘𝑦), (1st
‘𝑥)〉 =
〈𝑍, 𝑋〉) |
46 | 45, 40 | oveq12d 6668 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))
= (〈𝑍, 𝑋〉 · 𝑊)) |
47 | 22, 40 | oveq12d 6668 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (𝑥 · (2nd
‘𝑦)) = (〈𝑋, 𝑌〉 · 𝑊)) |
48 | 47 | oveqd 6667 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (𝑔(𝑥 · (2nd
‘𝑦))ℎ) = (𝑔(〈𝑋, 𝑌〉 · 𝑊)ℎ)) |
49 | | eqidd 2623 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → 𝑓 = 𝑓) |
50 | 46, 48, 49 | oveq123d 6671 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓) = ((𝑔(〈𝑋, 𝑌〉 · 𝑊)ℎ)(〈𝑍, 𝑋〉 · 𝑊)𝑓)) |
51 | 44, 50 | mpteq12dv 4733 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓)) = (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝑔(〈𝑋, 𝑌〉 · 𝑊)ℎ)(〈𝑍, 𝑋〉 · 𝑊)𝑓))) |
52 | 30, 41, 51 | mpt2eq123dv 6717 |
. 2
⊢ ((𝜑 ∧ (𝑥 = 〈𝑋, 𝑌〉 ∧ 𝑦 = 〈𝑍, 𝑊〉)) → (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (𝑌𝐻𝑊) ↦ (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝑔(〈𝑋, 𝑌〉 · 𝑊)ℎ)(〈𝑍, 𝑋〉 · 𝑊)𝑓)))) |
53 | | opelxpi 5148 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
54 | 24, 25, 53 | syl2anc 693 |
. 2
⊢ (𝜑 → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
55 | | opelxpi 5148 |
. . 3
⊢ ((𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → 〈𝑍, 𝑊〉 ∈ (𝐵 × 𝐵)) |
56 | 16, 17, 55 | syl2anc 693 |
. 2
⊢ (𝜑 → 〈𝑍, 𝑊〉 ∈ (𝐵 × 𝐵)) |
57 | | ovex 6678 |
. . . 4
⊢ (𝑍𝐻𝑋) ∈ V |
58 | | ovex 6678 |
. . . 4
⊢ (𝑌𝐻𝑊) ∈ V |
59 | 57, 58 | mpt2ex 7247 |
. . 3
⊢ (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (𝑌𝐻𝑊) ↦ (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝑔(〈𝑋, 𝑌〉 · 𝑊)ℎ)(〈𝑍, 𝑋〉 · 𝑊)𝑓))) ∈ V |
60 | 59 | a1i 11 |
. 2
⊢ (𝜑 → (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (𝑌𝐻𝑊) ↦ (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝑔(〈𝑋, 𝑌〉 · 𝑊)ℎ)(〈𝑍, 𝑋〉 · 𝑊)𝑓))) ∈ V) |
61 | 13, 52, 54, 56, 60 | ovmpt2d 6788 |
1
⊢ (𝜑 → (〈𝑋, 𝑌〉(2nd ‘𝑀)〈𝑍, 𝑊〉) = (𝑓 ∈ (𝑍𝐻𝑋), 𝑔 ∈ (𝑌𝐻𝑊) ↦ (ℎ ∈ (𝑋𝐻𝑌) ↦ ((𝑔(〈𝑋, 𝑌〉 · 𝑊)ℎ)(〈𝑍, 𝑋〉 · 𝑊)𝑓)))) |