# 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}={\mathrm{Base}}_{{G}}$
odval.2
odval.3
odval.4 ${⊢}{O}=\mathrm{od}\left({G}\right)$
odval.i
Assertion odlem1 ${⊢}{A}\in {X}\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)$

### Proof

Step Hyp Ref Expression
1 odval.1 ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 odval.2
3 odval.3
4 odval.4 ${⊢}{O}=\mathrm{od}\left({G}\right)$
5 odval.i
6 1 2 3 4 5 odval ${⊢}{A}\in {X}\to {O}\left({A}\right)=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)$
7 eqeq2 ${⊢}0=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)\to \left({O}\left({A}\right)=0↔{O}\left({A}\right)=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)\right)$
8 7 imbi1d ${⊢}0=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)\to \left(\left({O}\left({A}\right)=0\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)\right)↔\left({O}\left({A}\right)=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)\right)\right)$
9 eqeq2 ${⊢}sup\left({I},ℝ,<\right)=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)\to \left({O}\left({A}\right)=sup\left({I},ℝ,<\right)↔{O}\left({A}\right)=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)\right)$
10 9 imbi1d ${⊢}sup\left({I},ℝ,<\right)=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)\to \left(\left({O}\left({A}\right)=sup\left({I},ℝ,<\right)\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)\right)↔\left({O}\left({A}\right)=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)\right)\right)$
11 orc ${⊢}\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)$
12 11 expcom ${⊢}{I}=\varnothing \to \left({O}\left({A}\right)=0\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)\right)$
13 12 adantl ${⊢}\left({A}\in {X}\wedge {I}=\varnothing \right)\to \left({O}\left({A}\right)=0\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)\right)$
14 ssrab2
15 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
16 15 eqcomi ${⊢}{ℤ}_{\ge 1}=ℕ$
17 14 5 16 3sstr4i ${⊢}{I}\subseteq {ℤ}_{\ge 1}$
18 neqne ${⊢}¬{I}=\varnothing \to {I}\ne \varnothing$
19 18 adantl ${⊢}\left({A}\in {X}\wedge ¬{I}=\varnothing \right)\to {I}\ne \varnothing$
20 infssuzcl ${⊢}\left({I}\subseteq {ℤ}_{\ge 1}\wedge {I}\ne \varnothing \right)\to sup\left({I},ℝ,<\right)\in {I}$
21 17 19 20 sylancr ${⊢}\left({A}\in {X}\wedge ¬{I}=\varnothing \right)\to sup\left({I},ℝ,<\right)\in {I}$
22 eleq1a ${⊢}sup\left({I},ℝ,<\right)\in {I}\to \left({O}\left({A}\right)=sup\left({I},ℝ,<\right)\to {O}\left({A}\right)\in {I}\right)$
23 21 22 syl ${⊢}\left({A}\in {X}\wedge ¬{I}=\varnothing \right)\to \left({O}\left({A}\right)=sup\left({I},ℝ,<\right)\to {O}\left({A}\right)\in {I}\right)$
24 olc ${⊢}{O}\left({A}\right)\in {I}\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)$
25 23 24 syl6 ${⊢}\left({A}\in {X}\wedge ¬{I}=\varnothing \right)\to \left({O}\left({A}\right)=sup\left({I},ℝ,<\right)\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)\right)$
26 8 10 13 25 ifbothda ${⊢}{A}\in {X}\to \left({O}\left({A}\right)=if\left({I}=\varnothing ,0,sup\left({I},ℝ,<\right)\right)\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)\right)$
27 6 26 mpd ${⊢}{A}\in {X}\to \left(\left({O}\left({A}\right)=0\wedge {I}=\varnothing \right)\vee {O}\left({A}\right)\in {I}\right)$