Theorem issubmgm

Description: Expand definition of a submagma. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypotheses	issubmgm.b	$$⊢B={\mathrm{Base}}_M$$
	issubmgm.p	$$⊢\underset{\dot{}}{+}={+}_M$$
Assertion	issubmgm	$$⊢M\in \mathrm{Mgm}\to \left(S\in \mathrm{SubMgm}\left(M\right)\leftrightarrow \left(S\subseteq B\wedge \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		issubmgm.b	$$⊢B={\mathrm{Base}}_M$$
2		issubmgm.p	$$⊢\underset{\dot{}}{+}={+}_M$$
3		fveq2	$$⊢m=M\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
4	3	pweqd	$$⊢m=M\to 𝒫{\mathrm{Base}}_m=𝒫{\mathrm{Base}}_M$$
5		fveq2	$$⊢m=M\to {+}_m={+}_M$$
6	5	oveqd	$$⊢m=M\to x{+}_{m}y=x{+}_{M}y$$
7	6	eleq1d	$$⊢m=M\to \left(x{+}_{m}y\in t\leftrightarrow x{+}_{M}y\in t\right)$$
8	7	2ralbidv	$$⊢m=M\to \left(\forall x\in t\forall y\in tx{+}_{m}y\in t\leftrightarrow \forall x\in t\forall y\in tx{+}_{M}y\in t\right)$$
9	4 8	rabeqbidv	$$⊢m=M\to \left\{t\in 𝒫{\mathrm{Base}}_m|\forall x\in t\forall y\in tx{+}_{m}y\in t\right\}=\left\{t\in 𝒫{\mathrm{Base}}_M|\forall x\in t\forall y\in tx{+}_{M}y\in t\right\}$$
10		df-submgm	$$⊢\mathrm{SubMgm}=\left(m\in \mathrm{Mgm}⟼\left\{t\in 𝒫{\mathrm{Base}}_m|\forall x\in t\forall y\in tx{+}_{m}y\in t\right\}\right)$$
11		fvex	$$⊢{\mathrm{Base}}_M\in \mathrm{V}$$
12	11	pwex	$$⊢𝒫{\mathrm{Base}}_M\in \mathrm{V}$$
13	12	rabex	$$⊢\left\{t\in 𝒫{\mathrm{Base}}_M|\forall x\in t\forall y\in tx{+}_{M}y\in t\right\}\in \mathrm{V}$$
14	9 10 13	fvmpt	$$⊢M\in \mathrm{Mgm}\to \mathrm{SubMgm}\left(M\right)=\left\{t\in 𝒫{\mathrm{Base}}_M|\forall x\in t\forall y\in tx{+}_{M}y\in t\right\}$$
15	14	eleq2d	$$⊢M\in \mathrm{Mgm}\to \left(S\in \mathrm{SubMgm}\left(M\right)\leftrightarrow S\in \left\{t\in 𝒫{\mathrm{Base}}_M|\forall x\in t\forall y\in tx{+}_{M}y\in t\right\}\right)$$
16	11	elpw2	$$⊢S\in 𝒫{\mathrm{Base}}_M\leftrightarrow S\subseteq {\mathrm{Base}}_M$$
17	16	anbi1i	$$⊢\left(S\in 𝒫{\mathrm{Base}}_M\wedge \forall x\in S\forall y\in Sx{+}_{M}y\in S\right)\leftrightarrow \left(S\subseteq {\mathrm{Base}}_M\wedge \forall x\in S\forall y\in Sx{+}_{M}y\in S\right)$$
18		eleq2	$$⊢t=S\to \left(x{+}_{M}y\in t\leftrightarrow x{+}_{M}y\in S\right)$$
19	18	raleqbi1dv	$$⊢t=S\to \left(\forall y\in tx{+}_{M}y\in t\leftrightarrow \forall y\in Sx{+}_{M}y\in S\right)$$
20	19	raleqbi1dv	$$⊢t=S\to \left(\forall x\in t\forall y\in tx{+}_{M}y\in t\leftrightarrow \forall x\in S\forall y\in Sx{+}_{M}y\in S\right)$$
21	20	elrab	$$⊢S\in \left\{t\in 𝒫{\mathrm{Base}}_M|\forall x\in t\forall y\in tx{+}_{M}y\in t\right\}\leftrightarrow \left(S\in 𝒫{\mathrm{Base}}_M\wedge \forall x\in S\forall y\in Sx{+}_{M}y\in S\right)$$
22	1	sseq2i	$$⊢S\subseteq B\leftrightarrow S\subseteq {\mathrm{Base}}_M$$
23	2	oveqi	$$⊢x\underset{\dot{}}{+}y=x{+}_{M}y$$
24	23	eleq1i	$$⊢x\underset{\dot{}}{+}y\in S\leftrightarrow x{+}_{M}y\in S$$
25	24	2ralbii	$$⊢\forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\leftrightarrow \forall x\in S\forall y\in Sx{+}_{M}y\in S$$
26	22 25	anbi12i	$$⊢\left(S\subseteq B\wedge \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\right)\leftrightarrow \left(S\subseteq {\mathrm{Base}}_M\wedge \forall x\in S\forall y\in Sx{+}_{M}y\in S\right)$$
27	17 21 26	3bitr4i	$$⊢S\in \left\{t\in 𝒫{\mathrm{Base}}_M|\forall x\in t\forall y\in tx{+}_{M}y\in t\right\}\leftrightarrow \left(S\subseteq B\wedge \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\right)$$
28	15 27	syl6bb	$$⊢M\in \mathrm{Mgm}\to \left(S\in \mathrm{SubMgm}\left(M\right)\leftrightarrow \left(S\subseteq B\wedge \forall x\in S\forall y\in Sx\underset{\dot{}}{+}y\in S\right)\right)$$