Metamath Proof Explorer

Theorem issubmndb

Description: The submonoid predicate. Analogous to issubg . (Contributed by AV, 1-Feb-2024)

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

Proof

Step	Hyp	Ref	Expression
1		issubmndb.b	$⊢ B = {Base}_{G}$
2		issubmndb.z	$⊢ \underset{˙}{0} = 0_{G}$
3		eqid	$⊢ G ↾_{𝑠} S = G ↾_{𝑠} S$
4	1 2 3	issubm2	$⊢ G \in Mnd \to (S \in SubMnd (G) \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land G ↾_{𝑠} S \in Mnd))$
5		3anrot	$⊢ (G ↾_{𝑠} S \in Mnd \land S \subseteq B \land \underset{˙}{0} \in S) \leftrightarrow (S \subseteq B \land \underset{˙}{0} \in S \land G ↾_{𝑠} S \in Mnd)$
6		3anass	$⊢ (G ↾_{𝑠} S \in Mnd \land S \subseteq B \land \underset{˙}{0} \in S) \leftrightarrow (G ↾_{𝑠} S \in Mnd \land (S \subseteq B \land \underset{˙}{0} \in S))$
7	5 6	bitr3i	$⊢ (S \subseteq B \land \underset{˙}{0} \in S \land G ↾_{𝑠} S \in Mnd) \leftrightarrow (G ↾_{𝑠} S \in Mnd \land (S \subseteq B \land \underset{˙}{0} \in S))$
8	4 7	bitrdi	$⊢ G \in Mnd \to (S \in SubMnd (G) \leftrightarrow (G ↾_{𝑠} S \in Mnd \land (S \subseteq B \land \underset{˙}{0} \in S)))$
9	8	pm5.32i	$⊢ (G \in Mnd \land S \in SubMnd (G)) \leftrightarrow (G \in Mnd \land (G ↾_{𝑠} S \in Mnd \land (S \subseteq B \land \underset{˙}{0} \in S)))$
10		submrcl	$⊢ S \in SubMnd (G) \to G \in Mnd$
11	10	pm4.71ri	$⊢ S \in SubMnd (G) \leftrightarrow (G \in Mnd \land S \in SubMnd (G))$
12		anass	$⊢ ((G \in Mnd \land G ↾_{𝑠} S \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \leftrightarrow (G \in Mnd \land (G ↾_{𝑠} S \in Mnd \land (S \subseteq B \land \underset{˙}{0} \in S)))$
13	9 11 12	3bitr4i	$⊢ S \in SubMnd (G) \leftrightarrow ((G \in Mnd \land G ↾_{𝑠} S \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S))$