Proof of Theorem signstfvp
| Step | Hyp | Ref
| Expression |
| 1 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → 𝐹 ∈ Word ℝ) |
| 2 | | s1cl 14640 |
. . . . . . . 8
⊢ (𝐾 ∈ ℝ →
〈“𝐾”〉
∈ Word ℝ) |
| 3 | 2 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ 〈“𝐾”〉 ∈ Word
ℝ) |
| 4 | 3 | adantr 480 |
. . . . . 6
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → 〈“𝐾”〉 ∈ Word
ℝ) |
| 5 | | fzssfzo 34554 |
. . . . . . . 8
⊢ (𝑁 ∈
(0..^(♯‘𝐹))
→ (0...𝑁) ⊆
(0..^(♯‘𝐹))) |
| 6 | 5 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (0...𝑁) ⊆
(0..^(♯‘𝐹))) |
| 7 | 6 | sselda 3983 |
. . . . . 6
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → 𝑖 ∈ (0..^(♯‘𝐹))) |
| 8 | | ccatval1 14615 |
. . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ ∧ 𝑖
∈ (0..^(♯‘𝐹))) → ((𝐹 ++ 〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
| 9 | 1, 4, 7, 8 | syl3anc 1373 |
. . . . 5
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → ((𝐹 ++ 〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
| 10 | 9 | fveq2d 6910 |
. . . 4
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
∧ 𝑖 ∈ (0...𝑁)) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) = (sgn‘(𝐹‘𝑖))) |
| 11 | 10 | mpteq2dva 5242 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖)))) |
| 12 | 11 | oveq2d 7447 |
. 2
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (𝑊
Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖))))) |
| 13 | | ccatws1cl 14654 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ) |
| 14 | 13 | 3adant3 1133 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (𝐹 ++
〈“𝐾”〉) ∈ Word
ℝ) |
| 15 | | lencl 14571 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℕ0) |
| 16 | 15 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℤ) |
| 17 | 16 | uzidd 12894 |
. . . . . . 7
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
(ℤ≥‘(♯‘𝐹))) |
| 18 | | peano2uz 12943 |
. . . . . . 7
⊢
((♯‘𝐹)
∈ (ℤ≥‘(♯‘𝐹)) → ((♯‘𝐹) + 1) ∈
(ℤ≥‘(♯‘𝐹))) |
| 19 | | fzoss2 13727 |
. . . . . . 7
⊢
(((♯‘𝐹)
+ 1) ∈ (ℤ≥‘(♯‘𝐹)) → (0..^(♯‘𝐹)) ⊆
(0..^((♯‘𝐹) +
1))) |
| 20 | 17, 18, 19 | 3syl 18 |
. . . . . 6
⊢ (𝐹 ∈ Word ℝ →
(0..^(♯‘𝐹))
⊆ (0..^((♯‘𝐹) + 1))) |
| 21 | 20 | sselda 3983 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ 𝑁 ∈
(0..^((♯‘𝐹) +
1))) |
| 22 | 21 | 3adant2 1132 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ 𝑁 ∈
(0..^((♯‘𝐹) +
1))) |
| 23 | | ccatlen 14613 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (♯‘(𝐹 ++ 〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
| 24 | 2, 23 | sylan2 593 |
. . . . . . 7
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
| 25 | 24 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
| 26 | | s1len 14644 |
. . . . . . 7
⊢
(♯‘〈“𝐾”〉) = 1 |
| 27 | 26 | oveq2i 7442 |
. . . . . 6
⊢
((♯‘𝐹) +
(♯‘〈“𝐾”〉)) = ((♯‘𝐹) + 1) |
| 28 | 25, 27 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) + 1)) |
| 29 | 28 | oveq2d 7447 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉))) =
(0..^((♯‘𝐹) +
1))) |
| 30 | 22, 29 | eleqtrrd 2844 |
. . 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 34579 |
. . 3
⊢ (((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ ∧ 𝑁 ∈
(0..^(♯‘(𝐹 ++
〈“𝐾”〉)))) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑁) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))))) |
| 36 | 14, 30, 35 | syl2anc 584 |
. 2
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑁) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))))) |
| 37 | 31, 32, 33, 34 | signstfval 34579 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘𝐹)‘𝑁) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖))))) |
| 38 | 37 | 3adant2 1132 |
. 2
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘𝐹)‘𝑁) = (𝑊 Σg (𝑖 ∈ (0...𝑁) ↦ (sgn‘(𝐹‘𝑖))))) |
| 39 | 12, 36, 38 | 3eqtr4d 2787 |
1
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |