# Metamath Proof Explorer

## Theorem frgpup1

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) (Revised by Mario Carneiro, 28-Feb-2016)

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 frgpup1 ${⊢}{\phi }\to {E}\in \left({G}\mathrm{GrpHom}{H}\right)$

### 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 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
13 eqid ${⊢}{+}_{{H}}={+}_{{H}}$
14 9 frgpgrp ${⊢}{I}\in {V}\to {G}\in \mathrm{Grp}$
15 5 14 syl ${⊢}{\phi }\to {G}\in \mathrm{Grp}$
16 1 2 3 4 5 6 7 8 9 10 11 frgpupf ${⊢}{\phi }\to {E}:{X}⟶{B}$
17 eqid ${⊢}\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)=\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)$
18 9 17 8 frgpval
19 5 18 syl
20 2on ${⊢}{2}_{𝑜}\in \mathrm{On}$
21 xpexg ${⊢}\left({I}\in {V}\wedge {2}_{𝑜}\in \mathrm{On}\right)\to {I}×{2}_{𝑜}\in \mathrm{V}$
22 5 20 21 sylancl ${⊢}{\phi }\to {I}×{2}_{𝑜}\in \mathrm{V}$
23 wrdexg ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to \mathrm{Word}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}$
24 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)$
25 22 23 24 3syl ${⊢}{\phi }\to \mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
26 7 25 syl5eq ${⊢}{\phi }\to {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
27 eqid ${⊢}{\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
28 17 27 frmdbas ${⊢}{I}×{2}_{𝑜}\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
29 22 28 syl ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
30 26 29 eqtr4d ${⊢}{\phi }\to {W}={\mathrm{Base}}_{\mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)}$
31 8 fvexi
32 31 a1i
33 fvexd ${⊢}{\phi }\to \mathrm{freeMnd}\left({I}×{2}_{𝑜}\right)\in \mathrm{V}$
34 19 30 32 33 qusbas
35 34 10 syl6reqr
36 eqimss
37 35 36 syl
39 38 sselda
40 eqid
41 oveq2
42 41 fveq2d
43 fveq2
44 43 oveq2d
45 42 44 eqeq12d
46 37 sselda
48 fvoveq1
49 fveq2
50 49 oveq1d
51 48 50 eqeq12d
52 fviss ${⊢}\mathrm{I}\left(\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
53 7 52 eqsstri ${⊢}{W}\subseteq \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
54 53 sseli ${⊢}{t}\in {W}\to {t}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
55 53 sseli ${⊢}{u}\in {W}\to {u}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
56 ccatcl ${⊢}\left({t}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {u}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)\to {t}\mathrm{++}{u}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
57 54 55 56 syl2an ${⊢}\left({t}\in {W}\wedge {u}\in {W}\right)\to {t}\mathrm{++}{u}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
58 7 efgrcl ${⊢}{t}\in {W}\to \left({I}\in \mathrm{V}\wedge {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
59 58 adantr ${⊢}\left({t}\in {W}\wedge {u}\in {W}\right)\to \left({I}\in \mathrm{V}\wedge {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)\right)$
60 59 simprd ${⊢}\left({t}\in {W}\wedge {u}\in {W}\right)\to {W}=\mathrm{Word}\left({I}×{2}_{𝑜}\right)$
61 57 60 eleqtrrd ${⊢}\left({t}\in {W}\wedge {u}\in {W}\right)\to {t}\mathrm{++}{u}\in {W}$
62 1 2 3 4 5 6 7 8 9 10 11 frgpupval
63 61 62 sylan2
64 54 ad2antrl ${⊢}\left({\phi }\wedge \left({t}\in {W}\wedge {u}\in {W}\right)\right)\to {t}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
65 55 ad2antll ${⊢}\left({\phi }\wedge \left({t}\in {W}\wedge {u}\in {W}\right)\right)\to {u}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)$
66 1 2 3 4 5 6 frgpuptf ${⊢}{\phi }\to {T}:{I}×{2}_{𝑜}⟶{B}$
67 66 adantr ${⊢}\left({\phi }\wedge \left({t}\in {W}\wedge {u}\in {W}\right)\right)\to {T}:{I}×{2}_{𝑜}⟶{B}$
68 ccatco ${⊢}\left({t}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {u}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {T}:{I}×{2}_{𝑜}⟶{B}\right)\to {T}\circ \left({t}\mathrm{++}{u}\right)=\left({T}\circ {t}\right)\mathrm{++}\left({T}\circ {u}\right)$
69 64 65 67 68 syl3anc ${⊢}\left({\phi }\wedge \left({t}\in {W}\wedge {u}\in {W}\right)\right)\to {T}\circ \left({t}\mathrm{++}{u}\right)=\left({T}\circ {t}\right)\mathrm{++}\left({T}\circ {u}\right)$
70 69 oveq2d ${⊢}\left({\phi }\wedge \left({t}\in {W}\wedge {u}\in {W}\right)\right)\to {\sum }_{{H}}\left({T}\circ \left({t}\mathrm{++}{u}\right)\right)={\sum }_{{H}}\left(\left({T}\circ {t}\right)\mathrm{++}\left({T}\circ {u}\right)\right)$
71 grpmnd ${⊢}{H}\in \mathrm{Grp}\to {H}\in \mathrm{Mnd}$
72 4 71 syl ${⊢}{\phi }\to {H}\in \mathrm{Mnd}$
73 72 adantr ${⊢}\left({\phi }\wedge \left({t}\in {W}\wedge {u}\in {W}\right)\right)\to {H}\in \mathrm{Mnd}$
74 wrdco ${⊢}\left({t}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {T}:{I}×{2}_{𝑜}⟶{B}\right)\to {T}\circ {t}\in \mathrm{Word}{B}$
75 54 66 74 syl2anr ${⊢}\left({\phi }\wedge {t}\in {W}\right)\to {T}\circ {t}\in \mathrm{Word}{B}$
76 75 adantrr ${⊢}\left({\phi }\wedge \left({t}\in {W}\wedge {u}\in {W}\right)\right)\to {T}\circ {t}\in \mathrm{Word}{B}$
77 wrdco ${⊢}\left({u}\in \mathrm{Word}\left({I}×{2}_{𝑜}\right)\wedge {T}:{I}×{2}_{𝑜}⟶{B}\right)\to {T}\circ {u}\in \mathrm{Word}{B}$
78 65 67 77 syl2anc ${⊢}\left({\phi }\wedge \left({t}\in {W}\wedge {u}\in {W}\right)\right)\to {T}\circ {u}\in \mathrm{Word}{B}$
79 1 13 gsumccat ${⊢}\left({H}\in \mathrm{Mnd}\wedge {T}\circ {t}\in \mathrm{Word}{B}\wedge {T}\circ {u}\in \mathrm{Word}{B}\right)\to {\sum }_{{H}}\left(\left({T}\circ {t}\right)\mathrm{++}\left({T}\circ {u}\right)\right)=\left({\sum }_{{H}},\left({T}\circ {t}\right)\right){+}_{{H}}\left({\sum }_{{H}},\left({T}\circ {u}\right)\right)$
80 73 76 78 79 syl3anc ${⊢}\left({\phi }\wedge \left({t}\in {W}\wedge {u}\in {W}\right)\right)\to {\sum }_{{H}}\left(\left({T}\circ {t}\right)\mathrm{++}\left({T}\circ {u}\right)\right)=\left({\sum }_{{H}},\left({T}\circ {t}\right)\right){+}_{{H}}\left({\sum }_{{H}},\left({T}\circ {u}\right)\right)$
81 63 70 80 3eqtrd
82 7 9 8 12 frgpadd
84 83 fveq2d
85 1 2 3 4 5 6 7 8 9 10 11 frgpupval
96 39 95 syldan ${⊢}\left(\left({\phi }\wedge {a}\in {X}\right)\wedge {c}\in {X}\right)\to {E}\left({a}{+}_{{G}}{c}\right)={E}\left({a}\right){+}_{{H}}{E}\left({c}\right)$
97 96 anasss ${⊢}\left({\phi }\wedge \left({a}\in {X}\wedge {c}\in {X}\right)\right)\to {E}\left({a}{+}_{{G}}{c}\right)={E}\left({a}\right){+}_{{H}}{E}\left({c}\right)$
98 10 1 12 13 15 4 16 97 isghmd ${⊢}{\phi }\to {E}\in \left({G}\mathrm{GrpHom}{H}\right)$