Metamath Proof Explorer

Theorem subgsubm

Description: A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Assertion subgsubm ⊢ S ∈ SubGrp ⁡ G → S ∈ SubMnd ⁡ G

Proof

Step Hyp Ref Expression
1 subgrcl ⊢ S ∈ SubGrp ⁡ G → G ∈ Grp
2 eqid ⊢ inv g ⁡ G = inv g ⁡ G
3 2 issubg3 ⊢ G ∈ Grp → S ∈ SubGrp ⁡ G ↔ S ∈ SubMnd ⁡ G ∧ ∀ x ∈ S inv g ⁡ G ⁡ x ∈ S
4 1 3 syl ⊢ S ∈ SubGrp ⁡ G → S ∈ SubGrp ⁡ G ↔ S ∈ SubMnd ⁡ G ∧ ∀ x ∈ S inv g ⁡ G ⁡ x ∈ S
5 4 ibi ⊢ S ∈ SubGrp ⁡ G → S ∈ SubMnd ⁡ G ∧ ∀ x ∈ S inv g ⁡ G ⁡ x ∈ S
6 5 simpld ⊢ S ∈ SubGrp ⁡ G → S ∈ SubMnd ⁡ G