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 |
|
signs.h |
|- H = ( ( <" 0 "> ++ F ) oF - ( ( F ++ <" 0 "> ) oFC x. C ) ) |
6 |
1 2 3 4 5
|
signshf |
|- ( ( F e. Word RR /\ C e. RR+ ) -> H : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR ) |
7 |
|
ffn |
|- ( H : ( 0 ..^ ( ( # ` F ) + 1 ) ) --> RR -> H Fn ( 0 ..^ ( ( # ` F ) + 1 ) ) ) |
8 |
|
hashfn |
|- ( H Fn ( 0 ..^ ( ( # ` F ) + 1 ) ) -> ( # ` H ) = ( # ` ( 0 ..^ ( ( # ` F ) + 1 ) ) ) ) |
9 |
6 7 8
|
3syl |
|- ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` H ) = ( # ` ( 0 ..^ ( ( # ` F ) + 1 ) ) ) ) |
10 |
|
lencl |
|- ( F e. Word RR -> ( # ` F ) e. NN0 ) |
11 |
10
|
adantr |
|- ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` F ) e. NN0 ) |
12 |
|
1nn0 |
|- 1 e. NN0 |
13 |
12
|
a1i |
|- ( ( F e. Word RR /\ C e. RR+ ) -> 1 e. NN0 ) |
14 |
11 13
|
nn0addcld |
|- ( ( F e. Word RR /\ C e. RR+ ) -> ( ( # ` F ) + 1 ) e. NN0 ) |
15 |
|
hashfzo0 |
|- ( ( ( # ` F ) + 1 ) e. NN0 -> ( # ` ( 0 ..^ ( ( # ` F ) + 1 ) ) ) = ( ( # ` F ) + 1 ) ) |
16 |
14 15
|
syl |
|- ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` ( 0 ..^ ( ( # ` F ) + 1 ) ) ) = ( ( # ` F ) + 1 ) ) |
17 |
9 16
|
eqtrd |
|- ( ( F e. Word RR /\ C e. RR+ ) -> ( # ` H ) = ( ( # ` F ) + 1 ) ) |