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

Metamath Proof Explorer

Theorem odval

Description: Second substitution for the group order definition. (Contributed by Mario Carneiro, 13-Jul-2014) (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 odval 
|- ( A e. X -> ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )

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 oveq2 
 |-  ( x = A -> ( y .x. x ) = ( y .x. A ) )
7 6 eqeq1d 
 |-  ( x = A -> ( ( y .x. x ) = .0. <-> ( y .x. A ) = .0. ) )
8 7 rabbidv 
 |-  ( x = A -> { y e. NN | ( y .x. x ) = .0. } = { y e. NN | ( y .x. A ) = .0. } )
9 8 5 eqtr4di 
 |-  ( x = A -> { y e. NN | ( y .x. x ) = .0. } = I )
10 9 csbeq1d 
 |-  ( x = A -> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = [_ I / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
11 nnex 
 |-  NN e. _V
12 5 11 rabex2 
 |-  I e. _V
13 eqeq1 
 |-  ( i = I -> ( i = (/) <-> I = (/) ) )
14 infeq1 
 |-  ( i = I -> inf ( i , RR , < ) = inf ( I , RR , < ) )
15 13 14 ifbieq2d 
 |-  ( i = I -> if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )
16 12 15 csbie 
 |-  [_ I / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) )
17 10 16 eqtrdi 
 |-  ( x = A -> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )
18 1 2 3 4 odfval 
 |-  O = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
19 c0ex 
 |-  0 e. _V
20 ltso 
 |-  < Or RR
21 20 infex 
 |-  inf ( I , RR , < ) e. _V
22 19 21 ifex 
 |-  if ( I = (/) , 0 , inf ( I , RR , < ) ) e. _V
23 17 18 22 fvmpt 
 |-  ( A e. X -> ( O ` A ) = if ( I = (/) , 0 , inf ( I , RR , < ) ) )