Metamath Proof Explorer

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
Assertion issubmgm

Proof

Step Hyp Ref Expression
1 issubmgm.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 issubmgm.p
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}↔{x}{+}_{{M}}{y}\in {t}\right)$
8 7 2ralbidv ${⊢}{m}={M}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{m}}{y}\in {t}↔\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right)$
9 4 8 rabeqbidv ${⊢}{m}={M}\to \left\{{t}\in 𝒫{\mathrm{Base}}_{{m}}|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{m}}{y}\in {t}\right\}=\left\{{t}\in 𝒫{\mathrm{Base}}_{{M}}|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{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}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{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}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{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}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right\}$
15 14 eleq2d ${⊢}{M}\in \mathrm{Mgm}\to \left({S}\in \mathrm{SubMgm}\left({M}\right)↔{S}\in \left\{{t}\in 𝒫{\mathrm{Base}}_{{M}}|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right\}\right)$
16 11 elpw2 ${⊢}{S}\in 𝒫{\mathrm{Base}}_{{M}}↔{S}\subseteq {\mathrm{Base}}_{{M}}$
17 16 anbi1i ${⊢}\left({S}\in 𝒫{\mathrm{Base}}_{{M}}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {S}\right)↔\left({S}\subseteq {\mathrm{Base}}_{{M}}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {S}\right)$
18 eleq2 ${⊢}{t}={S}\to \left({x}{+}_{{M}}{y}\in {t}↔{x}{+}_{{M}}{y}\in {S}\right)$
19 18 raleqbi1dv ${⊢}{t}={S}\to \left(\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}↔\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {S}\right)$
20 19 raleqbi1dv ${⊢}{t}={S}\to \left(\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {S}\right)$
21 20 elrab ${⊢}{S}\in \left\{{t}\in 𝒫{\mathrm{Base}}_{{M}}|\forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right\}↔\left({S}\in 𝒫{\mathrm{Base}}_{{M}}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {S}\right)$
22 1 sseq2i ${⊢}{S}\subseteq {B}↔{S}\subseteq {\mathrm{Base}}_{{M}}$
23 2 oveqi
24 23 eleq1i
25 24 2ralbii
26 22 25 anbi12i
27 17 21 26 3bitr4i
28 15 27 syl6bb