Metamath Proof Explorer

Theorem signshf

Description: H , corresponding to the word F multiplied by ( x - C ) , as a function. (Contributed by Thierry Arnoux, 29-Sep-2018)

Ref Expression
Hypotheses signsv.p ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
signs.h ⊢ 𝐻 = ( ( ⟨“ 0 ”⟩ ++ 𝐹 ) ∘f − ( ( 𝐹 ++ ⟨“ 0 ”⟩ ) ∘f/c · 𝐶 ) )
Assertion signshf ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐻 : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ )

Proof

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 signs.h ⊢ 𝐻 = ( ( ⟨“ 0 ”⟩ ++ 𝐹 ) ∘f − ( ( 𝐹 ++ ⟨“ 0 ”⟩ ) ∘f/c · 𝐶 ) )
6 resubcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 − 𝑦 ) ∈ ℝ )
7 6 adantl ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 − 𝑦 ) ∈ ℝ )
8 0re ⊢ 0 ∈ ℝ
9 s1cl ⊢ ( 0 ∈ ℝ → ⟨“ 0 ”⟩ ∈ Word ℝ )
10 8 9 ax-mp ⊢ ⟨“ 0 ”⟩ ∈ Word ℝ
11 ccatcl ⊢ ( ( ⟨“ 0 ”⟩ ∈ Word ℝ ∧ 𝐹 ∈ Word ℝ ) → ( ⟨“ 0 ”⟩ ++ 𝐹 ) ∈ Word ℝ )
12 10 11 mpan ⊢ ( 𝐹 ∈ Word ℝ → ( ⟨“ 0 ”⟩ ++ 𝐹 ) ∈ Word ℝ )
13 wrdf ⊢ ( ( ⟨“ 0 ”⟩ ++ 𝐹 ) ∈ Word ℝ → ( ⟨“ 0 ”⟩ ++ 𝐹 ) : ( 0 ..^ ( ♯ ‘ ( ⟨“ 0 ”⟩ ++ 𝐹 ) ) ) ⟶ ℝ )
14 12 13 syl ⊢ ( 𝐹 ∈ Word ℝ → ( ⟨“ 0 ”⟩ ++ 𝐹 ) : ( 0 ..^ ( ♯ ‘ ( ⟨“ 0 ”⟩ ++ 𝐹 ) ) ) ⟶ ℝ )
15 1cnd ⊢ ( 𝐹 ∈ Word ℝ → 1 ∈ ℂ )
16 lencl ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
17 16 nn0cnd ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ 𝐹 ) ∈ ℂ )
18 ccatlen ⊢ ( ( ⟨“ 0 ”⟩ ∈ Word ℝ ∧ 𝐹 ∈ Word ℝ ) → ( ♯ ‘ ( ⟨“ 0 ”⟩ ++ 𝐹 ) ) = ( ( ♯ ‘ ⟨“ 0 ”⟩ ) + ( ♯ ‘ 𝐹 ) ) )
19 10 18 mpan ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ ( ⟨“ 0 ”⟩ ++ 𝐹 ) ) = ( ( ♯ ‘ ⟨“ 0 ”⟩ ) + ( ♯ ‘ 𝐹 ) ) )
20 s1len ⊢ ( ♯ ‘ ⟨“ 0 ”⟩ ) = 1
21 20 oveq1i ⊢ ( ( ♯ ‘ ⟨“ 0 ”⟩ ) + ( ♯ ‘ 𝐹 ) ) = ( 1 + ( ♯ ‘ 𝐹 ) )
22 19 21 eqtrdi ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ ( ⟨“ 0 ”⟩ ++ 𝐹 ) ) = ( 1 + ( ♯ ‘ 𝐹 ) ) )
23 15 17 22 comraddd ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ ( ⟨“ 0 ”⟩ ++ 𝐹 ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
24 23 oveq2d ⊢ ( 𝐹 ∈ Word ℝ → ( 0 ..^ ( ♯ ‘ ( ⟨“ 0 ”⟩ ++ 𝐹 ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
25 24 feq2d ⊢ ( 𝐹 ∈ Word ℝ → ( ( ⟨“ 0 ”⟩ ++ 𝐹 ) : ( 0 ..^ ( ♯ ‘ ( ⟨“ 0 ”⟩ ++ 𝐹 ) ) ) ⟶ ℝ ↔ ( ⟨“ 0 ”⟩ ++ 𝐹 ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ ) )
26 14 25 mpbid ⊢ ( 𝐹 ∈ Word ℝ → ( ⟨“ 0 ”⟩ ++ 𝐹 ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ )
27 26 adantr ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ⟨“ 0 ”⟩ ++ 𝐹 ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ )
28 remulcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
29 28 adantl ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
30 ccatcl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ ⟨“ 0 ”⟩ ∈ Word ℝ ) → ( 𝐹 ++ ⟨“ 0 ”⟩ ) ∈ Word ℝ )
31 10 30 mpan2 ⊢ ( 𝐹 ∈ Word ℝ → ( 𝐹 ++ ⟨“ 0 ”⟩ ) ∈ Word ℝ )
32 wrdf ⊢ ( ( 𝐹 ++ ⟨“ 0 ”⟩ ) ∈ Word ℝ → ( 𝐹 ++ ⟨“ 0 ”⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 0 ”⟩ ) ) ) ⟶ ℝ )
33 31 32 syl ⊢ ( 𝐹 ∈ Word ℝ → ( 𝐹 ++ ⟨“ 0 ”⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 0 ”⟩ ) ) ) ⟶ ℝ )
34 ccatws1len ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ ( 𝐹 ++ ⟨“ 0 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
35 34 oveq2d ⊢ ( 𝐹 ∈ Word ℝ → ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 0 ”⟩ ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
36 35 feq2d ⊢ ( 𝐹 ∈ Word ℝ → ( ( 𝐹 ++ ⟨“ 0 ”⟩ ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 0 ”⟩ ) ) ) ⟶ ℝ ↔ ( 𝐹 ++ ⟨“ 0 ”⟩ ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ ) )
37 33 36 mpbid ⊢ ( 𝐹 ∈ Word ℝ → ( 𝐹 ++ ⟨“ 0 ”⟩ ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ )
38 37 adantr ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐹 ++ ⟨“ 0 ”⟩ ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ )
39 ovexd ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∈ V )
40 rpre ⊢ ( 𝐶 ∈ ℝ+ → 𝐶 ∈ ℝ )
41 40 adantl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
42 29 38 39 41 ofcf ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐹 ++ ⟨“ 0 ”⟩ ) ∘f/c · 𝐶 ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ )
43 inidm ⊢ ( ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ∩ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) )
44 7 27 42 39 39 43 off ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ⟨“ 0 ”⟩ ++ 𝐹 ) ∘f − ( ( 𝐹 ++ ⟨“ 0 ”⟩ ) ∘f/c · 𝐶 ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ )
45 5 feq1i ⊢ ( 𝐻 : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ ↔ ( ( ⟨“ 0 ”⟩ ++ 𝐹 ) ∘f − ( ( 𝐹 ++ ⟨“ 0 ”⟩ ) ∘f/c · 𝐶 ) ) : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ )
46 44 45 sylibr ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐻 : ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) ⟶ ℝ )