Theorem iscyggen

Description: The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	iscyg.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	iscyg.2	⊢ · = ( .g ‘ 𝐺 )
	iscyg3.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
Assertion	iscyggen	⊢ ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		iscyg.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		iscyg.2	⊢ · = ( .g ‘ 𝐺 )
3		iscyg3.e	⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
4		simpl	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑛 ∈ ℤ ) → 𝑥 = 𝑋 )
5	4	oveq2d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · 𝑥 ) = ( 𝑛 · 𝑋 ) )
6	5	mpteq2dva	⊢ ( 𝑥 = 𝑋 → ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) )
7	6	rneqd	⊢ ( 𝑥 = 𝑋 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) )
8	7	eqeq1d	⊢ ( 𝑥 = 𝑋 → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ↔ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )
9	8 3	elrab2	⊢ ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )