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 ⊢ B = Base G
iscyg.2 ⊢ · ˙ = ⋅ G
iscyg3.e ⊢ E = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
Assertion iscyg2 ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ E ≠ ∅

Proof

Step Hyp Ref Expression
1 iscyg.1 ⊢ B = Base G
2 iscyg.2 ⊢ · ˙ = ⋅ G
3 iscyg3.e ⊢ E = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
4 1 2 iscyg ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
5 3 neeq1i ⊢ E ≠ ∅ ↔ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B ≠ ∅
6 rabn0 ⊢ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B ≠ ∅ ↔ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
7 5 6 bitri ⊢ E ≠ ∅ ↔ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
8 7 anbi2i ⊢ G ∈ Grp ∧ E ≠ ∅ ↔ G ∈ Grp ∧ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
9 4 8 bitr4i ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ E ≠ ∅