Metamath Proof Explorer

Theorem signstfvp

Description: Zero-skipping sign in a word compared to a shorter word. (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 signstfvp 
|- ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` N ) = ( ( T ` F ) ` N ) )

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 simpl1 
 |-  ( ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> F e. Word RR )
6 s1cl 
 |-  ( K e. RR -> <" K "> e. Word RR )
7 6 3ad2ant2 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> <" K "> e. Word RR )
8 7 adantr 
 |-  ( ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> <" K "> e. Word RR )
9 fzssfzo 
 |-  ( N e. ( 0 ..^ ( # ` F ) ) -> ( 0 ... N ) C_ ( 0 ..^ ( # ` F ) ) )
10 9 3ad2ant3 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( 0 ... N ) C_ ( 0 ..^ ( # ` F ) ) )
11 10 sselda 
 |-  ( ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> i e. ( 0 ..^ ( # ` F ) ) )
12 ccatval1 
 |-  ( ( F e. Word RR /\ <" K "> e. Word RR /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F ++ <" K "> ) ` i ) = ( F ` i ) )
13 5 8 11 12 syl3anc 
 |-  ( ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> ( ( F ++ <" K "> ) ` i ) = ( F ` i ) )
14 13 fveq2d 
 |-  ( ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ i e. ( 0 ... N ) ) -> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) = ( sgn ` ( F ` i ) ) )
15 14 mpteq2dva 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( i e. ( 0 ... N ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) = ( i e. ( 0 ... N ) |-> ( sgn ` ( F ` i ) ) ) )
16 15 oveq2d 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( W gsum ( i e. ( 0 ... N ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) = ( W gsum ( i e. ( 0 ... N ) |-> ( sgn ` ( F ` i ) ) ) ) )
17 ccatws1cl 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( F ++ <" K "> ) e. Word RR )
18 17 3adant3 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( F ++ <" K "> ) e. Word RR )
19 lencl 
 |-  ( F e. Word RR -> ( # ` F ) e. NN0 )
20 19 nn0zd 
 |-  ( F e. Word RR -> ( # ` F ) e. ZZ )
21 20 uzidd 
 |-  ( F e. Word RR -> ( # ` F ) e. ( ZZ>= ` ( # ` F ) ) )
22 peano2uz 
 |-  ( ( # ` F ) e. ( ZZ>= ` ( # ` F ) ) -> ( ( # ` F ) + 1 ) e. ( ZZ>= ` ( # ` F ) ) )
23 fzoss2 
 |-  ( ( ( # ` F ) + 1 ) e. ( ZZ>= ` ( # ` F ) ) -> ( 0 ..^ ( # ` F ) ) C_ ( 0 ..^ ( ( # ` F ) + 1 ) ) )
24 21 22 23 3syl 
 |-  ( F e. Word RR -> ( 0 ..^ ( # ` F ) ) C_ ( 0 ..^ ( ( # ` F ) + 1 ) ) )
25 24 sselda 
 |-  ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> N e. ( 0 ..^ ( ( # ` F ) + 1 ) ) )
26 25 3adant2 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> N e. ( 0 ..^ ( ( # ` F ) + 1 ) ) )
27 ccatlen 
 |-  ( ( F e. Word RR /\ <" K "> e. Word RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
28 6 27 sylan2 
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
29 28 3adant3 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
30 s1len 
 |-  ( # ` <" K "> ) = 1
31 30 oveq2i 
 |-  ( ( # ` F ) + ( # ` <" K "> ) ) = ( ( # ` F ) + 1 )
32 29 31 eqtrdi 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + 1 ) )
33 32 oveq2d 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
34 26 33 eleqtrrd 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> N e. ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) )
35 1 2 3 4 signstfval 
 |-  ( ( ( F ++ <" K "> ) e. Word RR /\ N e. ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` N ) = ( W gsum ( i e. ( 0 ... N ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
36 18 34 35 syl2anc 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` N ) = ( W gsum ( i e. ( 0 ... N ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
37 1 2 3 4 signstfval 
 |-  ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) = ( W gsum ( i e. ( 0 ... N ) |-> ( sgn ` ( F ` i ) ) ) ) )
38 37 3adant2 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) = ( W gsum ( i e. ( 0 ... N ) |-> ( sgn ` ( F ` i ) ) ) ) )
39 16 36 38 3eqtr4d 
 |-  ( ( F e. Word RR /\ K e. RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` N ) = ( ( T ` F ) ` N ) )