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 17065 |
. . . 4
⊢ (𝜑 → 𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))))〉) |
10 | | ovex 6823 |
. . . . . 6
⊢ (𝐶 Func 𝐷) ∈ V |
11 | | fvex 6342 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
12 | 5, 11 | eqeltri 2846 |
. . . . . 6
⊢ 𝐵 ∈ V |
13 | 10, 12 | mpt2ex 7397 |
. . . . 5
⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)) ∈ V |
14 | 10, 12 | xpex 7109 |
. . . . . 6
⊢ ((𝐶 Func 𝐷) × 𝐵) ∈ V |
15 | 14, 14 | mpt2ex 7397 |
. . . . 5
⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔)))) ∈ V |
16 | 13, 15 | op2ndd 7326 |
. . . 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
‘𝑦))‘𝑔))))) |
17 | 9, 16 | syl 17 |
. . 3
⊢ (𝜑 → (2nd
‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))))) |
18 | | fvexd 6344 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) ∈ V) |
19 | | simprl 754 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → 𝑥 = 〈𝐹, 𝑋〉) |
20 | 19 | fveq2d 6336 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) = (1st
‘〈𝐹, 𝑋〉)) |
21 | | evlf2.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
22 | | evlf2.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
23 | | op1stg 7327 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (1st ‘〈𝐹, 𝑋〉) = 𝐹) |
24 | 21, 22, 23 | syl2anc 573 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
25 | 24 | adantr 466 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
26 | 20, 25 | eqtrd 2805 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) = 𝐹) |
27 | | fvexd 6344 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) ∈ V) |
28 | | simplrr 763 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → 𝑦 = 〈𝐺, 𝑌〉) |
29 | 28 | fveq2d 6336 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = (1st
‘〈𝐺, 𝑌〉)) |
30 | | evlf2.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
31 | | evlf2.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
32 | | op1stg 7327 |
. . . . . . . 8
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝐺, 𝑌〉) = 𝐺) |
33 | 30, 31, 32 | syl2anc 573 |
. . . . . . 7
⊢ (𝜑 → (1st
‘〈𝐺, 𝑌〉) = 𝐺) |
34 | 33 | ad2antrr 705 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘〈𝐺, 𝑌〉) = 𝐺) |
35 | 29, 34 | eqtrd 2805 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = 𝐺) |
36 | | simplr 752 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑚 = 𝐹) |
37 | | simpr 471 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑛 = 𝐺) |
38 | 36, 37 | oveq12d 6811 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑚𝑁𝑛) = (𝐹𝑁𝐺)) |
39 | 19 | ad2antrr 705 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑥 = 〈𝐹, 𝑋〉) |
40 | 39 | fveq2d 6336 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = (2nd
‘〈𝐹, 𝑋〉)) |
41 | | op2ndg 7328 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
42 | 21, 22, 41 | syl2anc 573 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐹, 𝑋〉) = 𝑋) |
43 | 42 | ad3antrrr 709 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
44 | 40, 43 | eqtrd 2805 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = 𝑋) |
45 | 28 | adantr 466 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑦 = 〈𝐺, 𝑌〉) |
46 | 45 | fveq2d 6336 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = (2nd
‘〈𝐺, 𝑌〉)) |
47 | | op2ndg 7328 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝐺, 𝑌〉) = 𝑌) |
48 | 30, 31, 47 | syl2anc 573 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐺, 𝑌〉) = 𝑌) |
49 | 48 | ad3antrrr 709 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘〈𝐺, 𝑌〉) = 𝑌) |
50 | 46, 49 | eqtrd 2805 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = 𝑌) |
51 | 44, 50 | oveq12d 6811 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) = (𝑋𝐻𝑌)) |
52 | 36 | fveq2d 6336 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑚) = (1st ‘𝐹)) |
53 | 52, 44 | fveq12d 6338 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd
‘𝑥)) =
((1st ‘𝐹)‘𝑋)) |
54 | 52, 50 | fveq12d 6338 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd
‘𝑦)) =
((1st ‘𝐹)‘𝑌)) |
55 | 53, 54 | opeq12d 4547 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 〈((1st ‘𝑚)‘(2nd
‘𝑥)),
((1st ‘𝑚)‘(2nd ‘𝑦))〉 =
〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉) |
56 | 37 | fveq2d 6336 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑛) = (1st ‘𝐺)) |
57 | 56, 50 | fveq12d 6338 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑛)‘(2nd
‘𝑦)) =
((1st ‘𝐺)‘𝑌)) |
58 | 55, 57 | oveq12d 6811 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦))) = (〈((1st
‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))) |
59 | 50 | fveq2d 6336 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎‘(2nd ‘𝑦)) = (𝑎‘𝑌)) |
60 | 36 | fveq2d 6336 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑚) = (2nd ‘𝐹)) |
61 | 60, 44, 50 | oveq123d 6814 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦)) = (𝑋(2nd ‘𝐹)𝑌)) |
62 | 61 | fveq1d 6334 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔) = ((𝑋(2nd ‘𝐹)𝑌)‘𝑔)) |
63 | 58, 59, 62 | oveq123d 6814 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔)) = ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) |
64 | 38, 51, 63 | mpt2eq123dv 6864 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
65 | 27, 35, 64 | csbied2 3710 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → ⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
66 | 18, 26, 65 | csbied2 3710 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) →
⦋(1st ‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
67 | | opelxpi 5288 |
. . . 4
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → 〈𝐹, 𝑋〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
68 | 21, 22, 67 | syl2anc 573 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝑋〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
69 | | opelxpi 5288 |
. . . 4
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → 〈𝐺, 𝑌〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
70 | 30, 31, 69 | syl2anc 573 |
. . 3
⊢ (𝜑 → 〈𝐺, 𝑌〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
71 | | ovex 6823 |
. . . . 5
⊢ (𝐹𝑁𝐺) ∈ V |
72 | | ovex 6823 |
. . . . 5
⊢ (𝑋𝐻𝑌) ∈ V |
73 | 71, 72 | mpt2ex 7397 |
. . . 4
⊢ (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V |
74 | 73 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V) |
75 | 17, 66, 68, 70, 74 | ovmpt2d 6935 |
. 2
⊢ (𝜑 → (〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
76 | 1, 75 | syl5eq 2817 |
1
⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |