Metamath Proof Explorer


Theorem signstfvcl

Description: Closure of the zero skipping sign in case the first letter is not zero. (Contributed by Thierry Arnoux, 10-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 signstfvcl
|- ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 1 } )

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 simpll
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> F e. ( Word RR \ { (/) } ) )
6 5 eldifad
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> F e. Word RR )
7 1 2 3 4 signstcl
 |-  ( ( F e. Word RR /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 0 , 1 } )
8 6 7 sylancom
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 0 , 1 } )
9 1 2 3 4 signstfvneq0
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) =/= 0 )
10 eldifsn
 |-  ( ( ( T ` F ) ` N ) e. ( { -u 1 , 0 , 1 } \ { 0 } ) <-> ( ( ( T ` F ) ` N ) e. { -u 1 , 0 , 1 } /\ ( ( T ` F ) ` N ) =/= 0 ) )
11 8 9 10 sylanbrc
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. ( { -u 1 , 0 , 1 } \ { 0 } ) )
12 tpcomb
 |-  { -u 1 , 0 , 1 } = { -u 1 , 1 , 0 }
13 12 difeq1i
 |-  ( { -u 1 , 0 , 1 } \ { 0 } ) = ( { -u 1 , 1 , 0 } \ { 0 } )
14 neg1ne0
 |-  -u 1 =/= 0
15 ax-1ne0
 |-  1 =/= 0
16 diftpsn3
 |-  ( ( -u 1 =/= 0 /\ 1 =/= 0 ) -> ( { -u 1 , 1 , 0 } \ { 0 } ) = { -u 1 , 1 } )
17 14 15 16 mp2an
 |-  ( { -u 1 , 1 , 0 } \ { 0 } ) = { -u 1 , 1 }
18 13 17 eqtri
 |-  ( { -u 1 , 0 , 1 } \ { 0 } ) = { -u 1 , 1 }
19 11 18 eleqtrdi
 |-  ( ( ( F e. ( Word RR \ { (/) } ) /\ ( F ` 0 ) =/= 0 ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> ( ( T ` F ) ` N ) e. { -u 1 , 1 } )