signstfvp - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > signstfvp		Structured version Visualization version GIF version

Theorem signstfvp 31951

Description: Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 8-Oct-2018.)

**Hypotheses**
Ref	Expression
signsv.p	⊢ ⨣ = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
signsv.w	⊢ 𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+_g‘ndx), ⨣ ⟩}
signsv.t	⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖))))))
signsv.v	⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0))

**Assertion**
Ref	Expression
signstfvp	⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑁) = ((𝑇‘𝐹)‘𝑁))

Distinct variable groups: 𝑎,𝑏, ⨣ 𝑓,𝑖,𝑛,𝐹 𝑓,𝐾,𝑖,𝑛 𝑓,𝑊,𝑖,𝑛 𝑖,𝑁,𝑛 Allowed substitution hints: ⨣ (𝑓,𝑖,𝑗,𝑛) 𝑇(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏) 𝐹(𝑗,𝑎,𝑏) 𝐾(𝑗,𝑎,𝑏) 𝑁(𝑓,𝑗,𝑎,𝑏) 𝑉(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏) 𝑊(𝑗,𝑎,𝑏)

**Proof of Theorem signstfvp**
Step	Hyp	Ref	Expression
1		simpl1 1188	. . . . . 6 ⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 ∈ (0...𝑁)) → 𝐹 ∈ Word ℝ)
2		s1cl 13947	. . . . . . . 8 ⊢ (𝐾 ∈ ℝ → ⟨“𝐾”⟩ ∈ Word ℝ)
3	2	3ad2ant2 1131	. . . . . . 7 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ⟨“𝐾”⟩ ∈ Word ℝ)
4	3	adantr 484	. . . . . 6 ⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 ∈ (0...𝑁)) → ⟨“𝐾”⟩ ∈ Word ℝ)
5		fzssfzo 31919	. . . . . . . 8 ⊢ (𝑁 ∈ (0..^(♯‘𝐹)) → (0...𝑁) ⊆ (0..^(♯‘𝐹)))
6	5	3ad2ant3 1132	. . . . . . 7 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (0...𝑁) ⊆ (0..^(♯‘𝐹)))
7	6	sselda 3915	. . . . . 6 ⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0..^(♯‘𝐹)))
8		ccatval1 13921	. . . . . 6 ⊢ ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ ∧ 𝑖 ∈ (0..^(♯‘𝐹))) → ((𝐹 ++ ⟨“𝐾”⟩)‘𝑖) = (𝐹‘𝑖))
9	1, 4, 7, 8	syl3anc 1368	. . . . 5 ⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 ∈ (0...𝑁)) → ((𝐹 ++ ⟨“𝐾”⟩)‘𝑖) = (𝐹‘𝑖))
10	9	fveq2d 6649	. . . 4 ⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 ∈ (0...𝑁)) → (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)) = (sgn‘(𝐹‘𝑖)))
11	10	mpteq2dva 5125	. . 3 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖))) = (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖))))
12	11	oveq2d 7151	. 2 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝑊 Σ_g (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))) = (𝑊 Σ_g (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖)))))
13		ccatws1cl 13961	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ)
14	13	3adant3 1129	. . 3 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ)
15		lencl 13876	. . . . . . . . 9 ⊢ (𝐹 ∈ Word ℝ → (♯‘𝐹) ∈ ℕ₀)
16	15	nn0zd 12073	. . . . . . . 8 ⊢ (𝐹 ∈ Word ℝ → (♯‘𝐹) ∈ ℤ)
17	16	uzidd 12247	. . . . . . 7 ⊢ (𝐹 ∈ Word ℝ → (♯‘𝐹) ∈ (ℤ_≥‘(♯‘𝐹)))
18		peano2uz 12289	. . . . . . 7 ⊢ ((♯‘𝐹) ∈ (ℤ_≥‘(♯‘𝐹)) → ((♯‘𝐹) + 1) ∈ (ℤ_≥‘(♯‘𝐹)))
19		fzoss2 13060	. . . . . . 7 ⊢ (((♯‘𝐹) + 1) ∈ (ℤ_≥‘(♯‘𝐹)) → (0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1)))
20	17, 18, 19	3syl 18	. . . . . 6 ⊢ (𝐹 ∈ Word ℝ → (0..^(♯‘𝐹)) ⊆ (0..^((♯‘𝐹) + 1)))
21	20	sselda 3915	. . . . 5 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^((♯‘𝐹) + 1)))
22	21	3adant2 1128	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^((♯‘𝐹) + 1)))
23		ccatlen 13918	. . . . . . . 8 ⊢ ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ) → (♯‘(𝐹 ++ ⟨“𝐾”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐾”⟩)))
24	2, 23	sylan2 595	. . . . . . 7 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (♯‘(𝐹 ++ ⟨“𝐾”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐾”⟩)))
25	24	3adant3 1129	. . . . . 6 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (♯‘(𝐹 ++ ⟨“𝐾”⟩)) = ((♯‘𝐹) + (♯‘⟨“𝐾”⟩)))
26		s1len 13951	. . . . . . 7 ⊢ (♯‘⟨“𝐾”⟩) = 1
27	26	oveq2i 7146	. . . . . 6 ⊢ ((♯‘𝐹) + (♯‘⟨“𝐾”⟩)) = ((♯‘𝐹) + 1)
28	25, 27	eqtrdi 2849	. . . . 5 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (♯‘(𝐹 ++ ⟨“𝐾”⟩)) = ((♯‘𝐹) + 1))
29	28	oveq2d 7151	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (0..^(♯‘(𝐹 ++ ⟨“𝐾”⟩))) = (0..^((♯‘𝐹) + 1)))
30	22, 29	eleqtrrd 2893	. . 3 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘(𝐹 ++ ⟨“𝐾”⟩))))
31		signsv.p	. . . 4 ⊢ ⨣ = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
32		signsv.w	. . . 4 ⊢ 𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+_g‘ndx), ⨣ ⟩}
33		signsv.t	. . . 4 ⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(♯‘𝑓)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖))))))
34		signsv.v	. . . 4 ⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0))
35	31, 32, 33, 34	signstfval 31944	. . 3 ⊢ (((𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘(𝐹 ++ ⟨“𝐾”⟩)))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑁) = (𝑊 Σ_g (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))))
36	14, 30, 35	syl2anc 587	. 2 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑁) = (𝑊 Σ_g (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))))
37	31, 32, 33, 34	signstfval 31944	. . 3 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) = (𝑊 Σ_g (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖)))))
38	37	3adant2 1128	. 2 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) = (𝑊 Σ_g (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖)))))
39	12, 36, 38	3eqtr4d 2843	1 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑁) = ((𝑇‘𝐹)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ⊆ wss 3881 ifcif 4425 {cpr 4527 {ctp 4529 ⟨cop 4531 ↦ cmpt 5110 ‘cfv 6324 (class class class)co 7135 ∈ cmpo 7137 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 − cmin 10859 -cneg 10860 ℤ_≥cuz 12231 ...cfz 12885 ..^cfzo 13028 ♯chash 13686 Word cword 13857 ++ cconcat 13913 ⟨“cs1 13940 sgncsgn 14437 Σcsu 15034 ndxcnx 16472 Basecbs 16475 +_gcplusg 16557 Σ_g cgsu 16706

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-oadd 8089 df-er 8272 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-nn 11626 df-n0 11886 df-z 11970 df-uz 12232 df-fz 12886 df-fzo 13029 df-hash 13687 df-word 13858 df-concat 13914 df-s1 13941

This theorem is referenced by: signstfvneq0 31952 signstfvc 31954 signstfveq0 31957 signsvfn 31962

W3C validator