Metamath Proof Explorer

Theorem frgpup3lem

Description: The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses frgpup.b 
|- B = ( Base ` H )
frgpup.n 
|- N = ( invg ` H )
frgpup.t 
|- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )
frgpup.h 
|- ( ph -> H e. Grp )
frgpup.i 
|- ( ph -> I e. V )
frgpup.a 
|- ( ph -> F : I --> B )
frgpup.w 
|- W = ( _I ` Word ( I X. 2o ) )
frgpup.r 
|- .~ = ( ~FG ` I )
frgpup.g 
|- G = ( freeGrp ` I )
frgpup.x 
|- X = ( Base ` G )
frgpup.e 
|- E = ran ( g e. W |-> <. [ g ] .~ , ( H gsum ( T o. g ) ) >. )
frgpup.u 
|- U = ( varFGrp ` I )
frgpup3.k 
|- ( ph -> K e. ( G GrpHom H ) )
frgpup3.e 
|- ( ph -> ( K o. U ) = F )
Assertion frgpup3lem 
|- ( ph -> K = E )

Proof

Step Hyp Ref Expression
1 frgpup.b 
 |-  B = ( Base ` H )
2 frgpup.n 
 |-  N = ( invg ` H )
3 frgpup.t 
 |-  T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )
4 frgpup.h 
 |-  ( ph -> H e. Grp )
5 frgpup.i 
 |-  ( ph -> I e. V )
6 frgpup.a 
 |-  ( ph -> F : I --> B )
7 frgpup.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
8 frgpup.r 
 |-  .~ = ( ~FG ` I )
9 frgpup.g 
 |-  G = ( freeGrp ` I )
10 frgpup.x 
 |-  X = ( Base ` G )
11 frgpup.e 
 |-  E = ran ( g e. W |-> <. [ g ] .~ , ( H gsum ( T o. g ) ) >. )
12 frgpup.u 
 |-  U = ( varFGrp ` I )
13 frgpup3.k 
 |-  ( ph -> K e. ( G GrpHom H ) )
14 frgpup3.e 
 |-  ( ph -> ( K o. U ) = F )
15 10 1 ghmf 
 |-  ( K e. ( G GrpHom H ) -> K : X --> B )
16 ffn 
 |-  ( K : X --> B -> K Fn X )
17 13 15 16 3syl 
 |-  ( ph -> K Fn X )
18 1 2 3 4 5 6 7 8 9 10 11 frgpup1 
 |-  ( ph -> E e. ( G GrpHom H ) )
19 10 1 ghmf 
 |-  ( E e. ( G GrpHom H ) -> E : X --> B )
20 ffn 
 |-  ( E : X --> B -> E Fn X )
21 18 19 20 3syl 
 |-  ( ph -> E Fn X )
22 eqid 
 |-  ( freeMnd ` ( I X. 2o ) ) = ( freeMnd ` ( I X. 2o ) )
23 9 22 8 frgpval 
 |-  ( I e. V -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) )
24 5 23 syl 
 |-  ( ph -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) )
25 2on 
 |-  2o e. On
26 xpexg 
 |-  ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
27 5 25 26 sylancl 
 |-  ( ph -> ( I X. 2o ) e. _V )
28 wrdexg 
 |-  ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V )
29 fvi 
 |-  ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
30 27 28 29 3syl 
 |-  ( ph -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
31 7 30 syl5eq 
 |-  ( ph -> W = Word ( I X. 2o ) )
32 eqid 
 |-  ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) )
33 22 32 frmdbas 
 |-  ( ( I X. 2o ) e. _V -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
34 27 33 syl 
 |-  ( ph -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
35 31 34 eqtr4d 
 |-  ( ph -> W = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
36 8 fvexi 
 |-  .~ e. _V
37 36 a1i 
 |-  ( ph -> .~ e. _V )
38 fvexd 
 |-  ( ph -> ( freeMnd ` ( I X. 2o ) ) e. _V )
