Metamath Proof Explorer

Theorem abssval

Description: The value of surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Assertion abssval 
|- ( A e. No -> ( abs_s ` A ) = if ( 0s <_s A , A , ( -us ` A ) ) )

Proof

Step Hyp Ref Expression
1 df-abss 
 |-  abs_s = ( x e. No |-> if ( 0s <_s x , x , ( -us ` x ) ) )
2 breq2 
 |-  ( x = A -> ( 0s <_s x <-> 0s <_s A ) )
3 id 
 |-  ( x = A -> x = A )
4 fveq2 
 |-  ( x = A -> ( -us ` x ) = ( -us ` A ) )
5 2 3 4 ifbieq12d 
 |-  ( x = A -> if ( 0s <_s x , x , ( -us ` x ) ) = if ( 0s <_s A , A , ( -us ` A ) ) )
6 id 
 |-  ( A e. No -> A e. No )
7 negscl 
 |-  ( A e. No -> ( -us ` A ) e. No )
8 6 7 ifcld 
 |-  ( A e. No -> if ( 0s <_s A , A , ( -us ` A ) ) e. No )
9 1 5 6 8 fvmptd3 
 |-  ( A e. No -> ( abs_s ` A ) = if ( 0s <_s A , A , ( -us ` A ) ) )