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 
|- .x. = ( .g ` R )
elrgspn.n 
|- N = ( RingSpan ` R )
elrgspn.f 
|- F = { f e. ( ZZ ^m Word A ) | f finSupp 0 }
elrgspn.r 
|- ( ph -> R e. Ring )
elrgspn.a 
|- ( ph -> A C_ B )
elrgspnlem1.1 
|- S = ran ( g e. F |-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) )
Assertion elrgspnlem1 
|- ( ph -> S e. ( SubGrp ` R ) )

Proof

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