Metamath Proof Explorer

Theorem iscygd

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

Ref Expression
Hypotheses iscyg.1 ⊢B=BaseG
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=BaseG
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