Metamath Proof Explorer

Theorem subggrp

Description: A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis subggrp.h ⊢ H = G ↾ 𝑠 S
Assertion subggrp ⊢ S ∈ SubGrp ⁡ G → H ∈ Grp

Proof

Step Hyp Ref Expression
1 subggrp.h ⊢ H = G ↾ 𝑠 S
2 eqid ⊢ Base G = Base G
3 2 issubg ⊢ S ∈ SubGrp ⁡ G ↔ G ∈ Grp ∧ S ⊆ Base G ∧ G ↾ 𝑠 S ∈ Grp
4 3 simp3bi ⊢ S ∈ SubGrp ⁡ G → G ↾ 𝑠 S ∈ Grp
5 1 4 eqeltrid ⊢ S ∈ SubGrp ⁡ G → H ∈ Grp