Step | Hyp | Ref
| Expression |
1 | | mplbas2.s |
. . . . 5
mPwSer |
2 | | mplbas2.i |
. . . . 5
|
3 | | mplbas2.r |
. . . . 5
|
4 | 1, 2, 3 | psrassa 19414 |
. . . 4
AssAlg |
5 | | mplbas2.p |
. . . . . 6
mPoly |
6 | | eqid 2622 |
. . . . . 6
|
7 | | eqid 2622 |
. . . . . 6
|
8 | 5, 1, 6, 7 | mplbasss 19432 |
. . . . 5
|
9 | 8 | a1i 11 |
. . . 4
|
10 | | mplbas2.v |
. . . . . . . 8
mVar |
11 | | crngring 18558 |
. . . . . . . . 9
|
12 | 3, 11 | syl 17 |
. . . . . . . 8
|
13 | 1, 10, 7, 2, 12 | mvrf 19424 |
. . . . . . 7
|
14 | 13 | ffnd 6046 |
. . . . . 6
|
15 | 2 | adantr 481 |
. . . . . . . 8
|
16 | 12 | adantr 481 |
. . . . . . . 8
|
17 | | simpr 477 |
. . . . . . . 8
|
18 | 5, 10, 6, 15, 16, 17 | mvrcl 19449 |
. . . . . . 7
|
19 | 18 | ralrimiva 2966 |
. . . . . 6
|
20 | | ffnfv 6388 |
. . . . . 6
|
21 | 14, 19, 20 | sylanbrc 698 |
. . . . 5
|
22 | | frn 6053 |
. . . . 5
|
23 | 21, 22 | syl 17 |
. . . 4
|
24 | | mplbas2.a |
. . . . 5
AlgSpan |
25 | 24, 7 | aspss 19332 |
. . . 4
AssAlg
|
26 | 4, 9, 23, 25 | syl3anc 1326 |
. . 3
|
27 | 1, 5, 6, 2, 12 | mplsubrg 19440 |
. . . 4
SubRing |
28 | 1, 5, 6, 2, 12 | mpllss 19438 |
. . . 4
|
29 | | eqid 2622 |
. . . . 5
|
30 | 24, 7, 29 | aspid 19330 |
. . . 4
AssAlg
SubRing |
31 | 4, 27, 28, 30 | syl3anc 1326 |
. . 3
|
32 | 26, 31 | sseqtrd 3641 |
. 2
|
33 | | eqid 2622 |
. . . . . 6
|
34 | | eqid 2622 |
. . . . . 6
|
35 | | eqid 2622 |
. . . . . 6
|
36 | 2 | adantr 481 |
. . . . . 6
|
37 | | eqid 2622 |
. . . . . 6
|
38 | 12 | adantr 481 |
. . . . . 6
|
39 | | simpr 477 |
. . . . . 6
|
40 | 5, 33, 34, 35, 36, 6, 37, 38, 39 | mplcoe1 19465 |
. . . . 5
g
|
41 | | eqid 2622 |
. . . . . 6
|
42 | 5 | mplring 19452 |
. . . . . . . . 9
|
43 | 2, 12, 42 | syl2anc 693 |
. . . . . . . 8
|
44 | | ringabl 18580 |
. . . . . . . 8
|
45 | 43, 44 | syl 17 |
. . . . . . 7
|
46 | 45 | adantr 481 |
. . . . . 6
|
47 | | ovex 6678 |
. . . . . . . 8
|
48 | 47 | rabex 4813 |
. . . . . . 7
|
49 | 48 | a1i 11 |
. . . . . 6
|
50 | 23, 8 | syl6ss 3615 |
. . . . . . . . . 10
|
51 | 24, 7 | aspsubrg 19331 |
. . . . . . . . . 10
AssAlg
SubRing |
52 | 4, 50, 51 | syl2anc 693 |
. . . . . . . . 9
SubRing |
53 | 5, 1, 6 | mplval2 19431 |
. . . . . . . . . . 11
↾s |
54 | 53 | subsubrg 18806 |
. . . . . . . . . 10
SubRing SubRing
SubRing
|
55 | 27, 54 | syl 17 |
. . . . . . . . 9
SubRing
SubRing
|
56 | 52, 32, 55 | mpbir2and 957 |
. . . . . . . 8
SubRing |
57 | | subrgsubg 18786 |
. . . . . . . 8
SubRing
SubGrp |
58 | 56, 57 | syl 17 |
. . . . . . 7
SubGrp |
59 | 58 | adantr 481 |
. . . . . 6
SubGrp |
60 | 5 | mpllmod 19451 |
. . . . . . . . . 10
|
61 | 2, 12, 60 | syl2anc 693 |
. . . . . . . . 9
|
62 | 61 | ad2antrr 762 |
. . . . . . . 8
|
63 | 24, 7, 29 | asplss 19329 |
. . . . . . . . . . 11
AssAlg
|
64 | 4, 50, 63 | syl2anc 693 |
. . . . . . . . . 10
|
65 | 1, 2, 12 | psrlmod 19401 |
. . . . . . . . . . 11
|
66 | | eqid 2622 |
. . . . . . . . . . . 12
|
67 | 53, 29, 66 | lsslss 18961 |
. . . . . . . . . . 11
|
68 | 65, 28, 67 | syl2anc 693 |
. . . . . . . . . 10
|
69 | 64, 32, 68 | mpbir2and 957 |
. . . . . . . . 9
|
70 | 69 | ad2antrr 762 |
. . . . . . . 8
|
71 | | eqid 2622 |
. . . . . . . . . . 11
|
72 | 5, 71, 6, 33, 39 | mplelf 19433 |
. . . . . . . . . 10
|
73 | 72 | ffvelrnda 6359 |
. . . . . . . . 9
|
74 | 5, 36, 38 | mplsca 19445 |
. . . . . . . . . . 11
Scalar |
75 | 74 | adantr 481 |
. . . . . . . . . 10
Scalar |
76 | 75 | fveq2d 6195 |
. . . . . . . . 9
Scalar |
77 | 73, 76 | eleqtrd 2703 |
. . . . . . . 8
Scalar |
78 | 2 | ad2antrr 762 |
. . . . . . . . . 10
|
79 | | eqid 2622 |
. . . . . . . . . 10
mulGrp mulGrp |
80 | | eqid 2622 |
. . . . . . . . . 10
.gmulGrp .gmulGrp |
81 | 3 | ad2antrr 762 |
. . . . . . . . . 10
|
82 | | simpr 477 |
. . . . . . . . . 10
|
83 | 5, 33, 34, 35, 78, 79, 80, 10, 81, 82 | mplcoe2 19469 |
. . . . . . . . 9
mulGrp g .gmulGrp |
84 | | eqid 2622 |
. . . . . . . . . . 11
|
85 | 79, 84 | ringidval 18503 |
. . . . . . . . . 10
mulGrp |
86 | 5 | mplcrng 19453 |
. . . . . . . . . . . . 13
|
87 | 2, 3, 86 | syl2anc 693 |
. . . . . . . . . . . 12
|
88 | 79 | crngmgp 18555 |
. . . . . . . . . . . 12
mulGrp
CMnd |
89 | 87, 88 | syl 17 |
. . . . . . . . . . 11
mulGrp CMnd |
90 | 89 | ad2antrr 762 |
. . . . . . . . . 10
mulGrp CMnd |
91 | 56 | ad2antrr 762 |
. . . . . . . . . . 11
SubRing |
92 | 79 | subrgsubm 18793 |
. . . . . . . . . . 11
SubRing
SubMndmulGrp |
93 | 91, 92 | syl 17 |
. . . . . . . . . 10
SubMndmulGrp |
94 | | simplll 798 |
. . . . . . . . . . . 12
|
95 | 33 | psrbag 19364 |
. . . . . . . . . . . . . . . 16
|
96 | 36, 95 | syl 17 |
. . . . . . . . . . . . . . 15
|
97 | 96 | biimpa 501 |
. . . . . . . . . . . . . 14
|
98 | 97 | simpld 475 |
. . . . . . . . . . . . 13
|
99 | 98 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
100 | 24, 7 | aspssid 19333 |
. . . . . . . . . . . . . . 15
AssAlg
|
101 | 4, 50, 100 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
102 | 101 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
103 | 14 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
104 | | fnfvelrn 6356 |
. . . . . . . . . . . . . 14
|
105 | 103, 104 | sylan 488 |
. . . . . . . . . . . . 13
|
106 | 102, 105 | sseldd 3604 |
. . . . . . . . . . . 12
|
107 | 79, 6 | mgpbas 18495 |
. . . . . . . . . . . . 13
mulGrp |
108 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
109 | 79, 108 | mgpplusg 18493 |
. . . . . . . . . . . . 13
mulGrp |
110 | 108 | subrgmcl 18792 |
. . . . . . . . . . . . . 14
SubRing
|
111 | 56, 110 | syl3an1 1359 |
. . . . . . . . . . . . 13
|
112 | 84 | subrg1cl 18788 |
. . . . . . . . . . . . . 14
SubRing
|
113 | 56, 112 | syl 17 |
. . . . . . . . . . . . 13
|
114 | 107, 80, 109, 89, 32, 111, 85, 113 | mulgnn0subcl 17554 |
. . . . . . . . . . . 12
.gmulGrp |
115 | 94, 99, 106, 114 | syl3anc 1326 |
. . . . . . . . . . 11
.gmulGrp |
116 | | eqid 2622 |
. . . . . . . . . . 11
.gmulGrp .gmulGrp |
117 | 115, 116 | fmptd 6385 |
. . . . . . . . . 10
.gmulGrp
|
118 | | mptexg 6484 |
. . . . . . . . . . . . 13
.gmulGrp |
119 | 2, 118 | syl 17 |
. . . . . . . . . . . 12
.gmulGrp |
120 | 119 | ad2antrr 762 |
. . . . . . . . . . 11
.gmulGrp |
121 | | funmpt 5926 |
. . . . . . . . . . . 12
.gmulGrp |
122 | 121 | a1i 11 |
. . . . . . . . . . 11
.gmulGrp |
123 | | fvexd 6203 |
. . . . . . . . . . 11
|
124 | 97 | simprd 479 |
. . . . . . . . . . 11
|
125 | | elrabi 3359 |
. . . . . . . . . . . . . . 15
|
126 | | elmapi 7879 |
. . . . . . . . . . . . . . . . 17
|
127 | 126 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
128 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
129 | | frnnn0supp 11349 |
. . . . . . . . . . . . . . . . . 18
supp |
130 | 128, 127,
129 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
supp |
131 | | eqimss 3657 |
. . . . . . . . . . . . . . . . 17
supp
supp |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . 16
supp |
133 | | c0ex 10034 |
. . . . . . . . . . . . . . . . 17
|
134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
135 | 127, 132,
128, 134 | suppssr 7326 |
. . . . . . . . . . . . . . 15
|
136 | 125, 135 | sylanl2 683 |
. . . . . . . . . . . . . 14
|
137 | 136 | oveq1d 6665 |
. . . . . . . . . . . . 13
.gmulGrp .gmulGrp |
138 | 2 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
139 | 12 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
|
140 | | eldifi 3732 |
. . . . . . . . . . . . . . . 16
|
141 | 140 | adantl 482 |
. . . . . . . . . . . . . . 15
|
142 | 5, 10, 6, 138, 139, 141 | mvrcl 19449 |
. . . . . . . . . . . . . 14
|
143 | 107, 85, 80 | mulg0 17546 |
. . . . . . . . . . . . . 14
.gmulGrp |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . 13
.gmulGrp |
145 | 137, 144 | eqtrd 2656 |
. . . . . . . . . . . 12
.gmulGrp |
146 | 145, 78 | suppss2 7329 |
. . . . . . . . . . 11
.gmulGrp supp |
147 | | suppssfifsupp 8290 |
. . . . . . . . . . 11
.gmulGrp .gmulGrp
.gmulGrp supp .gmulGrp finSupp |
148 | 120, 122,
123, 124, 146, 147 | syl32anc 1334 |
. . . . . . . . . 10
.gmulGrp finSupp |
149 | 85, 90, 78, 93, 117, 148 | gsumsubmcl 18319 |
. . . . . . . . 9
mulGrp g .gmulGrp |
150 | 83, 149 | eqeltrd 2701 |
. . . . . . . 8
|
151 | | eqid 2622 |
. . . . . . . . 9
Scalar Scalar |
152 | | eqid 2622 |
. . . . . . . . 9
Scalar Scalar |
153 | 151, 37, 152, 66 | lssvscl 18955 |
. . . . . . . 8
Scalar
|
154 | 62, 70, 77, 150, 153 | syl22anc 1327 |
. . . . . . 7
|
155 | | eqid 2622 |
. . . . . . 7
|
156 | 154, 155 | fmptd 6385 |
. . . . . 6
|
157 | 47 | mptrabex 6488 |
. . . . . . . . 9
|
158 | | funmpt 5926 |
. . . . . . . . 9
|
159 | | fvex 6201 |
. . . . . . . . 9
|
160 | 157, 158,
159 | 3pm3.2i 1239 |
. . . . . . . 8
|
161 | 160 | a1i 11 |
. . . . . . 7
|
162 | 5, 1, 7, 34, 6 | mplelbas 19430 |
. . . . . . . . . 10
finSupp |
163 | 162 | simprbi 480 |
. . . . . . . . 9
finSupp |
164 | 163 | adantl 482 |
. . . . . . . 8
finSupp |
165 | 164 | fsuppimpd 8282 |
. . . . . . 7
supp |
166 | | ssid 3624 |
. . . . . . . . . . . . 13
supp supp |
167 | 166 | a1i 11 |
. . . . . . . . . . . 12
supp
supp |
168 | | fvexd 6203 |
. . . . . . . . . . . 12
|
169 | 72, 167, 49, 168 | suppssr 7326 |
. . . . . . . . . . 11
supp |
170 | 74 | fveq2d 6195 |
. . . . . . . . . . . 12
Scalar |
171 | 170 | adantr 481 |
. . . . . . . . . . 11
supp Scalar |
172 | 169, 171 | eqtrd 2656 |
. . . . . . . . . 10
supp Scalar |
173 | 172 | oveq1d 6665 |
. . . . . . . . 9
supp Scalar
|
174 | | eldifi 3732 |
. . . . . . . . . 10
supp
|
175 | 12 | ad2antrr 762 |
. . . . . . . . . . . 12
|
176 | 5, 6, 34, 35, 33, 78, 175, 82 | mplmon 19463 |
. . . . . . . . . . 11
|
177 | | eqid 2622 |
. . . . . . . . . . . 12
Scalar Scalar |
178 | 6, 151, 37, 177, 41 | lmod0vs 18896 |
. . . . . . . . . . 11
Scalar
|
179 | 62, 176, 178 | syl2anc 693 |
. . . . . . . . . 10
Scalar
|
180 | 174, 179 | sylan2 491 |
. . . . . . . . 9
supp Scalar
|
181 | 173, 180 | eqtrd 2656 |
. . . . . . . 8
supp |
182 | 181, 49 | suppss2 7329 |
. . . . . . 7
supp supp |
183 | | suppssfifsupp 8290 |
. . . . . . 7
supp
supp supp
finSupp |
184 | 161, 165,
182, 183 | syl12anc 1324 |
. . . . . 6
finSupp |
185 | 41, 46, 49, 59, 156, 184 | gsumsubgcl 18320 |
. . . . 5
g
|
186 | 40, 185 | eqeltrd 2701 |
. . . 4
|
187 | 186 | ex 450 |
. . 3
|
188 | 187 | ssrdv 3609 |
. 2
|
189 | 32, 188 | eqssd 3620 |
1
|