Step | Hyp | Ref
| Expression |
1 | | evlfval.e |
. 2
⊢ 𝐸 = (𝐶 eval_{F} 𝐷) |
2 | | df-evlf 17529 |
. . . 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 770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → 𝑐 = 𝐶) |
5 | | simprr 772 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → 𝑑 = 𝐷) |
6 | 4, 5 | oveq12d 7168 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑐 Func 𝑑) = (𝐶 Func 𝐷)) |
7 | 4 | fveq2d 6662 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (Base‘𝑐) = (Base‘𝐶)) |
8 | | evlfval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
9 | 7, 8 | eqtr4di 2811 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (Base‘𝑐) = 𝐵) |
10 | | eqidd 2759 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((1^{st} ‘𝑓)‘𝑥) = ((1^{st} ‘𝑓)‘𝑥)) |
11 | 6, 9, 10 | mpoeq123dv 7223 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑓 ∈ (𝑐 Func 𝑑), 𝑥 ∈ (Base‘𝑐) ↦ ((1^{st} ‘𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1^{st} ‘𝑓)‘𝑥))) |
12 | 6, 9 | xpeq12d 5555 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((𝑐 Func 𝑑) × (Base‘𝑐)) = ((𝐶 Func 𝐷) × 𝐵)) |
13 | 4, 5 | oveq12d 7168 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑐 Nat 𝑑) = (𝐶 Nat 𝐷)) |
14 | | evlfval.n |
. . . . . . . . . 10
⊢ 𝑁 = (𝐶 Nat 𝐷) |
15 | 13, 14 | eqtr4di 2811 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑐 Nat 𝑑) = 𝑁) |
16 | 15 | oveqd 7167 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (𝑚(𝑐 Nat 𝑑)𝑛) = (𝑚𝑁𝑛)) |
17 | 4 | fveq2d 6662 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (Hom ‘𝑐) = (Hom ‘𝐶)) |
18 | | evlfval.h |
. . . . . . . . . 10
⊢ 𝐻 = (Hom ‘𝐶) |
19 | 17, 18 | eqtr4di 2811 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (Hom ‘𝑐) = 𝐻) |
20 | 19 | oveqd 7167 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → ((2^{nd} ‘𝑥)(Hom ‘𝑐)(2^{nd} ‘𝑦)) = ((2^{nd} ‘𝑥)𝐻(2^{nd} ‘𝑦))) |
21 | 5 | fveq2d 6662 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (comp‘𝑑) = (comp‘𝐷)) |
22 | | evlfval.o |
. . . . . . . . . . 11
⊢ · =
(comp‘𝐷) |
23 | 21, 22 | eqtr4di 2811 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) → (comp‘𝑑) = · ) |
24 | 23 | oveqd 7167 |
. . . . . . . . 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 7167 |
. . . . . . . 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 | mpoeq123dv 7223 |
. . . . . . 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 3812 |
. . . . . 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 3812 |
. . . . 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 | mpoeq123dv 7223 |
. . . 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 4771 |
. . 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 5324 |
. . . 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 | ovmpod 7297 |
. 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 2805 |
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}
‘𝑦))‘𝑔))))⟩) |