Theorem conjsubg

Description: A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-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	conjsubg	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to \mathrm{ran}F\in \mathrm{SubGrp}\left(G\right)$$

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	1	subgss	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S\subseteq X$$
6	5	adantr	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to S\subseteq X$$
7		df-ima	$$⊢\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\left[S\right]=\mathrm{ran}\left({\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S\right)$$
8		resmpt	$$⊢S\subseteq X\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)$$
9	8 4	eqtr4di	$$⊢S\subseteq X\to {\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S=F$$
10	9	rneqd	$$⊢S\subseteq X\to \mathrm{ran}\left({\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\upharpoonright }_S\right)=\mathrm{ran}F$$
11	7 10	eqtrid	$$⊢S\subseteq X\to \left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\left[S\right]=\mathrm{ran}F$$
12	6 11	syl	$$⊢\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)\left[S\right]=\mathrm{ran}F$$
13		subgrcl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
14		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)$$
15	1 2 3 14	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)$$
16	13 15	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)$$
17	16	simpld	$$⊢\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)\in \left(G\mathrm{GrpHom}G\right)$$
18		simpl	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to S\in \mathrm{SubGrp}\left(G\right)$$
19		ghmima	$$⊢\left(\left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\in \left(G\mathrm{GrpHom}G\right)\wedge S\in \mathrm{SubGrp}\left(G\right)\right)\to \left(x\in X⟼\left(A\underset{\dot{}}{+}x\right)\underset{\dot{}}{-}A\right)\left[S\right]\in \mathrm{SubGrp}\left(G\right)$$
20	17 18 19	syl2anc	$$⊢\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)\left[S\right]\in \mathrm{SubGrp}\left(G\right)$$
21	12 20	eqeltrrd	$$⊢\left(S\in \mathrm{SubGrp}\left(G\right)\wedge A\in X\right)\to \mathrm{ran}F\in \mathrm{SubGrp}\left(G\right)$$