Metamath Proof Explorer

Theorem signstlen

Description: Length of the zero skipping sign 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 signstlen 
|- ( F e. Word RR -> ( # ` ( T ` F ) ) = ( # ` F ) )

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 ovex 
 |-  ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( F ` i ) ) ) ) e. _V
6 eqid 
 |-  ( n e. ( 0 ..^ ( # ` F ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( F ` i ) ) ) ) ) = ( n e. ( 0 ..^ ( # ` F ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( F ` i ) ) ) ) )
7 5 6 fnmpti 
 |-  ( n e. ( 0 ..^ ( # ` F ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( F ` i ) ) ) ) ) Fn ( 0 ..^ ( # ` F ) )
8 1 2 3 4 signstfv 
 |-  ( F e. Word RR -> ( T ` F ) = ( n e. ( 0 ..^ ( # ` F ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( F ` i ) ) ) ) ) )
9 8 fneq1d 
 |-  ( F e. Word RR -> ( ( T ` F ) Fn ( 0 ..^ ( # ` F ) ) <-> ( n e. ( 0 ..^ ( # ` F ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( F ` i ) ) ) ) ) Fn ( 0 ..^ ( # ` F ) ) ) )
10 7 9 mpbiri 
 |-  ( F e. Word RR -> ( T ` F ) Fn ( 0 ..^ ( # ` F ) ) )
11 hashfn 
 |-  ( ( T ` F ) Fn ( 0 ..^ ( # ` F ) ) -> ( # ` ( T ` F ) ) = ( # ` ( 0 ..^ ( # ` F ) ) ) )
12 10 11 syl 
 |-  ( F e. Word RR -> ( # ` ( T ` F ) ) = ( # ` ( 0 ..^ ( # ` F ) ) ) )
13 lencl 
 |-  ( F e. Word RR -> ( # ` F ) e. NN0 )
14 hashfzo0 
 |-  ( ( # ` F ) e. NN0 -> ( # ` ( 0 ..^ ( # ` F ) ) ) = ( # ` F ) )
15 13 14 syl 
 |-  ( F e. Word RR -> ( # ` ( 0 ..^ ( # ` F ) ) ) = ( # ` F ) )
16 12 15 eqtrd 
 |-  ( F e. Word RR -> ( # ` ( T ` F ) ) = ( # ` F ) )