Metamath Proof Explorer

Theorem iscyg

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

Ref Expression
Hypotheses iscyg.1 ⊢ B = Base G
iscyg.2 ⊢ · ˙ = ⋅ G
Assertion iscyg ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B

Proof

Step Hyp Ref Expression
1 iscyg.1 ⊢ B = Base G
2 iscyg.2 ⊢ · ˙ = ⋅ G
3 fveq2 ⊢ g = G → Base g = Base G
4 3 1 eqtr4di ⊢ g = G → Base g = B
5 fveq2 ⊢ g = G → ⋅ g = ⋅ G
6 5 2 eqtr4di ⊢ g = G → ⋅ g = · ˙
7 6 oveqd ⊢ g = G → n ⋅ g x = n · ˙ x
8 7 mpteq2dv ⊢ g = G → n ∈ ℤ ⟼ n ⋅ g x = n ∈ ℤ ⟼ n · ˙ x
9 8 rneqd ⊢ g = G → ran ⁡ n ∈ ℤ ⟼ n ⋅ g x = ran ⁡ n ∈ ℤ ⟼ n · ˙ x
10 9 4 eqeq12d ⊢ g = G → ran ⁡ n ∈ ℤ ⟼ n ⋅ g x = Base g ↔ ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
11 4 10 rexeqbidv ⊢ g = G → ∃ x ∈ Base g ran ⁡ n ∈ ℤ ⟼ n ⋅ g x = Base g ↔ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B
12 df-cyg ⊢ CycGrp = g ∈ Grp | ∃ x ∈ Base g ran ⁡ n ∈ ℤ ⟼ n ⋅ g x = Base g
13 11 12 elrab2 ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ ∃ x ∈ B ran ⁡ n ∈ ℤ ⟼ n · ˙ x = B