mgmsscl

Description: If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. Formerly part of proof of grpissubg . (Contributed by AV, 17-Feb-2024)

	Ref	Expression
Hypotheses	mgmsscl.b	$⊢ B = {Base}_{G}$
	mgmsscl.s	$⊢ S = {Base}_{H}$
Assertion	mgmsscl	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (X \in S \land Y \in S)) \to X +_{G} Y \in S$

Proof

Step	Hyp	Ref	Expression
1		mgmsscl.b	$⊢ B = {Base}_{G}$
2		mgmsscl.s	$⊢ S = {Base}_{H}$
3		ovres	$⊢ (X \in S \land Y \in S) \to X ({+_{G} ↾}_{(S \times S)}) Y = X +_{G} Y$
4	3	3ad2ant3	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (X \in S \land Y \in S)) \to X ({+_{G} ↾}_{(S \times S)}) Y = X +_{G} Y$
5		simp1r	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (X \in S \land Y \in S)) \to H \in Mgm$
6		simp3	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (X \in S \land Y \in S)) \to (X \in S \land Y \in S)$
7		3anass	$⊢ (H \in Mgm \land X \in S \land Y \in S) \leftrightarrow (H \in Mgm \land (X \in S \land Y \in S))$
8	5 6 7	sylanbrc	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (X \in S \land Y \in S)) \to (H \in Mgm \land X \in S \land Y \in S)$
9		eqid	$⊢ +_{H} = +_{H}$
10	2 9	mgmcl	$⊢ (H \in Mgm \land X \in S \land Y \in S) \to X +_{H} Y \in S$
11	8 10	syl	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (X \in S \land Y \in S)) \to X +_{H} Y \in S$
12		oveq	$⊢ {+_{G} ↾}_{(S \times S)} = +_{H} \to X ({+_{G} ↾}_{(S \times S)}) Y = X +_{H} Y$
13	12	eleq1d	$⊢ {+_{G} ↾}_{(S \times S)} = +_{H} \to (X ({+_{G} ↾}_{(S \times S)}) Y \in S \leftrightarrow X +_{H} Y \in S)$
14	13	eqcoms	$⊢ +_{H} = {+_{G} ↾}_{(S \times S)} \to (X ({+_{G} ↾}_{(S \times S)}) Y \in S \leftrightarrow X +_{H} Y \in S)$
15	14	adantl	$⊢ (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \to (X ({+_{G} ↾}_{(S \times S)}) Y \in S \leftrightarrow X +_{H} Y \in S)$
16	15	3ad2ant2	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (X \in S \land Y \in S)) \to (X ({+_{G} ↾}_{(S \times S)}) Y \in S \leftrightarrow X +_{H} Y \in S)$
17	11 16	mpbird	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (X \in S \land Y \in S)) \to X ({+_{G} ↾}_{(S \times S)}) Y \in S$
18	4 17	eqeltrrd	$⊢ ((G \in Mgm \land H \in Mgm) \land (S \subseteq B \land +_{H} = {+_{G} ↾}_{(S \times S)}) \land (X \in S \land Y \in S)) \to X +_{G} Y \in S$

Metamath Proof Explorer

Theorem mgmsscl

Proof