This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscyg2

Description: A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses iscyg.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
iscyg.2 ⊢ · = ( .g ‘ 𝐺 )
iscyg3.e ⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
Assertion iscyg2 ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐸 ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 iscyg.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 iscyg.2 ⊢ · = ( .g ‘ 𝐺 )
3 iscyg3.e ⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
4 1 2 iscyg ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ) )
5 3 neeq1i ⊢ ( 𝐸 ≠ ∅ ↔ { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } ≠ ∅ )
6 rabn0 ⊢ ( { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 )
7 5 6 bitri ⊢ ( 𝐸 ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 )
8 7 anbi2i ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ≠ ∅ ) ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ) )
9 4 8 bitr4i ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ 𝐸 ≠ ∅ ) )