# Metamath Proof Explorer

## Theorem issubm

Description: Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses issubm.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
issubm.z
issubm.p
Assertion issubm

### Proof

Step Hyp Ref Expression
1 issubm.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 issubm.z
3 issubm.p
4 fveq2 ${⊢}{m}={M}\to {\mathrm{Base}}_{{m}}={\mathrm{Base}}_{{M}}$
5 4 pweqd ${⊢}{m}={M}\to 𝒫{\mathrm{Base}}_{{m}}=𝒫{\mathrm{Base}}_{{M}}$
6 fveq2 ${⊢}{m}={M}\to {0}_{{m}}={0}_{{M}}$
7 6 eleq1d ${⊢}{m}={M}\to \left({0}_{{m}}\in {t}↔{0}_{{M}}\in {t}\right)$
8 fveq2 ${⊢}{m}={M}\to {+}_{{m}}={+}_{{M}}$
9 8 oveqd ${⊢}{m}={M}\to {x}{+}_{{m}}{y}={x}{+}_{{M}}{y}$
10 9 eleq1d ${⊢}{m}={M}\to \left({x}{+}_{{m}}{y}\in {t}↔{x}{+}_{{M}}{y}\in {t}\right)$
11 10 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)$
12 7 11 anbi12d ${⊢}{m}={M}\to \left(\left({0}_{{m}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{m}}{y}\in {t}\right)↔\left({0}_{{M}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right)\right)$
13 5 12 rabeqbidv ${⊢}{m}={M}\to \left\{{t}\in 𝒫{\mathrm{Base}}_{{m}}|\left({0}_{{m}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{m}}{y}\in {t}\right)\right\}=\left\{{t}\in 𝒫{\mathrm{Base}}_{{M}}|\left({0}_{{M}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right)\right\}$
14 df-submnd ${⊢}\mathrm{SubMnd}=\left({m}\in \mathrm{Mnd}⟼\left\{{t}\in 𝒫{\mathrm{Base}}_{{m}}|\left({0}_{{m}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{m}}{y}\in {t}\right)\right\}\right)$
15 fvex ${⊢}{\mathrm{Base}}_{{M}}\in \mathrm{V}$
16 15 pwex ${⊢}𝒫{\mathrm{Base}}_{{M}}\in \mathrm{V}$
17 16 rabex ${⊢}\left\{{t}\in 𝒫{\mathrm{Base}}_{{M}}|\left({0}_{{M}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right)\right\}\in \mathrm{V}$
18 13 14 17 fvmpt ${⊢}{M}\in \mathrm{Mnd}\to \mathrm{SubMnd}\left({M}\right)=\left\{{t}\in 𝒫{\mathrm{Base}}_{{M}}|\left({0}_{{M}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right)\right\}$
19 18 eleq2d ${⊢}{M}\in \mathrm{Mnd}\to \left({S}\in \mathrm{SubMnd}\left({M}\right)↔{S}\in \left\{{t}\in 𝒫{\mathrm{Base}}_{{M}}|\left({0}_{{M}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right)\right\}\right)$
20 eleq2 ${⊢}{t}={S}\to \left({0}_{{M}}\in {t}↔{0}_{{M}}\in {S}\right)$
21 eleq2 ${⊢}{t}={S}\to \left({x}{+}_{{M}}{y}\in {t}↔{x}{+}_{{M}}{y}\in {S}\right)$
22 21 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)$
23 22 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)$
24 20 23 anbi12d ${⊢}{t}={S}\to \left(\left({0}_{{M}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right)↔\left({0}_{{M}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {S}\right)\right)$
25 24 elrab ${⊢}{S}\in \left\{{t}\in 𝒫{\mathrm{Base}}_{{M}}|\left({0}_{{M}}\in {t}\wedge \forall {x}\in {t}\phantom{\rule{.4em}{0ex}}\forall {y}\in {t}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {t}\right)\right\}↔\left({S}\in 𝒫{\mathrm{Base}}_{{M}}\wedge \left({0}_{{M}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {S}\right)\right)$
26 1 sseq2i ${⊢}{S}\subseteq {B}↔{S}\subseteq {\mathrm{Base}}_{{M}}$
27 2 eleq1i
28 3 oveqi
29 28 eleq1i
30 29 2ralbii
31 27 30 anbi12i
32 26 31 anbi12i
33 3anass
34 15 elpw2 ${⊢}{S}\in 𝒫{\mathrm{Base}}_{{M}}↔{S}\subseteq {\mathrm{Base}}_{{M}}$
35 34 anbi1i ${⊢}\left({S}\in 𝒫{\mathrm{Base}}_{{M}}\wedge \left({0}_{{M}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {S}\right)\right)↔\left({S}\subseteq {\mathrm{Base}}_{{M}}\wedge \left({0}_{{M}}\in {S}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{+}_{{M}}{y}\in {S}\right)\right)$
36 32 33 35 3bitr4ri
37 25 36 bitri
38 19 37 syl6bb