Theorem signstfv

Description: Value of the zero-skipping sign word. (Contributed by Thierry Arnoux, 8-Oct-2018)

	Ref	Expression
Hypotheses	signsv.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)$$
	signsv.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{-1,0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
	signsv.t	$$⊢T=\left(f\in \mathrm{Word}ℝ⟼\left(n\in \left(0..^\left|f\right|\right)⟼\underset{i=0}{\overset{n}{{\sum }_W}}\mathrm{sgn}\left(f\left(i\right)\right)\right)\right)$$
	signsv.v	$$⊢V=\left(f\in \mathrm{Word}ℝ⟼\sum _{j\in \left(1..^\left|f\right|\right)}if\left(T\left(f\right)\left(j\right)\ne T\left(f\right)\left(j-1\right),1,0\right)\right)$$
Assertion	signstfv	$$⊢F\in \mathrm{Word}ℝ\to T\left(F\right)=\left(n\in \left(0..^\left|F\right|\right)⟼\underset{i=0}{\overset{n}{{\sum }_W}}\mathrm{sgn}\left(F\left(i\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		signsv.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		signsv.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{-1,0,1\right\}⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{⨣}⟩\right\}$$
3		signsv.t	$$⊢T=\left(f\in \mathrm{Word}ℝ⟼\left(n\in \left(0..^\left|f\right|\right)⟼\underset{i=0}{\overset{n}{{\sum }_W}}\mathrm{sgn}\left(f\left(i\right)\right)\right)\right)$$
4		signsv.v	$$⊢V=\left(f\in \mathrm{Word}ℝ⟼\sum _{j\in \left(1..^\left|f\right|\right)}if\left(T\left(f\right)\left(j\right)\ne T\left(f\right)\left(j-1\right),1,0\right)\right)$$
5		fveq2	$$⊢f=F\to \left|f\right|=\left|F\right|$$
6	5	oveq2d	$$⊢f=F\to \left(0..^\left|f\right|\right)=\left(0..^\left|F\right|\right)$$
7		simpl	$$⊢\left(f=F\wedge i\in \left(0\dots n\right)\right)\to f=F$$
8	7	fveq1d	$$⊢\left(f=F\wedge i\in \left(0\dots n\right)\right)\to f\left(i\right)=F\left(i\right)$$
9	8	fveq2d	$$⊢\left(f=F\wedge i\in \left(0\dots n\right)\right)\to \mathrm{sgn}\left(f\left(i\right)\right)=\mathrm{sgn}\left(F\left(i\right)\right)$$
10	9	mpteq2dva	$$⊢f=F\to \left(i\in \left(0\dots n\right)⟼\mathrm{sgn}\left(f\left(i\right)\right)\right)=\left(i\in \left(0\dots n\right)⟼\mathrm{sgn}\left(F\left(i\right)\right)\right)$$
11	10	oveq2d	$$⊢f=F\to \underset{i=0}{\overset{n}{{\sum }_W}}\mathrm{sgn}\left(f\left(i\right)\right)=\underset{i=0}{\overset{n}{{\sum }_W}}\mathrm{sgn}\left(F\left(i\right)\right)$$
12	6 11	mpteq12dv	$$⊢f=F\to \left(n\in \left(0..^\left|f\right|\right)⟼\underset{i=0}{\overset{n}{{\sum }_W}}\mathrm{sgn}\left(f\left(i\right)\right)\right)=\left(n\in \left(0..^\left|F\right|\right)⟼\underset{i=0}{\overset{n}{{\sum }_W}}\mathrm{sgn}\left(F\left(i\right)\right)\right)$$
13		ovex	$$⊢\left(0..^\left|F\right|\right)\in \mathrm{V}$$
14	13	mptex	$$⊢\left(n\in \left(0..^\left|F\right|\right)⟼\underset{i=0}{\overset{n}{{\sum }_W}}\mathrm{sgn}\left(F\left(i\right)\right)\right)\in \mathrm{V}$$
15	12 3 14	fvmpt	$$⊢F\in \mathrm{Word}ℝ\to T\left(F\right)=\left(n\in \left(0..^\left|F\right|\right)⟼\underset{i=0}{\overset{n}{{\sum }_W}}\mathrm{sgn}\left(F\left(i\right)\right)\right)$$