Metamath Proof Explorer

Theorem gexlem2

Description: Any positive annihilator of all the group elements is an upper bound on the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Hypotheses gexcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gexcl.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
gexid.3 ⊢ · = ( .g ‘ 𝐺 )
gexid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion gexlem2 ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑁 · 𝑥 ) = 0 ) → 𝐸 ∈ ( 1 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 gexcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gexcl.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
3 gexid.3 ⊢ · = ( .g ‘ 𝐺 )
4 gexid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 oveq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 · 𝑥 ) = ( 𝑁 · 𝑥 ) )
6 5 eqeq1d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑦 · 𝑥 ) = 0 ↔ ( 𝑁 · 𝑥 ) = 0 ) )
7 6 ralbidv ⊢ ( 𝑦 = 𝑁 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑁 · 𝑥 ) = 0 ) )
8 7 elrab ⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ↔ ( 𝑁 ∈ ℕ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑁 · 𝑥 ) = 0 ) )
9 eqid ⊢ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 }
10 1 3 4 2 9 gexval ⊢ ( 𝐺 ∈ 𝑉 → 𝐸 = if ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } = ∅ , 0 , inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ) )
11 ne0i ⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } → { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ≠ ∅ )
12 ifnefalse ⊢ ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ≠ ∅ → if ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } = ∅ , 0 , inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ) = inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) )
13 11 12 syl ⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } → if ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } = ∅ , 0 , inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ) = inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) )
14 10 13 sylan9eq ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → 𝐸 = inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) )
15 ssrab2 ⊢ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ⊆ ℕ
16 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
17 15 16 sseqtri ⊢ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ⊆ ( ℤ≥ ‘ 1 )
18 11 adantl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ≠ ∅ )
19 infssuzcl ⊢ ( ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ≠ ∅ ) → inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } )
20 17 18 19 sylancr ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } )
21 15 20 sselid ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ℕ )
22 infssuzle ⊢ ( ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ≤ 𝑁 )
23 17 22 mpan ⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } → inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ≤ 𝑁 )
24 23 adantl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ≤ 𝑁 )
25 elrabi ⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } → 𝑁 ∈ ℕ )
26 25 nnzd ⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } → 𝑁 ∈ ℤ )
27 fznn ⊢ ( 𝑁 ∈ ℤ → ( inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ( 1 ... 𝑁 ) ↔ ( inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ℕ ∧ inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ≤ 𝑁 ) ) )
28 26 27 syl ⊢ ( 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } → ( inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ( 1 ... 𝑁 ) ↔ ( inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ℕ ∧ inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ≤ 𝑁 ) ) )
29 28 adantl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → ( inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ( 1 ... 𝑁 ) ↔ ( inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ℕ ∧ inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ≤ 𝑁 ) ) )
30 21 24 29 mpbir2and ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → inf ( { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } , ℝ , < ) ∈ ( 1 ... 𝑁 ) )
31 14 30 eqeltrd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ) → 𝐸 ∈ ( 1 ... 𝑁 ) )
32 8 31 sylan2br ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ( 𝑁 ∈ ℕ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑁 · 𝑥 ) = 0 ) ) → 𝐸 ∈ ( 1 ... 𝑁 ) )
33 32 3impb ⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑁 · 𝑥 ) = 0 ) → 𝐸 ∈ ( 1 ... 𝑁 ) )