Metamath Proof Explorer

Theorem signshf

Description: H , corresponding to the word F multiplied by ( x - C ) , as a function. (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 signshf 
|- ( ( F e. Word RR /\ C e. RR+ ) -> H : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> 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 resubcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x - y ) e. RR )
7 6 adantl 
 |-  ( ( ( F e. Word RR /\ C e. RR+ ) /\ ( x e. RR /\ y e. RR ) ) -> ( x - y ) e. RR )
8 0re 
 |-  0 e. RR
9 s1cl 
 |-  ( 0 e. RR -> <" 0 "> e. Word RR )
10 8 9 ax-mp 
 |-  <" 0 "> e. Word RR
11 ccatcl 
 |-  ( ( <" 0 "> e. Word RR /\ F e. Word RR ) -> ( <" 0 "> ++ F ) e. Word RR )
12 10 11 mpan 
 |-  ( F e. Word RR -> ( <" 0 "> ++ F ) e. Word RR )
13 wrdf 
 |-  ( ( <" 0 "> ++ F ) e. Word RR -> ( <" 0 "> ++ F ) : ( 0 ..^ ( # ` ( <" 0 "> ++ F ) ) ) --> RR )
14 12 13 syl 
 |-  ( F e. Word RR -> ( <" 0 "> ++ F ) : ( 0 ..^ ( # ` ( <" 0 "> ++ F ) ) ) --> RR )
15 1cnd 
 |-  ( F e. Word RR -> 1 e. CC )
16 lencl 
 |-  ( F e. Word RR -> ( # ` F ) e. NN0 )
17 16 nn0cnd 
 |-  ( F e. Word RR -> ( # ` F ) e. CC )
18 ccatlen 
 |-  ( ( <" 0 "> e. Word RR /\ F e. Word RR ) -> ( # ` ( <" 0 "> ++ F ) ) = ( ( # ` <" 0 "> ) + ( # ` F ) ) )
19 10 18 mpan 
 |-  ( F e. Word RR -> ( # ` ( <" 0 "> ++ F ) ) = ( ( # ` <" 0 "> ) + ( # ` F ) ) )
20 s1len 
 |-  ( # ` <" 0 "> ) = 1
21 20 oveq1i 
 |-  ( ( # ` <" 0 "> ) + ( # ` F ) ) = ( 1 + ( # ` F ) )
22 19 21 eqtrdi 
 |-  ( F e. Word RR -> ( # ` ( <" 0 "> ++ F ) ) = ( 1 + ( # ` F ) ) )
23 15 17 22 comraddd 
 |-  ( F e. Word RR -> ( # ` ( <" 0 "> ++ F ) ) = ( ( # ` F ) + 1 ) )
24 23 oveq2d 
 |-  ( F e. Word RR -> ( 0 ..^ ( # ` ( <" 0 "> ++ F ) ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
25 24 feq2d 
 |-  ( F e. Word RR -> ( ( <" 0 "> ++ F ) : ( 0 ..^ ( # ` ( <" 0 "> ++ F ) ) ) --> RR <-> ( <" 0 "> ++ F ) : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR ) )
26 14 25 mpbid 
 |-  ( F e. Word RR -> ( <" 0 "> ++ F ) : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR )
27 26 adantr 
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( <" 0 "> ++ F ) : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR )
28 remulcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR )
29 28 adantl 
 |-  ( ( ( F e. Word RR /\ C e. RR+ ) /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
30 ccatcl 
 |-  ( ( F e. Word RR /\ <" 0 "> e. Word RR ) -> ( F ++ <" 0 "> ) e. Word RR )
31 10 30 mpan2 
 |-  ( F e. Word RR -> ( F ++ <" 0 "> ) e. Word RR )
32 wrdf 
 |-  ( ( F ++ <" 0 "> ) e. Word RR -> ( F ++ <" 0 "> ) : ( 0 ..^ ( # ` ( F ++ <" 0 "> ) ) ) --> RR )
33 31 32 syl 
 |-  ( F e. Word RR -> ( F ++ <" 0 "> ) : ( 0 ..^ ( # ` ( F ++ <" 0 "> ) ) ) --> RR )
34 ccatws1len 
 |-  ( F e. Word RR -> ( # ` ( F ++ <" 0 "> ) ) = ( ( # ` F ) + 1 ) )
35 34 oveq2d 
 |-  ( F e. Word RR -> ( 0 ..^ ( # ` ( F ++ <" 0 "> ) ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
36 35 feq2d 
 |-  ( F e. Word RR -> ( ( F ++ <" 0 "> ) : ( 0 ..^ ( # ` ( F ++ <" 0 "> ) ) ) --> RR <-> ( F ++ <" 0 "> ) : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR ) )
37 33 36 mpbid 
 |-  ( F e. Word RR -> ( F ++ <" 0 "> ) : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR )
38 37 adantr 
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( F ++ <" 0 "> ) : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR )
39 ovexd 
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( 0 ..^ ( ( # ` F ) + 1 ) ) e. _V )
40 rpre 
 |-  ( C e. RR+ -> C e. RR )
41 40 adantl 
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> C e. RR )
42 29 38 39 41 ofcf 
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( ( F ++ <" 0 "> ) oFC x. C ) : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR )
43 inidm 
 |-  ( ( 0 ..^ ( ( # ` F ) + 1 ) ) i^i ( 0 ..^ ( ( # ` F ) + 1 ) ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) )
44 7 27 42 39 39 43 off 
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> ) oFC x. C ) ) : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR )
45 5 feq1i 
 |-  ( H : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR <-> ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> ) oFC x. C ) ) : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR )
46 44 45 sylibr 
 |-  ( ( F e. Word RR /\ C e. RR+ ) -> H : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR )