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 = ( Base ` G )
iscyg.2 
|- .x. = ( .g ` G )
iscyg3.e 
|- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
cyggeninv.n 
|- N = ( invg ` G )
Assertion cyggeninv 
|- ( ( G e. Grp /\ X e. E ) -> ( N ` X ) e. E )

Proof

Step Hyp Ref Expression
1 iscyg.1 
 |-  B = ( Base ` G )
2 iscyg.2 
 |-  .x. = ( .g ` G )
3 iscyg3.e 
 |-  E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
4 cyggeninv.n 
 |-  N = ( invg ` G )
5 1 2 3 iscyggen2 
 |-  ( G e. Grp -> ( X e. E <-> ( X e. B /\ A. y e. B E. n e. ZZ y = ( n .x. X ) ) ) )
6 5 simprbda 
 |-  ( ( G e. Grp /\ X e. E ) -> X e. B )
7 1 4 grpinvcl 
 |-  ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )
8 6 7 syldan 
 |-  ( ( G e. Grp /\ X e. E ) -> ( N ` X ) e. B )
9 5 simplbda 
 |-  ( ( G e. Grp /\ X e. E ) -> A. y e. B E. n e. ZZ y = ( n .x. X ) )
10 oveq1 
 |-  ( n = m -> ( n .x. X ) = ( m .x. X ) )
11 10 eqeq2d 
 |-  ( n = m -> ( y = ( n .x. X ) <-> y = ( m .x. X ) ) )
12 11 cbvrexvw 
 |-  ( E. n e. ZZ y = ( n .x. X ) <-> E. m e. ZZ y = ( m .x. X ) )
13 znegcl 
 |-  ( m e. ZZ -> -u m e. ZZ )
14 13 adantl 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> -u m e. ZZ )
15 simpr 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> m e. ZZ )
16 15 zcnd 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> m e. CC )
17 16 negnegd 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> -u -u m = m )
18 17 oveq1d 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> ( -u -u m .x. X ) = ( m .x. X ) )
19 simplll 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> G e. Grp )
20 6 ad2antrr 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> X e. B )
21 1 2 4 mulgneg2 
 |-  ( ( G e. Grp /\ -u m e. ZZ /\ X e. B ) -> ( -u -u m .x. X ) = ( -u m .x. ( N ` X ) ) )
22 19 14 20 21 syl3anc 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> ( -u -u m .x. X ) = ( -u m .x. ( N ` X ) ) )
23 18 22 eqtr3d 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> ( m .x. X ) = ( -u m .x. ( N ` X ) ) )
24 oveq1 
 |-  ( n = -u m -> ( n .x. ( N ` X ) ) = ( -u m .x. ( N ` X ) ) )
25 24 rspceeqv 
 |-  ( ( -u m e. ZZ /\ ( m .x. X ) = ( -u m .x. ( N ` X ) ) ) -> E. n e. ZZ ( m .x. X ) = ( n .x. ( N ` X ) ) )
26 14 23 25 syl2anc 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> E. n e. ZZ ( m .x. X ) = ( n .x. ( N ` X ) ) )
27 eqeq1 
 |-  ( y = ( m .x. X ) -> ( y = ( n .x. ( N ` X ) ) <-> ( m .x. X ) = ( n .x. ( N ` X ) ) ) )
28 27 rexbidv 
 |-  ( y = ( m .x. X ) -> ( E. n e. ZZ y = ( n .x. ( N ` X ) ) <-> E. n e. ZZ ( m .x. X ) = ( n .x. ( N ` X ) ) ) )
29 26 28 syl5ibrcom 
 |-  ( ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) /\ m e. ZZ ) -> ( y = ( m .x. X ) -> E. n e. ZZ y = ( n .x. ( N ` X ) ) ) )
30 29 rexlimdva 
 |-  ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) -> ( E. m e. ZZ y = ( m .x. X ) -> E. n e. ZZ y = ( n .x. ( N ` X ) ) ) )
31 12 30 syl5bi 
 |-  ( ( ( G e. Grp /\ X e. E ) /\ y e. B ) -> ( E. n e. ZZ y = ( n .x. X ) -> E. n e. ZZ y = ( n .x. ( N ` X ) ) ) )
32 31 ralimdva 
 |-  ( ( G e. Grp /\ X e. E ) -> ( A. y e. B E. n e. ZZ y = ( n .x. X ) -> A. y e. B E. n e. ZZ y = ( n .x. ( N ` X ) ) ) )
33 9 32 mpd 
 |-  ( ( G e. Grp /\ X e. E ) -> A. y e. B E. n e. ZZ y = ( n .x. ( N ` X ) ) )
34 1 2 3 iscyggen2 
 |-  ( G e. Grp -> ( ( N ` X ) e. E <-> ( ( N ` X ) e. B /\ A. y e. B E. n e. ZZ y = ( n .x. ( N ` X ) ) ) ) )
35 34 adantr 
 |-  ( ( G e. Grp /\ X e. E ) -> ( ( N ` X ) e. E <-> ( ( N ` X ) e. B /\ A. y e. B E. n e. ZZ y = ( n .x. ( N ` X ) ) ) ) )
36 8 33 35 mpbir2and 
 |-  ( ( G e. Grp /\ X e. E ) -> ( N ` X ) e. E )