Metamath Proof Explorer


Theorem signsvf1

Description: In a single-letter word, which represents a constant polynomial, there is no change of sign. (Contributed by Thierry Arnoux, 8-Oct-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 ) )
Assertion signsvf1
|- ( K e. RR -> ( V ` <" K "> ) = 0 )

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 s1cl
 |-  ( K e. RR -> <" K "> e. Word RR )
6 1 2 3 4 signsvvfval
 |-  ( <" K "> e. Word RR -> ( V ` <" K "> ) = sum_ j e. ( 1 ..^ ( # ` <" K "> ) ) if ( ( ( T ` <" K "> ) ` j ) =/= ( ( T ` <" K "> ) ` ( j - 1 ) ) , 1 , 0 ) )
7 5 6 syl
 |-  ( K e. RR -> ( V ` <" K "> ) = sum_ j e. ( 1 ..^ ( # ` <" K "> ) ) if ( ( ( T ` <" K "> ) ` j ) =/= ( ( T ` <" K "> ) ` ( j - 1 ) ) , 1 , 0 ) )
8 s1len
 |-  ( # ` <" K "> ) = 1
9 8 oveq2i
 |-  ( 1 ..^ ( # ` <" K "> ) ) = ( 1 ..^ 1 )
10 fzo0
 |-  ( 1 ..^ 1 ) = (/)
11 9 10 eqtri
 |-  ( 1 ..^ ( # ` <" K "> ) ) = (/)
12 11 sumeq1i
 |-  sum_ j e. ( 1 ..^ ( # ` <" K "> ) ) if ( ( ( T ` <" K "> ) ` j ) =/= ( ( T ` <" K "> ) ` ( j - 1 ) ) , 1 , 0 ) = sum_ j e. (/) if ( ( ( T ` <" K "> ) ` j ) =/= ( ( T ` <" K "> ) ` ( j - 1 ) ) , 1 , 0 )
13 sum0
 |-  sum_ j e. (/) if ( ( ( T ` <" K "> ) ` j ) =/= ( ( T ` <" K "> ) ` ( j - 1 ) ) , 1 , 0 ) = 0
14 12 13 eqtri
 |-  sum_ j e. ( 1 ..^ ( # ` <" K "> ) ) if ( ( ( T ` <" K "> ) ` j ) =/= ( ( T ` <" K "> ) ` ( j - 1 ) ) , 1 , 0 ) = 0
15 7 14 eqtrdi
 |-  ( K e. RR -> ( V ` <" K "> ) = 0 )