Metamath Proof Explorer

Theorem signsvfpn

Description: Adding a letter of the same sign as the highest coefficient does not change the sign. (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 ) )
signsvf.e 
|- ( ph -> E e. ( Word RR \ { (/) } ) )
signsvf.0 
|- ( ph -> ( E ` 0 ) =/= 0 )
signsvf.f 
|- ( ph -> F = ( E ++ <" A "> ) )
signsvf.a 
|- ( ph -> A e. RR )
signsvf.n 
|- N = ( # ` E )
signsvf.b 
|- B = ( E ` ( N - 1 ) )
Assertion signsvfpn 
|- ( ( ph /\ 0 < ( B x. A ) ) -> ( V ` F ) = ( V ` E ) )

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 signsvf.e 
 |-  ( ph -> E e. ( Word RR \ { (/) } ) )
6 signsvf.0 
 |-  ( ph -> ( E ` 0 ) =/= 0 )
7 signsvf.f 
 |-  ( ph -> F = ( E ++ <" A "> ) )
8 signsvf.a 
 |-  ( ph -> A e. RR )
9 signsvf.n 
 |-  N = ( # ` E )
10 signsvf.b 
 |-  B = ( E ` ( N - 1 ) )
11 8 recnd 
 |-  ( ph -> A e. CC )
12 5 eldifad 
 |-  ( ph -> E e. Word RR )
13 wrdf 
 |-  ( E e. Word RR -> E : ( 0 ..^ ( # ` E ) ) --> RR )
14 12 13 syl 
 |-  ( ph -> E : ( 0 ..^ ( # ` E ) ) --> RR )
15 9 oveq1i 
 |-  ( N - 1 ) = ( ( # ` E ) - 1 )
16 eldifsn 
 |-  ( E e. ( Word RR \ { (/) } ) <-> ( E e. Word RR /\ E =/= (/) ) )
17 5 16 sylib 
 |-  ( ph -> ( E e. Word RR /\ E =/= (/) ) )
18 lennncl 
 |-  ( ( E e. Word RR /\ E =/= (/) ) -> ( # ` E ) e. NN )
19 fzo0end 
 |-  ( ( # ` E ) e. NN -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` E ) ) )
20 17 18 19 3syl 
 |-  ( ph -> ( ( # ` E ) - 1 ) e. ( 0 ..^ ( # ` E ) ) )
21 15 20 eqeltrid 
 |-  ( ph -> ( N - 1 ) e. ( 0 ..^ ( # ` E ) ) )
22 14 21 ffvelcdmd 
 |-  ( ph -> ( E ` ( N - 1 ) ) e. RR )
23 22 recnd 
 |-  ( ph -> ( E ` ( N - 1 ) ) e. CC )
24 10 23 eqeltrid 
 |-  ( ph -> B e. CC )
25 11 24 mulcomd 
 |-  ( ph -> ( A x. B ) = ( B x. A ) )
26 25 breq2d 
 |-  ( ph -> ( 0 < ( A x. B ) <-> 0 < ( B x. A ) ) )
27 10 22 eqeltrid 
 |-  ( ph -> B e. RR )
28 sgnmulsgp 
 |-  ( ( A e. RR /\ B e. RR ) -> ( 0 < ( A x. B ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) ) )
29 8 27 28 syl2anc 
 |-  ( ph -> ( 0 < ( A x. B ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) ) )
30 26 29 bitr3d 
 |-  ( ph -> ( 0 < ( B x. A ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) ) )
31 30 biimpa 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> 0 < ( ( sgn ` A ) x. ( sgn ` B ) ) )
32 5 adantr 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> E e. ( Word RR \ { (/) } ) )
33 24 adantr 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> B e. CC )
34 11 adantr 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> A e. CC )
35 simpr 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> 0 < ( B x. A ) )
36 35 gt0ne0d 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( B x. A ) =/= 0 )
37 33 34 36 mulne0bad 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> B =/= 0 )
38 10 37 eqnetrrid 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( E ` ( N - 1 ) ) =/= 0 )
39 1 2 3 4 9 signsvtn0 
 |-  ( ( E e. ( Word RR \ { (/) } ) /\ ( E ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` E ) ` ( N - 1 ) ) = ( sgn ` ( E ` ( N - 1 ) ) ) )
40 10 fveq2i 
 |-  ( sgn ` B ) = ( sgn ` ( E ` ( N - 1 ) ) )
41 39 40 eqtr4di 
 |-  ( ( E e. ( Word RR \ { (/) } ) /\ ( E ` ( N - 1 ) ) =/= 0 ) -> ( ( T ` E ) ` ( N - 1 ) ) = ( sgn ` B ) )
42 32 38 41 syl2anc 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( ( T ` E ) ` ( N - 1 ) ) = ( sgn ` B ) )
43 42 fveq2d 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) = ( sgn ` ( sgn ` B ) ) )
44 27 adantr 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> B e. RR )
45 44 rexrd 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> B e. RR* )
46 sgnsgn 
 |-  ( B e. RR* -> ( sgn ` ( sgn ` B ) ) = ( sgn ` B ) )
47 45 46 syl 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( sgn ` ( sgn ` B ) ) = ( sgn ` B ) )
48 43 47 eqtrd 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) = ( sgn ` B ) )
49 48 oveq2d 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) = ( ( sgn ` A ) x. ( sgn ` B ) ) )
50 31 49 breqtrrd 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> 0 < ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) )
51 8 adantr 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> A e. RR )
52 sgnclre 
 |-  ( B e. RR -> ( sgn ` B ) e. RR )
53 44 52 syl 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( sgn ` B ) e. RR )
54 42 53 eqeltrd 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( ( T ` E ) ` ( N - 1 ) ) e. RR )
55 sgnmulsgp 
 |-  ( ( A e. RR /\ ( ( T ` E ) ` ( N - 1 ) ) e. RR ) -> ( 0 < ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) ) )
56 51 54 55 syl2anc 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( 0 < ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) <-> 0 < ( ( sgn ` A ) x. ( sgn ` ( ( T ` E ) ` ( N - 1 ) ) ) ) ) )
57 50 56 mpbird 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> 0 < ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) )
58 eqid 
 |-  ( ( T ` E ) ` ( N - 1 ) ) = ( ( T ` E ) ` ( N - 1 ) )
59 1 2 3 4 5 6 7 8 9 58 signsvtp 
 |-  ( ( ph /\ 0 < ( A x. ( ( T ` E ) ` ( N - 1 ) ) ) ) -> ( V ` F ) = ( V ` E ) )
60 57 59 syldan 
 |-  ( ( ph /\ 0 < ( B x. A ) ) -> ( V ` F ) = ( V ` E ) )