Metamath Proof Explorer

Theorem elrgspnlem4

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 elrgspnlem4 
|- ( ph -> ( N ` A ) = S )

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 1 a1i 
 |-  ( ph -> B = ( Base ` R ) )
10 4 a1i 
 |-  ( ph -> N = ( RingSpan ` R ) )
11 eqidd 
 |-  ( ph -> ( N ` A ) = ( N ` A ) )
12 6 9 7 10 11 rgspnval 
 |-  ( ph -> ( N ` A ) = |^| { t e. ( SubRing ` R ) | A C_ t } )
13 sseq2 
 |-  ( t = S -> ( A C_ t <-> A C_ S ) )
14 1 2 3 4 5 6 7 8 elrgspnlem2 
 |-  ( ph -> S e. ( SubRing ` R ) )
15 1 2 3 4 5 6 7 8 elrgspnlem3 
 |-  ( ph -> A C_ S )
16 13 14 15 elrabd 
 |-  ( ph -> S e. { t e. ( SubRing ` R ) | A C_ t } )
17 intss1 
 |-  ( S e. { t e. ( SubRing ` R ) | A C_ t } -> |^| { t e. ( SubRing ` R ) | A C_ t } C_ S )
18 16 17 syl 
 |-  ( ph -> |^| { t e. ( SubRing ` R ) | A C_ t } C_ S )
19 simpr 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ s e. S ) /\ g e. F ) /\ s = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) -> s = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) )
20 eqidd 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) -> ( g supp 0 ) = ( g supp 0 ) )
21 oveq1 
 |-  ( f = g -> ( f supp 0 ) = ( g supp 0 ) )
22 21 eqeq1d 
 |-  ( f = g -> ( ( f supp 0 ) = ( g supp 0 ) <-> ( g supp 0 ) = ( g supp 0 ) ) )
23 fveq1 
 |-  ( f = g -> ( f ` w ) = ( g ` w ) )
24 23 oveq1d 
 |-  ( f = g -> ( ( f ` w ) .x. ( M gsum w ) ) = ( ( g ` w ) .x. ( M gsum w ) ) )
25 24 mpteq2dv 
 |-  ( f = g -> ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) = ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) )
26 25 oveq2d 
 |-  ( f = g -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) )
27 26 eleq1d 
 |-  ( f = g -> ( ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t <-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
28 22 27 imbi12d 
 |-  ( f = g -> ( ( ( f supp 0 ) = ( g supp 0 ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> ( ( g supp 0 ) = ( g supp 0 ) -> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
29 eqeq2 
 |-  ( i = (/) -> ( ( f supp 0 ) = i <-> ( f supp 0 ) = (/) ) )
30 29 imbi1d 
 |-  ( i = (/) -> ( ( ( f supp 0 ) = i -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> ( ( f supp 0 ) = (/) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
31 30 ralbidv 
 |-  ( i = (/) -> ( A. f e. F ( ( f supp 0 ) = i -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> A. f e. F ( ( f supp 0 ) = (/) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
32 eqeq2 
 |-  ( i = h -> ( ( f supp 0 ) = i <-> ( f supp 0 ) = h ) )
33 32 imbi1d 
 |-  ( i = h -> ( ( ( f supp 0 ) = i -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
34 33 ralbidv 
 |-  ( i = h -> ( A. f e. F ( ( f supp 0 ) = i -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
35 eqeq2 
 |-  ( i = ( h u. { x } ) -> ( ( f supp 0 ) = i <-> ( f supp 0 ) = ( h u. { x } ) ) )
36 35 imbi1d 
 |-  ( i = ( h u. { x } ) -> ( ( ( f supp 0 ) = i -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> ( ( f supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
37 36 ralbidv 
 |-  ( i = ( h u. { x } ) -> ( A. f e. F ( ( f supp 0 ) = i -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> A. f e. F ( ( f supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
38 eqeq2 
 |-  ( i = ( g supp 0 ) -> ( ( f supp 0 ) = i <-> ( f supp 0 ) = ( g supp 0 ) ) )
39 38 imbi1d 
 |-  ( i = ( g supp 0 ) -> ( ( ( f supp 0 ) = i -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> ( ( f supp 0 ) = ( g supp 0 ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
40 39 ralbidv 
 |-  ( i = ( g supp 0 ) -> ( A. f e. F ( ( f supp 0 ) = i -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> A. f e. F ( ( f supp 0 ) = ( g supp 0 ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
41 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
42 6 ringcmnd 
 |-  ( ph -> R e. CMnd )
43 42 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> R e. CMnd )
44 1 fvexi 
 |-  B e. _V
45 44 a1i 
 |-  ( ph -> B e. _V )
46 45 7 ssexd 
 |-  ( ph -> A e. _V )
47 wrdexg 
 |-  ( A e. _V -> Word A e. _V )
48 46 47 syl 
 |-  ( ph -> Word A e. _V )
49 48 ad5antr 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> Word A e. _V )
50 simp-4l 
 |-  ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) -> ph )
51 5 reqabi 
 |-  ( f e. F <-> ( f e. ( ZZ ^m Word A ) /\ f finSupp 0 ) )
52 51 simplbi 
 |-  ( f e. F -> f e. ( ZZ ^m Word A ) )
53 52 adantl 
 |-  ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) -> f e. ( ZZ ^m Word A ) )
54 zex 
 |-  ZZ e. _V
55 54 a1i 
 |-  ( ph -> ZZ e. _V )
56 55 48 elmapd 
 |-  ( ph -> ( f e. ( ZZ ^m Word A ) <-> f : Word A --> ZZ ) )
57 56 biimpa 
 |-  ( ( ph /\ f e. ( ZZ ^m Word A ) ) -> f : Word A --> ZZ )
58 50 53 57 syl2anc 
 |-  ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) -> f : Word A --> ZZ )
59 58 ffnd 
 |-  ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) -> f Fn Word A )
60 59 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> f Fn Word A )
61 49 adantr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> Word A e. _V )
62 0zd 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> 0 e. ZZ )
63 simpr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> w e. ( Word A \ (/) ) )
64 63 eldifad 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> w e. Word A )
65 63 eldifbd 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> -. w e. (/) )
66 simplr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> ( f supp 0 ) = (/) )
67 65 66 neleqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> -. w e. ( f supp 0 ) )
68 64 67 eldifd 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> w e. ( Word A \ ( f supp 0 ) ) )
69 60 61 62 68 fvdifsupp 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> ( f ` w ) = 0 )
70 69 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> ( ( f ` w ) .x. ( M gsum w ) ) = ( 0 .x. ( M gsum w ) ) )
71 2 ringmgp 
 |-  ( R e. Ring -> M e. Mnd )
72 6 71 syl 
 |-  ( ph -> M e. Mnd )
73 72 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> M e. Mnd )
74 sswrd 
 |-  ( A C_ B -> Word A C_ Word B )
75 7 74 syl 
 |-  ( ph -> Word A C_ Word B )
76 75 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> Word A C_ Word B )
77 76 64 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> w e. Word B )
78 2 1 mgpbas 
 |-  B = ( Base ` M )
79 78 gsumwcl 
 |-  ( ( M e. Mnd /\ w e. Word B ) -> ( M gsum w ) e. B )
80 73 77 79 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> ( M gsum w ) e. B )
81 1 41 3 mulg0 
 |-  ( ( M gsum w ) e. B -> ( 0 .x. ( M gsum w ) ) = ( 0g ` R ) )
82 80 81 syl 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> ( 0 .x. ( M gsum w ) ) = ( 0g ` R ) )
83 70 82 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. ( Word A \ (/) ) ) -> ( ( f ` w ) .x. ( M gsum w ) ) = ( 0g ` R ) )
84 0fi 
 |-  (/) e. Fin
85 84 a1i 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> (/) e. Fin )
86 6 ringgrpd 
 |-  ( ph -> R e. Grp )
87 86 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. Word A ) -> R e. Grp )
88 58 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. Word A ) -> f : Word A --> ZZ )
89 simpr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. Word A ) -> w e. Word A )
90 88 89 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. Word A ) -> ( f ` w ) e. ZZ )
91 72 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. Word A ) -> M e. Mnd )
92 75 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. Word A ) -> Word A C_ Word B )
93 92 89 sseldd 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. Word A ) -> w e. Word B )
94 91 93 79 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. Word A ) -> ( M gsum w ) e. B )
95 1 3 87 90 94 mulgcld 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) /\ w e. Word A ) -> ( ( f ` w ) .x. ( M gsum w ) ) e. B )
96 0ss 
 |-  (/) C_ Word A
97 96 a1i 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> (/) C_ Word A )
98 1 41 43 49 83 85 95 97 gsummptres2 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. (/) |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) )
99 mpt0 
 |-  ( w e. (/) |-> ( ( f ` w ) .x. ( M gsum w ) ) ) = (/)
100 99 a1i 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> ( w e. (/) |-> ( ( f ` w ) .x. ( M gsum w ) ) ) = (/) )
101 100 oveq2d 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> ( R gsum ( w e. (/) |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum (/) ) )
102 41 gsum0 
 |-  ( R gsum (/) ) = ( 0g ` R )
103 102 a1i 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> ( R gsum (/) ) = ( 0g ` R ) )
104 98 101 103 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) = ( 0g ` R ) )
105 subrgsubg 
 |-  ( t e. ( SubRing ` R ) -> t e. ( SubGrp ` R ) )
106 41 subg0cl 
 |-  ( t e. ( SubGrp ` R ) -> ( 0g ` R ) e. t )
107 105 106 syl 
 |-  ( t e. ( SubRing ` R ) -> ( 0g ` R ) e. t )
108 107 adantl 
 |-  ( ( ph /\ t e. ( SubRing ` R ) ) -> ( 0g ` R ) e. t )
109 108 ad4antr 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> ( 0g ` R ) e. t )
110 104 109 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) /\ ( f supp 0 ) = (/) ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t )
111 110 ex 
 |-  ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ f e. F ) -> ( ( f supp 0 ) = (/) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
112 111 ralrimiva 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) -> A. f e. F ( ( f supp 0 ) = (/) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
113 42 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> R e. CMnd )
114 48 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> Word A e. _V )
115 simp-5l 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) -> ph )
116 breq1 
 |-  ( f = e -> ( f finSupp 0 <-> e finSupp 0 ) )
117 116 5 elrab2 
 |-  ( e e. F <-> ( e e. ( ZZ ^m Word A ) /\ e finSupp 0 ) )
118 117 simplbi 
 |-  ( e e. F -> e e. ( ZZ ^m Word A ) )
119 55 48 elmapd 
 |-  ( ph -> ( e e. ( ZZ ^m Word A ) <-> e : Word A --> ZZ ) )
120 119 biimpa 
 |-  ( ( ph /\ e e. ( ZZ ^m Word A ) ) -> e : Word A --> ZZ )
121 118 120 sylan2 
 |-  ( ( ph /\ e e. F ) -> e : Word A --> ZZ )
122 115 121 sylancom 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) -> e : Word A --> ZZ )
123 122 adantl3r 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) -> e : Word A --> ZZ )
124 123 ffnd 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) -> e Fn Word A )
125 124 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> e Fn Word A )
126 114 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> Word A e. _V )
127 0zd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> 0 e. ZZ )
128 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> w e. ( Word A \ ( e supp 0 ) ) )
129 125 126 127 128 fvdifsupp 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> ( e ` w ) = 0 )
130 129 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> ( ( e ` w ) .x. ( M gsum w ) ) = ( 0 .x. ( M gsum w ) ) )
131 72 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> M e. Mnd )
132 75 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> Word A C_ Word B )
133 128 eldifad 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> w e. Word A )
134 132 133 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> w e. Word B )
135 131 134 79 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> ( M gsum w ) e. B )
136 135 81 syl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> ( 0 .x. ( M gsum w ) ) = ( 0g ` R ) )
137 130 136 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ ( e supp 0 ) ) ) -> ( ( e ` w ) .x. ( M gsum w ) ) = ( 0g ` R ) )
138 117 simprbi 
 |-  ( e e. F -> e finSupp 0 )
139 138 ad2antlr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> e finSupp 0 )
140 139 fsuppimpd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( e supp 0 ) e. Fin )
141 86 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> R e. Grp )
142 123 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> e : Word A --> ZZ )
143 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> w e. Word A )
144 142 143 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> ( e ` w ) e. ZZ )
145 72 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> M e. Mnd )
146 75 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> Word A C_ Word B )
147 146 sselda 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> w e. Word B )
148 145 147 79 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> ( M gsum w ) e. B )
149 1 3 141 144 148 mulgcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> ( ( e ` w ) .x. ( M gsum w ) ) e. B )
150 suppssdm 
 |-  ( e supp 0 ) C_ dom e
151 123 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> e : Word A --> ZZ )
152 150 151 fssdm 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( e supp 0 ) C_ Word A )
153 1 41 113 114 137 140 149 152 gsummptres2 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. ( e supp 0 ) |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) )
154 153 adantllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. ( e supp 0 ) |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) )
155 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( e supp 0 ) = ( h u. { x } ) )
156 155 mpteq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( w e. ( e supp 0 ) |-> ( ( e ` w ) .x. ( M gsum w ) ) ) = ( w e. ( h u. { x } ) |-> ( ( e ` w ) .x. ( M gsum w ) ) ) )
157 156 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. ( e supp 0 ) |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. ( h u. { x } ) |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) )
158 eqid 
 |-  ( +g ` R ) = ( +g ` R )
159 breq1 
 |-  ( f = g -> ( f finSupp 0 <-> g finSupp 0 ) )
160 159 5 elrab2 
 |-  ( g e. F <-> ( g e. ( ZZ ^m Word A ) /\ g finSupp 0 ) )
161 160 simprbi 
 |-  ( g e. F -> g finSupp 0 )
162 161 adantl 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) -> g finSupp 0 )
163 162 fsuppimpd 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) -> ( g supp 0 ) e. Fin )
164 163 ad4antr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( g supp 0 ) e. Fin )
165 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> h C_ ( g supp 0 ) )
166 164 165 ssfid 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> h e. Fin )
167 86 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> R e. Grp )
168 151 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> e : Word A --> ZZ )
169 suppssdm 
 |-  ( g supp 0 ) C_ dom g
170 simp-7l 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ph )
171 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> g e. F )
172 160 simplbi 
 |-  ( g e. F -> g e. ( ZZ ^m Word A ) )
173 55 48 elmapd 
 |-  ( ph -> ( g e. ( ZZ ^m Word A ) <-> g : Word A --> ZZ ) )
174 173 biimpa 
 |-  ( ( ph /\ g e. ( ZZ ^m Word A ) ) -> g : Word A --> ZZ )
175 172 174 sylan2 
 |-  ( ( ph /\ g e. F ) -> g : Word A --> ZZ )
176 170 171 175 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> g : Word A --> ZZ )
177 169 176 fssdm 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( g supp 0 ) C_ Word A )
178 165 177 sstrd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> h C_ Word A )
179 178 sselda 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> w e. Word A )
180 168 179 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> ( e ` w ) e. ZZ )
181 179 148 syldan 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> ( M gsum w ) e. B )
182 1 3 167 180 181 mulgcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> ( ( e ` w ) .x. ( M gsum w ) ) e. B )
183 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> x e. ( ( g supp 0 ) \ h ) )
184 183 eldifbd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> -. x e. h )
185 170 86 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> R e. Grp )
186 183 eldifad 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> x e. ( g supp 0 ) )
187 177 186 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> x e. Word A )
188 151 187 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( e ` x ) e. ZZ )
189 170 72 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> M e. Mnd )
190 146 187 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> x e. Word B )
191 78 gsumwcl 
 |-  ( ( M e. Mnd /\ x e. Word B ) -> ( M gsum x ) e. B )
192 189 190 191 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( M gsum x ) e. B )
193 1 3 185 188 192 mulgcld 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e ` x ) .x. ( M gsum x ) ) e. B )
194 fveq2 
 |-  ( w = x -> ( e ` w ) = ( e ` x ) )
195 oveq2 
 |-  ( w = x -> ( M gsum w ) = ( M gsum x ) )
196 194 195 oveq12d 
 |-  ( w = x -> ( ( e ` w ) .x. ( M gsum w ) ) = ( ( e ` x ) .x. ( M gsum x ) ) )
197 1 158 113 166 182 183 184 193 196 gsumunsn 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. ( h u. { x } ) |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) = ( ( R gsum ( w e. h |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) ( +g ` R ) ( ( e ` x ) .x. ( M gsum x ) ) ) )
198 197 adantllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. ( h u. { x } ) |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) = ( ( R gsum ( w e. h |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) ( +g ` R ) ( ( e ` x ) .x. ( M gsum x ) ) ) )
199 154 157 198 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) = ( ( R gsum ( w e. h |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) ( +g ` R ) ( ( e ` x ) .x. ( M gsum x ) ) ) )
200 105 ad8antlr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> t e. ( SubGrp ` R ) )
201 124 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> e Fn Word A )
202 0zd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> 0 e. ZZ )
203 201 187 202 fmptunsnop 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) )
204 203 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) )
205 204 fveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> ( ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) ` w ) = ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) )
206 eqid 
 |-  ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) = ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) )
207 eqidd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ y = x ) -> 0 = 0 )
208 201 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> e Fn Word A )
209 114 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> Word A e. _V )
210 0zd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> 0 e. ZZ )
211 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> y = w )
212 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> w e. ( Word A \ h ) )
213 212 eldifad 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> w e. Word A )
214 211 213 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> y e. Word A )
215 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> ( e supp 0 ) = ( h u. { x } ) )
216 212 eldifbd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> -. w e. h )
217 211 216 eqneltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> -. y e. h )
218 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> -. y = x )
219 218 neqned 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> y =/= x )
220 nelsn 
 |-  ( y =/= x -> -. y e. { x } )
221 219 220 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> -. y e. { x } )
222 nelun 
 |-  ( ( e supp 0 ) = ( h u. { x } ) -> ( -. y e. ( e supp 0 ) <-> ( -. y e. h /\ -. y e. { x } ) ) )
223 222 biimpar 
 |-  ( ( ( e supp 0 ) = ( h u. { x } ) /\ ( -. y e. h /\ -. y e. { x } ) ) -> -. y e. ( e supp 0 ) )
224 215 217 221 223 syl12anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> -. y e. ( e supp 0 ) )
225 214 224 eldifd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> y e. ( Word A \ ( e supp 0 ) ) )
226 208 209 210 225 fvdifsupp 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) /\ -. y = x ) -> ( e ` y ) = 0 )
227 207 226 ifeqda 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) /\ y = w ) -> if ( y = x , 0 , ( e ` y ) ) = 0 )
228 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> w e. ( Word A \ h ) )
229 228 eldifad 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> w e. Word A )
230 0zd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> 0 e. ZZ )
231 206 227 229 230 fvmptd2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> ( ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) ` w ) = 0 )
232 205 231 eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) = 0 )
233 232 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) = ( 0 .x. ( M gsum w ) ) )
234 229 148 syldan 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> ( M gsum w ) e. B )
235 234 81 syl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> ( 0 .x. ( M gsum w ) ) = ( 0g ` R ) )
236 233 235 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. ( Word A \ h ) ) -> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) = ( 0g ` R ) )
237 203 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) )
238 237 fveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> ( ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) ` w ) = ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) )
239 0zd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ y = x ) -> 0 e. ZZ )
240 151 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ -. y = x ) -> e : Word A --> ZZ )
241 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ -. y = x ) -> y e. Word A )
242 240 241 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ -. y = x ) -> ( e ` y ) e. ZZ )
243 239 242 ifclda 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) -> if ( y = x , 0 , ( e ` y ) ) e. ZZ )
244 243 fmpttd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) : Word A --> ZZ )
245 244 ffvelcdmda 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> ( ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) ` w ) e. ZZ )
246 238 245 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) e. ZZ )
247 1 3 141 246 148 mulgcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. Word A ) -> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) e. B )
248 1 41 113 114 236 166 247 178 gsummptres2 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. Word A |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. h |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) )
249 248 adantllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. Word A |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. h |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) )
250 203 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) )
251 250 fveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> ( ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) ` w ) = ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) )
252 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) /\ y = w ) -> y = w )
253 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) /\ y = w ) -> w e. h )
254 252 253 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) /\ y = w ) -> y e. h )
255 184 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) /\ y = w ) -> -. x e. h )
256 nelneq 
 |-  ( ( y e. h /\ -. x e. h ) -> -. y = x )
257 254 255 256 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) /\ y = w ) -> -. y = x )
258 257 iffalsed 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) /\ y = w ) -> if ( y = x , 0 , ( e ` y ) ) = ( e ` y ) )
259 252 fveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) /\ y = w ) -> ( e ` y ) = ( e ` w ) )
260 258 259 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) /\ y = w ) -> if ( y = x , 0 , ( e ` y ) ) = ( e ` w ) )
261 206 260 179 180 fvmptd2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> ( ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) ` w ) = ( e ` w ) )
262 251 261 eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) = ( e ` w ) )
263 262 oveq1d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ w e. h ) -> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) = ( ( e ` w ) .x. ( M gsum w ) ) )
264 263 mpteq2dva 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( w e. h |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) = ( w e. h |-> ( ( e ` w ) .x. ( M gsum w ) ) ) )
265 264 adantllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( w e. h |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) = ( w e. h |-> ( ( e ` w ) .x. ( M gsum w ) ) ) )
266 265 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. h |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. h |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) )
267 249 266 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. Word A |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. h |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) )
268 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> e e. F )
269 268 resexd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( e |` ( Word A \ { x } ) ) e. _V )
270 snex 
 |-  { <. x , 0 >. } e. _V
271 270 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> { <. x , 0 >. } e. _V )
272 269 271 202 suppun2 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) supp 0 ) = ( ( ( e |` ( Word A \ { x } ) ) supp 0 ) u. ( { <. x , 0 >. } supp 0 ) ) )
273 114 202 201 fdifsupp 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e |` ( Word A \ { x } ) ) supp 0 ) = ( ( e supp 0 ) \ { x } ) )
274 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( e supp 0 ) = ( h u. { x } ) )
275 274 difeq1d 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e supp 0 ) \ { x } ) = ( ( h u. { x } ) \ { x } ) )
276 disjsn 
 |-  ( ( h i^i { x } ) = (/) <-> -. x e. h )
277 undif5 
 |-  ( ( h i^i { x } ) = (/) -> ( ( h u. { x } ) \ { x } ) = h )
278 276 277 sylbir 
 |-  ( -. x e. h -> ( ( h u. { x } ) \ { x } ) = h )
279 184 278 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( h u. { x } ) \ { x } ) = h )
280 273 275 279 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e |` ( Word A \ { x } ) ) supp 0 ) = h )
281 vex 
 |-  x e. _V
282 c0ex 
 |-  0 e. _V
283 281 282 xpsn 
 |-  ( { x } X. { 0 } ) = { <. x , 0 >. }
284 283 oveq1i 
 |-  ( ( { x } X. { 0 } ) supp 0 ) = ( { <. x , 0 >. } supp 0 )
285 fczsupp0 
 |-  ( ( { x } X. { 0 } ) supp 0 ) = (/)
286 284 285 eqtr3i 
 |-  ( { <. x , 0 >. } supp 0 ) = (/)
287 286 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( { <. x , 0 >. } supp 0 ) = (/) )
288 280 287 uneq12d 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( ( e |` ( Word A \ { x } ) ) supp 0 ) u. ( { <. x , 0 >. } supp 0 ) ) = ( h u. (/) ) )
289 un0 
 |-  ( h u. (/) ) = h
290 289 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( h u. (/) ) = h )
291 272 288 290 3eqtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) supp 0 ) = h )
292 291 adantllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) supp 0 ) = h )
293 oveq1 
 |-  ( f = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) -> ( f supp 0 ) = ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) supp 0 ) )
294 293 eqeq1d 
 |-  ( f = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) -> ( ( f supp 0 ) = h <-> ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) supp 0 ) = h ) )
295 fveq1 
 |-  ( f = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) -> ( f ` w ) = ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) )
