This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐺 ) )