Metamath Proof Explorer


Theorem elrgspnlem1

Description: Lemma for elrgspn . (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses elrgspn.b B = Base R
elrgspn.m M = mulGrp R
elrgspn.x · ˙ = R
elrgspn.n N = RingSpan R
elrgspn.f F = f Word A | finSupp 0 f
elrgspn.r φ R Ring
elrgspn.a φ A B
elrgspnlem1.1 S = ran g F R w Word A g w · ˙ M w
Assertion elrgspnlem1 φ S SubGrp R

Proof

Step Hyp Ref Expression
1 elrgspn.b B = Base R
2 elrgspn.m M = mulGrp R
3 elrgspn.x · ˙ = R
4 elrgspn.n N = RingSpan R
5 elrgspn.f F = f Word A | finSupp 0 f
6 elrgspn.r φ R Ring
7 elrgspn.a φ A B
8 elrgspnlem1.1 S = ran g F R w Word A g w · ˙ M w
9 6 ringgrpd φ R Grp
10 simpr φ x S g F x = R w Word A g w · ˙ M w x = R w Word A g w · ˙ M w
11 eqid 0 R = 0 R
12 6 ringcmnd φ R CMnd
13 12 adantr φ g F R CMnd
14 1 fvexi B V
15 14 a1i φ B V
16 15 7 ssexd φ A V
17 wrdexg A V Word A V
18 16 17 syl φ Word A V
19 18 adantr φ g F Word A V
20 9 ad2antrr φ g F w Word A R Grp
21 5 ssrab3 F Word A
22 21 a1i φ F Word A
23 22 sselda φ g F g Word A
24 zex V
25 24 a1i φ V
26 25 18 elmapd φ g Word A g : Word A
27 26 adantr φ g F g Word A g : Word A
28 23 27 mpbid φ g F g : Word A
29 28 ffvelcdmda φ g F w Word A g w
30 2 ringmgp R Ring M Mnd
31 6 30 syl φ M Mnd
32 sswrd A B Word A Word B
33 7 32 syl φ Word A Word B
34 33 sselda φ w Word A w Word B
35 2 1 mgpbas B = Base M
36 35 gsumwcl M Mnd w Word B M w B
37 31 34 36 syl2an2r φ w Word A M w B
38 37 adantlr φ g F w Word A M w B
39 1 3 20 29 38 mulgcld φ g F w Word A g w · ˙ M w B
40 39 fmpttd φ g F w Word A g w · ˙ M w : Word A B
41 fvexd φ g F 0 R V
42 0zd φ g F 0
43 ssidd φ g F Word A Word A
44 breq1 f = g finSupp 0 f finSupp 0 g
45 44 5 elrab2 g F g Word A finSupp 0 g
46 45 simprbi g F finSupp 0 g
47 46 adantl φ g F finSupp 0 g
48 1 11 3 mulg0 y B 0 · ˙ y = 0 R
49 48 adantl φ g F y B 0 · ˙ y = 0 R
50 41 42 19 43 38 28 47 49 fisuppov1 φ g F finSupp 0 R w Word A g w · ˙ M w
51 1 11 13 19 40 50 gsumcl φ g F R w Word A g w · ˙ M w B
52 51 ad4ant13 φ x S g F x = R w Word A g w · ˙ M w R w Word A g w · ˙ M w B
53 10 52 eqeltrd φ x S g F x = R w Word A g w · ˙ M w x B
54 8 eleq2i x S x ran g F R w Word A g w · ˙ M w
55 eqid g F R w Word A g w · ˙ M w = g F R w Word A g w · ˙ M w
56 55 elrnmpt x V x ran g F R w Word A g w · ˙ M w g F x = R w Word A g w · ˙ M w
57 56 elv x ran g F R w Word A g w · ˙ M w g F x = R w Word A g w · ˙ M w
58 54 57 sylbb x S g F x = R w Word A g w · ˙ M w
59 58 adantl φ x S g F x = R w Word A g w · ˙ M w
60 53 59 r19.29a φ x S x B
61 60 1 eleqtrdi φ x S x Base R
62 61 ex φ x S x Base R
63 62 ssrdv φ S Base R
64 63 1 sseqtrrdi φ S B
65 breq1 f = Word A × 0 finSupp 0 f finSupp 0 Word A × 0
66 0z 0
67 66 fconst6 Word A × 0 : Word A
68 67 a1i φ Word A × 0 : Word A
69 25 18 68 elmapdd φ Word A × 0 Word A
70 c0ex 0 V
71 70 a1i φ 0 V
72 18 71 fczfsuppd φ finSupp 0 Word A × 0
73 65 69 72 elrabd φ Word A × 0 f Word A | finSupp 0 f
74 73 5 eleqtrrdi φ Word A × 0 F
75 simplr φ g = Word A × 0 w Word A g = Word A × 0
76 75 fveq1d φ g = Word A × 0 w Word A g w = Word A × 0 w
77 70 fconst Word A × 0 : Word A 0
78 77 a1i φ g = Word A × 0 w Word A Word A × 0 : Word A 0
79 simpr φ g = Word A × 0 w Word A w Word A
80 fvconst Word A × 0 : Word A 0 w Word A Word A × 0 w = 0
81 78 79 80 syl2anc φ g = Word A × 0 w Word A Word A × 0 w = 0
82 76 81 eqtrd φ g = Word A × 0 w Word A g w = 0
83 82 oveq1d φ g = Word A × 0 w Word A g w · ˙ M w = 0 · ˙ M w
84 37 adantlr φ g = Word A × 0 w Word A M w B
85 1 11 3 mulg0 M w B 0 · ˙ M w = 0 R
86 84 85 syl φ g = Word A × 0 w Word A 0 · ˙ M w = 0 R
87 83 86 eqtrd φ g = Word A × 0 w Word A g w · ˙ M w = 0 R
88 87 mpteq2dva φ g = Word A × 0 w Word A g w · ˙ M w = w Word A 0 R
89 88 oveq2d φ g = Word A × 0 R w Word A g w · ˙ M w = R w Word A 0 R
90 12 cmnmndd φ R Mnd
91 11 gsumz R Mnd Word A V R w Word A 0 R = 0 R
92 90 18 91 syl2anc φ R w Word A 0 R = 0 R
93 92 adantr φ g = Word A × 0 R w Word A 0 R = 0 R
94 89 93 eqtrd φ g = Word A × 0 R w Word A g w · ˙ M w = 0 R
95 94 eqeq2d φ g = Word A × 0 0 R = R w Word A g w · ˙ M w 0 R = 0 R
96 eqidd φ 0 R = 0 R
97 74 95 96 rspcedvd φ g F 0 R = R w Word A g w · ˙ M w
98 fvexd φ 0 R V
99 55 97 98 elrnmptd φ 0 R ran g F R w Word A g w · ˙ M w
100 99 8 eleqtrrdi φ 0 R S
101 100 ne0d φ S
102 simpllr φ x S y S g F x = R w Word A g w · ˙ M w i F y = R w Word A i w · ˙ M w x = R w Word A g w · ˙ M w
103 simpr φ x S y S g F x = R w Word A g w · ˙ M w i F y = R w Word A i w · ˙ M w y = R w Word A i w · ˙ M w
104 102 103 oveq12d φ x S y S g F x = R w Word A g w · ˙ M w i F y = R w Word A i w · ˙ M w x + R y = R w Word A g w · ˙ M w + R R w Word A i w · ˙ M w
105 eqid + R = + R
106 13 adantr φ g F i F R CMnd
107 19 adantr φ g F i F Word A V
108 39 adantlr φ g F i F w Word A g w · ˙ M w B
109 9 ad2antrr φ i F w Word A R Grp
110 breq1 f = i finSupp 0 f finSupp 0 i
111 110 5 elrab2 i F i Word A finSupp 0 i
112 111 simplbi i F i Word A
113 112 adantl φ i F i Word A
114 25 18 elmapd φ i Word A i : Word A
115 114 adantr φ i F i Word A i : Word A
116 113 115 mpbid φ i F i : Word A
117 116 ffvelcdmda φ i F w Word A i w
118 37 adantlr φ i F w Word A M w B
119 1 3 109 117 118 mulgcld φ i F w Word A i w · ˙ M w B
120 119 adantllr φ g F i F w Word A i w · ˙ M w B
121 eqidd φ g F i F w Word A g w · ˙ M w = w Word A g w · ˙ M w
122 eqidd φ g F i F w Word A i w · ˙ M w = w Word A i w · ˙ M w
123 50 adantr φ g F i F finSupp 0 R w Word A g w · ˙ M w
124 50 ralrimiva φ g F finSupp 0 R w Word A g w · ˙ M w
125 fveq1 g = i g w = i w
126 125 oveq1d g = i g w · ˙ M w = i w · ˙ M w
127 126 mpteq2dv g = i w Word A g w · ˙ M w = w Word A i w · ˙ M w
128 127 breq1d g = i finSupp 0 R w Word A g w · ˙ M w finSupp 0 R w Word A i w · ˙ M w
129 128 cbvralvw g F finSupp 0 R w Word A g w · ˙ M w i F finSupp 0 R w Word A i w · ˙ M w
130 124 129 sylib φ i F finSupp 0 R w Word A i w · ˙ M w
131 130 r19.21bi φ i F finSupp 0 R w Word A i w · ˙ M w
132 131 adantlr φ g F i F finSupp 0 R w Word A i w · ˙ M w
133 1 11 105 106 107 108 120 121 122 123 132 gsummptfsadd φ g F i F R w Word A g w · ˙ M w + R i w · ˙ M w = R w Word A g w · ˙ M w + R R w Word A i w · ˙ M w
134 28 ffnd φ g F g Fn Word A
135 134 adantr φ g F i F g Fn Word A
136 116 ffnd φ i F i Fn Word A
137 136 adantlr φ g F i F i Fn Word A
138 inidm Word A Word A = Word A
139 eqidd φ g F i F w Word A g w = g w
140 eqidd φ g F i F w Word A i w = i w
141 135 137 107 107 138 139 140 ofval φ g F i F w Word A g + f i w = g w + i w
142 141 oveq1d φ g F i F w Word A g + f i w · ˙ M w = g w + i w · ˙ M w
143 20 adantlr φ g F i F w Word A R Grp
144 29 adantlr φ g F i F w Word A g w
145 117 adantllr φ g F i F w Word A i w
146 38 adantlr φ g F i F w Word A M w B
147 1 3 105 mulgdir R Grp g w i w M w B g w + i w · ˙ M w = g w · ˙ M w + R i w · ˙ M w
148 143 144 145 146 147 syl13anc φ g F i F w Word A g w + i w · ˙ M w = g w · ˙ M w + R i w · ˙ M w
149 142 148 eqtr2d φ g F i F w Word A g w · ˙ M w + R i w · ˙ M w = g + f i w · ˙ M w
150 149 mpteq2dva φ g F i F w Word A g w · ˙ M w + R i w · ˙ M w = w Word A g + f i w · ˙ M w
151 150 oveq2d φ g F i F R w Word A g w · ˙ M w + R i w · ˙ M w = R w Word A g + f i w · ˙ M w
152 133 151 eqtr3d φ g F i F R w Word A g w · ˙ M w + R R w Word A i w · ˙ M w = R w Word A g + f i w · ˙ M w
153 fveq1 g = h g w = h w
154 153 oveq1d g = h g w · ˙ M w = h w · ˙ M w
155 154 mpteq2dv g = h w Word A g w · ˙ M w = w Word A h w · ˙ M w
156 155 oveq2d g = h R w Word A g w · ˙ M w = R w Word A h w · ˙ M w
157 156 cbvmptv g F R w Word A g w · ˙ M w = h F R w Word A h w · ˙ M w
158 fveq1 h = g + f i h w = g + f i w
159 158 oveq1d h = g + f i h w · ˙ M w = g + f i w · ˙ M w
160 159 mpteq2dv h = g + f i w Word A h w · ˙ M w = w Word A g + f i w · ˙ M w
161 160 oveq2d h = g + f i R w Word A h w · ˙ M w = R w Word A g + f i w · ˙ M w
162 161 eqeq2d h = g + f i R w Word A g + f i w · ˙ M w = R w Word A h w · ˙ M w R w Word A g + f i w · ˙ M w = R w Word A g + f i w · ˙ M w
163 breq1 f = g + f i finSupp 0 f finSupp 0 g + f i
164 24 a1i φ g F i F V
165 zaddcl x y x + y
166 165 adantl φ g F i F x y x + y
167 28 adantr φ g F i F g : Word A
168 116 adantlr φ g F i F i : Word A
169 166 167 168 107 107 138 off φ g F i F g + f i : Word A
170 164 107 169 elmapdd φ g F i F g + f i Word A
171 zringring ring Ring
172 ringmnd ring Ring ring Mnd
173 171 172 ax-mp ring Mnd
174 173 a1i φ g F i F ring Mnd
175 23 adantr φ g F i F g Word A
176 112 adantl φ g F i F i Word A
177 47 adantr φ g F i F finSupp 0 g
178 zring0 0 = 0 ring
179 177 178 breqtrdi φ g F i F finSupp 0 ring g
180 111 simprbi i F finSupp 0 i
181 180 adantl φ g F i F finSupp 0 i
182 181 178 breqtrdi φ g F i F finSupp 0 ring i
183 zringbas = Base ring
184 183 mndpfsupp ring Mnd Word A V g Word A i Word A finSupp 0 ring g finSupp 0 ring i finSupp 0 ring g + ring f i
185 174 107 175 176 179 182 184 syl222anc φ g F i F finSupp 0 ring g + ring f i
186 zringplusg + = + ring
187 186 a1i φ g F i F + = + ring
188 187 ofeqd φ g F i F f + = f + ring
189 188 oveqd φ g F i F g + f i = g + ring f i
190 178 a1i φ g F i F 0 = 0 ring
191 185 189 190 3brtr4d φ g F i F finSupp 0 g + f i
192 163 170 191 elrabd φ g F i F g + f i f Word A | finSupp 0 f
193 192 5 eleqtrrdi φ g F i F g + f i F
194 eqidd φ g F i F R w Word A g + f i w · ˙ M w = R w Word A g + f i w · ˙ M w
195 162 193 194 rspcedvdw φ g F i F h F R w Word A g + f i w · ˙ M w = R w Word A h w · ˙ M w
196 ovexd φ g F i F R w Word A g + f i w · ˙ M w V
197 157 195 196 elrnmptd φ g F i F R w Word A g + f i w · ˙ M w ran g F R w Word A g w · ˙ M w
198 197 8 eleqtrrdi φ g F i F R w Word A g + f i w · ˙ M w S
199 152 198 eqeltrd φ g F i F R w Word A g w · ˙ M w + R R w Word A i w · ˙ M w S
200 199 adantllr φ x S g F i F R w Word A g w · ˙ M w + R R w Word A i w · ˙ M w S
201 200 adantllr φ x S y S g F i F R w Word A g w · ˙ M w + R R w Word A i w · ˙ M w S
202 201 ad4ant13 φ x S y S g F x = R w Word A g w · ˙ M w i F y = R w Word A i w · ˙ M w R w Word A g w · ˙ M w + R R w Word A i w · ˙ M w S
203 104 202 eqeltrd φ x S y S g F x = R w Word A g w · ˙ M w i F y = R w Word A i w · ˙ M w x + R y S
204 8 eleq2i y S y ran g F R w Word A g w · ˙ M w
205 127 oveq2d g = i R w Word A g w · ˙ M w = R w Word A i w · ˙ M w
206 205 cbvmptv g F R w Word A g w · ˙ M w = i F R w Word A i w · ˙ M w
207 206 elrnmpt y V y ran g F R w Word A g w · ˙ M w i F y = R w Word A i w · ˙ M w
208 207 elv y ran g F R w Word A g w · ˙ M w i F y = R w Word A i w · ˙ M w
209 204 208 sylbb y S i F y = R w Word A i w · ˙ M w
210 209 adantl φ x S y S i F y = R w Word A i w · ˙ M w
211 210 ad2antrr φ x S y S g F x = R w Word A g w · ˙ M w i F y = R w Word A i w · ˙ M w
212 203 211 r19.29a φ x S y S g F x = R w Word A g w · ˙ M w x + R y S
213 59 adantr φ x S y S g F x = R w Word A g w · ˙ M w
214 212 213 r19.29a φ x S y S x + R y S
215 214 ralrimiva φ x S y S x + R y S
216 9 ad3antrrr φ x S g F x = R w Word A g w · ˙ M w R Grp
217 29 znegcld φ g F w Word A g w
218 1 3 20 217 38 mulgcld φ g F w Word A g w · ˙ M w B
219 218 fmpttd φ g F w Word A g w · ˙ M w : Word A B
220 28 adantr φ g F w Word A g : Word A
221 simpr φ g F w Word A w Word A
222 220 221 fvco3d φ g F w Word A z z g w = z z g w
223 eqid z z = z z
224 negeq z = g w z = g w
225 223 224 29 217 fvmptd3 φ g F w Word A z z g w = g w
226 222 225 eqtrd φ g F w Word A z z g w = g w
227 226 oveq1d φ g F w Word A z z g w · ˙ M w = g w · ˙ M w
228 227 mpteq2dva φ g F w Word A z z g w · ˙ M w = w Word A g w · ˙ M w
229 simpr φ z z
230 229 znegcld φ z z
231 230 fmpttd φ z z :
232 231 adantr φ g F z z :
233 232 28 fcod φ g F z z g : Word A
234 24 a1i φ g F V
235 negeq z = 0 z = 0
236 neg0 0 = 0
237 235 236 eqtrdi z = 0 z = 0
238 0zd φ 0
239 223 237 238 238 fvmptd3 φ z z 0 = 0
240 239 adantr φ g F z z 0 = 0
241 42 28 232 19 234 47 240 fsuppco2 φ g F finSupp 0 z z g
242 41 42 19 43 38 233 241 49 fisuppov1 φ g F finSupp 0 R w Word A z z g w · ˙ M w
243 228 242 eqbrtrrd φ g F finSupp 0 R w Word A g w · ˙ M w
244 1 11 13 19 219 243 gsumcl φ g F R w Word A g w · ˙ M w B
245 244 ad4ant13 φ x S g F x = R w Word A g w · ˙ M w R w Word A g w · ˙ M w B
246 10 oveq1d φ x S g F x = R w Word A g w · ˙ M w x + R R w Word A g w · ˙ M w = R w Word A g w · ˙ M w + R R w Word A g w · ˙ M w
247 eqidd φ g F w Word A g w · ˙ M w = w Word A g w · ˙ M w
248 eqidd φ g F w Word A g w · ˙ M w = w Word A g w · ˙ M w
249 1 11 105 13 19 39 218 247 248 50 243 gsummptfsadd φ g F R w Word A g w · ˙ M w + R g w · ˙ M w = R w Word A g w · ˙ M w + R R w Word A g w · ˙ M w
250 249 ad4ant13 φ x S g F x = R w Word A g w · ˙ M w R w Word A g w · ˙ M w + R g w · ˙ M w = R w Word A g w · ˙ M w + R R w Word A g w · ˙ M w
251 29 zcnd φ g F w Word A g w
252 251 negidd φ g F w Word A g w + g w = 0
253 252 oveq1d φ g F w Word A g w + g w · ˙ M w = 0 · ˙ M w
254 1 3 105 mulgdir R Grp g w g w M w B g w + g w · ˙ M w = g w · ˙ M w + R g w · ˙ M w
255 20 29 217 38 254 syl13anc φ g F w Word A g w + g w · ˙ M w = g w · ˙ M w + R g w · ˙ M w
256 38 85 syl φ g F w Word A 0 · ˙ M w = 0 R
257 253 255 256 3eqtr3d φ g F w Word A g w · ˙ M w + R g w · ˙ M w = 0 R
258 257 mpteq2dva φ g F w Word A g w · ˙ M w + R g w · ˙ M w = w Word A 0 R
259 258 oveq2d φ g F R w Word A g w · ˙ M w + R g w · ˙ M w = R w Word A 0 R
260 92 adantr φ g F R w Word A 0 R = 0 R
261 259 260 eqtrd φ g F R w Word A g w · ˙ M w + R g w · ˙ M w = 0 R
262 261 ad4ant13 φ x S g F x = R w Word A g w · ˙ M w R w Word A g w · ˙ M w + R g w · ˙ M w = 0 R
263 246 250 262 3eqtr2d φ x S g F x = R w Word A g w · ˙ M w x + R R w Word A g w · ˙ M w = 0 R
264 eqid inv g R = inv g R
265 1 105 11 264 grpinvid1 R Grp x B R w Word A g w · ˙ M w B inv g R x = R w Word A g w · ˙ M w x + R R w Word A g w · ˙ M w = 0 R
266 265 biimpar R Grp x B R w Word A g w · ˙ M w B x + R R w Word A g w · ˙ M w = 0 R inv g R x = R w Word A g w · ˙ M w
267 216 53 245 263 266 syl31anc φ x S g F x = R w Word A g w · ˙ M w inv g R x = R w Word A g w · ˙ M w
268 fveq1 h = v Word A g v h w = v Word A g v w
269 268 oveq1d h = v Word A g v h w · ˙ M w = v Word A g v w · ˙ M w
270 269 mpteq2dv h = v Word A g v w Word A h w · ˙ M w = w Word A v Word A g v w · ˙ M w
271 270 oveq2d h = v Word A g v R w Word A h w · ˙ M w = R w Word A v Word A g v w · ˙ M w
272 271 eqeq2d h = v Word A g v R w Word A g w · ˙ M w = R w Word A h w · ˙ M w R w Word A g w · ˙ M w = R w Word A v Word A g v w · ˙ M w
273 breq1 f = v Word A g v finSupp 0 f finSupp 0 v Word A g v
274 28 ffvelcdmda φ g F v Word A g v
275 274 znegcld φ g F v Word A g v
276 275 fmpttd φ g F v Word A g v : Word A
277 234 19 276 elmapdd φ g F v Word A g v Word A
278 276 ffund φ g F Fun v Word A g v
279 134 adantr φ g F v Word A supp 0 g g Fn Word A
280 19 adantr φ g F v Word A supp 0 g Word A V
281 0zd φ g F v Word A supp 0 g 0
282 simpr φ g F v Word A supp 0 g v Word A supp 0 g
283 279 280 281 282 fvdifsupp φ g F v Word A supp 0 g g v = 0
284 283 negeqd φ g F v Word A supp 0 g g v = 0
285 284 236 eqtrdi φ g F v Word A supp 0 g g v = 0
286 285 19 suppss2 φ g F v Word A g v supp 0 g supp 0
287 277 42 278 47 286 fsuppsssuppgd φ g F finSupp 0 v Word A g v
288 273 277 287 elrabd φ g F v Word A g v f Word A | finSupp 0 f
289 288 5 eleqtrrdi φ g F v Word A g v F
290 eqid v Word A g v = v Word A g v
291 fveq2 v = w g v = g w
292 291 negeqd v = w g v = g w
293 290 292 221 217 fvmptd3 φ g F w Word A v Word A g v w = g w
294 293 eqcomd φ g F w Word A g w = v Word A g v w
295 294 oveq1d φ g F w Word A g w · ˙ M w = v Word A g v w · ˙ M w
296 295 mpteq2dva φ g F w Word A g w · ˙ M w = w Word A v Word A g v w · ˙ M w
297 296 oveq2d φ g F R w Word A g w · ˙ M w = R w Word A v Word A g v w · ˙ M w
298 272 289 297 rspcedvdw φ g F h F R w Word A g w · ˙ M w = R w Word A h w · ˙ M w
299 157 298 244 elrnmptd φ g F R w Word A g w · ˙ M w ran g F R w Word A g w · ˙ M w
300 299 8 eleqtrrdi φ g F R w Word A g w · ˙ M w S
301 300 ad4ant13 φ x S g F x = R w Word A g w · ˙ M w R w Word A g w · ˙ M w S
302 267 301 eqeltrd φ x S g F x = R w Word A g w · ˙ M w inv g R x S
303 302 59 r19.29a φ x S inv g R x S
304 215 303 jca φ x S y S x + R y S inv g R x S
305 304 ralrimiva φ x S y S x + R y S inv g R x S
306 1 105 264 issubg2 R Grp S SubGrp R S B S x S y S x + R y S inv g R x S
307 306 biimpar R Grp S B S x S y S x + R y S inv g R x S S SubGrp R
308 9 64 101 305 307 syl13anc φ S SubGrp R