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\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	frgpupval	$$⊢\left(\phi \wedge A\in W\right)\to E\left(\left[A\right]\underset{\dot{}}{\sim }\right)={\sum }_H\left(T\circ A\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\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		ovexd	$$⊢\left(\phi \wedge g\in W\right)\to {\sum }_H\left(T\circ g\right)\in \mathrm{V}$$
13	7 8	efger	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}W$$
14	13	a1i	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}W$$
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	$$⊢\left(\phi \wedge A\in W\right)\to E\left(\left[A\right]\underset{\dot{}}{\sim }\right)={\sum }_H\left(T\circ A\right)$$