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

Metamath Proof Explorer

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