signshlen

Description: Length of H , corresponding to the word F multiplied by ( x - C ) . (Contributed by Thierry Arnoux, 14-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))$
	signs.h	$⊢ H = (⟨“ 0 ”⟩ ++ F) -_{f} ((F ++ ⟨“ 0 ”⟩) \circ_{fc} \times C)$
Assertion	signshlen	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|H\| = \|F\| + 1$

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		signs.h	$⊢ H = (⟨“ 0 ”⟩ ++ F) -_{f} ((F ++ ⟨“ 0 ”⟩) \circ_{fc} \times C)$
6	1 2 3 4 5	signshf	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to H : (0 ..^\|F\| + 1) ⟶ ℝ$
7		ffn	$⊢ H : (0 ..^\|F\| + 1) ⟶ ℝ \to H Fn (0 ..^\|F\| + 1)$
8		hashfn	$⊢ H Fn (0 ..^\|F\| + 1) \to \|H\| = \|(0 ..^\|F\| + 1)\|$
9	6 7 8	3syl	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|H\| = \|(0 ..^\|F\| + 1)\|$
10		lencl	$⊢ F \in Word ℝ \to \|F\| \in ℕ_{0}$
11	10	adantr	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|F\| \in ℕ_{0}$
12		1nn0	$⊢ 1 \in ℕ_{0}$
13	12	a1i	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to 1 \in ℕ_{0}$
14	11 13	nn0addcld	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|F\| + 1 \in ℕ_{0}$
15		hashfzo0	$⊢ \|F\| + 1 \in ℕ_{0} \to \|(0 ..^\|F\| + 1)\| = \|F\| + 1$
16	14 15	syl	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|(0 ..^\|F\| + 1)\| = \|F\| + 1$
17	9 16	eqtrd	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to \|H\| = \|F\| + 1$

Metamath Proof Explorer