Database
BASIC ALGEBRAIC STRUCTURES
Groups
Abelian groups
Cyclic groups
iscygd
Next ⟩
iscygodd
Metamath Proof Explorer
Ascii
Unicode
Theorem
iscygd
Description:
Definition of a cyclic group.
(Contributed by
Mario Carneiro
, 21-Apr-2016)
Ref
Expression
Hypotheses
iscyg.1
⊢
B
=
Base
G
iscyg.2
⊢
·
˙
=
⋅
G
iscygd.3
⊢
φ
→
G
∈
Grp
iscygd.4
⊢
φ
→
X
∈
B
iscygd.5
⊢
φ
∧
y
∈
B
→
∃
n
∈
ℤ
y
=
n
·
˙
X
Assertion
iscygd
⊢
φ
→
G
∈
CycGrp
Proof
Step
Hyp
Ref
Expression
1
iscyg.1
⊢
B
=
Base
G
2
iscyg.2
⊢
·
˙
=
⋅
G
3
iscygd.3
⊢
φ
→
G
∈
Grp
4
iscygd.4
⊢
φ
→
X
∈
B
5
iscygd.5
⊢
φ
∧
y
∈
B
→
∃
n
∈
ℤ
y
=
n
·
˙
X
6
5
ralrimiva
⊢
φ
→
∀
y
∈
B
∃
n
∈
ℤ
y
=
n
·
˙
X
7
eqid
⊢
x
∈
B
|
ran
⁡
n
∈
ℤ
⟼
n
·
˙
x
=
B
=
x
∈
B
|
ran
⁡
n
∈
ℤ
⟼
n
·
˙
x
=
B
8
1
2
7
iscyggen2
⊢
G
∈
Grp
→
X
∈
x
∈
B
|
ran
⁡
n
∈
ℤ
⟼
n
·
˙
x
=
B
↔
X
∈
B
∧
∀
y
∈
B
∃
n
∈
ℤ
y
=
n
·
˙
X
9
3
8
syl
⊢
φ
→
X
∈
x
∈
B
|
ran
⁡
n
∈
ℤ
⟼
n
·
˙
x
=
B
↔
X
∈
B
∧
∀
y
∈
B
∃
n
∈
ℤ
y
=
n
·
˙
X
10
4
6
9
mpbir2and
⊢
φ
→
X
∈
x
∈
B
|
ran
⁡
n
∈
ℤ
⟼
n
·
˙
x
=
B
11
10
ne0d
⊢
φ
→
x
∈
B
|
ran
⁡
n
∈
ℤ
⟼
n
·
˙
x
=
B
≠
∅
12
1
2
7
iscyg2
⊢
G
∈
CycGrp
↔
G
∈
Grp
∧
x
∈
B
|
ran
⁡
n
∈
ℤ
⟼
n
·
˙
x
=
B
≠
∅
13
3
11
12
sylanbrc
⊢
φ
→
G
∈
CycGrp