Metamath Proof Explorer

Theorem cyggenod

Description: An element is the generator of a finite group iff the order of the generator equals the order of the group. (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 }
cyggenod.o 
|- O = ( od ` G )
Assertion cyggenod 
|- ( ( G e. Grp /\ B e. Fin ) -> ( X e. E <-> ( X e. B /\ ( O ` X ) = ( # ` B ) ) ) )

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 cyggenod.o 
 |-  O = ( od ` G )
5 1 2 3 iscyggen 
 |-  ( X e. E <-> ( X e. B /\ ran ( n e. ZZ |-> ( n .x. X ) ) = B ) )
6 simplr 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> B e. Fin )
7 simplll 
 |-  ( ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) /\ n e. ZZ ) -> G e. Grp )
8 simpr 
 |-  ( ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) /\ n e. ZZ ) -> n e. ZZ )
9 simplr 
 |-  ( ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) /\ n e. ZZ ) -> X e. B )
10 1 2 mulgcl 
 |-  ( ( G e. Grp /\ n e. ZZ /\ X e. B ) -> ( n .x. X ) e. B )
11 7 8 9 10 syl3anc 
 |-  ( ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) /\ n e. ZZ ) -> ( n .x. X ) e. B )
12 11 fmpttd 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> ( n e. ZZ |-> ( n .x. X ) ) : ZZ --> B )
13 12 frnd 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> ran ( n e. ZZ |-> ( n .x. X ) ) C_ B )
14 6 13 ssfid 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> ran ( n e. ZZ |-> ( n .x. X ) ) e. Fin )
15 hashen 
 |-  ( ( ran ( n e. ZZ |-> ( n .x. X ) ) e. Fin /\ B e. Fin ) -> ( ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) = ( # ` B ) <-> ran ( n e. ZZ |-> ( n .x. X ) ) ~~ B ) )
16 14 6 15 syl2anc 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> ( ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) = ( # ` B ) <-> ran ( n e. ZZ |-> ( n .x. X ) ) ~~ B ) )
17 eqid 
 |-  ( n e. ZZ |-> ( n .x. X ) ) = ( n e. ZZ |-> ( n .x. X ) )
18 1 4 2 17 dfod2 
 |-  ( ( G e. Grp /\ X e. B ) -> ( O ` X ) = if ( ran ( n e. ZZ |-> ( n .x. X ) ) e. Fin , ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) , 0 ) )
19 18 adantlr 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> ( O ` X ) = if ( ran ( n e. ZZ |-> ( n .x. X ) ) e. Fin , ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) , 0 ) )
20 14 iftrued 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> if ( ran ( n e. ZZ |-> ( n .x. X ) ) e. Fin , ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) , 0 ) = ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) )
21 19 20 eqtr2d 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) = ( O ` X ) )
22 21 eqeq1d 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> ( ( # ` ran ( n e. ZZ |-> ( n .x. X ) ) ) = ( # ` B ) <-> ( O ` X ) = ( # ` B ) ) )
23 fisseneq 
 |-  ( ( B e. Fin /\ ran ( n e. ZZ |-> ( n .x. X ) ) C_ B /\ ran ( n e. ZZ |-> ( n .x. X ) ) ~~ B ) -> ran ( n e. ZZ |-> ( n .x. X ) ) = B )
24 23 3expia 
 |-  ( ( B e. Fin /\ ran ( n e. ZZ |-> ( n .x. X ) ) C_ B ) -> ( ran ( n e. ZZ |-> ( n .x. X ) ) ~~ B -> ran ( n e. ZZ |-> ( n .x. X ) ) = B ) )
25 enrefg 
 |-  ( B e. Fin -> B ~~ B )
26 25 adantr 
 |-  ( ( B e. Fin /\ ran ( n e. ZZ |-> ( n .x. X ) ) C_ B ) -> B ~~ B )
27 breq1 
 |-  ( ran ( n e. ZZ |-> ( n .x. X ) ) = B -> ( ran ( n e. ZZ |-> ( n .x. X ) ) ~~ B <-> B ~~ B ) )
28 26 27 syl5ibrcom 
 |-  ( ( B e. Fin /\ ran ( n e. ZZ |-> ( n .x. X ) ) C_ B ) -> ( ran ( n e. ZZ |-> ( n .x. X ) ) = B -> ran ( n e. ZZ |-> ( n .x. X ) ) ~~ B ) )
29 24 28 impbid 
 |-  ( ( B e. Fin /\ ran ( n e. ZZ |-> ( n .x. X ) ) C_ B ) -> ( ran ( n e. ZZ |-> ( n .x. X ) ) ~~ B <-> ran ( n e. ZZ |-> ( n .x. X ) ) = B ) )
30 6 13 29 syl2anc 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> ( ran ( n e. ZZ |-> ( n .x. X ) ) ~~ B <-> ran ( n e. ZZ |-> ( n .x. X ) ) = B ) )
31 16 22 30 3bitr3rd 
 |-  ( ( ( G e. Grp /\ B e. Fin ) /\ X e. B ) -> ( ran ( n e. ZZ |-> ( n .x. X ) ) = B <-> ( O ` X ) = ( # ` B ) ) )
32 31 pm5.32da 
 |-  ( ( G e. Grp /\ B e. Fin ) -> ( ( X e. B /\ ran ( n e. ZZ |-> ( n .x. X ) ) = B ) <-> ( X e. B /\ ( O ` X ) = ( # ` B ) ) ) )
33 5 32 syl5bb 
 |-  ( ( G e. Grp /\ B e. Fin ) -> ( X e. E <-> ( X e. B /\ ( O ` X ) = ( # ` B ) ) ) )