signstfval

Description: Value of the zero-skipping sign word. (Contributed by Thierry Arnoux, 8-Oct-2018)

	Ref	Expression
Hypotheses	signsv.p	$⊢ \underset{˙}{⨣} = (a \in \{- 1, 0, 1\}, b \in \{- 1, 0, 1\} ⟼ if (b = 0, a, b))$
	signsv.w	$⊢ W = \{⟨{Base}_{ndx}, \{- 1, 0, 1\}⟩, ⟨+_{ndx}, \underset{˙}{⨣}⟩\}$
	signsv.t	$⊢ T = (f \in Word ℝ ⟼ (n \in (0 ..^\|f\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (f (i))))$
	signsv.v	$⊢ V = (f \in Word ℝ ⟼ \sum_{j \in (1 ..^\|f\|)} if (T (f) (j) \neq T (f) (j - 1), 1, 0))$
Assertion	signstfval	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F) (N) = {\sum_{W}}_{i = 0}^{N} sgn (F (i))$

Step	Hyp	Ref	Expression
1		signsv.p	$⊢ \underset{˙}{⨣} = (a \in \{- 1, 0, 1\}, b \in \{- 1, 0, 1\} ⟼ if (b = 0, a, b))$
2		signsv.w	$⊢ W = \{⟨{Base}_{ndx}, \{- 1, 0, 1\}⟩, ⟨+_{ndx}, \underset{˙}{⨣}⟩\}$
3		signsv.t	$⊢ T = (f \in Word ℝ ⟼ (n \in (0 ..^\|f\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (f (i))))$
4		signsv.v	$⊢ V = (f \in Word ℝ ⟼ \sum_{j \in (1 ..^\|f\|)} if (T (f) (j) \neq T (f) (j - 1), 1, 0))$
5	1 2 3 4	signstfv	$⊢ F \in Word ℝ \to T (F) = (n \in (0 ..^\|F\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (F (i)))$
6	5	adantr	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F) = (n \in (0 ..^\|F\|) ⟼ {\sum_{W}}_{i = 0}^{n} sgn (F (i)))$
7		simpr	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land n = N) \to n = N$
8	7	oveq2d	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land n = N) \to (0 \dots n) = (0 \dots N)$
9	8	mpteq1d	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land n = N) \to (i \in (0 \dots n) ⟼ sgn (F (i))) = (i \in (0 \dots N) ⟼ sgn (F (i)))$
10	9	oveq2d	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land n = N) \to {\sum_{W}}_{i = 0}^{n} sgn (F (i)) = {\sum_{W}}_{i = 0}^{N} sgn (F (i))$
11		simpr	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to N \in (0 ..^\|F\|)$
12		ovexd	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to {\sum_{W}}_{i = 0}^{N} sgn (F (i)) \in V$
13	6 10 11 12	fvmptd	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F) (N) = {\sum_{W}}_{i = 0}^{N} sgn (F (i))$

Metamath Proof Explorer