Description: The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | iscyg.1 | |
|
iscyg.2 | |
||
iscyg3.e | |
||
cyggeninv.n | |
||
Assertion | cyggeninv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscyg.1 | |
|
2 | iscyg.2 | |
|
3 | iscyg3.e | |
|
4 | cyggeninv.n | |
|
5 | 1 2 3 | iscyggen2 | |
6 | 5 | simprbda | |
7 | 1 4 | grpinvcl | |
8 | 6 7 | syldan | |
9 | 5 | simplbda | |
10 | oveq1 | |
|
11 | 10 | eqeq2d | |
12 | 11 | cbvrexvw | |
13 | znegcl | |
|
14 | 13 | adantl | |
15 | simpr | |
|
16 | 15 | zcnd | |
17 | 16 | negnegd | |
18 | 17 | oveq1d | |
19 | simplll | |
|
20 | 6 | ad2antrr | |
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 | |
35 | 34 | adantr | |
36 | 8 33 35 | mpbir2and | |