Metamath Proof Explorer

Theorem signsvf0

Description: There is no change of sign in the empty 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 signsvf0 
|- ( V ` (/) ) = 0

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 wrd0 
 |-  (/) e. Word RR
6 1 2 3 4 signsvvfval 
 |-  ( (/) e. Word RR -> ( V ` (/) ) = sum_ j e. ( 1 ..^ ( # ` (/) ) ) if ( ( ( T ` (/) ) ` j ) =/= ( ( T ` (/) ) ` ( j - 1 ) ) , 1 , 0 ) )
7 5 6 ax-mp 
 |-  ( V ` (/) ) = sum_ j e. ( 1 ..^ ( # ` (/) ) ) if ( ( ( T ` (/) ) ` j ) =/= ( ( T ` (/) ) ` ( j - 1 ) ) , 1 , 0 )
8 hash0 
 |-  ( # ` (/) ) = 0
9 8 oveq2i 
 |-  ( 1 ..^ ( # ` (/) ) ) = ( 1 ..^ 0 )
10 0le1 
 |-  0 <_ 1
11 1z 
 |-  1 e. ZZ
12 0z 
 |-  0 e. ZZ
13 fzon 
 |-  ( ( 1 e. ZZ /\ 0 e. ZZ ) -> ( 0 <_ 1 <-> ( 1 ..^ 0 ) = (/) ) )
14 11 12 13 mp2an 
 |-  ( 0 <_ 1 <-> ( 1 ..^ 0 ) = (/) )
15 10 14 mpbi 
 |-  ( 1 ..^ 0 ) = (/)
16 9 15 eqtri 
 |-  ( 1 ..^ ( # ` (/) ) ) = (/)
17 16 sumeq1i 
 |-  sum_ j e. ( 1 ..^ ( # ` (/) ) ) if ( ( ( T ` (/) ) ` j ) =/= ( ( T ` (/) ) ` ( j - 1 ) ) , 1 , 0 ) = sum_ j e. (/) if ( ( ( T ` (/) ) ` j ) =/= ( ( T ` (/) ) ` ( j - 1 ) ) , 1 , 0 )
18 sum0 
 |-  sum_ j e. (/) if ( ( ( T ` (/) ) ` j ) =/= ( ( T ` (/) ) ` ( j - 1 ) ) , 1 , 0 ) = 0
19 7 17 18 3eqtri 
 |-  ( V ` (/) ) = 0