Step | Hyp | Ref
| Expression |
1 | | matgsum.j |
. . . 4
⊢ (𝜑 → 𝐽 ∈ 𝑊) |
2 | | mptexg 6389 |
. . . 4
⊢ (𝐽 ∈ 𝑊 → (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈)) ∈ V) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈)) ∈ V) |
4 | | matgsum.a |
. . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) |
5 | | ovex 6577 |
. . . . 5
⊢ (𝑁 Mat 𝑅) ∈ V |
6 | 4, 5 | eqeltri 2684 |
. . . 4
⊢ 𝐴 ∈ V |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐴 ∈ V) |
8 | | ovex 6577 |
. . . 4
⊢ (𝑅 freeLMod (𝑁 × 𝑁)) ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑅 freeLMod (𝑁 × 𝑁)) ∈ V) |
10 | | matgsum.i |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ Fin) |
11 | | matgsum.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
12 | | eqid 2610 |
. . . . . 6
⊢ (𝑅 freeLMod (𝑁 × 𝑁)) = (𝑅 freeLMod (𝑁 × 𝑁)) |
13 | 4, 12 | matbas 20038 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘(𝑅 freeLMod
(𝑁 × 𝑁))) = (Base‘𝐴)) |
14 | 10, 11, 13 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) = (Base‘𝐴)) |
15 | 14 | eqcomd 2616 |
. . 3
⊢ (𝜑 → (Base‘𝐴) = (Base‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
16 | 4, 12 | matplusg 20039 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(+g‘(𝑅
freeLMod (𝑁 × 𝑁))) = (+g‘𝐴)) |
17 | 10, 11, 16 | syl2anc 691 |
. . . 4
⊢ (𝜑 →
(+g‘(𝑅
freeLMod (𝑁 × 𝑁))) = (+g‘𝐴)) |
18 | 17 | eqcomd 2616 |
. . 3
⊢ (𝜑 → (+g‘𝐴) = (+g‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
19 | 3, 7, 9, 15, 18 | gsumpropd 17095 |
. 2
⊢ (𝜑 → (𝐴 Σg (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈))) = ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈)))) |
20 | | mpt2mpts 7123 |
. . . . . 6
⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈) = (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈) |
21 | 20 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈) = (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)) |
22 | 21 | mpteq2dv 4673 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈)) = (𝑦 ∈ 𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈))) |
23 | 22 | oveq2d 6565 |
. . 3
⊢ (𝜑 → ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈))) = ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦 ∈ 𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)))) |
24 | | eqid 2610 |
. . . 4
⊢
(Base‘(𝑅
freeLMod (𝑁 × 𝑁))) = (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) |
25 | | eqid 2610 |
. . . 4
⊢
(0g‘(𝑅 freeLMod (𝑁 × 𝑁))) = (0g‘(𝑅 freeLMod (𝑁 × 𝑁))) |
26 | | xpfi 8116 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝑁 × 𝑁) ∈ Fin) |
27 | 10, 10, 26 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑁 × 𝑁) ∈ Fin) |
28 | | matgsum.f |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈) ∈ 𝐵) |
29 | | matgsum.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐴) |
30 | 28, 29 | syl6eleq 2698 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈) ∈ (Base‘𝐴)) |
31 | 20 | eqcomi 2619 |
. . . . . 6
⊢ (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈) |
32 | 31 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈)) |
33 | 10, 11 | jca 553 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
34 | 33 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
35 | 34, 13 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) = (Base‘𝐴)) |
36 | 30, 32, 35 | 3eltr4d 2703 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈) ∈ (Base‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
37 | | matgsum.w |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈)) finSupp 0 ) |
38 | 31 | mpteq2i 4669 |
. . . . . 6
⊢ (𝑦 ∈ 𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)) = (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈)) |
39 | | matgsum.z |
. . . . . . 7
⊢ 0 =
(0g‘𝐴) |
40 | 39 | eqcomi 2619 |
. . . . . 6
⊢
(0g‘𝐴) = 0 |
41 | 37, 38, 40 | 3brtr4g 4617 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)) finSupp (0g‘𝐴)) |
42 | 4, 12 | mat0 20042 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘(𝑅
freeLMod (𝑁 × 𝑁))) = (0g‘𝐴)) |
43 | 10, 11, 42 | syl2anc 691 |
. . . . 5
⊢ (𝜑 →
(0g‘(𝑅
freeLMod (𝑁 × 𝑁))) = (0g‘𝐴)) |
44 | 41, 43 | breqtrrd 4611 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)) finSupp (0g‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
45 | 12, 24, 25, 27, 1, 11, 36, 44 | frlmgsum 19930 |
. . 3
⊢ (𝜑 → ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦 ∈ 𝐽 ↦ (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈))) = (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)))) |
46 | 23, 45 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((𝑅 freeLMod (𝑁 × 𝑁)) Σg (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈))) = (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)))) |
47 | | fvex 6113 |
. . . . . . . 8
⊢
(2nd ‘𝑧) ∈ V |
48 | | csbov2g 6589 |
. . . . . . . 8
⊢
((2nd ‘𝑧) ∈ V →
⦋(2nd ‘𝑧) / 𝑗⦌(𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)) = (𝑅 Σg
⦋(2nd ‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈))) |
49 | 47, 48 | ax-mp 5 |
. . . . . . 7
⊢
⦋(2nd ‘𝑧) / 𝑗⦌(𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)) = (𝑅 Σg
⦋(2nd ‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈)) |
50 | 49 | csbeq2i 3945 |
. . . . . 6
⊢
⦋(1st ‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌(𝑅 Σg
(𝑦 ∈ 𝐽 ↦ 𝑈)) = ⦋(1st
‘𝑧) / 𝑖⦌(𝑅 Σg
⦋(2nd ‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈)) |
51 | | fvex 6113 |
. . . . . . 7
⊢
(1st ‘𝑧) ∈ V |
52 | | csbov2g 6589 |
. . . . . . 7
⊢
((1st ‘𝑧) ∈ V →
⦋(1st ‘𝑧) / 𝑖⦌(𝑅 Σg
⦋(2nd ‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈)) = (𝑅 Σg
⦋(1st ‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈))) |
53 | 51, 52 | ax-mp 5 |
. . . . . 6
⊢
⦋(1st ‘𝑧) / 𝑖⦌(𝑅 Σg
⦋(2nd ‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈)) = (𝑅 Σg
⦋(1st ‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈)) |
54 | | csbmpt2 4935 |
. . . . . . . . . 10
⊢
((2nd ‘𝑧) ∈ V →
⦋(2nd ‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈) = (𝑦 ∈ 𝐽 ↦ ⦋(2nd
‘𝑧) / 𝑗⦌𝑈)) |
55 | 47, 54 | ax-mp 5 |
. . . . . . . . 9
⊢
⦋(2nd ‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈) = (𝑦 ∈ 𝐽 ↦ ⦋(2nd
‘𝑧) / 𝑗⦌𝑈) |
56 | 55 | csbeq2i 3945 |
. . . . . . . 8
⊢
⦋(1st ‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈) = ⦋(1st
‘𝑧) / 𝑖⦌(𝑦 ∈ 𝐽 ↦ ⦋(2nd
‘𝑧) / 𝑗⦌𝑈) |
57 | | csbmpt2 4935 |
. . . . . . . . 9
⊢
((1st ‘𝑧) ∈ V →
⦋(1st ‘𝑧) / 𝑖⦌(𝑦 ∈ 𝐽 ↦ ⦋(2nd
‘𝑧) / 𝑗⦌𝑈) = (𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)) |
58 | 51, 57 | ax-mp 5 |
. . . . . . . 8
⊢
⦋(1st ‘𝑧) / 𝑖⦌(𝑦 ∈ 𝐽 ↦ ⦋(2nd
‘𝑧) / 𝑗⦌𝑈) = (𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈) |
59 | 56, 58 | eqtri 2632 |
. . . . . . 7
⊢
⦋(1st ‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈) = (𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈) |
60 | 59 | oveq2i 6560 |
. . . . . 6
⊢ (𝑅 Σg
⦋(1st ‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌(𝑦 ∈ 𝐽 ↦ 𝑈)) = (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)) |
61 | 50, 53, 60 | 3eqtrri 2637 |
. . . . 5
⊢ (𝑅 Σg
(𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈)) = ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌(𝑅 Σg
(𝑦 ∈ 𝐽 ↦ 𝑈)) |
62 | 61 | mpteq2i 4669 |
. . . 4
⊢ (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈))) = (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌(𝑅 Σg
(𝑦 ∈ 𝐽 ↦ 𝑈))) |
63 | | mpt2mpts 7123 |
. . . 4
⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) = (𝑧 ∈ (𝑁 × 𝑁) ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌(𝑅 Σg
(𝑦 ∈ 𝐽 ↦ 𝑈))) |
64 | 62, 63 | eqtr4i 2635 |
. . 3
⊢ (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈))) |
65 | 64 | a1i 11 |
. 2
⊢ (𝜑 → (𝑧 ∈ (𝑁 × 𝑁) ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ ⦋(1st
‘𝑧) / 𝑖⦌⦋(2nd
‘𝑧) / 𝑗⦌𝑈))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
66 | 19, 46, 65 | 3eqtrd 2648 |
1
⊢ (𝜑 → (𝐴 Σg (𝑦 ∈ 𝐽 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ 𝑈))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |