This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrgspnlem2

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

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