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 
|- .x. = ( .g ` G )
odval.3 
|- .0. = ( 0g ` G )
odval.4 
|- O = ( od ` G )
odval.i 
|- I = { y e. NN | ( y .x. A ) = .0. }
Assertion odlem1 
|- ( A e. X -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) )

Proof

Step Hyp Ref Expression
1 odval.1 
 |-  X = ( Base ` G )
2 odval.2 
 |-  .x. = ( .g ` G )
3 odval.3 
 |-  .0. = ( 0g ` G )
4 odval.4 
 |-  O = ( od ` G )
5 odval.i 
 |-  I = { y e. NN | ( y .x. A ) = .0. }
6 1 2 3 4 5 odval 
 |-  ( A e. X -> ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )
7 eqeq2 
 |-  ( 0 = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( O ` A ) = 0 <-> ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) ) )
8 7 imbi1d 
 |-  ( 0 = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( ( O ` A ) = 0 -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) ) <-> ( ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) ) ) )
9 eqeq2 
 |-  ( inf ( I , RR , < ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( O ` A ) = inf ( I , RR , < ) <-> ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) ) )
10 9 imbi1d 
 |-  ( inf ( I , RR , < ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( ( O ` A ) = inf ( I , RR , < ) -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) ) <-> ( ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) ) ) )
11 orc 
 |-  ( ( ( O ` A ) = 0 /\ I = (/) ) -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) )
12 11 expcom 
 |-  ( I = (/) -> ( ( O ` A ) = 0 -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) ) )
13 12 adantl 
 |-  ( ( A e. X /\ I = (/) ) -> ( ( O ` A ) = 0 -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) ) )
14 ssrab2 
 |-  { y e. NN | ( y .x. A ) = .0. } C_ NN
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 15 eqcomi 
 |-  ( ZZ>= ` 1 ) = NN
17 14 5 16 3sstr4i 
 |-  I C_ ( ZZ>= ` 1 )
18 neqne 
 |-  ( -. I = (/) -> I =/= (/) )
19 18 adantl 
 |-  ( ( A e. X /\ -. I = (/) ) -> I =/= (/) )
20 infssuzcl 
 |-  ( ( I C_ ( ZZ>= ` 1 ) /\ I =/= (/) ) -> inf ( I , RR , < ) e. I )
21 17 19 20 sylancr 
 |-  ( ( A e. X /\ -. I = (/) ) -> inf ( I , RR , < ) e. I )
22 eleq1a 
 |-  ( inf ( I , RR , < ) e. I -> ( ( O ` A ) = inf ( I , RR , < ) -> ( O ` A ) e. I ) )
23 21 22 syl 
 |-  ( ( A e. X /\ -. I = (/) ) -> ( ( O ` A ) = inf ( I , RR , < ) -> ( O ` A ) e. I ) )
24 olc 
 |-  ( ( O ` A ) e. I -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) )
25 23 24 syl6 
 |-  ( ( A e. X /\ -. I = (/) ) -> ( ( O ` A ) = inf ( I , RR , < ) -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) ) )
26 8 10 13 25 ifbothda 
 |-  ( A e. X -> ( ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) ) )
27 6 26 mpd 
 |-  ( A e. X -> ( ( ( O ` A ) = 0 /\ I = (/) ) \/ ( O ` A ) e. I ) )