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 | oveq2d 6666 |
. . . . . . 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 | oveq2d 6666 |
. . . . . . 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 | oveq2d 6666 |
. . . . . . 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 | oveq2d 6666 |
. . . . . . 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 | | gsumvsca.k |
. . . . . . . . . 10
|
41 | | gsumvsca1.n |
. . . . . . . . . 10
|
42 | 40, 41 | sseldd 3604 |
. . . . . . . . 9
|
43 | | gsumvsca.g |
. . . . . . . . . 10
Scalar |
44 | | gsumvsca.t |
. . . . . . . . . 10
|
45 | | eqid 2622 |
. . . . . . . . . 10
|
46 | | gsumvsca.z |
. . . . . . . . . 10
|
47 | 43, 44, 45, 46 | slmdvs0 29778 |
. . . . . . . . 9
SLMod
|
48 | 39, 42, 47 | syl2anc 693 |
. . . . . . . 8
|
49 | 48 | eqcomd 2628 |
. . . . . . 7
|
50 | | mpt0 6021 |
. . . . . . . . 9
|
51 | 50 | oveq2i 6661 |
. . . . . . . 8
g
g |
52 | 46 | gsum0 17278 |
. . . . . . . 8
g |
53 | 51, 52 | eqtri 2644 |
. . . . . . 7
g
|
54 | | mpt0 6021 |
. . . . . . . . . 10
|
55 | 54 | oveq2i 6661 |
. . . . . . . . 9
g g |
56 | 55, 52 | eqtri 2644 |
. . . . . . . 8
g |
57 | 56 | oveq2i 6661 |
. . . . . . 7
g
|
58 | 49, 53, 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 | 42 | ad2antrl 764 |
. . . . . . . . . . 11
|
67 | | gsumvsca.b |
. . . . . . . . . . . 12
|
68 | | slmdcmn 29758 |
. . . . . . . . . . . . 13
SLMod CMnd |
69 | 65, 68 | syl 17 |
. . . . . . . . . . . 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 | | gsumvsca1.c |
. . . . . . . . . . . . . 14
|
77 | 72, 75, 76 | syl2anc 693 |
. . . . . . . . . . . . 13
|
78 | | eqid 2622 |
. . . . . . . . . . . . 13
|
79 | 77, 78 | fmptd 6385 |
. . . . . . . . . . . 12
|
80 | | simpll 790 |
. . . . . . . . . . . . 13
|
81 | | fvex 6201 |
. . . . . . . . . . . . . . 15
|
82 | 46, 81 | eqeltri 2697 |
. . . . . . . . . . . . . 14
|
83 | 82 | a1i 11 |
. . . . . . . . . . . . 13
|
84 | 78, 80, 77, 83 | fsuppmptdm 8286 |
. . . . . . . . . . . 12
finSupp |
85 | 67, 46, 69, 71, 79, 84 | gsumcl 18316 |
. . . . . . . . . . 11
g |
86 | 73 | unssbd 3791 |
. . . . . . . . . . . . 13
|
87 | | vex 3203 |
. . . . . . . . . . . . . 14
|
88 | 87 | snss 4316 |
. . . . . . . . . . . . 13
|
89 | 86, 88 | sylibr 224 |
. . . . . . . . . . . 12
|
90 | 76 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
91 | 90 | ad2antrl 764 |
. . . . . . . . . . . 12
|
92 | | rspcsbela 4006 |
. . . . . . . . . . . 12
|
93 | 89, 91, 92 | syl2anc 693 |
. . . . . . . . . . 11
|
94 | | gsumvsca.p |
. . . . . . . . . . . 12
|
95 | 67, 94, 43, 44, 45 | slmdvsdi 29768 |
. . . . . . . . . . 11
SLMod
g g
g |
96 | 65, 66, 85, 93, 95 | syl13anc 1328 |
. . . . . . . . . 10
g
g |
97 | 96 | adantr 481 |
. . . . . . . . 9
g g g
g |
98 | | nfcsb1v 3549 |
. . . . . . . . . . . 12
|
99 | 87 | a1i 11 |
. . . . . . . . . . . 12
|
100 | | simplr 792 |
. . . . . . . . . . . 12
|
101 | | csbeq1a 3542 |
. . . . . . . . . . . 12
|
102 | 98, 67, 94, 69, 80, 77, 99, 100, 93, 101 | gsumunsnf 18358 |
. . . . . . . . . . 11
g g |
103 | 102 | oveq2d 6666 |
. . . . . . . . . 10
g g |
104 | 103 | adantr 481 |
. . . . . . . . 9
g g g g |
105 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
106 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
107 | 105, 106,
98 | nfov 6676 |
. . . . . . . . . . . 12
|
108 | 72, 39 | syl 17 |
. . . . . . . . . . . . 13
SLMod |
109 | 72, 42 | syl 17 |
. . . . . . . . . . . . 13
|
110 | 67, 43, 44, 45 | slmdvscl 29767 |
. . . . . . . . . . . . 13
SLMod
|
111 | 108, 109,
77, 110 | syl3anc 1326 |
. . . . . . . . . . . 12
|
112 | 67, 43, 44, 45 | slmdvscl 29767 |
. . . . . . . . . . . . 13
SLMod
|
113 | 65, 66, 93, 112 | syl3anc 1326 |
. . . . . . . . . . . 12
|
114 | 101 | oveq2d 6666 |
. . . . . . . . . . . 12
|
115 | 107, 67, 94, 69, 80, 111, 99, 100, 113, 114 | gsumunsnf 18358 |
. . . . . . . . . . 11
g g
|
116 | 115 | adantr 481 |
. . . . . . . . . 10
g g g g
|
117 | | simpr 477 |
. . . . . . . . . . 11
g g g g |
118 | 117 | oveq1d 6665 |
. . . . . . . . . 10
g g g
g |
119 | 116, 118 | eqtrd 2656 |
. . . . . . . . 9
g g g g |
120 | 97, 104, 119 | 3eqtr4rd 2667 |
. . . . . . . 8
g g g g |
121 | 120 | exp31 630 |
. . . . . . 7
g g g g |
122 | 121 | a2d 29 |
. . . . . 6
g g
g g |
123 | 64, 122 | syl5 34 |
. . . . 5
g g
g g |
124 | 11, 20, 29, 38, 59, 123 | findcard2s 8201 |
. . . 4
g g |
125 | 124 | imp 445 |
. . 3
g g |
126 | 2, 125 | mpanr2 720 |
. 2
g g |
127 | 1, 126 | mpancom 703 |
1
g g |