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 17935 |
. . . 4
⊢ (𝜑 → 𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))))〉) |
10 | | ovex 7308 |
. . . . . 6
⊢ (𝐶 Func 𝐷) ∈ V |
11 | 5 | fvexi 6788 |
. . . . . 6
⊢ 𝐵 ∈ V |
12 | 10, 11 | mpoex 7920 |
. . . . 5
⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ 𝐵 ↦ ((1st ‘𝑓)‘𝑥)) ∈ V |
13 | 10, 11 | xpex 7603 |
. . . . . 6
⊢ ((𝐶 Func 𝐷) × 𝐵) ∈ V |
14 | 13, 13 | mpoex 7920 |
. . . . 5
⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × 𝐵), 𝑦 ∈ ((𝐶 Func 𝐷) × 𝐵) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔)))) ∈ V |
15 | 12, 14 | op2ndd 7842 |
. . . 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 6789 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) ∈ V) |
18 | | simprl 768 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → 𝑥 = 〈𝐹, 𝑋〉) |
19 | 18 | fveq2d 6778 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) = (1st
‘〈𝐹, 𝑋〉)) |
20 | | evlf2.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
21 | | evlf2.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
22 | | op1stg 7843 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (1st ‘〈𝐹, 𝑋〉) = 𝐹) |
23 | 20, 21, 22 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
24 | 23 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st
‘〈𝐹, 𝑋〉) = 𝐹) |
25 | 19, 24 | eqtrd 2778 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) → (1st ‘𝑥) = 𝐹) |
26 | | fvexd 6789 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) ∈ V) |
27 | | simplrr 775 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → 𝑦 = 〈𝐺, 𝑌〉) |
28 | 27 | fveq2d 6778 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = (1st
‘〈𝐺, 𝑌〉)) |
29 | | evlf2.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
30 | | evlf2.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
31 | | op1stg 7843 |
. . . . . . . 8
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (1st ‘〈𝐺, 𝑌〉) = 𝐺) |
32 | 29, 30, 31 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (1st
‘〈𝐺, 𝑌〉) = 𝐺) |
33 | 32 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘〈𝐺, 𝑌〉) = 𝐺) |
34 | 28, 33 | eqtrd 2778 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → (1st ‘𝑦) = 𝐺) |
35 | | simplr 766 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑚 = 𝐹) |
36 | | simpr 485 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑛 = 𝐺) |
37 | 35, 36 | oveq12d 7293 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑚𝑁𝑛) = (𝐹𝑁𝐺)) |
38 | 18 | ad2antrr 723 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑥 = 〈𝐹, 𝑋〉) |
39 | 38 | fveq2d 6778 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = (2nd
‘〈𝐹, 𝑋〉)) |
40 | | op2ndg 7844 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝑋 ∈ 𝐵) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
41 | 20, 21, 40 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐹, 𝑋〉) = 𝑋) |
42 | 41 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘〈𝐹, 𝑋〉) = 𝑋) |
43 | 39, 42 | eqtrd 2778 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑥) = 𝑋) |
44 | 27 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 𝑦 = 〈𝐺, 𝑌〉) |
45 | 44 | fveq2d 6778 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = (2nd
‘〈𝐺, 𝑌〉)) |
46 | | op2ndg 7844 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝑌 ∈ 𝐵) → (2nd ‘〈𝐺, 𝑌〉) = 𝑌) |
47 | 29, 30, 46 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (2nd
‘〈𝐺, 𝑌〉) = 𝑌) |
48 | 47 | ad3antrrr 727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘〈𝐺, 𝑌〉) = 𝑌) |
49 | 45, 48 | eqtrd 2778 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑦) = 𝑌) |
50 | 43, 49 | oveq12d 7293 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) = (𝑋𝐻𝑌)) |
51 | 35 | fveq2d 6778 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑚) = (1st ‘𝐹)) |
52 | 51, 43 | fveq12d 6781 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd
‘𝑥)) =
((1st ‘𝐹)‘𝑋)) |
53 | 51, 49 | fveq12d 6781 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑚)‘(2nd
‘𝑦)) =
((1st ‘𝐹)‘𝑌)) |
54 | 52, 53 | opeq12d 4812 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → 〈((1st ‘𝑚)‘(2nd
‘𝑥)),
((1st ‘𝑚)‘(2nd ‘𝑦))〉 =
〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉) |
55 | 36 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (1st ‘𝑛) = (1st ‘𝐺)) |
56 | 55, 49 | fveq12d 6781 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((1st ‘𝑛)‘(2nd
‘𝑦)) =
((1st ‘𝐺)‘𝑌)) |
57 | 54, 56 | oveq12d 7293 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦))) = (〈((1st
‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))) |
58 | 49 | fveq2d 6778 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎‘(2nd ‘𝑦)) = (𝑎‘𝑌)) |
59 | 35 | fveq2d 6778 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (2nd ‘𝑚) = (2nd ‘𝐹)) |
60 | 59, 43, 49 | oveq123d 7296 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦)) = (𝑋(2nd ‘𝐹)𝑌)) |
61 | 60 | fveq1d 6776 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔) = ((𝑋(2nd ‘𝐹)𝑌)‘𝑔)) |
62 | 57, 58, 61 | oveq123d 7296 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔)) = ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) |
63 | 37, 50, 62 | mpoeq123dv 7350 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) ∧ 𝑛 = 𝐺) → (𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
64 | 26, 34, 63 | csbied2 3872 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) ∧ 𝑚 = 𝐹) → ⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
65 | 17, 25, 64 | csbied2 3872 |
. . 3
⊢ ((𝜑 ∧ (𝑥 = 〈𝐹, 𝑋〉 ∧ 𝑦 = 〈𝐺, 𝑌〉)) →
⦋(1st ‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚𝑁𝑛), 𝑔 ∈ ((2nd ‘𝑥)𝐻(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉 · ((1st
‘𝑛)‘(2nd ‘𝑦)))(((2nd
‘𝑥)(2nd
‘𝑚)(2nd
‘𝑦))‘𝑔))) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
66 | 20, 21 | opelxpd 5627 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝑋〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
67 | 29, 30 | opelxpd 5627 |
. . 3
⊢ (𝜑 → 〈𝐺, 𝑌〉 ∈ ((𝐶 Func 𝐷) × 𝐵)) |
68 | | ovex 7308 |
. . . . 5
⊢ (𝐹𝑁𝐺) ∈ V |
69 | | ovex 7308 |
. . . . 5
⊢ (𝑋𝐻𝑌) ∈ V |
70 | 68, 69 | mpoex 7920 |
. . . 4
⊢ (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V |
71 | 70 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔))) ∈ V) |
72 | 16, 65, 66, 67, 71 | ovmpod 7425 |
. 2
⊢ (𝜑 → (〈𝐹, 𝑋〉(2nd ‘𝐸)〈𝐺, 𝑌〉) = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |
73 | 1, 72 | eqtrid 2790 |
1
⊢ (𝜑 → 𝐿 = (𝑎 ∈ (𝐹𝑁𝐺), 𝑔 ∈ (𝑋𝐻𝑌) ↦ ((𝑎‘𝑌)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑌)〉 · ((1st
‘𝐺)‘𝑌))((𝑋(2nd ‘𝐹)𝑌)‘𝑔)))) |