submmnd

Description: Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015)

		Ref	Expression
	Hypothesis	submmnd.h	$⊢ H = M ↾_{𝑠} S$
	Assertion	submmnd	$⊢ S \in SubMnd (M) \to H \in Mnd$

Step	Hyp	Ref	Expression
1		submmnd.h	$⊢ H = M ↾_{𝑠} S$
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	issubm2	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq {Base}_{M} \land 0_{M} \in S \land H \in Mnd))$
6	2 5	syl	$⊢ S \in SubMnd (M) \to (S \in SubMnd (M) \leftrightarrow (S \subseteq {Base}_{M} \land 0_{M} \in S \land H \in Mnd))$
7	6	ibi	$⊢ S \in SubMnd (M) \to (S \subseteq {Base}_{M} \land 0_{M} \in S \land H \in Mnd)$
8	7	simp3d	$⊢ S \in SubMnd (M) \to H \in Mnd$

Metamath Proof Explorer