Metamath Proof Explorer

Theorem signswlid

Description: The zero-skipping operation keeps nonzeros. (Contributed by Thierry Arnoux, 12-Oct-2018)

Ref Expression
Hypotheses signsw.p 
|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
signsw.w 
|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
Assertion signswlid 
|- ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y =/= 0 ) -> ( X .+^ Y ) = 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 signsw.w 
 |-  W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
3 1 signspval 
 |-  ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) -> ( X .+^ Y ) = if ( Y = 0 , X , Y ) )
4 3 adantr 
 |-  ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y =/= 0 ) -> ( X .+^ Y ) = if ( Y = 0 , X , Y ) )
5 simpr 
 |-  ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y =/= 0 ) -> Y =/= 0 )
6 5 neneqd 
 |-  ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y =/= 0 ) -> -. Y = 0 )
7 6 iffalsed 
 |-  ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y =/= 0 ) -> if ( Y = 0 , X , Y ) = Y )
8 4 7 eqtrd 
 |-  ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ Y =/= 0 ) -> ( X .+^ Y ) = Y )