issstrmgm

Description: Characterize a substructure as submagma by closure properties. (Contributed by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	issstrmgm.b	$⊢ B = {Base}_{G}$
	issstrmgm.p	$⊢ \underset{˙}{+} = +_{G}$
	issstrmgm.h	$⊢ H = G ↾_{𝑠} S$
Assertion	issstrmgm	$⊢ (H \in V \land S \subseteq B) \to (H \in Mgm \leftrightarrow \forall x \in S \forall y \in S x \underset{˙}{+} y \in S)$

Proof

Step	Hyp	Ref	Expression
1		issstrmgm.b	$⊢ B = {Base}_{G}$
2		issstrmgm.p	$⊢ \underset{˙}{+} = +_{G}$
3		issstrmgm.h	$⊢ H = G ↾_{𝑠} S$
4		simplr	$⊢ (((H \in V \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to H \in Mgm$
5		simplr	$⊢ ((H \in V \land S \subseteq B) \land H \in Mgm) \to S \subseteq B$
6	3 1	ressbas2	$⊢ S \subseteq B \to S = {Base}_{H}$
7	5 6	syl	$⊢ ((H \in V \land S \subseteq B) \land H \in Mgm) \to S = {Base}_{H}$
8	7	eleq2d	$⊢ ((H \in V \land S \subseteq B) \land H \in Mgm) \to (x \in S \leftrightarrow x \in {Base}_{H})$
9	8	biimpcd	$⊢ x \in S \to (((H \in V \land S \subseteq B) \land H \in Mgm) \to x \in {Base}_{H})$
10	9	adantr	$⊢ (x \in S \land y \in S) \to (((H \in V \land S \subseteq B) \land H \in Mgm) \to x \in {Base}_{H})$
11	10	impcom	$⊢ (((H \in V \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to x \in {Base}_{H}$
12	7	eleq2d	$⊢ ((H \in V \land S \subseteq B) \land H \in Mgm) \to (y \in S \leftrightarrow y \in {Base}_{H})$
13	12	biimpcd	$⊢ y \in S \to (((H \in V \land S \subseteq B) \land H \in Mgm) \to y \in {Base}_{H})$
14	13	adantl	$⊢ (x \in S \land y \in S) \to (((H \in V \land S \subseteq B) \land H \in Mgm) \to y \in {Base}_{H})$
15	14	impcom	$⊢ (((H \in V \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to y \in {Base}_{H}$
16		eqid	$⊢ {Base}_{H} = {Base}_{H}$
17		eqid	$⊢ +_{H} = +_{H}$
18	16 17	mgmcl	$⊢ (H \in Mgm \land x \in {Base}_{H} \land y \in {Base}_{H}) \to x +_{H} y \in {Base}_{H}$
19	4 11 15 18	syl3anc	$⊢ (((H \in V \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to x +_{H} y \in {Base}_{H}$
20	1	fvexi	$⊢ B \in V$
21	20	ssex	$⊢ S \subseteq B \to S \in V$
22	21	adantl	$⊢ (H \in V \land S \subseteq B) \to S \in V$
23	3 2	ressplusg	$⊢ S \in V \to \underset{˙}{+} = +_{H}$
24	22 23	syl	$⊢ (H \in V \land S \subseteq B) \to \underset{˙}{+} = +_{H}$
25	24	adantr	$⊢ ((H \in V \land S \subseteq B) \land H \in Mgm) \to \underset{˙}{+} = +_{H}$
26	25	oveqdr	$⊢ (((H \in V \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y = x +_{H} y$
27	7	adantr	$⊢ (((H \in V \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to S = {Base}_{H}$
28	19 26 27	3eltr4d	$⊢ (((H \in V \land S \subseteq B) \land H \in Mgm) \land (x \in S \land y \in S)) \to x \underset{˙}{+} y \in S$
29	28	ralrimivva	$⊢ ((H \in V \land S \subseteq B) \land H \in Mgm) \to \forall x \in S \forall y \in S x \underset{˙}{+} y \in S$
30	6	adantl	$⊢ (H \in V \land S \subseteq B) \to S = {Base}_{H}$
31	24	oveqd	$⊢ (H \in V \land S \subseteq B) \to x \underset{˙}{+} y = x +_{H} y$
32	31 30	eleq12d	$⊢ (H \in V \land S \subseteq B) \to (x \underset{˙}{+} y \in S \leftrightarrow x +_{H} y \in {Base}_{H})$
33	30 32	raleqbidv	$⊢ (H \in V \land S \subseteq B) \to (\forall y \in S x \underset{˙}{+} y \in S \leftrightarrow \forall y \in {Base}_{H} x +_{H} y \in {Base}_{H})$
34	30 33	raleqbidv	$⊢ (H \in V \land S \subseteq B) \to (\forall x \in S \forall y \in S x \underset{˙}{+} y \in S \leftrightarrow \forall x \in {Base}_{H} \forall y \in {Base}_{H} x +_{H} y \in {Base}_{H})$
35	34	biimpa	$⊢ ((H \in V \land S \subseteq B) \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S) \to \forall x \in {Base}_{H} \forall y \in {Base}_{H} x +_{H} y \in {Base}_{H}$
36	16 17	ismgm	$⊢ H \in V \to (H \in Mgm \leftrightarrow \forall x \in {Base}_{H} \forall y \in {Base}_{H} x +_{H} y \in {Base}_{H})$
37	36	ad2antrr	$⊢ ((H \in V \land S \subseteq B) \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S) \to (H \in Mgm \leftrightarrow \forall x \in {Base}_{H} \forall y \in {Base}_{H} x +_{H} y \in {Base}_{H})$
38	35 37	mpbird	$⊢ ((H \in V \land S \subseteq B) \land \forall x \in S \forall y \in S x \underset{˙}{+} y \in S) \to H \in Mgm$
39	29 38	impbida	$⊢ (H \in V \land S \subseteq B) \to (H \in Mgm \leftrightarrow \forall x \in S \forall y \in S x \underset{˙}{+} y \in S)$

Metamath Proof Explorer

Theorem issstrmgm

Proof