issubmgm2

Description: Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypotheses	issubmgm2.b	$⊢ B = {Base}_{M}$
	issubmgm2.h	$⊢ H = M ↾_{𝑠} S$
Assertion	issubmgm2	$⊢ M \in Mgm \to (S \in SubMgm (M) \leftrightarrow (S \subseteq B \land H \in Mgm))$

Proof

Step	Hyp	Ref	Expression
1		issubmgm2.b	$⊢ B = {Base}_{M}$
2		issubmgm2.h	$⊢ H = M ↾_{𝑠} S$
3		eqid	$⊢ +_{M} = +_{M}$
4	1 3	issubmgm	$⊢ M \in Mgm \to (S \in SubMgm (M) \leftrightarrow (S \subseteq B \land \forall x \in S \forall y \in S x +_{M} y \in S))$
5	2 1	ressbas2	$⊢ S \subseteq B \to S = {Base}_{H}$
6	5	ad2antlr	$⊢ ((M \in Mgm \land S \subseteq B) \land \forall x \in S \forall y \in S x +_{M} y \in S) \to S = {Base}_{H}$
7		ovex	$⊢ M ↾_{𝑠} S \in V$
8	2 7	eqeltri	$⊢ H \in V$
9	8	a1i	$⊢ ((M \in Mgm \land S \subseteq B) \land \forall x \in S \forall y \in S x +_{M} y \in S) \to H \in V$
10	1	fvexi	$⊢ B \in V$
11	10	ssex	$⊢ S \subseteq B \to S \in V$
12	11	ad2antlr	$⊢ ((M \in Mgm \land S \subseteq B) \land \forall x \in S \forall y \in S x +_{M} y \in S) \to S \in V$
13	2 3	ressplusg	$⊢ S \in V \to +_{M} = +_{H}$
14	12 13	syl	$⊢ ((M \in Mgm \land S \subseteq B) \land \forall x \in S \forall y \in S x +_{M} y \in S) \to +_{M} = +_{H}$
15		oveq1	$⊢ x = a \to x +_{M} y = a +_{M} y$
16	15	eleq1d	$⊢ x = a \to (x +_{M} y \in S \leftrightarrow a +_{M} y \in S)$
17		oveq2	$⊢ y = b \to a +_{M} y = a +_{M} b$
18	17	eleq1d	$⊢ y = b \to (a +_{M} y \in S \leftrightarrow a +_{M} b \in S)$
19	16 18	rspc2v	$⊢ (a \in S \land b \in S) \to (\forall x \in S \forall y \in S x +_{M} y \in S \to a +_{M} b \in S)$
20	19	com12	$⊢ \forall x \in S \forall y \in S x +_{M} y \in S \to ((a \in S \land b \in S) \to a +_{M} b \in S)$
21	20	adantl	$⊢ ((M \in Mgm \land S \subseteq B) \land \forall x \in S \forall y \in S x +_{M} y \in S) \to ((a \in S \land b \in S) \to a +_{M} b \in S)$
22	21	3impib	$⊢ (((M \in Mgm \land S \subseteq B) \land \forall x \in S \forall y \in S x +_{M} y \in S) \land a \in S \land b \in S) \to a +_{M} b \in S$
23	6 9 14 22	ismgmd	$⊢ ((M \in Mgm \land S \subseteq B) \land \forall x \in S \forall y \in S x +_{M} y \in S) \to H \in Mgm$
24		simplr	$⊢ (((M \in Mgm \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to H \in Mgm$
25		simprl	$⊢ (((M \in Mgm \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to x \in S$
26	5	ad3antlr	$⊢ (((M \in Mgm \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to S = {Base}_{H}$
27	25 26	eleqtrd	$⊢ (((M \in Mgm \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to x \in {Base}_{H}$
28		simpr	$⊢ (x \in S \land y \in S) \to y \in S$
29	28	adantl	$⊢ (((M \in Mgm \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to y \in S$
30	29 26	eleqtrd	$⊢ (((M \in Mgm \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to y \in {Base}_{H}$
31		eqid	$⊢ {Base}_{H} = {Base}_{H}$
32		eqid	$⊢ +_{H} = +_{H}$
33	31 32	mgmcl	$⊢ (H \in Mgm \land x \in {Base}_{H} \land y \in {Base}_{H}) \to x +_{H} y \in {Base}_{H}$
34	24 27 30 33	syl3anc	$⊢ (((M \in Mgm \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to x +_{H} y \in {Base}_{H}$
35	11	ad2antlr	$⊢ ((M \in Mgm \land S \subseteq B) \land H \in Mgm) \to S \in V$
36	35 13	syl	$⊢ ((M \in Mgm \land S \subseteq B) \land H \in Mgm) \to +_{M} = +_{H}$
37	36	oveqdr	$⊢ (((M \in Mgm \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to x +_{M} y = x +_{H} y$
38	34 37 26	3eltr4d	$⊢ (((M \in Mgm \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to x +_{M} y \in S$
39	38	ralrimivva	$⊢ ((M \in Mgm \land S \subseteq B) \land H \in Mgm) \to \forall x \in S \forall y \in S x +_{M} y \in S$
40	23 39	impbida	$⊢ (M \in Mgm \land S \subseteq B) \to (\forall x \in S \forall y \in S x +_{M} y \in S \leftrightarrow H \in Mgm)$
41	40	pm5.32da	$⊢ M \in Mgm \to ((S \subseteq B \land \forall x \in S \forall y \in S x +_{M} y \in S) \leftrightarrow (S \subseteq B \land H \in Mgm))$
42	4 41	bitrd	$⊢ M \in Mgm \to (S \in SubMgm (M) \leftrightarrow (S \subseteq B \land H \in Mgm))$

Metamath Proof Explorer

Theorem issubmgm2

Proof