Metamath Proof Explorer


Theorem submgmcl

Description: Submagmas are closed under the monoid operation. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis submgmcl.p + ˙ = + M
Assertion submgmcl S SubMgm M X S Y S X + ˙ Y S

Proof

Step Hyp Ref Expression
1 submgmcl.p + ˙ = + M
2 submgmrcl S SubMgm M M Mgm
3 eqid Base M = Base M
4 3 1 issubmgm M Mgm S SubMgm M S Base M x S y S x + ˙ y S
5 2 4 syl S SubMgm M S SubMgm M S Base M x S y S x + ˙ y S
6 5 ibi S SubMgm M S Base M x S y S x + ˙ y S
7 6 simprd S SubMgm M x S y S x + ˙ y S
8 ovrspc2v X S Y S x S y S x + ˙ y S X + ˙ Y S
9 7 8 sylan2 X S Y S S SubMgm M X + ˙ Y S
10 9 ancoms S SubMgm M X S Y S X + ˙ Y S
11 10 3impb S SubMgm M X S Y S X + ˙ Y S