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 ⊢ G ∈ Abel → NrmSGrp ⁡ G = SubGrp ⁡ G

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base G = Base G
2 eqid ⊢ + G = + G
3 1 2 ablcom ⊢ G ∈ Abel ∧ y ∈ Base G ∧ z ∈ Base G → y + G z = z + G y
4 3 3expb ⊢ G ∈ Abel ∧ y ∈ Base G ∧ z ∈ Base G → y + G z = z + G y
5 4 eleq1d ⊢ G ∈ Abel ∧ y ∈ Base G ∧ z ∈ Base G → y + G z ∈ x ↔ z + G y ∈ x
6 5 ralrimivva ⊢ G ∈ Abel → ∀ y ∈ Base G ∀ z ∈ Base G y + G z ∈ x ↔ z + G y ∈ x
7 1 2 isnsg ⊢ x ∈ NrmSGrp ⁡ G ↔ x ∈ SubGrp ⁡ G ∧ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ∈ x ↔ z + G y ∈ x
8 7 rbaib ⊢ ∀ y ∈ Base G ∀ z ∈ Base G y + G z ∈ x ↔ z + G y ∈ x → x ∈ NrmSGrp ⁡ G ↔ x ∈ SubGrp ⁡ G
9 6 8 syl ⊢ G ∈ Abel → x ∈ NrmSGrp ⁡ G ↔ x ∈ SubGrp ⁡ G
10 9 eqrdv ⊢ G ∈ Abel → NrmSGrp ⁡ G = SubGrp ⁡ G