odlem1

Description: The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Stefan O'Rear, 5-Sep-2015) (Revised by AV, 5-Oct-2020)

	Ref	Expression
Hypotheses	odval.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odval.2	⊢ · = ( ._g ‘ 𝐺 )
	odval.3	⊢ 0 = ( 0_g ‘ 𝐺 )
	odval.4	⊢ 𝑂 = ( od ‘ 𝐺 )
	odval.i	⊢ 𝐼 = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 }
Assertion	odlem1	⊢ ( 𝐴 ∈ 𝑋 → ( ( ( 𝑂 ‘ 𝐴 ) = 0 ∧ 𝐼 = ∅ ) ∨ ( 𝑂 ‘ 𝐴 ) ∈ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		odval.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odval.2	⊢ · = ( ._g ‘ 𝐺 )
3		odval.3	⊢ 0 = ( 0_g ‘ 𝐺 )
4		odval.4	⊢ 𝑂 = ( od ‘ 𝐺 )
5		odval.i	⊢ 𝐼 = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 }
6	1 2 3 4 5	odval	⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) = 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 ∧ 𝐼 = ∅ ) ∨ ( 𝑂 ‘ 𝐴 ) ∈ 𝐼 ) )

Metamath Proof Explorer

Theorem odlem1

Proof