Metamath Proof Explorer

Theorem signswn0

Description: The zero-skipping operation propagages nonzeros. (Contributed by Thierry Arnoux, 11-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 signswn0 
|- ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ X =/= 0 ) -> ( X .+^ Y ) =/= 0 )

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 } ) /\ X =/= 0 ) -> ( X .+^ Y ) = if ( Y = 0 , X , Y ) )
5 neeq1 
 |-  ( X = if ( Y = 0 , X , Y ) -> ( X =/= 0 <-> if ( Y = 0 , X , Y ) =/= 0 ) )
6 neeq1 
 |-  ( Y = if ( Y = 0 , X , Y ) -> ( Y =/= 0 <-> if ( Y = 0 , X , Y ) =/= 0 ) )
7 simplr 
 |-  ( ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ X =/= 0 ) /\ Y = 0 ) -> X =/= 0 )
8 simpr 
 |-  ( ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ X =/= 0 ) /\ -. Y = 0 ) -> -. Y = 0 )
9 8 neqned 
 |-  ( ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ X =/= 0 ) /\ -. Y = 0 ) -> Y =/= 0 )
10 5 6 7 9 ifbothda 
 |-  ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ X =/= 0 ) -> if ( Y = 0 , X , Y ) =/= 0 )
11 4 10 eqnetrd 
 |-  ( ( ( X e. { -u 1 , 0 , 1 } /\ Y e. { -u 1 , 0 , 1 } ) /\ X =/= 0 ) -> ( X .+^ Y ) =/= 0 )