This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gexlem1

Description: The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 23-Apr-2016) (Proof shortened by AV, 26-Sep-2020)

Ref Expression
Hypotheses gexval.1 
|- X = ( Base ` G )
gexval.2 
|- .x. = ( .g ` G )
gexval.3 
|- .0. = ( 0g ` G )
gexval.4 
|- E = ( gEx ` G )
gexval.i 
|- I = { y e. NN | A. x e. X ( y .x. x ) = .0. }
Assertion gexlem1 
|- ( G e. V -> ( ( E = 0 /\ I = (/) ) \/ E e. I ) )

Proof

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