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	bilani	|- ( ( ph /\ w e. T ) -> w e. ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) )
98	35 97	elrnmpt2d	|- ( ( ph /\ w e. T ) -> E. f e. ( P supp .0. ) w = <" ( P ` f ) f "> )
99	95 98	r19.29a	|- ( ( ph /\ w e. T ) -> ( w ` 1 ) e. ( P supp .0. ) )
100		fveq2	|- ( f = e -> ( P ` f ) = ( P ` e ) )
101		id	|- ( f = e -> f = e )
102	100 101	s2eqd	|- ( f = e -> <" ( P ` f ) f "> = <" ( P ` e ) e "> )
103	102	cbvmptv	|- ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) = ( e e. ( P supp .0. ) |-> <" ( P ` e ) e "> )
104		simpr	|- ( ( ph /\ e e. ( P supp .0. ) ) -> e e. ( P supp .0. ) )
105	77	adantr	|- ( ( ph /\ e e. ( P supp .0. ) ) -> P : F --> B )
106	105 87	ffvelcdmd	|- ( ( ph /\ e e. ( P supp .0. ) ) -> ( P ` e ) e. B )
107	26 69	sstrd	|- ( ph -> ( P supp .0. ) C_ B )
108	107	sselda	|- ( ( ph /\ e e. ( P supp .0. ) ) -> e e. B )
109	106 108	s2cld	|- ( ( ph /\ e e. ( P supp .0. ) ) -> <" ( P ` e ) e "> e. Word B )
110	103 104 109	elrnmpt1d	|- ( ( ph /\ e e. ( P supp .0. ) ) -> <" ( P ` e ) e "> e. ran ( f e. ( P supp .0. ) |-> <" ( P ` f ) f "> ) )
111	110 11	eleqtrrdi	|- ( ( ph /\ e e. ( P supp .0. ) ) -> <" ( P ` e ) e "> e. T )
112		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 "> )
113	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 ) )
114	112	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 ) )
115	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 )
116	113 114 115	3eqtrrd	|- ( ( ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> f = e )
117	116	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 ) )
118	117 116	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 "> )
119	112 118	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 "> )
120	98	ad4ant13	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) -> E. f e. ( P supp .0. ) w = <" ( P ` f ) f "> )
121	119 120	r19.29a	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ e = ( w ` 1 ) ) -> w = <" ( P ` e ) e "> )
122		simpr	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ w = <" ( P ` e ) e "> ) -> w = <" ( P ` e ) e "> )
123	122	fveq1d	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ w = <" ( P ` e ) e "> ) -> ( w ` 1 ) = ( <" ( P ` e ) e "> ` 1 ) )
124		s2fv1	|- ( e e. ( P supp .0. ) -> ( <" ( P ` e ) e "> ` 1 ) = e )
125	124	ad3antlr	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ w = <" ( P ` e ) e "> ) -> ( <" ( P ` e ) e "> ` 1 ) = e )
126	123 125	eqtr2d	|- ( ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) /\ w = <" ( P ` e ) e "> ) -> e = ( w ` 1 ) )
127	121 126	impbida	|- ( ( ( ph /\ e e. ( P supp .0. ) ) /\ w e. T ) -> ( e = ( w ` 1 ) <-> w = <" ( P ` e ) e "> ) )
128	111 127	reu6dv	|- ( ( ph /\ e e. ( P supp .0. ) ) -> E! w e. T e = ( w ` 1 ) )
129	82 1 3 85 58 49 86 88 99 128	gsummptf1o	|- ( ph -> ( R gsum ( e e. ( P supp .0. ) |-> ( ( P ` e ) .x. e ) ) ) = ( R gsum ( w e. T |-> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) ) ) )
130	81 129	eqtrd	|- ( ph -> ( R gsum ( e e. F |-> ( ( P ` e ) .x. e ) ) ) = ( R gsum ( w e. T |-> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) ) ) )
131	22	adantr	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> Word ( E u. F ) e. _V )
132	38	adantr	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> T C_ Word ( E u. F ) )
133		simpr	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> w e. ( Word ( E u. F ) \ T ) )
134		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 )
135	131 132 133 134	syl3anc	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) = 0 )
136	135	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 ) ) )
137		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
138	137	crngmgp	|- ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
139	5 138	syl	|- ( ph -> ( mulGrp ` R ) e. CMnd )
140	139	cmnmndd	|- ( ph -> ( mulGrp ` R ) e. Mnd )
141	76 69	unssd	|- ( ph -> ( E u. F ) C_ B )
142		sswrd	|- ( ( E u. F ) C_ B -> Word ( E u. F ) C_ Word B )
143	141 142	syl	|- ( ph -> Word ( E u. F ) C_ Word B )
144	143	ssdifssd	|- ( ph -> ( Word ( E u. F ) \ T ) C_ Word B )
145	144	sselda	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> w e. Word B )
146	137 1	mgpbas	|- B = ( Base ` ( mulGrp ` R ) )
147	146	gsumwcl	|- ( ( ( mulGrp ` R ) e. Mnd /\ w e. Word B ) -> ( ( mulGrp ` R ) gsum w ) e. B )
148	140 145 147	syl2an2r	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> ( ( mulGrp ` R ) gsum w ) e. B )
149		eqid	|- ( .g ` R ) = ( .g ` R )
150	1 3 149	mulg0	|- ( ( ( mulGrp ` R ) gsum w ) e. B -> ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
151	148 150	syl	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
152	136 151	eqtrd	|- ( ( ph /\ w e. ( Word ( E u. F ) \ T ) ) -> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
153	5	crnggrpd	|- ( ph -> R e. Grp )
154	153	adantr	|- ( ( ph /\ w e. Word ( E u. F ) ) -> R e. Grp )
155	44	ffvelcdmda	|- ( ( ph /\ w e. Word ( E u. F ) ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) e. ZZ )
156	143	sselda	|- ( ( ph /\ w e. Word ( E u. F ) ) -> w e. Word B )
157	140 156 147	syl2an2r	|- ( ( ph /\ w e. Word ( E u. F ) ) -> ( ( mulGrp ` R ) gsum w ) e. B )
158	1 149 154 155 157	mulgcld	|- ( ( ph /\ w e. Word ( E u. F ) ) -> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) e. B )
159	1 3 58 22 152 53 158 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 ) ) ) ) )
160	38 143	sstrd	|- ( ph -> T C_ Word B )
161	160	sselda	|- ( ( ph /\ w e. T ) -> w e. Word B )
162	140 161 147	syl2an2r	|- ( ( ph /\ w e. T ) -> ( ( mulGrp ` R ) gsum w ) e. B )
163	1 149	mulg1	|- ( ( ( mulGrp ` R ) gsum w ) e. B -> ( 1 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( ( mulGrp ` R ) gsum w ) )
164	162 163	syl	|- ( ( ph /\ w e. T ) -> ( 1 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( ( mulGrp ` R ) gsum w ) )
165	22	adantr	|- ( ( ph /\ w e. T ) -> Word ( E u. F ) e. _V )
166	38	adantr	|- ( ( ph /\ w e. T ) -> T C_ Word ( E u. F ) )
167		simpr	|- ( ( ph /\ w e. T ) -> w e. T )
168		ind1	|- ( ( Word ( E u. F ) e. _V /\ T C_ Word ( E u. F ) /\ w e. T ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) = 1 )
169	165 166 167 168	syl3anc	|- ( ( ph /\ w e. T ) -> ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) = 1 )
170	169	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 ) ) )
171	140	ad3antrrr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( mulGrp ` R ) e. Mnd )
172	77	ad3antrrr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> P : F --> B )
173	27	ad4ant13	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> f e. F )
174	172 173	ffvelcdmd	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( P ` f ) e. B )
175	107	ad3antrrr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( P supp .0. ) C_ B )
176	175 94	sseldd	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> f e. B )
177	137 2	mgpplusg	|- .x. = ( +g ` ( mulGrp ` R ) )
178	146 177	gsumws2	|- ( ( ( mulGrp ` R ) e. Mnd /\ ( P ` f ) e. B /\ f e. B ) -> ( ( mulGrp ` R ) gsum <" ( P ` f ) f "> ) = ( ( P ` f ) .x. f ) )
179	171 174 176 178	syl3anc	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( ( mulGrp ` R ) gsum <" ( P ` f ) f "> ) = ( ( P ` f ) .x. f ) )
180		simpr	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> w = <" ( P ` f ) f "> )
181	180	oveq2d	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( ( mulGrp ` R ) gsum w ) = ( ( mulGrp ` R ) gsum <" ( P ` f ) f "> ) )
182	93	fveq2d	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( P ` ( w ` 1 ) ) = ( P ` f ) )
183	182 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 ) )
184	179 181 183	3eqtr4rd	|- ( ( ( ( ph /\ w e. T ) /\ f e. ( P supp .0. ) ) /\ w = <" ( P ` f ) f "> ) -> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) = ( ( mulGrp ` R ) gsum w ) )
185	184 98	r19.29a	|- ( ( ph /\ w e. T ) -> ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) = ( ( mulGrp ` R ) gsum w ) )
186	164 170 185	3eqtr4d	|- ( ( ph /\ w e. T ) -> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( ( P ` ( w ` 1 ) ) .x. ( w ` 1 ) ) )
187	186	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 ) ) ) )
188	187	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 ) ) ) ) )
189	159 188	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 ) ) ) ) )
190	130 10 189	3eqtr4d	|- ( ph -> X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( ( ( _Ind ` Word ( E u. F ) ) ` T ) ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
191	16 56 190	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 ) ) ) ) )
192		breq1	|- ( h = i -> ( h finSupp 0 <-> i finSupp 0 ) )
193	192	cbvrabv	|- { h e. ( ZZ ^m Word ( E u. F ) ) | h finSupp 0 } = { i e. ( ZZ ^m Word ( E u. F ) ) | i finSupp 0 }
194	1 137 149 4 193 57 141	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 ) ) ) ) ) )
195	191 194	mpbird	|- ( ph -> X e. ( N ` ( E u. F ) ) )