Metamath Proof Explorer


Theorem elrgspnlem2

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 elrgspnlem2 φ S SubRing 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 1 2 3 4 5 6 7 8 elrgspnlem1 φ S SubGrp R
10 eqeq2 1 R = if w = 1 R 0 R v Word A if v = 1 0 w · ˙ M w = 1 R v Word A if v = 1 0 w · ˙ M w = if w = 1 R 0 R
11 eqeq2 0 R = if w = 1 R 0 R v Word A if v = 1 0 w · ˙ M w = 0 R v Word A if v = 1 0 w · ˙ M w = if w = 1 R 0 R
12 simpr φ w Word A w = w =
13 12 fveq2d φ w Word A w = v Word A if v = 1 0 w = v Word A if v = 1 0
14 eqid v Word A if v = 1 0 = v Word A if v = 1 0
15 simpr φ v = v =
16 15 iftrued φ v = if v = 1 0 = 1
17 wrd0 Word A
18 17 a1i φ Word A
19 1zzd φ 1
20 14 16 18 19 fvmptd2 φ v Word A if v = 1 0 = 1
21 20 ad2antrr φ w Word A w = v Word A if v = 1 0 = 1
22 13 21 eqtrd φ w Word A w = v Word A if v = 1 0 w = 1
23 12 oveq2d φ w Word A w = M w = M
24 eqid 1 R = 1 R
25 2 24 ringidval 1 R = 0 M
26 25 gsum0 M = 1 R
27 23 26 eqtrdi φ w Word A w = M w = 1 R
28 22 27 oveq12d φ w Word A w = v Word A if v = 1 0 w · ˙ M w = 1 · ˙ 1 R
29 1 24 ringidcl R Ring 1 R B
30 6 29 syl φ 1 R B
31 1 3 mulg1 1 R B 1 · ˙ 1 R = 1 R
32 30 31 syl φ 1 · ˙ 1 R = 1 R
33 32 ad2antrr φ w Word A w = 1 · ˙ 1 R = 1 R
34 28 33 eqtrd φ w Word A w = v Word A if v = 1 0 w · ˙ M w = 1 R
35 eqeq1 v = w v = w =
36 35 notbid v = w ¬ v = ¬ w =
37 36 biimparc ¬ w = v = w ¬ v =
38 37 adantll φ w Word A ¬ w = v = w ¬ v =
39 38 iffalsed φ w Word A ¬ w = v = w if v = 1 0 = 0
40 simplr φ w Word A ¬ w = w Word A
41 0zd φ w Word A ¬ w = 0
42 14 39 40 41 fvmptd2 φ w Word A ¬ w = v Word A if v = 1 0 w = 0
43 42 oveq1d φ w Word A ¬ w = v Word A if v = 1 0 w · ˙ M w = 0 · ˙ M w
44 2 ringmgp R Ring M Mnd
45 6 44 syl φ M Mnd
46 sswrd A B Word A Word B
47 7 46 syl φ Word A Word B
48 47 sselda φ w Word A w Word B
49 2 1 mgpbas B = Base M
50 49 gsumwcl M Mnd w Word B M w B
51 45 48 50 syl2an2r φ w Word A M w B
52 eqid 0 R = 0 R
53 1 52 3 mulg0 M w B 0 · ˙ M w = 0 R
54 51 53 syl φ w Word A 0 · ˙ M w = 0 R
55 54 adantr φ w Word A ¬ w = 0 · ˙ M w = 0 R
56 43 55 eqtrd φ w Word A ¬ w = v Word A if v = 1 0 w · ˙ M w = 0 R
57 10 11 34 56 ifbothda φ w Word A v Word A if v = 1 0 w · ˙ M w = if w = 1 R 0 R
58 57 mpteq2dva φ w Word A v Word A if v = 1 0 w · ˙ M w = w Word A if w = 1 R 0 R
59 58 oveq2d φ R w Word A v Word A if v = 1 0 w · ˙ M w = R w Word A if w = 1 R 0 R
60 6 ringcmnd φ R CMnd
61 60 cmnmndd φ R Mnd
62 1 fvexi B V
63 62 a1i φ B V
64 63 7 ssexd φ A V
65 wrdexg A V Word A V
66 64 65 syl φ Word A V
67 eqid w Word A if w = 1 R 0 R = w Word A if w = 1 R 0 R
68 30 1 eleqtrdi φ 1 R Base R
69 52 61 66 18 67 68 gsummptif1n0 φ R w Word A if w = 1 R 0 R = 1 R
70 59 69 eqtrd φ R w Word A v Word A if v = 1 0 w · ˙ M w = 1 R
71 eqid g F R w Word A g w · ˙ M w = g F R w Word A g w · ˙ M w
72 fveq1 g = v Word A if v = 1 0 g w = v Word A if v = 1 0 w
73 72 oveq1d g = v Word A if v = 1 0 g w · ˙ M w = v Word A if v = 1 0 w · ˙ M w
74 73 mpteq2dv g = v Word A if v = 1 0 w Word A g w · ˙ M w = w Word A v Word A if v = 1 0 w · ˙ M w
75 74 oveq2d g = v Word A if v = 1 0 R w Word A g w · ˙ M w = R w Word A v Word A if v = 1 0 w · ˙ M w
76 75 eqeq2d g = v Word A if v = 1 0 R w Word A v Word A if v = 1 0 w · ˙ M w = R w Word A g w · ˙ M w R w Word A v Word A if v = 1 0 w · ˙ M w = R w Word A v Word A if v = 1 0 w · ˙ M w
77 breq1 f = v Word A if v = 1 0 finSupp 0 f finSupp 0 v Word A if v = 1 0
78 zex V
79 78 a1i φ V
80 1zzd φ v Word A v = 1
81 0zd φ v Word A ¬ v = 0
82 80 81 ifclda φ v Word A if v = 1 0
83 82 fmpttd φ v Word A if v = 1 0 : Word A
84 79 66 83 elmapdd φ v Word A if v = 1 0 Word A
85 66 mptexd φ v Word A if v = 1 0 V
86 83 ffund φ Fun v Word A if v = 1 0
87 0zd φ 0
88 snfi Fin
89 88 a1i φ Fin
90 eldifsni v Word A v
91 90 adantl φ v Word A v
92 91 neneqd φ v Word A ¬ v =
93 92 iffalsed φ v Word A if v = 1 0 = 0
94 93 66 suppss2 φ v Word A if v = 1 0 supp 0
95 suppssfifsupp v Word A if v = 1 0 V Fun v Word A if v = 1 0 0 Fin v Word A if v = 1 0 supp 0 finSupp 0 v Word A if v = 1 0
96 85 86 87 89 94 95 syl32anc φ finSupp 0 v Word A if v = 1 0
97 77 84 96 elrabd φ v Word A if v = 1 0 f Word A | finSupp 0 f
98 97 5 eleqtrrdi φ v Word A if v = 1 0 F
99 eqidd φ R w Word A v Word A if v = 1 0 w · ˙ M w = R w Word A v Word A if v = 1 0 w · ˙ M w
100 76 98 99 rspcedvdw φ g F R w Word A v Word A if v = 1 0 w · ˙ M w = R w Word A g w · ˙ M w
101 ovexd φ R w Word A v Word A if v = 1 0 w · ˙ M w V
102 71 100 101 elrnmptd φ R w Word A v Word A if v = 1 0 w · ˙ M w ran g F R w Word A g w · ˙ M w
103 102 8 eleqtrrdi φ R w Word A v Word A if v = 1 0 w · ˙ M w S
104 70 103 eqeltrrd φ 1 R S
105 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
106 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
107 105 106 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
108 eqid R = R
109 66 ad2antrr φ g F i F Word A V
110 6 ad2antrr φ g F i F R Ring
111 6 ringgrpd φ R Grp
112 111 ad2antrr φ g F w Word A R Grp
113 5 ssrab3 F Word A
114 113 a1i φ F Word A
115 114 sselda φ g F g Word A
116 79 66 elmapd φ g Word A g : Word A
117 116 adantr φ g F g Word A g : Word A
118 115 117 mpbid φ g F g : Word A
119 118 ffvelcdmda φ g F w Word A g w
120 51 adantlr φ g F w Word A M w B
121 1 3 112 119 120 mulgcld φ g F w Word A g w · ˙ M w B
122 121 adantlr φ g F i F w Word A g w · ˙ M w B
123 122 ralrimiva φ g F i F w Word A g w · ˙ M w B
124 fveq2 u = w g u = g w
125 oveq2 u = w M u = M w
126 124 125 oveq12d u = w g u · ˙ M u = g w · ˙ M w
127 126 eleq1d u = w g u · ˙ M u B g w · ˙ M w B
128 127 cbvralvw u Word A g u · ˙ M u B w Word A g w · ˙ M w B
129 123 128 sylibr φ g F i F u Word A g u · ˙ M u B
130 129 r19.21bi φ g F i F u Word A g u · ˙ M u B
131 111 ad2antrr φ i F w Word A R Grp
132 breq1 f = i finSupp 0 f finSupp 0 i
133 132 5 elrab2 i F i Word A finSupp 0 i
134 133 simplbi i F i Word A
135 134 adantl φ i F i Word A
136 79 66 elmapd φ i Word A i : Word A
137 136 adantr φ i F i Word A i : Word A
138 135 137 mpbid φ i F i : Word A
139 138 ffvelcdmda φ i F w Word A i w
140 51 adantlr φ i F w Word A M w B
141 1 3 131 139 140 mulgcld φ i F w Word A i w · ˙ M w B
142 141 adantllr φ g F i F w Word A i w · ˙ M w B
143 142 ralrimiva φ g F i F w Word A i w · ˙ M w B
144 fveq2 v = w i v = i w
145 oveq2 v = w M v = M w
146 144 145 oveq12d v = w i v · ˙ M v = i w · ˙ M w
147 146 eleq1d v = w i v · ˙ M v B i w · ˙ M w B
148 147 cbvralvw v Word A i v · ˙ M v B w Word A i w · ˙ M w B
149 143 148 sylibr φ g F i F v Word A i v · ˙ M v B
150 149 r19.21bi φ g F i F v Word A i v · ˙ M v B
151 126 cbvmptv u Word A g u · ˙ M u = w Word A g w · ˙ M w
152 fvexd φ g F 0 R V
153 0zd φ g F 0
154 66 adantr φ g F Word A V
155 ssidd φ g F Word A Word A
156 breq1 f = g finSupp 0 f finSupp 0 g
157 156 5 elrab2 g F g Word A finSupp 0 g
158 157 simprbi g F finSupp 0 g
159 158 adantl φ g F finSupp 0 g
160 1 52 3 mulg0 y B 0 · ˙ y = 0 R
161 160 adantl φ g F y B 0 · ˙ y = 0 R
162 152 153 154 155 120 118 159 161 fisuppov1 φ g F finSupp 0 R w Word A g w · ˙ M w
163 162 adantr φ g F i F finSupp 0 R w Word A g w · ˙ M w
164 151 163 eqbrtrid φ g F i F finSupp 0 R u Word A g u · ˙ M u
165 146 cbvmptv v Word A i v · ˙ M v = w Word A i w · ˙ M w
166 162 ralrimiva φ g F finSupp 0 R w Word A g w · ˙ M w
167 fveq1 g = i g w = i w
168 167 oveq1d g = i g w · ˙ M w = i w · ˙ M w
169 168 mpteq2dv g = i w Word A g w · ˙ M w = w Word A i w · ˙ M w
170 169 breq1d g = i finSupp 0 R w Word A g w · ˙ M w finSupp 0 R w Word A i w · ˙ M w
171 170 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
172 166 171 sylib φ i F finSupp 0 R w Word A i w · ˙ M w
173 172 r19.21bi φ i F finSupp 0 R w Word A i w · ˙ M w
174 173 adantlr φ g F i F finSupp 0 R w Word A i w · ˙ M w
175 165 174 eqbrtrid φ g F i F finSupp 0 R v Word A i v · ˙ M v
176 1 108 52 109 109 110 130 150 164 175 gsumdixp φ g F i F R u Word A g u · ˙ M u R R v Word A i v · ˙ M v = R u Word A , v Word A g u · ˙ M u R i v · ˙ M v
177 151 oveq2i R u Word A g u · ˙ M u = R w Word A g w · ˙ M w
178 165 oveq2i R v Word A i v · ˙ M v = R w Word A i w · ˙ M w
179 177 178 oveq12i R u Word A g u · ˙ M u R R v Word A i v · ˙ M v = R w Word A g w · ˙ M w R R w Word A i w · ˙ M w
180 179 a1i φ g F i F R u Word A g u · ˙ M u R R v Word A i v · ˙ M v = R w Word A g w · ˙ M w R R w Word A i w · ˙ M w
181 110 ad2antrr φ g F i F w Word A f Word A R Ring
182 122 adantr φ g F i F w Word A f Word A g w · ˙ M w B
183 111 ad4antr φ g F i F w Word A f Word A R Grp
184 138 adantlr φ g F i F i : Word A
185 184 ffvelcdmda φ g F i F f Word A i f
186 185 adantlr φ g F i F w Word A f Word A i f
187 45 ad4antr φ g F i F w Word A f Word A M Mnd
188 47 adantr φ g F Word A Word B
189 188 ad2antrr φ g F i F w Word A Word A Word B
190 189 sselda φ g F i F w Word A f Word A f Word B
191 49 gsumwcl M Mnd f Word B M f B
192 187 190 191 syl2anc φ g F i F w Word A f Word A M f B
193 1 3 183 186 192 mulgcld φ g F i F w Word A f Word A i f · ˙ M f B
194 1 108 181 182 193 ringcld φ g F i F w Word A f Word A g w · ˙ M w R i f · ˙ M f B
195 194 anasss φ g F i F w Word A f Word A g w · ˙ M w R i f · ˙ M f B
196 195 ralrimivva φ g F i F w Word A f Word A g w · ˙ M w R i f · ˙ M f B
197 eqid w Word A , f Word A g w · ˙ M w R i f · ˙ M f = w Word A , f Word A g w · ˙ M w R i f · ˙ M f
198 197 fmpo w Word A f Word A g w · ˙ M w R i f · ˙ M f B w Word A , f Word A g w · ˙ M w R i f · ˙ M f : Word A × Word A B
199 196 198 sylib φ g F i F w Word A , f Word A g w · ˙ M w R i f · ˙ M f : Word A × Word A B
200 vex w V
201 vex f V
202 200 201 op1std a = w f 1 st a = w
203 202 fveq2d a = w f g 1 st a = g w
204 202 oveq2d a = w f M 1 st a = M w
205 203 204 oveq12d a = w f g 1 st a · ˙ M 1 st a = g w · ˙ M w
206 200 201 op2ndd a = w f 2 nd a = f
207 206 fveq2d a = w f i 2 nd a = i f
208 206 oveq2d a = w f M 2 nd a = M f
209 207 208 oveq12d a = w f i 2 nd a · ˙ M 2 nd a = i f · ˙ M f
210 205 209 oveq12d a = w f g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a = g w · ˙ M w R i f · ˙ M f
211 210 mpompt a Word A × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a = w Word A , f Word A g w · ˙ M w R i f · ˙ M f
212 66 66 xpexd φ Word A × Word A V
213 212 ad2antrr φ g F i F Word A × Word A V
214 213 mptexd φ g F i F a Word A × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a V
215 fvexd φ g F i F 0 R V
216 110 adantr φ g F i F a Word A × Word A R Ring
217 111 ad3antrrr φ g F i F a Word A × Word A R Grp
218 118 ad2antrr φ g F i F a Word A × Word A g : Word A
219 xp1st a Word A × Word A 1 st a Word A
220 219 adantl φ g F i F a Word A × Word A 1 st a Word A
221 218 220 ffvelcdmd φ g F i F a Word A × Word A g 1 st a
222 216 44 syl φ g F i F a Word A × Word A M Mnd
223 188 ad2antrr φ g F i F a Word A × Word A Word A Word B
224 223 220 sseldd φ g F i F a Word A × Word A 1 st a Word B
225 49 gsumwcl M Mnd 1 st a Word B M 1 st a B
226 222 224 225 syl2anc φ g F i F a Word A × Word A M 1 st a B
227 1 3 217 221 226 mulgcld φ g F i F a Word A × Word A g 1 st a · ˙ M 1 st a B
228 184 adantr φ g F i F a Word A × Word A i : Word A
229 xp2nd a Word A × Word A 2 nd a Word A
230 229 adantl φ g F i F a Word A × Word A 2 nd a Word A
231 228 230 ffvelcdmd φ g F i F a Word A × Word A i 2 nd a
232 223 230 sseldd φ g F i F a Word A × Word A 2 nd a Word B
233 49 gsumwcl M Mnd 2 nd a Word B M 2 nd a B
234 222 232 233 syl2anc φ g F i F a Word A × Word A M 2 nd a B
235 1 3 217 231 234 mulgcld φ g F i F a Word A × Word A i 2 nd a · ˙ M 2 nd a B
236 1 108 216 227 235 ringcld φ g F i F a Word A × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a B
237 236 fmpttd φ g F i F a Word A × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a : Word A × Word A B
238 237 ffund φ g F i F Fun a Word A × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a
239 159 fsuppimpd φ g F g supp 0 Fin
240 133 simprbi i F finSupp 0 i
241 240 adantl φ g F i F finSupp 0 i
242 241 fsuppimpd φ g F i F i supp 0 Fin
243 xpfi g supp 0 Fin i supp 0 Fin supp 0 g × supp 0 i Fin
244 239 242 243 syl2an2r φ g F i F supp 0 g × supp 0 i Fin
245 118 ffnd φ g F g Fn Word A
246 245 adantr φ g F i F g Fn Word A
247 246 ad2antrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A g Fn Word A
248 109 ad2antrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A Word A V
249 0zd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A 0
250 xp1st a Word A supp 0 g × Word A 1 st a Word A supp 0 g
251 250 adantl φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A 1 st a Word A supp 0 g
252 247 248 249 251 fvdifsupp φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A g 1 st a = 0
253 252 oveq1d φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A g 1 st a · ˙ M 1 st a = 0 · ˙ M 1 st a
254 45 ad4antr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A M Mnd
255 188 ad3antrrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A Word A Word B
256 251 eldifad φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A 1 st a Word A
257 255 256 sseldd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A 1 st a Word B
258 254 257 225 syl2anc φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A M 1 st a B
259 1 52 3 mulg0 M 1 st a B 0 · ˙ M 1 st a = 0 R
260 258 259 syl φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A 0 · ˙ M 1 st a = 0 R
261 253 260 eqtrd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A g 1 st a · ˙ M 1 st a = 0 R
262 261 oveq1d φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a = 0 R R i 2 nd a · ˙ M 2 nd a
263 110 ad2antrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A R Ring
264 111 ad4antr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A R Grp
265 184 ad2antrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A i : Word A
266 xp2nd a Word A supp 0 g × Word A 2 nd a Word A
267 266 adantl φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A 2 nd a Word A
268 265 267 ffvelcdmd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A i 2 nd a
269 255 267 sseldd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A 2 nd a Word B
270 254 269 233 syl2anc φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A M 2 nd a B
271 1 3 264 268 270 mulgcld φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A i 2 nd a · ˙ M 2 nd a B
272 1 108 52 263 271 ringlzd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A 0 R R i 2 nd a · ˙ M 2 nd a = 0 R
273 262 272 eqtrd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a = 0 R
274 138 ffnd φ i F i Fn Word A
275 274 adantlr φ g F i F i Fn Word A
276 275 ad2antrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i i Fn Word A
277 109 ad2antrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i Word A V
278 0zd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i 0
279 xp2nd a Word A × Word A supp 0 i 2 nd a Word A supp 0 i
280 279 adantl φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i 2 nd a Word A supp 0 i
281 276 277 278 280 fvdifsupp φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i i 2 nd a = 0
282 281 oveq1d φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i i 2 nd a · ˙ M 2 nd a = 0 · ˙ M 2 nd a
283 45 ad4antr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i M Mnd
284 188 ad3antrrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i Word A Word B
285 280 eldifad φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i 2 nd a Word A
286 284 285 sseldd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i 2 nd a Word B
287 283 286 233 syl2anc φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i M 2 nd a B
288 1 52 3 mulg0 M 2 nd a B 0 · ˙ M 2 nd a = 0 R
289 287 288 syl φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i 0 · ˙ M 2 nd a = 0 R
290 282 289 eqtrd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i i 2 nd a · ˙ M 2 nd a = 0 R
291 290 oveq2d φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a = g 1 st a · ˙ M 1 st a R 0 R
292 110 ad2antrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i R Ring
293 111 ad4antr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i R Grp
294 118 adantr φ g F i F g : Word A
295 294 ad2antrr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i g : Word A
296 xp1st a Word A × Word A supp 0 i 1 st a Word A
297 296 adantl φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i 1 st a Word A
298 295 297 ffvelcdmd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i g 1 st a
299 284 297 sseldd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i 1 st a Word B
300 283 299 225 syl2anc φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i M 1 st a B
301 1 3 293 298 300 mulgcld φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i g 1 st a · ˙ M 1 st a B
302 1 108 52 292 301 ringrzd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i g 1 st a · ˙ M 1 st a R 0 R = 0 R
303 291 302 eqtrd φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 i g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a = 0 R
304 simpr φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A × Word A supp 0 g × supp 0 i
305 difxp Word A × Word A supp 0 g × supp 0 i = Word A supp 0 g × Word A Word A × Word A supp 0 i
306 304 305 eleqtrdi φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A Word A × Word A supp 0 i
307 elun a Word A supp 0 g × Word A Word A × Word A supp 0 i a Word A supp 0 g × Word A a Word A × Word A supp 0 i
308 306 307 sylib φ g F i F a Word A × Word A supp 0 g × supp 0 i a Word A supp 0 g × Word A a Word A × Word A supp 0 i
309 273 303 308 mpjaodan φ g F i F a Word A × Word A supp 0 g × supp 0 i g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a = 0 R
310 309 213 suppss2 φ g F i F a Word A × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a supp 0 R supp 0 g × supp 0 i
311 244 310 ssfid φ g F i F a Word A × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a supp 0 R Fin
312 214 215 238 311 isfsuppd φ g F i F finSupp 0 R a Word A × Word A g 1 st a · ˙ M 1 st a R i 2 nd a · ˙ M 2 nd a
313 211 312 eqbrtrrid φ g F i F finSupp 0 R w Word A , f Word A g w · ˙ M w R i f · ˙ M f
314 60 ad2antrr φ g F i F R CMnd
315 7 ad2antrr φ g F i F A B
316 1 52 199 313 314 315 gsumwrd2dccat φ g F i F R w Word A , f Word A g w · ˙ M w R i f · ˙ M f = R v Word A R j = 0 v w Word A , f Word A g w · ˙ M w R i f · ˙ M f v prefix j v substr j v
317 126 oveq1d u = w g u · ˙ M u R i v · ˙ M v = g w · ˙ M w R i v · ˙ M v
318 fveq2 v = f i v = i f
319 oveq2 v = f M v = M f
320 318 319 oveq12d v = f i v · ˙ M v = i f · ˙ M f
321 320 oveq2d v = f g w · ˙ M w R i v · ˙ M v = g w · ˙ M w R i f · ˙ M f
322 317 321 cbvmpov u Word A , v Word A g u · ˙ M u R i v · ˙ M v = w Word A , f Word A g w · ˙ M w R i f · ˙ M f
323 322 oveq2i R u Word A , v Word A g u · ˙ M u R i v · ˙ M v = R w Word A , f Word A g w · ˙ M w R i f · ˙ M f
324 323 a1i φ g F i F R u Word A , v Word A g u · ˙ M u R i v · ˙ M v = R w Word A , f Word A g w · ˙ M w R i f · ˙ M f
325 pfxcctswrd v Word A j 0 v v prefix j ++ v substr j v = v
326 325 adantll φ g F i F v Word A j 0 v v prefix j ++ v substr j v = v
327 326 oveq2d φ g F i F v Word A j 0 v M v prefix j ++ v substr j v = M v
328 327 oveq2d φ g F i F v Word A j 0 v g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v = g v prefix j i v substr j v · ˙ M v
329 328 mpteq2dva φ g F i F v Word A j 0 v g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v = j 0 v g v prefix j i v substr j v · ˙ M v
330 329 oveq2d φ g F i F v Word A R j = 0 v g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v = R j = 0 v g v prefix j i v substr j v · ˙ M v
331 df-ov v prefix j w Word A , f Word A g w · ˙ M w R i f · ˙ M f v substr j v = w Word A , f Word A g w · ˙ M w R i f · ˙ M f v prefix j v substr j v
332 188 sselda φ g F w Word A w Word B
333 332 ad4ant13 φ g F i F w Word A f Word A w Word B
334 187 333 50 syl2anc φ g F i F w Word A f Word A M w B
335 1 3 108 mulgass3 R Ring i f M w B M f B M w R i f · ˙ M f = i f · ˙ M w R M f
336 181 186 334 192 335 syl13anc φ g F i F w Word A f Word A M w R i f · ˙ M f = i f · ˙ M w R M f
337 336 oveq2d φ g F i F w Word A f Word A g w · ˙ M w R i f · ˙ M f = g w · ˙ i f · ˙ M w R M f
338 119 ad4ant13 φ g F i F w Word A f Word A g w
339 1 3 108 mulgass2 R Ring g w M w B i f · ˙ M f B g w · ˙ M w R i f · ˙ M f = g w · ˙ M w R i f · ˙ M f
340 181 338 334 193 339 syl13anc φ g F i F w Word A f Word A g w · ˙ M w R i f · ˙ M f = g w · ˙ M w R i f · ˙ M f
341 1 108 181 334 192 ringcld φ g F i F w Word A f Word A M w R M f B
342 1 3 mulgass R Grp g w i f M w R M f B g w i f · ˙ M w R M f = g w · ˙ i f · ˙ M w R M f
343 183 338 186 341 342 syl13anc φ g F i F w Word A f Word A g w i f · ˙ M w R M f = g w · ˙ i f · ˙ M w R M f
344 337 340 343 3eqtr4d φ g F i F w Word A f Word A g w · ˙ M w R i f · ˙ M f = g w i f · ˙ M w R M f
345 2 108 mgpplusg R = + M
346 49 345 gsumccat M Mnd w Word B f Word B M w ++ f = M w R M f
347 187 333 190 346 syl3anc φ g F i F w Word A f Word A M w ++ f = M w R M f
348 347 oveq2d φ g F i F w Word A f Word A g w i f · ˙ M w ++ f = g w i f · ˙ M w R M f
349 344 348 eqtr4d φ g F i F w Word A f Word A g w · ˙ M w R i f · ˙ M f = g w i f · ˙ M w ++ f
350 349 adantllr φ g F i F v Word A w Word A f Word A g w · ˙ M w R i f · ˙ M f = g w i f · ˙ M w ++ f
351 350 adantllr φ g F i F v Word A j 0 v w Word A f Word A g w · ˙ M w R i f · ˙ M f = g w i f · ˙ M w ++ f
352 351 3impa φ g F i F v Word A j 0 v w Word A f Word A g w · ˙ M w R i f · ˙ M f = g w i f · ˙ M w ++ f
353 352 mpoeq3dva φ g F i F v Word A j 0 v w Word A , f Word A g w · ˙ M w R i f · ˙ M f = w Word A , f Word A g w i f · ˙ M w ++ f
354 fveq2 w = v prefix j g w = g v prefix j
355 fveq2 f = v substr j v i f = i v substr j v
356 354 355 oveqan12d w = v prefix j f = v substr j v g w i f = g v prefix j i v substr j v
357 oveq12 w = v prefix j f = v substr j v w ++ f = v prefix j ++ v substr j v
358 357 oveq2d w = v prefix j f = v substr j v M w ++ f = M v prefix j ++ v substr j v
359 356 358 oveq12d w = v prefix j f = v substr j v g w i f · ˙ M w ++ f = g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v
360 359 adantl φ g F i F v Word A j 0 v w = v prefix j f = v substr j v g w i f · ˙ M w ++ f = g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v
361 pfxcl v Word A v prefix j Word A
362 361 ad2antlr φ g F i F v Word A j 0 v v prefix j Word A
363 swrdcl v Word A v substr j v Word A
364 363 ad2antlr φ g F i F v Word A j 0 v v substr j v Word A
365 ovexd φ g F i F v Word A j 0 v g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v V
366 353 360 362 364 365 ovmpod φ g F i F v Word A j 0 v v prefix j w Word A , f Word A g w · ˙ M w R i f · ˙ M f v substr j v = g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v
367 331 366 eqtr3id φ g F i F v Word A j 0 v w Word A , f Word A g w · ˙ M w R i f · ˙ M f v prefix j v substr j v = g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v
368 367 mpteq2dva φ g F i F v Word A j 0 v w Word A , f Word A g w · ˙ M w R i f · ˙ M f v prefix j v substr j v = j 0 v g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v
369 368 oveq2d φ g F i F v Word A R j = 0 v w Word A , f Word A g w · ˙ M w R i f · ˙ M f v prefix j v substr j v = R j = 0 v g v prefix j i v substr j v · ˙ M v prefix j ++ v substr j v
370 eqid t Word A j = 0 t g t prefix j i t substr j t = t Word A j = 0 t g t prefix j i t substr j t
371 fveq2 t = v t = v
372 371 oveq2d t = v 0 t = 0 v
373 fvoveq1 t = v g t prefix j = g v prefix j
374 id t = v t = v
375 371 opeq2d t = v j t = j v
376 374 375 oveq12d t = v t substr j t = v substr j v
377 376 fveq2d t = v i t substr j t = i v substr j v
378 373 377 oveq12d t = v g t prefix j i t substr j t = g v prefix j i v substr j v
379 378 adantr t = v j 0 t g t prefix j i t substr j t = g v prefix j i v substr j v
380 372 379 sumeq12dv t = v j = 0 t g t prefix j i t substr j t = j = 0 v g v prefix j i v substr j v
381 simpr φ g F i F v Word A v Word A
382 fzfid φ g F i F v Word A 0 v Fin
383 294 ad2antrr φ g F i F v Word A j 0 v g : Word A
384 383 362 ffvelcdmd φ g F i F v Word A j 0 v g v prefix j
385 184 ad2antrr φ g F i F v Word A j 0 v i : Word A
386 385 364 ffvelcdmd φ g F i F v Word A j 0 v i v substr j v
387 384 386 zmulcld φ g F i F v Word A j 0 v g v prefix j i v substr j v
388 387 zcnd φ g F i F v Word A j 0 v g v prefix j i v substr j v
389 382 388 fsumcl φ g F i F v Word A j = 0 v g v prefix j i v substr j v
390 370 380 381 389 fvmptd3 φ g F i F v Word A t Word A j = 0 t g t prefix j i t substr j t v = j = 0 v g v prefix j i v substr j v
391 390 oveq1d φ g F i F v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = j = 0 v g v prefix j i v substr j v · ˙ M v
392 111 ad3antrrr φ g F i F v Word A R Grp
393 45 ad3antrrr φ g F i F v Word A M Mnd
394 315 46 syl φ g F i F Word A Word B
395 394 sselda φ g F i F v Word A v Word B
396 49 gsumwcl M Mnd v Word B M v B
397 393 395 396 syl2anc φ g F i F v Word A M v B
398 1 3 392 382 397 387 gsummulgc2 φ g F i F v Word A R j = 0 v g v prefix j i v substr j v · ˙ M v = j = 0 v g v prefix j i v substr j v · ˙ M v
399 391 398 eqtr4d φ g F i F v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = R j = 0 v g v prefix j i v substr j v · ˙ M v
400 330 369 399 3eqtr4rd φ g F i F v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = R j = 0 v w Word A , f Word A g w · ˙ M w R i f · ˙ M f v prefix j v substr j v
401 400 mpteq2dva φ g F i F v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = v Word A R j = 0 v w Word A , f Word A g w · ˙ M w R i f · ˙ M f v prefix j v substr j v
402 401 oveq2d φ g F i F R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = R v Word A R j = 0 v w Word A , f Word A g w · ˙ M w R i f · ˙ M f v prefix j v substr j v
403 316 324 402 3eqtr4d φ g F i F R u Word A , v Word A g u · ˙ M u R i v · ˙ M v = R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v
404 176 180 403 3eqtr3d φ g F i F R w Word A g w · ˙ M w R R w Word A i w · ˙ M w = R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v
405 fveq1 g = h g w = h w
406 405 oveq1d g = h g w · ˙ M w = h w · ˙ M w
407 406 mpteq2dv g = h w Word A g w · ˙ M w = w Word A h w · ˙ M w
408 407 oveq2d g = h R w Word A g w · ˙ M w = R w Word A h w · ˙ M w
409 408 cbvmptv g F R w Word A g w · ˙ M w = h F R w Word A h w · ˙ M w
410 fveq1 h = t Word A j = 0 t g t prefix j i t substr j t h w = t Word A j = 0 t g t prefix j i t substr j t w
411 410 oveq1d h = t Word A j = 0 t g t prefix j i t substr j t h w · ˙ M w = t Word A j = 0 t g t prefix j i t substr j t w · ˙ M w
412 411 mpteq2dv h = t Word A j = 0 t g t prefix j i t substr j t w Word A h w · ˙ M w = w Word A t Word A j = 0 t g t prefix j i t substr j t w · ˙ M w
413 412 oveq2d h = t Word A j = 0 t g t prefix j i t substr j t R w Word A h w · ˙ M w = R w Word A t Word A j = 0 t g t prefix j i t substr j t w · ˙ M w
414 413 eqeq2d h = t Word A j = 0 t g t prefix j i t substr j t R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = R w Word A h w · ˙ M w R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = R w Word A t Word A j = 0 t g t prefix j i t substr j t w · ˙ M w
415 breq1 f = t Word A j = 0 t g t prefix j i t substr j t finSupp 0 f finSupp 0 t Word A j = 0 t g t prefix j i t substr j t
416 78 a1i φ g F i F V
417 fzfid φ g F i F t Word A 0 t Fin
418 294 ad2antrr φ g F i F t Word A j 0 t g : Word A
419 pfxcl t Word A t prefix j Word A
420 419 ad2antlr φ g F i F t Word A j 0 t t prefix j Word A
421 418 420 ffvelcdmd φ g F i F t Word A j 0 t g t prefix j
422 184 ad2antrr φ g F i F t Word A j 0 t i : Word A
423 swrdcl t Word A t substr j t Word A
424 423 ad2antlr φ g F i F t Word A j 0 t t substr j t Word A
425 422 424 ffvelcdmd φ g F i F t Word A j 0 t i t substr j t
426 421 425 zmulcld φ g F i F t Word A j 0 t g t prefix j i t substr j t
427 417 426 fsumzcl φ g F i F t Word A j = 0 t g t prefix j i t substr j t
428 427 fmpttd φ g F i F t Word A j = 0 t g t prefix j i t substr j t : Word A
429 416 109 428 elmapdd φ g F i F t Word A j = 0 t g t prefix j i t substr j t Word A
430 0zd φ g F i F 0
431 428 ffund φ g F i F Fun t Word A j = 0 t g t prefix j i t substr j t
432 ccatfn ++ Fn V × V
433 fnfun ++ Fn V × V Fun ++
434 432 433 ax-mp Fun ++
435 imafi Fun ++ supp 0 g × supp 0 i Fin ++ supp 0 g × supp 0 i Fin
436 434 244 435 sylancr φ g F i F ++ supp 0 g × supp 0 i Fin
437 fveq2 t = w t = w
438 437 oveq2d t = w 0 t = 0 w
439 fvoveq1 t = w g t prefix j = g w prefix j
440 id t = w t = w
441 437 opeq2d t = w j t = j w
442 440 441 oveq12d t = w t substr j t = w substr j w
443 442 fveq2d t = w i t substr j t = i w substr j w
444 439 443 oveq12d t = w g t prefix j i t substr j t = g w prefix j i w substr j w
445 444 adantr t = w j 0 t g t prefix j i t substr j t = g w prefix j i w substr j w
446 438 445 sumeq12dv t = w j = 0 t g t prefix j i t substr j t = j = 0 w g w prefix j i w substr j w
447 oveq1 u = w prefix j u ++ v = w prefix j ++ v
448 447 eqeq2d u = w prefix j w = u ++ v w = w prefix j ++ v
449 oveq2 v = w substr j w w prefix j ++ v = w prefix j ++ w substr j w
450 449 eqeq2d v = w substr j w w = w prefix j ++ v w = w prefix j ++ w substr j w
451 246 ad4antr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 g Fn Word A
452 109 ad4antr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 Word A V
453 0zd φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 0
454 simpr φ g F i F w Word A ++ supp 0 g × supp 0 i w Word A ++ supp 0 g × supp 0 i
455 454 eldifad φ g F i F w Word A ++ supp 0 g × supp 0 i w Word A
456 455 adantr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w w Word A
457 pfxcl w Word A w prefix j Word A
458 456 457 syl φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w w prefix j Word A
459 458 ad2antrr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w prefix j Word A
460 simplr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 g w prefix j 0
461 451 452 453 459 460 elsuppfnd φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w prefix j supp 0 g
462 275 ad4antr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 i Fn Word A
463 swrdcl w Word A w substr j w Word A
464 456 463 syl φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w w substr j w Word A
465 464 ad2antrr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w substr j w Word A
466 simpr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 i w substr j w 0
467 462 452 453 465 466 elsuppfnd φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w substr j w supp 0 i
468 456 ad2antrr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w Word A
469 simpllr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 j 0 w
470 pfxcctswrd w Word A j 0 w w prefix j ++ w substr j w = w
471 468 469 470 syl2anc φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w prefix j ++ w substr j w = w
472 471 eqcomd φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w = w prefix j ++ w substr j w
473 448 450 461 467 472 2rspcedvdw φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 u supp 0 g v supp 0 i w = u ++ v
474 fnov ++ Fn V × V ++ = u V , v V u ++ v
475 432 474 mpbi ++ = u V , v V u ++ v
476 200 a1i w V
477 ssv g supp 0 V
478 477 a1i g supp 0 V
479 ssv i supp 0 V
480 479 a1i i supp 0 V
481 475 476 478 480 elimampo w ++ supp 0 g × supp 0 i u supp 0 g v supp 0 i w = u ++ v
482 481 mptru w ++ supp 0 g × supp 0 i u supp 0 g v supp 0 i w = u ++ v
483 473 482 sylibr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w ++ supp 0 g × supp 0 i
484 483 anasss φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w ++ supp 0 g × supp 0 i
485 454 ad3antrrr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 w Word A ++ supp 0 g × supp 0 i
486 485 eldifbd φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 ¬ w ++ supp 0 g × supp 0 i
487 486 anasss φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j 0 i w substr j w 0 ¬ w ++ supp 0 g × supp 0 i
488 484 487 pm2.65da φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w ¬ g w prefix j 0 i w substr j w 0
489 df-ne g w prefix j 0 ¬ g w prefix j = 0
490 df-ne i w substr j w 0 ¬ i w substr j w = 0
491 489 490 anbi12i g w prefix j 0 i w substr j w 0 ¬ g w prefix j = 0 ¬ i w substr j w = 0
492 491 notbii ¬ g w prefix j 0 i w substr j w 0 ¬ ¬ g w prefix j = 0 ¬ i w substr j w = 0
493 pm4.57 ¬ ¬ g w prefix j = 0 ¬ i w substr j w = 0 g w prefix j = 0 i w substr j w = 0
494 492 493 bitr2i g w prefix j = 0 i w substr j w = 0 ¬ g w prefix j 0 i w substr j w 0
495 488 494 sylibr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j = 0 i w substr j w = 0
496 294 ad2antrr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g : Word A
497 496 458 ffvelcdmd φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j
498 497 zcnd φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j
499 184 ad2antrr φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w i : Word A
500 499 464 ffvelcdmd φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w i w substr j w
501 500 zcnd φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w i w substr j w
502 498 501 mul0ord φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j i w substr j w = 0 g w prefix j = 0 i w substr j w = 0
503 495 502 mpbird φ g F i F w Word A ++ supp 0 g × supp 0 i j 0 w g w prefix j i w substr j w = 0
504 503 sumeq2dv φ g F i F w Word A ++ supp 0 g × supp 0 i j = 0 w g w prefix j i w substr j w = j = 0 w 0
505 fzssuz 0 w 0
506 sumz 0 w 0 0 w Fin j = 0 w 0 = 0
507 506 orcs 0 w 0 j = 0 w 0 = 0
508 505 507 mp1i φ g F i F w Word A ++ supp 0 g × supp 0 i j = 0 w 0 = 0
509 504 508 eqtrd φ g F i F w Word A ++ supp 0 g × supp 0 i j = 0 w g w prefix j i w substr j w = 0
510 446 509 sylan9eqr φ g F i F w Word A ++ supp 0 g × supp 0 i t = w j = 0 t g t prefix j i t substr j t = 0
511 0zd φ g F i F w Word A ++ supp 0 g × supp 0 i 0
512 370 510 455 511 fvmptd2 φ g F i F w Word A ++ supp 0 g × supp 0 i t Word A j = 0 t g t prefix j i t substr j t w = 0
513 428 512 suppss φ g F i F t Word A j = 0 t g t prefix j i t substr j t supp 0 ++ supp 0 g × supp 0 i
514 436 513 ssfid φ g F i F t Word A j = 0 t g t prefix j i t substr j t supp 0 Fin
515 429 430 431 514 isfsuppd φ g F i F finSupp 0 t Word A j = 0 t g t prefix j i t substr j t
516 415 429 515 elrabd φ g F i F t Word A j = 0 t g t prefix j i t substr j t f Word A | finSupp 0 f
517 516 5 eleqtrrdi φ g F i F t Word A j = 0 t g t prefix j i t substr j t F
518 fveq2 v = w t Word A j = 0 t g t prefix j i t substr j t v = t Word A j = 0 t g t prefix j i t substr j t w
519 518 145 oveq12d v = w t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = t Word A j = 0 t g t prefix j i t substr j t w · ˙ M w
520 519 cbvmptv v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = w Word A t Word A j = 0 t g t prefix j i t substr j t w · ˙ M w
521 520 oveq2i R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = R w Word A t Word A j = 0 t g t prefix j i t substr j t w · ˙ M w
522 521 a1i φ g F i F R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = R w Word A t Word A j = 0 t g t prefix j i t substr j t w · ˙ M w
523 414 517 522 rspcedvdw φ g F i F h F R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v = R w Word A h w · ˙ M w
524 ovexd φ g F i F R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v V
525 409 523 524 elrnmptd φ g F i F R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v ran g F R w Word A g w · ˙ M w
526 525 8 eleqtrrdi φ g F i F R v Word A t Word A j = 0 t g t prefix j i t substr j t v · ˙ M v S
527 404 526 eqeltrd φ g F i F R w Word A g w · ˙ M w R R w Word A i w · ˙ M w S
528 527 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
529 528 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
530 529 adantlr φ x S y S g F x = R w Word A g w · ˙ M w i F R w Word A g w · ˙ M w R R w Word A i w · ˙ M w S
531 530 adantr φ 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
532 107 531 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
533 8 eleq2i y S y ran g F R w Word A g w · ˙ M w
534 169 oveq2d g = i R w Word A g w · ˙ M w = R w Word A i w · ˙ M w
535 534 cbvmptv g F R w Word A g w · ˙ M w = i F R w Word A i w · ˙ M w
536 535 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
537 536 elv y ran g F R w Word A g w · ˙ M w i F y = R w Word A i w · ˙ M w
538 533 537 sylbb y S i F y = R w Word A i w · ˙ M w
539 538 adantl φ x S y S i F y = R w Word A i w · ˙ M w
540 539 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
541 532 540 r19.29a φ x S y S g F x = R w Word A g w · ˙ M w x R y S
542 8 eleq2i x S x ran g F R w Word A g w · ˙ M w
543 71 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
544 543 elv x ran g F R w Word A g w · ˙ M w g F x = R w Word A g w · ˙ M w
545 542 544 sylbb x S g F x = R w Word A g w · ˙ M w
546 545 ad2antlr φ x S y S g F x = R w Word A g w · ˙ M w
547 541 546 r19.29a φ x S y S x R y S
548 547 anasss φ x S y S x R y S
549 548 ralrimivva φ x S y S x R y S
550 1 24 108 issubrg2 R Ring S SubRing R S SubGrp R 1 R S x S y S x R y S
551 550 biimpar R Ring S SubGrp R 1 R S x S y S x R y S S SubRing R
552 6 9 104 549 551 syl13anc φ S SubRing R