Theorem submgmcl

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

	Ref	Expression
Hypothesis	submgmcl.p	$$⊢\underset{\dot{}}{+}={+}_M$$
Assertion	submgmcl	$$⊢\left(S\in \mathrm{SubMgm}\left(M\right)\wedge X\in S\wedge Y\in S\right)\to X\underset{\dot{}}{+}Y\in S$$

Proof

Step	Hyp	Ref	Expression
1		submgmcl.p	$$⊢\underset{\dot{}}{+}={+}_M$$
2		submgmrcl	$$⊢S\in \mathrm{SubMgm}\left(M\right)\to M\in \mathrm{Mgm}$$
3		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
4	3 1	issubmgm	$$⊢M\in \mathrm{Mgm}\to \left(S\in \mathrm{SubMgm}\left(M\right)\leftrightarrow \left(S\subseteq {\mathrm{Base}}_M\wedge \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\right)\right)$$
5	2 4	syl	$$⊢S\in \mathrm{SubMgm}\left(M\right)\to \left(S\in \mathrm{SubMgm}\left(M\right)\leftrightarrow \left(S\subseteq {\mathrm{Base}}_M\wedge \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\right)\right)$$
6	5	ibi	$$⊢S\in \mathrm{SubMgm}\left(M\right)\to \left(S\subseteq {\mathrm{Base}}_M\wedge \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\right)$$
7	6	simprd	$$⊢S\in \mathrm{SubMgm}\left(M\right)\to \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S$$
8		ovrspc2v	$$⊢\left(\left(X\in S\wedge Y\in S\right)\wedge \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\right)\to X\underset{\dot{}}{+}Y\in S$$
9	7 8	sylan2	$$⊢\left(\left(X\in S\wedge Y\in S\right)\wedge S\in \mathrm{SubMgm}\left(M\right)\right)\to X\underset{\dot{}}{+}Y\in S$$
10	9	ancoms	$$⊢\left(S\in \mathrm{SubMgm}\left(M\right)\wedge \left(X\in S\wedge Y\in S\right)\right)\to X\underset{\dot{}}{+}Y\in S$$
11	10	3impb	$$⊢\left(S\in \mathrm{SubMgm}\left(M\right)\wedge X\in S\wedge Y\in S\right)\to X\underset{\dot{}}{+}Y\in S$$