This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )