Theorem nsgconj

Description: The conjugation of an element of a normal subgroup is in the subgroup. (Contributed by Mario Carneiro, 4-Feb-2015)

	Ref	Expression
Hypotheses	isnsg3.1	$$⊢X={\mathrm{Base}}_G$$
	isnsg3.2	$$⊢\underset{\dot{}}{+}={+}_G$$
	isnsg3.3	$$⊢\underset{\dot{}}{-}={-}_G$$
Assertion	nsgconj	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{-}A\in S$$

Proof

Step	Hyp	Ref	Expression
1		isnsg3.1	$$⊢X={\mathrm{Base}}_G$$
2		isnsg3.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3		isnsg3.3	$$⊢\underset{\dot{}}{-}={-}_G$$
4		nsgsubg	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to S\in \mathrm{SubGrp}\left(G\right)$$
5	4	3ad2ant1	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to S\in \mathrm{SubGrp}\left(G\right)$$
6		subgrcl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
7	5 6	syl	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to G\in \mathrm{Grp}$$
8		simp2	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to A\in X$$
9	1	subgss	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to S\subseteq X$$
10	5 9	syl	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to S\subseteq X$$
11		simp3	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to B\in S$$
12	10 11	sseldd	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to B\in X$$
13	1 2 3	grpaddsubass	$$⊢\left(G\in \mathrm{Grp}\wedge \left(A\in X\wedge B\in X\wedge A\in X\right)\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{-}A=A\underset{\dot{}}{+}\left(B\underset{\dot{}}{-}A\right)$$
14	7 8 12 8 13	syl13anc	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{-}A=A\underset{\dot{}}{+}\left(B\underset{\dot{}}{-}A\right)$$
15	1 2 3	grpnpcan	$$⊢\left(G\in \mathrm{Grp}\wedge B\in X\wedge A\in X\right)\to \left(B\underset{\dot{}}{-}A\right)\underset{\dot{}}{+}A=B$$
16	7 12 8 15	syl3anc	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to \left(B\underset{\dot{}}{-}A\right)\underset{\dot{}}{+}A=B$$
17	16 11	eqeltrd	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to \left(B\underset{\dot{}}{-}A\right)\underset{\dot{}}{+}A\in S$$
18		simp1	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to S\in \mathrm{NrmSGrp}\left(G\right)$$
19	1 3	grpsubcl	$$⊢\left(G\in \mathrm{Grp}\wedge B\in X\wedge A\in X\right)\to B\underset{\dot{}}{-}A\in X$$
20	7 12 8 19	syl3anc	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to B\underset{\dot{}}{-}A\in X$$
21	1 2	nsgbi	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge B\underset{\dot{}}{-}A\in X\wedge A\in X\right)\to \left(\left(B\underset{\dot{}}{-}A\right)\underset{\dot{}}{+}A\in S\leftrightarrow A\underset{\dot{}}{+}\left(B\underset{\dot{}}{-}A\right)\in S\right)$$
22	18 20 8 21	syl3anc	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to \left(\left(B\underset{\dot{}}{-}A\right)\underset{\dot{}}{+}A\in S\leftrightarrow A\underset{\dot{}}{+}\left(B\underset{\dot{}}{-}A\right)\in S\right)$$
23	17 22	mpbid	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to A\underset{\dot{}}{+}\left(B\underset{\dot{}}{-}A\right)\in S$$
24	14 23	eqeltrd	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in S\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{-}A\in S$$