Theorem gexlem1

Description: The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 23-Apr-2016) (Proof shortened by AV, 26-Sep-2020)

	Ref	Expression
Hypotheses	gexval.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	gexval.2	⊢ · = ( .g ‘ 𝐺 )
	gexval.3	⊢ 0 = ( 0g ‘ 𝐺 )
	gexval.4	⊢ 𝐸 = ( gEx ‘ 𝐺 )
	gexval.i	⊢ 𝐼 = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 }
Assertion	gexlem1	⊢ ( 𝐺 ∈ 𝑉 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		gexval.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		gexval.2	⊢ · = ( .g ‘ 𝐺 )
3		gexval.3	⊢ 0 = ( 0g ‘ 𝐺 )
4		gexval.4	⊢ 𝐸 = ( gEx ‘ 𝐺 )
5		gexval.i	⊢ 𝐼 = { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 }
6	1 2 3 4 5	gexval	⊢ ( 𝐺 ∈ 𝑉 → 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) )
7		eqeq2	⊢ ( 0 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( 𝐸 = 0 ↔ 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) ) )
8	7	imbi1d	⊢ ( 0 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = 0 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ↔ ( 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ) )
9		eqeq2	⊢ ( inf ( 𝐼 , ℝ , < ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( 𝐸 = inf ( 𝐼 , ℝ , < ) ↔ 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) ) )
10	9	imbi1d	⊢ ( inf ( 𝐼 , ℝ , < ) = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = inf ( 𝐼 , ℝ , < ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ↔ ( 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) ) )
11		orc	⊢ ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) )
12	11	expcom	⊢ ( 𝐼 = ∅ → ( 𝐸 = 0 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) )
13	12	adantl	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝐼 = ∅ ) → ( 𝐸 = 0 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) )
14		ssrab2	⊢ { 𝑦 ∈ ℕ ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑦 · 𝑥 ) = 0 } ⊆ ℕ
15		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
16	15	eqcomi	⊢ ( ℤ≥ ‘ 1 ) = ℕ
17	14 5 16	3sstr4i	⊢ 𝐼 ⊆ ( ℤ≥ ‘ 1 )
18		neqne	⊢ ( ¬ 𝐼 = ∅ → 𝐼 ≠ ∅ )
19	18	adantl	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ¬ 𝐼 = ∅ ) → 𝐼 ≠ ∅ )
20		infssuzcl	⊢ ( ( 𝐼 ⊆ ( ℤ≥ ‘ 1 ) ∧ 𝐼 ≠ ∅ ) → inf ( 𝐼 , ℝ , < ) ∈ 𝐼 )
21	17 19 20	sylancr	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ¬ 𝐼 = ∅ ) → inf ( 𝐼 , ℝ , < ) ∈ 𝐼 )
22		eleq1a	⊢ ( inf ( 𝐼 , ℝ , < ) ∈ 𝐼 → ( 𝐸 = inf ( 𝐼 , ℝ , < ) → 𝐸 ∈ 𝐼 ) )
23	21 22	syl	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ¬ 𝐼 = ∅ ) → ( 𝐸 = inf ( 𝐼 , ℝ , < ) → 𝐸 ∈ 𝐼 ) )
24		olc	⊢ ( 𝐸 ∈ 𝐼 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) )
25	23 24	syl6	⊢ ( ( 𝐺 ∈ 𝑉 ∧ ¬ 𝐼 = ∅ ) → ( 𝐸 = inf ( 𝐼 , ℝ , < ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) )
26	8 10 13 25	ifbothda	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐸 = if ( 𝐼 = ∅ , 0 , inf ( 𝐼 , ℝ , < ) ) → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) ) )
27	6 26	mpd	⊢ ( 𝐺 ∈ 𝑉 → ( ( 𝐸 = 0 ∧ 𝐼 = ∅ ) ∨ 𝐸 ∈ 𝐼 ) )