Metamath Proof Explorer


Theorem signstfvn

Description: Zero-skipping sign in a word compared to a shorter 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 signstfvn
|- ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) )

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 1 2 signswbase
 |-  { -u 1 , 0 , 1 } = ( Base ` W )
6 1 2 signswmnd
 |-  W e. Mnd
7 6 a1i
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> W e. Mnd )
8 eldifi
 |-  ( F e. ( Word RR \ { (/) } ) -> F e. Word RR )
9 lencl
 |-  ( F e. Word RR -> ( # ` F ) e. NN0 )
10 8 9 syl
 |-  ( F e. ( Word RR \ { (/) } ) -> ( # ` F ) e. NN0 )
11 eldifsn
 |-  ( F e. ( Word RR \ { (/) } ) <-> ( F e. Word RR /\ F =/= (/) ) )
12 hasheq0
 |-  ( F e. Word RR -> ( ( # ` F ) = 0 <-> F = (/) ) )
13 12 necon3bid
 |-  ( F e. Word RR -> ( ( # ` F ) =/= 0 <-> F =/= (/) ) )
14 13 biimpar
 |-  ( ( F e. Word RR /\ F =/= (/) ) -> ( # ` F ) =/= 0 )
15 11 14 sylbi
 |-  ( F e. ( Word RR \ { (/) } ) -> ( # ` F ) =/= 0 )
16 elnnne0
 |-  ( ( # ` F ) e. NN <-> ( ( # ` F ) e. NN0 /\ ( # ` F ) =/= 0 ) )
17 10 15 16 sylanbrc
 |-  ( F e. ( Word RR \ { (/) } ) -> ( # ` F ) e. NN )
18 17 adantr
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( # ` F ) e. NN )
19 nnm1nn0
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. NN0 )
20 18 19 syl
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( # ` F ) - 1 ) e. NN0 )
21 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
22 20 21 eleqtrdi
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( # ` F ) - 1 ) e. ( ZZ>= ` 0 ) )
23 ccatws1cl
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( F ++ <" K "> ) e. Word RR )
24 23 adantr
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( F ++ <" K "> ) e. Word RR )
25 wrdf
 |-  ( ( F ++ <" K "> ) e. Word RR -> ( F ++ <" K "> ) : ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) --> RR )
26 24 25 syl
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( F ++ <" K "> ) : ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) --> RR )
27 9 nn0zd
 |-  ( F e. Word RR -> ( # ` F ) e. ZZ )
28 fzoval
 |-  ( ( # ` F ) e. ZZ -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
29 27 28 syl
 |-  ( F e. Word RR -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
30 29 adantr
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ... ( ( # ` F ) - 1 ) ) )
31 fzossfz
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
32 30 31 eqsstrrdi
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ... ( # ` F ) ) )
33 s1cl
 |-  ( K e. RR -> <" K "> e. Word RR )
34 ccatlen
 |-  ( ( F e. Word RR /\ <" K "> e. Word RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
35 33 34 sylan2
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + ( # ` <" K "> ) ) )
36 s1len
 |-  ( # ` <" K "> ) = 1
37 36 oveq2i
 |-  ( ( # ` F ) + ( # ` <" K "> ) ) = ( ( # ` F ) + 1 )
38 35 37 eqtrdi
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` ( F ++ <" K "> ) ) = ( ( # ` F ) + 1 ) )
39 38 oveq2d
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) = ( 0 ..^ ( ( # ` F ) + 1 ) ) )
40 27 adantr
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` F ) e. ZZ )
41 40 peano2zd
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( # ` F ) + 1 ) e. ZZ )
42 fzoval
 |-  ( ( ( # ` F ) + 1 ) e. ZZ -> ( 0 ..^ ( ( # ` F ) + 1 ) ) = ( 0 ... ( ( ( # ` F ) + 1 ) - 1 ) ) )
43 41 42 syl
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ..^ ( ( # ` F ) + 1 ) ) = ( 0 ... ( ( ( # ` F ) + 1 ) - 1 ) ) )
44 9 nn0cnd
 |-  ( F e. Word RR -> ( # ` F ) e. CC )
45 1cnd
 |-  ( F e. Word RR -> 1 e. CC )
46 44 45 pncand
 |-  ( F e. Word RR -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) )
47 46 adantr
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) )
48 47 oveq2d
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ... ( ( ( # ` F ) + 1 ) - 1 ) ) = ( 0 ... ( # ` F ) ) )
49 39 43 48 3eqtrd
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) = ( 0 ... ( # ` F ) ) )
50 32 49 sseqtrrd
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( 0 ... ( ( # ` F ) - 1 ) ) C_ ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) )
51 50 sselda
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) )
52 26 51 ffvelrnd
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( ( F ++ <" K "> ) ` i ) e. RR )
53 8 52 sylanl1
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( ( F ++ <" K "> ) ` i ) e. RR )
54 53 rexrd
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( ( F ++ <" K "> ) ` i ) e. RR* )
55 sgncl
 |-  ( ( ( F ++ <" K "> ) ` i ) e. RR* -> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) e. { -u 1 , 0 , 1 } )
56 54 55 syl
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) e. { -u 1 , 0 , 1 } )
57 1 2 signswplusg
 |-  .+^ = ( +g ` W )
58 rexr
 |-  ( K e. RR -> K e. RR* )
59 sgncl
 |-  ( K e. RR* -> ( sgn ` K ) e. { -u 1 , 0 , 1 } )
60 58 59 syl
 |-  ( K e. RR -> ( sgn ` K ) e. { -u 1 , 0 , 1 } )
61 60 adantl
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( sgn ` K ) e. { -u 1 , 0 , 1 } )
62 id
 |-  ( i = ( ( ( # ` F ) - 1 ) + 1 ) -> i = ( ( ( # ` F ) - 1 ) + 1 ) )
63 44 45 npcand
 |-  ( F e. Word RR -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
64 63 adantr
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
65 62 64 sylan9eqr
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> i = ( # ` F ) )
66 65 fveq2d
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( ( F ++ <" K "> ) ` i ) = ( ( F ++ <" K "> ) ` ( # ` F ) ) )
67 ccatws1ls
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( F ++ <" K "> ) ` ( # ` F ) ) = K )
68 67 adantr
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( ( F ++ <" K "> ) ` ( # ` F ) ) = K )
69 66 68 eqtrd
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( ( F ++ <" K "> ) ` i ) = K )
70 8 69 sylanl1
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( ( F ++ <" K "> ) ` i ) = K )
71 70 fveq2d
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) /\ i = ( ( ( # ` F ) - 1 ) + 1 ) ) -> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) = ( sgn ` K ) )
72 5 7 22 56 57 61 71 gsumnunsn
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( W gsum ( i e. ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) = ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) .+^ ( sgn ` K ) ) )
73 8 63 syl
 |-  ( F e. ( Word RR \ { (/) } ) -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
74 73 adantr
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( ( # ` F ) - 1 ) + 1 ) = ( # ` F ) )
75 74 oveq2d
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) ) = ( 0 ... ( # ` F ) ) )
76 75 mpteq1d
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( i e. ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) = ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) )
77 76 oveq2d
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( W gsum ( i e. ( 0 ... ( ( ( # ` F ) - 1 ) + 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) = ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
78 simpll
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> F e. Word RR )
79 33 ad2antlr
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> <" K "> e. Word RR )
80 30 eleq2d
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( i e. ( 0 ..^ ( # ` F ) ) <-> i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) )
81 80 biimpar
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` F ) ) )
82 ccatval1
 |-  ( ( F e. Word RR /\ <" K "> e. Word RR /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F ++ <" K "> ) ` i ) = ( F ` i ) )
83 78 79 81 82 syl3anc
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( ( F ++ <" K "> ) ` i ) = ( F ` i ) )
84 83 fveq2d
 |-  ( ( ( F e. Word RR /\ K e. RR ) /\ i e. ( 0 ... ( ( # ` F ) - 1 ) ) ) -> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) = ( sgn ` ( F ` i ) ) )
85 84 mpteq2dva
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) = ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) )
86 8 85 sylan
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) = ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) )
87 86 oveq2d
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) = ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) )
88 87 oveq1d
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) .+^ ( sgn ` K ) ) = ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) .+^ ( sgn ` K ) ) )
89 72 77 88 3eqtr3d
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) = ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) .+^ ( sgn ` K ) ) )
90 eqid
 |-  ( # ` F ) = ( # ` F )
91 90 olci
 |-  ( ( # ` F ) e. ( 0 ..^ ( # ` F ) ) \/ ( # ` F ) = ( # ` F ) )
92 9 21 eleqtrdi
 |-  ( F e. Word RR -> ( # ` F ) e. ( ZZ>= ` 0 ) )
93 fzosplitsni
 |-  ( ( # ` F ) e. ( ZZ>= ` 0 ) -> ( ( # ` F ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) <-> ( ( # ` F ) e. ( 0 ..^ ( # ` F ) ) \/ ( # ` F ) = ( # ` F ) ) ) )
94 92 93 syl
 |-  ( F e. Word RR -> ( ( # ` F ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) <-> ( ( # ` F ) e. ( 0 ..^ ( # ` F ) ) \/ ( # ` F ) = ( # ` F ) ) ) )
95 91 94 mpbiri
 |-  ( F e. Word RR -> ( # ` F ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) )
96 95 adantr
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` F ) e. ( 0 ..^ ( ( # ` F ) + 1 ) ) )
97 96 39 eleqtrrd
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( # ` F ) e. ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) )
98 1 2 3 4 signstfval
 |-  ( ( ( F ++ <" K "> ) e. Word RR /\ ( # ` F ) e. ( 0 ..^ ( # ` ( F ++ <" K "> ) ) ) ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
99 23 97 98 syl2anc
 |-  ( ( F e. Word RR /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
100 8 99 sylan
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( W gsum ( i e. ( 0 ... ( # ` F ) ) |-> ( sgn ` ( ( F ++ <" K "> ) ` i ) ) ) ) )
101 fzo0end
 |-  ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
102 17 101 syl
 |-  ( F e. ( Word RR \ { (/) } ) -> ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) )
103 1 2 3 4 signstfval
 |-  ( ( F e. Word RR /\ ( ( # ` F ) - 1 ) e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) = ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) )
104 8 102 103 syl2anc
 |-  ( F e. ( Word RR \ { (/) } ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) = ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) )
105 104 adantr
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) = ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) )
106 105 oveq1d
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) = ( ( W gsum ( i e. ( 0 ... ( ( # ` F ) - 1 ) ) |-> ( sgn ` ( F ` i ) ) ) ) .+^ ( sgn ` K ) ) )
107 89 100 106 3eqtr4d
 |-  ( ( F e. ( Word RR \ { (/) } ) /\ K e. RR ) -> ( ( T ` ( F ++ <" K "> ) ) ` ( # ` F ) ) = ( ( ( T ` F ) ` ( ( # ` F ) - 1 ) ) .+^ ( sgn ` K ) ) )