Metamath Proof Explorer


Theorem iscygd

Description: Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses iscyg.1 𝐵 = ( Base ‘ 𝐺 )
iscyg.2 · = ( .g𝐺 )
iscygd.3 ( 𝜑𝐺 ∈ Grp )
iscygd.4 ( 𝜑𝑋𝐵 )
iscygd.5 ( ( 𝜑𝑦𝐵 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) )
Assertion iscygd ( 𝜑𝐺 ∈ CycGrp )

Proof

Step Hyp Ref Expression
1 iscyg.1 𝐵 = ( Base ‘ 𝐺 )
2 iscyg.2 · = ( .g𝐺 )
3 iscygd.3 ( 𝜑𝐺 ∈ Grp )
4 iscygd.4 ( 𝜑𝑋𝐵 )
5 iscygd.5 ( ( 𝜑𝑦𝐵 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) )
6 5 ralrimiva ( 𝜑 → ∀ 𝑦𝐵𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) )
7 eqid { 𝑥𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } = { 𝑥𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
8 1 2 7 iscyggen2 ( 𝐺 ∈ Grp → ( 𝑋 ∈ { 𝑥𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } ↔ ( 𝑋𝐵 ∧ ∀ 𝑦𝐵𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) ) ) )
9 3 8 syl ( 𝜑 → ( 𝑋 ∈ { 𝑥𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } ↔ ( 𝑋𝐵 ∧ ∀ 𝑦𝐵𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) ) ) )
10 4 6 9 mpbir2and ( 𝜑𝑋 ∈ { 𝑥𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } )
11 10 ne0d ( 𝜑 → { 𝑥𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } ≠ ∅ )
12 1 2 7 iscyg2 ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ { 𝑥𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } ≠ ∅ ) )
13 3 11 12 sylanbrc ( 𝜑𝐺 ∈ CycGrp )