Metamath Proof Explorer

Theorem signstres

Description: Restriction of a zero skipping sign to a subword. (Contributed by Thierry Arnoux, 11-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 signstres 
|- ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( ( T ` F ) |` ( 0 ..^ N ) ) = ( T ` ( F |` ( 0 ..^ 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 1 2 3 4 signstf 
 |-  ( F e. Word RR -> ( T ` F ) e. Word RR )
6 wrdf 
 |-  ( ( T ` F ) e. Word RR -> ( T ` F ) : ( 0 ..^ ( # ` ( T ` F ) ) ) --> RR )
7 ffn 
 |-  ( ( T ` F ) : ( 0 ..^ ( # ` ( T ` F ) ) ) --> RR -> ( T ` F ) Fn ( 0 ..^ ( # ` ( T ` F ) ) ) )
8 5 6 7 3syl 
 |-  ( F e. Word RR -> ( T ` F ) Fn ( 0 ..^ ( # ` ( T ` F ) ) ) )
9 1 2 3 4 signstlen 
 |-  ( F e. Word RR -> ( # ` ( T ` F ) ) = ( # ` F ) )
10 9 oveq2d 
 |-  ( F e. Word RR -> ( 0 ..^ ( # ` ( T ` F ) ) ) = ( 0 ..^ ( # ` F ) ) )
11 10 fneq2d 
 |-  ( F e. Word RR -> ( ( T ` F ) Fn ( 0 ..^ ( # ` ( T ` F ) ) ) <-> ( T ` F ) Fn ( 0 ..^ ( # ` F ) ) ) )
12 8 11 mpbid 
 |-  ( F e. Word RR -> ( T ` F ) Fn ( 0 ..^ ( # ` F ) ) )
13 fnresin 
 |-  ( ( T ` F ) Fn ( 0 ..^ ( # ` F ) ) -> ( ( T ` F ) |` ( 0 ..^ N ) ) Fn ( ( 0 ..^ ( # ` F ) ) i^i ( 0 ..^ N ) ) )
14 12 13 syl 
 |-  ( F e. Word RR -> ( ( T ` F ) |` ( 0 ..^ N ) ) Fn ( ( 0 ..^ ( # ` F ) ) i^i ( 0 ..^ N ) ) )
15 14 adantr 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( ( T ` F ) |` ( 0 ..^ N ) ) Fn ( ( 0 ..^ ( # ` F ) ) i^i ( 0 ..^ N ) ) )
16 elfzuz3 
 |-  ( N e. ( 0 ... ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` N ) )
17 fzoss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` N ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
18 16 17 syl 
 |-  ( N e. ( 0 ... ( # ` F ) ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
19 18 adantl 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) )
20 incom 
 |-  ( ( 0 ..^ N ) i^i ( 0 ..^ ( # ` F ) ) ) = ( ( 0 ..^ ( # ` F ) ) i^i ( 0 ..^ N ) )
21 dfss2 
 |-  ( ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) <-> ( ( 0 ..^ N ) i^i ( 0 ..^ ( # ` F ) ) ) = ( 0 ..^ N ) )
22 21 biimpi 
 |-  ( ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) -> ( ( 0 ..^ N ) i^i ( 0 ..^ ( # ` F ) ) ) = ( 0 ..^ N ) )
23 20 22 eqtr3id 
 |-  ( ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) -> ( ( 0 ..^ ( # ` F ) ) i^i ( 0 ..^ N ) ) = ( 0 ..^ N ) )
24 23 fneq2d 
 |-  ( ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) -> ( ( ( T ` F ) |` ( 0 ..^ N ) ) Fn ( ( 0 ..^ ( # ` F ) ) i^i ( 0 ..^ N ) ) <-> ( ( T ` F ) |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) ) )
25 19 24 syl 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( ( ( T ` F ) |` ( 0 ..^ N ) ) Fn ( ( 0 ..^ ( # ` F ) ) i^i ( 0 ..^ N ) ) <-> ( ( T ` F ) |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) ) )
26 15 25 mpbid 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( ( T ` F ) |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) )
27 wrdres 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) e. Word RR )
28 1 2 3 4 signstf 
 |-  ( ( F |` ( 0 ..^ N ) ) e. Word RR -> ( T ` ( F |` ( 0 ..^ N ) ) ) e. Word RR )
29 wrdf 
 |-  ( ( T ` ( F |` ( 0 ..^ N ) ) ) e. Word RR -> ( T ` ( F |` ( 0 ..^ N ) ) ) : ( 0 ..^ ( # ` ( T ` ( F |` ( 0 ..^ N ) ) ) ) ) --> RR )
30 ffn 
 |-  ( ( T ` ( F |` ( 0 ..^ N ) ) ) : ( 0 ..^ ( # ` ( T ` ( F |` ( 0 ..^ N ) ) ) ) ) --> RR -> ( T ` ( F |` ( 0 ..^ N ) ) ) Fn ( 0 ..^ ( # ` ( T ` ( F |` ( 0 ..^ N ) ) ) ) ) )
31 27 28 29 30 4syl 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( T ` ( F |` ( 0 ..^ N ) ) ) Fn ( 0 ..^ ( # ` ( T ` ( F |` ( 0 ..^ N ) ) ) ) ) )
32 1 2 3 4 signstlen 
 |-  ( ( F |` ( 0 ..^ N ) ) e. Word RR -> ( # ` ( T ` ( F |` ( 0 ..^ N ) ) ) ) = ( # ` ( F |` ( 0 ..^ N ) ) ) )
33 27 32 syl 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( T ` ( F |` ( 0 ..^ N ) ) ) ) = ( # ` ( F |` ( 0 ..^ N ) ) ) )
34 wrdfn 
 |-  ( F e. Word RR -> F Fn ( 0 ..^ ( # ` F ) ) )
35 fnssres 
 |-  ( ( F Fn ( 0 ..^ ( # ` F ) ) /\ ( 0 ..^ N ) C_ ( 0 ..^ ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) )
36 34 18 35 syl2an 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( F |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) )
37 hashfn 
 |-  ( ( F |` ( 0 ..^ N ) ) Fn ( 0 ..^ N ) -> ( # ` ( F |` ( 0 ..^ N ) ) ) = ( # ` ( 0 ..^ N ) ) )
38 36 37 syl 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F |` ( 0 ..^ N ) ) ) = ( # ` ( 0 ..^ N ) ) )
39 elfznn0 
 |-  ( N e. ( 0 ... ( # ` F ) ) -> N e. NN0 )
40 hashfzo0 
 |-  ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
41 39 40 syl 
 |-  ( N e. ( 0 ... ( # ` F ) ) -> ( # ` ( 0 ..^ N ) ) = N )
42 41 adantl 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( 0 ..^ N ) ) = N )
43 33 38 42 3eqtrd 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( T ` ( F |` ( 0 ..^ N ) ) ) ) = N )
44 43 oveq2d 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( 0 ..^ ( # ` ( T ` ( F |` ( 0 ..^ N ) ) ) ) ) = ( 0 ..^ N ) )
45 44 fneq2d 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( ( T ` ( F |` ( 0 ..^ N ) ) ) Fn ( 0 ..^ ( # ` ( T ` ( F |` ( 0 ..^ N ) ) ) ) ) <-> ( T ` ( F |` ( 0 ..^ N ) ) ) Fn ( 0 ..^ N ) ) )
46 31 45 mpbid 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( T ` ( F |` ( 0 ..^ N ) ) ) Fn ( 0 ..^ N ) )
47 fvres 
 |-  ( m e. ( 0 ..^ N ) -> ( ( ( T ` F ) |` ( 0 ..^ N ) ) ` m ) = ( ( T ` F ) ` m ) )
48 47 ad3antlr 
 |-  ( ( ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) /\ g e. Word RR ) /\ F = ( ( F |` ( 0 ..^ N ) ) ++ g ) ) -> ( ( ( T ` F ) |` ( 0 ..^ N ) ) ` m ) = ( ( T ` F ) ` m ) )
49 simpr 
 |-  ( ( ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) /\ g e. Word RR ) /\ F = ( ( F |` ( 0 ..^ N ) ) ++ g ) ) -> F = ( ( F |` ( 0 ..^ N ) ) ++ g ) )
50 49 fveq2d 
 |-  ( ( ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) /\ g e. Word RR ) /\ F = ( ( F |` ( 0 ..^ N ) ) ++ g ) ) -> ( T ` F ) = ( T ` ( ( F |` ( 0 ..^ N ) ) ++ g ) ) )
51 50 fveq1d 
 |-  ( ( ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) /\ g e. Word RR ) /\ F = ( ( F |` ( 0 ..^ N ) ) ++ g ) ) -> ( ( T ` F ) ` m ) = ( ( T ` ( ( F |` ( 0 ..^ N ) ) ++ g ) ) ` m ) )
52 27 ad3antrrr 
 |-  ( ( ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) /\ g e. Word RR ) /\ F = ( ( F |` ( 0 ..^ N ) ) ++ g ) ) -> ( F |` ( 0 ..^ N ) ) e. Word RR )
53 simplr 
 |-  ( ( ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) /\ g e. Word RR ) /\ F = ( ( F |` ( 0 ..^ N ) ) ++ g ) ) -> g e. Word RR )
54 38 42 eqtrd 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( # ` ( F |` ( 0 ..^ N ) ) ) = N )
55 54 oveq2d 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( 0 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) = ( 0 ..^ N ) )
56 55 eleq2d 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( m e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) <-> m e. ( 0 ..^ N ) ) )
57 56 biimpar 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) -> m e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) )
58 57 ad2antrr 
 |-  ( ( ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) /\ g e. Word RR ) /\ F = ( ( F |` ( 0 ..^ N ) ) ++ g ) ) -> m e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) )
59 1 2 3 4 signstfvc 
 |-  ( ( ( F |` ( 0 ..^ N ) ) e. Word RR /\ g e. Word RR /\ m e. ( 0 ..^ ( # ` ( F |` ( 0 ..^ N ) ) ) ) ) -> ( ( T ` ( ( F |` ( 0 ..^ N ) ) ++ g ) ) ` m ) = ( ( T ` ( F |` ( 0 ..^ N ) ) ) ` m ) )
60 52 53 58 59 syl3anc 
 |-  ( ( ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) /\ g e. Word RR ) /\ F = ( ( F |` ( 0 ..^ N ) ) ++ g ) ) -> ( ( T ` ( ( F |` ( 0 ..^ N ) ) ++ g ) ) ` m ) = ( ( T ` ( F |` ( 0 ..^ N ) ) ) ` m ) )
61 48 51 60 3eqtrd 
 |-  ( ( ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) /\ g e. Word RR ) /\ F = ( ( F |` ( 0 ..^ N ) ) ++ g ) ) -> ( ( ( T ` F ) |` ( 0 ..^ N ) ) ` m ) = ( ( T ` ( F |` ( 0 ..^ N ) ) ) ` m ) )
62 wrdsplex 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> E. g e. Word RR F = ( ( F |` ( 0 ..^ N ) ) ++ g ) )
63 62 adantr 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) -> E. g e. Word RR F = ( ( F |` ( 0 ..^ N ) ) ++ g ) )
64 61 63 r19.29a 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) /\ m e. ( 0 ..^ N ) ) -> ( ( ( T ` F ) |` ( 0 ..^ N ) ) ` m ) = ( ( T ` ( F |` ( 0 ..^ N ) ) ) ` m ) )
65 26 46 64 eqfnfvd 
 |-  ( ( F e. Word RR /\ N e. ( 0 ... ( # ` F ) ) ) -> ( ( T ` F ) |` ( 0 ..^ N ) ) = ( T ` ( F |` ( 0 ..^ N ) ) ) )