Metamath Proof Explorer

Theorem signstlen

Description: Length 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 signstlen ⊢ F ∈ Word ℝ → T ⁡ F = F

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 ovex ⊢ ∑ W i = 0 n sgn ⁡ F ⁡ i ∈ V
6 eqid ⊢ n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i = n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i
7 5 6 fnmpti ⊢ n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i Fn 0 ..^ F
8 1 2 3 4 signstfv ⊢ F ∈ Word ℝ → T ⁡ F = n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i
9 8 fneq1d ⊢ F ∈ Word ℝ → T ⁡ F Fn 0 ..^ F ↔ n ∈ 0 ..^ F ⟼ ∑ W i = 0 n sgn ⁡ F ⁡ i Fn 0 ..^ F
10 7 9 mpbiri ⊢ F ∈ Word ℝ → T ⁡ F Fn 0 ..^ F
11 hashfn ⊢ T ⁡ F Fn 0 ..^ F → T ⁡ F = 0 ..^ F
12 10 11 syl ⊢ F ∈ Word ℝ → T ⁡ F = 0 ..^ F
13 lencl ⊢ F ∈ Word ℝ → F ∈ ℕ 0
14 hashfzo0 ⊢ F ∈ ℕ 0 → 0 ..^ F = F
15 13 14 syl ⊢ F ∈ Word ℝ → 0 ..^ F = F
16 12 15 eqtrd ⊢ F ∈ Word ℝ → T ⁡ F = F