resmndismnd

Description: If the base set of a monoid is contained in the base set of another monoid, and the group operation of the monoid is the restriction of the group operation of the other monoid to its base set, and the identity element of the the other monoid is contained in the base set of the monoid, then the other monoid restricted to the base set of the monoid is a monoid. Analogous to resgrpisgrp . (Contributed by AV, 17-Feb-2024)

	Ref	Expression
Hypotheses	mndissubm.b	$⊢ B = {Base}_{G}$
	mndissubm.s	$⊢ S = {Base}_{H}$
	mndissubm.z	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	resmndismnd	$⊢ (G \in Mnd \land H \in Mnd) \to ((S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to G ↾_{𝑠} S \in Mnd)$

Proof

Step	Hyp	Ref	Expression
1		mndissubm.b	$⊢ B = {Base}_{G}$
2		mndissubm.s	$⊢ S = {Base}_{H}$
3		mndissubm.z	$⊢ \underset{˙}{0} = 0_{G}$
4	1 2 3	mndissubm	$⊢ (G \in Mnd \land H \in Mnd) \to ((S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to S \in SubMnd (G))$
5	4	imp	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to S \in SubMnd (G)$
6		simpl	$⊢ (G \in Mnd \land H \in Mnd) \to G \in Mnd$
7		3simpa	$⊢ (S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to (S \subseteq B \land \underset{˙}{0} \in S)$
8	6 7	anim12i	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to (G \in Mnd \land (S \subseteq B \land \underset{˙}{0} \in S))$
9	8	biantrud	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to (G ↾_{𝑠} S \in Mnd \leftrightarrow (G ↾_{𝑠} S \in Mnd \land (G \in Mnd \land (S \subseteq B \land \underset{˙}{0} \in S))))$
10		an21	$⊢ ((G \in Mnd \land G ↾_{𝑠} S \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)) \leftrightarrow (G ↾_{𝑠} S \in Mnd \land (G \in Mnd \land (S \subseteq B \land \underset{˙}{0} \in S)))$
11	9 10	syl6bbr	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to (G ↾_{𝑠} S \in Mnd \leftrightarrow ((G \in Mnd \land G ↾_{𝑠} S \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S)))$
12	1 3	issubmndb	$⊢ S \in SubMnd (G) \leftrightarrow ((G \in Mnd \land G ↾_{𝑠} S \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S))$
13	11 12	syl6bbr	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to (G ↾_{𝑠} S \in Mnd \leftrightarrow S \in SubMnd (G))$
14	5 13	mpbird	$⊢ ((G \in Mnd \land H \in Mnd) \land (S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)})) \to G ↾_{𝑠} S \in Mnd$
15	14	ex	$⊢ (G \in Mnd \land H \in Mnd) \to ((S \subseteq B \land \underset{˙}{0} \in S \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to G ↾_{𝑠} S \in Mnd)$

Metamath Proof Explorer

Theorem resmndismnd

Proof