Metamath Proof Explorer

Theorem cyggeninv

Description: The inverse of a cyclic generator is a generator. (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
cyggeninv.n ⊢ N = inv g ⁡ G
Assertion cyggeninv ⊢ G ∈ Grp ∧ X ∈ E → N ⁡ X ∈ E

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 cyggeninv.n ⊢ N = inv g ⁡ G
5 1 2 3 iscyggen2 ⊢ G ∈ Grp → X ∈ E ↔ X ∈ B ∧ ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ X
6 5 simprbda ⊢ G ∈ Grp ∧ X ∈ E → X ∈ B
7 1 4 grpinvcl ⊢ G ∈ Grp ∧ X ∈ B → N ⁡ X ∈ B
8 6 7 syldan ⊢ G ∈ Grp ∧ X ∈ E → N ⁡ X ∈ B
9 5 simplbda ⊢ G ∈ Grp ∧ X ∈ E → ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ X
10 oveq1 ⊢ n = m → n · ˙ X = m · ˙ X
11 10 eqeq2d ⊢ n = m → y = n · ˙ X ↔ y = m · ˙ X
12 11 cbvrexvw ⊢ ∃ n ∈ ℤ y = n · ˙ X ↔ ∃ m ∈ ℤ y = m · ˙ X
13 znegcl ⊢ m ∈ ℤ → − m ∈ ℤ
14 13 adantl ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → − m ∈ ℤ
15 simpr ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → m ∈ ℤ
16 15 zcnd ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → m ∈ ℂ
17 16 negnegd ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → − − m = m
18 17 oveq1d ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → − − m · ˙ X = m · ˙ X
19 simplll ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → G ∈ Grp
20 6 ad2antrr ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → X ∈ B
21 1 2 4 mulgneg2 ⊢ G ∈ Grp ∧ − m ∈ ℤ ∧ X ∈ B → − − m · ˙ X = − m · ˙ N ⁡ X
22 19 14 20 21 syl3anc ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → − − m · ˙ X = − m · ˙ N ⁡ X
23 18 22 eqtr3d ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → m · ˙ X = − m · ˙ N ⁡ X
24 oveq1 ⊢ n = − m → n · ˙ N ⁡ X = − m · ˙ N ⁡ X
25 24 rspceeqv ⊢ − m ∈ ℤ ∧ m · ˙ X = − m · ˙ N ⁡ X → ∃ n ∈ ℤ m · ˙ X = n · ˙ N ⁡ X
26 14 23 25 syl2anc ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → ∃ n ∈ ℤ m · ˙ X = n · ˙ N ⁡ X
27 eqeq1 ⊢ y = m · ˙ X → y = n · ˙ N ⁡ X ↔ m · ˙ X = n · ˙ N ⁡ X
28 27 rexbidv ⊢ y = m · ˙ X → ∃ n ∈ ℤ y = n · ˙ N ⁡ X ↔ ∃ n ∈ ℤ m · ˙ X = n · ˙ N ⁡ X
29 26 28 syl5ibrcom ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B ∧ m ∈ ℤ → y = m · ˙ X → ∃ n ∈ ℤ y = n · ˙ N ⁡ X
30 29 rexlimdva ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B → ∃ m ∈ ℤ y = m · ˙ X → ∃ n ∈ ℤ y = n · ˙ N ⁡ X
31 12 30 biimtrid ⊢ G ∈ Grp ∧ X ∈ E ∧ y ∈ B → ∃ n ∈ ℤ y = n · ˙ X → ∃ n ∈ ℤ y = n · ˙ N ⁡ X
32 31 ralimdva ⊢ G ∈ Grp ∧ X ∈ E → ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ X → ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ N ⁡ X
33 9 32 mpd ⊢ G ∈ Grp ∧ X ∈ E → ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ N ⁡ X
34 1 2 3 iscyggen2 ⊢ G ∈ Grp → N ⁡ X ∈ E ↔ N ⁡ X ∈ B ∧ ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ N ⁡ X
35 34 adantr ⊢ G ∈ Grp ∧ X ∈ E → N ⁡ X ∈ E ↔ N ⁡ X ∈ B ∧ ∀ y ∈ B ∃ n ∈ ℤ y = n · ˙ N ⁡ X
36 8 33 35 mpbir2and ⊢ G ∈ Grp ∧ X ∈ E → N ⁡ X ∈ E