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∈−101,b∈−101⟼ifb=0ab
signsv.w ⊢W=Basendx−101+ndx⨣˙
signsv.t ⊢T=f∈Wordℝ⟼n∈0..^f⟼∑Wi=0nsgn⁡f⁡i
signsv.v ⊢V=f∈Wordℝ⟼∑j∈1..^fifT⁡f⁡j≠T⁡f⁡j−110
Assertion signsvf0 ⊢V⁡∅=0

Proof

Step Hyp Ref Expression
1 signsv.p ⊢⨣˙=a∈−101,b∈−101⟼ifb=0ab
2 signsv.w ⊢W=Basendx−101+ndx⨣˙
3 signsv.t ⊢T=f∈Wordℝ⟼n∈0..^f⟼∑Wi=0nsgn⁡f⁡i
4 signsv.v ⊢V=f∈Wordℝ⟼∑j∈1..^fifT⁡f⁡j≠T⁡f⁡j−110
5 wrd0 ⊢∅∈Wordℝ
6 1 2 3 4 signsvvfval ⊢∅∈Wordℝ→V⁡∅=∑j∈1..^∅ifT⁡∅⁡j≠T⁡∅⁡j−110
7 5 6 ax-mp ⊢V⁡∅=∑j∈1..^∅ifT⁡∅⁡j≠T⁡∅⁡j−110
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..^∅ifT⁡∅⁡j≠T⁡∅⁡j−110=∑j∈∅ifT⁡∅⁡j≠T⁡∅⁡j−110
18 sum0 ⊢∑j∈∅ifT⁡∅⁡j≠T⁡∅⁡j−110=0
19 7 17 18 3eqtri ⊢V⁡∅=0