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 ⊢ 𝐵 = ( 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 )