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

Metamath Proof Explorer

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 ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑋 ) ) = 𝐵 ) )