Metamath Proof Explorer

Theorem gexex

Description: In an abelian group with finite exponent, there is an element in the group with order equal to the exponent. In other words, all orders of elements divide the largest order of an element of the group. This fails if E = 0 , for example in an infinite p-group, where there are elements of arbitrarily large orders (so E is zero) but no elements of infinite order. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexex.1 
|- X = ( Base ` G )
gexex.2 
|- E = ( gEx ` G )
gexex.3 
|- O = ( od ` G )
Assertion gexex 
|- ( ( G e. Abel /\ E e. NN ) -> E. x e. X ( O ` x ) = E )

Proof

Step Hyp Ref Expression
1 gexex.1 
 |-  X = ( Base ` G )
2 gexex.2 
 |-  E = ( gEx ` G )
3 gexex.3 
 |-  O = ( od ` G )
4 simpll 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) -> G e. Abel )
5 simplr 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) -> E e. NN )
6 simprl 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) -> x e. X )
7 1 3 odf 
 |-  O : X --> NN0
8 frn 
 |-  ( O : X --> NN0 -> ran O C_ NN0 )
9 7 8 ax-mp 
 |-  ran O C_ NN0
10 nn0ssz 
 |-  NN0 C_ ZZ
11 9 10 sstri 
 |-  ran O C_ ZZ
12 nnz 
 |-  ( E e. NN -> E e. ZZ )
13 12 adantl 
 |-  ( ( G e. Abel /\ E e. NN ) -> E e. ZZ )
14 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
15 14 adantr 
 |-  ( ( G e. Abel /\ E e. NN ) -> G e. Grp )
16 1 2 3 gexod 
 |-  ( ( G e. Grp /\ x e. X ) -> ( O ` x ) || E )
17 15 16 sylan 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ x e. X ) -> ( O ` x ) || E )
18 1 3 odcl 
 |-  ( x e. X -> ( O ` x ) e. NN0 )
19 18 adantl 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ x e. X ) -> ( O ` x ) e. NN0 )
20 19 nn0zd 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ x e. X ) -> ( O ` x ) e. ZZ )
21 simplr 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ x e. X ) -> E e. NN )
22 dvdsle 
 |-  ( ( ( O ` x ) e. ZZ /\ E e. NN ) -> ( ( O ` x ) || E -> ( O ` x ) <_ E ) )
23 20 21 22 syl2anc 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ x e. X ) -> ( ( O ` x ) || E -> ( O ` x ) <_ E ) )
24 17 23 mpd 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ x e. X ) -> ( O ` x ) <_ E )
25 24 ralrimiva 
 |-  ( ( G e. Abel /\ E e. NN ) -> A. x e. X ( O ` x ) <_ E )
26 ffn 
 |-  ( O : X --> NN0 -> O Fn X )
27 7 26 ax-mp 
 |-  O Fn X
28 breq1 
 |-  ( y = ( O ` x ) -> ( y <_ E <-> ( O ` x ) <_ E ) )
29 28 ralrn 
 |-  ( O Fn X -> ( A. y e. ran O y <_ E <-> A. x e. X ( O ` x ) <_ E ) )
30 27 29 ax-mp 
 |-  ( A. y e. ran O y <_ E <-> A. x e. X ( O ` x ) <_ E )
31 25 30 sylibr 
 |-  ( ( G e. Abel /\ E e. NN ) -> A. y e. ran O y <_ E )
32 brralrspcev 
 |-  ( ( E e. ZZ /\ A. y e. ran O y <_ E ) -> E. n e. ZZ A. y e. ran O y <_ n )
33 13 31 32 syl2anc 
 |-  ( ( G e. Abel /\ E e. NN ) -> E. n e. ZZ A. y e. ran O y <_ n )
34 33 ad2antrr 
 |-  ( ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) /\ y e. X ) -> E. n e. ZZ A. y e. ran O y <_ n )
35 27 a1i 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) -> O Fn X )
36 fnfvelrn 
 |-  ( ( O Fn X /\ y e. X ) -> ( O ` y ) e. ran O )
37 35 36 sylan 
 |-  ( ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) /\ y e. X ) -> ( O ` y ) e. ran O )
38 suprzub 
 |-  ( ( ran O C_ ZZ /\ E. n e. ZZ A. y e. ran O y <_ n /\ ( O ` y ) e. ran O ) -> ( O ` y ) <_ sup ( ran O , RR , < ) )
39 11 34 37 38 mp3an2i 
 |-  ( ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) /\ y e. X ) -> ( O ` y ) <_ sup ( ran O , RR , < ) )
40 simplrr 
 |-  ( ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) /\ y e. X ) -> ( O ` x ) = sup ( ran O , RR , < ) )
41 39 40 breqtrrd 
 |-  ( ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) /\ y e. X ) -> ( O ` y ) <_ ( O ` x ) )
42 1 2 3 4 5 6 41 gexexlem 
 |-  ( ( ( G e. Abel /\ E e. NN ) /\ ( x e. X /\ ( O ` x ) = sup ( ran O , RR , < ) ) ) -> ( O ` x ) = E )
43 1 grpbn0 
 |-  ( G e. Grp -> X =/= (/) )
44 15 43 syl 
 |-  ( ( G e. Abel /\ E e. NN ) -> X =/= (/) )
45 7 fdmi 
 |-  dom O = X
46 45 eqeq1i 
 |-  ( dom O = (/) <-> X = (/) )
47 dm0rn0 
 |-  ( dom O = (/) <-> ran O = (/) )
48 46 47 bitr3i 
 |-  ( X = (/) <-> ran O = (/) )
49 48 necon3bii 
 |-  ( X =/= (/) <-> ran O =/= (/) )
50 44 49 sylib 
 |-  ( ( G e. Abel /\ E e. NN ) -> ran O =/= (/) )
51 suprzcl2 
 |-  ( ( ran O C_ ZZ /\ ran O =/= (/) /\ E. n e. ZZ A. y e. ran O y <_ n ) -> sup ( ran O , RR , < ) e. ran O )
52 11 50 33 51 mp3an2i 
 |-  ( ( G e. Abel /\ E e. NN ) -> sup ( ran O , RR , < ) e. ran O )
53 fvelrnb 
 |-  ( O Fn X -> ( sup ( ran O , RR , < ) e. ran O <-> E. x e. X ( O ` x ) = sup ( ran O , RR , < ) ) )
54 27 53 ax-mp 
 |-  ( sup ( ran O , RR , < ) e. ran O <-> E. x e. X ( O ` x ) = sup ( ran O , RR , < ) )
55 52 54 sylib 
 |-  ( ( G e. Abel /\ E e. NN ) -> E. x e. X ( O ` x ) = sup ( ran O , RR , < ) )
56 42 55 reximddv 
 |-  ( ( G e. Abel /\ E e. NN ) -> E. x e. X ( O ` x ) = E )