Metamath Proof Explorer

Theorem 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 ⊢ X = Base G
odval.2 ⊢ · ˙ = ⋅ G
odval.3 ⊢ 0 ˙ = 0 G
odval.4 ⊢ O = od ⁡ G
odval.i ⊢ I = y ∈ ℕ | y · ˙ A = 0 ˙
Assertion odlem1 ⊢ A ∈ X → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I

Proof

Step Hyp Ref Expression
1 odval.1 ⊢ X = Base G
2 odval.2 ⊢ · ˙ = ⋅ G
3 odval.3 ⊢ 0 ˙ = 0 G
4 odval.4 ⊢ O = od ⁡ G
5 odval.i ⊢ I = y ∈ ℕ | y · ˙ A = 0 ˙
6 1 2 3 4 5 odval ⊢ A ∈ X → O ⁡ A = if I = ∅ 0 inf I ℝ <
7 eqeq2 ⊢ 0 = if I = ∅ 0 inf I ℝ < → O ⁡ A = 0 ↔ O ⁡ A = if I = ∅ 0 inf I ℝ <
8 7 imbi1d ⊢ 0 = if I = ∅ 0 inf I ℝ < → O ⁡ A = 0 → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I ↔ O ⁡ A = if I = ∅ 0 inf I ℝ < → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I
9 eqeq2 ⊢ inf I ℝ < = if I = ∅ 0 inf I ℝ < → O ⁡ A = inf I ℝ < ↔ O ⁡ A = if I = ∅ 0 inf I ℝ <
10 9 imbi1d ⊢ inf I ℝ < = if I = ∅ 0 inf I ℝ < → O ⁡ A = inf I ℝ < → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I ↔ O ⁡ A = if I = ∅ 0 inf I ℝ < → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I
11 orc ⊢ O ⁡ A = 0 ∧ I = ∅ → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I
12 11 expcom ⊢ I = ∅ → O ⁡ A = 0 → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I
13 12 adantl ⊢ A ∈ X ∧ I = ∅ → O ⁡ A = 0 → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I
14 ssrab2 ⊢ y ∈ ℕ | y · ˙ A = 0 ˙ ⊆ ℕ
15 nnuz ⊢ ℕ = ℤ ≥ 1
16 15 eqcomi ⊢ ℤ ≥ 1 = ℕ
17 14 5 16 3sstr4i ⊢ I ⊆ ℤ ≥ 1
18 neqne ⊢ ¬ I = ∅ → I ≠ ∅
19 18 adantl ⊢ A ∈ X ∧ ¬ I = ∅ → I ≠ ∅
20 infssuzcl ⊢ I ⊆ ℤ ≥ 1 ∧ I ≠ ∅ → inf I ℝ < ∈ I
21 17 19 20 sylancr ⊢ A ∈ X ∧ ¬ I = ∅ → inf I ℝ < ∈ I
22 eleq1a ⊢ inf I ℝ < ∈ I → O ⁡ A = inf I ℝ < → O ⁡ A ∈ I
23 21 22 syl ⊢ A ∈ X ∧ ¬ I = ∅ → O ⁡ A = inf I ℝ < → O ⁡ A ∈ I
24 olc ⊢ O ⁡ A ∈ I → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I
25 23 24 syl6 ⊢ A ∈ X ∧ ¬ I = ∅ → O ⁡ A = inf I ℝ < → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I
26 8 10 13 25 ifbothda ⊢ A ∈ X → O ⁡ A = if I = ∅ 0 inf I ℝ < → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I
27 6 26 mpd ⊢ A ∈ X → O ⁡ A = 0 ∧ I = ∅ ∨ O ⁡ A ∈ I