Metamath Proof Explorer

Theorem signstfv

Description: Value of the zero-skipping sign 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 signstfv ⊢ F ∈ Word ℝ → T ⁡ F = n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i

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 → 0 ..^ f = 0 ..^ F
7 simpl ⊢ f = F ∧ i ∈ 0 … n → f = F
8 7 fveq1d ⊢ f = F ∧ i ∈ 0 … n → f ⁡ i = F ⁡ i
9 8 fveq2d ⊢ f = F ∧ i ∈ 0 … n → sgn ⁡ f ⁡ i = sgn ⁡ F ⁡ i
10 9 mpteq2dva ⊢ f = F → i ∈ 0 … n ⟼ sgn ⁡ f ⁡ i = i ∈ 0 … n ⟼ sgn ⁡ F ⁡ i
11 10 oveq2d ⊢ f = F → ∑ W i = 0 n sgn ⁡ f ⁡ i = ∑ W i = 0 n sgn ⁡ F ⁡ i
12 6 11 mpteq12dv ⊢ f = F → n ∈ 0 ..^ f ⟼ ∑ W i = 0 n sgn ⁡ f ⁡ i = n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i
13 ovex ⊢ 0 ..^ F ∈ V
14 13 mptex ⊢ n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i ∈ V
15 12 3 14 fvmpt ⊢ F ∈ Word ℝ → T ⁡ F = n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i