subm0cl

Description: Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015)

		Ref	Expression
	Hypothesis	subm0cl.z	$⊢ \underset{˙}{0} = 0_{M}$
	Assertion	subm0cl	$⊢ S \in SubMnd (M) \to \underset{˙}{0} \in S$

Step	Hyp	Ref	Expression
1		subm0cl.z	$⊢ \underset{˙}{0} = 0_{M}$
2		submrcl	$⊢ S \in SubMnd (M) \to M \in Mnd$
3		eqid	$⊢ {Base}_{M} = {Base}_{M}$
4		eqid	$⊢ M ↾_{𝑠} S = M ↾_{𝑠} S$
5	3 1 4	issubm2	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq {Base}_{M} \land \underset{˙}{0} \in S \land M ↾_{𝑠} S \in Mnd))$
6	2 5	syl	$⊢ S \in SubMnd (M) \to (S \in SubMnd (M) \leftrightarrow (S \subseteq {Base}_{M} \land \underset{˙}{0} \in S \land M ↾_{𝑠} S \in Mnd))$
7	6	ibi	$⊢ S \in SubMnd (M) \to (S \subseteq {Base}_{M} \land \underset{˙}{0} \in S \land M ↾_{𝑠} S \in Mnd)$
8	7	simp2d	$⊢ S \in SubMnd (M) \to \underset{˙}{0} \in S$

Metamath Proof Explorer