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		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\times 2_{𝑜}\right)\right)\subseteq \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
15	7 14	eqsstri	$$⊢W\subseteq \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
16	15	sseli	$$⊢g\in W\to g\in \mathrm{Word}\left(I\times 2_{𝑜}\right)$$
17	1 2 3 4 5 6	frgpuptf	$$⊢\phi \to T:I\times 2_{𝑜}⟶B$$
18		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$$
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	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}W$$
23	22	a1i	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}W$$
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	$$⊢\left(\phi \wedge g\underset{\dot{}}{\sim }h\right)\to {\sum }_H\left(T\circ g\right)={\sum }_H\left(T\circ h\right)$$
29	11 21 23 25 27 28	qliftfund	$$⊢\phi \to \mathrm{Fun}E$$
30	11 21 23 25	qliftf	$$⊢\phi \to \left(\mathrm{Fun}E\leftrightarrow E:W/\underset{\dot{}}{\sim }⟶B\right)$$
31	29 30	mpbid	$$⊢\phi \to E:W/\underset{\dot{}}{\sim }⟶B$$
32		eqid	$$⊢\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)$$
33	9 32 8	frgpval	$$⊢I\in V\to G=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right){/}_{𝑠}\underset{\dot{}}{\sim }$$
34	5 33	syl	$$⊢\phi \to G=\mathrm{freeMnd}\left(I\times 2_{𝑜}\right){/}_{𝑠}\underset{\dot{}}{\sim }$$
35		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
36		xpexg	$$⊢\left(I\in V\wedge 2_{𝑜}\in \mathrm{On}\right)\to I\times 2_{𝑜}\in \mathrm{V}$$
37	5 35 36	sylancl	$$⊢\phi \to I\times 2_{𝑜}\in \mathrm{V}$$
38		wrdexg	$$⊢I\times 2_{𝑜}\in \mathrm{V}\to \mathrm{Word}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
39		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)$$
40	37 38 39	3syl	$$⊢\phi \to \mathrm{I}\left(\mathrm{Word}\left(I\times 2_{𝑜}\right)\right)=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
41	7 40	syl5eq	$$⊢\phi \to W=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
42		eqid	$$⊢{\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}={\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}$$
43	32 42	frmdbas	$$⊢I\times 2_{𝑜}\in \mathrm{V}\to {\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
44	37 43	syl	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}=\mathrm{Word}\left(I\times 2_{𝑜}\right)$$
45	41 44	eqtr4d	$$⊢\phi \to W={\mathrm{Base}}_{\mathrm{freeMnd}\left(I\times 2_{𝑜}\right)}$$
46	8	fvexi	$$⊢\underset{\dot{}}{\sim }\in \mathrm{V}$$
47	46	a1i	$$⊢\phi \to \underset{\dot{}}{\sim }\in \mathrm{V}$$
48		fvexd	$$⊢\phi \to \mathrm{freeMnd}\left(I\times 2_{𝑜}\right)\in \mathrm{V}$$
49	34 45 47 48	qusbas	$$⊢\phi \to W/\underset{\dot{}}{\sim }={\mathrm{Base}}_G$$
50	10 49	eqtr4id	$$⊢\phi \to X=W/\underset{\dot{}}{\sim }$$
51	50	feq2d	$$⊢\phi \to \left(E:X⟶B\leftrightarrow E:W/\underset{\dot{}}{\sim }⟶B\right)$$
52	31 51	mpbird	$$⊢\phi \to E:X⟶B$$