Theorem signshwrd

Description: H , corresponding to the word F multiplied by ( x - C ) , is a word. (Contributed by Thierry Arnoux, 29-Sep-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)$$
	signs.h	$$⊢H=\left(⟨“0”⟩\mathrm{++}F\right){-}_f\left(\left(F\mathrm{++}⟨“0”⟩\right){\circ }_{\mathrm{fc}}\times C\right)$$
Assertion	signshwrd	$$⊢\left(F\in \mathrm{Word}ℝ\wedge C\in {ℝ}^{+}\right)\to H\in \mathrm{Word}ℝ$$

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		signs.h	$$⊢H=\left(⟨“0”⟩\mathrm{++}F\right){-}_f\left(\left(F\mathrm{++}⟨“0”⟩\right){\circ }_{\mathrm{fc}}\times C\right)$$
6	1 2 3 4 5	signshf	$$⊢\left(F\in \mathrm{Word}ℝ\wedge C\in {ℝ}^{+}\right)\to H:\left(0..^\left|F\right|+1\right)⟶ℝ$$
7		iswrdi	$$⊢H:\left(0..^\left|F\right|+1\right)⟶ℝ\to H\in \mathrm{Word}ℝ$$
8	6 7	syl	$$⊢\left(F\in \mathrm{Word}ℝ\wedge C\in {ℝ}^{+}\right)\to H\in \mathrm{Word}ℝ$$