Proof of Theorem signstf0
Step | Hyp | Ref
| Expression |
1 | | s1len 14196 |
. . . . . 6
⊢
(♯‘〈“𝐾”〉) = 1 |
2 | 1 | oveq2i 7246 |
. . . . 5
⊢
(0..^(♯‘〈“𝐾”〉)) = (0..^1) |
3 | | fzo01 13354 |
. . . . 5
⊢ (0..^1) =
{0} |
4 | 2, 3 | eqtri 2767 |
. . . 4
⊢
(0..^(♯‘〈“𝐾”〉)) = {0} |
5 | 4 | a1i 11 |
. . 3
⊢ (𝐾 ∈ ℝ →
(0..^(♯‘〈“𝐾”〉)) = {0}) |
6 | | simpr 488 |
. . . . . 6
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) → 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) |
7 | 6, 4 | eleqtrdi 2850 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) → 𝑛 ∈ {0}) |
8 | | velsn 4574 |
. . . . 5
⊢ (𝑛 ∈ {0} ↔ 𝑛 = 0) |
9 | 7, 8 | sylib 221 |
. . . 4
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) → 𝑛 = 0) |
10 | | oveq2 7243 |
. . . . . . . . 9
⊢ (𝑛 = 0 → (0...𝑛) = (0...0)) |
11 | | 0z 12217 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
12 | | fzsn 13184 |
. . . . . . . . . 10
⊢ (0 ∈
ℤ → (0...0) = {0}) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
⊢ (0...0) =
{0} |
14 | 10, 13 | eqtrdi 2796 |
. . . . . . . 8
⊢ (𝑛 = 0 → (0...𝑛) = {0}) |
15 | 14 | mpteq1d 5161 |
. . . . . . 7
⊢ (𝑛 = 0 → (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖))) = (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) |
16 | 15 | oveq2d 7251 |
. . . . . 6
⊢ (𝑛 = 0 → (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))) = (𝑊 Σg (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖))))) |
17 | 16 | adantl 485 |
. . . . 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 32280 |
. . . . . . . 8
⊢ 𝑊 ∈ Mnd |
21 | 20 | a1i 11 |
. . . . . . 7
⊢ (𝐾 ∈ ℝ → 𝑊 ∈ Mnd) |
22 | | 0re 10865 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
23 | 22 | a1i 11 |
. . . . . . 7
⊢ (𝐾 ∈ ℝ → 0 ∈
ℝ) |
24 | | s1fv 14200 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) = 𝐾) |
25 | | id 22 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℝ → 𝐾 ∈
ℝ) |
26 | 24, 25 | eqeltrd 2840 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) ∈
ℝ) |
27 | 26 | rexrd 10913 |
. . . . . . . 8
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) ∈
ℝ*) |
28 | | sgncl 32249 |
. . . . . . . 8
⊢
((〈“𝐾”〉‘0) ∈
ℝ* → (sgn‘(〈“𝐾”〉‘0)) ∈ {-1, 0,
1}) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ (𝐾 ∈ ℝ →
(sgn‘(〈“𝐾”〉‘0)) ∈ {-1, 0,
1}) |
30 | 18, 19 | signswbase 32277 |
. . . . . . . 8
⊢ {-1, 0,
1} = (Base‘𝑊) |
31 | | 2fveq3 6744 |
. . . . . . . 8
⊢ (𝑖 = 0 →
(sgn‘(〈“𝐾”〉‘𝑖)) = (sgn‘(〈“𝐾”〉‘0))) |
32 | 30, 31 | gsumsn 19372 |
. . . . . . 7
⊢ ((𝑊 ∈ Mnd ∧ 0 ∈
ℝ ∧ (sgn‘(〈“𝐾”〉‘0)) ∈ {-1, 0, 1})
→ (𝑊
Σg (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘(〈“𝐾”〉‘0))) |
33 | 21, 23, 29, 32 | syl3anc 1373 |
. . . . . 6
⊢ (𝐾 ∈ ℝ → (𝑊 Σg
(𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘(〈“𝐾”〉‘0))) |
34 | 33 | adantr 484 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) → (𝑊 Σg (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘(〈“𝐾”〉‘0))) |
35 | 24 | fveq2d 6743 |
. . . . . 6
⊢ (𝐾 ∈ ℝ →
(sgn‘(〈“𝐾”〉‘0)) = (sgn‘𝐾)) |
36 | 35 | adantr 484 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) →
(sgn‘(〈“𝐾”〉‘0)) = (sgn‘𝐾)) |
37 | 17, 34, 36 | 3eqtrd 2783 |
. . . 4
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) → (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘𝐾)) |
38 | 9, 37 | syldan 594 |
. . 3
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) → (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘𝐾)) |
39 | 5, 38 | mpteq12dva 5156 |
. 2
⊢ (𝐾 ∈ ℝ → (𝑛 ∈
(0..^(♯‘〈“𝐾”〉)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖))))) = (𝑛 ∈ {0} ↦ (sgn‘𝐾))) |
40 | | s1cl 14192 |
. . 3
⊢ (𝐾 ∈ ℝ →
〈“𝐾”〉
∈ Word ℝ) |
41 | | signsv.t |
. . . 4
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈
(0..^(♯‘𝑓))
↦ (𝑊
Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
42 | | signsv.v |
. . . 4
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈
(1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
43 | 18, 19, 41, 42 | signstfv 32286 |
. . 3
⊢
(〈“𝐾”〉 ∈ Word ℝ →
(𝑇‘〈“𝐾”〉) = (𝑛 ∈
(0..^(♯‘〈“𝐾”〉)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))))) |
44 | 40, 43 | syl 17 |
. 2
⊢ (𝐾 ∈ ℝ → (𝑇‘〈“𝐾”〉) = (𝑛 ∈
(0..^(♯‘〈“𝐾”〉)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))))) |
45 | | sgnclre 32250 |
. . . 4
⊢ (𝐾 ∈ ℝ →
(sgn‘𝐾) ∈
ℝ) |
46 | | s1val 14188 |
. . . 4
⊢
((sgn‘𝐾)
∈ ℝ → 〈“(sgn‘𝐾)”〉 = {〈0, (sgn‘𝐾)〉}) |
47 | 45, 46 | syl 17 |
. . 3
⊢ (𝐾 ∈ ℝ →
〈“(sgn‘𝐾)”〉 = {〈0, (sgn‘𝐾)〉}) |
48 | | fmptsn 7004 |
. . . 4
⊢ ((0
∈ ℝ ∧ (sgn‘𝐾) ∈ ℝ) → {〈0,
(sgn‘𝐾)〉} =
(𝑛 ∈ {0} ↦
(sgn‘𝐾))) |
49 | 22, 45, 48 | sylancr 590 |
. . 3
⊢ (𝐾 ∈ ℝ → {〈0,
(sgn‘𝐾)〉} =
(𝑛 ∈ {0} ↦
(sgn‘𝐾))) |
50 | 47, 49 | eqtrd 2779 |
. 2
⊢ (𝐾 ∈ ℝ →
〈“(sgn‘𝐾)”〉 = (𝑛 ∈ {0} ↦ (sgn‘𝐾))) |
51 | 39, 44, 50 | 3eqtr4d 2789 |
1
⊢ (𝐾 ∈ ℝ → (𝑇‘〈“𝐾”〉) =
〈“(sgn‘𝐾)”〉) |