Theorem conjsubgen

Description: A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypotheses	conjghm.x	$$⊢X={\mathrm{Base}}_G$$
	conjghm.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	conjghm.m	$$⊢\underset{\dot{}}{-}={-}_G$$
	conjsubg.f	$$⊢F=\left(x\in S⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)$$
Assertion	conjsubgen	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to S\approx \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		conjghm.x	$$⊢X={\mathrm{Base}}_G$$
2		conjghm.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		conjghm.m	$$⊢\underset{\dot{}}{-}={-}_G$$
4		conjsubg.f	$$⊢F=\left(x\in S⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)$$
5		subgrcl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
6		eqid	$$⊢\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)=\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)$$
7	1 2 3 6	conjghm	$$⊢\left(G\in \mathrm{Grp}\wedge A\in X\right)\to \left(\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\in \left(G\mathrm{GrpHom}G\right)\wedge \left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right):X\underset{1-1\; onto}{⟶}X\right)$$
8	5 7	sylan	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to \left(\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\in \left(G\mathrm{GrpHom}G\right)\wedge \left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right):X\underset{1-1\; onto}{⟶}X\right)$$
9		f1of1	$$⊢\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right):X\underset{1-1\; onto}{⟶}X\to \left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right):X\underset{1-1}{⟶}X$$
10	8 9	simpl2im	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to \left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right):X\underset{1-1}{⟶}X$$
11	1	subgss	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S\subseteq X$$
12	11	adantr	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to S\subseteq X$$
13		f1ssres	$$⊢\left(\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right):X\underset{1-1}{⟶}X\wedge S\subseteq X\right)\to \left({\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S\right):S\underset{1-1}{⟶}X$$
14	10 12 13	syl2anc	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to \left({\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S\right):S\underset{1-1}{⟶}X$$
15	12	resmptd	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to {\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S=\left(x\in S⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)$$
16	15 4	eqtr4di	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to {\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S=F$$
17		f1eq1	$$⊢{\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S=F\to \left(\left({\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S\right):S\underset{1-1}{⟶}X\leftrightarrow F:S\underset{1-1}{⟶}X\right)$$
18	16 17	syl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to \left(\left({\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S\right):S\underset{1-1}{⟶}X\leftrightarrow F:S\underset{1-1}{⟶}X\right)$$
19	14 18	mpbid	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to F:S\underset{1-1}{⟶}X$$
20		f1f1orn	$$⊢F:S\underset{1-1}{⟶}X\to F:S\underset{1-1\; onto}{⟶}\mathrm{ran}F$$
21	19 20	syl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to F:S\underset{1-1\; onto}{⟶}\mathrm{ran}F$$
22		f1oeng	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge F:S\underset{1-1\; onto}{⟶}\mathrm{ran}F\right)\to S\approx \mathrm{ran}F$$
23	21 22	syldan	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to S\approx \mathrm{ran}F$$