Theorem elrgspnsubrunlem1

Description: Lemma for elrgspnsubrun , first direction. (Contributed by Thierry Arnoux, 13-Oct-2025)

	Ref	Expression
Hypotheses	elrgspnsubrun.b	|- B = ( Base ` R )
	elrgspnsubrun.t	|- .x. = ( .r ` R )
	elrgspnsubrun.z	|- .0. = ( 0g ` R )
	elrgspnsubrun.n	|- N = ( RingSpan ` R )
	elrgspnsubrun.r	|- ( ph -> R e. CRing )
	elrgspnsubrun.e	|- ( ph -> E e. ( SubRing ` R ) )
	elrgspnsubrun.f	|- ( ph -> F e. ( SubRing ` R ) )
	elrgspnsubrunlem1.p1	|- ( ph -> P : F --> E )
	elrgspnsubrunlem1.p2	|- ( ph -> P finSupp .0. )
	elrgspnsubrunlem1.x	|- ( ph -> X = ( R gsum ( e e. F |-> ( ( P ` e ) .x. e ) ) ) )
	elrgspnsubrunlem1.t	|- T = ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> )
Assertion	elrgspnsubrunlem1	|- ( ph -> X e. ( N ` ( E u. F ) ) )

Proof

Step	Hyp	Ref	Expression
1		elrgspnsubrun.b	|- B = ( Base ` R )
2		elrgspnsubrun.t	|- .x. = ( .r ` R )
3		elrgspnsubrun.z	|- .0. = ( 0g ` R )
4		elrgspnsubrun.n	|- N = ( RingSpan ` R )
5		elrgspnsubrun.r	|- ( ph -> R e. CRing )
6		elrgspnsubrun.e	|- ( ph -> E e. ( SubRing ` R ) )
7		elrgspnsubrun.f	|- ( ph -> F e. ( SubRing ` R ) )
8		elrgspnsubrunlem1.p1	|- ( ph -> P : F --> E )
9		elrgspnsubrunlem1.p2	|- ( ph -> P finSupp .0. )
10		elrgspnsubrunlem1.x	|- ( ph -> X = ( R gsum ( e e. F |-> ( ( P ` e ) .x. e ) ) ) )
11		elrgspnsubrunlem1.t	|- T = ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> )
12		fveq1	|- ( g = ( ( _Ind ` Word ( E u. F ) ) ` T ) -> ( g ` w ) = ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) )
13	12	oveq1d	|- ( g = ( ( _Ind ` Word ( E u. F ) ) ` T ) -> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) )
14	13	mpteq2dv	|- ( g = ( ( _Ind ` Word ( E u. F ) ) ` T ) -> ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) = ( w e. Word ( E u. F ) |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) )
15	14	oveq2d	|- ( g = ( ( _Ind ` Word ( E u. F ) ) ` T ) -> ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( w e. Word ( E u. F ) |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
16	15	eqeq2d	|- ( g = ( ( _Ind ` Word ( E u. F ) ) ` T ) -> ( X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) <-> X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) )
17		breq1	|- ( h = ( ( _Ind ` Word ( E u. F ) ) ` T ) -> ( h finSupp 0 <-> ( ( _Ind ` Word ( E u. F ) ) ` T ) finSupp 0 ) )
18		zex	|- ZZ e. _V
19	18	a1i	|- ( ph -> ZZ e. _V )
20	6 7	unexd	|- ( ph -> ( E u. F ) e. _V )
21		wrdexg	|- ( ( E u. F ) e. _V -> Word ( E u. F ) e. _V )
22	20 21	syl	|- ( ph -> Word ( E u. F ) e. _V )
23		ssun1	|- E C_ ( E u. F )
24	8	adantr	|- ( ( ph /\ f e. ( P supp .0. ) ) -> P : F --> E )
25		suppssdm	|- ( P supp .0. ) C_ dom P
26	25 8	fssdm	|- ( ph -> ( P supp .0. ) C_ F )
27	26	sselda	|- ( ( ph /\ f e. ( P supp .0. ) ) -> f e. F )
28	24 27	ffvelcdmd	|- ( ( ph /\ f e. ( P supp .0. ) ) -> ( P ` f ) e. E )
29	23 28	sselid	|- ( ( ph /\ f e. ( P supp .0. ) ) -> ( P ` f ) e. ( E u. F ) )
30		ssun2	|- F C_ ( E u. F )
31	26 30	sstrdi	|- ( ph -> ( P supp .0. ) C_ ( E u. F ) )
32	31	sselda	|- ( ( ph /\ f e. ( P supp .0. ) ) -> f e. ( E u. F ) )
33	29 32	s2cld	|- ( ( ph /\ f e. ( P supp .0. ) ) -> <" ( P ` f ) f "> e. Word ( E u. F ) )
34	33	ralrimiva	|- ( ph -> A. f e. ( P supp .0. ) <" ( P ` f ) f "> e. Word ( E u. F ) )
35		eqid	|- ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) = ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> )
36	35	rnmptss	|- ( A. f e. ( P supp .0. ) <" ( P ` f ) f "> e. Word ( E u. F ) -> ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) C_ Word ( E u. F ) )
37	34 36	syl	|- ( ph -> ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) C_ Word ( E u. F ) )
38	11 37	eqsstrid	|- ( ph -> T C_ Word ( E u. F ) )
39		indf	|- ( ( Word ( E u. F ) e. _V /\ T C_ Word ( E u. F ) ) -> ( ( _Ind ` Word ( E u. F ) ) ` T ) : Word ( E u. F ) --> { 0 , 1 } )
40	22 38 39	syl2anc	|- ( ph -> ( ( _Ind ` Word ( E u. F ) ) ` T ) : Word ( E u. F ) --> { 0 , 1 } )
41		0zd	|- ( ph -> 0 e. ZZ )
42		1zzd	|- ( ph -> 1 e. ZZ )
43	41 42	prssd	|- ( ph -> { 0 , 1 } C_ ZZ )
44	40 43	fssd	|- ( ph -> ( ( _Ind ` Word ( E u. F ) ) ` T ) : Word ( E u. F ) --> ZZ )
45	19 22 44	elmapdd	|- ( ph -> ( ( _Ind ` Word ( E u. F ) ) ` T ) e. ( ZZ ^m Word ( E u. F ) ) )
46	40	ffund	|- ( ph -> Fun ( ( _Ind ` Word ( E u. F ) ) ` T ) )
47		indsupp	|- ( ( Word ( E u. F ) e. _V /\ T C_ Word ( E u. F ) ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) supp 0 ) = T )
48	22 38 47	syl2anc	|- ( ph -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) supp 0 ) = T )
49	9	fsuppimpd	|- ( ph -> ( P supp .0. ) e. Fin )
50		mptfi	|- ( ( P supp .0. ) e. Fin -> ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) e. Fin )
51		rnfi	|- ( ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) e. Fin -> ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) e. Fin )
52	49 50 51	3syl	|- ( ph -> ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) e. Fin )
53	11 52	eqeltrid	|- ( ph -> T e. Fin )
54	48 53	eqeltrd	|- ( ph -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) supp 0 ) e. Fin )
55	45 41 46 54	isfsuppd	|- ( ph -> ( ( _Ind ` Word ( E u. F ) ) ` T ) finSupp 0 )
56	17 45 55	elrabd	|- ( ph -> ( ( _Ind ` Word ( E u. F ) ) ` T ) e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } )
57	5	crngringd	|- ( ph -> R e. Ring )
58	57	ringcmnd	|- ( ph -> R e. CMnd )
59	8	ffnd	|- ( ph -> P Fn F )
60	59	adantr	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> P Fn F )
61	7	adantr	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> F e. ( SubRing ` R ) )
62	3	fvexi	|- .0. e. _V
63	62	a1i	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> .0. e. _V )
64		simpr	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> e e. ( F \ ( P supp .0. ) ) )
65	60 61 63 64	fvdifsupp	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> ( P ` e ) = .0. )
66	65	oveq1d	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> ( ( P ` e ) .x. e ) = ( .0. .x. e ) )
67	57	adantr	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> R e. Ring )
68	1	subrgss	|- ( F e. ( SubRing ` R ) -> F C_ B )
69	7 68	syl	|- ( ph -> F C_ B )
70	69	ssdifssd	|- ( ph -> ( F \ ( P supp .0. ) ) C_ B )
71	70	sselda	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> e e. B )
72	1 2 3 67 71	ringlzd	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> ( .0. .x. e ) = .0. )
73	66 72	eqtrd	|- ( ( ph /\ e e. ( F \ ( P supp .0. ) ) ) -> ( ( P ` e ) .x. e ) = .0. )
74	57	adantr	|- ( ( ph /\ e e. F ) -> R e. Ring )
75	1	subrgss	|- ( E e. ( SubRing ` R ) -> E C_ B )
76	6 75	syl	|- ( ph -> E C_ B )
77	8 76	fssd	|- ( ph -> P : F --> B )
78	77	ffvelcdmda	|- ( ( ph /\ e e. F ) -> ( P ` e ) e. B )
79	69	sselda	|- ( ( ph /\ e e. F ) -> e e. B )
80	1 2 74 78 79	ringcld	|- ( ( ph /\ e e. F ) -> ( ( P ` e ) .x. e ) e. B )
81	1 3 58 7 73 49 80 26	gsummptres2	|- ( ph -> ( R gsum ( e e. F |-> ( ( P ` e ) .x. e ) ) ) = ( R gsum ( e e. ( P supp .0. ) |-> ( ( P ` e ) .x. e ) ) ) )
82		nfcv	|- F/_ e ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) )
83		fveq2	|- ( e = ( w ` 1 ) -> ( P ` e ) = ( P ` ( w ` 1 ) ) )
84		id	|- ( e = ( w ` 1 ) -> e = ( w ` 1 ) )
85	83 84	oveq12d	|- ( e = ( w ` 1 ) -> ( ( P ` e ) .x. e ) = ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) )
86		ssidd	|- ( ph -> B C_ B )
87	26	sselda	|- ( ( ph /\ e e. ( P supp .0. ) ) -> e e. F )
88	87 80	syldan	|- ( ( ph /\ e e. ( P supp .0. ) ) -> ( ( P ` e ) .x. e ) e. B )
89		fveq1	|- ( w = <" ( P ` f ) f "> -> ( w ` 1 ) = ( <" ( P ` f ) f "> ` 1 ) )
90	89	adantl	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( w ` 1 ) = ( <" ( P ` f ) f "> ` 1 ) )
91		s2fv1	|- ( f e. ( P supp .0. ) -> ( <" ( P ` f ) f "> ` 1 ) = f )
92	91	ad2antlr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( <" ( P ` f ) f "> ` 1 ) = f )
93	90 92	eqtrd	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( w ` 1 ) = f )
94		simplr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> f e. ( P supp .0. ) )
95	93 94	eqeltrd	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( w ` 1 ) e. ( P supp .0. ) )
96	11	eleq2i	|- ( w e. T <-> w e. ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) )
97	96	biimpi	|- ( w e. T -> w e. ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) )
98	97	adantl	|- ( ( ph /\ w e. T ) -> w e. ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) )
99	35 98	elrnmpt2d	|- ( ( ph /\ w e. T ) -> E. f e. ( P supp .0. ) w = <" ( P ` f ) f "> )
100	95 99	r19.29a	|- ( ( ph /\ w e. T ) -> ( w ` 1 ) e. ( P supp .0. ) )
101		fveq2	|- ( f = e -> ( P ` f ) = ( P ` e ) )
102		id	|- ( f = e -> f = e )
103	101 102	s2eqd	|- ( f = e -> <" ( P ` f ) f "> = <" ( P ` e ) e "> )
104	103	cbvmptv	|- ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) = ( e e. ( P supp .0. ) |-> <" ( P ` e ) e "> )
105		simpr	|- ( ( ph /\ e e. ( P supp .0. ) ) -> e e. ( P supp .0. ) )
106	77	adantr	|- ( ( ph /\ e e. ( P supp .0. ) ) -> P : F --> B )
107	106 87	ffvelcdmd	|- ( ( ph /\ e e. ( P supp .0. ) ) -> ( P ` e ) e. B )
108	26 69	sstrd	|- ( ph -> ( P supp .0. ) C_ B )
109	108	sselda	|- ( ( ph /\ e e. ( P supp .0. ) ) -> e e. B )
110	107 109	s2cld	|- ( ( ph /\ e e. ( P supp .0. ) ) -> <" ( P ` e ) e "> e. Word B )
111	104 105 110	elrnmpt1d	|- ( ( ph /\ e e. ( P supp .0. ) ) -> <" ( P ` e ) e "> e. ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) )
112	111 11	eleqtrrdi	|- ( ( ph /\ e e. ( P supp .0. ) ) -> <" ( P ` e ) e "> e. T )
113		simpr	|- ( ( ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> w = <" ( P ` f ) f "> )
114	84	ad3antlr	|- ( ( ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> e = ( w ` 1 ) )
115	113	fveq1d	|- ( ( ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( w ` 1 ) = ( <" ( P ` f ) f "> ` 1 ) )
116	91	ad2antlr	|- ( ( ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( <" ( P ` f ) f "> ` 1 ) = f )
117	114 115 116	3eqtrrd	|- ( ( ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> f = e )
118	117	fveq2d	|- ( ( ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( P ` f ) = ( P ` e ) )
119	118 117	s2eqd	|- ( ( ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> <" ( P ` f ) f "> = <" ( P ` e ) e "> )
120	113 119	eqtrd	|- ( ( ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> w = <" ( P ` e ) e "> )
121	99	ad4ant13	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) -> E. f e. ( P supp .0. ) w = <" ( P ` f ) f "> )
122	120 121	r19.29a	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) -> w = <" ( P ` e ) e "> )
123		simpr	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ w = <" ( P ` e ) e "> ) -> w = <" ( P ` e ) e "> )
124	123	fveq1d	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ w = <" ( P ` e ) e "> ) -> ( w ` 1 ) = ( <" ( P ` e ) e "> ` 1 ) )
125		s2fv1	|- ( e e. ( P supp .0. ) -> ( <" ( P ` e ) e "> ` 1 ) = e )
126	125	ad3antlr	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ w = <" ( P ` e ) e "> ) -> ( <" ( P ` e ) e "> ` 1 ) = e )
127	124 126	eqtr2d	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ w = <" ( P ` e ) e "> ) -> e = ( w ` 1 ) )
128	122 127	impbida	|- ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) -> ( e = ( w ` 1 ) <-> w = <" ( P ` e ) e "> ) )
129	112 128	reu6dv	|- ( ( ph /\ e e. ( P supp .0. ) ) -> E! w e. T e = ( w ` 1 ) )
130	82 1 3 85 58 49 86 88 100 129	gsummptf1o	|- ( ph -> ( R gsum ( e e. ( P supp .0. ) |-> ( ( P ` e ) .x. e ) ) ) = ( R gsum ( w e. T |-> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) ) ) )
131	81 130	eqtrd	|- ( ph -> ( R gsum ( e e. F |-> ( ( P ` e ) .x. e ) ) ) = ( R gsum ( w e. T |-> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) ) ) )
132	22	adantr	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> Word ( E u. F ) e. _V )
133	38	adantr	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> T C_ Word ( E u. F ) )
134		simpr	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> w e. ( Word ( E u. F ) \ T ) )
135		ind0	|- ( ( Word ( E u. F ) e. _V /\ T C_ Word ( E u. F ) /\ w e. ( Word ( E u. F ) \ T ) ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) = 0 )
136	132 133 134 135	syl3anc	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) = 0 )
137	136	oveq1d	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) )
138		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
139	138	crngmgp	|- ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
140	5 139	syl	|- ( ph -> ( mulGrp ` R ) e. CMnd )
141	140	cmnmndd	|- ( ph -> ( mulGrp ` R ) e. Mnd )
142	76 69	unssd	|- ( ph -> ( E u. F ) C_ B )
143		sswrd	|- ( ( E u. F ) C_ B -> Word ( E u. F ) C_ Word B )
144	142 143	syl	|- ( ph -> Word ( E u. F ) C_ Word B )
145	144	ssdifssd	|- ( ph -> ( Word ( E u. F ) \ T ) C_ Word B )
146	145	sselda	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> w e. Word B )
147	138 1	mgpbas	|- B = ( Base ` ( mulGrp ` R ) )
148	147	gsumwcl	|- ( ( ( mulGrp ` R ) e. Mnd /\ w e. Word B ) -> ( ( mulGrp ` R ) gsum w ) e. B )
149	141 146 148	syl2an2r	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> ( ( mulGrp ` R ) gsum w ) e. B )
150		eqid	|- ( .g ` R ) = ( .g ` R )
151	1 3 150	mulg0	|- ( ( ( mulGrp ` R ) gsum w ) e. B -> ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
152	149 151	syl	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
153	137 152	eqtrd	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
154	5	crnggrpd	|- ( ph -> R e. Grp )
155	154	adantr	|- ( ( ph /\ w e. Word ( E u. F ) ) -> R e. Grp )
156	44	ffvelcdmda	|- ( ( ph /\ w e. Word ( E u. F ) ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) e. ZZ )
157	144	sselda	|- ( ( ph /\ w e. Word ( E u. F ) ) -> w e. Word B )
158	141 157 148	syl2an2r	|- ( ( ph /\ w e. Word ( E u. F ) ) -> ( ( mulGrp ` R ) gsum w ) e. B )
159	1 150 155 156 158	mulgcld	|- ( ( ph /\ w e. Word ( E u. F ) ) -> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) e. B )
160	1 3 58 22 153 53 159 38	gsummptres2	|- ( ph -> ( R gsum ( w e. Word ( E u. F ) |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( w e. T |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
161	38 144	sstrd	|- ( ph -> T C_ Word B )
162	161	sselda	|- ( ( ph /\ w e. T ) -> w e. Word B )
163	141 162 148	syl2an2r	|- ( ( ph /\ w e. T ) -> ( ( mulGrp ` R ) gsum w ) e. B )
164	1 150	mulg1	|- ( ( ( mulGrp ` R ) gsum w ) e. B -> ( 1 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( ( mulGrp ` R ) gsum w ) )
165	163 164	syl	|- ( ( ph /\ w e. T ) -> ( 1 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( ( mulGrp ` R ) gsum w ) )
166	22	adantr	|- ( ( ph /\ w e. T ) -> Word ( E u. F ) e. _V )
167	38	adantr	|- ( ( ph /\ w e. T ) -> T C_ Word ( E u. F ) )
168		simpr	|- ( ( ph /\ w e. T ) -> w e. T )
169		ind1	|- ( ( Word ( E u. F ) e. _V /\ T C_ Word ( E u. F ) /\ w e. T ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) = 1 )
170	166 167 168 169	syl3anc	|- ( ( ph /\ w e. T ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) = 1 )
171	170	oveq1d	|- ( ( ph /\ w e. T ) -> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( 1 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) )
172	141	ad3antrrr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( mulGrp ` R ) e. Mnd )
173	77	ad3antrrr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> P : F --> B )
174	27	ad4ant13	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> f e. F )
175	173 174	ffvelcdmd	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( P ` f ) e. B )
176	108	ad3antrrr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( P supp .0. ) C_ B )
177	176 94	sseldd	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> f e. B )
178	138 2	mgpplusg	|- .x. = ( +g ` ( mulGrp ` R ) )
179	147 178	gsumws2	|- ( ( ( mulGrp ` R ) e. Mnd /\ ( P ` f ) e. B /\ f e. B ) -> ( ( mulGrp ` R ) gsum <" ( P ` f ) f "> ) = ( ( P ` f ) .x. f ) )
180	172 175 177 179	syl3anc	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( ( mulGrp ` R ) gsum <" ( P ` f ) f "> ) = ( ( P ` f ) .x. f ) )
181		simpr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> w = <" ( P ` f ) f "> )
182	181	oveq2d	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( ( mulGrp ` R ) gsum w ) = ( ( mulGrp ` R ) gsum <" ( P ` f ) f "> ) )
183	93	fveq2d	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( P ` ( w ` 1 ) ) = ( P ` f ) )
184	183 93	oveq12d	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) = ( ( P ` f ) .x. f ) )
185	180 182 184	3eqtr4rd	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) = ( ( mulGrp ` R ) gsum w ) )
186	185 99	r19.29a	|- ( ( ph /\ w e. T ) -> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) = ( ( mulGrp ` R ) gsum w ) )
187	165 171 186	3eqtr4d	|- ( ( ph /\ w e. T ) -> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) )
188	187	mpteq2dva	|- ( ph -> ( w e. T |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) = ( w e. T |-> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) ) )
189	188	oveq2d	|- ( ph -> ( R gsum ( w e. T |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( w e. T |-> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) ) ) )
190	160 189	eqtrd	|- ( ph -> ( R gsum ( w e. Word ( E u. F ) |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( w e. T |-> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) ) ) )
191	131 10 190	3eqtr4d	|- ( ph -> X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
192	16 56 191	rspcedvdw	|- ( ph -> E. g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
193		breq1	|- ( h = i -> ( h finSupp 0 <-> i finSupp 0 ) )
194	193	cbvrabv	|- { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } = { i e. ( ZZ ^m Word ( E u. F ) ) | i finSupp 0 }
195	1 138 150 4 194 57 142	elrgspn	|- ( ph -> ( X e. ( N ` ( E u. F ) ) <-> E. g e. { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( g ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) )
196	192 195	mpbird	|- ( ph -> X e. ( N ` ( E u. F ) ) )