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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
iscyg.2 ⊢ · = ( .g ‘ 𝐺 )
iscyg3.e ⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
cyggeninv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
Assertion cyggeninv ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 iscyg.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 iscyg.2 ⊢ · = ( .g ‘ 𝐺 )
3 iscyg3.e ⊢ 𝐸 = { 𝑥 ∈ 𝐵 ∣ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = 𝐵 }
4 cyggeninv.n ⊢ 𝑁 = ( invg ‘ 𝐺 )
5 1 2 3 iscyggen2 ⊢ ( 𝐺 ∈ Grp → ( 𝑋 ∈ 𝐸 ↔ ( 𝑋 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) ) ) )
6 5 simprbda ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) → 𝑋 ∈ 𝐵 )
7 1 4 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
8 6 7 syldan ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
9 5 simplbda ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) )
10 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 · 𝑋 ) = ( 𝑚 · 𝑋 ) )
11 10 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑦 = ( 𝑛 · 𝑋 ) ↔ 𝑦 = ( 𝑚 · 𝑋 ) ) )
12 11 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) ↔ ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝑚 · 𝑋 ) )
13 znegcl ⊢ ( 𝑚 ∈ ℤ → - 𝑚 ∈ ℤ )
14 13 adantl ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → - 𝑚 ∈ ℤ )
15 simpr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ )
16 15 zcnd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℂ )
17 16 negnegd ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → - - 𝑚 = 𝑚 )
18 17 oveq1d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → ( - - 𝑚 · 𝑋 ) = ( 𝑚 · 𝑋 ) )
19 simplll ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → 𝐺 ∈ Grp )
20 6 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → 𝑋 ∈ 𝐵 )
21 1 2 4 mulgneg2 ⊢ ( ( 𝐺 ∈ Grp ∧ - 𝑚 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - - 𝑚 · 𝑋 ) = ( - 𝑚 · ( 𝑁 ‘ 𝑋 ) ) )
22 19 14 20 21 syl3anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → ( - - 𝑚 · 𝑋 ) = ( - 𝑚 · ( 𝑁 ‘ 𝑋 ) ) )
23 18 22 eqtr3d ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → ( 𝑚 · 𝑋 ) = ( - 𝑚 · ( 𝑁 ‘ 𝑋 ) ) )
24 oveq1 ⊢ ( 𝑛 = - 𝑚 → ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) = ( - 𝑚 · ( 𝑁 ‘ 𝑋 ) ) )
25 24 rspceeqv ⊢ ( ( - 𝑚 ∈ ℤ ∧ ( 𝑚 · 𝑋 ) = ( - 𝑚 · ( 𝑁 ‘ 𝑋 ) ) ) → ∃ 𝑛 ∈ ℤ ( 𝑚 · 𝑋 ) = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) )
26 14 23 25 syl2anc ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → ∃ 𝑛 ∈ ℤ ( 𝑚 · 𝑋 ) = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) )
27 eqeq1 ⊢ ( 𝑦 = ( 𝑚 · 𝑋 ) → ( 𝑦 = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ↔ ( 𝑚 · 𝑋 ) = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ) )
28 27 rexbidv ⊢ ( 𝑦 = ( 𝑚 · 𝑋 ) → ( ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ↔ ∃ 𝑛 ∈ ℤ ( 𝑚 · 𝑋 ) = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ) )
29 26 28 syl5ibrcom ⊢ ( ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑚 ∈ ℤ ) → ( 𝑦 = ( 𝑚 · 𝑋 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ) )
30 29 rexlimdva ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑚 ∈ ℤ 𝑦 = ( 𝑚 · 𝑋 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ) )
31 12 30 syl5bi ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) → ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ) )
32 31 ralimdva ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · 𝑋 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ) )
33 9 32 mpd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) )
34 1 2 3 iscyggen2 ⊢ ( 𝐺 ∈ Grp → ( ( 𝑁 ‘ 𝑋 ) ∈ 𝐸 ↔ ( ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ) ) )
35 34 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) → ( ( 𝑁 ‘ 𝑋 ) ∈ 𝐸 ↔ ( ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ∃ 𝑛 ∈ ℤ 𝑦 = ( 𝑛 · ( 𝑁 ‘ 𝑋 ) ) ) ) )
36 8 33 35 mpbir2and ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐸 )