signstres

Description: Restriction of a zero skipping sign to a subword. (Contributed by Thierry Arnoux, 11-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	signstres	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to {T (F) ↾}_{(0 ..^N)} = T ({F ↾}_{(0 ..^N)})$

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	1 2 3 4	signstf	$⊢ F \in Word ℝ \to T (F) \in Word ℝ$
6		wrdf	$⊢ T (F) \in Word ℝ \to T (F) : (0 ..^\|T (F)\|) ⟶ ℝ$
7		ffn	$⊢ T (F) : (0 ..^\|T (F)\|) ⟶ ℝ \to T (F) Fn (0 ..^\|T (F)\|)$
8	5 6 7	3syl	$⊢ F \in Word ℝ \to T (F) Fn (0 ..^\|T (F)\|)$
9	1 2 3 4	signstlen	$⊢ F \in Word ℝ \to \|T (F)\| = \|F\|$
10	9	oveq2d	$⊢ F \in Word ℝ \to (0 ..^\|T (F)\|) = (0 ..^\|F\|)$
11	10	fneq2d	$⊢ F \in Word ℝ \to (T (F) Fn (0 ..^\|T (F)\|) \leftrightarrow T (F) Fn (0 ..^\|F\|))$
12	8 11	mpbid	$⊢ F \in Word ℝ \to T (F) Fn (0 ..^\|F\|)$
13		fnresin	$⊢ T (F) Fn (0 ..^\|F\|) \to ({T (F) ↾}_{(0 ..^N)}) Fn ((0 ..^\|F\|) \cap (0 ..^N))$
14	12 13	syl	$⊢ F \in Word ℝ \to ({T (F) ↾}_{(0 ..^N)}) Fn ((0 ..^\|F\|) \cap (0 ..^N))$
15	14	adantr	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to ({T (F) ↾}_{(0 ..^N)}) Fn ((0 ..^\|F\|) \cap (0 ..^N))$
16		elfzuz3	$⊢ N \in (0 \dots \|F\|) \to \|F\| \in ℤ_{\geq N}$
17		fzoss2	$⊢ \|F\| \in ℤ_{\geq N} \to (0 ..^N) \subseteq (0 ..^\|F\|)$
18	16 17	syl	$⊢ N \in (0 \dots \|F\|) \to (0 ..^N) \subseteq (0 ..^\|F\|)$
19	18	adantl	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to (0 ..^N) \subseteq (0 ..^\|F\|)$
20		incom	$⊢ (0 ..^N) \cap (0 ..^\|F\|) = (0 ..^\|F\|) \cap (0 ..^N)$
21		df-ss	$⊢ (0 ..^N) \subseteq (0 ..^\|F\|) \leftrightarrow (0 ..^N) \cap (0 ..^\|F\|) = (0 ..^N)$
22	21	biimpi	$⊢ (0 ..^N) \subseteq (0 ..^\|F\|) \to (0 ..^N) \cap (0 ..^\|F\|) = (0 ..^N)$
23	20 22	eqtr3id	$⊢ (0 ..^N) \subseteq (0 ..^\|F\|) \to (0 ..^\|F\|) \cap (0 ..^N) = (0 ..^N)$
24	23	fneq2d	$⊢ (0 ..^N) \subseteq (0 ..^\|F\|) \to (({T (F) ↾}_{(0 ..^N)}) Fn ((0 ..^\|F\|) \cap (0 ..^N)) \leftrightarrow ({T (F) ↾}_{(0 ..^N)}) Fn (0 ..^N))$
25	19 24	syl	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to (({T (F) ↾}_{(0 ..^N)}) Fn ((0 ..^\|F\|) \cap (0 ..^N)) \leftrightarrow ({T (F) ↾}_{(0 ..^N)}) Fn (0 ..^N))$
26	15 25	mpbid	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to ({T (F) ↾}_{(0 ..^N)}) Fn (0 ..^N)$
27		wrdres	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to {F ↾}_{(0 ..^N)} \in Word ℝ$
28	1 2 3 4	signstf	$⊢ {F ↾}_{(0 ..^N)} \in Word ℝ \to T ({F ↾}_{(0 ..^N)}) \in Word ℝ$
29		wrdf	$⊢ T ({F ↾}_{(0 ..^N)}) \in Word ℝ \to T ({F ↾}_{(0 ..^N)}) : (0 ..^\|T ({F ↾}_{(0 ..^N)})\|) ⟶ ℝ$
30		ffn	$⊢ T ({F ↾}_{(0 ..^N)}) : (0 ..^\|T ({F ↾}_{(0 ..^N)})\|) ⟶ ℝ \to T ({F ↾}_{(0 ..^N)}) Fn (0 ..^\|T ({F ↾}_{(0 ..^N)})\|)$
31	27 28 29 30	4syl	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to T ({F ↾}_{(0 ..^N)}) Fn (0 ..^\|T ({F ↾}_{(0 ..^N)})\|)$
32	1 2 3 4	signstlen	$⊢ {F ↾}_{(0 ..^N)} \in Word ℝ \to \|T ({F ↾}_{(0 ..^N)})\| = \|{F ↾}_{(0 ..^N)}\|$
33	27 32	syl	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to \|T ({F ↾}_{(0 ..^N)})\| = \|{F ↾}_{(0 ..^N)}\|$
34		wrdfn	$⊢ F \in Word ℝ \to F Fn (0 ..^\|F\|)$
35		fnssres	$⊢ (F Fn (0 ..^\|F\|) \land (0 ..^N) \subseteq (0 ..^\|F\|)) \to ({F ↾}_{(0 ..^N)}) Fn (0 ..^N)$
36	34 18 35	syl2an	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to ({F ↾}_{(0 ..^N)}) Fn (0 ..^N)$
37		hashfn	$⊢ ({F ↾}_{(0 ..^N)}) Fn (0 ..^N) \to \|{F ↾}_{(0 ..^N)}\| = \|(0 ..^N)\|$
38	36 37	syl	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to \|{F ↾}_{(0 ..^N)}\| = \|(0 ..^N)\|$
39		elfznn0	$⊢ N \in (0 \dots \|F\|) \to N \in ℕ_{0}$
40		hashfzo0	$⊢ N \in ℕ_{0} \to \|(0 ..^N)\| = N$
41	39 40	syl	$⊢ N \in (0 \dots \|F\|) \to \|(0 ..^N)\| = N$
42	41	adantl	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to \|(0 ..^N)\| = N$
43	33 38 42	3eqtrd	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to \|T ({F ↾}_{(0 ..^N)})\| = N$
44	43	oveq2d	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to (0 ..^\|T ({F ↾}_{(0 ..^N)})\|) = (0 ..^N)$
45	44	fneq2d	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to (T ({F ↾}_{(0 ..^N)}) Fn (0 ..^\|T ({F ↾}_{(0 ..^N)})\|) \leftrightarrow T ({F ↾}_{(0 ..^N)}) Fn (0 ..^N))$
46	31 45	mpbid	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to T ({F ↾}_{(0 ..^N)}) Fn (0 ..^N)$
47		fvres	$⊢ m \in (0 ..^N) \to ({T (F) ↾}_{(0 ..^N)}) (m) = T (F) (m)$
48	47	ad3antlr	$⊢ ((((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \land g \in Word ℝ) \land F = ({F ↾}_{(0 ..^N)}) ++ g) \to ({T (F) ↾}_{(0 ..^N)}) (m) = T (F) (m)$
49		simpr	$⊢ ((((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \land g \in Word ℝ) \land F = ({F ↾}_{(0 ..^N)}) ++ g) \to F = ({F ↾}_{(0 ..^N)}) ++ g$
50	49	fveq2d	$⊢ ((((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \land g \in Word ℝ) \land F = ({F ↾}_{(0 ..^N)}) ++ g) \to T (F) = T (({F ↾}_{(0 ..^N)}) ++ g)$
51	50	fveq1d	$⊢ ((((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \land g \in Word ℝ) \land F = ({F ↾}_{(0 ..^N)}) ++ g) \to T (F) (m) = T (({F ↾}_{(0 ..^N)}) ++ g) (m)$
52	27	ad3antrrr	$⊢ ((((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \land g \in Word ℝ) \land F = ({F ↾}_{(0 ..^N)}) ++ g) \to {F ↾}_{(0 ..^N)} \in Word ℝ$
53		simplr	$⊢ ((((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \land g \in Word ℝ) \land F = ({F ↾}_{(0 ..^N)}) ++ g) \to g \in Word ℝ$
54	38 42	eqtrd	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to \|{F ↾}_{(0 ..^N)}\| = N$
55	54	oveq2d	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to (0 ..^\|{F ↾}_{(0 ..^N)}\|) = (0 ..^N)$
56	55	eleq2d	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to (m \in (0 ..^\|{F ↾}_{(0 ..^N)}\|) \leftrightarrow m \in (0 ..^N))$
57	56	biimpar	$⊢ ((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \to m \in (0 ..^\|{F ↾}_{(0 ..^N)}\|)$
58	57	ad2antrr	$⊢ ((((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \land g \in Word ℝ) \land F = ({F ↾}_{(0 ..^N)}) ++ g) \to m \in (0 ..^\|{F ↾}_{(0 ..^N)}\|)$
59	1 2 3 4	signstfvc	$⊢ ({F ↾}_{(0 ..^N)} \in Word ℝ \land g \in Word ℝ \land m \in (0 ..^\|{F ↾}_{(0 ..^N)}\|)) \to T (({F ↾}_{(0 ..^N)}) ++ g) (m) = T ({F ↾}_{(0 ..^N)}) (m)$
60	52 53 58 59	syl3anc	$⊢ ((((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \land g \in Word ℝ) \land F = ({F ↾}_{(0 ..^N)}) ++ g) \to T (({F ↾}_{(0 ..^N)}) ++ g) (m) = T ({F ↾}_{(0 ..^N)}) (m)$
61	48 51 60	3eqtrd	$⊢ ((((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \land g \in Word ℝ) \land F = ({F ↾}_{(0 ..^N)}) ++ g) \to ({T (F) ↾}_{(0 ..^N)}) (m) = T ({F ↾}_{(0 ..^N)}) (m)$
62		wrdsplex	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to \exists g \in Word ℝ F = ({F ↾}_{(0 ..^N)}) ++ g$
63	62	adantr	$⊢ ((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \to \exists g \in Word ℝ F = ({F ↾}_{(0 ..^N)}) ++ g$
64	61 63	r19.29a	$⊢ ((F \in Word ℝ \land N \in (0 \dots \|F\|)) \land m \in (0 ..^N)) \to ({T (F) ↾}_{(0 ..^N)}) (m) = T ({F ↾}_{(0 ..^N)}) (m)$
65	26 46 64	eqfnfvd	$⊢ (F \in Word ℝ \land N \in (0 \dots \|F\|)) \to {T (F) ↾}_{(0 ..^N)} = T ({F ↾}_{(0 ..^N)})$

Metamath Proof Explorer

Theorem signstres

Proof