Metamath Proof Explorer


Theorem signsvf1

Description: In a single-letter word, which represents a constant polynomial, there is no change of sign. (Contributed by Thierry Arnoux, 8-Oct-2018)

Ref Expression
Hypotheses signsv.p ˙ = a 1 0 1 , b 1 0 1 if b = 0 a b
signsv.w W = Base ndx 1 0 1 + ndx ˙
signsv.t T = f Word n 0 ..^ f W i = 0 n sgn f i
signsv.v V = f Word j 1 ..^ f if T f j T f j 1 1 0
Assertion signsvf1 K V ⟨“ K ”⟩ = 0

Proof

Step Hyp Ref Expression
1 signsv.p ˙ = a 1 0 1 , b 1 0 1 if b = 0 a b
2 signsv.w W = Base ndx 1 0 1 + ndx ˙
3 signsv.t T = f Word n 0 ..^ f W i = 0 n sgn f i
4 signsv.v V = f Word j 1 ..^ f if T f j T f j 1 1 0
5 s1cl K ⟨“ K ”⟩ Word
6 1 2 3 4 signsvvfval ⟨“ K ”⟩ Word V ⟨“ K ”⟩ = j 1 ..^ ⟨“ K ”⟩ if T ⟨“ K ”⟩ j T ⟨“ K ”⟩ j 1 1 0
7 5 6 syl K V ⟨“ K ”⟩ = j 1 ..^ ⟨“ K ”⟩ if T ⟨“ K ”⟩ j T ⟨“ K ”⟩ j 1 1 0
8 s1len ⟨“ K ”⟩ = 1
9 8 oveq2i 1 ..^ ⟨“ K ”⟩ = 1 ..^ 1
10 fzo0 1 ..^ 1 =
11 9 10 eqtri 1 ..^ ⟨“ K ”⟩ =
12 11 sumeq1i j 1 ..^ ⟨“ K ”⟩ if T ⟨“ K ”⟩ j T ⟨“ K ”⟩ j 1 1 0 = j if T ⟨“ K ”⟩ j T ⟨“ K ”⟩ j 1 1 0
13 sum0 j if T ⟨“ K ”⟩ j T ⟨“ K ”⟩ j 1 1 0 = 0
14 12 13 eqtri j 1 ..^ ⟨“ K ”⟩ if T ⟨“ K ”⟩ j T ⟨“ K ”⟩ j 1 1 0 = 0
15 7 14 eqtrdi K V ⟨“ K ”⟩ = 0