| Step | Hyp | Ref
| Expression |
| 1 | | evlf2.l |
. 2
⊢ 𝐿 = (〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉) |
| 2 | | evlfval.e |
. . . . 5
⊢ 𝐸 = (𝐶 evalF 𝐷) |
| 3 | | evlfval.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 4 | | evlfval.d |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 5 | | evlfval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐶) |
| 6 | | evlfval.h |
. . . . 5
⊢ 𝐻 = (Hom ‘𝐶) |
| 7 | | evlfval.o |
. . . . 5
⊢ · =
(comp‘𝐷) |
| 8 | | evlfval.n |
. . . . 5
⊢ 𝑁 = (𝐶 Nat 𝐷) |
| 9 | 2, 3, 4, 5, 6, 7, 8 | evlfval 18262 |
. . . 4
⊢ (𝜑 → 𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))))〉) |
| 10 | | ovex 7464 |
. . . . . 6
⊢ (𝐶 Func 𝐷) ∈ V |
| 11 | 5 | fvexi 6920 |
. . . . . 6
⊢ 𝐵 ∈ V |
| 12 | 10, 11 | mpoex 8104 |
. . . . 5
⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)) ∈ V |
| 13 | 10, 11 | xpex 7773 |
. . . . . 6
⊢ ((𝐶 Func 𝐷) × 𝐵) ∈ V |
| 14 | 13, 13 | mpoex 8104 |
. . . . 5
⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔)))) ∈ V |
| 15 | 12, 14 | op2ndd 8025 |
. . . 4
⊢ (𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))))〉 →
(2nd ‘𝐸) =
(𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))))) |
| 16 | 9, 15 | syl 17 |
. . 3
⊢ (𝜑 → (2nd
‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))))) |
| 17 | | fvexd 6921 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) ∈ V) |
| 18 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → 𝑥 = 〈𝐹, 𝑋〉) |
| 19 | 18 | fveq2d 6910 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) = (1st
‘〈𝐹, 𝑋〉)) |
| 20 | | evlf2.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
| 21 | | evlf2.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 22 | | op1stg 8026 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (1st ‘〈𝐹, 𝑋〉) = 𝐹) |
| 23 | 20, 21, 22 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
| 24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
| 25 | 19, 24 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) = 𝐹) |
| 26 | | fvexd 6921 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) ∈ V) |
| 27 | | simplrr 778 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → 𝑦 = 〈𝐺, 𝑌〉) |
| 28 | 27 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = (1st
‘〈𝐺, 𝑌〉)) |
| 29 | | evlf2.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
| 30 | | evlf2.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 31 | | op1stg 8026 |
. . . . . . . 8
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝐺, 𝑌〉) = 𝐺) |
| 32 | 29, 30, 31 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (1st
‘〈𝐺, 𝑌〉) = 𝐺) |
| 33 | 32 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘〈𝐺, 𝑌〉) = 𝐺) |
| 34 | 28, 33 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = 𝐺) |
| 35 | | simplr 769 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑚 = 𝐹) |
| 36 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑛 = 𝐺) |
| 37 | 35, 36 | oveq12d 7449 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑚𝑁𝑛) = (𝐹𝑁𝐺)) |
| 38 | 18 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑥 = 〈𝐹, 𝑋〉) |
| 39 | 38 | fveq2d 6910 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = (2nd
‘〈𝐹, 𝑋〉)) |
| 40 | | op2ndg 8027 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
| 41 | 20, 21, 40 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐹, 𝑋〉) = 𝑋) |
| 42 | 41 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
| 43 | 39, 42 | eqtrd 2777 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = 𝑋) |
| 44 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑦 = 〈𝐺, 𝑌〉) |
| 45 | 44 | fveq2d 6910 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = (2nd
‘〈𝐺, 𝑌〉)) |
| 46 | | op2ndg 8027 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝐺, 𝑌〉) = 𝑌) |
| 47 | 29, 30, 46 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐺, 𝑌〉) = 𝑌) |
| 48 | 47 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘〈𝐺, 𝑌〉) = 𝑌) |
| 49 | 45, 48 | eqtrd 2777 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = 𝑌) |
| 50 | 43, 49 | oveq12d 7449 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) = (𝑋𝐻𝑌)) |
| 51 | 35 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑚) = (1st ‘𝐹)) |
| 52 | 51, 43 | fveq12d 6913 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd
‘𝑥)) =
((1st ‘𝐹)‘𝑋)) |
| 53 | 51, 49 | fveq12d 6913 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd
‘𝑦)) =
((1st ‘𝐹)‘𝑌)) |
| 54 | 52, 53 | opeq12d 4881 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 〈((1st ‘𝑚)‘(2nd
‘𝑥)),
((1st ‘𝑚)‘(2nd ‘𝑦))〉 =
〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉) |
| 55 | 36 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑛) = (1st ‘𝐺)) |
| 56 | 55, 49 | fveq12d 6913 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑛)‘(2nd
‘𝑦)) =
((1st ‘𝐺)‘𝑌)) |
| 57 | 54, 56 | oveq12d 7449 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦))) = (〈((1st
‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))) |
| 58 | 49 | fveq2d 6910 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎‘(2nd ‘𝑦)) = (𝑎‘𝑌)) |
| 59 | 35 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑚) = (2nd ‘𝐹)) |
| 60 | 59, 43, 49 | oveq123d 7452 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦)) = (𝑋(2nd ‘𝐹)𝑌)) |
| 61 | 60 | fveq1d 6908 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔) = ((𝑋(2nd ‘𝐹)𝑌)‘𝑔)) |
| 62 | 57, 58, 61 | oveq123d 7452 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔)) = ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) |
| 63 | 37, 50, 62 | mpoeq123dv 7508 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
| 64 | 26, 34, 63 | csbied2 3936 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → ⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
| 65 | 17, 25, 64 | csbied2 3936 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) →
⦋(1st ‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
| 66 | 20, 21 | opelxpd 5724 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝑋〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
| 67 | 29, 30 | opelxpd 5724 |
. . 3
⊢ (𝜑 → 〈𝐺, 𝑌〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
| 68 | | ovex 7464 |
. . . . 5
⊢ (𝐹𝑁𝐺) ∈ V |
| 69 | | ovex 7464 |
. . . . 5
⊢ (𝑋𝐻𝑌) ∈ V |
| 70 | 68, 69 | mpoex 8104 |
. . . 4
⊢ (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V |
| 71 | 70 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V) |
| 72 | 16, 65, 66, 67, 71 | ovmpod 7585 |
. 2
⊢ (𝜑 → (〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
| 73 | 1, 72 | eqtrid 2789 |
1
⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |