Metamath Proof Explorer


Theorem signshlen

Description: Length of H , corresponding to the word F multiplied by ( x - C ) . (Contributed by Thierry Arnoux, 14-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 ) )
signs.h
|- H = ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> ) oFC x. C ) )
Assertion signshlen
|- ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` H ) = ( ( # ` F ) + 1 ) )

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 ffn
 |-  ( H : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR -> H Fn ( 0 ..^ ( ( # ` F ) + 1 ) ) )
8 hashfn
 |-  ( H Fn ( 0 ..^ ( ( # ` F ) + 1 ) ) -> ( # ` H ) = ( # ` ( 0 ..^ ( ( # ` F ) + 1 ) ) ) )
9 6 7 8 3syl
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` H ) = ( # ` ( 0 ..^ ( ( # ` F ) + 1 ) ) ) )
10 lencl
 |-  ( F e. Word RR -> ( # ` F ) e. NN0 )
11 10 adantr
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` F ) e. NN0 )
12 1nn0
 |-  1 e. NN0
13 12 a1i
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> 1 e. NN0 )
14 11 13 nn0addcld
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( ( # ` F ) + 1 ) e. NN0 )
15 hashfzo0
 |-  ( ( ( # ` F ) + 1 ) e. NN0 -> ( # ` ( 0 ..^ ( ( # ` F ) + 1 ) ) ) = ( ( # ` F ) + 1 ) )
16 14 15 syl
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` ( 0 ..^ ( ( # ` F ) + 1 ) ) ) = ( ( # ` F ) + 1 ) )
17 9 16 eqtrd
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` H ) = ( ( # ` F ) + 1 ) )