Metamath Proof Explorer

Theorem iscyggen2

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

Ref Expression
Hypotheses iscyg.1 ⊢B=BaseG
iscyg.2 ⊢·˙=⋅G
iscyg3.e ⊢E=x∈B|ran⁡n∈ℤ⟼n·˙x=B
Assertion iscyggen2 ⊢G∈Grp→X∈E↔X∈B∧∀y∈B∃n∈ℤy=n·˙X

Proof

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