Step | Hyp | Ref
| Expression |
1 | | hofval.m |
. 2
⊢ 𝑀 =
(Hom_{F}‘𝐶) |
2 | | df-hof 17370 |
. . 3
⊢
Hom_{F} = (𝑐 ∈ Cat ↦
⟨(Hom_{f} ‘𝑐), ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))))⟩) |
3 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → 𝑐 = 𝐶) |
4 | 3 | fveq2d 6500 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Hom_{f}
‘𝑐) =
(Hom_{f} ‘𝐶)) |
5 | | fvexd 6511 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Base‘𝑐) ∈ V) |
6 | 3 | fveq2d 6500 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Base‘𝑐) = (Base‘𝐶)) |
7 | | hofval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
8 | 6, 7 | syl6eqr 2825 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → (Base‘𝑐) = 𝐵) |
9 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
10 | 9 | sqxpeqd 5435 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
11 | | simplr 757 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑐 = 𝐶) |
12 | 11 | fveq2d 6500 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = (Hom ‘𝐶)) |
13 | | hofval.h |
. . . . . . . . 9
⊢ 𝐻 = (Hom ‘𝐶) |
14 | 12, 13 | syl6eqr 2825 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (Hom ‘𝑐) = 𝐻) |
15 | 14 | oveqd 6991 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)) = ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥))) |
16 | 14 | oveqd 6991 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) = ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦))) |
17 | 14 | fveq1d 6498 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑐)‘𝑥) = (𝐻‘𝑥)) |
18 | 11 | fveq2d 6500 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = (comp‘𝐶)) |
19 | | hofval.o |
. . . . . . . . . . 11
⊢ · =
(comp‘𝐶) |
20 | 18, 19 | syl6eqr 2825 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (comp‘𝑐) = · ) |
21 | 20 | oveqd 6991 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦)) = (⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))) |
22 | 20 | oveqd 6991 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥(comp‘𝑐)(2^{nd} ‘𝑦)) = (𝑥 · (2^{nd}
‘𝑦))) |
23 | 22 | oveqd 6991 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ) = (𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)) |
24 | | eqidd 2772 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → 𝑓 = 𝑓) |
25 | 21, 23, 24 | oveq123d 6995 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓) = ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓)) |
26 | 17, 25 | mpteq12dv 5008 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓)) = (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))) |
27 | 15, 16, 26 | mpoeq123dv 7045 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))) = (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓)))) |
28 | 10, 10, 27 | mpoeq123dv 7045 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 = 𝐶) ∧ 𝑏 = 𝐵) → (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))) |
29 | 5, 8, 28 | csbied2 3809 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → ⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓)))) = (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))) |
30 | 4, 29 | opeq12d 4681 |
. . 3
⊢ ((𝜑 ∧ 𝑐 = 𝐶) → ⟨(Hom_{f}
‘𝑐),
⦋(Base‘𝑐) / 𝑏⦌(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝑐)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝑐)(2^{nd} ‘𝑦))𝑓))))⟩ = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩) |
31 | | hofval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
32 | | opex 5209 |
. . . 4
⊢
⟨(Hom_{f} ‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩ ∈ V |
33 | 32 | a1i 11 |
. . 3
⊢ (𝜑 →
⟨(Hom_{f} ‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩ ∈ V) |
34 | 2, 30, 31, 33 | fvmptd2 6600 |
. 2
⊢ (𝜑 →
(Hom_{F}‘𝐶) = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩) |
35 | 1, 34 | syl5eq 2819 |
1
⊢ (𝜑 → 𝑀 = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ (𝐵 × 𝐵), 𝑦 ∈ (𝐵 × 𝐵) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)𝐻(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ (ℎ ∈ (𝐻‘𝑥) ↦ ((𝑔(𝑥 · (2^{nd}
‘𝑦))ℎ)(⟨(1^{st}
‘𝑦), (1^{st}
‘𝑥)⟩ ·
(2^{nd} ‘𝑦))𝑓))))⟩) |