Database
BASIC ALGEBRAIC STRUCTURES
Groups
Subgroups and Quotient groups
issubgrpd
Next ⟩
issubg3
Metamath Proof Explorer
Ascii
Unicode
Theorem
issubgrpd
Description:
Prove a subgroup by closure.
(Contributed by
Stefan O'Rear
, 7-Dec-2014)
Ref
Expression
Hypotheses
issubgrpd.s
⊢
φ
→
S
=
I
↾
𝑠
D
issubgrpd.z
⊢
φ
→
0
˙
=
0
I
issubgrpd.p
⊢
φ
→
+
˙
=
+
I
issubgrpd.ss
⊢
φ
→
D
⊆
Base
I
issubgrpd.zcl
⊢
φ
→
0
˙
∈
D
issubgrpd.acl
⊢
φ
∧
x
∈
D
∧
y
∈
D
→
x
+
˙
y
∈
D
issubgrpd.ncl
⊢
φ
∧
x
∈
D
→
inv
g
⁡
I
⁡
x
∈
D
issubgrpd.g
⊢
φ
→
I
∈
Grp
Assertion
issubgrpd
⊢
φ
→
S
∈
Grp
Proof
Step
Hyp
Ref
Expression
1
issubgrpd.s
⊢
φ
→
S
=
I
↾
𝑠
D
2
issubgrpd.z
⊢
φ
→
0
˙
=
0
I
3
issubgrpd.p
⊢
φ
→
+
˙
=
+
I
4
issubgrpd.ss
⊢
φ
→
D
⊆
Base
I
5
issubgrpd.zcl
⊢
φ
→
0
˙
∈
D
6
issubgrpd.acl
⊢
φ
∧
x
∈
D
∧
y
∈
D
→
x
+
˙
y
∈
D
7
issubgrpd.ncl
⊢
φ
∧
x
∈
D
→
inv
g
⁡
I
⁡
x
∈
D
8
issubgrpd.g
⊢
φ
→
I
∈
Grp
9
1
2
3
4
5
6
7
8
issubgrpd2
⊢
φ
→
D
∈
SubGrp
⁡
I
10
eqid
⊢
I
↾
𝑠
D
=
I
↾
𝑠
D
11
10
subggrp
⊢
D
∈
SubGrp
⁡
I
→
I
↾
𝑠
D
∈
Grp
12
9
11
syl
⊢
φ
→
I
↾
𝑠
D
∈
Grp
13
1
12
eqeltrd
⊢
φ
→
S
∈
Grp