Metamath Proof Explorer

Theorem gexval

Description: Value of the exponent of a group. (Contributed by Mario Carneiro, 23-Apr-2016) (Revised 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 gexval 
|- ( G e. V -> E = if ( I = (/) , 0 , inf ( I , RR , < ) ) )

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 df-gex 
 |-  gEx = ( g e. _V |-> [_ { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
7 nnex 
 |-  NN e. _V
8 7 rabex 
 |-  { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } e. _V
9 8 a1i 
 |-  ( ( G e. V /\ g = G ) -> { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } e. _V )
10 simpr 
 |-  ( ( G e. V /\ g = G ) -> g = G )
11 10 fveq2d 
 |-  ( ( G e. V /\ g = G ) -> ( Base ` g ) = ( Base ` G ) )
12 11 1 eqtr4di 
 |-  ( ( G e. V /\ g = G ) -> ( Base ` g ) = X )
13 10 fveq2d 
 |-  ( ( G e. V /\ g = G ) -> ( .g ` g ) = ( .g ` G ) )
14 13 2 eqtr4di 
 |-  ( ( G e. V /\ g = G ) -> ( .g ` g ) = .x. )
15 14 oveqd 
 |-  ( ( G e. V /\ g = G ) -> ( y ( .g ` g ) x ) = ( y .x. x ) )
16 10 fveq2d 
 |-  ( ( G e. V /\ g = G ) -> ( 0g ` g ) = ( 0g ` G ) )
17 16 3 eqtr4di 
 |-  ( ( G e. V /\ g = G ) -> ( 0g ` g ) = .0. )
18 15 17 eqeq12d 
 |-  ( ( G e. V /\ g = G ) -> ( ( y ( .g ` g ) x ) = ( 0g ` g ) <-> ( y .x. x ) = .0. ) )
19 12 18 raleqbidv 
 |-  ( ( G e. V /\ g = G ) -> ( A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) <-> A. x e. X ( y .x. x ) = .0. ) )
20 19 rabbidv 
 |-  ( ( G e. V /\ g = G ) -> { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } = { y e. NN | A. x e. X ( y .x. x ) = .0. } )
21 20 5 eqtr4di 
 |-  ( ( G e. V /\ g = G ) -> { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } = I )
22 21 eqeq2d 
 |-  ( ( G e. V /\ g = G ) -> ( i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } <-> i = I ) )
23 22 biimpa 
 |-  ( ( ( G e. V /\ g = G ) /\ i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } ) -> i = I )
24 23 eqeq1d 
 |-  ( ( ( G e. V /\ g = G ) /\ i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } ) -> ( i = (/) <-> I = (/) ) )
25 23 infeq1d 
 |-  ( ( ( G e. V /\ g = G ) /\ i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } ) -> inf ( i , RR , < ) = inf ( I , RR , < ) )
26 24 25 ifbieq2d 
 |-  ( ( ( G e. V /\ g = G ) /\ i = { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } ) -> if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )
27 9 26 csbied 
 |-  ( ( G e. V /\ g = G ) -> [_ { y e. NN | A. x e. ( Base ` g ) ( y ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )
28 elex 
 |-  ( G e. V -> G e. _V )
29 c0ex 
 |-  0 e. _V
30 ltso 
 |-  < Or RR
31 30 infex 
 |-  inf ( I , RR , < ) e. _V
32 29 31 ifex 
 |-  if ( I = (/) , 0 , inf ( I , RR , < ) ) e. _V
33 32 a1i 
 |-  ( G e. V -> if ( I = (/) , 0 , inf ( I , RR , < ) ) e. _V )
34 6 27 28 33 fvmptd2 
 |-  ( G e. V -> ( gEx ` G ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )
35 4 34 syl5eq 
 |-  ( G e. V -> E = if ( I = (/) , 0 , inf ( I , RR , < ) ) )