Metamath Proof Explorer

Theorem signspval

Description: The value of the skipping 0 sign operation. (Contributed by Thierry Arnoux, 9-Sep-2018)

Ref Expression
Hypothesis signsw.p 
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
Assertion signspval 
|- ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( X .+^ Y ) = if ( Y = 0 , X , Y ) )

Proof

Step Hyp Ref Expression
1 signsw.p 
 |-  .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
2 ifcl 
 |-  ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> if ( Y = 0 , X , Y ) e. { -u 1 , 0 , 1 } )
3 ifeq1 
 |-  ( a = X -> if ( b = 0 , a , b ) = if ( b = 0 , X , b ) )
4 eqeq1 
 |-  ( b = Y -> ( b = 0 <-> Y = 0 ) )
5 id 
 |-  ( b = Y -> b = Y )
6 4 5 ifbieq2d 
 |-  ( b = Y -> if ( b = 0 , X , b ) = if ( Y = 0 , X , Y ) )
7 3 6 1 ovmpog 
 |-  ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } /\ if ( Y = 0 , X , Y ) e. { -u 1 , 0 , 1 } ) -> ( X .+^ Y ) = if ( Y = 0 , X , Y ) )
8 2 7 mpd3an3 
 |-  ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( X .+^ Y ) = if ( Y = 0 , X , Y ) )