# Metamath Proof Explorer

## Theorem frgpupval

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 frgpupval

### 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 ovexd ${⊢}\left({\phi }\wedge {g}\in {W}\right)\to {\sum }_{{H}}\left({T}\circ {g}\right)\in \mathrm{V}$
13 7 8 efger
14 13 a1i
15 7 fvexi ${⊢}{W}\in \mathrm{V}$
16 15 a1i ${⊢}{\phi }\to {W}\in \mathrm{V}$
17 coeq2 ${⊢}{g}={A}\to {T}\circ {g}={T}\circ {A}$
18 17 oveq2d ${⊢}{g}={A}\to {\sum }_{{H}}\left({T}\circ {g}\right)={\sum }_{{H}}\left({T}\circ {A}\right)$
19 1 2 3 4 5 6 7 8 9 10 11 frgpupf ${⊢}{\phi }\to {E}:{X}⟶{B}$
20 19 ffund ${⊢}{\phi }\to \mathrm{Fun}{E}$
21 11 12 14 16 18 20 qliftval