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	|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
	signsv.w	|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
	signsv.t	|- T = ( f e. Word RR |-> ( n e. ( 0 ..^ ( # ` f ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( f ` i ) ) ) ) ) )
	signsv.v	|- V = ( f e. Word RR |-> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )
	signs.h	|- H = ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> ) oFC x. C ) )
Assertion	signshwrd	|- ( ( F e. Word RR /\ C e. RR+ ) -> H e. Word RR )

Proof

Step	Hyp	Ref	Expression
1		signsv.p	|- .+^ = ( a e. { -u 1 , 0 , 1 } , b e. { -u 1 , 0 , 1 } |-> if ( b = 0 , a , b ) )
2		signsv.w	|- W = { <. ( Base ` ndx ) , { -u 1 , 0 , 1 } >. , <. ( +g ` ndx ) , .+^ >. }
3		signsv.t	|- T = ( f e. Word RR |-> ( n e. ( 0 ..^ ( # ` f ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( f ` i ) ) ) ) ) )
4		signsv.v	|- V = ( f e. Word RR |-> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) )
5		signs.h	|- H = ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> ) oFC x. C ) )
6	1 2 3 4 5	signshf	|- ( ( F e. Word RR /\ C e. RR+ ) -> H : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR )
7		iswrdi	|- ( H : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR -> H e. Word RR )
8	6 7	syl	|- ( ( F e. Word RR /\ C e. RR+ ) -> H e. Word RR )