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

Metamath Proof Explorer

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