Database
BASIC ALGEBRAIC STRUCTURES
Groups
Subgroups and Quotient groups
subgsubm
Next ⟩
subsubg
Metamath Proof Explorer
Ascii
Unicode
Theorem
subgsubm
Description:
A subgroup is a submonoid.
(Contributed by
Mario Carneiro
, 18-Jun-2015)
Ref
Expression
Assertion
subgsubm
⊢
S
∈
SubGrp
⁡
G
→
S
∈
SubMnd
⁡
G
Proof
Step
Hyp
Ref
Expression
1
subgrcl
⊢
S
∈
SubGrp
⁡
G
→
G
∈
Grp
2
eqid
⊢
inv
g
⁡
G
=
inv
g
⁡
G
3
2
issubg3
⊢
G
∈
Grp
→
S
∈
SubGrp
⁡
G
↔
S
∈
SubMnd
⁡
G
∧
∀
x
∈
S
inv
g
⁡
G
⁡
x
∈
S
4
1
3
syl
⊢
S
∈
SubGrp
⁡
G
→
S
∈
SubGrp
⁡
G
↔
S
∈
SubMnd
⁡
G
∧
∀
x
∈
S
inv
g
⁡
G
⁡
x
∈
S
5
4
ibi
⊢
S
∈
SubGrp
⁡
G
→
S
∈
SubMnd
⁡
G
∧
∀
x
∈
S
inv
g
⁡
G
⁡
x
∈
S
6
5
simpld
⊢
S
∈
SubGrp
⁡
G
→
S
∈
SubMnd
⁡
G