Step |
Hyp |
Ref |
Expression |
1 |
|
signsv.p |
⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) ) |
2 |
|
signsv.w |
⊢ 𝑊 = { 〈 ( Base ‘ ndx ) , { - 1 , 0 , 1 } 〉 , 〈 ( +g ‘ ndx ) , ⨣ 〉 } |
3 |
|
signsv.t |
⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) ) |
4 |
|
signsv.v |
⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) ) |
5 |
1 2 3 4
|
signstfv |
⊢ ( 𝐹 ∈ Word ℝ → ( 𝑇 ‘ 𝐹 ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) ) ) |
6 |
|
neg1rr |
⊢ - 1 ∈ ℝ |
7 |
|
0re |
⊢ 0 ∈ ℝ |
8 |
|
1re |
⊢ 1 ∈ ℝ |
9 |
|
tpssi |
⊢ ( ( - 1 ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ ) → { - 1 , 0 , 1 } ⊆ ℝ ) |
10 |
6 7 8 9
|
mp3an |
⊢ { - 1 , 0 , 1 } ⊆ ℝ |
11 |
1 2
|
signswbase |
⊢ { - 1 , 0 , 1 } = ( Base ‘ 𝑊 ) |
12 |
1 2
|
signswmnd |
⊢ 𝑊 ∈ Mnd |
13 |
12
|
a1i |
⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑊 ∈ Mnd ) |
14 |
|
fzo0ssnn0 |
⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ℕ0 |
15 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
16 |
14 15
|
sseqtri |
⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( ℤ≥ ‘ 0 ) |
17 |
16
|
a1i |
⊢ ( 𝐹 ∈ Word ℝ → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( ℤ≥ ‘ 0 ) ) |
18 |
17
|
sselda |
⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 0 ) ) |
19 |
|
wrdf |
⊢ ( 𝐹 ∈ Word ℝ → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ℝ ) |
20 |
19
|
ad2antrr |
⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ℝ ) |
21 |
|
fzssfzo |
⊢ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 0 ... 𝑛 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) |
22 |
21
|
adantl |
⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 0 ... 𝑛 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) |
23 |
22
|
sselda |
⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) |
24 |
20 23
|
ffvelrnd |
⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ ) |
25 |
24
|
rexrd |
⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ* ) |
26 |
|
sgncl |
⊢ ( ( 𝐹 ‘ 𝑖 ) ∈ ℝ* → ( sgn ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ { - 1 , 0 , 1 } ) |
27 |
25 26
|
syl |
⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( sgn ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ { - 1 , 0 , 1 } ) |
28 |
11 13 18 27
|
gsumncl |
⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) ∈ { - 1 , 0 , 1 } ) |
29 |
10 28
|
sselid |
⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝐹 ‘ 𝑖 ) ) ) ) ∈ ℝ ) |
30 |
5 29
|
fmpt3d |
⊢ ( 𝐹 ∈ Word ℝ → ( 𝑇 ‘ 𝐹 ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ℝ ) |
31 |
|
iswrdi |
⊢ ( ( 𝑇 ‘ 𝐹 ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ ℝ → ( 𝑇 ‘ 𝐹 ) ∈ Word ℝ ) |
32 |
30 31
|
syl |
⊢ ( 𝐹 ∈ Word ℝ → ( 𝑇 ‘ 𝐹 ) ∈ Word ℝ ) |