39 24 35 37 38 qusbas 
 |-  ( ph -> ( W /. .~ ) = ( Base ` G ) )
40 10 39 eqtr4id 
 |-  ( ph -> X = ( W /. .~ ) )
41 eqimss 
 |-  ( X = ( W /. .~ ) -> X C_ ( W /. .~ ) )
42 40 41 syl 
 |-  ( ph -> X C_ ( W /. .~ ) )
43 42 sselda 
 |-  ( ( ph /\ a e. X ) -> a e. ( W /. .~ ) )
44 eqid 
 |-  ( W /. .~ ) = ( W /. .~ )
45 fveq2 
 |-  ( [ t ] .~ = a -> ( K ` [ t ] .~ ) = ( K ` a ) )
46 fveq2 
 |-  ( [ t ] .~ = a -> ( E ` [ t ] .~ ) = ( E ` a ) )
47 45 46 eqeq12d 
 |-  ( [ t ] .~ = a -> ( ( K ` [ t ] .~ ) = ( E ` [ t ] .~ ) <-> ( K ` a ) = ( E ` a ) ) )
48 simpr 
 |-  ( ( ph /\ t e. W ) -> t e. W )
49 31 adantr 
 |-  ( ( ph /\ t e. W ) -> W = Word ( I X. 2o ) )
50 48 49 eleqtrd 
 |-  ( ( ph /\ t e. W ) -> t e. Word ( I X. 2o ) )
51 wrdf 
 |-  ( t e. Word ( I X. 2o ) -> t : ( 0 ..^ ( # ` t ) ) --> ( I X. 2o ) )
52 50 51 syl 
 |-  ( ( ph /\ t e. W ) -> t : ( 0 ..^ ( # ` t ) ) --> ( I X. 2o ) )
53 52 ffvelrnda 
 |-  ( ( ( ph /\ t e. W ) /\ n e. ( 0 ..^ ( # ` t ) ) ) -> ( t ` n ) e. ( I X. 2o ) )
54 elxp2 
 |-  ( ( t ` n ) e. ( I X. 2o ) <-> E. i e. I E. j e. 2o ( t ` n ) = <. i , j >. )
55 53 54 sylib 
 |-  ( ( ( ph /\ t e. W ) /\ n e. ( 0 ..^ ( # ` t ) ) ) -> E. i e. I E. j e. 2o ( t ` n ) = <. i , j >. )
56 fveq2 
 |-  ( y = i -> ( F ` y ) = ( F ` i ) )
57 56 fveq2d 
 |-  ( y = i -> ( N ` ( F ` y ) ) = ( N ` ( F ` i ) ) )
58 56 57 ifeq12d 
 |-  ( y = i -> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) = if ( z = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) )
59 eqeq1 
 |-  ( z = j -> ( z = (/) <-> j = (/) ) )
60 59 ifbid 
 |-  ( z = j -> if ( z = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) )
61 fvex 
 |-  ( F ` i ) e. _V
62 fvex 
 |-  ( N ` ( F ` i ) ) e. _V
63 61 62 ifex 
 |-  if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) e. _V
64 58 60 3 63 ovmpo 
 |-  ( ( i e. I /\ j e. 2o ) -> ( i T j ) = if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) )
65 64 adantl 
 |-  ( ( ph /\ ( i e. I /\ j e. 2o ) ) -> ( i T j ) = if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) )
66 elpri 
 |-  ( j e. { (/) , 1o } -> ( j = (/) \/ j = 1o ) )
67 df2o3 
 |-  2o = { (/) , 1o }
68 66 67 eleq2s 
 |-  ( j e. 2o -> ( j = (/) \/ j = 1o ) )
69 14 adantr 
 |-  ( ( ph /\ i e. I ) -> ( K o. U ) = F )
70 69 fveq1d 
 |-  ( ( ph /\ i e. I ) -> ( ( K o. U ) ` i ) = ( F ` i ) )
71 8 12 9 10 vrgpf 
 |-  ( I e. V -> U : I --> X )
72 5 71 syl 
 |-  ( ph -> U : I --> X )
73 fvco3 
 |-  ( ( U : I --> X /\ i e. I ) -> ( ( K o. U ) ` i ) = ( K ` ( U ` i ) ) )
74 72 73 sylan 
 |-  ( ( ph /\ i e. I ) -> ( ( K o. U ) ` i ) = ( K ` ( U ` i ) ) )
75 70 74 eqtr3d 
 |-  ( ( ph /\ i e. I ) -> ( F ` i ) = ( K ` ( U ` i ) ) )
76 75 adantr 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> ( F ` i ) = ( K ` ( U ` i ) ) )
77 iftrue 
 |-  ( j = (/) -> if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = ( F ` i ) )
78 77 adantl 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = ( F ` i ) )
79 simpr 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> j = (/) )
80 79 opeq2d 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> <. i , j >. = <. i , (/) >. )
81 80 s1eqd 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> <" <. i , j >. "> = <" <. i , (/) >. "> )
82 81 eceq1d 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> [ <" <. i , j >. "> ] .~ = [ <" <. i , (/) >. "> ] .~ )
83 8 12 vrgpval 
 |-  ( ( I e. V /\ i e. I ) -> ( U ` i ) = [ <" <. i , (/) >. "> ] .~ )
84 5 83 sylan 
 |-  ( ( ph /\ i e. I ) -> ( U ` i ) = [ <" <. i , (/) >. "> ] .~ )
85 84 adantr 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> ( U ` i ) = [ <" <. i , (/) >. "> ] .~ )
86 82 85 eqtr4d 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> [ <" <. i , j >. "> ] .~ = ( U ` i ) )
87 86 fveq2d 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> ( K ` [ <" <. i , j >. "> ] .~ ) = ( K ` ( U ` i ) ) )
88 76 78 87 3eqtr4d 
 |-  ( ( ( ph /\ i e. I ) /\ j = (/) ) -> if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = ( K ` [ <" <. i , j >. "> ] .~ ) )
89 75 fveq2d 
 |-  ( ( ph /\ i e. I ) -> ( N ` ( F ` i ) ) = ( N ` ( K ` ( U ` i ) ) ) )
90 72 ffvelrnda 
 |-  ( ( ph /\ i e. I ) -> ( U ` i ) e. X )
91 eqid 
 |-  ( invg ` G ) = ( invg ` G )
92 10 91 2 ghminv 
 |-  ( ( K e. ( G GrpHom H ) /\ ( U ` i ) e. X ) -> ( K ` ( ( invg ` G ) ` ( U ` i ) ) ) = ( N ` ( K ` ( U ` i ) ) ) )
93 13 90 92 syl2an2r 
 |-  ( ( ph /\ i e. I ) -> ( K ` ( ( invg ` G ) ` ( U ` i ) ) ) = ( N ` ( K ` ( U ` i ) ) ) )
94 89 93 eqtr4d 
 |-  ( ( ph /\ i e. I ) -> ( N ` ( F ` i ) ) = ( K ` ( ( invg ` G ) ` ( U ` i ) ) ) )
