Theorem nsgbi

Description: Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		isnsg.1	$$⊢X={\mathrm{Base}}_G$$
2		isnsg.2	$$⊢\underset{\dot{}}{+}={+}_G$$
3	1 2	isnsg	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\leftrightarrow \left(S\in \mathrm{SubGrp}\left(G\right)\wedge \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)\right)$$
4	3	simprbi	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)$$
5		oveq1	$$⊢x=A\to x\underset{\dot{}}{+}y=A\underset{\dot{}}{+}y$$
6	5	eleq1d	$$⊢x=A\to \left(x\underset{\dot{}}{+}y\in S\leftrightarrow A\underset{\dot{}}{+}y\in S\right)$$
7		oveq2	$$⊢x=A\to y\underset{\dot{}}{+}x=y\underset{\dot{}}{+}A$$
8	7	eleq1d	$$⊢x=A\to \left(y\underset{\dot{}}{+}x\in S\leftrightarrow y\underset{\dot{}}{+}A\in S\right)$$
9	6 8	bibi12d	$$⊢x=A\to \left(\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)\leftrightarrow \left(A\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}A\in S\right)\right)$$
10		oveq2	$$⊢y=B\to A\underset{\dot{}}{+}y=A\underset{\dot{}}{+}B$$
11	10	eleq1d	$$⊢y=B\to \left(A\underset{\dot{}}{+}y\in S\leftrightarrow A\underset{\dot{}}{+}B\in S\right)$$
12		oveq1	$$⊢y=B\to y\underset{\dot{}}{+}A=B\underset{\dot{}}{+}A$$
13	12	eleq1d	$$⊢y=B\to \left(y\underset{\dot{}}{+}A\in S\leftrightarrow B\underset{\dot{}}{+}A\in S\right)$$
14	11 13	bibi12d	$$⊢y=B\to \left(\left(A\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}A\in S\right)\leftrightarrow \left(A\underset{\dot{}}{+}B\in S\leftrightarrow B\underset{\dot{}}{+}A\in S\right)\right)$$
15	9 14	rspc2v	$$⊢\left(A\in X\wedge B\in X\right)\to \left(\forall x\in X\forall y\in X\left(x\underset{\dot{}}{+}y\in S\leftrightarrow y\underset{\dot{}}{+}x\in S\right)\to \left(A\underset{\dot{}}{+}B\in S\leftrightarrow B\underset{\dot{}}{+}A\in S\right)\right)$$
16	4 15	syl5com	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \left(\left(A\in X\wedge B\in X\right)\to \left(A\underset{\dot{}}{+}B\in S\leftrightarrow B\underset{\dot{}}{+}A\in S\right)\right)$$
17	16	3impib	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge A\in X\wedge B\in X\right)\to \left(A\underset{\dot{}}{+}B\in S\leftrightarrow B\underset{\dot{}}{+}A\in S\right)$$