Theorem signsvvf

Description: V is a function. (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	signsvvf	$$⊢V:\mathrm{Word}ℝ⟶{\mathbb{N}}_0$$

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		fzofi	$$⊢\left(1..^\left|f\right|\right)\in \mathrm{Fin}$$
6	5	a1i	$$⊢f\in \mathrm{Word}ℝ\to \left(1..^\left|f\right|\right)\in \mathrm{Fin}$$
7		1nn0	$$⊢1\in {\mathbb{N}}_0$$
8	7	a1i	$$⊢\left(\left(f\in \mathrm{Word}ℝ\wedge j\in \left(1..^\left|f\right|\right)\right)\wedge T\left(f\right)\left(j\right)\ne T\left(f\right)\left(j-1\right)\right)\to 1\in {\mathbb{N}}_0$$
9		0nn0	$$⊢0\in {\mathbb{N}}_0$$
10	9	a1i	$$⊢\left(\left(f\in \mathrm{Word}ℝ\wedge j\in \left(1..^\left|f\right|\right)\right)\wedge \neg T\left(f\right)\left(j\right)\ne T\left(f\right)\left(j-1\right)\right)\to 0\in {\mathbb{N}}_0$$
11	8 10	ifclda	$$⊢\left(f\in \mathrm{Word}ℝ\wedge j\in \left(1..^\left|f\right|\right)\right)\to if\left(T\left(f\right)\left(j\right)\ne T\left(f\right)\left(j-1\right),1,0\right)\in {\mathbb{N}}_0$$
12	6 11	fsumnn0cl	$$⊢f\in \mathrm{Word}ℝ\to \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)\in {\mathbb{N}}_0$$
13	4 12	fmpti	$$⊢V:\mathrm{Word}ℝ⟶{\mathbb{N}}_0$$