Metamath Proof Explorer

Theorem frgpupf

Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015)

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 ) ) >. )
Assertion frgpupf 
|- ( ph -> E : X --> B )

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 4 grpmndd 
 |-  ( ph -> H e. Mnd )
13 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
14 7 13 eqsstri 
 |-  W C_ Word ( I X. 2o )
15 14 sseli 
 |-  ( g e. W -> g e. Word ( I X. 2o ) )
16 1 2 3 4 5 6 frgpuptf 
 |-  ( ph -> T : ( I X. 2o ) --> B )
17 wrdco 
 |-  ( ( g e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. g ) e. Word B )
18 15 16 17 syl2anr 
 |-  ( ( ph /\ g e. W ) -> ( T o. g ) e. Word B )
19 1 gsumwcl 
 |-  ( ( H e. Mnd /\ ( T o. g ) e. Word B ) -> ( H gsum ( T o. g ) ) e. B )
20 12 18 19 syl2an2r 
 |-  ( ( ph /\ g e. W ) -> ( H gsum ( T o. g ) ) e. B )
21 7 8 efger 
 |-  .~ Er W
22 21 a1i 
 |-  ( ph -> .~ Er W )
23 7 fvexi 
 |-  W e. _V
24 23 a1i 
 |-  ( ph -> W e. _V )
25 coeq2 
 |-  ( g = h -> ( T o. g ) = ( T o. h ) )
26 25 oveq2d 
 |-  ( g = h -> ( H gsum ( T o. g ) ) = ( H gsum ( T o. h ) ) )
27 1 2 3 4 5 6 7 8 frgpuplem 
 |-  ( ( ph /\ g .~ h ) -> ( H gsum ( T o. g ) ) = ( H gsum ( T o. h ) ) )
28 11 20 22 24 26 27 qliftfund 
 |-  ( ph -> Fun E )
29 11 20 22 24 qliftf 
 |-  ( ph -> ( Fun E <-> E : ( W /. .~ ) --> B ) )
30 28 29 mpbid 
 |-  ( ph -> E : ( W /. .~ ) --> B )
31 eqid 
 |-  ( freeMnd ` ( I X. 2o ) ) = ( freeMnd ` ( I X. 2o ) )
32 9 31 8 frgpval 
 |-  ( I e. V -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) )
33 5 32 syl 
 |-  ( ph -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) )
34 2on 
 |-  2o e. On
35 xpexg 
 |-  ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
36 5 34 35 sylancl 
 |-  ( ph -> ( I X. 2o ) e. _V )
37 wrdexg 
 |-  ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V )
38 fvi 
 |-  ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
39 36 37 38 3syl 
 |-  ( ph -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
40 7 39 syl5eq 
 |-  ( ph -> W = Word ( I X. 2o ) )
41 eqid 
 |-  ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) )
42 31 41 frmdbas 
 |-  ( ( I X. 2o ) e. _V -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
43 36 42 syl 
 |-  ( ph -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
44 40 43 eqtr4d 
 |-  ( ph -> W = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
45 8 fvexi 
 |-  .~ e. _V
46 45 a1i 
 |-  ( ph -> .~ e. _V )
47 fvexd 
 |-  ( ph -> ( freeMnd ` ( I X. 2o ) ) e. _V )
48 33 44 46 47 qusbas 
 |-  ( ph -> ( W /. .~ ) = ( Base ` G ) )
49 10 48 eqtr4id 
 |-  ( ph -> X = ( W /. .~ ) )
50 49 feq2d 
 |-  ( ph -> ( E : X --> B <-> E : ( W /. .~ ) --> B ) )
51 30 50 mpbird 
 |-  ( ph -> E : X --> B )