# 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}=\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)$
frgpmhm.w ${⊢}{W}={\mathrm{Base}}_{{M}}$
frgpmhm.g ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
frgpmhm.r
frgpmhm.f
Assertion frgpmhm ${⊢}{I}\in {V}\to {F}\in \left({M}\mathrm{MndHom}{G}\right)$

### Proof

Step Hyp Ref Expression
1 frgpmhm.m ${⊢}{M}=\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)$
2 frgpmhm.w ${⊢}{W}={\mathrm{Base}}_{{M}}$
3 frgpmhm.g ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
4 frgpmhm.r
5 frgpmhm.f
6 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
7 xpexg ${⊢}\left({I}\in {V}\wedge {2}_{𝑜}\in \mathrm{On}\right)\to {I}×{2}_{𝑜}\in \mathrm{V}$
8 6 7 mpan2 ${⊢}{I}\in {V}\to {I}×{2}_{𝑜}\in \mathrm{V}$
9 1 frmdmnd ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to {M}\in \mathrm{Mnd}$
10 8 9 syl ${⊢}{I}\in {V}\to {M}\in \mathrm{Mnd}$
11 3 frgpgrp ${⊢}{I}\in {V}\to {G}\in \mathrm{Grp}$
12 grpmnd ${⊢}{G}\in \mathrm{Grp}\to {G}\in \mathrm{Mnd}$
13 11 12 syl ${⊢}{I}\in {V}\to {G}\in \mathrm{Mnd}$
14 1 2 frmdbas ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
15 wrdexg ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to \mathrm{Word}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}$
16 fvi ${⊢}\mathrm{Word}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}\to \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
17 15 16 syl ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
18 14 17 eqtr4d ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to {W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
19 8 18 syl ${⊢}{I}\in {V}\to {W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
20 19 eleq2d ${⊢}{I}\in {V}\to \left({x}\in {W}↔{x}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)$
21 20 biimpa ${⊢}\left({I}\in {V}\wedge {x}\in {W}\right)\to {x}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
22 eqid ${⊢}\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
23 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
24 3 4 22 23 frgpeccl
25 21 24 syl
26 25 5 fmptd ${⊢}{I}\in {V}\to {F}:{W}⟶{\mathrm{Base}}_{{G}}$
27 22 4 efger
28 ereq2
29 19 28 syl
30 27 29 mpbiri
32 2 fvexi ${⊢}{W}\in \mathrm{V}$
33 32 a1i ${⊢}\left({I}\in {V}\wedge \left({a}\in {W}\wedge {b}\in {W}\right)\right)\to {W}\in \mathrm{V}$
34 31 33 5 divsfval
35 eqid ${⊢}{+}_{{M}}={+}_{{M}}$
36 1 2 35 frmdadd ${⊢}\left({a}\in {W}\wedge {b}\in {W}\right)\to {a}{+}_{{M}}{b}={a}\mathrm{++}{b}$
37 36 adantl ${⊢}\left({I}\in {V}\wedge \left({a}\in {W}\wedge {b}\in {W}\right)\right)\to {a}{+}_{{M}}{b}={a}\mathrm{++}{b}$
38 37 fveq2d ${⊢}\left({I}\in {V}\wedge \left({a}\in {W}\wedge {b}\in {W}\right)\right)\to {F}\left({a}{+}_{{M}}{b}\right)={F}\left({a}\mathrm{++}{b}\right)$
39 31 33 5 divsfval
40 31 33 5 divsfval
41 39 40 oveq12d
42 19 eleq2d ${⊢}{I}\in {V}\to \left({a}\in {W}↔{a}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)$
43 19 eleq2d ${⊢}{I}\in {V}\to \left({b}\in {W}↔{b}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)$
44 42 43 anbi12d ${⊢}{I}\in {V}\to \left(\left({a}\in {W}\wedge {b}\in {W}\right)↔\left({a}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\wedge {b}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)\right)$
45 44 biimpa ${⊢}\left({I}\in {V}\wedge \left({a}\in {W}\wedge {b}\in {W}\right)\right)\to \left({a}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\wedge {b}\in \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\right)$
46 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
47 22 3 4 46 frgpadd
48 45 47 syl
49 41 48 eqtrd
50 34 38 49 3eqtr4d ${⊢}\left({I}\in {V}\wedge \left({a}\in {W}\wedge {b}\in {W}\right)\right)\to {F}\left({a}{+}_{{M}}{b}\right)={F}\left({a}\right){+}_{{G}}{F}\left({b}\right)$
51 50 ralrimivva ${⊢}{I}\in {V}\to \forall {a}\in {W}\phantom{\rule{.4em}{0ex}}\forall {b}\in {W}\phantom{\rule{.4em}{0ex}}{F}\left({a}{+}_{{M}}{b}\right)={F}\left({a}\right){+}_{{G}}{F}\left({b}\right)$
52 32 a1i ${⊢}{I}\in {V}\to {W}\in \mathrm{V}$
53 30 52 5 divsfval
54 3 4 frgp0
55 54 simprd
56 53 55 eqtrd ${⊢}{I}\in {V}\to {F}\left(\varnothing \right)={0}_{{G}}$
57 26 51 56 3jca ${⊢}{I}\in {V}\to \left({F}:{W}⟶{\mathrm{Base}}_{{G}}\wedge \forall {a}\in {W}\phantom{\rule{.4em}{0ex}}\forall {b}\in {W}\phantom{\rule{.4em}{0ex}}{F}\left({a}{+}_{{M}}{b}\right)={F}\left({a}\right){+}_{{G}}{F}\left({b}\right)\wedge {F}\left(\varnothing \right)={0}_{{G}}\right)$
58 1 frmd0 ${⊢}\varnothing ={0}_{{M}}$
59 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
60 2 23 35 46 58 59 ismhm ${⊢}{F}\in \left({M}\mathrm{MndHom}{G}\right)↔\left(\left({M}\in \mathrm{Mnd}\wedge {G}\in \mathrm{Mnd}\right)\wedge \left({F}:{W}⟶{\mathrm{Base}}_{{G}}\wedge \forall {a}\in {W}\phantom{\rule{.4em}{0ex}}\forall {b}\in {W}\phantom{\rule{.4em}{0ex}}{F}\left({a}{+}_{{M}}{b}\right)={F}\left({a}\right){+}_{{G}}{F}\left({b}\right)\wedge {F}\left(\varnothing \right)={0}_{{G}}\right)\right)$
61 10 13 57 60 syl21anbrc ${⊢}{I}\in {V}\to {F}\in \left({M}\mathrm{MndHom}{G}\right)$