submcl

Description: Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015)

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

Step	Hyp	Ref	Expression
1		submcl.p	$⊢ \underset{˙}{+} = +_{M}$
2		submrcl	$⊢ S \in SubMnd (M) \to M \in Mnd$
3		eqid	$⊢ {Base}_{M} = {Base}_{M}$
4		eqid	$⊢ 0_{M} = 0_{M}$
5	3 4 1	issubm	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq {Base}_{M} \land 0_{M} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S))$
6	2 5	syl	$⊢ S \in SubMnd (M) \to (S \in SubMnd (M) \leftrightarrow (S \subseteq {Base}_{M} \land 0_{M} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S))$
7	6	ibi	$⊢ S \in SubMnd (M) \to (S \subseteq {Base}_{M} \land 0_{M} \in S \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S)$
8	7	simp3d	$⊢ S \in SubMnd (M) \to \forall x \in S \forall y \in S x \underset{˙}{+} y \in S$
9		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$
10	8 9	sylan2	$⊢ ((X \in S \land Y \in S) \land S \in SubMnd (M)) \to X \underset{˙}{+} Y \in S$
11	10	ancoms	$⊢ (S \in SubMnd (M) \land (X \in S \land Y \in S)) \to X \underset{˙}{+} Y \in S$
12	11	3impb	$⊢ (S \in SubMnd (M) \land X \in S \land Y \in S) \to X \underset{˙}{+} Y \in S$

Metamath Proof Explorer