Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cyggeninv Structured version   Unicode version

Theorem cyggeninv 15486
 Description: The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypotheses
Ref Expression
iscyg.1
iscyg.2 .g
iscyg3.e
cyggeninv.n
Assertion
Ref Expression
cyggeninv
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem cyggeninv
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iscyg.1 . . . . 5
2 iscyg.2 . . . . 5 .g
3 iscyg3.e . . . . 5
41, 2, 3iscyggen2 15484 . . . 4
54simprbda 607 . . 3
6 cyggeninv.n . . . 4
71, 6grpinvcl 14843 . . 3
85, 7syldan 457 . 2
94simplbda 608 . . 3
10 oveq1 6081 . . . . . . 7
1110eqeq2d 2447 . . . . . 6
1211cbvrexv 2926 . . . . 5
13 znegcl 10306 . . . . . . . . 9
1413adantl 453 . . . . . . . 8
15 simpr 448 . . . . . . . . . . . 12
1615zcnd 10369 . . . . . . . . . . 11
1716negnegd 9395 . . . . . . . . . 10
1817oveq1d 6089 . . . . . . . . 9
19 simplll 735 . . . . . . . . . 10
205ad2antrr 707 . . . . . . . . . 10
211, 2, 6mulgneg2 14910 . . . . . . . . . 10
2219, 14, 20, 21syl3anc 1184 . . . . . . . . 9
2318, 22eqtr3d 2470 . . . . . . . 8
24 oveq1 6081 . . . . . . . . . 10
2524eqeq2d 2447 . . . . . . . . 9
2625rspcev 3045 . . . . . . . 8
2714, 23, 26syl2anc 643 . . . . . . 7
28 eqeq1 2442 . . . . . . . 8
2928rexbidv 2719 . . . . . . 7
3027, 29syl5ibrcom 214 . . . . . 6
3130rexlimdva 2823 . . . . 5
3212, 31syl5bi 209 . . . 4
3332ralimdva 2777 . . 3
349, 33mpd 15 . 2
351, 2, 3iscyggen2 15484 . . 3