Proof of Theorem signstfvn
Step | Hyp | Ref
| Expression |
1 | | signsv.p |
. . . . 5
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
2 | | signsv.w |
. . . . 5
⊢ 𝑊 = {〈(Base‘ndx), {-1,
0, 1}〉, 〈(+g‘ndx), ⨣
〉} |
3 | 1, 2 | signswbase 32533 |
. . . 4
⊢ {-1, 0,
1} = (Base‘𝑊) |
4 | 1, 2 | signswmnd 32536 |
. . . . 5
⊢ 𝑊 ∈ Mnd |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝑊 ∈
Mnd) |
6 | | eldifi 4061 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → 𝐹 ∈
Word ℝ) |
7 | | lencl 14236 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℕ0) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ∈
ℕ0) |
9 | | eldifsn 4720 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) |
10 | | hasheq0 14078 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word ℝ →
((♯‘𝐹) = 0
↔ 𝐹 =
∅)) |
11 | 10 | necon3bid 2988 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word ℝ →
((♯‘𝐹) ≠ 0
↔ 𝐹 ≠
∅)) |
12 | 11 | biimpar 478 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) →
(♯‘𝐹) ≠
0) |
13 | 9, 12 | sylbi 216 |
. . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ≠ 0) |
14 | | elnnne0 12247 |
. . . . . . . 8
⊢
((♯‘𝐹)
∈ ℕ ↔ ((♯‘𝐹) ∈ ℕ0 ∧
(♯‘𝐹) ≠
0)) |
15 | 8, 13, 14 | sylanbrc 583 |
. . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ∈ ℕ) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (♯‘𝐹) ∈ ℕ) |
17 | | nnm1nn0 12274 |
. . . . . 6
⊢
((♯‘𝐹)
∈ ℕ → ((♯‘𝐹) − 1) ∈
ℕ0) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((♯‘𝐹) − 1) ∈
ℕ0) |
19 | | nn0uz 12620 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
20 | 18, 19 | eleqtrdi 2849 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((♯‘𝐹) − 1) ∈
(ℤ≥‘0)) |
21 | | ccatws1cl 14321 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (𝐹 ++
〈“𝐾”〉) ∈ Word
ℝ) |
23 | | wrdf 14222 |
. . . . . . . . 9
⊢ ((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ → (𝐹 ++
〈“𝐾”〉):(0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))⟶ℝ) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (𝐹 ++
〈“𝐾”〉):(0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))⟶ℝ) |
25 | 7 | nn0zd 12424 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℤ) |
26 | | fzoval 13388 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹)
∈ ℤ → (0..^(♯‘𝐹)) = (0...((♯‘𝐹) − 1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ Word ℝ →
(0..^(♯‘𝐹)) =
(0...((♯‘𝐹)
− 1))) |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^(♯‘𝐹)) =
(0...((♯‘𝐹)
− 1))) |
29 | | fzossfz 13406 |
. . . . . . . . . . 11
⊢
(0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹)) |
30 | 28, 29 | eqsstrrdi 3976 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0...((♯‘𝐹)
− 1)) ⊆ (0...(♯‘𝐹))) |
31 | | s1cl 14307 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℝ →
〈“𝐾”〉
∈ Word ℝ) |
32 | | ccatlen 14278 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (♯‘(𝐹 ++ 〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
33 | 31, 32 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
34 | | s1len 14311 |
. . . . . . . . . . . . . 14
⊢
(♯‘〈“𝐾”〉) = 1 |
35 | 34 | oveq2i 7286 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹) +
(♯‘〈“𝐾”〉)) = ((♯‘𝐹) + 1) |
36 | 33, 35 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) + 1)) |
37 | 36 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^(♯‘(𝐹 ++
〈“𝐾”〉))) =
(0..^((♯‘𝐹) +
1))) |
38 | 25 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘𝐹) ∈
ℤ) |
39 | 38 | peano2zd 12429 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
((♯‘𝐹) + 1)
∈ ℤ) |
40 | | fzoval 13388 |
. . . . . . . . . . . 12
⊢
(((♯‘𝐹)
+ 1) ∈ ℤ → (0..^((♯‘𝐹) + 1)) = (0...(((♯‘𝐹) + 1) −
1))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^((♯‘𝐹) +
1)) = (0...(((♯‘𝐹) + 1) − 1))) |
42 | 7 | nn0cnd 12295 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℂ) |
43 | | 1cnd 10970 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word ℝ → 1
∈ ℂ) |
44 | 42, 43 | pncand 11333 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word ℝ →
(((♯‘𝐹) + 1)
− 1) = (♯‘𝐹)) |
45 | 44 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(((♯‘𝐹) + 1)
− 1) = (♯‘𝐹)) |
46 | 45 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0...(((♯‘𝐹) +
1) − 1)) = (0...(♯‘𝐹))) |
47 | 37, 41, 46 | 3eqtrd 2782 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^(♯‘(𝐹 ++
〈“𝐾”〉))) = (0...(♯‘𝐹))) |
48 | 30, 47 | sseqtrrd 3962 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0...((♯‘𝐹)
− 1)) ⊆ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))) |
49 | 48 | sselda 3921 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 𝑖
∈ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))) |
50 | 24, 49 | ffvelrnd 6962 |
. . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈ ℝ) |
51 | 6, 50 | sylanl1 677 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈ ℝ) |
52 | 51 | rexrd 11025 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈
ℝ*) |
53 | | sgncl 32505 |
. . . . 5
⊢ (((𝐹 ++ 〈“𝐾”〉)‘𝑖) ∈ ℝ*
→ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)) ∈ {-1, 0, 1}) |
54 | 52, 53 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) ∈ {-1, 0, 1}) |
55 | 1, 2 | signswplusg 32534 |
. . . 4
⊢ ⨣ =
(+g‘𝑊) |
56 | | rexr 11021 |
. . . . . 6
⊢ (𝐾 ∈ ℝ → 𝐾 ∈
ℝ*) |
57 | | sgncl 32505 |
. . . . . 6
⊢ (𝐾 ∈ ℝ*
→ (sgn‘𝐾) ∈
{-1, 0, 1}) |
58 | 56, 57 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ ℝ →
(sgn‘𝐾) ∈ {-1,
0, 1}) |
59 | 58 | adantl 482 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (sgn‘𝐾) ∈ {-1, 0, 1}) |
60 | | id 22 |
. . . . . . . . 9
⊢ (𝑖 = (((♯‘𝐹) − 1) + 1) → 𝑖 = (((♯‘𝐹) − 1) +
1)) |
61 | 42, 43 | npcand 11336 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word ℝ →
(((♯‘𝐹) −
1) + 1) = (♯‘𝐹)) |
62 | 61 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(((♯‘𝐹) −
1) + 1) = (♯‘𝐹)) |
63 | 60, 62 | sylan9eqr 2800 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) → 𝑖 = (♯‘𝐹)) |
64 | 63 | fveq2d 6778 |
. . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) →
((𝐹 ++ 〈“𝐾”〉)‘𝑖) = ((𝐹 ++ 〈“𝐾”〉)‘(♯‘𝐹))) |
65 | | ccatws1ls 14343 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → ((𝐹 ++ 〈“𝐾”〉)‘(♯‘𝐹)) = 𝐾) |
66 | 65 | adantr 481 |
. . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) →
((𝐹 ++ 〈“𝐾”〉)‘(♯‘𝐹)) = 𝐾) |
67 | 64, 66 | eqtrd 2778 |
. . . . . 6
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) →
((𝐹 ++ 〈“𝐾”〉)‘𝑖) = 𝐾) |
68 | 6, 67 | sylanl1 677 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((♯‘𝐹) −
1) + 1)) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) = 𝐾) |
69 | 68 | fveq2d 6778 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((♯‘𝐹) −
1) + 1)) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) = (sgn‘𝐾)) |
70 | 3, 5, 20, 54, 55, 59, 69 | gsumnunsn 32520 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(((♯‘𝐹) − 1) + 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) ⨣ (sgn‘𝐾))) |
71 | 6, 61 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) |
72 | 71 | adantr 481 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) |
73 | 72 | oveq2d 7291 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0...(((♯‘𝐹) − 1) + 1)) =
(0...(♯‘𝐹))) |
74 | 73 | mpteq1d 5169 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑖 ∈
(0...(((♯‘𝐹)
− 1) + 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...(♯‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) |
75 | 74 | oveq2d 7291 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(((♯‘𝐹) − 1) + 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) |
76 | | simpll 764 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 𝐹
∈ Word ℝ) |
77 | 31 | ad2antlr 724 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 〈“𝐾”〉 ∈ Word
ℝ) |
78 | 28 | eleq2d 2824 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝑖 ∈
(0..^(♯‘𝐹))
↔ 𝑖 ∈
(0...((♯‘𝐹)
− 1)))) |
79 | 78 | biimpar 478 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 𝑖
∈ (0..^(♯‘𝐹))) |
80 | | ccatval1 14281 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ ∧ 𝑖
∈ (0..^(♯‘𝐹))) → ((𝐹 ++ 〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
81 | 76, 77, 79, 80 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
82 | 81 | fveq2d 6778 |
. . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) = (sgn‘(𝐹‘𝑖))) |
83 | 82 | mpteq2dva 5174 |
. . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖)))) |
84 | 6, 83 | sylan 580 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖)))) |
85 | 84 | oveq2d 7291 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) |
86 | 85 | oveq1d 7290 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑊
Σg (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) ⨣ (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) |
87 | 70, 75, 86 | 3eqtr3d 2786 |
. 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(♯‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) |
88 | | eqid 2738 |
. . . . . . . 8
⊢
(♯‘𝐹) =
(♯‘𝐹) |
89 | 88 | olci 863 |
. . . . . . 7
⊢
((♯‘𝐹)
∈ (0..^(♯‘𝐹)) ∨ (♯‘𝐹) = (♯‘𝐹)) |
90 | 7, 19 | eleqtrdi 2849 |
. . . . . . . 8
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
(ℤ≥‘0)) |
91 | | fzosplitsni 13498 |
. . . . . . . 8
⊢
((♯‘𝐹)
∈ (ℤ≥‘0) → ((♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1)) ↔ ((♯‘𝐹) ∈ (0..^(♯‘𝐹)) ∨ (♯‘𝐹) = (♯‘𝐹)))) |
92 | 90, 91 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ Word ℝ →
((♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1)) ↔ ((♯‘𝐹) ∈ (0..^(♯‘𝐹)) ∨ (♯‘𝐹) = (♯‘𝐹)))) |
93 | 89, 92 | mpbiri 257 |
. . . . . 6
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1))) |
94 | 93 | adantr 481 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1))) |
95 | 94, 37 | eleqtrrd 2842 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘𝐹) ∈
(0..^(♯‘(𝐹 ++
〈“𝐾”〉)))) |
96 | | signsv.t |
. . . . 5
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈
(0..^(♯‘𝑓))
↦ (𝑊
Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
97 | | signsv.v |
. . . . 5
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈
(1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
98 | 1, 2, 96, 97 | signstfval 32543 |
. . . 4
⊢ (((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ ∧ (♯‘𝐹) ∈ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) |
99 | 21, 95, 98 | syl2anc 584 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) |
100 | 6, 99 | sylan 580 |
. 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) |
101 | | fzo0end 13479 |
. . . . . 6
⊢
((♯‘𝐹)
∈ ℕ → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) |
102 | 15, 101 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) |
103 | 1, 2, 96, 97 | signstfval 32543 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧
((♯‘𝐹) −
1) ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) |
104 | 6, 102, 103 | syl2anc 584 |
. . . 4
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) |
105 | 104 | adantr 481 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) |
106 | 105 | oveq1d 7290 |
. 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) |
107 | 87, 100, 106 | 3eqtr4d 2788 |
1
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾))) |