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 = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
signsv.w 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⟩ }
signsv.t 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓𝑖 ) ) ) ) ) )
signsv.v 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
Assertion signsvf0 ( 𝑉 ‘ ∅ ) = 0

Proof

Step Hyp Ref Expression
1 signsv.p = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2 signsv.w 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⟩ }
3 signsv.t 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓𝑖 ) ) ) ) ) )
4 signsv.v 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
5 wrd0 ∅ ∈ Word ℝ
6 1 2 3 4 signsvvfval ( ∅ ∈ Word ℝ → ( 𝑉 ‘ ∅ ) = Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ ∅ ) ) if ( ( ( 𝑇 ‘ ∅ ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ∅ ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
7 5 6 ax-mp ( 𝑉 ‘ ∅ ) = Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ ∅ ) ) if ( ( ( 𝑇 ‘ ∅ ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ∅ ) ‘ ( 𝑗 − 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 Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ ∅ ) ) if ( ( ( 𝑇 ‘ ∅ ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ∅ ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) = Σ 𝑗 ∈ ∅ if ( ( ( 𝑇 ‘ ∅ ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ∅ ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 )
18 sum0 Σ 𝑗 ∈ ∅ if ( ( ( 𝑇 ‘ ∅ ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ∅ ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) = 0
19 7 17 18 3eqtri ( 𝑉 ‘ ∅ ) = 0