296 295 oveq1d 
 |-  ( f = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) -> ( ( f ` w ) .x. ( M gsum w ) ) = ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) )
297 296 mpteq2dv 
 |-  ( f = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) -> ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) = ( w e. Word A |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) )
298 297 oveq2d 
 |-  ( f = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. Word A |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) )
299 298 eleq1d 
 |-  ( f = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) -> ( ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t <-> ( R gsum ( w e. Word A |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
300 294 299 imbi12d 
 |-  ( f = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) -> ( ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
301 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
302 breq1 
 |-  ( f = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) -> ( f finSupp 0 <-> ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) finSupp 0 ) )
303 54 a1i 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ZZ e. _V )
304 114 adantllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> Word A e. _V )
305 203 adantllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) = ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) )
306 0zd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ y = x ) -> 0 e. ZZ )
307 simp-10l 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ -. y = x ) -> ph )
308 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ -. y = x ) -> e e. F )
309 307 308 121 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ -. y = x ) -> e : Word A --> ZZ )
310 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ -. y = x ) -> y e. Word A )
311 309 310 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) /\ -. y = x ) -> ( e ` y ) e. ZZ )
312 306 311 ifclda 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) /\ y e. Word A ) -> if ( y = x , 0 , ( e ` y ) ) e. ZZ )
313 312 fmpttd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( y e. Word A |-> if ( y = x , 0 , ( e ` y ) ) ) : Word A --> ZZ )
314 305 313 feq1dd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) : Word A --> ZZ )
315 303 304 314 elmapdd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) e. ( ZZ ^m Word A ) )
316 0zd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> 0 e. ZZ )
317 314 ffund 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> Fun ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) )
318 166 adantllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> h e. Fin )
319 292 318 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) supp 0 ) e. Fin )
320 315 316 317 319 isfsuppd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) finSupp 0 )
321 302 315 320 elrabd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) e. { f e. ( ZZ ^m Word A ) | f finSupp 0 } )
322 321 5 eleqtrrdi 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) e. F )
323 300 301 322 rspcdva 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
324 292 323 mpd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. Word A |-> ( ( ( ( e |` ( Word A \ { x } ) ) u. { <. x , 0 >. } ) ` w ) .x. ( M gsum w ) ) ) ) e. t )
325 267 324 eqeltrrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. h |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) e. t )
326 86 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> R e. Grp )
327 2 subrgsubm 
 |-  ( t e. ( SubRing ` R ) -> t e. ( SubMnd ` M ) )
328 327 ad8antlr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> t e. ( SubMnd ` M ) )
329 sswrd 
 |-  ( A C_ t -> Word A C_ Word t )
330 329 ad7antlr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> Word A C_ Word t )
331 187 adantllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> x e. Word A )
332 330 331 sseldd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> x e. Word t )
333 gsumwsubmcl 
 |-  ( ( t e. ( SubMnd ` M ) /\ x e. Word t ) -> ( M gsum x ) e. t )
