Metamath Proof Explorer

Theorem iscyg3

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

Ref Expression
Hypotheses iscyg.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
iscyg.2 ⊢ · = ( .g ‘ 𝐺 )
Assertion iscyg3 ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 iscyg.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 iscyg.2 ⊢ · = ( .g ‘ 𝐺 )
3 1 2 iscyg ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ) )
4 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) → ( 𝑛 · 𝑥 ) ∈ 𝐵 )
5 4 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑛 ∈ ℤ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑛 · 𝑥 ) ∈ 𝐵 )
6 5 an32s ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · 𝑥 ) ∈ 𝐵 )
7 6 fmpttd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) : ℤ ⟶ 𝐵 )
8 frn ⊢ ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) : ℤ ⟶ 𝐵 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ⊆ 𝐵 )
9 eqss ⊢ ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ↔ ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ⊆ 𝐵 ∧ 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ) )
10 9 baib ⊢ ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ⊆ 𝐵 → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ↔ 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ) )
11 7 8 10 3syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ↔ 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ) )
12 dfss3 ⊢ ( 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) )
13 eqid ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) )
14 ovex ⊢ ( 𝑛 · 𝑥 ) ∈ V
15 13 14 elrnmpti ⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ↔ ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑥 ) )
16 15 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑥 ) )
17 12 16 bitri ⊢ ( 𝐵 ⊆ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑥 ) )
18 11 17 bitrdi ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ↔ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑥 ) ) )
19 18 rexbidva ⊢ ( 𝐺 ∈ Grp → ( ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ↔ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑥 ) ) )
20 19 pm5.32i ⊢ ( ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 ) ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑥 ) ) )
21 3 20 bitri ⊢ ( 𝐺 ∈ CycGrp ↔ ( 𝐺 ∈ Grp ∧ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑥 ) ) )