Metamath Proof Explorer

Theorem signsvfn

Description: Number of changes in a word compared to a shorter word. (Contributed by Thierry Arnoux, 12-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 signsvfn 
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( V ` ( F ++ <" K "> ) ) = ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 , 1 , 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 eldifi 
 |-  ( F e. ( Word RR \ { (/) } ) -> F e. Word RR )
6 s1cl 
 |-  ( K e. RR -> <" K "> e. Word RR )
7 ccatcl 
 |-  ( ( F e. Word RR /\ <" K "> e. Word RR ) -> ( F ++ <" K "> ) e. Word RR )
8 5 6 7 syl2an 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( F ++ <" K "> ) e. Word RR )
9 1 2 3 4 signsvvfval 
 |-  ( ( F ++ <" K "> ) e. Word RR -> ( V ` ( F ++ <" K "> ) ) = sum_ j e. ( 1 ..^ ( # ` ( F ++ <" K "> ) ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) )
10 8 9 syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( V ` ( F ++ <" K "> ) ) = sum_ j e. ( 1 ..^ ( # ` ( F ++ <" K "> ) ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) )
11 ccatlen 
 |-  ( ( F e. Word RR /\ <" K "> e. Word RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
12 5 6 11 syl2an 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
13 s1len 
 |-  ( # ` <" K "> ) = 1
14 13 oveq2i 
 |-  ( ( # ` F ) + ( # ` <" K "> ) ) = ( ( # ` F ) + 1 )
15 12 14 eqtrdi 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + 1 ) )
16 15 oveq2d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( 1 ..^ ( # ` ( F ++ <" K "> ) ) ) = ( 1 ..^ ( ( # ` F ) + 1 ) ) )
17 16 sumeq1d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> sum_ j e. ( 1 ..^ ( # ` ( F ++ <" K "> ) ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = sum_ j e. ( 1 ..^ ( ( # ` F ) + 1 ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) )
18 eldifsn 
 |-  ( F e. ( Word RR \ { (/) } ) <-> ( F e. Word RR /\ F =/= (/) ) )
19 lennncl 
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> ( # ` F ) e. NN )
20 18 19 sylbi 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( # ` F ) e. NN )
21 nnuz 
 |-  NN = ( ZZ>= ` 1 )
22 20 21 eleqtrdi 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( # ` F ) e. ( ZZ>= ` 1 ) )
23 22 adantr 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( # ` F ) e. ( ZZ>= ` 1 ) )
24 1cnd 
 |-  ( ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ... ( # ` F ) ) ) /\ ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) ) -> 1 e. CC )
25 0cnd 
 |-  ( ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ... ( # ` F ) ) ) /\ -. ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) ) -> 0 e. CC )
26 24 25 ifclda 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ... ( # ` F ) ) ) -> if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) e. CC )
27 fveq2 
 |-  ( j = ( # ` F ) -> ( ( T ` ( F ++ <" K "> ) ) ` j ) = ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) )
28 fvoveq1 
 |-  ( j = ( # ` F ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) = ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) )
29 27 28 neeq12d 
 |-  ( j = ( # ` F ) -> ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) <-> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) ) )
30 29 ifbid 
 |-  ( j = ( # ` F ) -> if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = if ( ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) )
31 23 26 30 fzosump1 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> sum_ j e. ( 1 ..^ ( ( # ` F ) + 1 ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = ( sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) + if ( ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) ) )
32 10 17 31 3eqtrd 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( V ` ( F ++ <" K "> ) ) = ( sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) + if ( ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) ) )
33 32 adantlr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( V ` ( F ++ <" K "> ) ) = ( sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) + if ( ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) ) )
34 simpl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> F e. ( Word RR \ { (/) } ) )
35 34 eldifad 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> F e. Word RR )
36 35 adantr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> F e. Word RR )
37 simplr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> K e. RR )
38 fzo0ss1 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) )
39 38 a1i 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) ) )
40 39 sselda 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> j e. ( 0 ..^ ( # ` F ) ) )
41 1 2 3 4 signstfvp 
 |-  ( ( F e. Word RR /\ K e. RR /\ j e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` j ) = ( ( T ` F ) ` j ) )
42 36 37 40 41 syl3anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` j ) = ( ( T ` F ) ` j ) )
43 elfzoel2 
 |-  ( j e. ( 1 ..^ ( # ` F ) ) -> ( # ` F ) e. ZZ )
44 43 adantl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> ( # ` F ) e. ZZ )
45 1nn0 
 |-  1 e. NN0
46 eluzmn 
 |-  ( ( ( # ` F ) e. ZZ /\ 1 e. NN0 ) -> ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) )
47 44 45 46 sylancl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) )
48 fzoss2 
 |-  ( ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
49 47 48 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> ( 0 ..^ ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` F ) ) )
50 elfzo1elm1fzo0 
 |-  ( j e. ( 1 ..^ ( # ` F ) ) -> ( j - 1 ) e. ( 0 ..^ ( ( # ` F ) - 1 ) ) )
51 50 adantl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> ( j - 1 ) e. ( 0 ..^ ( ( # ` F ) - 1 ) ) )
52 49 51 sseldd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> ( j - 1 ) e. ( 0 ..^ ( # ` F ) ) )
53 1 2 3 4 signstfvp 
 |-  ( ( F e. Word RR /\ K e. RR /\ ( j - 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) = ( ( T ` F ) ` ( j - 1 ) ) )
54 36 37 52 53 syl3anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) = ( ( T ` F ) ` ( j - 1 ) ) )
55 42 54 neeq12d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) <-> ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) ) )
56 55 ifbid 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ j e. ( 1 ..^ ( # ` F ) ) ) -> if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
57 56 sumeq2dv 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
58 1 2 3 4 signsvvfval 
 |-  ( F e. Word RR -> ( V ` F ) = sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
59 35 58 syl 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( V ` F ) = sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` F ) ` j ) =/= ( ( T ` F ) ` ( j - 1 ) ) , 1 , 0 ) )
60 57 59 eqtr4d 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = ( V ` F ) )
61 60 adantlr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) = ( V ` F ) )
62 1 2 3 4 signstfvn 
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) )
63 62 adantlr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) )
64 35 adantlr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> F e. Word RR )
65 simpr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> K e. RR )
66 fzo0end 
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
67 20 66 syl 
 |-  ( F e. ( Word RR \ { (/) } ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
68 67 ad2antrr 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
69 1 2 3 4 signstfvp 
 |-  ( ( F e. Word RR /\ K e. RR /\ ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) = ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) )
70 64 65 68 69 syl3anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) = ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) )
71 63 70 neeq12d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) =/= ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) )
72 1 2 3 4 signstfvcl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. { -u 1 , 1 } )
73 68 72 syldan 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. { -u 1 , 1 } )
74 rexr 
 |-  ( K e. RR -> K e. RR* )
75 sgncl 
 |-  ( K e. RR* -> ( sgn ` K ) e. { -u 1 , 0 , 1 } )
76 74 75 syl 
 |-  ( K e. RR -> ( sgn ` K ) e. { -u 1 , 0 , 1 } )
77 76 adantl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( sgn ` K ) e. { -u 1 , 0 , 1 } )
78 1 2 signswch 
 |-  ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. { -u 1 , 1 } /\ ( sgn ` K ) e. { -u 1 , 0 , 1 } ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) =/= ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. ( sgn ` K ) ) < 0 ) )
79 73 77 78 syl2anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) =/= ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. ( sgn ` K ) ) < 0 ) )
80 65 rexrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> K e. RR* )
81 sgnsgn 
 |-  ( K e. RR* -> ( sgn ` ( sgn ` K ) ) = ( sgn ` K ) )
82 80 81 syl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( sgn ` ( sgn ` K ) ) = ( sgn ` K ) )
83 82 oveq2d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. ( sgn ` ( sgn ` K ) ) ) = ( ( sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. ( sgn ` K ) ) )
84 83 breq1d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. ( sgn ` ( sgn ` K ) ) ) < 0 <-> ( ( sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. ( sgn ` K ) ) < 0 ) )
85 neg1rr 
 |-  -u 1 e. RR
86 1re 
 |-  1 e. RR
87 prssi 
 |-  ( ( -u 1 e. RR /\ 1 e. RR ) -> { -u 1 , 1 } C_ RR )
88 85 86 87 mp2an 
 |-  { -u 1 , 1 } C_ RR
89 88 73 sselid 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. RR )
90 sgnclre 
 |-  ( K e. RR -> ( sgn ` K ) e. RR )
91 90 adantl 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( sgn ` K ) e. RR )
92 sgnmulsgn 
 |-  ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. RR /\ ( sgn ` K ) e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. ( sgn ` K ) ) < 0 <-> ( ( sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. ( sgn ` ( sgn ` K ) ) ) < 0 ) )