334 328 332 333 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( M gsum x ) e. t )
335 123 ad4ant13 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> e : Word A --> ZZ )
336 335 331 ffvelcdmd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( e ` x ) e. ZZ )
337 1 3 326 334 200 336 subgmulgcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( e ` x ) .x. ( M gsum x ) ) e. t )
338 158 200 325 337 subgcld 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( ( R gsum ( w e. h |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) ( +g ` R ) ( ( e ` x ) .x. ( M gsum x ) ) ) e. t )
339 199 338 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) /\ ( e supp 0 ) = ( h u. { x } ) ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) e. t )
340 339 ex 
 |-  ( ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) /\ e e. F ) -> ( ( e supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
341 340 ralrimiva 
 |-  ( ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) /\ A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) -> A. e e. F ( ( e supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
342 341 ex 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ h C_ ( g supp 0 ) ) /\ x e. ( ( g supp 0 ) \ h ) ) -> ( A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) -> A. e e. F ( ( e supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
343 342 anasss 
 |-  ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ ( h C_ ( g supp 0 ) /\ x e. ( ( g supp 0 ) \ h ) ) ) -> ( A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) -> A. e e. F ( ( e supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
344 oveq1 
 |-  ( e = f -> ( e supp 0 ) = ( f supp 0 ) )
345 344 eqeq1d 
 |-  ( e = f -> ( ( e supp 0 ) = ( h u. { x } ) <-> ( f supp 0 ) = ( h u. { x } ) ) )
346 fveq1 
 |-  ( e = f -> ( e ` w ) = ( f ` w ) )
347 346 oveq1d 
 |-  ( e = f -> ( ( e ` w ) .x. ( M gsum w ) ) = ( ( f ` w ) .x. ( M gsum w ) ) )
348 347 mpteq2dv 
 |-  ( e = f -> ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) = ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) )
349 348 oveq2d 
 |-  ( e = f -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) = ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) )
350 349 eleq1d 
 |-  ( e = f -> ( ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) e. t <-> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
351 345 350 imbi12d 
 |-  ( e = f -> ( ( ( e supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> ( ( f supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
352 351 cbvralvw 
 |-  ( A. e e. F ( ( e supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( e ` w ) .x. ( M gsum w ) ) ) ) e. t ) <-> A. f e. F ( ( f supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
353 343 352 imbitrdi 
 |-  ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) /\ ( h C_ ( g supp 0 ) /\ x e. ( ( g supp 0 ) \ h ) ) ) -> ( A. f e. F ( ( f supp 0 ) = h -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) -> A. f e. F ( ( f supp 0 ) = ( h u. { x } ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) ) )
354 31 34 37 40 112 353 163 findcard2d 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) -> A. f e. F ( ( f supp 0 ) = ( g supp 0 ) -> ( R gsum ( w e. Word A |-> ( ( f ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
355 simpr 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) -> g e. F )
356 28 354 355 rspcdva 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) -> ( ( g supp 0 ) = ( g supp 0 ) -> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) e. t ) )
357 20 356 mpd 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ g e. F ) -> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) e. t )
358 357 ad4ant13 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ s e. S ) /\ g e. F ) /\ s = ( 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. t )
359 19 358 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ s e. S ) /\ g e. F ) /\ s = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) -> s e. t )
360 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 ) ) ) ) )
361 8 eleq2i 
 |-  ( s e. S <-> s e. ran ( g e. F |-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) )
362 361 biimpi 
 |-  ( s e. S -> s e. ran ( g e. F |-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) )
363 362 adantl 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ s e. S ) -> s e. ran ( g e. F |-> ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) ) )
364 360 363 elrnmpt2d 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ s e. S ) -> E. g e. F s = ( R gsum ( w e. Word A |-> ( ( g ` w ) .x. ( M gsum w ) ) ) ) )
365 359 364 r19.29a 
 |-  ( ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) /\ s e. S ) -> s e. t )
366 365 ex 
 |-  ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) -> ( s e. S -> s e. t ) )
367 366 ssrdv 
 |-  ( ( ( ph /\ t e. ( SubRing ` R ) ) /\ A C_ t ) -> S C_ t )
368 367 ex 
 |-  ( ( ph /\ t e. ( SubRing ` R ) ) -> ( A C_ t -> S C_ t ) )
369 368 ralrimiva 
 |-  ( ph -> A. t e. ( SubRing ` R ) ( A C_ t -> S C_ t ) )
370 ssintrab 
 |-  ( S C_ |^| { t e. ( SubRing ` R ) | A C_ t } <-> A. t e. ( SubRing ` R ) ( A C_ t -> S C_ t ) )
371 369 370 sylibr 
 |-  ( ph -> S C_ |^| { t e. ( SubRing ` R ) | A C_ t } )
372 18 371 eqssd 
 |-  ( ph -> |^| { t e. ( SubRing ` R ) | A C_ t } = S )
373 12 372 eqtrd 
 |-  ( ph -> ( N ` A ) = S )