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 32103 |
. . . 4
⊢ {-1, 0,
1} = (Base‘𝑊) |
4 | 1, 2 | signswmnd 32106 |
. . . . 5
⊢ 𝑊 ∈ Mnd |
5 | 4 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝑊 ∈
Mnd) |
6 | | eldifi 4017 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → 𝐹 ∈
Word ℝ) |
7 | | lencl 13974 |
. . . . . . . . 9
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℕ0) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ∈
ℕ0) |
9 | | eldifsn 4675 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) |
10 | | hasheq0 13816 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word ℝ →
((♯‘𝐹) = 0
↔ 𝐹 =
∅)) |
11 | 10 | necon3bid 2978 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word ℝ →
((♯‘𝐹) ≠ 0
↔ 𝐹 ≠
∅)) |
12 | 11 | biimpar 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) →
(♯‘𝐹) ≠
0) |
13 | 9, 12 | sylbi 220 |
. . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ≠ 0) |
14 | | elnnne0 11990 |
. . . . . . . 8
⊢
((♯‘𝐹)
∈ ℕ ↔ ((♯‘𝐹) ∈ ℕ0 ∧
(♯‘𝐹) ≠
0)) |
15 | 8, 13, 14 | sylanbrc 586 |
. . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ∈ ℕ) |
16 | 15 | adantr 484 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (♯‘𝐹) ∈ ℕ) |
17 | | nnm1nn0 12017 |
. . . . . 6
⊢
((♯‘𝐹)
∈ ℕ → ((♯‘𝐹) − 1) ∈
ℕ0) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((♯‘𝐹) − 1) ∈
ℕ0) |
19 | | nn0uz 12362 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
20 | 18, 19 | eleqtrdi 2843 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((♯‘𝐹) − 1) ∈
(ℤ≥‘0)) |
21 | | ccatws1cl 14059 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ) |
22 | 21 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (𝐹 ++
〈“𝐾”〉) ∈ Word
ℝ) |
23 | | wrdf 13960 |
. . . . . . . . 9
⊢ ((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ → (𝐹 ++
〈“𝐾”〉):(0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))⟶ℝ) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (𝐹 ++
〈“𝐾”〉):(0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))⟶ℝ) |
25 | 7 | nn0zd 12166 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℤ) |
26 | | fzoval 13130 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹)
∈ ℤ → (0..^(♯‘𝐹)) = (0...((♯‘𝐹) − 1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ Word ℝ →
(0..^(♯‘𝐹)) =
(0...((♯‘𝐹)
− 1))) |
28 | 27 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^(♯‘𝐹)) =
(0...((♯‘𝐹)
− 1))) |
29 | | fzossfz 13147 |
. . . . . . . . . . 11
⊢
(0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹)) |
30 | 28, 29 | eqsstrrdi 3932 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0...((♯‘𝐹)
− 1)) ⊆ (0...(♯‘𝐹))) |
31 | | s1cl 14045 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℝ →
〈“𝐾”〉
∈ Word ℝ) |
32 | | ccatlen 14016 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (♯‘(𝐹 ++ 〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
33 | 31, 32 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) |
34 | | s1len 14049 |
. . . . . . . . . . . . . 14
⊢
(♯‘〈“𝐾”〉) = 1 |
35 | 34 | oveq2i 7181 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐹) +
(♯‘〈“𝐾”〉)) = ((♯‘𝐹) + 1) |
36 | 33, 35 | eqtrdi 2789 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) + 1)) |
37 | 36 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^(♯‘(𝐹 ++
〈“𝐾”〉))) =
(0..^((♯‘𝐹) +
1))) |
38 | 25 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘𝐹) ∈
ℤ) |
39 | 38 | peano2zd 12171 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
((♯‘𝐹) + 1)
∈ ℤ) |
40 | | fzoval 13130 |
. . . . . . . . . . . 12
⊢
(((♯‘𝐹)
+ 1) ∈ ℤ → (0..^((♯‘𝐹) + 1)) = (0...(((♯‘𝐹) + 1) −
1))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^((♯‘𝐹) +
1)) = (0...(((♯‘𝐹) + 1) − 1))) |
42 | 7 | nn0cnd 12038 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℂ) |
43 | | 1cnd 10714 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word ℝ → 1
∈ ℂ) |
44 | 42, 43 | pncand 11076 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word ℝ →
(((♯‘𝐹) + 1)
− 1) = (♯‘𝐹)) |
45 | 44 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(((♯‘𝐹) + 1)
− 1) = (♯‘𝐹)) |
46 | 45 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0...(((♯‘𝐹) +
1) − 1)) = (0...(♯‘𝐹))) |
47 | 37, 41, 46 | 3eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^(♯‘(𝐹 ++
〈“𝐾”〉))) = (0...(♯‘𝐹))) |
48 | 30, 47 | sseqtrrd 3918 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0...((♯‘𝐹)
− 1)) ⊆ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))) |
49 | 48 | sselda 3877 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 𝑖
∈ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))) |
50 | 24, 49 | ffvelrnd 6862 |
. . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈ ℝ) |
51 | 6, 50 | sylanl1 680 |
. . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈ ℝ) |
52 | 51 | rexrd 10769 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈
ℝ*) |
53 | | sgncl 32075 |
. . . . 5
⊢ (((𝐹 ++ 〈“𝐾”〉)‘𝑖) ∈ ℝ*
→ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)) ∈ {-1, 0, 1}) |
54 | 52, 53 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) ∈ {-1, 0, 1}) |
55 | 1, 2 | signswplusg 32104 |
. . . 4
⊢ ⨣ =
(+g‘𝑊) |
56 | | rexr 10765 |
. . . . . 6
⊢ (𝐾 ∈ ℝ → 𝐾 ∈
ℝ*) |
57 | | sgncl 32075 |
. . . . . 6
⊢ (𝐾 ∈ ℝ*
→ (sgn‘𝐾) ∈
{-1, 0, 1}) |
58 | 56, 57 | syl 17 |
. . . . 5
⊢ (𝐾 ∈ ℝ →
(sgn‘𝐾) ∈ {-1,
0, 1}) |
59 | 58 | adantl 485 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (sgn‘𝐾) ∈ {-1, 0, 1}) |
60 | | id 22 |
. . . . . . . . 9
⊢ (𝑖 = (((♯‘𝐹) − 1) + 1) → 𝑖 = (((♯‘𝐹) − 1) +
1)) |
61 | 42, 43 | npcand 11079 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word ℝ →
(((♯‘𝐹) −
1) + 1) = (♯‘𝐹)) |
62 | 61 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(((♯‘𝐹) −
1) + 1) = (♯‘𝐹)) |
63 | 60, 62 | sylan9eqr 2795 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) → 𝑖 = (♯‘𝐹)) |
64 | 63 | fveq2d 6678 |
. . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) →
((𝐹 ++ 〈“𝐾”〉)‘𝑖) = ((𝐹 ++ 〈“𝐾”〉)‘(♯‘𝐹))) |
65 | | ccatws1ls 14081 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → ((𝐹 ++ 〈“𝐾”〉)‘(♯‘𝐹)) = 𝐾) |
66 | 65 | adantr 484 |
. . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) →
((𝐹 ++ 〈“𝐾”〉)‘(♯‘𝐹)) = 𝐾) |
67 | 64, 66 | eqtrd 2773 |
. . . . . 6
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) →
((𝐹 ++ 〈“𝐾”〉)‘𝑖) = 𝐾) |
68 | 6, 67 | sylanl1 680 |
. . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((♯‘𝐹) −
1) + 1)) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) = 𝐾) |
69 | 68 | fveq2d 6678 |
. . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((♯‘𝐹) −
1) + 1)) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) = (sgn‘𝐾)) |
70 | 3, 5, 20, 54, 55, 59, 69 | gsumnunsn 32090 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(((♯‘𝐹) − 1) + 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) ⨣ (sgn‘𝐾))) |
71 | 6, 61 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) |
72 | 71 | adantr 484 |
. . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) |
73 | 72 | oveq2d 7186 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0...(((♯‘𝐹) − 1) + 1)) =
(0...(♯‘𝐹))) |
74 | 73 | mpteq1d 5119 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑖 ∈
(0...(((♯‘𝐹)
− 1) + 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...(♯‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) |
75 | 74 | oveq2d 7186 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(((♯‘𝐹) − 1) + 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) |
76 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 𝐹
∈ Word ℝ) |
77 | 31 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 〈“𝐾”〉 ∈ Word
ℝ) |
78 | 28 | eleq2d 2818 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝑖 ∈
(0..^(♯‘𝐹))
↔ 𝑖 ∈
(0...((♯‘𝐹)
− 1)))) |
79 | 78 | biimpar 481 |
. . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 𝑖
∈ (0..^(♯‘𝐹))) |
80 | | ccatval1 14019 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ ∧ 𝑖
∈ (0..^(♯‘𝐹))) → ((𝐹 ++ 〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
81 | 76, 77, 79, 80 | syl3anc 1372 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) |
82 | 81 | fveq2d 6678 |
. . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) = (sgn‘(𝐹‘𝑖))) |
83 | 82 | mpteq2dva 5125 |
. . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖)))) |
84 | 6, 83 | sylan 583 |
. . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖)))) |
85 | 84 | oveq2d 7186 |
. . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) |
86 | 85 | oveq1d 7185 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑊
Σg (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) ⨣ (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) |
87 | 70, 75, 86 | 3eqtr3d 2781 |
. 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(♯‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) |
88 | | eqid 2738 |
. . . . . . . 8
⊢
(♯‘𝐹) =
(♯‘𝐹) |
89 | 88 | olci 865 |
. . . . . . 7
⊢
((♯‘𝐹)
∈ (0..^(♯‘𝐹)) ∨ (♯‘𝐹) = (♯‘𝐹)) |
90 | 7, 19 | eleqtrdi 2843 |
. . . . . . . 8
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
(ℤ≥‘0)) |
91 | | fzosplitsni 13239 |
. . . . . . . 8
⊢
((♯‘𝐹)
∈ (ℤ≥‘0) → ((♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1)) ↔ ((♯‘𝐹) ∈ (0..^(♯‘𝐹)) ∨ (♯‘𝐹) = (♯‘𝐹)))) |
92 | 90, 91 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ Word ℝ →
((♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1)) ↔ ((♯‘𝐹) ∈ (0..^(♯‘𝐹)) ∨ (♯‘𝐹) = (♯‘𝐹)))) |
93 | 89, 92 | mpbiri 261 |
. . . . . 6
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1))) |
94 | 93 | adantr 484 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1))) |
95 | 94, 37 | eleqtrrd 2836 |
. . . 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 32113 |
. . . 4
⊢ (((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ ∧ (♯‘𝐹) ∈ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) |
99 | 21, 95, 98 | syl2anc 587 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) |
100 | 6, 99 | sylan 583 |
. 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) |
101 | | fzo0end 13220 |
. . . . . 6
⊢
((♯‘𝐹)
∈ ℕ → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) |
102 | 15, 101 | syl 17 |
. . . . 5
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) |
103 | 1, 2, 96, 97 | signstfval 32113 |
. . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧
((♯‘𝐹) −
1) ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) |
104 | 6, 102, 103 | syl2anc 587 |
. . . 4
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) |
105 | 104 | adantr 484 |
. . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) |
106 | 105 | oveq1d 7185 |
. 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) |
107 | 87, 100, 106 | 3eqtr4d 2783 |
1
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾))) |