Metamath Proof Explorer

Theorem signstf0

Description: Sign of a single letter 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 signstf0 
|- ( K e. RR -> ( T ` <" K "> ) = <" ( 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 s1len 
 |-  ( # ` <" K "> ) = 1
6 5 oveq2i 
 |-  ( 0 ..^ ( # ` <" K "> ) ) = ( 0 ..^ 1 )
7 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
8 6 7 eqtri 
 |-  ( 0 ..^ ( # ` <" K "> ) ) = { 0 }
9 8 a1i 
 |-  ( K e. RR -> ( 0 ..^ ( # ` <" K "> ) ) = { 0 } )
10 simpr 
 |-  ( ( K e. RR /\ n e. ( 0 ..^ ( # ` <" K "> ) ) ) -> n e. ( 0 ..^ ( # ` <" K "> ) ) )
11 10 8 eleqtrdi 
 |-  ( ( K e. RR /\ n e. ( 0 ..^ ( # ` <" K "> ) ) ) -> n e. { 0 } )
12 velsn 
 |-  ( n e. { 0 } <-> n = 0 )
13 11 12 sylib 
 |-  ( ( K e. RR /\ n e. ( 0 ..^ ( # ` <" K "> ) ) ) -> n = 0 )
14 oveq2 
 |-  ( n = 0 -> ( 0 ... n ) = ( 0 ... 0 ) )
15 0z 
 |-  0 e. ZZ
16 fzsn 
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
17 15 16 ax-mp 
 |-  ( 0 ... 0 ) = { 0 }
18 14 17 eqtrdi 
 |-  ( n = 0 -> ( 0 ... n ) = { 0 } )
19 18 mpteq1d 
 |-  ( n = 0 -> ( i e. ( 0 ... n ) |-> ( sgn ` ( <" K "> ` i ) ) ) = ( i e. { 0 } |-> ( sgn ` ( <" K "> ` i ) ) ) )
20 19 oveq2d 
 |-  ( n = 0 -> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( <" K "> ` i ) ) ) ) = ( W gsum ( i e. { 0 } |-> ( sgn ` ( <" K "> ` i ) ) ) ) )
21 20 adantl 
 |-  ( ( K e. RR /\ n = 0 ) -> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( <" K "> ` i ) ) ) ) = ( W gsum ( i e. { 0 } |-> ( sgn ` ( <" K "> ` i ) ) ) ) )
22 1 2 signswmnd 
 |-  W e. Mnd
23 22 a1i 
 |-  ( K e. RR -> W e. Mnd )
24 0re 
 |-  0 e. RR
25 24 a1i 
 |-  ( K e. RR -> 0 e. RR )
26 s1fv 
 |-  ( K e. RR -> ( <" K "> ` 0 ) = K )
27 id 
 |-  ( K e. RR -> K e. RR )
28 26 27 eqeltrd 
 |-  ( K e. RR -> ( <" K "> ` 0 ) e. RR )
29 28 rexrd 
 |-  ( K e. RR -> ( <" K "> ` 0 ) e. RR* )
30 sgncl 
 |-  ( ( <" K "> ` 0 ) e. RR* -> ( sgn ` ( <" K "> ` 0 ) ) e. { -u 1 , 0 , 1 } )
31 29 30 syl 
 |-  ( K e. RR -> ( sgn ` ( <" K "> ` 0 ) ) e. { -u 1 , 0 , 1 } )
32 1 2 signswbase 
 |-  { -u 1 , 0 , 1 } = ( Base ` W )
33 2fveq3 
 |-  ( i = 0 -> ( sgn ` ( <" K "> ` i ) ) = ( sgn ` ( <" K "> ` 0 ) ) )
34 32 33 gsumsn 
 |-  ( ( W e. Mnd /\ 0 e. RR /\ ( sgn ` ( <" K "> ` 0 ) ) e. { -u 1 , 0 , 1 } ) -> ( W gsum ( i e. { 0 } |-> ( sgn ` ( <" K "> ` i ) ) ) ) = ( sgn ` ( <" K "> ` 0 ) ) )
35 23 25 31 34 syl3anc 
 |-  ( K e. RR -> ( W gsum ( i e. { 0 } |-> ( sgn ` ( <" K "> ` i ) ) ) ) = ( sgn ` ( <" K "> ` 0 ) ) )
36 35 adantr 
 |-  ( ( K e. RR /\ n = 0 ) -> ( W gsum ( i e. { 0 } |-> ( sgn ` ( <" K "> ` i ) ) ) ) = ( sgn ` ( <" K "> ` 0 ) ) )
37 26 fveq2d 
 |-  ( K e. RR -> ( sgn ` ( <" K "> ` 0 ) ) = ( sgn ` K ) )
38 37 adantr 
 |-  ( ( K e. RR /\ n = 0 ) -> ( sgn ` ( <" K "> ` 0 ) ) = ( sgn ` K ) )
39 21 36 38 3eqtrd 
 |-  ( ( K e. RR /\ n = 0 ) -> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( <" K "> ` i ) ) ) ) = ( sgn ` K ) )
40 13 39 syldan 
 |-  ( ( K e. RR /\ n e. ( 0 ..^ ( # ` <" K "> ) ) ) -> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( <" K "> ` i ) ) ) ) = ( sgn ` K ) )
41 9 40 mpteq12dva 
 |-  ( K e. RR -> ( n e. ( 0 ..^ ( # ` <" K "> ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( <" K "> ` i ) ) ) ) ) = ( n e. { 0 } |-> ( sgn ` K ) ) )
42 s1cl 
 |-  ( K e. RR -> <" K "> e. Word RR )
43 1 2 3 4 signstfv 
 |-  ( <" K "> e. Word RR -> ( T ` <" K "> ) = ( n e. ( 0 ..^ ( # ` <" K "> ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( <" K "> ` i ) ) ) ) ) )
44 42 43 syl 
 |-  ( K e. RR -> ( T ` <" K "> ) = ( n e. ( 0 ..^ ( # ` <" K "> ) ) |-> ( W gsum ( i e. ( 0 ... n ) |-> ( sgn ` ( <" K "> ` i ) ) ) ) ) )
45 sgnclre 
 |-  ( K e. RR -> ( sgn ` K ) e. RR )
46 s1val 
 |-  ( ( sgn ` K ) e. RR -> <" ( sgn ` K ) "> = { <. 0 , ( sgn ` K ) >. } )
47 45 46 syl 
 |-  ( K e. RR -> <" ( sgn ` K ) "> = { <. 0 , ( sgn ` K ) >. } )
48 fmptsn 
 |-  ( ( 0 e. RR /\ ( sgn ` K ) e. RR ) -> { <. 0 , ( sgn ` K ) >. } = ( n e. { 0 } |-> ( sgn ` K ) ) )
49 24 45 48 sylancr 
 |-  ( K e. RR -> { <. 0 , ( sgn ` K ) >. } = ( n e. { 0 } |-> ( sgn ` K ) ) )
50 47 49 eqtrd 
 |-  ( K e. RR -> <" ( sgn ` K ) "> = ( n e. { 0 } |-> ( sgn ` K ) ) )
51 41 44 50 3eqtr4d 
 |-  ( K e. RR -> ( T ` <" K "> ) = <" ( sgn ` K ) "> )