Theorem signswrid

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	signswrid	|- ( X e. { -u 1 , 0 , 1 } -> ( X .+^ 0 ) = X )

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		c0ex	|- 0 e. _V
4	3	tpid2	|- 0 e. { -u 1 , 0 , 1 }
5	1	signspval	|- ( ( X e. { -u 1 , 0 , 1 } /\ 0 e. { -u 1 , 0 , 1 } ) -> ( X .+^ 0 ) = if ( 0 = 0 , X , 0 ) )
6	4 5	mpan2	|- ( X e. { -u 1 , 0 , 1 } -> ( X .+^ 0 ) = if ( 0 = 0 , X , 0 ) )
7		eqid	|- 0 = 0
8		iftrue	|- ( 0 = 0 -> if ( 0 = 0 , X , 0 ) = X )
9	7 8	mp1i	|- ( X e. { -u 1 , 0 , 1 } -> if ( 0 = 0 , X , 0 ) = X )
10	6 9	eqtrd	|- ( X e. { -u 1 , 0 , 1 } -> ( X .+^ 0 ) = X )