Metamath Proof Explorer

Theorem submgmmgm

Description: Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis submgmmgm.h ⊢ H = M ↾ 𝑠 S
Assertion submgmmgm ⊢ S ∈ SubMgm ⁡ M → H ∈ Mgm

Proof

Step Hyp Ref Expression
1 submgmmgm.h ⊢ H = M ↾ 𝑠 S
2 submgmrcl ⊢ S ∈ SubMgm ⁡ M → M ∈ Mgm
3 eqid ⊢ Base M = Base M
4 3 1 issubmgm2 ⊢ M ∈ Mgm → S ∈ SubMgm ⁡ M ↔ S ⊆ Base M ∧ H ∈ Mgm
5 2 4 syl ⊢ S ∈ SubMgm ⁡ M → S ∈ SubMgm ⁡ M ↔ S ⊆ Base M ∧ H ∈ Mgm
6 5 ibi ⊢ S ∈ SubMgm ⁡ M → S ⊆ Base M ∧ H ∈ Mgm
7 6 simprd ⊢ S ∈ SubMgm ⁡ M → H ∈ Mgm