Step | Hyp | Ref
| Expression |
1 | | gsumvsca.a |
. 2
|
2 | | ssid 3624 |
. . 3
|
3 | | sseq1 3626 |
. . . . . . 7
|
4 | 3 | anbi2d 740 |
. . . . . 6
|
5 | | mpteq1 4737 |
. . . . . . . 8
|
6 | 5 | oveq2d 6666 |
. . . . . . 7
g g
|
7 | | mpteq1 4737 |
. . . . . . . . 9
|
8 | 7 | oveq2d 6666 |
. . . . . . . 8
g g |
9 | 8 | oveq1d 6665 |
. . . . . . 7
g g |
10 | 6, 9 | eqeq12d 2637 |
. . . . . 6
g g g
g |
11 | 4, 10 | imbi12d 334 |
. . . . 5
g g g
g |
12 | | sseq1 3626 |
. . . . . . 7
|
13 | 12 | anbi2d 740 |
. . . . . 6
|
14 | | mpteq1 4737 |
. . . . . . . 8
|
15 | 14 | oveq2d 6666 |
. . . . . . 7
g g |
16 | | mpteq1 4737 |
. . . . . . . . 9
|
17 | 16 | oveq2d 6666 |
. . . . . . . 8
g g |
18 | 17 | oveq1d 6665 |
. . . . . . 7
g g |
19 | 15, 18 | eqeq12d 2637 |
. . . . . 6
g g g g |
20 | 13, 19 | imbi12d 334 |
. . . . 5
g g
g g |
21 | | sseq1 3626 |
. . . . . . 7
|
22 | 21 | anbi2d 740 |
. . . . . 6
|
23 | | mpteq1 4737 |
. . . . . . . 8
|
24 | 23 | oveq2d 6666 |
. . . . . . 7
g g |
25 | | mpteq1 4737 |
. . . . . . . . 9
|
26 | 25 | oveq2d 6666 |
. . . . . . . 8
g g |
27 | 26 | oveq1d 6665 |
. . . . . . 7
g g |
28 | 24, 27 | eqeq12d 2637 |
. . . . . 6
g g g g |
29 | 22, 28 | imbi12d 334 |
. . . . 5
g g g g |
30 | | sseq1 3626 |
. . . . . . 7
|
31 | 30 | anbi2d 740 |
. . . . . 6
|
32 | | mpteq1 4737 |
. . . . . . . 8
|
33 | 32 | oveq2d 6666 |
. . . . . . 7
g g |
34 | | mpteq1 4737 |
. . . . . . . . 9
|
35 | 34 | oveq2d 6666 |
. . . . . . . 8
g g |
36 | 35 | oveq1d 6665 |
. . . . . . 7
g g |
37 | 33, 36 | eqeq12d 2637 |
. . . . . 6
g g g g |
38 | 31, 37 | imbi12d 334 |
. . . . 5
g g
g g |
39 | | gsumvsca.w |
. . . . . . . . 9
SLMod |
40 | | gsumvsca2.n |
. . . . . . . . 9
|
41 | | gsumvsca.b |
. . . . . . . . . 10
|
42 | | gsumvsca.g |
. . . . . . . . . 10
Scalar |
43 | | gsumvsca.t |
. . . . . . . . . 10
|
44 | | eqid 2622 |
. . . . . . . . . 10
|
45 | | gsumvsca.z |
. . . . . . . . . 10
|
46 | 41, 42, 43, 44, 45 | slmd0vs 29777 |
. . . . . . . . 9
SLMod
|
47 | 39, 40, 46 | syl2anc 693 |
. . . . . . . 8
|
48 | 47 | eqcomd 2628 |
. . . . . . 7
|
49 | | mpt0 6021 |
. . . . . . . . 9
|
50 | 49 | oveq2i 6661 |
. . . . . . . 8
g
g |
51 | 45 | gsum0 17278 |
. . . . . . . 8
g |
52 | 50, 51 | eqtri 2644 |
. . . . . . 7
g
|
53 | | mpt0 6021 |
. . . . . . . . . 10
|
54 | 53 | oveq2i 6661 |
. . . . . . . . 9
g g |
55 | 44 | gsum0 17278 |
. . . . . . . . 9
g |
56 | 54, 55 | eqtri 2644 |
. . . . . . . 8
g |
57 | 56 | oveq1i 6660 |
. . . . . . 7
g
|
58 | 48, 52, 57 | 3eqtr4g 2681 |
. . . . . 6
g
g |
59 | 58 | adantr 481 |
. . . . 5
g g |
60 | | ssun1 3776 |
. . . . . . . . 9
|
61 | | sstr2 3610 |
. . . . . . . . 9
|
62 | 60, 61 | ax-mp 5 |
. . . . . . . 8
|
63 | 62 | anim2i 593 |
. . . . . . 7
|
64 | 63 | imim1i 63 |
. . . . . 6
g g
g g |
65 | 39 | ad2antrl 764 |
. . . . . . . . . . 11
SLMod |
66 | | eqid 2622 |
. . . . . . . . . . . 12
|
67 | 42 | slmdsrg 29760 |
. . . . . . . . . . . . 13
SLMod SRing |
68 | | srgcmn 18508 |
. . . . . . . . . . . . 13
SRing CMnd |
69 | 65, 67, 68 | 3syl 18 |
. . . . . . . . . . . 12
CMnd |
70 | | vex 3203 |
. . . . . . . . . . . . 13
|
71 | 70 | a1i 11 |
. . . . . . . . . . . 12
|
72 | | simplrl 800 |
. . . . . . . . . . . . . 14
|
73 | | simprr 796 |
. . . . . . . . . . . . . . . 16
|
74 | 73 | unssad 3790 |
. . . . . . . . . . . . . . 15
|
75 | 74 | sselda 3603 |
. . . . . . . . . . . . . 14
|
76 | | gsumvsca.k |
. . . . . . . . . . . . . . . 16
|
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . 15
|
78 | | gsumvsca2.c |
. . . . . . . . . . . . . . 15
|
79 | 77, 78 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
80 | 72, 75, 79 | syl2anc 693 |
. . . . . . . . . . . . 13
|
81 | | eqid 2622 |
. . . . . . . . . . . . 13
|
82 | 80, 81 | fmptd 6385 |
. . . . . . . . . . . 12
|
83 | | simpll 790 |
. . . . . . . . . . . . 13
|
84 | 72, 75, 78 | syl2anc 693 |
. . . . . . . . . . . . 13
|
85 | | fvexd 6203 |
. . . . . . . . . . . . 13
|
86 | 81, 83, 84, 85 | fsuppmptdm 8286 |
. . . . . . . . . . . 12
finSupp |
87 | 66, 44, 69, 71, 82, 86 | gsumcl 18316 |
. . . . . . . . . . 11
g |
88 | 73 | unssbd 3791 |
. . . . . . . . . . . . 13
|
89 | | vex 3203 |
. . . . . . . . . . . . . 14
|
90 | 89 | snss 4316 |
. . . . . . . . . . . . 13
|
91 | 88, 90 | sylibr 224 |
. . . . . . . . . . . 12
|
92 | 79 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
93 | 92 | ad2antrl 764 |
. . . . . . . . . . . 12
|
94 | | rspcsbela 4006 |
. . . . . . . . . . . 12
|
95 | 91, 93, 94 | syl2anc 693 |
. . . . . . . . . . 11
|
96 | 40 | ad2antrl 764 |
. . . . . . . . . . 11
|
97 | | gsumvsca.p |
. . . . . . . . . . . 12
|
98 | | eqid 2622 |
. . . . . . . . . . . 12
|
99 | 41, 97, 42, 43, 66, 98 | slmdvsdir 29769 |
. . . . . . . . . . 11
SLMod
g
g g
|
100 | 65, 87, 95, 96, 99 | syl13anc 1328 |
. . . . . . . . . 10
g g
|
101 | 100 | adantr 481 |
. . . . . . . . 9
g g g g
|
102 | | nfcsb1v 3549 |
. . . . . . . . . . . 12
|
103 | 89 | a1i 11 |
. . . . . . . . . . . 12
|
104 | | simplr 792 |
. . . . . . . . . . . 12
|
105 | | csbeq1a 3542 |
. . . . . . . . . . . 12
|
106 | 102, 66, 98, 69, 83, 80, 103, 104, 95, 105 | gsumunsnf 18358 |
. . . . . . . . . . 11
g g |
107 | 106 | oveq1d 6665 |
. . . . . . . . . 10
g g |
108 | 107 | adantr 481 |
. . . . . . . . 9
g g g g |
109 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
110 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
111 | 102, 109,
110 | nfov 6676 |
. . . . . . . . . . . 12
|
112 | | slmdcmn 29758 |
. . . . . . . . . . . . 13
SLMod CMnd |
113 | 65, 112 | syl 17 |
. . . . . . . . . . . 12
CMnd |
114 | 72, 39 | syl 17 |
. . . . . . . . . . . . 13
SLMod |
115 | 72, 40 | syl 17 |
. . . . . . . . . . . . 13
|
116 | 41, 42, 43, 66 | slmdvscl 29767 |
. . . . . . . . . . . . 13
SLMod
|
117 | 114, 80, 115, 116 | syl3anc 1326 |
. . . . . . . . . . . 12
|
118 | 41, 42, 43, 66 | slmdvscl 29767 |
. . . . . . . . . . . . 13
SLMod
|
119 | 65, 95, 96, 118 | syl3anc 1326 |
. . . . . . . . . . . 12
|
120 | 105 | oveq1d 6665 |
. . . . . . . . . . . 12
|
121 | 111, 41, 97, 113, 83, 117, 103, 104, 119, 120 | gsumunsnf 18358 |
. . . . . . . . . . 11
g g
|
122 | 121 | adantr 481 |
. . . . . . . . . 10
g g g g
|
123 | | simpr 477 |
. . . . . . . . . . 11
g g g g |
124 | 123 | oveq1d 6665 |
. . . . . . . . . 10
g g g g
|
125 | 122, 124 | eqtrd 2656 |
. . . . . . . . 9
g g g g
|
126 | 101, 108,
125 | 3eqtr4rd 2667 |
. . . . . . . 8
g g g g |
127 | 126 | exp31 630 |
. . . . . . 7
g g g g |
128 | 127 | a2d 29 |
. . . . . 6
g g g g |
129 | 64, 128 | syl5 34 |
. . . . 5
g g
g g |
130 | 11, 20, 29, 38, 59, 129 | findcard2s 8201 |
. . . 4
g g |
131 | 130 | imp 445 |
. . 3
g g |
132 | 2, 131 | mpanr2 720 |
. 2
g g |
133 | 1, 132 | mpancom 703 |
1
g g |