Metamath Proof Explorer

Theorem signstf0

Description: Sign of a single letter word. (Contributed by Thierry Arnoux, 8-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 signstf0 ( 𝐾 ∈ ℝ → ( 𝑇 ‘ ⟨“ 𝐾 ”⟩ ) = ⟨“ ( sgn ‘ 𝐾 ) ”⟩ )

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 s1len ⊢ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) = 1
6 5 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) = ( 0 ..^ 1 )
7 fzo01 ⊢ ( 0 ..^ 1 ) = { 0 }
8 6 7 eqtri ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) = { 0 }
9 8 a1i ⊢ ( 𝐾 ∈ ℝ → ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) = { 0 } )
10 simpr ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) ) → 𝑛 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) )
11 10 8 eleqtrdi ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) ) → 𝑛 ∈ { 0 } )
12 velsn ⊢ ( 𝑛 ∈ { 0 } ↔ 𝑛 = 0 )
13 11 12 sylib ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) ) → 𝑛 = 0 )
14 oveq2 ⊢ ( 𝑛 = 0 → ( 0 ... 𝑛 ) = ( 0 ... 0 ) )
15 0z ⊢ 0 ∈ ℤ
16 fzsn ⊢ ( 0 ∈ ℤ → ( 0 ... 0 ) = { 0 } )
17 15 16 ax-mp ⊢ ( 0 ... 0 ) = { 0 }
18 14 17 eqtrdi ⊢ ( 𝑛 = 0 → ( 0 ... 𝑛 ) = { 0 } )
19 18 mpteq1d ⊢ ( 𝑛 = 0 → ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) = ( 𝑖 ∈ { 0 } ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) )
20 19 oveq2d ⊢ ( 𝑛 = 0 → ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) = ( 𝑊 Σg ( 𝑖 ∈ { 0 } ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) )
21 20 adantl ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑛 = 0 ) → ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) = ( 𝑊 Σg ( 𝑖 ∈ { 0 } ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) )
22 1 2 signswmnd ⊢ 𝑊 ∈ Mnd
23 22 a1i ⊢ ( 𝐾 ∈ ℝ → 𝑊 ∈ Mnd )
24 0re ⊢ 0 ∈ ℝ
25 24 a1i ⊢ ( 𝐾 ∈ ℝ → 0 ∈ ℝ )
26 s1fv ⊢ ( 𝐾 ∈ ℝ → ( ⟨“ 𝐾 ”⟩ ‘ 0 ) = 𝐾 )
27 id ⊢ ( 𝐾 ∈ ℝ → 𝐾 ∈ ℝ )
28 26 27 eqeltrd ⊢ ( 𝐾 ∈ ℝ → ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ∈ ℝ )
29 28 rexrd ⊢ ( 𝐾 ∈ ℝ → ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ∈ ℝ* )
30 sgncl ⊢ ( ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ∈ ℝ* → ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ) ∈ { - 1 , 0 , 1 } )
31 29 30 syl ⊢ ( 𝐾 ∈ ℝ → ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ) ∈ { - 1 , 0 , 1 } )
32 1 2 signswbase ⊢ { - 1 , 0 , 1 } = ( Base ‘ 𝑊 )
33 2fveq3 ⊢ ( 𝑖 = 0 → ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) = ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ) )
34 32 33 gsumsn ⊢ ( ( 𝑊 ∈ Mnd ∧ 0 ∈ ℝ ∧ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ) ∈ { - 1 , 0 , 1 } ) → ( 𝑊 Σg ( 𝑖 ∈ { 0 } ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) = ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ) )
35 23 25 31 34 syl3anc ⊢ ( 𝐾 ∈ ℝ → ( 𝑊 Σg ( 𝑖 ∈ { 0 } ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) = ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ) )
36 35 adantr ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑛 = 0 ) → ( 𝑊 Σg ( 𝑖 ∈ { 0 } ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) = ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ) )
37 26 fveq2d ⊢ ( 𝐾 ∈ ℝ → ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ) = ( sgn ‘ 𝐾 ) )
38 37 adantr ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑛 = 0 ) → ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 0 ) ) = ( sgn ‘ 𝐾 ) )
39 21 36 38 3eqtrd ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑛 = 0 ) → ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) = ( sgn ‘ 𝐾 ) )
40 13 39 syldan ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) ) → ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) = ( sgn ‘ 𝐾 ) )
41 9 40 mpteq12dva ⊢ ( 𝐾 ∈ ℝ → ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) ) = ( 𝑛 ∈ { 0 } ↦ ( sgn ‘ 𝐾 ) ) )
42 s1cl ⊢ ( 𝐾 ∈ ℝ → ⟨“ 𝐾 ”⟩ ∈ Word ℝ )
43 1 2 3 4 signstfv ⊢ ( ⟨“ 𝐾 ”⟩ ∈ Word ℝ → ( 𝑇 ‘ ⟨“ 𝐾 ”⟩ ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) ) )
44 42 43 syl ⊢ ( 𝐾 ∈ ℝ → ( 𝑇 ‘ ⟨“ 𝐾 ”⟩ ) = ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( ⟨“ 𝐾 ”⟩ ‘ 𝑖 ) ) ) ) ) )
45 sgnclre ⊢ ( 𝐾 ∈ ℝ → ( sgn ‘ 𝐾 ) ∈ ℝ )
46 s1val ⊢ ( ( sgn ‘ 𝐾 ) ∈ ℝ → ⟨“ ( sgn ‘ 𝐾 ) ”⟩ = { ⟨ 0 , ( sgn ‘ 𝐾 ) ⟩ } )
47 45 46 syl ⊢ ( 𝐾 ∈ ℝ → ⟨“ ( sgn ‘ 𝐾 ) ”⟩ = { ⟨ 0 , ( sgn ‘ 𝐾 ) ⟩ } )
48 fmptsn ⊢ ( ( 0 ∈ ℝ ∧ ( sgn ‘ 𝐾 ) ∈ ℝ ) → { ⟨ 0 , ( sgn ‘ 𝐾 ) ⟩ } = ( 𝑛 ∈ { 0 } ↦ ( sgn ‘ 𝐾 ) ) )
49 24 45 48 sylancr ⊢ ( 𝐾 ∈ ℝ → { ⟨ 0 , ( sgn ‘ 𝐾 ) ⟩ } = ( 𝑛 ∈ { 0 } ↦ ( sgn ‘ 𝐾 ) ) )
50 47 49 eqtrd ⊢ ( 𝐾 ∈ ℝ → ⟨“ ( sgn ‘ 𝐾 ) ”⟩ = ( 𝑛 ∈ { 0 } ↦ ( sgn ‘ 𝐾 ) ) )
51 41 44 50 3eqtr4d ⊢ ( 𝐾 ∈ ℝ → ( 𝑇 ‘ ⟨“ 𝐾 ”⟩ ) = ⟨“ ( sgn ‘ 𝐾 ) ”⟩ )