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