Theorem frgpuptinv

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$$
	frgpuptinv.m	$$⊢M=\left(y\in I,z\in 2_{𝑜}⟼⟨y,1_{𝑜}\setminus z⟩\right)$$
Assertion	frgpuptinv	$$⊢\left(\phi \wedge A\in \left(I\times 2_{𝑜}\right)\right)\to T\left(M\left(A\right)\right)=N\left(T\left(A\right)\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		frgpuptinv.m	$$⊢M=\left(y\in I,z\in 2_{𝑜}⟼⟨y,1_{𝑜}\setminus z⟩\right)$$
8		elxp2	$$⊢A\in \left(I\times 2_{𝑜}\right)\leftrightarrow \exists a\in I\exists b\in 2_{𝑜}A=⟨a,b⟩$$
9	7	efgmval	$$⊢\left(a\in I\wedge b\in 2_{𝑜}\right)\to aMb=⟨a,1_{𝑜}\setminus b⟩$$
10	9	adantl	$$⊢\left(\phi \wedge \left(a\in I\wedge b\in 2_{𝑜}\right)\right)\to aMb=⟨a,1_{𝑜}\setminus b⟩$$
11	10	fveq2d	$$⊢\left(\phi \wedge \left(a\in I\wedge b\in 2_{𝑜}\right)\right)\to T\left(aMb\right)=T\left(⟨a,1_{𝑜}\setminus b⟩\right)$$
12		df-ov	$$⊢aT\left(1_{𝑜}\setminus b\right)=T\left(⟨a,1_{𝑜}\setminus b⟩\right)$$
13	11 12	eqtr4di	$$⊢\left(\phi \wedge \left(a\in I\wedge b\in 2_{𝑜}\right)\right)\to T\left(aMb\right)=aT\left(1_{𝑜}\setminus b\right)$$
14		elpri	$$⊢b\in \left\{\varnothing ,1_{𝑜}\right\}\to \left(b=\varnothing \vee b=1_{𝑜}\right)$$
15		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
16	14 15	eleq2s	$$⊢b\in 2_{𝑜}\to \left(b=\varnothing \vee b=1_{𝑜}\right)$$
17		simpr	$$⊢\left(\phi \wedge a\in I\right)\to a\in I$$
18		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
19	18	prid2	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
20	19 15	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
21		1n0	$$⊢1_{𝑜}\ne \varnothing$$
22		neeq1	$$⊢z=1_{𝑜}\to \left(z\ne \varnothing \leftrightarrow 1_{𝑜}\ne \varnothing \right)$$
23	21 22	mpbiri	$$⊢z=1_{𝑜}\to z\ne \varnothing$$
24		ifnefalse	$$⊢z\ne \varnothing \to if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)=N\left(F\left(y\right)\right)$$
25	23 24	syl	$$⊢z=1_{𝑜}\to if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)=N\left(F\left(y\right)\right)$$
26		fveq2	$$⊢y=a\to F\left(y\right)=F\left(a\right)$$
27	26	fveq2d	$$⊢y=a\to N\left(F\left(y\right)\right)=N\left(F\left(a\right)\right)$$
28	25 27	sylan9eqr	$$⊢\left(y=a\wedge z=1_{𝑜}\right)\to if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)=N\left(F\left(a\right)\right)$$
29		fvex	$$⊢N\left(F\left(a\right)\right)\in \mathrm{V}$$
30	28 3 29	ovmpoa	$$⊢\left(a\in I\wedge 1_{𝑜}\in 2_{𝑜}\right)\to aT{1}_{𝑜}=N\left(F\left(a\right)\right)$$
31	17 20 30	sylancl	$$⊢\left(\phi \wedge a\in I\right)\to aT{1}_{𝑜}=N\left(F\left(a\right)\right)$$
32		0ex	$$⊢\varnothing \in \mathrm{V}$$
33	32	prid1	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}$$
34	33 15	eleqtrri	$$⊢\varnothing \in 2_{𝑜}$$
35		iftrue	$$⊢z=\varnothing \to if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)=F\left(y\right)$$
36	35 26	sylan9eqr	$$⊢\left(y=a\wedge z=\varnothing \right)\to if\left(z=\varnothing ,F\left(y\right),N\left(F\left(y\right)\right)\right)=F\left(a\right)$$
37		fvex	$$⊢F\left(a\right)\in \mathrm{V}$$
38	36 3 37	ovmpoa	$$⊢\left(a\in I\wedge \varnothing \in 2_{𝑜}\right)\to aT\varnothing =F\left(a\right)$$
39	17 34 38	sylancl	$$⊢\left(\phi \wedge a\in I\right)\to aT\varnothing =F\left(a\right)$$
40	39	fveq2d	$$⊢\left(\phi \wedge a\in I\right)\to N\left(aT\varnothing \right)=N\left(F\left(a\right)\right)$$
41	31 40	eqtr4d	$$⊢\left(\phi \wedge a\in I\right)\to aT{1}_{𝑜}=N\left(aT\varnothing \right)$$
42		difeq2	$$⊢b=\varnothing \to 1_{𝑜}\setminus b=1_{𝑜}\setminus \varnothing$$
43		dif0	$$⊢1_{𝑜}\setminus \varnothing =1_{𝑜}$$
44	42 43	eqtrdi	$$⊢b=\varnothing \to 1_{𝑜}\setminus b=1_{𝑜}$$
45	44	oveq2d	$$⊢b=\varnothing \to aT\left(1_{𝑜}\setminus b\right)=aT{1}_{𝑜}$$
46		oveq2	$$⊢b=\varnothing \to aTb=aT\varnothing$$
47	46	fveq2d	$$⊢b=\varnothing \to N\left(aTb\right)=N\left(aT\varnothing \right)$$
48	45 47	eqeq12d	$$⊢b=\varnothing \to \left(aT\left(1_{𝑜}\setminus b\right)=N\left(aTb\right)\leftrightarrow aT{1}_{𝑜}=N\left(aT\varnothing \right)\right)$$
49	41 48	syl5ibrcom	$$⊢\left(\phi \wedge a\in I\right)\to \left(b=\varnothing \to aT\left(1_{𝑜}\setminus b\right)=N\left(aTb\right)\right)$$
50	41	fveq2d	$$⊢\left(\phi \wedge a\in I\right)\to N\left(aT{1}_{𝑜}\right)=N\left(N\left(aT\varnothing \right)\right)$$
51	6	ffvelcdmda	$$⊢\left(\phi \wedge a\in I\right)\to F\left(a\right)\in B$$
52	39 51	eqeltrd	$$⊢\left(\phi \wedge a\in I\right)\to aT\varnothing \in B$$
53	1 2	grpinvinv	$$⊢\left(H\in \mathrm{Grp}\wedge aT\varnothing \in B\right)\to N\left(N\left(aT\varnothing \right)\right)=aT\varnothing$$
54	4 52 53	syl2an2r	$$⊢\left(\phi \wedge a\in I\right)\to N\left(N\left(aT\varnothing \right)\right)=aT\varnothing$$
55	50 54	eqtr2d	$$⊢\left(\phi \wedge a\in I\right)\to aT\varnothing =N\left(aT{1}_{𝑜}\right)$$
56		difeq2	$$⊢b=1_{𝑜}\to 1_{𝑜}\setminus b=1_{𝑜}\setminus 1_{𝑜}$$
57		difid	$$⊢1_{𝑜}\setminus 1_{𝑜}=\varnothing$$
58	56 57	eqtrdi	$$⊢b=1_{𝑜}\to 1_{𝑜}\setminus b=\varnothing$$
59	58	oveq2d	$$⊢b=1_{𝑜}\to aT\left(1_{𝑜}\setminus b\right)=aT\varnothing$$
60		oveq2	$$⊢b=1_{𝑜}\to aTb=aT{1}_{𝑜}$$
61	60	fveq2d	$$⊢b=1_{𝑜}\to N\left(aTb\right)=N\left(aT{1}_{𝑜}\right)$$
62	59 61	eqeq12d	$$⊢b=1_{𝑜}\to \left(aT\left(1_{𝑜}\setminus b\right)=N\left(aTb\right)\leftrightarrow aT\varnothing =N\left(aT{1}_{𝑜}\right)\right)$$
63	55 62	syl5ibrcom	$$⊢\left(\phi \wedge a\in I\right)\to \left(b=1_{𝑜}\to aT\left(1_{𝑜}\setminus b\right)=N\left(aTb\right)\right)$$
64	49 63	jaod	$$⊢\left(\phi \wedge a\in I\right)\to \left(\left(b=\varnothing \vee b=1_{𝑜}\right)\to aT\left(1_{𝑜}\setminus b\right)=N\left(aTb\right)\right)$$
65	16 64	syl5	$$⊢\left(\phi \wedge a\in I\right)\to \left(b\in 2_{𝑜}\to aT\left(1_{𝑜}\setminus b\right)=N\left(aTb\right)\right)$$
66	65	impr	$$⊢\left(\phi \wedge \left(a\in I\wedge b\in 2_{𝑜}\right)\right)\to aT\left(1_{𝑜}\setminus b\right)=N\left(aTb\right)$$
67	13 66	eqtrd	$$⊢\left(\phi \wedge \left(a\in I\wedge b\in 2_{𝑜}\right)\right)\to T\left(aMb\right)=N\left(aTb\right)$$
68		fveq2	$$⊢A=⟨a,b⟩\to M\left(A\right)=M\left(⟨a,b⟩\right)$$
69		df-ov	$$⊢aMb=M\left(⟨a,b⟩\right)$$
70	68 69	eqtr4di	$$⊢A=⟨a,b⟩\to M\left(A\right)=aMb$$
71	70	fveq2d	$$⊢A=⟨a,b⟩\to T\left(M\left(A\right)\right)=T\left(aMb\right)$$
72		fveq2	$$⊢A=⟨a,b⟩\to T\left(A\right)=T\left(⟨a,b⟩\right)$$
73		df-ov	$$⊢aTb=T\left(⟨a,b⟩\right)$$
74	72 73	eqtr4di	$$⊢A=⟨a,b⟩\to T\left(A\right)=aTb$$
75	74	fveq2d	$$⊢A=⟨a,b⟩\to N\left(T\left(A\right)\right)=N\left(aTb\right)$$
76	71 75	eqeq12d	$$⊢A=⟨a,b⟩\to \left(T\left(M\left(A\right)\right)=N\left(T\left(A\right)\right)\leftrightarrow T\left(aMb\right)=N\left(aTb\right)\right)$$
77	67 76	syl5ibrcom	$$⊢\left(\phi \wedge \left(a\in I\wedge b\in 2_{𝑜}\right)\right)\to \left(A=⟨a,b⟩\to T\left(M\left(A\right)\right)=N\left(T\left(A\right)\right)\right)$$
78	77	rexlimdvva	$$⊢\phi \to \left(\exists a\in I\exists b\in 2_{𝑜}A=⟨a,b⟩\to T\left(M\left(A\right)\right)=N\left(T\left(A\right)\right)\right)$$
79	8 78	biimtrid	$$⊢\phi \to \left(A\in \left(I\times 2_{𝑜}\right)\to T\left(M\left(A\right)\right)=N\left(T\left(A\right)\right)\right)$$
80	79	imp	$$⊢\left(\phi \wedge A\in \left(I\times 2_{𝑜}\right)\right)\to T\left(M\left(A\right)\right)=N\left(T\left(A\right)\right)$$