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 ... 𝑁 ) )