Metamath Proof Explorer


Theorem signstfvcl

Description: Closure of the zero skipping sign in case the first letter is not zero. (Contributed by Thierry Arnoux, 10-Oct-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 ) )
Assertion signstfvcl ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇𝐹 ) ‘ 𝑁 ) ∈ { - 1 , 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 simpll ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) )
6 5 eldifad ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ∈ Word ℝ )
7 1 2 3 4 signstcl ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇𝐹 ) ‘ 𝑁 ) ∈ { - 1 , 0 , 1 } )
8 6 7 sylancom ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇𝐹 ) ‘ 𝑁 ) ∈ { - 1 , 0 , 1 } )
9 1 2 3 4 signstfvneq0 ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇𝐹 ) ‘ 𝑁 ) ≠ 0 )
10 eldifsn ( ( ( 𝑇𝐹 ) ‘ 𝑁 ) ∈ ( { - 1 , 0 , 1 } ∖ { 0 } ) ↔ ( ( ( 𝑇𝐹 ) ‘ 𝑁 ) ∈ { - 1 , 0 , 1 } ∧ ( ( 𝑇𝐹 ) ‘ 𝑁 ) ≠ 0 ) )
11 8 9 10 sylanbrc ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇𝐹 ) ‘ 𝑁 ) ∈ ( { - 1 , 0 , 1 } ∖ { 0 } ) )
12 tpcomb { - 1 , 0 , 1 } = { - 1 , 1 , 0 }
13 12 difeq1i ( { - 1 , 0 , 1 } ∖ { 0 } ) = ( { - 1 , 1 , 0 } ∖ { 0 } )
14 neg1ne0 - 1 ≠ 0
15 ax-1ne0 1 ≠ 0
16 diftpsn3 ( ( - 1 ≠ 0 ∧ 1 ≠ 0 ) → ( { - 1 , 1 , 0 } ∖ { 0 } ) = { - 1 , 1 } )
17 14 15 16 mp2an ( { - 1 , 1 , 0 } ∖ { 0 } ) = { - 1 , 1 }
18 13 17 eqtri ( { - 1 , 0 , 1 } ∖ { 0 } ) = { - 1 , 1 }
19 11 18 eleqtrdi ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇𝐹 ) ‘ 𝑁 ) ∈ { - 1 , 1 } )