Metamath Proof Explorer

Theorem issubm2

Description: Submonoids are subsets that are also monoids with the same zero. (Contributed by Mario Carneiro, 7-Mar-2015)

		Ref	Expression
	Hypotheses	issubm2.b	$⊢ B = {Base}_{M}$
		issubm2.z	$⊢ \underset{˙}{0} = 0_{M}$
		issubm2.h	$⊢ H = M ↾_{𝑠} S$
	Assertion	issubm2	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land H \in Mnd))$

Proof

Step	Hyp	Ref	Expression
1		issubm2.b	$⊢ B = {Base}_{M}$
2		issubm2.z	$⊢ \underset{˙}{0} = 0_{M}$
3		issubm2.h	$⊢ H = M ↾_{𝑠} S$
4		eqid	$⊢ +_{M} = +_{M}$
5	1 2 4	issubm	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S))$
6	1 4 2 3	issubmnd	$⊢ (M \in Mnd \land S \subseteq B \land \underset{˙}{0} \in S) \to (H \in Mnd \leftrightarrow \forall x \in S \forall y \in S x +_{M} y \in S)$
7	6	bicomd	$⊢ (M \in Mnd \land S \subseteq B \land \underset{˙}{0} \in S) \to (\forall x \in S \forall y \in S x +_{M} y \in S \leftrightarrow H \in Mnd)$
8	7	3expb	$⊢ (M \in Mnd \land (S \subseteq B \land \underset{˙}{0} \in S)) \to (\forall x \in S \forall y \in S x +_{M} y \in S \leftrightarrow H \in Mnd)$
9	8	pm5.32da	$⊢ M \in Mnd \to (((S \subseteq B \land \underset{˙}{0} \in S) \land \forall x \in S \forall y \in S x +_{M} y \in S) \leftrightarrow ((S \subseteq B \land \underset{˙}{0} \in S) \land H \in Mnd))$
10		df-3an	$⊢ (S \subseteq B \land \underset{˙}{0} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S) \leftrightarrow ((S \subseteq B \land \underset{˙}{0} \in S) \land \forall x \in S \forall y \in S x +_{M} y \in S)$
11		df-3an	$⊢ (S \subseteq B \land \underset{˙}{0} \in S \land H \in Mnd) \leftrightarrow ((S \subseteq B \land \underset{˙}{0} \in S) \land H \in Mnd)$
12	9 10 11	3bitr4g	$⊢ M \in Mnd \to ((S \subseteq B \land \underset{˙}{0} \in S \land \forall x \in S \forall y \in S x +_{M} y \in S) \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land H \in Mnd))$
13	5 12	bitrd	$⊢ M \in Mnd \to (S \in SubMnd (M) \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land H \in Mnd))$