submgmcl

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

		Ref	Expression
	Hypothesis	submgmcl.p	$⊢ \underset{˙}{+} = +_{M}$
	Assertion	submgmcl	$⊢ (S \in SubMgm (M) \land X \in S \land Y \in S) \to X \underset{˙}{+} Y \in S$

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

Metamath Proof Explorer