95 94 adantr 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> ( N ` ( F ` i ) ) = ( K ` ( ( invg ` G ) ` ( U ` i ) ) ) )
96 1n0 
 |-  1o =/= (/)
97 simpr 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> j = 1o )
98 97 neeq1d 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> ( j =/= (/) <-> 1o =/= (/) ) )
99 96 98 mpbiri 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> j =/= (/) )
100 ifnefalse 
 |-  ( j =/= (/) -> if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = ( N ` ( F ` i ) ) )
101 99 100 syl 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = ( N ` ( F ` i ) ) )
102 97 opeq2d 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> <. i , j >. = <. i , 1o >. )
103 102 s1eqd 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> <" <. i , j >. "> = <" <. i , 1o >. "> )
104 103 eceq1d 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> [ <" <. i , j >. "> ] .~ = [ <" <. i , 1o >. "> ] .~ )
105 8 12 9 91 vrgpinv 
 |-  ( ( I e. V /\ i e. I ) -> ( ( invg ` G ) ` ( U ` i ) ) = [ <" <. i , 1o >. "> ] .~ )
106 5 105 sylan 
 |-  ( ( ph /\ i e. I ) -> ( ( invg ` G ) ` ( U ` i ) ) = [ <" <. i , 1o >. "> ] .~ )
