Metamath Proof Explorer

Theorem signstfvc

Description: Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 11-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 signstfvc 
|- ( ( F e. Word RR /\ G e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ G ) ) ` N ) = ( ( T ` F ) ` N ) )

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 oveq2 
 |-  ( g = (/) -> ( F ++ g ) = ( F ++ (/) ) )
6 5 fveq2d 
 |-  ( g = (/) -> ( T ` ( F ++ g ) ) = ( T ` ( F ++ (/) ) ) )
7 6 fveq1d 
 |-  ( g = (/) -> ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` ( F ++ (/) ) ) ` N ) )
8 7 eqeq1d 
 |-  ( g = (/) -> ( ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` F ) ` N ) <-> ( ( T ` ( F ++ (/) ) ) ` N ) = ( ( T ` F ) ` N ) ) )
9 8 imbi2d 
 |-  ( g = (/) -> ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` F ) ` N ) ) <-> ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ (/) ) ) ` N ) = ( ( T ` F ) ` N ) ) ) )
10 oveq2 
 |-  ( g = e -> ( F ++ g ) = ( F ++ e ) )
11 10 fveq2d 
 |-  ( g = e -> ( T ` ( F ++ g ) ) = ( T ` ( F ++ e ) ) )
12 11 fveq1d 
 |-  ( g = e -> ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` ( F ++ e ) ) ` N ) )
13 12 eqeq1d 
 |-  ( g = e -> ( ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` F ) ` N ) <-> ( ( T ` ( F ++ e ) ) ` N ) = ( ( T ` F ) ` N ) ) )
14 13 imbi2d 
 |-  ( g = e -> ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` F ) ` N ) ) <-> ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ e ) ) ` N ) = ( ( T ` F ) ` N ) ) ) )
15 oveq2 
 |-  ( g = ( e ++ <" k "> ) -> ( F ++ g ) = ( F ++ ( e ++ <" k "> ) ) )
16 15 fveq2d 
 |-  ( g = ( e ++ <" k "> ) -> ( T ` ( F ++ g ) ) = ( T ` ( F ++ ( e ++ <" k "> ) ) ) )
17 16 fveq1d 
 |-  ( g = ( e ++ <" k "> ) -> ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` ( F ++ ( e ++ <" k "> ) ) ) ` N ) )
18 17 eqeq1d 
 |-  ( g = ( e ++ <" k "> ) -> ( ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` F ) ` N ) <-> ( ( T ` ( F ++ ( e ++ <" k "> ) ) ) ` N ) = ( ( T ` F ) ` N ) ) )
19 18 imbi2d 
 |-  ( g = ( e ++ <" k "> ) -> ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` F ) ` N ) ) <-> ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ ( e ++ <" k "> ) ) ) ` N ) = ( ( T ` F ) ` N ) ) ) )
20 oveq2 
 |-  ( g = G -> ( F ++ g ) = ( F ++ G ) )
21 20 fveq2d 
 |-  ( g = G -> ( T ` ( F ++ g ) ) = ( T ` ( F ++ G ) ) )
22 21 fveq1d 
 |-  ( g = G -> ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` ( F ++ G ) ) ` N ) )
23 22 eqeq1d 
 |-  ( g = G -> ( ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` F ) ` N ) <-> ( ( T ` ( F ++ G ) ) ` N ) = ( ( T ` F ) ` N ) ) )
24 23 imbi2d 
 |-  ( g = G -> ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ g ) ) ` N ) = ( ( T ` F ) ` N ) ) <-> ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ G ) ) ` N ) = ( ( T ` F ) ` N ) ) ) )
25 ccatrid 
 |-  ( F e. Word RR -> ( F ++ (/) ) = F )
26 25 fveq2d 
 |-  ( F e. Word RR -> ( T ` ( F ++ (/) ) ) = ( T ` F ) )
27 26 fveq1d 
 |-  ( F e. Word RR -> ( ( T ` ( F ++ (/) ) ) ` N ) = ( ( T ` F ) ` N ) )
28 27 adantr 
 |-  ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ (/) ) ) ` N ) = ( ( T ` F ) ` N ) )
29 s1cl 
 |-  ( k e. RR -> <" k "> e. Word RR )
30 ccatass 
 |-  ( ( F e. Word RR /\ e e. Word RR /\ <" k "> e. Word RR ) -> ( ( F ++ e ) ++ <" k "> ) = ( F ++ ( e ++ <" k "> ) ) )
31 29 30 syl3an3 
 |-  ( ( F e. Word RR /\ e e. Word RR /\ k e. RR ) -> ( ( F ++ e ) ++ <" k "> ) = ( F ++ ( e ++ <" k "> ) ) )
32 31 3expb 
 |-  ( ( F e. Word RR /\ ( e e. Word RR /\ k e. RR ) ) -> ( ( F ++ e ) ++ <" k "> ) = ( F ++ ( e ++ <" k "> ) ) )
33 32 adantlr 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> ( ( F ++ e ) ++ <" k "> ) = ( F ++ ( e ++ <" k "> ) ) )
34 33 fveq2d 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> ( T ` ( ( F ++ e ) ++ <" k "> ) ) = ( T ` ( F ++ ( e ++ <" k "> ) ) ) )
35 34 fveq1d 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> ( ( T ` ( ( F ++ e ) ++ <" k "> ) ) ` N ) = ( ( T ` ( F ++ ( e ++ <" k "> ) ) ) ` N ) )
36 ccatcl 
 |-  ( ( F e. Word RR /\ e e. Word RR ) -> ( F ++ e ) e. Word RR )
37 36 ad2ant2r 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> ( F ++ e ) e. Word RR )
38 simprr 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> k e. RR )
39 lencl 
 |-  ( F e. Word RR -> ( # ` F ) e. NN0 )
