Metamath Proof Explorer

Theorem signsvvf

Description: V is a function. (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 signsvvf 
|- V : Word RR --> NN0

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 fzofi 
 |-  ( 1 ..^ ( # ` f ) ) e. Fin
6 5 a1i 
 |-  ( f e. Word RR -> ( 1 ..^ ( # ` f ) ) e. Fin )
7 1nn0 
 |-  1 e. NN0
8 7 a1i 
 |-  ( ( ( f e. Word RR /\ j e. ( 1 ..^ ( # ` f ) ) ) /\ ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) ) -> 1 e. NN0 )
9 0nn0 
 |-  0 e. NN0
10 9 a1i 
 |-  ( ( ( f e. Word RR /\ j e. ( 1 ..^ ( # ` f ) ) ) /\ -. ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) ) -> 0 e. NN0 )
11 8 10 ifclda 
 |-  ( ( f e. Word RR /\ j e. ( 1 ..^ ( # ` f ) ) ) -> if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) e. NN0 )
12 6 11 fsumnn0cl 
 |-  ( f e. Word RR -> sum_ j e. ( 1 ..^ ( # ` f ) ) if ( ( ( T ` f ) ` j ) =/= ( ( T ` f ) ` ( j - 1 ) ) , 1 , 0 ) e. NN0 )
13 4 12 fmpti 
 |-  V : Word RR --> NN0