107 106 adantr 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> ( ( invg ` G ) ` ( U ` i ) ) = [ <" <. i , 1o >. "> ] .~ )
108 104 107 eqtr4d 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> [ <" <. i , j >. "> ] .~ = ( ( invg ` G ) ` ( U ` i ) ) )
109 108 fveq2d 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> ( K ` [ <" <. i , j >. "> ] .~ ) = ( K ` ( ( invg ` G ) ` ( U ` i ) ) ) )
110 95 101 109 3eqtr4d 
 |-  ( ( ( ph /\ i e. I ) /\ j = 1o ) -> if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = ( K ` [ <" <. i , j >. "> ] .~ ) )
111 88 110 jaodan 
 |-  ( ( ( ph /\ i e. I ) /\ ( j = (/) \/ j = 1o ) ) -> if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = ( K ` [ <" <. i , j >. "> ] .~ ) )
112 68 111 sylan2 
 |-  ( ( ( ph /\ i e. I ) /\ j e. 2o ) -> if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = ( K ` [ <" <. i , j >. "> ] .~ ) )
113 112 anasss 
 |-  ( ( ph /\ ( i e. I /\ j e. 2o ) ) -> if ( j = (/) , ( F ` i ) , ( N ` ( F ` i ) ) ) = ( K ` [ <" <. i , j >. "> ] .~ ) )
114 65 113 eqtrd 
 |-  ( ( ph /\ ( i e. I /\ j e. 2o ) ) -> ( i T j ) = ( K ` [ <" <. i , j >. "> ] .~ ) )
115 fveq2 
 |-  ( ( t ` n ) = <. i , j >. -> ( T ` ( t ` n ) ) = ( T ` <. i , j >. ) )
116 df-ov 
 |-  ( i T j ) = ( T ` <. i , j >. )
117 115 116 eqtr4di 
 |-  ( ( t ` n ) = <. i , j >. -> ( T ` ( t ` n ) ) = ( i T j ) )
118 s1eq 
 |-  ( ( t ` n ) = <. i , j >. -> <" ( t ` n ) "> = <" <. i , j >. "> )
119 118 eceq1d 
 |-  ( ( t ` n ) = <. i , j >. -> [ <" ( t ` n ) "> ] .~ = [ <" <. i , j >. "> ] .~ )
120 119 fveq2d 
 |-  ( ( t ` n ) = <. i , j >. -> ( K ` [ <" ( t ` n ) "> ] .~ ) = ( K ` [ <" <. i , j >. "> ] .~ ) )
121 117 120 eqeq12d 
 |-  ( ( t ` n ) = <. i , j >. -> ( ( T ` ( t ` n ) ) = ( K ` [ <" ( t ` n ) "> ] .~ ) <-> ( i T j ) = ( K ` [ <" <. i , j >. "> ] .~ ) ) )
122 114 121 syl5ibrcom 
 |-  ( ( ph /\ ( i e. I /\ j e. 2o ) ) -> ( ( t ` n ) = <. i , j >. -> ( T ` ( t ` n ) ) = ( K ` [ <" ( t ` n ) "> ] .~ ) ) )
123 122 rexlimdvva 
 |-  ( ph -> ( E. i e. I E. j e. 2o ( t ` n ) = <. i , j >. -> ( T ` ( t ` n ) ) = ( K ` [ <" ( t ` n ) "> ] .~ ) ) )
124 123 ad2antrr 
 |-  ( ( ( ph /\ t e. W ) /\ n e. ( 0 ..^ ( # ` t ) ) ) -> ( E. i e. I E. j e. 2o ( t ` n ) = <. i , j >. -> ( T ` ( t ` n ) ) = ( K ` [ <" ( t ` n ) "> ] .~ ) ) )
125 55 124 mpd 
 |-  ( ( ( ph /\ t e. W ) /\ n e. ( 0 ..^ ( # ` t ) ) ) -> ( T ` ( t ` n ) ) = ( K ` [ <" ( t ` n ) "> ] .~ ) )
126 125 mpteq2dva 
 |-  ( ( ph /\ t e. W ) -> ( n e. ( 0 ..^ ( # ` t ) ) |-> ( T ` ( t ` n ) ) ) = ( n e. ( 0 ..^ ( # ` t ) ) |-> ( K ` [ <" ( t ` n ) "> ] .~ ) ) )
127 1 2 3 4 5 6 frgpuptf 
 |-  ( ph -> T : ( I X. 2o ) --> B )
128 fcompt 
 |-  ( ( T : ( I X. 2o ) --> B /\ t : ( 0 ..^ ( # ` t ) ) --> ( I X. 2o ) ) -> ( T o. t ) = ( n e. ( 0 ..^ ( # ` t ) ) |-> ( T ` ( t ` n ) ) ) )
129 127 52 128 syl2an2r 
 |-  ( ( ph /\ t e. W ) -> ( T o. t ) = ( n e. ( 0 ..^ ( # ` t ) ) |-> ( T ` ( t ` n ) ) ) )
130 53 s1cld 
 |-  ( ( ( ph /\ t e. W ) /\ n e. ( 0 ..^ ( # ` t ) ) ) -> <" ( t ` n ) "> e. Word ( I X. 2o ) )
131 31 ad2antrr 
 |-  ( ( ( ph /\ t e. W ) /\ n e. ( 0 ..^ ( # ` t ) ) ) -> W = Word ( I X. 2o ) )
132 130 131 eleqtrrd 
 |-  ( ( ( ph /\ t e. W ) /\ n e. ( 0 ..^ ( # ` t ) ) ) -> <" ( t ` n ) "> e. W )
133 9 8 7 10 frgpeccl 
 |-  ( <" ( t ` n ) "> e. W -> [ <" ( t ` n ) "> ] .~ e. X )
134 132 133 syl 
 |-  ( ( ( ph /\ t e. W ) /\ n e. ( 0 ..^ ( # ` t ) ) ) -> [ <" ( t ` n ) "> ] .~ e. X )
135 52 feqmptd 
 |-  ( ( ph /\ t e. W ) -> t = ( n e. ( 0 ..^ ( # ` t ) ) |-> ( t ` n ) ) )
136 5 adantr 
 |-  ( ( ph /\ t e. W ) -> I e. V )
137 136 25 26 sylancl 
 |-  ( ( ph /\ t e. W ) -> ( I X. 2o ) e. _V )
138 eqid 
 |-  ( varFMnd ` ( I X. 2o ) ) = ( varFMnd ` ( I X. 2o ) )
139 138 vrmdfval 
 |-  ( ( I X. 2o ) e. _V -> ( varFMnd ` ( I X. 2o ) ) = ( w e. ( I X. 2o ) |-> <" w "> ) )
140 137 139 syl 
 |-  ( ( ph /\ t e. W ) -> ( varFMnd ` ( I X. 2o ) ) = ( w e. ( I X. 2o ) |-> <" w "> ) )
141 s1eq 
 |-  ( w = ( t ` n ) -> <" w "> = <" ( t ` n ) "> )
142 53 135 140 141 fmptco 
 |-  ( ( ph /\ t e. W ) -> ( ( varFMnd ` ( I X. 2o ) ) o. t ) = ( n e. ( 0 ..^ ( # ` t ) ) |-> <" ( t ` n ) "> ) )
143 eqidd 
 |-  ( ( ph /\ t e. W ) -> ( w e. W |-> [ w ] .~ ) = ( w e. W |-> [ w ] .~ ) )
144 eceq1 
 |-  ( w = <" ( t ` n ) "> -> [ w ] .~ = [ <" ( t ` n ) "> ] .~ )
145 132 142 143 144 fmptco 
 |-  ( ( ph /\ t e. W ) -> ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) = ( n e. ( 0 ..^ ( # ` t ) ) |-> [ <" ( t ` n ) "> ] .~ ) )
146 13 adantr 
 |-  ( ( ph /\ t e. W ) -> K e. ( G GrpHom H ) )
147 146 15 syl 
 |-  ( ( ph /\ t e. W ) -> K : X --> B )
148 147 feqmptd 
 |-  ( ( ph /\ t e. W ) -> K = ( w e. X |-> ( K ` w ) ) )
149 fveq2 
 |-  ( w = [ <" ( t ` n ) "> ] .~ -> ( K ` w ) = ( K ` [ <" ( t ` n ) "> ] .~ ) )
150 134 145 148 149 fmptco 
 |-  ( ( ph /\ t e. W ) -> ( K o. ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) = ( n e. ( 0 ..^ ( # ` t ) ) |-> ( K ` [ <" ( t ` n ) "> ] .~ ) ) )
151 126 129 150 3eqtr4d 
 |-  ( ( ph /\ t e. W ) -> ( T o. t ) = ( K o. ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) )
152 151 oveq2d 
 |-  ( ( ph /\ t e. W ) -> ( H gsum ( T o. t ) ) = ( H gsum ( K o. ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) ) )
153 1 2 3 4 5 6 7 8 9 10 11 frgpupval 
 |-  ( ( ph /\ t e. W ) -> ( E ` [ t ] .~ ) = ( H gsum ( T o. t ) ) )
154 ghmmhm 
 |-  ( K e. ( G GrpHom H ) -> K e. ( G MndHom H ) )
155 146 154 syl 
 |-  ( ( ph /\ t e. W ) -> K e. ( G MndHom H ) )
156 138 vrmdf 
 |-  ( ( I X. 2o ) e. _V -> ( varFMnd ` ( I X. 2o ) ) : ( I X. 2o ) --> Word ( I X. 2o ) )
157 137 156 syl 
 |-  ( ( ph /\ t e. W ) -> ( varFMnd ` ( I X. 2o ) ) : ( I X. 2o ) --> Word ( I X. 2o ) )
158 49 feq3d 
 |-  ( ( ph /\ t e. W ) -> ( ( varFMnd ` ( I X. 2o ) ) : ( I X. 2o ) --> W <-> ( varFMnd ` ( I X. 2o ) ) : ( I X. 2o ) --> Word ( I X. 2o ) ) )
159 157 158 mpbird 
 |-  ( ( ph /\ t e. W ) -> ( varFMnd ` ( I X. 2o ) ) : ( I X. 2o ) --> W )
160 wrdco 
 |-  ( ( t e. Word ( I X. 2o ) /\ ( varFMnd ` ( I X. 2o ) ) : ( I X. 2o ) --> W ) -> ( ( varFMnd ` ( I X. 2o ) ) o. t ) e. Word W )
161 50 159 160 syl2anc 
 |-  ( ( ph /\ t e. W ) -> ( ( varFMnd ` ( I X. 2o ) ) o. t ) e. Word W )
162 35 adantr 
 |-  ( ( ph /\ t e. W ) -> W = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
163 162 mpteq1d 
 |-  ( ( ph /\ t e. W ) -> ( w e. W |-> [ w ] .~ ) = ( w e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) |-> [ w ] .~ ) )
164 eqid 
 |-  ( w e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) |-> [ w ] .~ ) = ( w e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) |-> [ w ] .~ )
165 22 32 9 8 164 frgpmhm 
 |-  ( I e. V -> ( w e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) |-> [ w ] .~ ) e. ( ( freeMnd ` ( I X. 2o ) ) MndHom G ) )
166 136 165 syl 
 |-  ( ( ph /\ t e. W ) -> ( w e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) |-> [ w ] .~ ) e. ( ( freeMnd ` ( I X. 2o ) ) MndHom G ) )
167 163 166 eqeltrd 
 |-  ( ( ph /\ t e. W ) -> ( w e. W |-> [ w ] .~ ) e. ( ( freeMnd ` ( I X. 2o ) ) MndHom G ) )
168 32 10 mhmf 
 |-  ( ( w e. W |-> [ w ] .~ ) e. ( ( freeMnd ` ( I X. 2o ) ) MndHom G ) -> ( w e. W |-> [ w ] .~ ) : ( Base ` ( freeMnd ` ( I X. 2o ) ) ) --> X )
169 167 168 syl 
 |-  ( ( ph /\ t e. W ) -> ( w e. W |-> [ w ] .~ ) : ( Base ` ( freeMnd ` ( I X. 2o ) ) ) --> X )
170 162 feq2d 
 |-  ( ( ph /\ t e. W ) -> ( ( w e. W |-> [ w ] .~ ) : W --> X <-> ( w e. W |-> [ w ] .~ ) : ( Base ` ( freeMnd ` ( I X. 2o ) ) ) --> X ) )
171 169 170 mpbird 
 |-  ( ( ph /\ t e. W ) -> ( w e. W |-> [ w ] .~ ) : W --> X )
172 wrdco 
 |-  ( ( ( ( varFMnd ` ( I X. 2o ) ) o. t ) e. Word W /\ ( w e. W |-> [ w ] .~ ) : W --> X ) -> ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) e. Word X )
173 161 171 172 syl2anc 
 |-  ( ( ph /\ t e. W ) -> ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) e. Word X )
174 10 gsumwmhm 
 |-  ( ( K e. ( G MndHom H ) /\ ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) e. Word X ) -> ( K ` ( G gsum ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) ) = ( H gsum ( K o. ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) ) )
175 155 173 174 syl2anc 
 |-  ( ( ph /\ t e. W ) -> ( K ` ( G gsum ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) ) = ( H gsum ( K o. ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) ) )
176 152 153 175 3eqtr4d 
 |-  ( ( ph /\ t e. W ) -> ( E ` [ t ] .~ ) = ( K ` ( G gsum ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) ) )
177 22 138 frmdgsum 
 |-  ( ( ( I X. 2o ) e. _V /\ t e. Word ( I X. 2o ) ) -> ( ( freeMnd ` ( I X. 2o ) ) gsum ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) = t )
178 27 50 177 syl2an2r 
 |-  ( ( ph /\ t e. W ) -> ( ( freeMnd ` ( I X. 2o ) ) gsum ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) = t )
179 178 fveq2d 
 |-  ( ( ph /\ t e. W ) -> ( ( w e. W |-> [ w ] .~ ) ` ( ( freeMnd ` ( I X. 2o ) ) gsum ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) = ( ( w e. W |-> [ w ] .~ ) ` t ) )
180 wrdco 
 |-  ( ( t e. Word ( I X. 2o ) /\ ( varFMnd ` ( I X. 2o ) ) : ( I X. 2o ) --> Word ( I X. 2o ) ) -> ( ( varFMnd ` ( I X. 2o ) ) o. t ) e. Word Word ( I X. 2o ) )
181 50 157 180 syl2anc 
 |-  ( ( ph /\ t e. W ) -> ( ( varFMnd ` ( I X. 2o ) ) o. t ) e. Word Word ( I X. 2o ) )
182 34 adantr 
 |-  ( ( ph /\ t e. W ) -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
183 wrdeq 
 |-  ( ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) -> Word ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word Word ( I X. 2o ) )
184 182 183 syl 
 |-  ( ( ph /\ t e. W ) -> Word ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word Word ( I X. 2o ) )
185 181 184 eleqtrrd 
 |-  ( ( ph /\ t e. W ) -> ( ( varFMnd ` ( I X. 2o ) ) o. t ) e. Word ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
186 32 gsumwmhm 
 |-  ( ( ( w e. W |-> [ w ] .~ ) e. ( ( freeMnd ` ( I X. 2o ) ) MndHom G ) /\ ( ( varFMnd ` ( I X. 2o ) ) o. t ) e. Word ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) -> ( ( w e. W |-> [ w ] .~ ) ` ( ( freeMnd ` ( I X. 2o ) ) gsum ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) = ( G gsum ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) )
187 167 185 186 syl2anc 
 |-  ( ( ph /\ t e. W ) -> ( ( w e. W |-> [ w ] .~ ) ` ( ( freeMnd ` ( I X. 2o ) ) gsum ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) = ( G gsum ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) )
188 7 8 efger 
 |-  .~ Er W
189 188 a1i 
 |-  ( ( ph /\ t e. W ) -> .~ Er W )
190 7 fvexi 
 |-  W e. _V
191 190 a1i 
 |-  ( ( ph /\ t e. W ) -> W e. _V )
192 eqid 
 |-  ( w e. W |-> [ w ] .~ ) = ( w e. W |-> [ w ] .~ )
193 189 191 192 divsfval 
 |-  ( ( ph /\ t e. W ) -> ( ( w e. W |-> [ w ] .~ ) ` t ) = [ t ] .~ )
194 179 187 193 3eqtr3d 
 |-  ( ( ph /\ t e. W ) -> ( G gsum ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) = [ t ] .~ )
195 194 fveq2d 
 |-  ( ( ph /\ t e. W ) -> ( K ` ( G gsum ( ( w e. W |-> [ w ] .~ ) o. ( ( varFMnd ` ( I X. 2o ) ) o. t ) ) ) ) = ( K ` [ t ] .~ ) )
196 176 195 eqtr2d 
 |-  ( ( ph /\ t e. W ) -> ( K ` [ t ] .~ ) = ( E ` [ t ] .~ ) )
197 44 47 196 ectocld 
 |-  ( ( ph /\ a e. ( W /. .~ ) ) -> ( K ` a ) = ( E ` a ) )
198 43 197 syldan 
 |-  ( ( ph /\ a e. X ) -> ( K ` a ) = ( E ` a ) )
199 17 21 198 eqfnfvd 
 |-  ( ph -> K = E )