# 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}={\mathrm{Base}}_{{G}}$
iscyg.2
iscyg3.e
cyggeninv.n ${⊢}{N}={inv}_{g}\left({G}\right)$
Assertion cyggeninv ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\to {N}\left({X}\right)\in {E}$

### Proof

Step Hyp Ref Expression
1 iscyg.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 iscyg.2
3 iscyg3.e
4 cyggeninv.n ${⊢}{N}={inv}_{g}\left({G}\right)$
5 1 2 3 iscyggen2
6 5 simprbda ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\to {X}\in {B}$
7 1 4 grpinvcl ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {B}\right)\to {N}\left({X}\right)\in {B}$
8 6 7 syldan ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\to {N}\left({X}\right)\in {B}$
9 5 simplbda
10 oveq1
11 10 eqeq2d
12 11 cbvrexvw
13 znegcl ${⊢}{m}\in ℤ\to -{m}\in ℤ$
14 13 adantl ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\wedge {y}\in {B}\right)\wedge {m}\in ℤ\right)\to -{m}\in ℤ$
15 simpr ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\wedge {y}\in {B}\right)\wedge {m}\in ℤ\right)\to {m}\in ℤ$
16 15 zcnd ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\wedge {y}\in {B}\right)\wedge {m}\in ℤ\right)\to {m}\in ℂ$
17 16 negnegd ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\wedge {y}\in {B}\right)\wedge {m}\in ℤ\right)\to -\left(-{m}\right)={m}$
18 17 oveq1d
19 simplll ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\wedge {y}\in {B}\right)\wedge {m}\in ℤ\right)\to {G}\in \mathrm{Grp}$
20 6 ad2antrr ${⊢}\left(\left(\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\wedge {y}\in {B}\right)\wedge {m}\in ℤ\right)\to {X}\in {B}$
21 1 2 4 mulgneg2
22 19 14 20 21 syl3anc
23 18 22 eqtr3d
24 oveq1
25 24 rspceeqv
26 14 23 25 syl2anc
27 eqeq1
28 27 rexbidv
29 26 28 syl5ibrcom
30 29 rexlimdva
31 12 30 syl5bi
32 31 ralimdva
33 9 32 mpd
34 1 2 3 iscyggen2
36 8 33 35 mpbir2and ${⊢}\left({G}\in \mathrm{Grp}\wedge {X}\in {E}\right)\to {N}\left({X}\right)\in {E}$