Metamath Proof Explorer


Theorem signsvf0

Description: There is no change of sign in the empty word. (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 signsvf0 V = 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 wrd0 Word
6 1 2 3 4 signsvvfval Word V = j 1 ..^ if T j T j 1 1 0
7 5 6 ax-mp V = j 1 ..^ if T j T j 1 1 0
8 hash0 = 0
9 8 oveq2i 1 ..^ = 1 ..^ 0
10 0le1 0 1
11 1z 1
12 0z 0
13 fzon 1 0 0 1 1 ..^ 0 =
14 11 12 13 mp2an 0 1 1 ..^ 0 =
15 10 14 mpbi 1 ..^ 0 =
16 9 15 eqtri 1 ..^ =
17 16 sumeq1i j 1 ..^ if T j T j 1 1 0 = j if T j T j 1 1 0
18 sum0 j if T j T j 1 1 0 = 0
19 7 17 18 3eqtri V = 0