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 )