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