| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rlocaddval.1 |
|
| 2 |
|
rlocaddval.2 |
|
| 3 |
|
rlocaddval.3 |
|
| 4 |
|
rlocaddval.4 |
|
| 5 |
|
rlocaddval.5 |
|
| 6 |
|
rlocaddval.r |
|
| 7 |
|
rlocaddval.s |
|
| 8 |
|
rlocaddval.6 |
|
| 9 |
|
rlocaddval.7 |
|
| 10 |
|
rlocaddval.8 |
|
| 11 |
|
rlocaddval.9 |
|
| 12 |
|
rlocaddval.10 |
|
| 13 |
8 10
|
opelxpd |
|
| 14 |
9 11
|
opelxpd |
|
| 15 |
|
eqid |
|
| 16 |
|
eqid |
|
| 17 |
|
eqid |
|
| 18 |
|
eqid |
|
| 19 |
|
eqid |
|
| 20 |
|
eqid |
|
| 21 |
|
eqid |
|
| 22 |
|
eqid |
|
| 23 |
|
eqid |
|
| 24 |
|
eqid |
|
| 25 |
|
eqid |
|
| 26 |
|
eqid |
|
| 27 |
|
eqid |
|
| 28 |
|
eqid |
|
| 29 |
|
eqid |
|
| 30 |
29 1
|
mgpbas |
|
| 31 |
30
|
submss |
|
| 32 |
7 31
|
syl |
|
| 33 |
1 15 2 16 3 17 18 19 20 21 5 22 23 24 25 26 27 28 6 32
|
rlocval |
|
| 34 |
4 33
|
eqtrid |
|
| 35 |
|
eqidd |
|
| 36 |
|
eqid |
|
| 37 |
36
|
imasvalstr |
|
| 38 |
|
baseid |
|
| 39 |
|
snsstp1 |
|
| 40 |
|
ssun1 |
|
| 41 |
|
ssun1 |
|
| 42 |
40 41
|
sstri |
|
| 43 |
39 42
|
sstri |
|
| 44 |
1
|
fvexi |
|
| 45 |
44
|
a1i |
|
| 46 |
45 7
|
xpexd |
|
| 47 |
|
eqid |
|
| 48 |
35 37 38 43 46 47
|
strfv3 |
|
| 49 |
48
|
eqcomd |
|
| 50 |
|
eqid |
|
| 51 |
1 15 50 2 16 21 5 6 7
|
erler |
|
| 52 |
|
tpex |
|
| 53 |
|
tpex |
|
| 54 |
52 53
|
unex |
|
| 55 |
|
tpex |
|
| 56 |
54 55
|
unex |
|
| 57 |
56
|
a1i |
|
| 58 |
32
|
ad2antrr |
|
| 59 |
58
|
ad2antrr |
|
| 60 |
59
|
ad2antrr |
|
| 61 |
|
eqidd |
|
| 62 |
|
eqidd |
|
| 63 |
6
|
crnggrpd |
|
| 64 |
63
|
ad6antr |
|
| 65 |
6
|
crngringd |
|
| 66 |
65
|
ad6antr |
|
| 67 |
|
simplr |
|
| 68 |
1 5 58 67
|
erlcl1 |
|
| 69 |
68
|
ad4antr |
|
| 70 |
|
xp1st |
|
| 71 |
69 70
|
syl |
|
| 72 |
|
simpr |
|
| 73 |
1 5 58 72
|
erlcl1 |
|
| 74 |
73
|
ad4antr |
|
| 75 |
|
xp2nd |
|
| 76 |
74 75
|
syl |
|
| 77 |
60 76
|
sseldd |
|
| 78 |
1 2 66 71 77
|
ringcld |
|
| 79 |
|
xp1st |
|
| 80 |
74 79
|
syl |
|
| 81 |
|
xp2nd |
|
| 82 |
69 81
|
syl |
|
| 83 |
60 82
|
sseldd |
|
| 84 |
1 2 66 80 83
|
ringcld |
|
| 85 |
1 3 64 78 84
|
grpcld |
|
| 86 |
1 5 58 67
|
erlcl2 |
|
| 87 |
86
|
ad4antr |
|
| 88 |
|
xp1st |
|
| 89 |
87 88
|
syl |
|
| 90 |
1 5 58 72
|
erlcl2 |
|
| 91 |
90
|
ad4antr |
|
| 92 |
|
xp2nd |
|
| 93 |
91 92
|
syl |
|
| 94 |
60 93
|
sseldd |
|
| 95 |
1 2 66 89 94
|
ringcld |
|
| 96 |
|
xp1st |
|
| 97 |
91 96
|
syl |
|
| 98 |
|
xp2nd |
|
| 99 |
87 98
|
syl |
|
| 100 |
60 99
|
sseldd |
|
| 101 |
1 2 66 97 100
|
ringcld |
|
| 102 |
1 3 64 95 101
|
grpcld |
|
| 103 |
7
|
ad6antr |
|
| 104 |
29 2
|
mgpplusg |
|
| 105 |
104
|
submcl |
|
| 106 |
103 82 76 105
|
syl3anc |
|
| 107 |
104
|
submcl |
|
| 108 |
103 99 93 107
|
syl3anc |
|
| 109 |
|
simp-4r |
|
| 110 |
|
simplr |
|
| 111 |
104
|
submcl |
|
| 112 |
103 109 110 111
|
syl3anc |
|
| 113 |
60 108
|
sseldd |
|
| 114 |
1 3 2
|
ringdir |
|
| 115 |
66 78 84 113 114
|
syl13anc |
|
| 116 |
60 106
|
sseldd |
|
| 117 |
1 3 2
|
ringdir |
|
| 118 |
66 95 101 116 117
|
syl13anc |
|
| 119 |
115 118
|
oveq12d |
|
| 120 |
119
|
oveq2d |
|
| 121 |
60 109
|
sseldd |
|
| 122 |
60 110
|
sseldd |
|
| 123 |
1 2 66 121 122
|
ringcld |
|
| 124 |
1 2 66 78 113
|
ringcld |
|
| 125 |
1 2 66 84 113
|
ringcld |
|
| 126 |
1 3 64 124 125
|
grpcld |
|
| 127 |
1 2 66 95 116
|
ringcld |
|
| 128 |
1 2 66 101 116
|
ringcld |
|
| 129 |
1 3 64 127 128
|
grpcld |
|
| 130 |
1 2 16 66 123 126 129
|
ringsubdi |
|
| 131 |
1 3 2
|
ringdi |
|
| 132 |
66 123 124 125 131
|
syl13anc |
|
| 133 |
1 3 2
|
ringdi |
|
| 134 |
66 123 127 128 133
|
syl13anc |
|
| 135 |
132 134
|
oveq12d |
|
| 136 |
66
|
ringabld |
|
| 137 |
1 2 66 123 124
|
ringcld |
|
| 138 |
1 2 66 123 125
|
ringcld |
|
| 139 |
1 2 66 123 127
|
ringcld |
|
| 140 |
1 2 66 123 128
|
ringcld |
|
| 141 |
1 3 16
|
ablsub4 |
|
| 142 |
136 137 138 139 140 141
|
syl122anc |
|
| 143 |
29
|
crngmgp |
|
| 144 |
6 143
|
syl |
|
| 145 |
144
|
ad6antr |
|
| 146 |
30 104 145 121 122 71 77 100 94
|
cmn246135 |
|
| 147 |
30 104 145 121 122 89 94 83 77
|
cmn246135 |
|
| 148 |
30 104
|
cmncom |
|
| 149 |
145 77 94 148
|
syl3anc |
|
| 150 |
149
|
oveq2d |
|
| 151 |
150
|
oveq1d |
|
| 152 |
147 151
|
eqtr4d |
|
| 153 |
146 152
|
oveq12d |
|
| 154 |
1 2 66 71 100
|
ringcld |
|
| 155 |
1 2 66 89 83
|
ringcld |
|
| 156 |
1 2 16 66 121 154 155
|
ringsubdi |
|
| 157 |
|
simpllr |
|
| 158 |
156 157
|
eqtr3d |
|
| 159 |
158
|
oveq2d |
|
| 160 |
1 2 66 77 94
|
ringcld |
|
| 161 |
1 2 66 122 160
|
ringcld |
|
| 162 |
1 2 66 121 154
|
ringcld |
|
| 163 |
1 2 66 121 155
|
ringcld |
|
| 164 |
1 2 16 66 161 162 163
|
ringsubdi |
|
| 165 |
1 2 15 66 161
|
ringrzd |
|
| 166 |
159 164 165
|
3eqtr3d |
|
| 167 |
153 166
|
eqtrd |
|
| 168 |
30 104 145 121 122 80 83 100 94
|
cmn145236 |
|
| 169 |
30 104 145 121 122 97 100 83 77
|
cmn145236 |
|
| 170 |
30 104
|
cmncom |
|
| 171 |
145 100 83 170
|
syl3anc |
|
| 172 |
171
|
oveq2d |
|
| 173 |
172
|
oveq1d |
|
| 174 |
169 173
|
eqtrd |
|
| 175 |
168 174
|
oveq12d |
|
| 176 |
1 2 66 80 94
|
ringcld |
|
| 177 |
1 2 66 97 77
|
ringcld |
|
| 178 |
1 2 16 66 122 176 177
|
ringsubdi |
|
| 179 |
|
simpr |
|
| 180 |
178 179
|
eqtr3d |
|
| 181 |
180
|
oveq2d |
|
| 182 |
1 2 66 83 100
|
ringcld |
|
| 183 |
1 2 66 121 182
|
ringcld |
|
| 184 |
1 2 66 122 176
|
ringcld |
|
| 185 |
1 2 66 122 177
|
ringcld |
|
| 186 |
1 2 16 66 183 184 185
|
ringsubdi |
|
| 187 |
1 2 15 66 183
|
ringrzd |
|
| 188 |
181 186 187
|
3eqtr3d |
|
| 189 |
175 188
|
eqtrd |
|
| 190 |
167 189
|
oveq12d |
|
| 191 |
1 15
|
grpidcl |
|
| 192 |
64 191
|
syl |
|
| 193 |
1 3 15 64 192
|
grplidd |
|
| 194 |
190 193
|
eqtrd |
|
| 195 |
135 142 194
|
3eqtrd |
|
| 196 |
120 130 195
|
3eqtrd |
|
| 197 |
1 5 60 15 2 16 61 62 85 102 106 108 112 196
|
erlbrd |
|
| 198 |
72
|
ad2antrr |
|
| 199 |
1 5 59 15 2 16 198
|
erldi |
|
| 200 |
197 199
|
r19.29a |
|
| 201 |
1 5 58 15 2 16 67
|
erldi |
|
| 202 |
200 201
|
r19.29a |
|
| 203 |
|
plusgid |
|
| 204 |
|
snsstp2 |
|
| 205 |
204 42
|
sstri |
|
| 206 |
24
|
mpoexg |
|
| 207 |
46 46 206
|
syl2anc |
|
| 208 |
|
eqid |
|
| 209 |
35 37 203 205 207 208
|
strfv3 |
|
| 210 |
209
|
ad2antrr |
|
| 211 |
210
|
oveqd |
|
| 212 |
|
opex |
|
| 213 |
212
|
a1i |
|
| 214 |
|
simpl |
|
| 215 |
214
|
fveq2d |
|
| 216 |
|
simpr |
|
| 217 |
216
|
fveq2d |
|
| 218 |
215 217
|
oveq12d |
|
| 219 |
216
|
fveq2d |
|
| 220 |
214
|
fveq2d |
|
| 221 |
219 220
|
oveq12d |
|
| 222 |
218 221
|
oveq12d |
|
| 223 |
220 217
|
oveq12d |
|
| 224 |
222 223
|
opeq12d |
|
| 225 |
224 24
|
ovmpoga |
|
| 226 |
68 73 213 225
|
syl3anc |
|
| 227 |
211 226
|
eqtrd |
|
| 228 |
210
|
oveqd |
|
| 229 |
|
opex |
|
| 230 |
229
|
a1i |
|
| 231 |
|
simpl |
|
| 232 |
231
|
fveq2d |
|
| 233 |
|
simpr |
|
| 234 |
233
|
fveq2d |
|
| 235 |
232 234
|
oveq12d |
|
| 236 |
233
|
fveq2d |
|
| 237 |
231
|
fveq2d |
|
| 238 |
236 237
|
oveq12d |
|
| 239 |
235 238
|
oveq12d |
|
| 240 |
237 234
|
oveq12d |
|
| 241 |
239 240
|
opeq12d |
|
| 242 |
241 24
|
ovmpoga |
|
| 243 |
86 90 230 242
|
syl3anc |
|
| 244 |
228 243
|
eqtrd |
|
| 245 |
227 244
|
breq12d |
|
| 246 |
202 245
|
mpbird |
|
| 247 |
246
|
anasss |
|
| 248 |
247
|
ex |
|
| 249 |
209
|
oveqd |
|
| 250 |
249
|
ad2antrr |
|
| 251 |
|
simplr |
|
| 252 |
|
simpr |
|
| 253 |
229
|
a1i |
|
| 254 |
251 252 253 242
|
syl3anc |
|
| 255 |
63
|
ad2antrr |
|
| 256 |
65
|
ad2antrr |
|
| 257 |
251 88
|
syl |
|
| 258 |
32
|
ad2antrr |
|
| 259 |
252 92
|
syl |
|
| 260 |
258 259
|
sseldd |
|
| 261 |
1 2 256 257 260
|
ringcld |
|
| 262 |
252 96
|
syl |
|
| 263 |
251 98
|
syl |
|
| 264 |
258 263
|
sseldd |
|
| 265 |
1 2 256 262 264
|
ringcld |
|
| 266 |
1 3 255 261 265
|
grpcld |
|
| 267 |
7
|
ad2antrr |
|
| 268 |
267 263 259 107
|
syl3anc |
|
| 269 |
266 268
|
opelxpd |
|
| 270 |
254 269
|
eqeltrd |
|
| 271 |
250 270
|
eqeltrd |
|
| 272 |
271
|
anasss |
|
| 273 |
34 49 51 57 248 272 208 12
|
qusaddval |
|
| 274 |
13 14 273
|
mpd3an23 |
|
| 275 |
209
|
oveqd |
|
| 276 |
24
|
a1i |
|
| 277 |
|
simprl |
|
| 278 |
277
|
fveq2d |
|
| 279 |
8
|
adantr |
|
| 280 |
10
|
adantr |
|
| 281 |
|
op1stg |
|
| 282 |
279 280 281
|
syl2anc |
|
| 283 |
278 282
|
eqtrd |
|
| 284 |
|
simprr |
|
| 285 |
284
|
fveq2d |
|
| 286 |
9
|
adantr |
|
| 287 |
11
|
adantr |
|
| 288 |
|
op2ndg |
|
| 289 |
286 287 288
|
syl2anc |
|
| 290 |
285 289
|
eqtrd |
|
| 291 |
283 290
|
oveq12d |
|
| 292 |
284
|
fveq2d |
|
| 293 |
|
op1stg |
|
| 294 |
286 287 293
|
syl2anc |
|
| 295 |
292 294
|
eqtrd |
|
| 296 |
277
|
fveq2d |
|
| 297 |
|
op2ndg |
|
| 298 |
279 280 297
|
syl2anc |
|
| 299 |
296 298
|
eqtrd |
|
| 300 |
295 299
|
oveq12d |
|
| 301 |
291 300
|
oveq12d |
|
| 302 |
299 290
|
oveq12d |
|
| 303 |
301 302
|
opeq12d |
|
| 304 |
|
opex |
|
| 305 |
304
|
a1i |
|
| 306 |
276 303 13 14 305
|
ovmpod |
|
| 307 |
275 306
|
eqtrd |
|
| 308 |
307
|
eceq1d |
|
| 309 |
274 308
|
eqtrd |
|