Theorem cayleylem2

Description: Lemma for cayley . (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	cayleylem1.x	$$⊢X={\mathrm{Base}}_G$$
	cayleylem1.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	cayleylem1.u	$$⊢\underset{\dot{}}{0}=0_G$$
	cayleylem1.h	$$⊢H=\mathrm{SymGrp}\left(X\right)$$
	cayleylem1.s	$$⊢S={\mathrm{Base}}_H$$
	cayleylem1.f	$$⊢F=\left(g\in X⟼\left(a\in X⟼g\underset{\dot{}}{+}a\right)\right)$$
Assertion	cayleylem2	$$⊢G\in \mathrm{Grp}\to F:X\underset{1-1}{⟶}S$$

Proof

Step	Hyp	Ref	Expression
1		cayleylem1.x	$$⊢X={\mathrm{Base}}_G$$
2		cayleylem1.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		cayleylem1.u	$$⊢\underset{\dot{}}{0}=0_G$$
4		cayleylem1.h	$$⊢H=\mathrm{SymGrp}\left(X\right)$$
5		cayleylem1.s	$$⊢S={\mathrm{Base}}_H$$
6		cayleylem1.f	$$⊢F=\left(g\in X⟼\left(a\in X⟼g\underset{\dot{}}{+}a\right)\right)$$
7		fveq1	$$⊢F\left(x\right)=0_H\to F\left(x\right)\left(\underset{\dot{}}{0}\right)=0_H\left(\underset{\dot{}}{0}\right)$$
8		simpr	$$⊢\left(G\in \mathrm{Grp}\wedge x\in X\right)\to x\in X$$
9	1 3	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in X$$
10	9	adantr	$$⊢\left(G\in \mathrm{Grp}\wedge x\in X\right)\to \underset{\dot{}}{0}\in X$$
11	6 1	grplactval	$$⊢\left(x\in X\wedge \underset{\dot{}}{0}\in X\right)\to F\left(x\right)\left(\underset{\dot{}}{0}\right)=x\underset{\dot{}}{+}\underset{\dot{}}{0}$$
12	8 10 11	syl2anc	$$⊢\left(G\in \mathrm{Grp}\wedge x\in X\right)\to F\left(x\right)\left(\underset{\dot{}}{0}\right)=x\underset{\dot{}}{+}\underset{\dot{}}{0}$$
13	1 2 3	grprid	$$⊢\left(G\in \mathrm{Grp}\wedge x\in X\right)\to x\underset{\dot{}}{+}\underset{\dot{}}{0}=x$$
14	12 13	eqtrd	$$⊢\left(G\in \mathrm{Grp}\wedge x\in X\right)\to F\left(x\right)\left(\underset{\dot{}}{0}\right)=x$$
15	1	fvexi	$$⊢X\in \mathrm{V}$$
16	4	symgid	$$⊢X\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_X=0_H$$
17	15 16	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_X=0_H$$
18	17	fveq1i	$$⊢\left({\mathrm{I}\upharpoonright }_X\right)\left(\underset{\dot{}}{0}\right)=0_H\left(\underset{\dot{}}{0}\right)$$
19		fvresi	$$⊢\underset{\dot{}}{0}\in X\to \left({\mathrm{I}\upharpoonright }_X\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
20	10 19	syl	$$⊢\left(G\in \mathrm{Grp}\wedge x\in X\right)\to \left({\mathrm{I}\upharpoonright }_X\right)\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
21	18 20	eqtr3id	$$⊢\left(G\in \mathrm{Grp}\wedge x\in X\right)\to 0_H\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
22	14 21	eqeq12d	$$⊢\left(G\in \mathrm{Grp}\wedge x\in X\right)\to \left(F\left(x\right)\left(\underset{\dot{}}{0}\right)=0_H\left(\underset{\dot{}}{0}\right)\leftrightarrow x=\underset{\dot{}}{0}\right)$$
23	7 22	syl5ib	$$⊢\left(G\in \mathrm{Grp}\wedge x\in X\right)\to \left(F\left(x\right)=0_H\to x=\underset{\dot{}}{0}\right)$$
24	23	ralrimiva	$$⊢G\in \mathrm{Grp}\to \forall x\in X\left(F\left(x\right)=0_H\to x=\underset{\dot{}}{0}\right)$$
25	1 2 3 4 5 6	cayleylem1	$$⊢G\in \mathrm{Grp}\to F\in \left(G\mathrm{GrpHom}H\right)$$
26		eqid	$$⊢0_H=0_H$$
27	1 5 3 26	ghmf1	$$⊢F\in \left(G\mathrm{GrpHom}H\right)\to \left(F:X\underset{1-1}{⟶}S\leftrightarrow \forall x\in X\left(F\left(x\right)=0_H\to x=\underset{\dot{}}{0}\right)\right)$$
28	25 27	syl	$$⊢G\in \mathrm{Grp}\to \left(F:X\underset{1-1}{⟶}S\leftrightarrow \forall x\in X\left(F\left(x\right)=0_H\to x=\underset{\dot{}}{0}\right)\right)$$
29	24 28	mpbird	$$⊢G\in \mathrm{Grp}\to F:X\underset{1-1}{⟶}S$$