| Step | Hyp | Ref
| Expression |
| 1 | | hofval.m |
. 2
⊢ 𝑀 =
(HomF‘𝐶) |
| 2 | | df-hof 18295 |
. . 3
⊢
HomF = (𝑐 ∈ Cat ↦
〈(Homf ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝑐)(2nd ‘𝑦))𝑓))))〉) |
| 3 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → 𝑐 = 𝐶) |
| 4 | 3 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Homf
‘𝑐) =
(Homf ‘𝐶)) |
| 5 | | fvexd 6921 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Base‘𝑐) ∈ V) |
| 6 | 3 | fveq2d 6910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Base‘𝑐) = (Base‘𝐶)) |
| 7 | | hofval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Base‘𝑐) = 𝐵) |
| 9 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
| 10 | 9 | sqxpeqd 5717 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
| 11 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶) |
| 12 | 11 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶)) |
| 13 | | hofval.h |
. . . . . . . . 9
⊢ 𝐻 = (Hom ‘𝐶) |
| 14 | 12, 13 | eqtr4di 2795 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻) |
| 15 | 14 | oveqd 7448 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)) = ((1st ‘𝑦)𝐻(1st ‘𝑥))) |
| 16 | 14 | oveqd 7448 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) = ((2nd ‘𝑥)𝐻(2nd ‘𝑦))) |
| 17 | 14 | fveq1d 6908 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑐)‘𝑥) = (𝐻‘𝑥)) |
| 18 | 11 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = (comp‘𝐶)) |
| 19 | | hofval.o |
. . . . . . . . . . 11
⊢ · =
(comp‘𝐶) |
| 20 | 18, 19 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = · ) |
| 21 | 20 | oveqd 7448 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝑐)(2nd ‘𝑦)) = (〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))) |
| 22 | 20 | oveqd 7448 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥(comp‘𝑐)(2nd ‘𝑦)) = (𝑥 · (2nd
‘𝑦))) |
| 23 | 22 | oveqd 7448 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ) = (𝑔(𝑥 · (2nd
‘𝑦))ℎ)) |
| 24 | | eqidd 2738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓) |
| 25 | 21, 23, 24 | oveq123d 7452 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝑐)(2nd ‘𝑦))𝑓) = ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓)) |
| 26 | 17, 25 | mpteq12dv 5233 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝑐)(2nd ‘𝑦))𝑓)) = (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))) |
| 27 | 15, 16, 26 | mpoeq123dv 7508 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝑐)(2nd ‘𝑦))𝑓))) = (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓)))) |
| 28 | 10, 10, 27 | mpoeq123dv 7508 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝑐)(2nd ‘𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))) |
| 29 | 5, 8, 28 | csbied2 3936 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝑐)(2nd ‘𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))) |
| 30 | 4, 29 | opeq12d 4881 |
. . 3
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → 〈(Homf
‘𝑐),
⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝑐)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑐)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝑐)(2nd ‘𝑦))𝑓))))〉 = 〈(Homf
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))〉) |
| 31 | | hofval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 32 | | opex 5469 |
. . . 4
⊢
〈(Homf ‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))〉 ∈ V |
| 33 | 32 | a1i 11 |
. . 3
⊢ (𝜑 →
〈(Homf ‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))〉 ∈ V) |
| 34 | 2, 30, 31, 33 | fvmptd2 7024 |
. 2
⊢ (𝜑 →
(HomF‘𝐶) = 〈(Homf
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))〉) |
| 35 | 1, 34 | eqtrid 2789 |
1
⊢ (𝜑 → 𝑀 = 〈(Homf
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1st ‘𝑦)𝐻(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2nd
‘𝑦))ℎ)(〈(1st
‘𝑦), (1st
‘𝑥)〉 ·
(2nd ‘𝑦))𝑓))))〉) |