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=BaseG
iscyg.2 ·˙=G
iscyg3.e E=xB|rannn·˙x=B
cyggeninv.n N=invgG
Assertion cyggeninv GGrpXENXE

Proof

Step Hyp Ref Expression
1 iscyg.1 B=BaseG
2 iscyg.2 ·˙=G
3 iscyg3.e E=xB|rannn·˙x=B
4 cyggeninv.n N=invgG
5 1 2 3 iscyggen2 GGrpXEXByBny=n·˙X
6 5 simprbda GGrpXEXB
7 1 4 grpinvcl GGrpXBNXB
8 6 7 syldan GGrpXENXB
9 5 simplbda GGrpXEyBny=n·˙X
10 oveq1 n=mn·˙X=m·˙X
11 10 eqeq2d n=my=n·˙Xy=m·˙X
12 11 cbvrexvw ny=n·˙Xmy=m·˙X
13 znegcl mm
14 13 adantl GGrpXEyBmm
15 simpr GGrpXEyBmm
16 15 zcnd GGrpXEyBmm
17 16 negnegd GGrpXEyBmm=m
18 17 oveq1d GGrpXEyBmm·˙X=m·˙X
19 simplll GGrpXEyBmGGrp
20 6 ad2antrr GGrpXEyBmXB
21 1 2 4 mulgneg2 GGrpmXBm·˙X=m·˙NX
22 19 14 20 21 syl3anc GGrpXEyBmm·˙X=m·˙NX
23 18 22 eqtr3d GGrpXEyBmm·˙X=m·˙NX
24 oveq1 n=mn·˙NX=m·˙NX
25 24 rspceeqv mm·˙X=m·˙NXnm·˙X=n·˙NX
26 14 23 25 syl2anc GGrpXEyBmnm·˙X=n·˙NX
27 eqeq1 y=m·˙Xy=n·˙NXm·˙X=n·˙NX
28 27 rexbidv y=m·˙Xny=n·˙NXnm·˙X=n·˙NX
29 26 28 syl5ibrcom GGrpXEyBmy=m·˙Xny=n·˙NX
30 29 rexlimdva GGrpXEyBmy=m·˙Xny=n·˙NX
31 12 30 syl5bi GGrpXEyBny=n·˙Xny=n·˙NX
32 31 ralimdva GGrpXEyBny=n·˙XyBny=n·˙NX
33 9 32 mpd GGrpXEyBny=n·˙NX
34 1 2 3 iscyggen2 GGrpNXENXByBny=n·˙NX
35 34 adantr GGrpXENXENXByBny=n·˙NX
36 8 33 35 mpbir2and GGrpXENXE