Metamath Proof Explorer

Theorem cyggex2

Description: The exponent of a cyclic group is 0 if the group is infinite, otherwise it equals the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses cygctb.1 
|- B = ( Base ` G )
cyggex.o 
|- E = ( gEx ` G )
Assertion cyggex2 
|- ( G e. CycGrp -> E = if ( B e. Fin , ( # ` B ) , 0 ) )

Proof

Step Hyp Ref Expression
1 cygctb.1 
 |-  B = ( Base ` G )
2 cyggex.o 
 |-  E = ( gEx ` G )
3 eqid 
 |-  ( .g ` G ) = ( .g ` G )
4 eqid 
 |-  { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } = { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B }
5 1 3 4 iscyg2 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) ) )
6 n0 
 |-  ( { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) <-> E. y y e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } )
7 ssrab2 
 |-  { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } C_ B
8 simpr 
 |-  ( ( G e. Grp /\ y e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } ) -> y e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } )
9 7 8 sseldi 
 |-  ( ( G e. Grp /\ y e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } ) -> y e. B )
10 eqid 
 |-  ( od ` G ) = ( od ` G )
11 1 3 4 10 cyggenod2 
 |-  ( ( G e. Grp /\ y e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } ) -> ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) )
12 9 11 jca 
 |-  ( ( G e. Grp /\ y e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } ) -> ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) )
13 12 ex 
 |-  ( G e. Grp -> ( y e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } -> ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) )
14 1 2 gexcl 
 |-  ( G e. Grp -> E e. NN0 )
15 14 adantr 
 |-  ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) -> E e. NN0 )
16 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
17 16 adantl 
 |-  ( ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) /\ B e. Fin ) -> ( # ` B ) e. NN0 )
18 0nn0 
 |-  0 e. NN0
19 18 a1i 
 |-  ( ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) /\ -. B e. Fin ) -> 0 e. NN0 )
20 17 19 ifclda 
 |-  ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) -> if ( B e. Fin , ( # ` B ) , 0 ) e. NN0 )
21 breq2 
 |-  ( ( # ` B ) = if ( B e. Fin , ( # ` B ) , 0 ) -> ( E || ( # ` B ) <-> E || if ( B e. Fin , ( # ` B ) , 0 ) ) )
22 breq2 
 |-  ( 0 = if ( B e. Fin , ( # ` B ) , 0 ) -> ( E || 0 <-> E || if ( B e. Fin , ( # ` B ) , 0 ) ) )
23 1 2 gexdvds3 
 |-  ( ( G e. Grp /\ B e. Fin ) -> E || ( # ` B ) )
24 23 adantlr 
 |-  ( ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) /\ B e. Fin ) -> E || ( # ` B ) )
25 15 adantr 
 |-  ( ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) /\ -. B e. Fin ) -> E e. NN0 )
26 nn0z 
 |-  ( E e. NN0 -> E e. ZZ )
27 dvds0 
 |-  ( E e. ZZ -> E || 0 )
28 25 26 27 3syl 
 |-  ( ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) /\ -. B e. Fin ) -> E || 0 )
29 21 22 24 28 ifbothda 
 |-  ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) -> E || if ( B e. Fin , ( # ` B ) , 0 ) )
30 simprr 
 |-  ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) -> ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) )
31 1 2 10 gexod 
 |-  ( ( G e. Grp /\ y e. B ) -> ( ( od ` G ) ` y ) || E )
32 31 adantrr 
 |-  ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) -> ( ( od ` G ) ` y ) || E )
33 30 32 eqbrtrrd 
 |-  ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) -> if ( B e. Fin , ( # ` B ) , 0 ) || E )
34 dvdseq 
 |-  ( ( ( E e. NN0 /\ if ( B e. Fin , ( # ` B ) , 0 ) e. NN0 ) /\ ( E || if ( B e. Fin , ( # ` B ) , 0 ) /\ if ( B e. Fin , ( # ` B ) , 0 ) || E ) ) -> E = if ( B e. Fin , ( # ` B ) , 0 ) )
35 15 20 29 33 34 syl22anc 
 |-  ( ( G e. Grp /\ ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) ) -> E = if ( B e. Fin , ( # ` B ) , 0 ) )
36 35 ex 
 |-  ( G e. Grp -> ( ( y e. B /\ ( ( od ` G ) ` y ) = if ( B e. Fin , ( # ` B ) , 0 ) ) -> E = if ( B e. Fin , ( # ` B ) , 0 ) ) )
37 13 36 syld 
 |-  ( G e. Grp -> ( y e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } -> E = if ( B e. Fin , ( # ` B ) , 0 ) ) )
38 37 exlimdv 
 |-  ( G e. Grp -> ( E. y y e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } -> E = if ( B e. Fin , ( # ` B ) , 0 ) ) )
39 6 38 syl5bi 
 |-  ( G e. Grp -> ( { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) -> E = if ( B e. Fin , ( # ` B ) , 0 ) ) )
40 39 imp 
 |-  ( ( G e. Grp /\ { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) ) -> E = if ( B e. Fin , ( # ` B ) , 0 ) )
41 5 40 sylbi 
 |-  ( G e. CycGrp -> E = if ( B e. Fin , ( # ` B ) , 0 ) )