Metamath Proof Explorer

Theorem signstf0

Description: Sign of a single letter word. (Contributed by Thierry Arnoux, 8-Oct-2018)

Ref Expression
Hypotheses signsv.p ⊢ ⨣ ˙ = a ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
signsv.w ⊢ W = Base ndx − 1 0 1 + ndx ⨣ ˙
signsv.t ⊢ T = f ∈ Word ℝ ⟼ n ∈ 0 ..^ f ⟼ ∑ W i = 0 n sgn ⁡ f ⁡ i
signsv.v ⊢ V = f ∈ Word ℝ ⟼ ∑ j ∈ 1 ..^ f if T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 1 0
Assertion signstf0 ⊢ K ∈ ℝ → T ⁡ ⟨“ K ”⟩ = ⟨“ sgn ⁡ K ”⟩

Proof

Step Hyp Ref Expression
1 signsv.p ⊢ ⨣ ˙ = a ∈ − 1 0 1 , b ∈ − 1 0 1 ⟼ if b = 0 a b
2 signsv.w ⊢ W = Base ndx − 1 0 1 + ndx ⨣ ˙
3 signsv.t ⊢ T = f ∈ Word ℝ ⟼ n ∈ 0 ..^ f ⟼ ∑ W i = 0 n sgn ⁡ f ⁡ i
4 signsv.v ⊢ V = f ∈ Word ℝ ⟼ ∑ j ∈ 1 ..^ f if T ⁡ f ⁡ j ≠ T ⁡ f ⁡ j − 1 1 0
5 s1len ⊢ ⟨“ K ”⟩ = 1
6 5 oveq2i ⊢ 0 ..^ ⟨“ K ”⟩ = 0 ..^ 1
7 fzo01 ⊢ 0 ..^ 1 = 0
8 6 7 eqtri ⊢ 0 ..^ ⟨“ K ”⟩ = 0
9 8 a1i ⊢ K ∈ ℝ → 0 ..^ ⟨“ K ”⟩ = 0
10 simpr ⊢ K ∈ ℝ ∧ n ∈ 0 ..^ ⟨“ K ”⟩ → n ∈ 0 ..^ ⟨“ K ”⟩
11 10 8 eleqtrdi ⊢ K ∈ ℝ ∧ n ∈ 0 ..^ ⟨“ K ”⟩ → n ∈ 0
12 velsn ⊢ n ∈ 0 ↔ n = 0
13 11 12 sylib ⊢ K ∈ ℝ ∧ n ∈ 0 ..^ ⟨“ K ”⟩ → n = 0
14 oveq2 ⊢ n = 0 → 0 … n = 0 … 0
15 0z ⊢ 0 ∈ ℤ
16 fzsn ⊢ 0 ∈ ℤ → 0 … 0 = 0
17 15 16 ax-mp ⊢ 0 … 0 = 0
18 14 17 eqtrdi ⊢ n = 0 → 0 … n = 0
19 18 mpteq1d ⊢ n = 0 → i ∈ 0 … n ⟼ sgn ⁡ ⟨“ K ”⟩ ⁡ i = i ∈ 0 ⟼ sgn ⁡ ⟨“ K ”⟩ ⁡ i
20 19 oveq2d ⊢ n = 0 → ∑ W i = 0 n sgn ⁡ ⟨“ K ”⟩ ⁡ i = ∑ W i ∈ 0 sgn ⁡ ⟨“ K ”⟩ ⁡ i
21 20 adantl ⊢ K ∈ ℝ ∧ n = 0 → ∑ W i = 0 n sgn ⁡ ⟨“ K ”⟩ ⁡ i = ∑ W i ∈ 0 sgn ⁡ ⟨“ K ”⟩ ⁡ i
22 1 2 signswmnd ⊢ W ∈ Mnd
23 22 a1i ⊢ K ∈ ℝ → W ∈ Mnd
24 0re ⊢ 0 ∈ ℝ
25 24 a1i ⊢ K ∈ ℝ → 0 ∈ ℝ
26 s1fv ⊢ K ∈ ℝ → ⟨“ K ”⟩ ⁡ 0 = K
27 id ⊢ K ∈ ℝ → K ∈ ℝ
28 26 27 eqeltrd ⊢ K ∈ ℝ → ⟨“ K ”⟩ ⁡ 0 ∈ ℝ
29 28 rexrd ⊢ K ∈ ℝ → ⟨“ K ”⟩ ⁡ 0 ∈ ℝ *
30 sgncl ⊢ ⟨“ K ”⟩ ⁡ 0 ∈ ℝ * → sgn ⁡ ⟨“ K ”⟩ ⁡ 0 ∈ − 1 0 1
31 29 30 syl ⊢ K ∈ ℝ → sgn ⁡ ⟨“ K ”⟩ ⁡ 0 ∈ − 1 0 1
32 1 2 signswbase ⊢ − 1 0 1 = Base W
33 2fveq3 ⊢ i = 0 → sgn ⁡ ⟨“ K ”⟩ ⁡ i = sgn ⁡ ⟨“ K ”⟩ ⁡ 0
34 32 33 gsumsn ⊢ W ∈ Mnd ∧ 0 ∈ ℝ ∧ sgn ⁡ ⟨“ K ”⟩ ⁡ 0 ∈ − 1 0 1 → ∑ W i ∈ 0 sgn ⁡ ⟨“ K ”⟩ ⁡ i = sgn ⁡ ⟨“ K ”⟩ ⁡ 0
35 23 25 31 34 syl3anc ⊢ K ∈ ℝ → ∑ W i ∈ 0 sgn ⁡ ⟨“ K ”⟩ ⁡ i = sgn ⁡ ⟨“ K ”⟩ ⁡ 0
36 35 adantr ⊢ K ∈ ℝ ∧ n = 0 → ∑ W i ∈ 0 sgn ⁡ ⟨“ K ”⟩ ⁡ i = sgn ⁡ ⟨“ K ”⟩ ⁡ 0
37 26 fveq2d ⊢ K ∈ ℝ → sgn ⁡ ⟨“ K ”⟩ ⁡ 0 = sgn ⁡ K
38 37 adantr ⊢ K ∈ ℝ ∧ n = 0 → sgn ⁡ ⟨“ K ”⟩ ⁡ 0 = sgn ⁡ K
39 21 36 38 3eqtrd ⊢ K ∈ ℝ ∧ n = 0 → ∑ W i = 0 n sgn ⁡ ⟨“ K ”⟩ ⁡ i = sgn ⁡ K
40 13 39 syldan ⊢ K ∈ ℝ ∧ n ∈ 0 ..^ ⟨“ K ”⟩ → ∑ W i = 0 n sgn ⁡ ⟨“ K ”⟩ ⁡ i = sgn ⁡ K
41 9 40 mpteq12dva ⊢ K ∈ ℝ → n ∈ 0 ..^ ⟨“ K ”⟩ ⟼ ∑ W i = 0 n sgn ⁡ ⟨“ K ”⟩ ⁡ i = n ∈ 0 ⟼ sgn ⁡ K
42 s1cl ⊢ K ∈ ℝ → ⟨“ K ”⟩ ∈ Word ℝ
43 1 2 3 4 signstfv ⊢ ⟨“ K ”⟩ ∈ Word ℝ → T ⁡ ⟨“ K ”⟩ = n ∈ 0 ..^ ⟨“ K ”⟩ ⟼ ∑ W i = 0 n sgn ⁡ ⟨“ K ”⟩ ⁡ i
44 42 43 syl ⊢ K ∈ ℝ → T ⁡ ⟨“ K ”⟩ = n ∈ 0 ..^ ⟨“ K ”⟩ ⟼ ∑ W i = 0 n sgn ⁡ ⟨“ K ”⟩ ⁡ i
45 sgnclre ⊢ K ∈ ℝ → sgn ⁡ K ∈ ℝ
46 s1val ⊢ sgn ⁡ K ∈ ℝ → ⟨“ sgn ⁡ K ”⟩ = 0 sgn ⁡ K
47 45 46 syl ⊢ K ∈ ℝ → ⟨“ sgn ⁡ K ”⟩ = 0 sgn ⁡ K
48 fmptsn ⊢ 0 ∈ ℝ ∧ sgn ⁡ K ∈ ℝ → 0 sgn ⁡ K = n ∈ 0 ⟼ sgn ⁡ K
49 24 45 48 sylancr ⊢ K ∈ ℝ → 0 sgn ⁡ K = n ∈ 0 ⟼ sgn ⁡ K
50 47 49 eqtrd ⊢ K ∈ ℝ → ⟨“ sgn ⁡ K ”⟩ = n ∈ 0 ⟼ sgn ⁡ K
51 41 44 50 3eqtr4d ⊢ K ∈ ℝ → T ⁡ ⟨“ K ”⟩ = ⟨“ sgn ⁡ K ”⟩