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 ) )