Step | Hyp | Ref
| Expression |
1 | | evlfval.e |
. 2
⊢ 𝐸 = (𝐶 eval_{F} 𝐷) |
2 | | df-evlf 16900 |
. . . 4
⊢
eval_{F} = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))))⟩) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → eval_{F} =
(𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))))⟩)) |
4 | | simprl 809 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → 𝑐 = 𝐶) |
5 | | simprr 811 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → 𝑑 = 𝐷) |
6 | 4, 5 | oveq12d 6708 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑐 Func 𝑑) = (𝐶 Func 𝐷)) |
7 | 4 | fveq2d 6233 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (Base‘𝑐) = (Base‘𝐶)) |
8 | | evlfval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
9 | 7, 8 | syl6eqr 2703 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (Base‘𝑐) = 𝐵) |
10 | | eqidd 2652 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((1^{st} ‘𝑓)‘𝑥) = ((1^{st} ‘𝑓)‘𝑥)) |
11 | 6, 9, 10 | mpt2eq123dv 6759 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1^{st} ‘𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1^{st} ‘𝑓)‘𝑥))) |
12 | 6, 9 | xpeq12d 5174 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((𝑐 Func 𝑑) × (Base‘𝑐)) = ((𝐶 Func 𝐷) × 𝐵)) |
13 | 4, 5 | oveq12d 6708 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑐 Nat 𝑑) = (𝐶 Nat 𝐷)) |
14 | | evlfval.n |
. . . . . . . . . 10
⊢ 𝑁 = (𝐶 Nat 𝐷) |
15 | 13, 14 | syl6eqr 2703 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑐 Nat 𝑑) = 𝑁) |
16 | 15 | oveqd 6707 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑚(𝑐 Nat 𝑑)𝑛) = (𝑚𝑁𝑛)) |
17 | 4 | fveq2d 6233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (Hom ‘𝑐) = (Hom ‘𝐶)) |
18 | | evlfval.h |
. . . . . . . . . 10
⊢ 𝐻 = (Hom ‘𝐶) |
19 | 17, 18 | syl6eqr 2703 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (Hom ‘𝑐) = 𝐻) |
20 | 19 | oveqd 6707 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) = ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦))) |
21 | 5 | fveq2d 6233 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (comp‘𝑑) = (comp‘𝐷)) |
22 | | evlfval.o |
. . . . . . . . . . 11
⊢ · =
(comp‘𝐷) |
23 | 21, 22 | syl6eqr 2703 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (comp‘𝑑) = · ) |
24 | 23 | oveqd 6707 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦))) =
(⟨((1^{st} ‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))) |
25 | 24 | oveqd 6707 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔)) = ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔))) |
26 | 16, 20, 25 | mpt2eq123dv 6759 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))) = (𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔)))) |
27 | 26 | csbeq2dv 4025 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))) = ⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔)))) |
28 | 27 | csbeq2dv 4025 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))) = ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔)))) |
29 | 12, 12, 28 | mpt2eq123dv 6759 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔)))) = (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔))))) |
30 | 11, 29 | opeq12d 4441 |
. . 3
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ⟨(𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)), 𝑦 ∈ ((𝑐 Func 𝑑) × (Base‘𝑐)) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝑐 Nat 𝑑)𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩(comp‘𝑑)((1^{st} ‘𝑛)‘(2^{nd}
‘𝑦)))(((2^{nd} ‘𝑥)(2^{nd} ‘𝑚)(2^{nd} ‘𝑦))‘𝑔))))⟩ = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔))))⟩) |
31 | | evlfval.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
32 | | evlfval.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ Cat) |
33 | | opex 4962 |
. . . 4
⊢
⟨(𝑓 ∈
(𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔))))⟩ ∈
V |
34 | 33 | a1i 11 |
. . 3
⊢ (𝜑 → ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔))))⟩ ∈
V) |
35 | 3, 30, 31, 32, 34 | ovmpt2d 6830 |
. 2
⊢ (𝜑 → (𝐶 eval_{F} 𝐷) = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔))))⟩) |
36 | 1, 35 | syl5eq 2697 |
1
⊢ (𝜑 → 𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1^{st} ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1^{st}
‘𝑥) / 𝑚⦌⦋(1^{st}
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦)) ↦ ((𝑎‘(2^{nd} ‘𝑦))(⟨((1^{st}
‘𝑚)‘(2^{nd} ‘𝑥)), ((1^{st}
‘𝑚)‘(2^{nd} ‘𝑦))⟩ · ((1^{st}
‘𝑛)‘(2^{nd} ‘𝑦)))(((2^{nd}
‘𝑥)(2^{nd}
‘𝑚)(2^{nd}
‘𝑦))‘𝑔))))⟩) |