Theorem frgpuptf

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$$
Assertion	frgpuptf	$$⊢\phi \to T:I\times 2_{𝑜}⟶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	6	ffvelcdmda	$$⊢\left(\phi \wedge y\in I\right)\to F\left(y\right)\in B$$
8	7	adantrr	$$⊢\left(\phi \wedge \left(y\in I\wedge z\in 2_{𝑜}\right)\right)\to F\left(y\right)\in B$$
9	1 2	grpinvcl	$$⊢\left(H\in \mathrm{Grp}\wedge F\left(y\right)\in B\right)\to N\left(F\left(y\right)\right)\in B$$
10	4 8 9	syl2an2r	$$⊢\left(\phi \wedge \left(y\in I\wedge z\in 2_{𝑜}\right)\right)\to N\left(F\left(y\right)\right)\in B$$
11	8 10	ifcld	$$⊢\left(\phi \wedge \left(y\in I\wedge z\in 2_{𝑜}\right)\right)\to if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)\in B$$
12	11	ralrimivva	$$⊢\phi \to \forall y\in I\forall z\in 2_{𝑜}if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)\in B$$
13	3	fmpo	$$⊢\forall y\in I\forall z\in 2_{𝑜}if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)\in B\leftrightarrow T:I\times 2_{𝑜}⟶B$$
14	12 13	sylib	$$⊢\phi \to T:I\times 2_{𝑜}⟶B$$