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 ) )