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\times 2_{𝑜}\right)\right)$$
	frgpup.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
	frgpup.g	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
	frgpup.x	$$⊢X={\mathrm{Base}}_G$$
	frgpup.e	$$⊢E=\mathrm{ran}\left(g\in W⟼⟨\left[g\right]\underset{\dot{}}{\sim },{\sum }_H\left(T\circ g\right)⟩\right)$$
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\times 2_{𝑜}\right)\right)$$
8		frgpup.r	$$⊢\underset{\dot{}}{\sim }={~}_{\mathit{FG}}\left(I\right)$$
9		frgpup.g	$$⊢G=\mathrm{freeGrp}\left(I\right)$$
10		frgpup.x	$$⊢X={\mathrm{Base}}_G$$
11		frgpup.e	$$⊢E=\mathrm{ran}\left(g\in W⟼⟨\left[g\right]\underset{\dot{}}{\sim },{\sum }_H\left(T\circ g\right)⟩\right)$$
12	4	grpmndd	$$⊢\phi \to H\in \mathrm{Mnd}$$
13		fviss	$$⊢\mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)\subseteq \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
14	7 13	eqsstri	$$⊢W\subseteq \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
15	14	sseli	$$⊢g\in W\to g\in \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
16	1 2 3 4 5 6	frgpuptf	$$⊢\phi \to T:I\times 2_{𝑜}⟶B$$
17		wrdco	$$⊢\left(g\in \mathrm{Word}\left(I\times 2_{𝑜}\right)\wedge T:I\times 2_{𝑜}⟶B\right)\to T\circ g\in \mathrm{Word}B$$
18	15 16 17	syl2anr	$$⊢\left(\phi \wedge g\in W\right)\to T\circ g\in \mathrm{Word}B$$
19	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$$
20	12 18 19	syl2an2r	$$⊢\left(\phi \wedge g\in W\right)\to {\sum }_H\left(T\circ g\right)\in B$$
21	7 8	efger	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}W$$
22	21	a1i	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}W$$
23	7	fvexi	$$⊢W\in \mathrm{V}$$
24	23	a1i	$$⊢\phi \to W\in \mathrm{V}$$
25		coeq2	$$⊢g=h\to T\circ g=T\circ h$$
26	25	oveq2d	$$⊢g=h\to {\sum }_H\left(T\circ g\right)={\sum }_H\left(T\circ h\right)$$
27	1 2 3 4 5 6 7 8	frgpuplem	$$⊢\left(\phi \wedge g\underset{\dot{}}{\sim }h\right)\to {\sum }_H\left(T\circ g\right)={\sum }_H\left(T\circ h\right)$$
28	11 20 22 24 26 27	qliftfund	$$⊢\phi \to \mathrm{Fun}E$$
29	11 20 22 24	qliftf	$$⊢\phi \to \left(\mathrm{Fun}E\leftrightarrow E:W/\underset{\dot{}}{\sim }⟶B\right)$$
30	28 29	mpbid	$$⊢\phi \to E:W/\underset{\dot{}}{\sim }⟶B$$
31		eqid	$$⊢\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)$$
32	9 31 8	frgpval	$$⊢I\in V\to G=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right){/}_{𝑠}\underset{\dot{}}{\sim }$$
33	5 32	syl	$$⊢\phi \to G=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right){/}_{𝑠}\underset{\dot{}}{\sim }$$
34		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
35		xpexg	$$⊢\left(I\in V\wedge 2_{𝑜}\in \mathrm{On}\right)\to I\times 2_{𝑜}\in \mathrm{V}$$
36	5 34 35	sylancl	$$⊢\phi \to I\times 2_{𝑜}\in \mathrm{V}$$
37		wrdexg	$$⊢I\times 2_{𝑜}\in \mathrm{V}\to \mathrm{Word}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
38		fvi	$$⊢\mathrm{Word}\left(I\times 2_{𝑜}\right)\in \mathrm{V}\to \mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
39	36 37 38	3syl	$$⊢\phi \to \mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
40	7 39	syl5eq	$$⊢\phi \to W=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
41		eqid	$$⊢{\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}={\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}$$
42	31 41	frmdbas	$$⊢I\times 2_{𝑜}\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
43	36 42	syl	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
44	40 43	eqtr4d	$$⊢\phi \to W={\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}$$
45	8	fvexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
46	45	a1i	$$⊢\phi \to \underset{\dot{}}{\sim }\in \mathrm{V}$$
47		fvexd	$$⊢\phi \to \mathrm{freeMnd}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
48	33 44 46 47	qusbas	$$⊢\phi \to W/\underset{\dot{}}{\sim }={\mathrm{Base}}_G$$
49	10 48	eqtr4id	$$⊢\phi \to X=W/\underset{\dot{}}{\sim }$$
50	49	feq2d	$$⊢\phi \to \left(E:X⟶B\leftrightarrow E:W/\underset{\dot{}}{\sim }⟶B\right)$$
51	30 50	mpbird	$$⊢\phi \to E:X⟶B$$