signshf

Description: H , corresponding to the word F multiplied by ( x - C ) , as a function. (Contributed by Thierry Arnoux, 29-Sep-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	signshf	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to H : (0 ..^\|F\| + 1) ⟶ ℝ$

Proof

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		resubcl	$⊢ (x \in ℝ \land y \in ℝ) \to x - y \in ℝ$
7	6	adantl	$⊢ ((F \in Word ℝ \land C \in ℝ^{+}) \land (x \in ℝ \land y \in ℝ)) \to x - y \in ℝ$
8		0re	$⊢ 0 \in ℝ$
9		s1cl	$⊢ 0 \in ℝ \to ⟨“ 0 ”⟩ \in Word ℝ$
10	8 9	ax-mp	$⊢ ⟨“ 0 ”⟩ \in Word ℝ$
11		ccatcl	$⊢ (⟨“ 0 ”⟩ \in Word ℝ \land F \in Word ℝ) \to ⟨“ 0 ”⟩ ++ F \in Word ℝ$
12	10 11	mpan	$⊢ F \in Word ℝ \to ⟨“ 0 ”⟩ ++ F \in Word ℝ$
13		wrdf	$⊢ ⟨“ 0 ”⟩ ++ F \in Word ℝ \to (⟨“ 0 ”⟩ ++ F) : (0 ..^\|⟨“ 0 ”⟩ ++ F\|) ⟶ ℝ$
14	12 13	syl	$⊢ F \in Word ℝ \to (⟨“ 0 ”⟩ ++ F) : (0 ..^\|⟨“ 0 ”⟩ ++ F\|) ⟶ ℝ$
15		1cnd	$⊢ F \in Word ℝ \to 1 \in ℂ$
16		lencl	$⊢ F \in Word ℝ \to \|F\| \in ℕ_{0}$
17	16	nn0cnd	$⊢ F \in Word ℝ \to \|F\| \in ℂ$
18		ccatlen	$⊢ (⟨“ 0 ”⟩ \in Word ℝ \land F \in Word ℝ) \to \|⟨“ 0 ”⟩ ++ F\| = \|⟨“ 0 ”⟩\| + \|F\|$
19	10 18	mpan	$⊢ F \in Word ℝ \to \|⟨“ 0 ”⟩ ++ F\| = \|⟨“ 0 ”⟩\| + \|F\|$
20		s1len	$⊢ \|⟨“ 0 ”⟩\| = 1$
21	20	oveq1i	$⊢ \|⟨“ 0 ”⟩\| + \|F\| = 1 + \|F\|$
22	19 21	eqtrdi	$⊢ F \in Word ℝ \to \|⟨“ 0 ”⟩ ++ F\| = 1 + \|F\|$
23	15 17 22	comraddd	$⊢ F \in Word ℝ \to \|⟨“ 0 ”⟩ ++ F\| = \|F\| + 1$
24	23	oveq2d	$⊢ F \in Word ℝ \to (0 ..^\|⟨“ 0 ”⟩ ++ F\|) = (0 ..^\|F\| + 1)$
25	24	feq2d	$⊢ F \in Word ℝ \to ((⟨“ 0 ”⟩ ++ F) : (0 ..^\|⟨“ 0 ”⟩ ++ F\|) ⟶ ℝ \leftrightarrow (⟨“ 0 ”⟩ ++ F) : (0 ..^\|F\| + 1) ⟶ ℝ)$
26	14 25	mpbid	$⊢ F \in Word ℝ \to (⟨“ 0 ”⟩ ++ F) : (0 ..^\|F\| + 1) ⟶ ℝ$
27	26	adantr	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to (⟨“ 0 ”⟩ ++ F) : (0 ..^\|F\| + 1) ⟶ ℝ$
28		remulcl	$⊢ (x \in ℝ \land y \in ℝ) \to x y \in ℝ$
29	28	adantl	$⊢ ((F \in Word ℝ \land C \in ℝ^{+}) \land (x \in ℝ \land y \in ℝ)) \to x y \in ℝ$
30		ccatcl	$⊢ (F \in Word ℝ \land ⟨“ 0 ”⟩ \in Word ℝ) \to F ++ ⟨“ 0 ”⟩ \in Word ℝ$
31	10 30	mpan2	$⊢ F \in Word ℝ \to F ++ ⟨“ 0 ”⟩ \in Word ℝ$
32		wrdf	$⊢ F ++ ⟨“ 0 ”⟩ \in Word ℝ \to (F ++ ⟨“ 0 ”⟩) : (0 ..^\|F ++ ⟨“ 0 ”⟩\|) ⟶ ℝ$
33	31 32	syl	$⊢ F \in Word ℝ \to (F ++ ⟨“ 0 ”⟩) : (0 ..^\|F ++ ⟨“ 0 ”⟩\|) ⟶ ℝ$
34		ccatws1len	$⊢ F \in Word ℝ \to \|F ++ ⟨“ 0 ”⟩\| = \|F\| + 1$
35	34	oveq2d	$⊢ F \in Word ℝ \to (0 ..^\|F ++ ⟨“ 0 ”⟩\|) = (0 ..^\|F\| + 1)$
36	35	feq2d	$⊢ F \in Word ℝ \to ((F ++ ⟨“ 0 ”⟩) : (0 ..^\|F ++ ⟨“ 0 ”⟩\|) ⟶ ℝ \leftrightarrow (F ++ ⟨“ 0 ”⟩) : (0 ..^\|F\| + 1) ⟶ ℝ)$
37	33 36	mpbid	$⊢ F \in Word ℝ \to (F ++ ⟨“ 0 ”⟩) : (0 ..^\|F\| + 1) ⟶ ℝ$
38	37	adantr	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to (F ++ ⟨“ 0 ”⟩) : (0 ..^\|F\| + 1) ⟶ ℝ$
39		ovexd	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to (0 ..^\|F\| + 1) \in V$
40		rpre	$⊢ C \in ℝ^{+} \to C \in ℝ$
41	40	adantl	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to C \in ℝ$
42	29 38 39 41	ofcf	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to ((F ++ ⟨“ 0 ”⟩) \circ_{fc} \times C) : (0 ..^\|F\| + 1) ⟶ ℝ$
43		inidm	$⊢ (0 ..^\|F\| + 1) \cap (0 ..^\|F\| + 1) = (0 ..^\|F\| + 1)$
44	7 27 42 39 39 43	off	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to ((⟨“ 0 ”⟩ ++ F) -_{f} ((F ++ ⟨“ 0 ”⟩) \circ_{fc} \times C)) : (0 ..^\|F\| + 1) ⟶ ℝ$
45	5	feq1i	$⊢ H : (0 ..^\|F\| + 1) ⟶ ℝ \leftrightarrow ((⟨“ 0 ”⟩ ++ F) -_{f} ((F ++ ⟨“ 0 ”⟩) \circ_{fc} \times C)) : (0 ..^\|F\| + 1) ⟶ ℝ$
46	44 45	sylibr	$⊢ (F \in Word ℝ \land C \in ℝ^{+}) \to H : (0 ..^\|F\| + 1) ⟶ ℝ$

Metamath Proof Explorer

Theorem signshf

Proof