Description: A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | nsgsubg | ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) | |
2 | eqid | ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) | |
3 | 1 2 | isnsg | ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑆 ) ) ) |
4 | 3 | simplbi | ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |