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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gexex.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
gexex.3 ⊢ 𝑂 = ( od ‘ 𝐺 )
Assertion gexex ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∃ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) = 𝐸 )

Proof

Step Hyp Ref Expression
1 gexex.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gexex.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
3 gexex.3 ⊢ 𝑂 = ( od ‘ 𝐺 )
4 simpll ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → 𝐺 ∈ Abel )
5 simplr ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → 𝐸 ∈ ℕ )
6 simprl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → 𝑥 ∈ 𝑋 )
7 1 3 odf ⊢ 𝑂 : 𝑋 ⟶ ℕ0
8 frn ⊢ ( 𝑂 : 𝑋 ⟶ ℕ0 → ran 𝑂 ⊆ ℕ0 )
9 7 8 ax-mp ⊢ ran 𝑂 ⊆ ℕ0
10 nn0ssz ⊢ ℕ0 ⊆ ℤ
11 9 10 sstri ⊢ ran 𝑂 ⊆ ℤ
12 nnz ⊢ ( 𝐸 ∈ ℕ → 𝐸 ∈ ℤ )
13 12 adantl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → 𝐸 ∈ ℤ )
14 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
15 14 adantr ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → 𝐺 ∈ Grp )
16 1 2 3 gexod ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑥 ) ∥ 𝐸 )
17 15 16 sylan ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑥 ) ∥ 𝐸 )
18 1 3 odcl ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
19 18 adantl ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
20 19 nn0zd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑥 ) ∈ ℤ )
21 simplr ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ∈ ℕ )
22 dvdsle ⊢ ( ( ( 𝑂 ‘ 𝑥 ) ∈ ℤ ∧ 𝐸 ∈ ℕ ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝐸 → ( 𝑂 ‘ 𝑥 ) ≤ 𝐸 ) )
23 20 21 22 syl2anc ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 𝐸 → ( 𝑂 ‘ 𝑥 ) ≤ 𝐸 ) )
24 17 23 mpd ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑥 ) ≤ 𝐸 )
25 24 ralrimiva ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ≤ 𝐸 )
26 ffn ⊢ ( 𝑂 : 𝑋 ⟶ ℕ0 → 𝑂 Fn 𝑋 )
27 7 26 ax-mp ⊢ 𝑂 Fn 𝑋
28 breq1 ⊢ ( 𝑦 = ( 𝑂 ‘ 𝑥 ) → ( 𝑦 ≤ 𝐸 ↔ ( 𝑂 ‘ 𝑥 ) ≤ 𝐸 ) )
29 28 ralrn ⊢ ( 𝑂 Fn 𝑋 → ( ∀ 𝑦 ∈ ran 𝑂 𝑦 ≤ 𝐸 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ≤ 𝐸 ) )
30 27 29 ax-mp ⊢ ( ∀ 𝑦 ∈ ran 𝑂 𝑦 ≤ 𝐸 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) ≤ 𝐸 )
31 25 30 sylibr ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∀ 𝑦 ∈ ran 𝑂 𝑦 ≤ 𝐸 )
32 brralrspcev ⊢ ( ( 𝐸 ∈ ℤ ∧ ∀ 𝑦 ∈ ran 𝑂 𝑦 ≤ 𝐸 ) → ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦 ≤ 𝑛 )
33 13 31 32 syl2anc ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦 ≤ 𝑛 )
34 33 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦 ≤ 𝑛 )
35 27 a1i ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → 𝑂 Fn 𝑋 )
36 fnfvelrn ⊢ ( ( 𝑂 Fn 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑦 ) ∈ ran 𝑂 )
37 35 36 sylan ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑦 ) ∈ ran 𝑂 )
38 suprzub ⊢ ( ( ran 𝑂 ⊆ ℤ ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦 ≤ 𝑛 ∧ ( 𝑂 ‘ 𝑦 ) ∈ ran 𝑂 ) → ( 𝑂 ‘ 𝑦 ) ≤ sup ( ran 𝑂 , ℝ , < ) )
39 11 34 37 38 mp3an2i ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑦 ) ≤ sup ( ran 𝑂 , ℝ , < ) )
40 simplrr ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) )
41 39 40 breqtrrd ⊢ ( ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑂 ‘ 𝑦 ) ≤ ( 𝑂 ‘ 𝑥 ) )
42 1 2 3 4 5 6 41 gexexlem ⊢ ( ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) ) → ( 𝑂 ‘ 𝑥 ) = 𝐸 )
43 1 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
44 15 43 syl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → 𝑋 ≠ ∅ )
45 7 fdmi ⊢ dom 𝑂 = 𝑋
46 45 eqeq1i ⊢ ( dom 𝑂 = ∅ ↔ 𝑋 = ∅ )
47 dm0rn0 ⊢ ( dom 𝑂 = ∅ ↔ ran 𝑂 = ∅ )
48 46 47 bitr3i ⊢ ( 𝑋 = ∅ ↔ ran 𝑂 = ∅ )
49 48 necon3bii ⊢ ( 𝑋 ≠ ∅ ↔ ran 𝑂 ≠ ∅ )
50 44 49 sylib ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ran 𝑂 ≠ ∅ )
51 suprzcl2 ⊢ ( ( ran 𝑂 ⊆ ℤ ∧ ran 𝑂 ≠ ∅ ∧ ∃ 𝑛 ∈ ℤ ∀ 𝑦 ∈ ran 𝑂 𝑦 ≤ 𝑛 ) → sup ( ran 𝑂 , ℝ , < ) ∈ ran 𝑂 )
52 11 50 33 51 mp3an2i ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → sup ( ran 𝑂 , ℝ , < ) ∈ ran 𝑂 )
53 fvelrnb ⊢ ( 𝑂 Fn 𝑋 → ( sup ( ran 𝑂 , ℝ , < ) ∈ ran 𝑂 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) ) )
54 27 53 ax-mp ⊢ ( sup ( ran 𝑂 , ℝ , < ) ∈ ran 𝑂 ↔ ∃ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) )
55 52 54 sylib ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∃ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) = sup ( ran 𝑂 , ℝ , < ) )
56 42 55 reximddv ⊢ ( ( 𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ ) → ∃ 𝑥 ∈ 𝑋 ( 𝑂 ‘ 𝑥 ) = 𝐸 )