# 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}={\mathrm{Base}}_{{H}}$
frgpup.n ${⊢}{N}={inv}_{g}\left({H}\right)$
frgpup.t ${⊢}{T}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼if\left({z}=\varnothing ,{F}\left({y}\right),{N}\left({F}\left({y}\right)\right)\right)\right)$
frgpup.h ${⊢}{\phi }\to {H}\in \mathrm{Grp}$
frgpup.i ${⊢}{\phi }\to {I}\in {V}$
frgpup.a ${⊢}{\phi }\to {F}:{I}⟶{B}$
frgpup.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
frgpup.r
frgpup.g ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
frgpup.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
frgpup.e
Assertion frgpupf ${⊢}{\phi }\to {E}:{X}⟶{B}$

### Proof

Step Hyp Ref Expression
1 frgpup.b ${⊢}{B}={\mathrm{Base}}_{{H}}$
2 frgpup.n ${⊢}{N}={inv}_{g}\left({H}\right)$
3 frgpup.t ${⊢}{T}=\left({y}\in {I},{z}\in {2}_{𝑜}⟼if\left({z}=\varnothing ,{F}\left({y}\right),{N}\left({F}\left({y}\right)\right)\right)\right)$
4 frgpup.h ${⊢}{\phi }\to {H}\in \mathrm{Grp}$
5 frgpup.i ${⊢}{\phi }\to {I}\in {V}$
6 frgpup.a ${⊢}{\phi }\to {F}:{I}⟶{B}$
7 frgpup.w ${⊢}{W}=\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
8 frgpup.r
9 frgpup.g ${⊢}{G}=\mathrm{freeGrp}\left({I}\right)$
10 frgpup.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
11 frgpup.e
12 grpmnd ${⊢}{H}\in \mathrm{Grp}\to {H}\in \mathrm{Mnd}$
13 4 12 syl ${⊢}{\phi }\to {H}\in \mathrm{Mnd}$
14 fviss ${⊢}\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
15 7 14 eqsstri ${⊢}{W}\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
16 15 sseli ${⊢}{g}\in {W}\to {g}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
17 1 2 3 4 5 6 frgpuptf ${⊢}{\phi }\to {T}:{I}×{2}_{𝑜}⟶{B}$
18 wrdco ${⊢}\left({g}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {T}:{I}×{2}_{𝑜}⟶{B}\right)\to {T}\circ {g}\in \mathrm{Word}{B}$
19 16 17 18 syl2anr ${⊢}\left({\phi }\wedge {g}\in {W}\right)\to {T}\circ {g}\in \mathrm{Word}{B}$
20 1 gsumwcl ${⊢}\left({H}\in \mathrm{Mnd}\wedge {T}\circ {g}\in \mathrm{Word}{B}\right)\to {\sum }_{{H}}\left({T}\circ {g}\right)\in {B}$
21 13 19 20 syl2an2r ${⊢}\left({\phi }\wedge {g}\in {W}\right)\to {\sum }_{{H}}\left({T}\circ {g}\right)\in {B}$
22 7 8 efger
23 22 a1i
24 7 fvexi ${⊢}{W}\in \mathrm{V}$
25 24 a1i ${⊢}{\phi }\to {W}\in \mathrm{V}$
26 coeq2 ${⊢}{g}={h}\to {T}\circ {g}={T}\circ {h}$
27 26 oveq2d ${⊢}{g}={h}\to {\sum }_{{H}}\left({T}\circ {g}\right)={\sum }_{{H}}\left({T}\circ {h}\right)$
28 1 2 3 4 5 6 7 8 frgpuplem
29 11 21 23 25 27 28 qliftfund ${⊢}{\phi }\to \mathrm{Fun}{E}$
30 11 21 23 25 qliftf
31 29 30 mpbid
32 eqid ${⊢}\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)=\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)$
33 9 32 8 frgpval
34 5 33 syl
35 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
36 xpexg ${⊢}\left({I}\in {V}\wedge {2}_{𝑜}\in \mathrm{On}\right)\to {I}×{2}_{𝑜}\in \mathrm{V}$
37 5 35 36 sylancl ${⊢}{\phi }\to {I}×{2}_{𝑜}\in \mathrm{V}$
38 wrdexg ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to \mathrm{Word}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}$
39 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)$
40 37 38 39 3syl ${⊢}{\phi }\to \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
41 7 40 syl5eq ${⊢}{\phi }\to {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
42 eqid ${⊢}{\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
43 32 42 frmdbas ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
44 37 43 syl ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
45 41 44 eqtr4d ${⊢}{\phi }\to {W}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
46 8 fvexi
47 46 a1i
48 fvexd ${⊢}{\phi }\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}$
49 34 45 47 48 qusbas
50 49 10 syl6reqr
51 50 feq2d
52 31 51 mpbird ${⊢}{\phi }\to {E}:{X}⟶{B}$