signstfvp

Description: Zero-skipping sign in a word compared to a shorter 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	signstfvp	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ ⟨“ K ”⟩) (N) = T (F) (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		simpl1	$⊢ ((F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to F \in Word ℝ$
6		s1cl	$⊢ K \in ℝ \to ⟨“ K ”⟩ \in Word ℝ$
7	6	3ad2ant2	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to ⟨“ K ”⟩ \in Word ℝ$
8	7	adantr	$⊢ ((F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to ⟨“ K ”⟩ \in Word ℝ$
9		fzssfzo	$⊢ N \in (0 ..^\|F\|) \to (0 \dots N) \subseteq (0 ..^\|F\|)$
10	9	3ad2ant3	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to (0 \dots N) \subseteq (0 ..^\|F\|)$
11	10	sselda	$⊢ ((F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to i \in (0 ..^\|F\|)$
12		ccatval1	$⊢ (F \in Word ℝ \land ⟨“ K ”⟩ \in Word ℝ \land i \in (0 ..^\|F\|)) \to (F ++ ⟨“ K ”⟩) (i) = F (i)$
13	5 8 11 12	syl3anc	$⊢ ((F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to (F ++ ⟨“ K ”⟩) (i) = F (i)$
14	13	fveq2d	$⊢ ((F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \land i \in (0 \dots N)) \to sgn ((F ++ ⟨“ K ”⟩) (i)) = sgn (F (i))$
15	14	mpteq2dva	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to (i \in (0 \dots N) ⟼ sgn ((F ++ ⟨“ K ”⟩) (i))) = (i \in (0 \dots N) ⟼ sgn (F (i)))$
16	15	oveq2d	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to {\sum_{W}}_{i = 0}^{N} sgn ((F ++ ⟨“ K ”⟩) (i)) = {\sum_{W}}_{i = 0}^{N} sgn (F (i))$
17		ccatws1cl	$⊢ (F \in Word ℝ \land K \in ℝ) \to F ++ ⟨“ K ”⟩ \in Word ℝ$
18	17	3adant3	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to F ++ ⟨“ K ”⟩ \in Word ℝ$
19		lencl	$⊢ F \in Word ℝ \to \|F\| \in ℕ_{0}$
20	19	nn0zd	$⊢ F \in Word ℝ \to \|F\| \in ℤ$
21	20	uzidd	$⊢ F \in Word ℝ \to \|F\| \in ℤ_{\geq \|F\|}$
22		peano2uz	$⊢ \|F\| \in ℤ_{\geq \|F\|} \to \|F\| + 1 \in ℤ_{\geq \|F\|}$
23		fzoss2	$⊢ \|F\| + 1 \in ℤ_{\geq \|F\|} \to (0 ..^\|F\|) \subseteq (0 ..^\|F\| + 1)$
24	21 22 23	3syl	$⊢ F \in Word ℝ \to (0 ..^\|F\|) \subseteq (0 ..^\|F\| + 1)$
25	24	sselda	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to N \in (0 ..^\|F\| + 1)$
26	25	3adant2	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to N \in (0 ..^\|F\| + 1)$
27		ccatlen	$⊢ (F \in Word ℝ \land ⟨“ K ”⟩ \in Word ℝ) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + \|⟨“ K ”⟩\|$
28	6 27	sylan2	$⊢ (F \in Word ℝ \land K \in ℝ) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + \|⟨“ K ”⟩\|$
29	28	3adant3	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + \|⟨“ K ”⟩\|$
30		s1len	$⊢ \|⟨“ K ”⟩\| = 1$
31	30	oveq2i	$⊢ \|F\| + \|⟨“ K ”⟩\| = \|F\| + 1$
32	29 31	eqtrdi	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to \|F ++ ⟨“ K ”⟩\| = \|F\| + 1$
33	32	oveq2d	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to (0 ..^\|F ++ ⟨“ K ”⟩\|) = (0 ..^\|F\| + 1)$
34	26 33	eleqtrrd	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to N \in (0 ..^\|F ++ ⟨“ K ”⟩\|)$
35	1 2 3 4	signstfval	$⊢ (F ++ ⟨“ K ”⟩ \in Word ℝ \land N \in (0 ..^\|F ++ ⟨“ K ”⟩\|)) \to T (F ++ ⟨“ K ”⟩) (N) = {\sum_{W}}_{i = 0}^{N} sgn ((F ++ ⟨“ K ”⟩) (i))$
36	18 34 35	syl2anc	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ ⟨“ K ”⟩) (N) = {\sum_{W}}_{i = 0}^{N} sgn ((F ++ ⟨“ K ”⟩) (i))$
37	1 2 3 4	signstfval	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F) (N) = {\sum_{W}}_{i = 0}^{N} sgn (F (i))$
38	37	3adant2	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to T (F) (N) = {\sum_{W}}_{i = 0}^{N} sgn (F (i))$
39	16 36 38	3eqtr4d	$⊢ (F \in Word ℝ \land K \in ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ ⟨“ K ”⟩) (N) = T (F) (N)$

Metamath Proof Explorer

Theorem signstfvp

Proof