Theorem signswrid

Description: The zero-skipping operation propagates nonzeros. (Contributed by Thierry Arnoux, 11-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	signswrid	$$⊢X\in \left\{-1,0,1\right\}\to X\underset{\dot{}}{⨣}0=X$$

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		c0ex	$$⊢0\in \mathrm{V}$$
4	3	tpid2	$$⊢0\in \left\{-1,0,1\right\}$$
5	1	signspval	$$⊢\left(X\in \left\{-1,0,1\right\}\wedge 0\in \left\{-1,0,1\right\}\right)\to X\underset{\dot{}}{⨣}0=if\left(0=0,X,0\right)$$
6	4 5	mpan2	$$⊢X\in \left\{-1,0,1\right\}\to X\underset{\dot{}}{⨣}0=if\left(0=0,X,0\right)$$
7		eqid	$$⊢0=0$$
8		iftrue	$$⊢0=0\to if\left(0=0,X,0\right)=X$$
9	7 8	mp1i	$$⊢X\in \left\{-1,0,1\right\}\to if\left(0=0,X,0\right)=X$$
10	6 9	eqtrd	$$⊢X\in \left\{-1,0,1\right\}\to X\underset{\dot{}}{⨣}0=X$$