Theorem signswlid

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

	Ref	Expression
Hypotheses	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)$$
	signsw.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{-1,0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
Assertion	signswlid	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge Y\ne 0\right)\to X\underset{\dot{}}{⨣}Y=Y$$

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		signsw.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{-1,0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
3	1	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)$$
4	3	adantr	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge Y\ne 0\right)\to X\underset{\dot{}}{⨣}Y=if\left(Y=0,X,Y\right)$$
5		simpr	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge Y\ne 0\right)\to Y\ne 0$$
6	5	neneqd	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge Y\ne 0\right)\to \neg Y=0$$
7	6	iffalsed	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge Y\ne 0\right)\to if\left(Y=0,X,Y\right)=Y$$
8	4 7	eqtrd	$$⊢\left(\left(X\in \left\{-1,0,1\right\}\wedge Y\in \left\{-1,0,1\right\}\right)\wedge Y\ne 0\right)\to X\underset{\dot{}}{⨣}Y=Y$$