# Metamath Proof Explorer

## Theorem issubmgm2

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

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

### Proof

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