Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Monoids (extension)
Magma homomorphisms and submagmas
submgmbas
Next ⟩
subsubmgm
Metamath Proof Explorer
Ascii
Unicode
Theorem
submgmbas
Description:
The base set of a submagma.
(Contributed by
AV
, 26-Feb-2020)
Ref
Expression
Hypothesis
submgmmgm.h
⊢
H
=
M
↾
𝑠
S
Assertion
submgmbas
⊢
S
∈
SubMgm
⁡
M
→
S
=
Base
H
Proof
Step
Hyp
Ref
Expression
1
submgmmgm.h
⊢
H
=
M
↾
𝑠
S
2
eqid
⊢
Base
M
=
Base
M
3
2
submgmss
⊢
S
∈
SubMgm
⁡
M
→
S
⊆
Base
M
4
1
2
ressbas2
⊢
S
⊆
Base
M
→
S
=
Base
H
5
3
4
syl
⊢
S
∈
SubMgm
⁡
M
→
S
=
Base
H