Metamath Proof Explorer

Theorem frgpmhm

Description: The "natural map" from words of the free monoid to their cosets in the free group is a surjective monoid homomorphism. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses frgpmhm.m 
|- M = ( freeMnd ` ( I X. 2o ) )
frgpmhm.w 
|- W = ( Base ` M )
frgpmhm.g 
|- G = ( freeGrp ` I )
frgpmhm.r 
|- .~ = ( ~FG ` I )
frgpmhm.f 
|- F = ( x e. W |-> [ x ] .~ )
Assertion frgpmhm 
|- ( I e. V -> F e. ( M MndHom G ) )

Proof

Step Hyp Ref Expression
1 frgpmhm.m 
 |-  M = ( freeMnd ` ( I X. 2o ) )
2 frgpmhm.w 
 |-  W = ( Base ` M )
3 frgpmhm.g 
 |-  G = ( freeGrp ` I )
4 frgpmhm.r 
 |-  .~ = ( ~FG ` I )
5 frgpmhm.f 
 |-  F = ( x e. W |-> [ x ] .~ )
6 2on 
 |-  2o e. On
7 xpexg 
 |-  ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
8 6 7 mpan2 
 |-  ( I e. V -> ( I X. 2o ) e. _V )
9 1 frmdmnd 
 |-  ( ( I X. 2o ) e. _V -> M e. Mnd )
10 8 9 syl 
 |-  ( I e. V -> M e. Mnd )
11 3 frgpgrp 
 |-  ( I e. V -> G e. Grp )
12 11 grpmndd 
 |-  ( I e. V -> G e. Mnd )
13 1 2 frmdbas 
 |-  ( ( I X. 2o ) e. _V -> W = Word ( I X. 2o ) )
14 wrdexg 
 |-  ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V )
15 fvi 
 |-  ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
16 14 15 syl 
 |-  ( ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
17 13 16 eqtr4d 
 |-  ( ( I X. 2o ) e. _V -> W = ( _I ` Word ( I X. 2o ) ) )
18 8 17 syl 
 |-  ( I e. V -> W = ( _I ` Word ( I X. 2o ) ) )
19 18 eleq2d 
 |-  ( I e. V -> ( x e. W <-> x e. ( _I ` Word ( I X. 2o ) ) ) )
20 19 biimpa 
 |-  ( ( I e. V /\ x e. W ) -> x e. ( _I ` Word ( I X. 2o ) ) )
21 eqid 
 |-  ( _I ` Word ( I X. 2o ) ) = ( _I ` Word ( I X. 2o ) )
22 eqid 
 |-  ( Base ` G ) = ( Base ` G )
23 3 4 21 22 frgpeccl 
 |-  ( x e. ( _I ` Word ( I X. 2o ) ) -> [ x ] .~ e. ( Base ` G ) )
24 20 23 syl 
 |-  ( ( I e. V /\ x e. W ) -> [ x ] .~ e. ( Base ` G ) )
25 24 5 fmptd 
 |-  ( I e. V -> F : W --> ( Base ` G ) )
26 21 4 efger 
 |-  .~ Er ( _I ` Word ( I X. 2o ) )
27 ereq2 
 |-  ( W = ( _I ` Word ( I X. 2o ) ) -> ( .~ Er W <-> .~ Er ( _I ` Word ( I X. 2o ) ) ) )
28 18 27 syl 
 |-  ( I e. V -> ( .~ Er W <-> .~ Er ( _I ` Word ( I X. 2o ) ) ) )
29 26 28 mpbiri 
 |-  ( I e. V -> .~ Er W )
30 29 adantr 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> .~ Er W )
31 2 fvexi 
 |-  W e. _V
32 31 a1i 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> W e. _V )
33 30 32 5 divsfval 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` ( a ++ b ) ) = [ ( a ++ b ) ] .~ )
34 eqid 
 |-  ( +g ` M ) = ( +g ` M )
35 1 2 34 frmdadd 
 |-  ( ( a e. W /\ b e. W ) -> ( a ( +g ` M ) b ) = ( a ++ b ) )
36 35 adantl 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( a ( +g ` M ) b ) = ( a ++ b ) )
37 36 fveq2d 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` ( a ( +g ` M ) b ) ) = ( F ` ( a ++ b ) ) )
38 30 32 5 divsfval 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` a ) = [ a ] .~ )
39 30 32 5 divsfval 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` b ) = [ b ] .~ )
40 38 39 oveq12d 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( ( F ` a ) ( +g ` G ) ( F ` b ) ) = ( [ a ] .~ ( +g ` G ) [ b ] .~ ) )
41 18 eleq2d 
 |-  ( I e. V -> ( a e. W <-> a e. ( _I ` Word ( I X. 2o ) ) ) )
42 18 eleq2d 
 |-  ( I e. V -> ( b e. W <-> b e. ( _I ` Word ( I X. 2o ) ) ) )
43 41 42 anbi12d 
 |-  ( I e. V -> ( ( a e. W /\ b e. W ) <-> ( a e. ( _I ` Word ( I X. 2o ) ) /\ b e. ( _I ` Word ( I X. 2o ) ) ) ) )
44 43 biimpa 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( a e. ( _I ` Word ( I X. 2o ) ) /\ b e. ( _I ` Word ( I X. 2o ) ) ) )
45 eqid 
 |-  ( +g ` G ) = ( +g ` G )
46 21 3 4 45 frgpadd 
 |-  ( ( a e. ( _I ` Word ( I X. 2o ) ) /\ b e. ( _I ` Word ( I X. 2o ) ) ) -> ( [ a ] .~ ( +g ` G ) [ b ] .~ ) = [ ( a ++ b ) ] .~ )
47 44 46 syl 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( [ a ] .~ ( +g ` G ) [ b ] .~ ) = [ ( a ++ b ) ] .~ )
48 40 47 eqtrd 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( ( F ` a ) ( +g ` G ) ( F ` b ) ) = [ ( a ++ b ) ] .~ )
49 33 37 48 3eqtr4d 
 |-  ( ( I e. V /\ ( a e. W /\ b e. W ) ) -> ( F ` ( a ( +g ` M ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) )
50 49 ralrimivva 
 |-  ( I e. V -> A. a e. W A. b e. W ( F ` ( a ( +g ` M ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) )
51 31 a1i 
 |-  ( I e. V -> W e. _V )
52 29 51 5 divsfval 
 |-  ( I e. V -> ( F ` (/) ) = [ (/) ] .~ )
53 3 4 frgp0 
 |-  ( I e. V -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )
54 53 simprd 
 |-  ( I e. V -> [ (/) ] .~ = ( 0g ` G ) )
55 52 54 eqtrd 
 |-  ( I e. V -> ( F ` (/) ) = ( 0g ` G ) )
56 25 50 55 3jca 
 |-  ( I e. V -> ( F : W --> ( Base ` G ) /\ A. a e. W A. b e. W ( F ` ( a ( +g ` M ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) /\ ( F ` (/) ) = ( 0g ` G ) ) )
57 1 frmd0 
 |-  (/) = ( 0g ` M )
58 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
59 2 22 34 45 57 58 ismhm 
 |-  ( F e. ( M MndHom G ) <-> ( ( M e. Mnd /\ G e. Mnd ) /\ ( F : W --> ( Base ` G ) /\ A. a e. W A. b e. W ( F ` ( a ( +g ` M ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) /\ ( F ` (/) ) = ( 0g ` G ) ) ) )
60 10 12 56 59 syl21anbrc 
 |-  ( I e. V -> F e. ( M MndHom G ) )