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

Theorem signstfvn 30774
 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
signstfvn ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) = (((𝑇𝐹)‘((#‘𝐹) − 1)) (sgn‘𝐾)))
Distinct variable groups:   𝑎,𝑏,   𝑓,𝑖,𝑛,𝐹   𝑓,𝐾,𝑖,𝑛   𝑓,𝑊,𝑖,𝑛
Allowed substitution hints:   (𝑓,𝑖,𝑗,𝑛)   𝑇(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏)   𝐹(𝑗,𝑎,𝑏)   𝐾(𝑗,𝑎,𝑏)   𝑉(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏)   𝑊(𝑗,𝑎,𝑏)

Proof of Theorem signstfvn
StepHypRef Expression
1 signsv.p . . . . 5 = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
2 signsv.w . . . . 5 𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+g‘ndx), ⟩}
31, 2signswbase 30759 . . . 4 {-1, 0, 1} = (Base‘𝑊)
41, 2signswmnd 30762 . . . . 5 𝑊 ∈ Mnd
54a1i 11 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 𝑊 ∈ Mnd)
6 eldifi 3765 . . . . . . . . 9 (𝐹 ∈ (Word ℝ ∖ {∅}) → 𝐹 ∈ Word ℝ)
7 lencl 13356 . . . . . . . . 9 (𝐹 ∈ Word ℝ → (#‘𝐹) ∈ ℕ0)
86, 7syl 17 . . . . . . . 8 (𝐹 ∈ (Word ℝ ∖ {∅}) → (#‘𝐹) ∈ ℕ0)
9 eldifsn 4350 . . . . . . . . 9 (𝐹 ∈ (Word ℝ ∖ {∅}) ↔ (𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅))
10 hasheq0 13192 . . . . . . . . . . 11 (𝐹 ∈ Word ℝ → ((#‘𝐹) = 0 ↔ 𝐹 = ∅))
1110necon3bid 2867 . . . . . . . . . 10 (𝐹 ∈ Word ℝ → ((#‘𝐹) ≠ 0 ↔ 𝐹 ≠ ∅))
1211biimpar 501 . . . . . . . . 9 ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) → (#‘𝐹) ≠ 0)
139, 12sylbi 207 . . . . . . . 8 (𝐹 ∈ (Word ℝ ∖ {∅}) → (#‘𝐹) ≠ 0)
14 elnnne0 11344 . . . . . . . 8 ((#‘𝐹) ∈ ℕ ↔ ((#‘𝐹) ∈ ℕ0 ∧ (#‘𝐹) ≠ 0))
158, 13, 14sylanbrc 699 . . . . . . 7 (𝐹 ∈ (Word ℝ ∖ {∅}) → (#‘𝐹) ∈ ℕ)
1615adantr 480 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈ ℕ)
17 nnm1nn0 11372 . . . . . 6 ((#‘𝐹) ∈ ℕ → ((#‘𝐹) − 1) ∈ ℕ0)
1816, 17syl 17 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((#‘𝐹) − 1) ∈ ℕ0)
19 nn0uz 11760 . . . . 5 0 = (ℤ‘0)
2018, 19syl6eleq 2740 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((#‘𝐹) − 1) ∈ (ℤ‘0))
21 s1cl 13418 . . . . . . . . . 10 (𝐾 ∈ ℝ → ⟨“𝐾”⟩ ∈ Word ℝ)
22 ccatcl 13392 . . . . . . . . . 10 ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ) → (𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ)
236, 21, 22syl2an 493 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ)
2423adantr 480 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → (𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ)
25 wrdf 13342 . . . . . . . 8 ((𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ → (𝐹 ++ ⟨“𝐾”⟩):(0..^(#‘(𝐹 ++ ⟨“𝐾”⟩)))⟶ℝ)
2624, 25syl 17 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → (𝐹 ++ ⟨“𝐾”⟩):(0..^(#‘(𝐹 ++ ⟨“𝐾”⟩)))⟶ℝ)
278adantr 480 . . . . . . . . . . . 12 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈ ℕ0)
2827nn0zd 11518 . . . . . . . . . . 11 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈ ℤ)
29 fzoval 12510 . . . . . . . . . . 11 ((#‘𝐹) ∈ ℤ → (0..^(#‘𝐹)) = (0...((#‘𝐹) − 1)))
3028, 29syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (0..^(#‘𝐹)) = (0...((#‘𝐹) − 1)))
31 fzossfz 12527 . . . . . . . . . 10 (0..^(#‘𝐹)) ⊆ (0...(#‘𝐹))
3230, 31syl6eqssr 3689 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (0...((#‘𝐹) − 1)) ⊆ (0...(#‘𝐹)))
33 ccatlen 13393 . . . . . . . . . . . . 13 ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ) → (#‘(𝐹 ++ ⟨“𝐾”⟩)) = ((#‘𝐹) + (#‘⟨“𝐾”⟩)))
346, 21, 33syl2an 493 . . . . . . . . . . . 12 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘(𝐹 ++ ⟨“𝐾”⟩)) = ((#‘𝐹) + (#‘⟨“𝐾”⟩)))
35 s1len 13422 . . . . . . . . . . . . 13 (#‘⟨“𝐾”⟩) = 1
3635oveq2i 6701 . . . . . . . . . . . 12 ((#‘𝐹) + (#‘⟨“𝐾”⟩)) = ((#‘𝐹) + 1)
3734, 36syl6eq 2701 . . . . . . . . . . 11 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘(𝐹 ++ ⟨“𝐾”⟩)) = ((#‘𝐹) + 1))
3837oveq2d 6706 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (0..^(#‘(𝐹 ++ ⟨“𝐾”⟩))) = (0..^((#‘𝐹) + 1)))
3928peano2zd 11523 . . . . . . . . . . 11 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((#‘𝐹) + 1) ∈ ℤ)
40 fzoval 12510 . . . . . . . . . . 11 (((#‘𝐹) + 1) ∈ ℤ → (0..^((#‘𝐹) + 1)) = (0...(((#‘𝐹) + 1) − 1)))
4139, 40syl 17 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (0..^((#‘𝐹) + 1)) = (0...(((#‘𝐹) + 1) − 1)))
4227nn0cnd 11391 . . . . . . . . . . . 12 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈ ℂ)
43 1cnd 10094 . . . . . . . . . . . 12 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 1 ∈ ℂ)
4442, 43pncand 10431 . . . . . . . . . . 11 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (((#‘𝐹) + 1) − 1) = (#‘𝐹))
4544oveq2d 6706 . . . . . . . . . 10 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (0...(((#‘𝐹) + 1) − 1)) = (0...(#‘𝐹)))
4638, 41, 453eqtrd 2689 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (0..^(#‘(𝐹 ++ ⟨“𝐾”⟩))) = (0...(#‘𝐹)))
4732, 46sseqtr4d 3675 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (0...((#‘𝐹) − 1)) ⊆ (0..^(#‘(𝐹 ++ ⟨“𝐾”⟩))))
4847sselda 3636 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → 𝑖 ∈ (0..^(#‘(𝐹 ++ ⟨“𝐾”⟩))))
4926, 48ffvelrnd 6400 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → ((𝐹 ++ ⟨“𝐾”⟩)‘𝑖) ∈ ℝ)
5049rexrd 10127 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → ((𝐹 ++ ⟨“𝐾”⟩)‘𝑖) ∈ ℝ*)
51 sgncl 30728 . . . . 5 (((𝐹 ++ ⟨“𝐾”⟩)‘𝑖) ∈ ℝ* → (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)) ∈ {-1, 0, 1})
5250, 51syl 17 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)) ∈ {-1, 0, 1})
531, 2signswplusg 30760 . . . 4 = (+g𝑊)
54 simpr 476 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈ ℝ)
5554rexrd 10127 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 𝐾 ∈ ℝ*)
56 sgncl 30728 . . . . 5 (𝐾 ∈ ℝ* → (sgn‘𝐾) ∈ {-1, 0, 1})
5755, 56syl 17 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (sgn‘𝐾) ∈ {-1, 0, 1})
58 simpr 476 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((#‘𝐹) − 1) + 1)) → 𝑖 = (((#‘𝐹) − 1) + 1))
5942, 43npcand 10434 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (((#‘𝐹) − 1) + 1) = (#‘𝐹))
6059adantr 480 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((#‘𝐹) − 1) + 1)) → (((#‘𝐹) − 1) + 1) = (#‘𝐹))
6158, 60eqtrd 2685 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((#‘𝐹) − 1) + 1)) → 𝑖 = (#‘𝐹))
6261fveq2d 6233 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((#‘𝐹) − 1) + 1)) → ((𝐹 ++ ⟨“𝐾”⟩)‘𝑖) = ((𝐹 ++ ⟨“𝐾”⟩)‘(#‘𝐹)))
636adantr 480 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 𝐹 ∈ Word ℝ)
6454, 21syl 17 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ⟨“𝐾”⟩ ∈ Word ℝ)
65 c0ex 10072 . . . . . . . . . . . . 13 0 ∈ V
6665snid 4241 . . . . . . . . . . . 12 0 ∈ {0}
67 fzo01 12590 . . . . . . . . . . . 12 (0..^1) = {0}
6866, 67eleqtrri 2729 . . . . . . . . . . 11 0 ∈ (0..^1)
6935oveq2i 6701 . . . . . . . . . . 11 (0..^(#‘⟨“𝐾”⟩)) = (0..^1)
7068, 69eleqtrri 2729 . . . . . . . . . 10 0 ∈ (0..^(#‘⟨“𝐾”⟩))
7170a1i 11 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → 0 ∈ (0..^(#‘⟨“𝐾”⟩)))
72 ccatval3 13397 . . . . . . . . 9 ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ ∧ 0 ∈ (0..^(#‘⟨“𝐾”⟩))) → ((𝐹 ++ ⟨“𝐾”⟩)‘(0 + (#‘𝐹))) = (⟨“𝐾”⟩‘0))
7363, 64, 71, 72syl3anc 1366 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝐹 ++ ⟨“𝐾”⟩)‘(0 + (#‘𝐹))) = (⟨“𝐾”⟩‘0))
7442addid2d 10275 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (0 + (#‘𝐹)) = (#‘𝐹))
7574fveq2d 6233 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝐹 ++ ⟨“𝐾”⟩)‘(0 + (#‘𝐹))) = ((𝐹 ++ ⟨“𝐾”⟩)‘(#‘𝐹)))
76 s1fv 13427 . . . . . . . . 9 (𝐾 ∈ ℝ → (⟨“𝐾”⟩‘0) = 𝐾)
7754, 76syl 17 . . . . . . . 8 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (⟨“𝐾”⟩‘0) = 𝐾)
7873, 75, 773eqtr3d 2693 . . . . . . 7 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝐹 ++ ⟨“𝐾”⟩)‘(#‘𝐹)) = 𝐾)
7978adantr 480 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((#‘𝐹) − 1) + 1)) → ((𝐹 ++ ⟨“𝐾”⟩)‘(#‘𝐹)) = 𝐾)
8062, 79eqtrd 2685 . . . . 5 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((#‘𝐹) − 1) + 1)) → ((𝐹 ++ ⟨“𝐾”⟩)‘𝑖) = 𝐾)
8180fveq2d 6233 . . . 4 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((#‘𝐹) − 1) + 1)) → (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)) = (sgn‘𝐾))
823, 5, 20, 52, 53, 57, 81gsumnunsn 30743 . . 3 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑊 Σg (𝑖 ∈ (0...(((#‘𝐹) − 1) + 1)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))) (sgn‘𝐾)))
8359oveq2d 6706 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (0...(((#‘𝐹) − 1) + 1)) = (0...(#‘𝐹)))
8483mpteq1d 4771 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑖 ∈ (0...(((#‘𝐹) − 1) + 1)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖))) = (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖))))
8584oveq2d 6706 . . 3 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑊 Σg (𝑖 ∈ (0...(((#‘𝐹) − 1) + 1)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))) = (𝑊 Σg (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))))
8663adantr 480 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → 𝐹 ∈ Word ℝ)
8764adantr 480 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → ⟨“𝐾”⟩ ∈ Word ℝ)
8830eleq2d 2716 . . . . . . . . 9 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑖 ∈ (0..^(#‘𝐹)) ↔ 𝑖 ∈ (0...((#‘𝐹) − 1))))
8988biimpar 501 . . . . . . . 8 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → 𝑖 ∈ (0..^(#‘𝐹)))
90 ccatval1 13395 . . . . . . . 8 ((𝐹 ∈ Word ℝ ∧ ⟨“𝐾”⟩ ∈ Word ℝ ∧ 𝑖 ∈ (0..^(#‘𝐹))) → ((𝐹 ++ ⟨“𝐾”⟩)‘𝑖) = (𝐹𝑖))
9186, 87, 89, 90syl3anc 1366 . . . . . . 7 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → ((𝐹 ++ ⟨“𝐾”⟩)‘𝑖) = (𝐹𝑖))
9291fveq2d 6233 . . . . . 6 (((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈ (0...((#‘𝐹) − 1))) → (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)) = (sgn‘(𝐹𝑖)))
9392mpteq2dva 4777 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖))) = (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘(𝐹𝑖))))
9493oveq2d 6706 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))) = (𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘(𝐹𝑖)))))
9594oveq1d 6705 . . 3 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))) (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘(𝐹𝑖)))) (sgn‘𝐾)))
9682, 85, 953eqtr3d 2693 . 2 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (𝑊 Σg (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘(𝐹𝑖)))) (sgn‘𝐾)))
97 eqidd 2652 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) = (#‘𝐹))
9897olcd 407 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((#‘𝐹) ∈ (0..^(#‘𝐹)) ∨ (#‘𝐹) = (#‘𝐹)))
9927, 19syl6eleq 2740 . . . . . 6 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈ (ℤ‘0))
100 fzosplitsni 12619 . . . . . 6 ((#‘𝐹) ∈ (ℤ‘0) → ((#‘𝐹) ∈ (0..^((#‘𝐹) + 1)) ↔ ((#‘𝐹) ∈ (0..^(#‘𝐹)) ∨ (#‘𝐹) = (#‘𝐹))))
10199, 100syl 17 . . . . 5 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((#‘𝐹) ∈ (0..^((#‘𝐹) + 1)) ↔ ((#‘𝐹) ∈ (0..^(#‘𝐹)) ∨ (#‘𝐹) = (#‘𝐹))))
10298, 101mpbird 247 . . . 4 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈ (0..^((#‘𝐹) + 1)))
103102, 38eleqtrrd 2733 . . 3 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (#‘𝐹) ∈ (0..^(#‘(𝐹 ++ ⟨“𝐾”⟩))))
104 signsv.t . . . 4 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓𝑖))))))
105 signsv.v . . . 4 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇𝑓)‘𝑗) ≠ ((𝑇𝑓)‘(𝑗 − 1)), 1, 0))
1061, 2, 104, 105signstfval 30769 . . 3 (((𝐹 ++ ⟨“𝐾”⟩) ∈ Word ℝ ∧ (#‘𝐹) ∈ (0..^(#‘(𝐹 ++ ⟨“𝐾”⟩)))) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) = (𝑊 Σg (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))))
10723, 103, 106syl2anc 694 . 2 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) = (𝑊 Σg (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ ⟨“𝐾”⟩)‘𝑖)))))
108 fzo0end 12600 . . . . . 6 ((#‘𝐹) ∈ ℕ → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
10915, 108syl 17 . . . . 5 (𝐹 ∈ (Word ℝ ∖ {∅}) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹)))
1101, 2, 104, 105signstfval 30769 . . . . 5 ((𝐹 ∈ Word ℝ ∧ ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹))) → ((𝑇𝐹)‘((#‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘(𝐹𝑖)))))
1116, 109, 110syl2anc 694 . . . 4 (𝐹 ∈ (Word ℝ ∖ {∅}) → ((𝑇𝐹)‘((#‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘(𝐹𝑖)))))
112111adantr 480 . . 3 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝑇𝐹)‘((#‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘(𝐹𝑖)))))
113112oveq1d 6705 . 2 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → (((𝑇𝐹)‘((#‘𝐹) − 1)) (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘(𝐹𝑖)))) (sgn‘𝐾)))
11496, 107, 1133eqtr4d 2695 1 ((𝐹 ∈ (Word ℝ ∖ {∅}) ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ ⟨“𝐾”⟩))‘(#‘𝐹)) = (((𝑇𝐹)‘((#‘𝐹) − 1)) (sgn‘𝐾)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ≠ wne 2823   ∖ cdif 3604  ∅c0 3948  ifcif 4119  {csn 4210  {cpr 4212  {ctp 4214  ⟨cop 4216   ↦ cmpt 4762  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977  ℝ*cxr 10111   − cmin 10304  -cneg 10305  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ...cfz 12364  ..^cfzo 12504  #chash 13157  Word cword 13323   ++ cconcat 13325  ⟨“cs1 13326  sgncsgn 13870  Σcsu 14460  ndxcnx 15901  Basecbs 15904  +gcplusg 15988   Σg cgsu 16148  Mndcmnd 17341 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-seq 12842  df-hash 13158  df-word 13331  df-concat 13333  df-s1 13334  df-sgn 13871  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-plusg 16001  df-0g 16149  df-gsum 16150  df-mgm 17289  df-sgrp 17331  df-mnd 17342 This theorem is referenced by:  signsvtn0  30775  signstfvneq0  30777  signstfveq0  30782  signsvfn  30787
 Copyright terms: Public domain W3C validator