Metamath Proof Explorer

Theorem signsvvfval

Description: The value of V , which represents the number of times the sign changes in a word. (Contributed by Thierry Arnoux, 7-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 signsvvfval ⊢ F ∈ Word ℝ → V ⁡ F = ∑ j ∈ 1 ..^ F if T ⁡ F ⁡ j ≠ T ⁡ F ⁡ j − 1 1 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 fveq2 ⊢ f = F → f = F
6 5 oveq2d ⊢ f = F → 1 ..^ f = 1 ..^ F
7 fveq2 ⊢ f = F → T ⁡ f = T ⁡ F
8 7 fveq1d ⊢ f = F → T ⁡ f ⁡ j = T ⁡ F ⁡ j
9 7 fveq1d ⊢ f = F → T ⁡ f ⁡ j − 1 = T ⁡ F ⁡ j − 1
10 8 9 neeq12d ⊢ f = F → T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 ↔ T ⁡ F ⁡ j ≠ T ⁡ F ⁡ j − 1
11 10 ifbid ⊢ f = F → if T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 1 0 = if T ⁡ F ⁡ j ≠ T ⁡ F ⁡ j − 1 1 0
12 11 adantr ⊢ f = F ∧ j ∈ 1 ..^ f → if T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 1 0 = if T ⁡ F ⁡ j ≠ T ⁡ F ⁡ j − 1 1 0
13 6 12 sumeq12dv ⊢ f = F → ∑ j ∈ 1 ..^ f if T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 1 0 = ∑ j ∈ 1 ..^ F if T ⁡ F ⁡ j ≠ T ⁡ F ⁡ j − 1 1 0
14 sumex ⊢ ∑ j ∈ 1 ..^ F if T ⁡ F ⁡ j ≠ T ⁡ F ⁡ j − 1 1 0 ∈ V
15 13 4 14 fvmpt ⊢ F ∈ Word ℝ → V ⁡ F = ∑ j ∈ 1 ..^ F if T ⁡ F ⁡ j ≠ T ⁡ F ⁡ j − 1 1 0