Proof of Theorem signstf0
Step | Hyp | Ref
| Expression |
1 | | s1len 13238 |
. . . . . 6
⊢
(#‘〈“𝐾”〉) = 1 |
2 | 1 | oveq2i 6560 |
. . . . 5
⊢
(0..^(#‘〈“𝐾”〉)) = (0..^1) |
3 | | fzo01 12417 |
. . . . 5
⊢ (0..^1) =
{0} |
4 | 2, 3 | eqtri 2632 |
. . . 4
⊢
(0..^(#‘〈“𝐾”〉)) = {0} |
5 | 4 | a1i 11 |
. . 3
⊢ (𝐾 ∈ ℝ →
(0..^(#‘〈“𝐾”〉)) = {0}) |
6 | | simpr 476 |
. . . . . 6
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(#‘〈“𝐾”〉))) → 𝑛 ∈ (0..^(#‘〈“𝐾”〉))) |
7 | 6, 4 | syl6eleq 2698 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(#‘〈“𝐾”〉))) → 𝑛 ∈ {0}) |
8 | | velsn 4141 |
. . . . 5
⊢ (𝑛 ∈ {0} ↔ 𝑛 = 0) |
9 | 7, 8 | sylib 207 |
. . . 4
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(#‘〈“𝐾”〉))) → 𝑛 = 0) |
10 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑛 = 0 → (0...𝑛) = (0...0)) |
11 | | 0z 11265 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
12 | | fzsn 12254 |
. . . . . . . . . 10
⊢ (0 ∈
ℤ → (0...0) = {0}) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
⊢ (0...0) =
{0} |
14 | 10, 13 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑛 = 0 → (0...𝑛) = {0}) |
15 | 14 | mpteq1d 4666 |
. . . . . . 7
⊢ (𝑛 = 0 → (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖))) = (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) |
16 | 15 | oveq2d 6565 |
. . . . . 6
⊢ (𝑛 = 0 → (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))) = (𝑊 Σg (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖))))) |
17 | 16 | adantl 481 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) → (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))) = (𝑊 Σg (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖))))) |
18 | | signsv.p |
. . . . . . . . 9
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
19 | | signsv.w |
. . . . . . . . 9
⊢ 𝑊 = {〈(Base‘ndx), {-1,
0, 1}〉, 〈(+g‘ndx), ⨣
〉} |
20 | 18, 19 | signswmnd 29960 |
. . . . . . . 8
⊢ 𝑊 ∈ Mnd |
21 | 20 | a1i 11 |
. . . . . . 7
⊢ (𝐾 ∈ ℝ → 𝑊 ∈ Mnd) |
22 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
23 | 22 | a1i 11 |
. . . . . . 7
⊢ (𝐾 ∈ ℝ → 0 ∈
ℝ) |
24 | | s1fv 13243 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) = 𝐾) |
25 | | id 22 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℝ → 𝐾 ∈
ℝ) |
26 | 24, 25 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) ∈
ℝ) |
27 | 26 | rexrd 9968 |
. . . . . . . 8
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) ∈
ℝ*) |
28 | | sgncl 29927 |
. . . . . . . 8
⊢
((〈“𝐾”〉‘0) ∈
ℝ* → (sgn‘(〈“𝐾”〉‘0)) ∈ {-1, 0,
1}) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ ℝ →
(sgn‘(〈“𝐾”〉‘0)) ∈ {-1, 0,
1}) |
30 | 18, 19 | signswbase 29957 |
. . . . . . . 8
⊢ {-1, 0,
1} = (Base‘𝑊) |
31 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (〈“𝐾”〉‘𝑖) = (〈“𝐾”〉‘0)) |
32 | 31 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑖 = 0 →
(sgn‘(〈“𝐾”〉‘𝑖)) = (sgn‘(〈“𝐾”〉‘0))) |
33 | 30, 32 | gsumsn 18177 |
. . . . . . 7
⊢ ((𝑊 ∈ Mnd ∧ 0 ∈
ℝ ∧ (sgn‘(〈“𝐾”〉‘0)) ∈ {-1, 0, 1})
→ (𝑊
Σg (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘(〈“𝐾”〉‘0))) |
34 | 21, 23, 29, 33 | syl3anc 1318 |
. . . . . 6
⊢ (𝐾 ∈ ℝ → (𝑊 Σg
(𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘(〈“𝐾”〉‘0))) |
35 | 34 | adantr 480 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) → (𝑊 Σg (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘(〈“𝐾”〉‘0))) |
36 | 24 | fveq2d 6107 |
. . . . . 6
⊢ (𝐾 ∈ ℝ →
(sgn‘(〈“𝐾”〉‘0)) = (sgn‘𝐾)) |
37 | 36 | adantr 480 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) →
(sgn‘(〈“𝐾”〉‘0)) = (sgn‘𝐾)) |
38 | 17, 35, 37 | 3eqtrd 2648 |
. . . 4
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) → (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘𝐾)) |
39 | 9, 38 | syldan 486 |
. . 3
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(#‘〈“𝐾”〉))) → (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘𝐾)) |
40 | 5, 39 | mpteq12dva 4662 |
. 2
⊢ (𝐾 ∈ ℝ → (𝑛 ∈
(0..^(#‘〈“𝐾”〉)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖))))) = (𝑛 ∈ {0} ↦ (sgn‘𝐾))) |
41 | | s1cl 13235 |
. . 3
⊢ (𝐾 ∈ ℝ →
〈“𝐾”〉
∈ Word ℝ) |
42 | | signsv.t |
. . . 4
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
43 | | signsv.v |
. . . 4
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
44 | 18, 19, 42, 43 | signstfv 29966 |
. . 3
⊢
(〈“𝐾”〉 ∈ Word ℝ →
(𝑇‘〈“𝐾”〉) = (𝑛 ∈
(0..^(#‘〈“𝐾”〉)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))))) |
45 | 41, 44 | syl 17 |
. 2
⊢ (𝐾 ∈ ℝ → (𝑇‘〈“𝐾”〉) = (𝑛 ∈
(0..^(#‘〈“𝐾”〉)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))))) |
46 | | sgnclre 29928 |
. . . 4
⊢ (𝐾 ∈ ℝ →
(sgn‘𝐾) ∈
ℝ) |
47 | | s1val 13231 |
. . . 4
⊢
((sgn‘𝐾)
∈ ℝ → 〈“(sgn‘𝐾)”〉 = {〈0, (sgn‘𝐾)〉}) |
48 | 46, 47 | syl 17 |
. . 3
⊢ (𝐾 ∈ ℝ →
〈“(sgn‘𝐾)”〉 = {〈0, (sgn‘𝐾)〉}) |
49 | | fmptsn 6338 |
. . . 4
⊢ ((0
∈ ℝ ∧ (sgn‘𝐾) ∈ ℝ) → {〈0,
(sgn‘𝐾)〉} =
(𝑛 ∈ {0} ↦
(sgn‘𝐾))) |
50 | 22, 46, 49 | sylancr 694 |
. . 3
⊢ (𝐾 ∈ ℝ → {〈0,
(sgn‘𝐾)〉} =
(𝑛 ∈ {0} ↦
(sgn‘𝐾))) |
51 | 48, 50 | eqtrd 2644 |
. 2
⊢ (𝐾 ∈ ℝ →
〈“(sgn‘𝐾)”〉 = (𝑛 ∈ {0} ↦ (sgn‘𝐾))) |
52 | 40, 45, 51 | 3eqtr4d 2654 |
1
⊢ (𝐾 ∈ ℝ → (𝑇‘〈“𝐾”〉) =
〈“(sgn‘𝐾)”〉) |