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 30631 |
. . . 4
⊢ {-1, 0,
1} = (Base‘𝑊) |
4 | 1, 2 | signswmnd 30634 |
. . . . 5
⊢ 𝑊 ∈ Mnd |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝑊 ∈
Mnd) |
6 | | eldifi 3732 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → 𝐹 ∈
Word ℝ) |
7 | | lencl 13324 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word ℝ →
(#‘𝐹) ∈
ℕ0) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (#‘𝐹) ∈
ℕ0) |
9 | | eldifsn 4317 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) |
10 | | hasheq0 13154 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word ℝ →
((#‘𝐹) = 0 ↔
𝐹 =
∅)) |
11 | 10 | necon3bid 2838 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word ℝ →
((#‘𝐹) ≠ 0 ↔
𝐹 ≠
∅)) |
12 | 11 | biimpar 502 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) →
(#‘𝐹) ≠
0) |
13 | 9, 12 | sylbi 207 |
. . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (#‘𝐹) ≠ 0) |
14 | | elnnne0 11306 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
ℕ ↔ ((#‘𝐹)
∈ ℕ0 ∧ (#‘𝐹) ≠ 0)) |
15 | 8, 13, 14 | sylanbrc 698 |
. . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (#‘𝐹) ∈ ℕ) |
16 | 15 | adantr 481 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘𝐹)
∈ ℕ) |
17 | | nnm1nn0 11334 |
. . . . . 6
⊢
((#‘𝐹) ∈
ℕ → ((#‘𝐹)
− 1) ∈ ℕ0) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((#‘𝐹) − 1) ∈
ℕ0) |
19 | | nn0uz 11722 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
20 | 18, 19 | syl6eleq 2711 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((#‘𝐹) − 1) ∈
(ℤ≥‘0)) |
21 | | s1cl 13382 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℝ →
〈“𝐾”〉
∈ Word ℝ) |
22 | | ccatcl 13359 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ) |
23 | 6, 21, 22 | syl2an 494 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝐹 ++
〈“𝐾”〉) ∈ Word
ℝ) |
24 | 23 | adantr 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → (𝐹 ++
〈“𝐾”〉) ∈ Word
ℝ) |
25 | | wrdf 13310 |
. . . . . . . 8
⊢ ((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ → (𝐹 ++
〈“𝐾”〉):(0..^(#‘(𝐹 ++ 〈“𝐾”〉)))⟶ℝ) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → (𝐹 ++
〈“𝐾”〉):(0..^(#‘(𝐹 ++ 〈“𝐾”〉)))⟶ℝ) |
27 | 8 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘𝐹)
∈ ℕ0) |
28 | 27 | nn0zd 11480 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘𝐹)
∈ ℤ) |
29 | | fzoval 12471 |
. . . . . . . . . . 11
⊢
((#‘𝐹) ∈
ℤ → (0..^(#‘𝐹)) = (0...((#‘𝐹) − 1))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0..^(#‘𝐹)) = (0...((#‘𝐹) − 1))) |
31 | | fzossfz 12488 |
. . . . . . . . . 10
⊢
(0..^(#‘𝐹))
⊆ (0...(#‘𝐹)) |
32 | 30, 31 | syl6eqssr 3656 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0...((#‘𝐹) − 1)) ⊆ (0...(#‘𝐹))) |
33 | | ccatlen 13360 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (#‘(𝐹 ++ 〈“𝐾”〉)) = ((#‘𝐹) + (#‘〈“𝐾”〉))) |
34 | 6, 21, 33 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘(𝐹
++ 〈“𝐾”〉)) = ((#‘𝐹) + (#‘〈“𝐾”〉))) |
35 | | s1len 13385 |
. . . . . . . . . . . . 13
⊢
(#‘〈“𝐾”〉) = 1 |
36 | 35 | oveq2i 6661 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) +
(#‘〈“𝐾”〉)) = ((#‘𝐹) + 1) |
37 | 34, 36 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘(𝐹
++ 〈“𝐾”〉)) = ((#‘𝐹) + 1)) |
38 | 37 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0..^(#‘(𝐹 ++ 〈“𝐾”〉))) = (0..^((#‘𝐹) + 1))) |
39 | 28 | peano2zd 11485 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((#‘𝐹) + 1) ∈ ℤ) |
40 | | fzoval 12471 |
. . . . . . . . . . 11
⊢
(((#‘𝐹) + 1)
∈ ℤ → (0..^((#‘𝐹) + 1)) = (0...(((#‘𝐹) + 1) − 1))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0..^((#‘𝐹) + 1)) = (0...(((#‘𝐹) + 1) − 1))) |
42 | 27 | nn0cnd 11353 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘𝐹)
∈ ℂ) |
43 | | 1cnd 10056 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 1 ∈ ℂ) |
44 | 42, 43 | pncand 10393 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (((#‘𝐹) + 1) − 1) = (#‘𝐹)) |
45 | 44 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0...(((#‘𝐹) + 1) − 1)) = (0...(#‘𝐹))) |
46 | 38, 41, 45 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0..^(#‘(𝐹 ++ 〈“𝐾”〉))) = (0...(#‘𝐹))) |
47 | 32, 46 | sseqtr4d 3642 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0...((#‘𝐹) − 1)) ⊆ (0..^(#‘(𝐹 ++ 〈“𝐾”〉)))) |
48 | 47 | sselda 3603 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → 𝑖 ∈
(0..^(#‘(𝐹 ++
〈“𝐾”〉)))) |
49 | 26, 48 | ffvelrnd 6360 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈ ℝ) |
50 | 49 | rexrd 10089 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈
ℝ*) |
51 | | sgncl 30600 |
. . . . 5
⊢ (((𝐹 ++ 〈“𝐾”〉)‘𝑖) ∈ ℝ*
→ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)) ∈ {-1, 0, 1}) |
52 | 50, 51 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → (sgn‘((𝐹
++ 〈“𝐾”〉)‘𝑖)) ∈ {-1, 0, 1}) |
53 | 1, 2 | signswplusg 30632 |
. . . 4
⊢ ⨣ =
(+g‘𝑊) |
54 | | simpr 477 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝐾 ∈
ℝ) |
55 | 54 | rexrd 10089 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝐾 ∈
ℝ*) |
56 | | sgncl 30600 |
. . . . 5
⊢ (𝐾 ∈ ℝ*
→ (sgn‘𝐾) ∈
{-1, 0, 1}) |
57 | 55, 56 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (sgn‘𝐾) ∈ {-1, 0, 1}) |
58 | | simpr 477 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((#‘𝐹) − 1) +
1)) → 𝑖 =
(((#‘𝐹) − 1) +
1)) |
59 | 42, 43 | npcand 10396 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (((#‘𝐹) − 1) + 1) = (#‘𝐹)) |
60 | 59 | adantr 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((#‘𝐹) − 1) +
1)) → (((#‘𝐹)
− 1) + 1) = (#‘𝐹)) |
61 | 58, 60 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((#‘𝐹) − 1) +
1)) → 𝑖 =
(#‘𝐹)) |
62 | 61 | fveq2d 6195 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((#‘𝐹) − 1) +
1)) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) = ((𝐹 ++ 〈“𝐾”〉)‘(#‘𝐹))) |
63 | 6 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝐹 ∈
Word ℝ) |
64 | 54, 21 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 〈“𝐾”〉 ∈ Word
ℝ) |
65 | | c0ex 10034 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
66 | 65 | snid 4208 |
. . . . . . . . . . . 12
⊢ 0 ∈
{0} |
67 | | fzo01 12550 |
. . . . . . . . . . . 12
⊢ (0..^1) =
{0} |
68 | 66, 67 | eleqtrri 2700 |
. . . . . . . . . . 11
⊢ 0 ∈
(0..^1) |
69 | 35 | oveq2i 6661 |
. . . . . . . . . . 11
⊢
(0..^(#‘〈“𝐾”〉)) = (0..^1) |
70 | 68, 69 | eleqtrri 2700 |
. . . . . . . . . 10
⊢ 0 ∈
(0..^(#‘〈“𝐾”〉)) |
71 | 70 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 0 ∈ (0..^(#‘〈“𝐾”〉))) |
72 | | ccatval3 13363 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ ∧ 0 ∈ (0..^(#‘〈“𝐾”〉))) → ((𝐹 ++ 〈“𝐾”〉)‘(0 + (#‘𝐹))) = (〈“𝐾”〉‘0)) |
73 | 63, 64, 71, 72 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝐹 ++
〈“𝐾”〉)‘(0 + (#‘𝐹))) = (〈“𝐾”〉‘0)) |
74 | 42 | addid2d 10237 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0 + (#‘𝐹)) = (#‘𝐹)) |
75 | 74 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝐹 ++
〈“𝐾”〉)‘(0 + (#‘𝐹))) = ((𝐹 ++ 〈“𝐾”〉)‘(#‘𝐹))) |
76 | | s1fv 13390 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) = 𝐾) |
77 | 54, 76 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (〈“𝐾”〉‘0) = 𝐾) |
78 | 73, 75, 77 | 3eqtr3d 2664 |
. . . . . . 7
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝐹 ++
〈“𝐾”〉)‘(#‘𝐹)) = 𝐾) |
79 | 78 | adantr 481 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((#‘𝐹) − 1) +
1)) → ((𝐹 ++
〈“𝐾”〉)‘(#‘𝐹)) = 𝐾) |
80 | 62, 79 | eqtrd 2656 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((#‘𝐹) − 1) +
1)) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) = 𝐾) |
81 | 80 | fveq2d 6195 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((#‘𝐹) − 1) +
1)) → (sgn‘((𝐹
++ 〈“𝐾”〉)‘𝑖)) = (sgn‘𝐾)) |
82 | 3, 5, 20, 52, 53, 57, 81 | gsumnunsn 30615 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(((#‘𝐹) − 1) + 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) ⨣ (sgn‘𝐾))) |
83 | 59 | oveq2d 6666 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0...(((#‘𝐹) − 1) + 1)) = (0...(#‘𝐹))) |
84 | 83 | mpteq1d 4738 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑖 ∈
(0...(((#‘𝐹) −
1) + 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) |
85 | 84 | oveq2d 6666 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(((#‘𝐹) − 1) + 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))))) |
86 | 63 | adantr 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → 𝐹 ∈ Word
ℝ) |
87 | 64 | adantr 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → 〈“𝐾”〉 ∈ Word
ℝ) |
88 | 30 | eleq2d 2687 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑖 ∈
(0..^(#‘𝐹)) ↔
𝑖 ∈
(0...((#‘𝐹) −
1)))) |
89 | 88 | biimpar 502 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → 𝑖 ∈
(0..^(#‘𝐹))) |
90 | | ccatval1 13361 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ ∧ 𝑖
∈ (0..^(#‘𝐹)))
→ ((𝐹 ++
〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
91 | 86, 87, 89, 90 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
92 | 91 | fveq2d 6195 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((#‘𝐹) −
1))) → (sgn‘((𝐹
++ 〈“𝐾”〉)‘𝑖)) = (sgn‘(𝐹‘𝑖))) |
93 | 92 | mpteq2dva 4744 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑖 ∈
(0...((#‘𝐹) −
1)) ↦ (sgn‘((𝐹
++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘(𝐹‘𝑖)))) |
94 | 93 | oveq2d 6666 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖))))) |
95 | 94 | oveq1d 6665 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑊
Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) ⨣ (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) |
96 | 82, 85, 95 | 3eqtr3d 2664 |
. 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) |
97 | | eqidd 2623 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘𝐹)
= (#‘𝐹)) |
98 | 97 | olcd 408 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((#‘𝐹) ∈ (0..^(#‘𝐹)) ∨ (#‘𝐹) = (#‘𝐹))) |
99 | 27, 19 | syl6eleq 2711 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘𝐹)
∈ (ℤ≥‘0)) |
100 | | fzosplitsni 12579 |
. . . . . 6
⊢
((#‘𝐹) ∈
(ℤ≥‘0) → ((#‘𝐹) ∈ (0..^((#‘𝐹) + 1)) ↔ ((#‘𝐹) ∈ (0..^(#‘𝐹)) ∨ (#‘𝐹) = (#‘𝐹)))) |
101 | 99, 100 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((#‘𝐹) ∈ (0..^((#‘𝐹) + 1)) ↔ ((#‘𝐹) ∈ (0..^(#‘𝐹)) ∨ (#‘𝐹) = (#‘𝐹)))) |
102 | 98, 101 | mpbird 247 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘𝐹)
∈ (0..^((#‘𝐹) +
1))) |
103 | 102, 38 | eleqtrrd 2704 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (#‘𝐹)
∈ (0..^(#‘(𝐹 ++
〈“𝐾”〉)))) |
104 | | signsv.t |
. . . 4
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
105 | | signsv.v |
. . . 4
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
106 | 1, 2, 104, 105 | signstfval 30641 |
. . 3
⊢ (((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ ∧ (#‘𝐹)
∈ (0..^(#‘(𝐹 ++
〈“𝐾”〉)))) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) = (𝑊 Σg (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))))) |
107 | 23, 103, 106 | syl2anc 693 |
. 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) = (𝑊 Σg (𝑖 ∈ (0...(#‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))))) |
108 | | fzo0end 12560 |
. . . . . 6
⊢
((#‘𝐹) ∈
ℕ → ((#‘𝐹)
− 1) ∈ (0..^(#‘𝐹))) |
109 | 15, 108 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ((#‘𝐹) − 1) ∈ (0..^(#‘𝐹))) |
110 | 1, 2, 104, 105 | signstfval 30641 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧
((#‘𝐹) − 1)
∈ (0..^(#‘𝐹)))
→ ((𝑇‘𝐹)‘((#‘𝐹) − 1)) = (𝑊 Σg
(𝑖 ∈
(0...((#‘𝐹) −
1)) ↦ (sgn‘(𝐹‘𝑖))))) |
111 | 6, 109, 110 | syl2anc 693 |
. . . 4
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ((𝑇‘𝐹)‘((#‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖))))) |
112 | 111 | adantr 481 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘𝐹)‘((#‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖))))) |
113 | 112 | oveq1d 6665 |
. 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (((𝑇‘𝐹)‘((#‘𝐹) − 1)) ⨣ (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈ (0...((#‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) |
114 | 96, 107, 113 | 3eqtr4d 2666 |
1
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(#‘𝐹)) = (((𝑇‘𝐹)‘((#‘𝐹) − 1)) ⨣ (sgn‘𝐾))) |