Theorem signspval

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

	Ref	Expression
Hypothesis	signsw.p	$$⊢\underset{\dot{}}{⨣}=\left(a\in \left\{-1,0,1\right\},b\in \left\{-1,0,1\right\}⟼if\left(b=0,a,b\right)\right)$$
Assertion	signspval	$$⊢\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\to X\underset{\dot{}}{⨣}Y=if\left(Y=0,X,Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		signsw.p	$$⊢\underset{\dot{}}{⨣}=\left(a\in \left\{-1,0,1\right\},b\in \left\{-1,0,1\right\}⟼if\left(b=0,a,b\right)\right)$$
2		ifcl	$$⊢\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\to if\left(Y=0,X,Y\right)\in \left\{-1,0,1\right\}$$
3		ifeq1	$$⊢a=X\to if\left(b=0,a,b\right)=if\left(b=0,X,b\right)$$
4		eqeq1	$$⊢b=Y\to \left(b=0\leftrightarrow Y=0\right)$$
5		id	$$⊢b=Y\to b=Y$$
6	4 5	ifbieq2d	$$⊢b=Y\to if\left(b=0,X,b\right)=if\left(Y=0,X,Y\right)$$
7	3 6 1	ovmpog	$$⊢\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\wedge if\left(Y=0,X,Y\right)\in \left\{-1,0,1\right\}\right)\to X\underset{\dot{}}{⨣}Y=if\left(Y=0,X,Y\right)$$
8	2 7	mpd3an3	$$⊢\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\to X\underset{\dot{}}{⨣}Y=if\left(Y=0,X,Y\right)$$