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

Theorem signsvfn 29985
 Description: Number of changes in a word compared to a shorter word. (Contributed by Thierry Arnoux, 12-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
signsvfn (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = ((𝑉𝐹) + if((((𝑇𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0, 1, 0)))
Distinct variable groups:   𝑎,𝑏,   𝑓,𝑖,𝑛,𝐹   𝑓,𝐾,𝑖,𝑛   𝑓,𝑊,𝑖,𝑛   𝑖,𝑎,𝑗,𝑛,𝐹,𝑏   𝐾,𝑎,𝑏,𝑗,𝑓   𝑇,𝑎   𝑓,𝑏,𝑇,𝑗,𝑛
Allowed substitution hints:   (𝑓,𝑖,𝑗,𝑛)   𝑇(𝑖)   𝑉(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏)   𝑊(𝑗,𝑎,𝑏)

Proof of Theorem signsvfn
StepHypRef Expression
1 simpl 472 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 𝐹 ∈ (Word ℝ ∖ {∅}))
21eldifad 3552 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 𝐹 ∈ Word ℝ)
3 simpr 476 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈ ℝ)
43s1cld 13236 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ⟨“𝐾”⟩ ∈ Word ℝ)
5 ccatcl 13212 . . . . . 6 ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ) → (𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ)
62, 4, 5syl2anc 691 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ)
7 signsv.p . . . . . 6 = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
8 signsv.w . . . . . 6 𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}
9 signsv.t . . . . . 6 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))
10 signsv.v . . . . . 6 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))
117, 8, 9, 10signsvvfval 29981 . . . . 5 ((𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = Σ𝑗 ∈ (1..^(#‘(𝐹 ++ ⟨“𝐾”⟩)))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0))
126, 11syl 17 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = Σ𝑗 ∈ (1..^(#‘(𝐹 ++ ⟨“𝐾”⟩)))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0))
13 ccatlen 13213 . . . . . . . 8 ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ) → (#‘(𝐹 ++ ⟨“𝐾”⟩)) = ((#‘𝐹) + (#‘⟨“𝐾”⟩)))
142, 4, 13syl2anc 691 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘(𝐹 ++ ⟨“𝐾”⟩)) = ((#‘𝐹) + (#‘⟨“𝐾”⟩)))
15 s1len 13238 . . . . . . . 8 (#‘⟨“𝐾”⟩) = 1
1615oveq2i 6560 . . . . . . 7 ((#‘𝐹) + (#‘⟨“𝐾”⟩)) = ((#‘𝐹) + 1)
1714, 16syl6eq 2660 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘(𝐹 ++ ⟨“𝐾”⟩)) = ((#‘𝐹) + 1))
1817oveq2d 6565 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (1..^(#‘(𝐹 ++ ⟨“𝐾”⟩))) = (1..^((#‘𝐹) + 1)))
1918sumeq1d 14279 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^(#‘(𝐹 ++ ⟨“𝐾”⟩)))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = Σ𝑗 ∈ (1..^((#‘𝐹) + 1))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0))
20 eldifsn 4260 . . . . . . . 8 (𝐹 ∈ (Word ℝ ∖ {∅}) ↔ (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅))
21 lennncl 13180 . . . . . . . 8 ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → (#‘𝐹) ∈ ℕ)
2220, 21sylbi 206 . . . . . . 7 (𝐹 ∈ (Word ℝ ∖ {∅}) → (#‘𝐹) ∈ ℕ)
23 nnuz 11599 . . . . . . 7 ℕ = (ℤ‘1)
2422, 23syl6eleq 2698 . . . . . 6 (𝐹 ∈ (Word ℝ ∖ {∅}) → (#‘𝐹) ∈ (ℤ‘1))
2524adantr 480 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈ (ℤ‘1))
26 1cnd 9935 . . . . . 6 ((((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1...(#‘𝐹))) ∧ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1))) → 1 ∈ ℂ)
27 0cnd 9912 . . . . . 6 ((((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1...(#‘𝐹))) ∧ ¬ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1))) → 0 ∈ ℂ)
2826, 27ifclda 4070 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1...(#‘𝐹))) → if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) ∈ ℂ)
29 fveq2 6103 . . . . . . 7 (𝑗 = (#‘𝐹) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) = ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)))
30 oveq1 6556 . . . . . . . 8 (𝑗 = (#‘𝐹) → (𝑗 − 1) = ((#‘𝐹) − 1))
3130fveq2d 6107 . . . . . . 7 (𝑗 = (#‘𝐹) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) = ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)))
3229, 31neeq12d 2843 . . . . . 6 (𝑗 = (#‘𝐹) → (((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) ↔ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1))))
3332ifbid 4058 . . . . 5 (𝑗 = (#‘𝐹) → if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)), 1, 0))
3425, 28, 33fzosump1 14325 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^((#‘𝐹) + 1))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = (Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)), 1, 0)))
3512, 19, 343eqtrd 2648 . . 3 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = (Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)), 1, 0)))
3635adantlr 747 . 2 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = (Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)), 1, 0)))
372adantr 480 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → 𝐹 ∈ Word ℝ)
383adantr 480 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → 𝐾 ∈ ℝ)
39 fzo0ss1 12367 . . . . . . . . . . 11 (1..^(#‘𝐹)) ⊆ (0..^(#‘𝐹))
4039a1i 11 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (1..^(#‘𝐹)) ⊆ (0..^(#‘𝐹)))
4140sselda 3568 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → 𝑗 ∈ (0..^(#‘𝐹)))
427, 8, 9, 10signstfvp 29974 . . . . . . . . 9 ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) = ((𝑇𝐹)‘𝑗))
4337, 38, 41, 42syl3anc 1318 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) = ((𝑇𝐹)‘𝑗))
44 elfzoel2 12338 . . . . . . . . . . . . 13 (𝑗 ∈ (1..^(#‘𝐹)) → (#‘𝐹) ∈ ℤ)
4544adantl 481 . . . . . . . . . . . 12 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → (#‘𝐹) ∈ ℤ)
46 1nn0 11185 . . . . . . . . . . . 12 1 ∈ ℕ0
47 eluzmn 11570 . . . . . . . . . . . 12 (((#‘𝐹) ∈ ℤ ∧ 1 ∈ ℕ0) → (#‘𝐹) ∈ (ℤ‘((#‘𝐹) − 1)))
4845, 46, 47sylancl 693 . . . . . . . . . . 11 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → (#‘𝐹) ∈ (ℤ‘((#‘𝐹) − 1)))
49 fzoss2 12365 . . . . . . . . . . 11 ((#‘𝐹) ∈ (ℤ‘((#‘𝐹) − 1)) → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)))
5048, 49syl 17 . . . . . . . . . 10 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → (0..^((#‘𝐹) − 1)) ⊆ (0..^(#‘𝐹)))
51 simpr 476 . . . . . . . . . . 11 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → 𝑗 ∈ (1..^(#‘𝐹)))
52 elfzoelz 12339 . . . . . . . . . . . . 13 (𝑗 ∈ (1..^(#‘𝐹)) → 𝑗 ∈ ℤ)
5352adantl 481 . . . . . . . . . . . 12 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → 𝑗 ∈ ℤ)
54 elfzom1b 12433 . . . . . . . . . . . 12 ((𝑗 ∈ ℤ ∧ (#‘𝐹) ∈ ℤ) → (𝑗 ∈ (1..^(#‘𝐹)) ↔ (𝑗 − 1) ∈ (0..^((#‘𝐹) − 1))))
5553, 45, 54syl2anc 691 . . . . . . . . . . 11 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → (𝑗 ∈ (1..^(#‘𝐹)) ↔ (𝑗 − 1) ∈ (0..^((#‘𝐹) − 1))))
5651, 55mpbid 221 . . . . . . . . . 10 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → (𝑗 − 1) ∈ (0..^((#‘𝐹) − 1)))
5750, 56sseldd 3569 . . . . . . . . 9 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → (𝑗 − 1) ∈ (0..^(#‘𝐹)))
587, 8, 9, 10signstfvp 29974 . . . . . . . . 9 ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ (𝑗 − 1) ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) = ((𝑇𝐹)‘(𝑗 − 1)))
5937, 38, 57, 58syl3anc 1318 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) = ((𝑇𝐹)‘(𝑗 − 1)))
6043, 59neeq12d 2843 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → (((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)) ↔ ((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1))))
6160ifbid 4058 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑗 ∈ (1..^(#‘𝐹))) → if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = if(((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1)), 1, 0))
6261sumeq2dv 14281 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1)), 1, 0))
637, 8, 9, 10signsvvfval 29981 . . . . . 6 (𝐹 ∈ Word ℝ → (𝑉𝐹) = Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1)), 1, 0))
642, 63syl 17 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑉𝐹) = Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇𝐹)‘𝑗) ≠ ((𝑇𝐹)‘(𝑗 − 1)), 1, 0))
6562, 64eqtr4d 2647 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = (𝑉𝐹))
6665adantlr 747 . . 3 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) = (𝑉𝐹))
677, 8, 9, 10signstfvn 29972 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) = (((𝑇𝐹)‘((#‘𝐹) − 1)) (sgn‘𝐾)))
6867adantlr 747 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) = (((𝑇𝐹)‘((#‘𝐹) − 1)) (sgn‘𝐾)))
692adantlr 747 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐹 ∈ Word ℝ)
70 simpr 476 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈ ℝ)
7122ad2antrr 758 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈ ℕ)
72 fzo0end 12426 . . . . . . . 8 ((#‘𝐹) ∈ ℕ → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
7371, 72syl 17 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
747, 8, 9, 10signstfvp 29974 . . . . . . 7 ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)) = ((𝑇𝐹)‘((#‘𝐹) − 1)))
7569, 70, 73, 74syl3anc 1318 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)) = ((𝑇𝐹)‘((#‘𝐹) − 1)))
7668, 75neeq12d 2843 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)) ↔ (((𝑇𝐹)‘((#‘𝐹) − 1)) (sgn‘𝐾)) ≠ ((𝑇𝐹)‘((#‘𝐹) − 1))))
777, 8, 9, 10signstfvcl 29976 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹))) → ((𝑇𝐹)‘((#‘𝐹) − 1)) ∈ {-1, 1})
7873, 77syldan 486 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇𝐹)‘((#‘𝐹) − 1)) ∈ {-1, 1})
7970rexrd 9968 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈ ℝ*)
80 sgncl 29927 . . . . . . 7 (𝐾 ∈ ℝ* → (sgn‘𝐾) ∈ {-1, 0, 1})
8179, 80syl 17 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘𝐾) ∈ {-1, 0, 1})
827, 8signswch 29964 . . . . . 6 ((((𝑇𝐹)‘((#‘𝐹) − 1)) ∈ {-1, 1} ∧ (sgn‘𝐾) ∈ {-1, 0, 1}) → ((((𝑇𝐹)‘((#‘𝐹) − 1)) (sgn‘𝐾)) ≠ ((𝑇𝐹)‘((#‘𝐹) − 1)) ↔ (((𝑇𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0))
8378, 81, 82syl2anc 691 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((#‘𝐹) − 1)) (sgn‘𝐾)) ≠ ((𝑇𝐹)‘((#‘𝐹) − 1)) ↔ (((𝑇𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0))
84 sgnsgn 29937 . . . . . . . . 9 (𝐾 ∈ ℝ* → (sgn‘(sgn‘𝐾)) = (sgn‘𝐾))
8579, 84syl 17 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘(sgn‘𝐾)) = (sgn‘𝐾))
8685oveq2d 6565 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((sgn‘((𝑇𝐹)‘((#‘𝐹) − 1))) · (sgn‘(sgn‘𝐾))) = ((sgn‘((𝑇𝐹)‘((#‘𝐹) − 1))) · (sgn‘𝐾)))
8786breq1d 4593 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((sgn‘((𝑇𝐹)‘((#‘𝐹) − 1))) · (sgn‘(sgn‘𝐾))) < 0 ↔ ((sgn‘((𝑇𝐹)‘((#‘𝐹) − 1))) · (sgn‘𝐾)) < 0))
88 neg1rr 11002 . . . . . . . . 9 -1 ∈ ℝ
89 1re 9918 . . . . . . . . 9 1 ∈ ℝ
90 prssi 4293 . . . . . . . . 9 ((-1 ∈ ℝ ∧ 1 ∈ ℝ) → {-1, 1} ⊆ ℝ)
9188, 89, 90mp2an 704 . . . . . . . 8 {-1, 1} ⊆ ℝ
9291, 78sseldi 3566 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((𝑇𝐹)‘((#‘𝐹) − 1)) ∈ ℝ)
93 sgnclre 29928 . . . . . . . 8 (𝐾 ∈ ℝ → (sgn‘𝐾) ∈ ℝ)
9493adantl 481 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (sgn‘𝐾) ∈ ℝ)
95 sgnmulsgn 29938 . . . . . . 7 ((((𝑇𝐹)‘((#‘𝐹) − 1)) ∈ ℝ ∧ (sgn‘𝐾) ∈ ℝ) → ((((𝑇𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔ ((sgn‘((𝑇𝐹)‘((#‘𝐹) − 1))) · (sgn‘(sgn‘𝐾))) < 0))
9692, 94, 95syl2anc 691 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔ ((sgn‘((𝑇𝐹)‘((#‘𝐹) − 1))) · (sgn‘(sgn‘𝐾))) < 0))
97 sgnmulsgn 29938 . . . . . . 7 ((((𝑇𝐹)‘((#‘𝐹) − 1)) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0 ↔ ((sgn‘((𝑇𝐹)‘((#‘𝐹) − 1))) · (sgn‘𝐾)) < 0))
9892, 70, 97syl2anc 691 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0 ↔ ((sgn‘((𝑇𝐹)‘((#‘𝐹) − 1))) · (sgn‘𝐾)) < 0))
9987, 96, 983bitr4d 299 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → ((((𝑇𝐹)‘((#‘𝐹) − 1)) · (sgn‘𝐾)) < 0 ↔ (((𝑇𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0))
10076, 83, 993bitrd 293 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)) ↔ (((𝑇𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0))
101100ifbid 4058 . . 3 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)), 1, 0) = if((((𝑇𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0, 1, 0))
10266, 101oveq12d 6567 . 2 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (Σ𝑗 ∈ (1..^(#‘𝐹))if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘𝑗) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(𝑗 − 1)), 1, 0) + if(((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) ≠ ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘((#‘𝐹) − 1)), 1, 0)) = ((𝑉𝐹) + if((((𝑇𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0, 1, 0)))
10336, 102eqtrd 2644 1 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝐾 ∈ ℝ) → (𝑉‘(𝐹 ++ ⟨“𝐾”⟩)) = ((𝑉𝐹) + if((((𝑇𝐹)‘((#‘𝐹) − 1)) · 𝐾) < 0, 1, 0)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {csn 4125  {cpr 4127  {ctp 4129  ⟨cop 4131   class class class wbr 4583   ↦ cmpt 4643  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℝ*cxr 9952   < clt 9953   − cmin 10145  -cneg 10146  ℕcn 10897  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197  ..^cfzo 12334  #chash 12979  Word cword 13146   ++ cconcat 13148  ⟨“cs1 13149  sgncsgn 13674  Σcsu 14264  ndxcnx 15692  Basecbs 15695  +gcplusg 15768   Σg cgsu 15924 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-seq 12664  df-exp 12723  df-hash 12980  df-word 13154  df-lsw 13155  df-concat 13156  df-s1 13157  df-substr 13158  df-sgn 13675  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-sum 14265  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mulg 17364  df-cntz 17573 This theorem is referenced by:  signsvtp  29986  signsvtn  29987  signlem0  29990
 Copyright terms: Public domain W3C validator