93 89 91 92 syl2anc 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. ( sgn ` K ) ) < 0 <-> ( ( sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. ( sgn ` ( sgn ` K ) ) ) < 0 ) )
94 sgnmulsgn 
 |-  ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) e. RR /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 <-> ( ( sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. ( sgn ` K ) ) < 0 ) )
95 89 94 sylancom 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 <-> ( ( sgn ` ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) ) x. ( sgn ` K ) ) < 0 ) )
96 84 93 95 3bitr4d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. ( sgn ` K ) ) < 0 <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 ) )
97 71 79 96 3bitrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) <-> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 ) )
98 97 ifbid 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> if ( ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) = if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 , 1 , 0 ) )
99 61 98 oveq12d 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( sum_ j e. ( 1 ..^ ( # ` F ) ) if ( ( ( T ` ( F ++ <" K "> ) ) ` j ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( j - 1 ) ) , 1 , 0 ) + if ( ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) =/= ( ( T ` ( F ++ <" K "> ) ) ` ( ( # ` F ) - 1 ) ) , 1 , 0 ) ) = ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 , 1 , 0 ) ) )
100 33 99 eqtrd 
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ K e. RR ) -> ( V ` ( F ++ <" K "> ) ) = ( ( V ` F ) + if ( ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) x. K ) < 0 , 1 , 0 ) ) )