Metamath Proof Explorer

Theorem iscyg3

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

Ref Expression
Hypotheses iscyg.1 ⊢B=BaseG
iscyg.2 ⊢·˙=⋅G
Assertion iscyg3 ⊢G∈CycGrp↔G∈Grp∧∃x∈B∀y∈B∃n∈ℤy=n·˙x

Proof

Step Hyp Ref Expression
1 iscyg.1 ⊢B=BaseG
2 iscyg.2 ⊢·˙=⋅G
3 1 2 iscyg ⊢G∈CycGrp↔G∈Grp∧∃x∈Bran⁡n∈ℤ⟼n·˙x=B
4 1 2 mulgcl ⊢G∈Grp∧n∈ℤ∧x∈B→n·˙x∈B
5 4 3expa ⊢G∈Grp∧n∈ℤ∧x∈B→n·˙x∈B
6 5 an32s ⊢G∈Grp∧x∈B∧n∈ℤ→n·˙x∈B
7 6 fmpttd ⊢G∈Grp∧x∈B→n∈ℤ⟼n·˙x:ℤ⟶B
8 frn ⊢n∈ℤ⟼n·˙x:ℤ⟶B→ran⁡n∈ℤ⟼n·˙x⊆B
9 eqss ⊢ran⁡n∈ℤ⟼n·˙x=B↔ran⁡n∈ℤ⟼n·˙x⊆B∧B⊆ran⁡n∈ℤ⟼n·˙x
10 9 baib ⊢ran⁡n∈ℤ⟼n·˙x⊆B→ran⁡n∈ℤ⟼n·˙x=B↔B⊆ran⁡n∈ℤ⟼n·˙x
11 7 8 10 3syl ⊢G∈Grp∧x∈B→ran⁡n∈ℤ⟼n·˙x=B↔B⊆ran⁡n∈ℤ⟼n·˙x
12 dfss3 ⊢B⊆ran⁡n∈ℤ⟼n·˙x↔∀y∈By∈ran⁡n∈ℤ⟼n·˙x
13 eqid ⊢n∈ℤ⟼n·˙x=n∈ℤ⟼n·˙x
14 ovex ⊢n·˙x∈V
15 13 14 elrnmpti ⊢y∈ran⁡n∈ℤ⟼n·˙x↔∃n∈ℤy=n·˙x
16 15 ralbii ⊢∀y∈By∈ran⁡n∈ℤ⟼n·˙x↔∀y∈B∃n∈ℤy=n·˙x
17 12 16 bitri ⊢B⊆ran⁡n∈ℤ⟼n·˙x↔∀y∈B∃n∈ℤy=n·˙x
18 11 17 bitrdi ⊢G∈Grp∧x∈B→ran⁡n∈ℤ⟼n·˙x=B↔∀y∈B∃n∈ℤy=n·˙x
19 18 rexbidva ⊢G∈Grp→∃x∈Bran⁡n∈ℤ⟼n·˙x=B↔∃x∈B∀y∈B∃n∈ℤy=n·˙x
20 19 pm5.32i ⊢G∈Grp∧∃x∈Bran⁡n∈ℤ⟼n·˙x=B↔G∈Grp∧∃x∈B∀y∈B∃n∈ℤy=n·˙x
21 3 20 bitri ⊢G∈CycGrp↔G∈Grp∧∃x∈B∀y∈B∃n∈ℤy=n·˙x