Theorem ablnsg

Description: Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Assertion	ablnsg	⊢ ( 𝐺 ∈ Abel → ( NrmSGrp ‘ 𝐺 ) = ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
2		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
3	1 2	ablcom	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) )
4	3	3expb	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) )
5	4	eleq1d	⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 ↔ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑥 ) )
6	5	ralrimivva	⊢ ( 𝐺 ∈ Abel → ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 ↔ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑥 ) )
7	1 2	isnsg	⊢ ( 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 ↔ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑥 ) ) )
8	7	rbaib	⊢ ( ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑥 ↔ ( 𝑧 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑥 ) → ( 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) )
9	6 8	syl	⊢ ( 𝐺 ∈ Abel → ( 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ) )
10	9	eqrdv	⊢ ( 𝐺 ∈ Abel → ( NrmSGrp ‘ 𝐺 ) = ( SubGrp ‘ 𝐺 ) )