Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Monoids (extension)
Magma homomorphisms and submagmas
submgmcl
Next ⟩
submgmmgm
Metamath Proof Explorer
Ascii
Unicode
Theorem
submgmcl
Description:
Submagmas are closed under the monoid operation.
(Contributed by
AV
, 26-Feb-2020)
Ref
Expression
Hypothesis
submgmcl.p
⊢
+
˙
=
+
M
Assertion
submgmcl
⊢
S
∈
SubMgm
⁡
M
∧
X
∈
S
∧
Y
∈
S
→
X
+
˙
Y
∈
S
Proof
Step
Hyp
Ref
Expression
1
submgmcl.p
⊢
+
˙
=
+
M
2
submgmrcl
⊢
S
∈
SubMgm
⁡
M
→
M
∈
Mgm
3
eqid
⊢
Base
M
=
Base
M
4
3
1
issubmgm
⊢
M
∈
Mgm
→
S
∈
SubMgm
⁡
M
↔
S
⊆
Base
M
∧
∀
x
∈
S
∀
y
∈
S
x
+
˙
y
∈
S
5
2
4
syl
⊢
S
∈
SubMgm
⁡
M
→
S
∈
SubMgm
⁡
M
↔
S
⊆
Base
M
∧
∀
x
∈
S
∀
y
∈
S
x
+
˙
y
∈
S
6
5
ibi
⊢
S
∈
SubMgm
⁡
M
→
S
⊆
Base
M
∧
∀
x
∈
S
∀
y
∈
S
x
+
˙
y
∈
S
7
6
simprd
⊢
S
∈
SubMgm
⁡
M
→
∀
x
∈
S
∀
y
∈
S
x
+
˙
y
∈
S
8
ovrspc2v
⊢
X
∈
S
∧
Y
∈
S
∧
∀
x
∈
S
∀
y
∈
S
x
+
˙
y
∈
S
→
X
+
˙
Y
∈
S
9
7
8
sylan2
⊢
X
∈
S
∧
Y
∈
S
∧
S
∈
SubMgm
⁡
M
→
X
+
˙
Y
∈
S
10
9
ancoms
⊢
S
∈
SubMgm
⁡
M
∧
X
∈
S
∧
Y
∈
S
→
X
+
˙
Y
∈
S
11
10
3impb
⊢
S
∈
SubMgm
⁡
M
∧
X
∈
S
∧
Y
∈
S
→
X
+
˙
Y
∈
S