Proof of Theorem signstfvp
Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → 𝐹 ∈ Word ℝ) |
2 | | s1cl 14057 |
. . . . . . . 8
⊢ (𝐾 ∈ ℝ →
〈“𝐾”〉
∈ Word ℝ) |
3 | 2 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ 〈“𝐾”〉 ∈ Word
ℝ) |
4 | 3 | adantr 484 |
. . . . . 6
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → 〈“𝐾”〉 ∈ Word
ℝ) |
5 | | fzssfzo 32100 |
. . . . . . . 8
⊢ (𝑁 ∈
(0..^(♯‘𝐹))
→ (0...𝑁) ⊆
(0..^(♯‘𝐹))) |
6 | 5 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (0...𝑁) ⊆
(0..^(♯‘𝐹))) |
7 | 6 | sselda 3887 |
. . . . . 6
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0..^(♯‘𝐹))) |
8 | | ccatval1 14031 |
. . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ ∧ 𝑖
∈ (0..^(♯‘𝐹))) → ((𝐹 ++ 〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
9 | 1, 4, 7, 8 | syl3anc 1372 |
. . . . 5
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → ((𝐹 ++ 〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
10 | 9 | fveq2d 6690 |
. . . 4
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) = (sgn‘(𝐹‘𝑖))) |
11 | 10 | mpteq2dva 5135 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖)))) |
12 | 11 | oveq2d 7198 |
. 2
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (𝑊
Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖))))) |
13 | | ccatws1cl 14071 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ) |
14 | 13 | 3adant3 1133 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (𝐹 ++
〈“𝐾”〉) ∈ Word
ℝ) |
15 | | lencl 13986 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℕ0) |
16 | 15 | nn0zd 12178 |
. . . . . . . 8
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℤ) |
17 | 16 | uzidd 12352 |
. . . . . . 7
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
(ℤ≥‘(♯‘𝐹))) |
18 | | peano2uz 12395 |
. . . . . . 7
⊢
((♯‘𝐹)
∈ (ℤ≥‘(♯‘𝐹)) → ((♯‘𝐹) + 1) ∈
(ℤ≥‘(♯‘𝐹))) |
19 | | fzoss2 13168 |
. . . . . . 7
⊢
(((♯‘𝐹)
+ 1) ∈ (ℤ≥‘(♯‘𝐹)) → (0..^(♯‘𝐹)) ⊆
(0..^((♯‘𝐹) +
1))) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . 6
⊢ (𝐹 ∈ Word ℝ →
(0..^(♯‘𝐹))
⊆ (0..^((♯‘𝐹) + 1))) |
21 | 20 | sselda 3887 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ 𝑁 ∈
(0..^((♯‘𝐹) +
1))) |
22 | 21 | 3adant2 1132 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ 𝑁 ∈
(0..^((♯‘𝐹) +
1))) |
23 | | ccatlen 14028 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (♯‘(𝐹 ++ 〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
24 | 2, 23 | sylan2 596 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
25 | 24 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
26 | | s1len 14061 |
. . . . . . 7
⊢
(♯‘〈“𝐾”〉) = 1 |
27 | 26 | oveq2i 7193 |
. . . . . 6
⊢
((♯‘𝐹) +
(♯‘〈“𝐾”〉)) = ((♯‘𝐹) + 1) |
28 | 25, 27 | eqtrdi 2790 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) + 1)) |
29 | 28 | oveq2d 7198 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉))) =
(0..^((♯‘𝐹) +
1))) |
30 | 22, 29 | eleqtrrd 2837 |
. . 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 32125 |
. . 3
⊢ (((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ ∧ 𝑁 ∈
(0..^(♯‘(𝐹 ++
〈“𝐾”〉)))) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑁) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))))) |
36 | 14, 30, 35 | syl2anc 587 |
. 2
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑁) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))))) |
37 | 31, 32, 33, 34 | signstfval 32125 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘𝐹)‘𝑁) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖))))) |
38 | 37 | 3adant2 1132 |
. 2
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘𝐹)‘𝑁) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖))))) |
39 | 12, 36, 38 | 3eqtr4d 2784 |
1
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |