signstfvc

Description: Zero-skipping sign in a word compared to a shorter word. (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	signstfvc	$⊢ (F \in Word ℝ \land G \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ G) (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		oveq2	$⊢ g = \emptyset \to F ++ g = F ++ \emptyset$
6	5	fveq2d	$⊢ g = \emptyset \to T (F ++ g) = T (F ++ \emptyset)$
7	6	fveq1d	$⊢ g = \emptyset \to T (F ++ g) (N) = T (F ++ \emptyset) (N)$
8	7	eqeq1d	$⊢ g = \emptyset \to (T (F ++ g) (N) = T (F) (N) \leftrightarrow T (F ++ \emptyset) (N) = T (F) (N))$
9	8	imbi2d	$⊢ g = \emptyset \to (((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ g) (N) = T (F) (N)) \leftrightarrow ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ \emptyset) (N) = T (F) (N)))$
10		oveq2	$⊢ g = e \to F ++ g = F ++ e$
11	10	fveq2d	$⊢ g = e \to T (F ++ g) = T (F ++ e)$
12	11	fveq1d	$⊢ g = e \to T (F ++ g) (N) = T (F ++ e) (N)$
13	12	eqeq1d	$⊢ g = e \to (T (F ++ g) (N) = T (F) (N) \leftrightarrow T (F ++ e) (N) = T (F) (N))$
14	13	imbi2d	$⊢ g = e \to (((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ g) (N) = T (F) (N)) \leftrightarrow ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ e) (N) = T (F) (N)))$
15		oveq2	$⊢ g = e ++ ⟨“ k ”⟩ \to F ++ g = F ++ (e ++ ⟨“ k ”⟩)$
16	15	fveq2d	$⊢ g = e ++ ⟨“ k ”⟩ \to T (F ++ g) = T (F ++ (e ++ ⟨“ k ”⟩))$
17	16	fveq1d	$⊢ g = e ++ ⟨“ k ”⟩ \to T (F ++ g) (N) = T (F ++ (e ++ ⟨“ k ”⟩)) (N)$
18	17	eqeq1d	$⊢ g = e ++ ⟨“ k ”⟩ \to (T (F ++ g) (N) = T (F) (N) \leftrightarrow T (F ++ (e ++ ⟨“ k ”⟩)) (N) = T (F) (N))$
19	18	imbi2d	$⊢ g = e ++ ⟨“ k ”⟩ \to (((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ g) (N) = T (F) (N)) \leftrightarrow ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ (e ++ ⟨“ k ”⟩)) (N) = T (F) (N)))$
20		oveq2	$⊢ g = G \to F ++ g = F ++ G$
21	20	fveq2d	$⊢ g = G \to T (F ++ g) = T (F ++ G)$
22	21	fveq1d	$⊢ g = G \to T (F ++ g) (N) = T (F ++ G) (N)$
23	22	eqeq1d	$⊢ g = G \to (T (F ++ g) (N) = T (F) (N) \leftrightarrow T (F ++ G) (N) = T (F) (N))$
24	23	imbi2d	$⊢ g = G \to (((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ g) (N) = T (F) (N)) \leftrightarrow ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ G) (N) = T (F) (N)))$
25		ccatrid	$⊢ F \in Word ℝ \to F ++ \emptyset = F$
26	25	fveq2d	$⊢ F \in Word ℝ \to T (F ++ \emptyset) = T (F)$
27	26	fveq1d	$⊢ F \in Word ℝ \to T (F ++ \emptyset) (N) = T (F) (N)$
28	27	adantr	$⊢ (F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ \emptyset) (N) = T (F) (N)$
29		s1cl	$⊢ k \in ℝ \to ⟨“ k ”⟩ \in Word ℝ$
30		ccatass	$⊢ (F \in Word ℝ \land e \in Word ℝ \land ⟨“ k ”⟩ \in Word ℝ) \to (F ++ e) ++ ⟨“ k ”⟩ = F ++ (e ++ ⟨“ k ”⟩)$
31	29 30	syl3an3	$⊢ (F \in Word ℝ \land e \in Word ℝ \land k \in ℝ) \to (F ++ e) ++ ⟨“ k ”⟩ = F ++ (e ++ ⟨“ k ”⟩)$
32	31	3expb	$⊢ (F \in Word ℝ \land (e \in Word ℝ \land k \in ℝ)) \to (F ++ e) ++ ⟨“ k ”⟩ = F ++ (e ++ ⟨“ k ”⟩)$
33	32	adantlr	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to (F ++ e) ++ ⟨“ k ”⟩ = F ++ (e ++ ⟨“ k ”⟩)$
34	33	fveq2d	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to T ((F ++ e) ++ ⟨“ k ”⟩) = T (F ++ (e ++ ⟨“ k ”⟩))$
35	34	fveq1d	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to T ((F ++ e) ++ ⟨“ k ”⟩) (N) = T (F ++ (e ++ ⟨“ k ”⟩)) (N)$
36		ccatcl	$⊢ (F \in Word ℝ \land e \in Word ℝ) \to F ++ e \in Word ℝ$
37	36	ad2ant2r	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to F ++ e \in Word ℝ$
38		simprr	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to k \in ℝ$
39		lencl	$⊢ F \in Word ℝ \to \|F\| \in ℕ_{0}$
40	39	nn0zd	$⊢ F \in Word ℝ \to \|F\| \in ℤ$
41	40	adantr	$⊢ (F \in Word ℝ \land e \in Word ℝ) \to \|F\| \in ℤ$
42		lencl	$⊢ F ++ e \in Word ℝ \to \|F ++ e\| \in ℕ_{0}$
43	36 42	syl	$⊢ (F \in Word ℝ \land e \in Word ℝ) \to \|F ++ e\| \in ℕ_{0}$
44	43	nn0zd	$⊢ (F \in Word ℝ \land e \in Word ℝ) \to \|F ++ e\| \in ℤ$
45	39	nn0red	$⊢ F \in Word ℝ \to \|F\| \in ℝ$
46		lencl	$⊢ e \in Word ℝ \to \|e\| \in ℕ_{0}$
47		nn0addge1	$⊢ (\|F\| \in ℝ \land \|e\| \in ℕ_{0}) \to \|F\| \leq \|F\| + \|e\|$
48	45 46 47	syl2an	$⊢ (F \in Word ℝ \land e \in Word ℝ) \to \|F\| \leq \|F\| + \|e\|$
49		ccatlen	$⊢ (F \in Word ℝ \land e \in Word ℝ) \to \|F ++ e\| = \|F\| + \|e\|$
50	48 49	breqtrrd	$⊢ (F \in Word ℝ \land e \in Word ℝ) \to \|F\| \leq \|F ++ e\|$
51		eluz2	$⊢ \|F ++ e\| \in ℤ_{\geq \|F\|} \leftrightarrow (\|F\| \in ℤ \land \|F ++ e\| \in ℤ \land \|F\| \leq \|F ++ e\|)$
52	41 44 50 51	syl3anbrc	$⊢ (F \in Word ℝ \land e \in Word ℝ) \to \|F ++ e\| \in ℤ_{\geq \|F\|}$
53		fzoss2	$⊢ \|F ++ e\| \in ℤ_{\geq \|F\|} \to (0 ..^\|F\|) \subseteq (0 ..^\|F ++ e\|)$
54	52 53	syl	$⊢ (F \in Word ℝ \land e \in Word ℝ) \to (0 ..^\|F\|) \subseteq (0 ..^\|F ++ e\|)$
55	54	ad2ant2r	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to (0 ..^\|F\|) \subseteq (0 ..^\|F ++ e\|)$
56		simplr	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to N \in (0 ..^\|F\|)$
57	55 56	sseldd	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to N \in (0 ..^\|F ++ e\|)$
58	1 2 3 4	signstfvp	$⊢ (F ++ e \in Word ℝ \land k \in ℝ \land N \in (0 ..^\|F ++ e\|)) \to T ((F ++ e) ++ ⟨“ k ”⟩) (N) = T (F ++ e) (N)$
59	37 38 57 58	syl3anc	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to T ((F ++ e) ++ ⟨“ k ”⟩) (N) = T (F ++ e) (N)$
60	35 59	eqtr3d	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to T (F ++ (e ++ ⟨“ k ”⟩)) (N) = T (F ++ e) (N)$
61		id	$⊢ T (F ++ e) (N) = T (F) (N) \to T (F ++ e) (N) = T (F) (N)$
62	60 61	sylan9eq	$⊢ (((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \land T (F ++ e) (N) = T (F) (N)) \to T (F ++ (e ++ ⟨“ k ”⟩)) (N) = T (F) (N)$
63	62	ex	$⊢ ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \land (e \in Word ℝ \land k \in ℝ)) \to (T (F ++ e) (N) = T (F) (N) \to T (F ++ (e ++ ⟨“ k ”⟩)) (N) = T (F) (N))$
64	63	expcom	$⊢ (e \in Word ℝ \land k \in ℝ) \to ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to (T (F ++ e) (N) = T (F) (N) \to T (F ++ (e ++ ⟨“ k ”⟩)) (N) = T (F) (N)))$
65	64	a2d	$⊢ (e \in Word ℝ \land k \in ℝ) \to (((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ e) (N) = T (F) (N)) \to ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ (e ++ ⟨“ k ”⟩)) (N) = T (F) (N)))$
66	9 14 19 24 28 65	wrdind	$⊢ G \in Word ℝ \to ((F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ G) (N) = T (F) (N))$
67	66	3impib	$⊢ (G \in Word ℝ \land F \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ G) (N) = T (F) (N)$
68	67	3com12	$⊢ (F \in Word ℝ \land G \in Word ℝ \land N \in (0 ..^\|F\|)) \to T (F ++ G) (N) = T (F) (N)$

Metamath Proof Explorer

Theorem signstfvc

Proof