Metamath Proof Explorer


Theorem signsvvf

Description: V is a function. (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 signsvvf 𝑉 : Word ℝ ⟶ ℕ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 fzofi ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ∈ Fin
6 5 a1i ( 𝑓 ∈ Word ℝ → ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ∈ Fin )
7 1nn0 1 ∈ ℕ0
8 7 a1i ( ( ( 𝑓 ∈ Word ℝ ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑇𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇𝑓 ) ‘ ( 𝑗 − 1 ) ) ) → 1 ∈ ℕ0 )
9 0nn0 0 ∈ ℕ0
10 9 a1i ( ( ( 𝑓 ∈ Word ℝ ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ¬ ( ( 𝑇𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇𝑓 ) ‘ ( 𝑗 − 1 ) ) ) → 0 ∈ ℕ0 )
11 8 10 ifclda ( ( 𝑓 ∈ Word ℝ ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) → if ( ( ( 𝑇𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) ∈ ℕ0 )
12 6 11 fsumnn0cl ( 𝑓 ∈ Word ℝ → Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) ∈ ℕ0 )
13 4 12 fmpti 𝑉 : Word ℝ ⟶ ℕ0