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 34570 | . . . 4
⊢ {-1, 0,
1} = (Base‘𝑊) | 
| 4 | 1, 2 | signswmnd 34573 | . . . . 5
⊢ 𝑊 ∈ Mnd | 
| 5 | 4 | a1i 11 | . . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → 𝑊 ∈
Mnd) | 
| 6 |  | eldifi 4130 | . . . . . . . . 9
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → 𝐹 ∈
Word ℝ) | 
| 7 |  | lencl 14572 | . . . . . . . . 9
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℕ0) | 
| 8 | 6, 7 | syl 17 | . . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ∈
ℕ0) | 
| 9 |  | eldifsn 4785 | . . . . . . . . 9
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) ↔ (𝐹 ∈
Word ℝ ∧ 𝐹 ≠
∅)) | 
| 10 |  | hasheq0 14403 | . . . . . . . . . . 11
⊢ (𝐹 ∈ Word ℝ →
((♯‘𝐹) = 0
↔ 𝐹 =
∅)) | 
| 11 | 10 | necon3bid 2984 | . . . . . . . . . 10
⊢ (𝐹 ∈ Word ℝ →
((♯‘𝐹) ≠ 0
↔ 𝐹 ≠
∅)) | 
| 12 | 11 | biimpar 477 | . . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅) →
(♯‘𝐹) ≠
0) | 
| 13 | 9, 12 | sylbi 217 | . . . . . . . 8
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ≠ 0) | 
| 14 |  | elnnne0 12542 | . . . . . . . 8
⊢
((♯‘𝐹)
∈ ℕ ↔ ((♯‘𝐹) ∈ ℕ0 ∧
(♯‘𝐹) ≠
0)) | 
| 15 | 8, 13, 14 | sylanbrc 583 | . . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (♯‘𝐹) ∈ ℕ) | 
| 16 | 15 | adantr 480 | . . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (♯‘𝐹) ∈ ℕ) | 
| 17 |  | nnm1nn0 12569 | . . . . . 6
⊢
((♯‘𝐹)
∈ ℕ → ((♯‘𝐹) − 1) ∈
ℕ0) | 
| 18 | 16, 17 | syl 17 | . . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((♯‘𝐹) − 1) ∈
ℕ0) | 
| 19 |  | nn0uz 12921 | . . . . 5
⊢
ℕ0 = (ℤ≥‘0) | 
| 20 | 18, 19 | eleqtrdi 2850 | . . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((♯‘𝐹) − 1) ∈
(ℤ≥‘0)) | 
| 21 |  | ccatws1cl 14655 | . . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ) | 
| 22 | 21 | adantr 480 | . . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (𝐹 ++
〈“𝐾”〉) ∈ Word
ℝ) | 
| 23 |  | wrdf 14558 | . . . . . . . . 9
⊢ ((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ → (𝐹 ++
〈“𝐾”〉):(0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))⟶ℝ) | 
| 24 | 22, 23 | syl 17 | . . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (𝐹 ++
〈“𝐾”〉):(0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))⟶ℝ) | 
| 25 | 7 | nn0zd 12641 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℤ) | 
| 26 |  | fzoval 13701 | . . . . . . . . . . . . 13
⊢
((♯‘𝐹)
∈ ℤ → (0..^(♯‘𝐹)) = (0...((♯‘𝐹) − 1))) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . . . 12
⊢ (𝐹 ∈ Word ℝ →
(0..^(♯‘𝐹)) =
(0...((♯‘𝐹)
− 1))) | 
| 28 | 27 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^(♯‘𝐹)) =
(0...((♯‘𝐹)
− 1))) | 
| 29 |  | fzossfz 13719 | . . . . . . . . . . 11
⊢
(0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹)) | 
| 30 | 28, 29 | eqsstrrdi 4028 | . . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0...((♯‘𝐹)
− 1)) ⊆ (0...(♯‘𝐹))) | 
| 31 |  | s1cl 14641 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℝ →
〈“𝐾”〉
∈ Word ℝ) | 
| 32 |  | ccatlen 14614 | . . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ) → (♯‘(𝐹 ++ 〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) | 
| 33 | 31, 32 | sylan2 593 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) +
(♯‘〈“𝐾”〉))) | 
| 34 |  | s1len 14645 | . . . . . . . . . . . . . 14
⊢
(♯‘〈“𝐾”〉) = 1 | 
| 35 | 34 | oveq2i 7443 | . . . . . . . . . . . . 13
⊢
((♯‘𝐹) +
(♯‘〈“𝐾”〉)) = ((♯‘𝐹) + 1) | 
| 36 | 33, 35 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘(𝐹 ++
〈“𝐾”〉)) = ((♯‘𝐹) + 1)) | 
| 37 | 36 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^(♯‘(𝐹 ++
〈“𝐾”〉))) =
(0..^((♯‘𝐹) +
1))) | 
| 38 | 25 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘𝐹) ∈
ℤ) | 
| 39 | 38 | peano2zd 12727 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
((♯‘𝐹) + 1)
∈ ℤ) | 
| 40 |  | fzoval 13701 | . . . . . . . . . . . 12
⊢
(((♯‘𝐹)
+ 1) ∈ ℤ → (0..^((♯‘𝐹) + 1)) = (0...(((♯‘𝐹) + 1) −
1))) | 
| 41 | 39, 40 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^((♯‘𝐹) +
1)) = (0...(((♯‘𝐹) + 1) − 1))) | 
| 42 | 7 | nn0cnd 12591 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℂ) | 
| 43 |  | 1cnd 11257 | . . . . . . . . . . . . . 14
⊢ (𝐹 ∈ Word ℝ → 1
∈ ℂ) | 
| 44 | 42, 43 | pncand 11622 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ Word ℝ →
(((♯‘𝐹) + 1)
− 1) = (♯‘𝐹)) | 
| 45 | 44 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(((♯‘𝐹) + 1)
− 1) = (♯‘𝐹)) | 
| 46 | 45 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0...(((♯‘𝐹) +
1) − 1)) = (0...(♯‘𝐹))) | 
| 47 | 37, 41, 46 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0..^(♯‘(𝐹 ++
〈“𝐾”〉))) = (0...(♯‘𝐹))) | 
| 48 | 30, 47 | sseqtrrd 4020 | . . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(0...((♯‘𝐹)
− 1)) ⊆ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))) | 
| 49 | 48 | sselda 3982 | . . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 𝑖
∈ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))) | 
| 50 | 24, 49 | ffvelcdmd 7104 | . . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈ ℝ) | 
| 51 | 6, 50 | sylanl1 680 | . . . . . 6
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈ ℝ) | 
| 52 | 51 | rexrd 11312 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) ∈
ℝ*) | 
| 53 |  | sgncl 34542 | . . . . 5
⊢ (((𝐹 ++ 〈“𝐾”〉)‘𝑖) ∈ ℝ*
→ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)) ∈ {-1, 0, 1}) | 
| 54 | 52, 53 | syl 17 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) ∈ {-1, 0, 1}) | 
| 55 | 1, 2 | signswplusg 34571 | . . . 4
⊢  ⨣ =
(+g‘𝑊) | 
| 56 |  | rexr 11308 | . . . . . 6
⊢ (𝐾 ∈ ℝ → 𝐾 ∈
ℝ*) | 
| 57 |  | sgncl 34542 | . . . . . 6
⊢ (𝐾 ∈ ℝ*
→ (sgn‘𝐾) ∈
{-1, 0, 1}) | 
| 58 | 56, 57 | syl 17 | . . . . 5
⊢ (𝐾 ∈ ℝ →
(sgn‘𝐾) ∈ {-1,
0, 1}) | 
| 59 | 58 | adantl 481 | . . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (sgn‘𝐾) ∈ {-1, 0, 1}) | 
| 60 |  | id 22 | . . . . . . . . 9
⊢ (𝑖 = (((♯‘𝐹) − 1) + 1) → 𝑖 = (((♯‘𝐹) − 1) +
1)) | 
| 61 | 42, 43 | npcand 11625 | . . . . . . . . . 10
⊢ (𝐹 ∈ Word ℝ →
(((♯‘𝐹) −
1) + 1) = (♯‘𝐹)) | 
| 62 | 61 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(((♯‘𝐹) −
1) + 1) = (♯‘𝐹)) | 
| 63 | 60, 62 | sylan9eqr 2798 | . . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) → 𝑖 = (♯‘𝐹)) | 
| 64 | 63 | fveq2d 6909 | . . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) →
((𝐹 ++ 〈“𝐾”〉)‘𝑖) = ((𝐹 ++ 〈“𝐾”〉)‘(♯‘𝐹))) | 
| 65 |  | ccatws1ls 14672 | . . . . . . . 8
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → ((𝐹 ++ 〈“𝐾”〉)‘(♯‘𝐹)) = 𝐾) | 
| 66 | 65 | adantr 480 | . . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) →
((𝐹 ++ 〈“𝐾”〉)‘(♯‘𝐹)) = 𝐾) | 
| 67 | 64, 66 | eqtrd 2776 | . . . . . 6
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 = (((♯‘𝐹) − 1) + 1)) →
((𝐹 ++ 〈“𝐾”〉)‘𝑖) = 𝐾) | 
| 68 | 6, 67 | sylanl1 680 | . . . . 5
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((♯‘𝐹) −
1) + 1)) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) = 𝐾) | 
| 69 | 68 | fveq2d 6909 | . . . 4
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) ∧ 𝑖 =
(((♯‘𝐹) −
1) + 1)) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) = (sgn‘𝐾)) | 
| 70 | 3, 5, 20, 54, 55, 59, 69 | gsumnunsn 34557 | . . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(((♯‘𝐹) − 1) + 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) ⨣ (sgn‘𝐾))) | 
| 71 | 6, 61 | syl 17 | . . . . . . 7
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) | 
| 72 | 71 | adantr 480 | . . . . . 6
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹)) | 
| 73 | 72 | oveq2d 7448 | . . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (0...(((♯‘𝐹) − 1) + 1)) =
(0...(♯‘𝐹))) | 
| 74 | 73 | mpteq1d 5236 | . . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑖 ∈
(0...(((♯‘𝐹)
− 1) + 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...(♯‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) | 
| 75 | 74 | oveq2d 7448 | . . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(((♯‘𝐹) − 1) + 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) | 
| 76 |  | simpll 766 | . . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 𝐹
∈ Word ℝ) | 
| 77 | 31 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 〈“𝐾”〉 ∈ Word
ℝ) | 
| 78 | 28 | eleq2d 2826 | . . . . . . . . . 10
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝑖 ∈
(0..^(♯‘𝐹))
↔ 𝑖 ∈
(0...((♯‘𝐹)
− 1)))) | 
| 79 | 78 | biimpar 477 | . . . . . . . . 9
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → 𝑖
∈ (0..^(♯‘𝐹))) | 
| 80 |  | ccatval1 14616 | . . . . . . . . 9
⊢ ((𝐹 ∈ Word ℝ ∧
〈“𝐾”〉
∈ Word ℝ ∧ 𝑖
∈ (0..^(♯‘𝐹))) → ((𝐹 ++ 〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) | 
| 81 | 76, 77, 79, 80 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → ((𝐹 ++
〈“𝐾”〉)‘𝑖) = (𝐹‘𝑖)) | 
| 82 | 81 | fveq2d 6909 | . . . . . . 7
⊢ (((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) ∧ 𝑖 ∈
(0...((♯‘𝐹)
− 1))) → (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)) = (sgn‘(𝐹‘𝑖))) | 
| 83 | 82 | mpteq2dva 5241 | . . . . . 6
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖)))) | 
| 84 | 6, 83 | sylan 580 | . . . . 5
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖))) = (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘(𝐹‘𝑖)))) | 
| 85 | 84 | oveq2d 7448 | . . . 4
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) | 
| 86 | 85 | oveq1d 7447 | . . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑊
Σg (𝑖 ∈ (0...((♯‘𝐹) − 1)) ↦
(sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖)))) ⨣ (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) | 
| 87 | 70, 75, 86 | 3eqtr3d 2784 | . 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (𝑊
Σg (𝑖 ∈ (0...(♯‘𝐹)) ↦ (sgn‘((𝐹 ++ 〈“𝐾”〉)‘𝑖)))) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) | 
| 88 |  | eqid 2736 | . . . . . . . 8
⊢
(♯‘𝐹) =
(♯‘𝐹) | 
| 89 | 88 | olci 866 | . . . . . . 7
⊢
((♯‘𝐹)
∈ (0..^(♯‘𝐹)) ∨ (♯‘𝐹) = (♯‘𝐹)) | 
| 90 | 7, 19 | eleqtrdi 2850 | . . . . . . . 8
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
(ℤ≥‘0)) | 
| 91 |  | fzosplitsni 13818 | . . . . . . . 8
⊢
((♯‘𝐹)
∈ (ℤ≥‘0) → ((♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1)) ↔ ((♯‘𝐹) ∈ (0..^(♯‘𝐹)) ∨ (♯‘𝐹) = (♯‘𝐹)))) | 
| 92 | 90, 91 | syl 17 | . . . . . . 7
⊢ (𝐹 ∈ Word ℝ →
((♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1)) ↔ ((♯‘𝐹) ∈ (0..^(♯‘𝐹)) ∨ (♯‘𝐹) = (♯‘𝐹)))) | 
| 93 | 89, 92 | mpbiri 258 | . . . . . 6
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1))) | 
| 94 | 93 | adantr 480 | . . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) →
(♯‘𝐹) ∈
(0..^((♯‘𝐹) +
1))) | 
| 95 | 94, 37 | eleqtrrd 2843 | . . . 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 34580 | . . . 4
⊢ (((𝐹 ++ 〈“𝐾”〉) ∈ Word
ℝ ∧ (♯‘𝐹) ∈ (0..^(♯‘(𝐹 ++ 〈“𝐾”〉)))) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) | 
| 99 | 21, 95, 98 | syl2anc 584 | . . 3
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) | 
| 100 | 6, 99 | sylan 580 | . 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (𝑊 Σg (𝑖 ∈
(0...(♯‘𝐹))
↦ (sgn‘((𝐹 ++
〈“𝐾”〉)‘𝑖))))) | 
| 101 |  | fzo0end 13798 | . . . . . 6
⊢
((♯‘𝐹)
∈ ℕ → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) | 
| 102 | 15, 101 | syl 17 | . . . . 5
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ((♯‘𝐹) − 1) ∈
(0..^(♯‘𝐹))) | 
| 103 | 1, 2, 96, 97 | signstfval 34580 | . . . . 5
⊢ ((𝐹 ∈ Word ℝ ∧
((♯‘𝐹) −
1) ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) | 
| 104 | 6, 102, 103 | syl2anc 584 | . . . 4
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) | 
| 105 | 104 | adantr 480 | . . 3
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘𝐹)‘((♯‘𝐹) − 1)) = (𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖))))) | 
| 106 | 105 | oveq1d 7447 | . 2
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾)) = ((𝑊 Σg (𝑖 ∈
(0...((♯‘𝐹)
− 1)) ↦ (sgn‘(𝐹‘𝑖)))) ⨣ (sgn‘𝐾))) | 
| 107 | 87, 100, 106 | 3eqtr4d 2786 | 1
⊢ ((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ 𝐾 ∈
ℝ) → ((𝑇‘(𝐹 ++ 〈“𝐾”〉))‘(♯‘𝐹)) = (((𝑇‘𝐹)‘((♯‘𝐹) − 1)) ⨣ (sgn‘𝐾))) |