Theorem nsgbi

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

	Ref	Expression
Hypotheses	isnsg.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	isnsg.2	⊢ + = ( +g ‘ 𝐺 )
Assertion	nsgbi	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 + 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		isnsg.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		isnsg.2	⊢ + = ( +g ‘ 𝐺 )
3	1 2	isnsg	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ) )
4	3	simprbi	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) )
5		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 + 𝑦 ) = ( 𝐴 + 𝑦 ) )
6	5	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝐴 + 𝑦 ) ∈ 𝑆 ) )
7		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 + 𝑥 ) = ( 𝑦 + 𝐴 ) )
8	7	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 + 𝑥 ) ∈ 𝑆 ↔ ( 𝑦 + 𝐴 ) ∈ 𝑆 ) )
9	6 8	bibi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝐴 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝐴 ) ∈ 𝑆 ) ) )
10		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 + 𝑦 ) = ( 𝐴 + 𝐵 ) )
11	10	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 + 𝑦 ) ∈ 𝑆 ↔ ( 𝐴 + 𝐵 ) ∈ 𝑆 ) )
12		oveq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 + 𝐴 ) = ( 𝐵 + 𝐴 ) )
13	12	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 + 𝐴 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) )
14	11 13	bibi12d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝐴 ) ∈ 𝑆 ) ↔ ( ( 𝐴 + 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) ) )
15	9 14	rspc2v	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) → ( ( 𝐴 + 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) ) )
16	4 15	syl5com	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 + 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) ) )
17	16	3impib	⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 + 𝐵 ) ∈ 𝑆 ↔ ( 𝐵 + 𝐴 ) ∈ 𝑆 ) )