40 39 nn0zd 
 |-  ( F e. Word RR -> ( # ` F ) e. ZZ )
41 40 adantr 
 |-  ( ( F e. Word RR /\ e e. Word RR ) -> ( # ` F ) e. ZZ )
42 lencl 
 |-  ( ( F ++ e ) e. Word RR -> ( # ` ( F ++ e ) ) e. NN0 )
43 36 42 syl 
 |-  ( ( F e. Word RR /\ e e. Word RR ) -> ( # ` ( F ++ e ) ) e. NN0 )
44 43 nn0zd 
 |-  ( ( F e. Word RR /\ e e. Word RR ) -> ( # ` ( F ++ e ) ) e. ZZ )
45 39 nn0red 
 |-  ( F e. Word RR -> ( # ` F ) e. RR )
46 lencl 
 |-  ( e e. Word RR -> ( # ` e ) e. NN0 )
47 nn0addge1 
 |-  ( ( ( # ` F ) e. RR /\ ( # ` e ) e. NN0 ) -> ( # ` F ) <_ ( ( # ` F ) + ( # ` e ) ) )
48 45 46 47 syl2an 
 |-  ( ( F e. Word RR /\ e e. Word RR ) -> ( # ` F ) <_ ( ( # ` F ) + ( # ` e ) ) )
49 ccatlen 
 |-  ( ( F e. Word RR /\ e e. Word RR ) -> ( # ` ( F ++ e ) ) = ( ( # ` F ) + ( # ` e ) ) )
50 48 49 breqtrrd 
 |-  ( ( F e. Word RR /\ e e. Word RR ) -> ( # ` F ) <_ ( # ` ( F ++ e ) ) )
51 eluz2 
 |-  ( ( # ` ( F ++ e ) ) e. ( ZZ>= ` ( # ` F ) ) <-> ( ( # ` F ) e. ZZ /\ ( # ` ( F ++ e ) ) e. ZZ /\ ( # ` F ) <_ ( # ` ( F ++ e ) ) ) )
52 41 44 50 51 syl3anbrc 
 |-  ( ( F e. Word RR /\ e e. Word RR ) -> ( # ` ( F ++ e ) ) e. ( ZZ>= ` ( # ` F ) ) )
53 fzoss2 
 |-  ( ( # ` ( F ++ e ) ) e. ( ZZ>= ` ( # ` F ) ) -> ( 0 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` ( F ++ e ) ) ) )
54 52 53 syl 
 |-  ( ( F e. Word RR /\ e e. Word RR ) -> ( 0 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` ( F ++ e ) ) ) )
55 54 ad2ant2r 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> ( 0 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` ( F ++ e ) ) ) )
56 simplr 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> N e. ( 0 ..^ ( # ` F ) ) )
57 55 56 sseldd 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> N e. ( 0 ..^ ( # ` ( F ++ e ) ) ) )
58 1 2 3 4 signstfvp 
 |-  ( ( ( F ++ e ) e. Word RR /\ k e. RR /\ N e. ( 0 ..^ ( # ` ( F ++ e ) ) ) ) -> ( ( T ` ( ( F ++ e ) ++ <" k "> ) ) ` N ) = ( ( T ` ( F ++ e ) ) ` N ) )
59 37 38 57 58 syl3anc 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> ( ( T ` ( ( F ++ e ) ++ <" k "> ) ) ` N ) = ( ( T ` ( F ++ e ) ) ` N ) )
60 35 59 eqtr3d 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> ( ( T ` ( F ++ ( e ++ <" k "> ) ) ) ` N ) = ( ( T ` ( F ++ e ) ) ` N ) )
61 id 
 |-  ( ( ( T ` ( F ++ e ) ) ` N ) = ( ( T ` F ) ` N ) -> ( ( T ` ( F ++ e ) ) ` N ) = ( ( T ` F ) ` N ) )
62 60 61 sylan9eq 
 |-  ( ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) /\ ( ( T ` ( F ++ e ) ) ` N ) = ( ( T ` F ) ` N ) ) -> ( ( T ` ( F ++ ( e ++ <" k "> ) ) ) ` N ) = ( ( T ` F ) ` N ) )
63 62 ex 
 |-  ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) /\ ( e e. Word RR /\ k e. RR ) ) -> ( ( ( T ` ( F ++ e ) ) ` N ) = ( ( T ` F ) ` N ) -> ( ( T ` ( F ++ ( e ++ <" k "> ) ) ) ` N ) = ( ( T ` F ) ` N ) ) )
64 63 expcom 
 |-  ( ( e e. Word RR /\ k e. RR ) -> ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( T ` ( F ++ e ) ) ` N ) = ( ( T ` F ) ` N ) -> ( ( T ` ( F ++ ( e ++ <" k "> ) ) ) ` N ) = ( ( T ` F ) ` N ) ) ) )
65 64 a2d 
 |-  ( ( e e. Word RR /\ k e. RR ) -> ( ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ e ) ) ` N ) = ( ( T ` F ) ` N ) ) -> ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ ( e ++ <" k "> ) ) ) ` N ) = ( ( T ` F ) ` N ) ) ) )
66 9 14 19 24 28 65 wrdind 
 |-  ( G e. Word RR -> ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ G ) ) ` N ) = ( ( T ` F ) ` N ) ) )
67 66 3impib 
 |-  ( ( G e. Word RR /\ F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ G ) ) ` N ) = ( ( T ` F ) ` N ) )
68 67 3com12 
 |-  ( ( F e. Word RR /\ G e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` ( F ++ G ) ) ` N ) = ( ( T ` F ) ` N ) )