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 16680 |
. . . 4
⊢ (𝜑 → 𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))))〉) |
10 | | ovex 6577 |
. . . . . 6
⊢ (𝐶 Func 𝐷) ∈ V |
11 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
12 | 5, 11 | eqeltri 2684 |
. . . . . 6
⊢ 𝐵 ∈ V |
13 | 10, 12 | mpt2ex 7136 |
. . . . 5
⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)) ∈ V |
14 | 10, 12 | xpex 6860 |
. . . . . 6
⊢ ((𝐶 Func 𝐷) × 𝐵) ∈ V |
15 | 14, 14 | mpt2ex 7136 |
. . . . 5
⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔)))) ∈ V |
16 | 13, 15 | op2ndd 7070 |
. . . 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 | | fvex 6113 |
. . . . 5
⊢
(1st ‘𝑥) ∈ V |
19 | 18 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) ∈ V) |
20 | | simprl 790 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → 𝑥 = 〈𝐹, 𝑋〉) |
21 | 20 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) = (1st
‘〈𝐹, 𝑋〉)) |
22 | | evlf2.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
23 | | evlf2.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
24 | | op1stg 7071 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (1st ‘〈𝐹, 𝑋〉) = 𝐹) |
25 | 22, 23, 24 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
26 | 25 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
27 | 21, 26 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) = 𝐹) |
28 | | fvex 6113 |
. . . . . 6
⊢
(1st ‘𝑦) ∈ V |
29 | 28 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) ∈ V) |
30 | | simplrr 797 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → 𝑦 = 〈𝐺, 𝑌〉) |
31 | 30 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = (1st
‘〈𝐺, 𝑌〉)) |
32 | | evlf2.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
33 | | evlf2.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
34 | | op1stg 7071 |
. . . . . . . 8
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝐺, 𝑌〉) = 𝐺) |
35 | 32, 33, 34 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (1st
‘〈𝐺, 𝑌〉) = 𝐺) |
36 | 35 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘〈𝐺, 𝑌〉) = 𝐺) |
37 | 31, 36 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = 𝐺) |
38 | | simplr 788 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑚 = 𝐹) |
39 | | simpr 476 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑛 = 𝐺) |
40 | 38, 39 | oveq12d 6567 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑚𝑁𝑛) = (𝐹𝑁𝐺)) |
41 | 20 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑥 = 〈𝐹, 𝑋〉) |
42 | 41 | fveq2d 6107 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = (2nd
‘〈𝐹, 𝑋〉)) |
43 | | op2ndg 7072 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
44 | 22, 23, 43 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐹, 𝑋〉) = 𝑋) |
45 | 44 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
46 | 42, 45 | eqtrd 2644 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = 𝑋) |
47 | 30 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑦 = 〈𝐺, 𝑌〉) |
48 | 47 | fveq2d 6107 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = (2nd
‘〈𝐺, 𝑌〉)) |
49 | | op2ndg 7072 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝐺, 𝑌〉) = 𝑌) |
50 | 32, 33, 49 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐺, 𝑌〉) = 𝑌) |
51 | 50 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘〈𝐺, 𝑌〉) = 𝑌) |
52 | 48, 51 | eqtrd 2644 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = 𝑌) |
53 | 46, 52 | oveq12d 6567 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) = (𝑋𝐻𝑌)) |
54 | 38 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑚) = (1st ‘𝐹)) |
55 | 54, 46 | fveq12d 6109 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd
‘𝑥)) =
((1st ‘𝐹)‘𝑋)) |
56 | 54, 52 | fveq12d 6109 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd
‘𝑦)) =
((1st ‘𝐹)‘𝑌)) |
57 | 55, 56 | opeq12d 4348 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 〈((1st ‘𝑚)‘(2nd
‘𝑥)),
((1st ‘𝑚)‘(2nd ‘𝑦))〉 =
〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉) |
58 | 39 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑛) = (1st ‘𝐺)) |
59 | 58, 52 | fveq12d 6109 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑛)‘(2nd
‘𝑦)) =
((1st ‘𝐺)‘𝑌)) |
60 | 57, 59 | oveq12d 6567 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦))) = (〈((1st
‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))) |
61 | 52 | fveq2d 6107 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎‘(2nd ‘𝑦)) = (𝑎‘𝑌)) |
62 | 38 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑚) = (2nd ‘𝐹)) |
63 | 62, 46, 52 | oveq123d 6570 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦)) = (𝑋(2nd ‘𝐹)𝑌)) |
64 | 63 | fveq1d 6105 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔) = ((𝑋(2nd ‘𝐹)𝑌)‘𝑔)) |
65 | 60, 61, 64 | oveq123d 6570 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔)) = ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) |
66 | 40, 53, 65 | mpt2eq123dv 6615 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
67 | 29, 37, 66 | csbied2 3527 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → ⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
68 | 19, 27, 67 | csbied2 3527 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) →
⦋(1st ‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
69 | | opelxpi 5072 |
. . . 4
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → 〈𝐹, 𝑋〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
70 | 22, 23, 69 | syl2anc 691 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝑋〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
71 | | opelxpi 5072 |
. . . 4
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → 〈𝐺, 𝑌〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
72 | 32, 33, 71 | syl2anc 691 |
. . 3
⊢ (𝜑 → 〈𝐺, 𝑌〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
73 | | ovex 6577 |
. . . . 5
⊢ (𝐹𝑁𝐺) ∈ V |
74 | | ovex 6577 |
. . . . 5
⊢ (𝑋𝐻𝑌) ∈ V |
75 | 73, 74 | mpt2ex 7136 |
. . . 4
⊢ (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V |
76 | 75 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V) |
77 | 17, 68, 70, 72, 76 | ovmpt2d 6686 |
. 2
⊢ (𝜑 → (〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
78 | 1, 77 | syl5eq 2656 |
1
⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |