Proof of Theorem signstf0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | s1len 14645 | . . . . . 6
⊢
(♯‘〈“𝐾”〉) = 1 | 
| 2 | 1 | oveq2i 7443 | . . . . 5
⊢
(0..^(♯‘〈“𝐾”〉)) = (0..^1) | 
| 3 |  | fzo01 13787 | . . . . 5
⊢ (0..^1) =
{0} | 
| 4 | 2, 3 | eqtri 2764 | . . . 4
⊢
(0..^(♯‘〈“𝐾”〉)) = {0} | 
| 5 | 4 | a1i 11 | . . 3
⊢ (𝐾 ∈ ℝ →
(0..^(♯‘〈“𝐾”〉)) = {0}) | 
| 6 |  | simpr 484 | . . . . . 6
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) → 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) | 
| 7 | 6, 4 | eleqtrdi 2850 | . . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) → 𝑛 ∈ {0}) | 
| 8 |  | velsn 4641 | . . . . 5
⊢ (𝑛 ∈ {0} ↔ 𝑛 = 0) | 
| 9 | 7, 8 | sylib 218 | . . . 4
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) → 𝑛 = 0) | 
| 10 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑛 = 0 → (0...𝑛) = (0...0)) | 
| 11 |  | 0z 12626 | . . . . . . . . . 10
⊢ 0 ∈
ℤ | 
| 12 |  | fzsn 13607 | . . . . . . . . . 10
⊢ (0 ∈
ℤ → (0...0) = {0}) | 
| 13 | 11, 12 | ax-mp 5 | . . . . . . . . 9
⊢ (0...0) =
{0} | 
| 14 | 10, 13 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑛 = 0 → (0...𝑛) = {0}) | 
| 15 | 14 | mpteq1d 5236 | . . . . . . 7
⊢ (𝑛 = 0 → (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖))) = (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) | 
| 16 | 15 | oveq2d 7448 | . . . . . 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 34573 | . . . . . . . 8
⊢ 𝑊 ∈ Mnd | 
| 21 | 20 | a1i 11 | . . . . . . 7
⊢ (𝐾 ∈ ℝ → 𝑊 ∈ Mnd) | 
| 22 |  | 0re 11264 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 23 | 22 | a1i 11 | . . . . . . 7
⊢ (𝐾 ∈ ℝ → 0 ∈
ℝ) | 
| 24 |  | s1fv 14649 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) = 𝐾) | 
| 25 |  | id 22 | . . . . . . . . . 10
⊢ (𝐾 ∈ ℝ → 𝐾 ∈
ℝ) | 
| 26 | 24, 25 | eqeltrd 2840 | . . . . . . . . 9
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) ∈
ℝ) | 
| 27 | 26 | rexrd 11312 | . . . . . . . 8
⊢ (𝐾 ∈ ℝ →
(〈“𝐾”〉‘0) ∈
ℝ*) | 
| 28 |  | sgncl 34542 | . . . . . . . 8
⊢
((〈“𝐾”〉‘0) ∈
ℝ* → (sgn‘(〈“𝐾”〉‘0)) ∈ {-1, 0,
1}) | 
| 29 | 27, 28 | syl 17 | . . . . . . 7
⊢ (𝐾 ∈ ℝ →
(sgn‘(〈“𝐾”〉‘0)) ∈ {-1, 0,
1}) | 
| 30 | 18, 19 | signswbase 34570 | . . . . . . . 8
⊢ {-1, 0,
1} = (Base‘𝑊) | 
| 31 |  | 2fveq3 6910 | . . . . . . . 8
⊢ (𝑖 = 0 →
(sgn‘(〈“𝐾”〉‘𝑖)) = (sgn‘(〈“𝐾”〉‘0))) | 
| 32 | 30, 31 | gsumsn 19973 | . . . . . . 7
⊢ ((𝑊 ∈ Mnd ∧ 0 ∈
ℝ ∧ (sgn‘(〈“𝐾”〉‘0)) ∈ {-1, 0, 1})
→ (𝑊
Σg (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘(〈“𝐾”〉‘0))) | 
| 33 | 21, 23, 29, 32 | syl3anc 1372 | . . . . . 6
⊢ (𝐾 ∈ ℝ → (𝑊 Σg
(𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘(〈“𝐾”〉‘0))) | 
| 34 | 33 | adantr 480 | . . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) → (𝑊 Σg (𝑖 ∈ {0} ↦
(sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘(〈“𝐾”〉‘0))) | 
| 35 | 24 | fveq2d 6909 | . . . . . 6
⊢ (𝐾 ∈ ℝ →
(sgn‘(〈“𝐾”〉‘0)) = (sgn‘𝐾)) | 
| 36 | 35 | adantr 480 | . . . . 5
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) →
(sgn‘(〈“𝐾”〉‘0)) = (sgn‘𝐾)) | 
| 37 | 17, 34, 36 | 3eqtrd 2780 | . . . 4
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 = 0) → (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘𝐾)) | 
| 38 | 9, 37 | syldan 591 | . . 3
⊢ ((𝐾 ∈ ℝ ∧ 𝑛 ∈
(0..^(♯‘〈“𝐾”〉))) → (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))) = (sgn‘𝐾)) | 
| 39 | 5, 38 | mpteq12dva 5230 | . 2
⊢ (𝐾 ∈ ℝ → (𝑛 ∈
(0..^(♯‘〈“𝐾”〉)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖))))) = (𝑛 ∈ {0} ↦ (sgn‘𝐾))) | 
| 40 |  | s1cl 14641 | . . 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 34579 | . . 3
⊢
(〈“𝐾”〉 ∈ Word ℝ →
(𝑇‘〈“𝐾”〉) = (𝑛 ∈
(0..^(♯‘〈“𝐾”〉)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))))) | 
| 44 | 40, 43 | syl 17 | . 2
⊢ (𝐾 ∈ ℝ → (𝑇‘〈“𝐾”〉) = (𝑛 ∈
(0..^(♯‘〈“𝐾”〉)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(〈“𝐾”〉‘𝑖)))))) | 
| 45 |  | sgnclre 34543 | . . . 4
⊢ (𝐾 ∈ ℝ →
(sgn‘𝐾) ∈
ℝ) | 
| 46 |  | s1val 14637 | . . . 4
⊢
((sgn‘𝐾)
∈ ℝ → 〈“(sgn‘𝐾)”〉 = {〈0, (sgn‘𝐾)〉}) | 
| 47 | 45, 46 | syl 17 | . . 3
⊢ (𝐾 ∈ ℝ →
〈“(sgn‘𝐾)”〉 = {〈0, (sgn‘𝐾)〉}) | 
| 48 |  | fmptsn 7188 | . . . 4
⊢ ((0
∈ ℝ ∧ (sgn‘𝐾) ∈ ℝ) → {〈0,
(sgn‘𝐾)〉} =
(𝑛 ∈ {0} ↦
(sgn‘𝐾))) | 
| 49 | 22, 45, 48 | sylancr 587 | . . 3
⊢ (𝐾 ∈ ℝ → {〈0,
(sgn‘𝐾)〉} =
(𝑛 ∈ {0} ↦
(sgn‘𝐾))) | 
| 50 | 47, 49 | eqtrd 2776 | . 2
⊢ (𝐾 ∈ ℝ →
〈“(sgn‘𝐾)”〉 = (𝑛 ∈ {0} ↦ (sgn‘𝐾))) | 
| 51 | 39, 44, 50 | 3eqtr4d 2786 | 1
⊢ (𝐾 ∈ ℝ → (𝑇‘〈“𝐾”〉) =
〈“(sgn‘𝐾)”〉) |