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=BaseG
odval.2 ⊢·˙=⋅G
odval.3 ⊢0˙=0G
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=BaseG
2 odval.2 ⊢·˙=⋅G
3 odval.3 ⊢0˙=0G
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=ifI=∅0supIℝ<
7 eqeq2 ⊢0=ifI=∅0supIℝ<→O⁡A=0↔O⁡A=ifI=∅0supIℝ<
8 7 imbi1d ⊢0=ifI=∅0supIℝ<→O⁡A=0→O⁡A=0∧I=∅∨O⁡A∈I↔O⁡A=ifI=∅0supIℝ<→O⁡A=0∧I=∅∨O⁡A∈I
9 eqeq2 ⊢supIℝ<=ifI=∅0supIℝ<→O⁡A=supIℝ<↔O⁡A=ifI=∅0supIℝ<
10 9 imbi1d ⊢supIℝ<=ifI=∅0supIℝ<→O⁡A=supIℝ<→O⁡A=0∧I=∅∨O⁡A∈I↔O⁡A=ifI=∅0supIℝ<→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≠∅→supIℝ<∈I
21 17 19 20 sylancr ⊢A∈X∧¬I=∅→supIℝ<∈I
22 eleq1a ⊢supIℝ<∈I→O⁡A=supIℝ<→O⁡A∈I
23 21 22 syl ⊢A∈X∧¬I=∅→O⁡A=supIℝ<→O⁡A∈I
24 olc ⊢O⁡A∈I→O⁡A=0∧I=∅∨O⁡A∈I
25 23 24 syl6 ⊢A∈X∧¬I=∅→O⁡A=supIℝ<→O⁡A=0∧I=∅∨O⁡A∈I
26 8 10 13 25 ifbothda ⊢A∈X→O⁡A=ifI=∅0supIℝ<→O⁡A=0∧I=∅∨O⁡A∈I
27 6 26 mpd ⊢A∈X→O⁡A=0∧I=∅∨O⁡A∈I