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 = Base G
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 = Base G
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 ∈ B y ∈ 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 ∈ B y ∈ 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