Metamath Proof Explorer

Theorem stoweidlem38

Description: This lemma is used to prove the existence of a function p as in Lemma 1 of BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Z is used for t_0, P is used for p, ( Gi ) is used for p__(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem38.1 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
stoweidlem38.2 ⊢ 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
stoweidlem38.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
stoweidlem38.4 ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 )
stoweidlem38.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
Assertion stoweidlem38 ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 0 ≤ ( 𝑃 ‘ 𝑆 ) ∧ ( 𝑃 ‘ 𝑆 ) ≤ 1 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem38.1 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
2 stoweidlem38.2 ⊢ 𝑃 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑡 ) ) )
3 stoweidlem38.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 stoweidlem38.4 ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 )
5 stoweidlem38.5 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
6 3 nnrecred ⊢ ( 𝜑 → ( 1 / 𝑀 ) ∈ ℝ )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 1 / 𝑀 ) ∈ ℝ )
8 fzfid ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 1 ... 𝑀 ) ∈ Fin )
9 1 4 5 stoweidlem15 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → ( ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ∧ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ≤ 1 ) )
10 9 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ )
11 10 an32s ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ )
12 8 11 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ )
13 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
14 0le1 ⊢ 0 ≤ 1
15 14 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
16 3 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
17 3 nngt0d ⊢ ( 𝜑 → 0 < 𝑀 )
18 divge0 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → 0 ≤ ( 1 / 𝑀 ) )
19 13 15 16 17 18 syl22anc ⊢ ( 𝜑 → 0 ≤ ( 1 / 𝑀 ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → 0 ≤ ( 1 / 𝑀 ) )
21 9 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) )
22 21 an32s ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 0 ≤ ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) )
23 8 11 22 fsumge0 ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → 0 ≤ Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) )
24 7 12 20 23 mulge0d ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → 0 ≤ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) )
25 1 2 3 4 5 stoweidlem30 ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑆 ) = ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) )
26 24 25 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → 0 ≤ ( 𝑃 ‘ 𝑆 ) )
27 1red ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 1 ∈ ℝ )
28 9 simp3d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ≤ 1 )
29 28 an32s ⊢ ( ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ≤ 1 )
30 8 11 27 29 fsumle ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ≤ Σ 𝑖 ∈ ( 1 ... 𝑀 ) 1 )
31 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
32 ax-1cn ⊢ 1 ∈ ℂ
33 fsumconst ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · 1 ) )
34 31 32 33 sylancl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) 1 = ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · 1 ) )
35 3 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
36 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
37 35 36 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
38 37 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · 1 ) = ( 𝑀 · 1 ) )
39 3 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
40 39 mulid1d ⊢ ( 𝜑 → ( 𝑀 · 1 ) = 𝑀 )
41 34 38 40 3eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑀 ) 1 = 𝑀 )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) 1 = 𝑀 )
43 30 42 breqtrd ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ≤ 𝑀 )
44 16 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → 𝑀 ∈ ℝ )
45 1red ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → 1 ∈ ℝ )
46 0lt1 ⊢ 0 < 1
47 46 a1i ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → 0 < 1 )
48 16 17 jca ⊢ ( 𝜑 → ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) )
50 divgt0 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → 0 < ( 1 / 𝑀 ) )
51 45 47 49 50 syl21anc ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → 0 < ( 1 / 𝑀 ) )
52 lemul2 ⊢ ( ( Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( ( 1 / 𝑀 ) ∈ ℝ ∧ 0 < ( 1 / 𝑀 ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ≤ 𝑀 ↔ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) ≤ ( ( 1 / 𝑀 ) · 𝑀 ) ) )
53 12 44 7 51 52 syl112anc ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ≤ 𝑀 ↔ ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) ≤ ( ( 1 / 𝑀 ) · 𝑀 ) ) )
54 43 53 mpbid ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( ( 1 / 𝑀 ) · Σ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐺 ‘ 𝑖 ) ‘ 𝑆 ) ) ≤ ( ( 1 / 𝑀 ) · 𝑀 ) )
55 25 54 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑆 ) ≤ ( ( 1 / 𝑀 ) · 𝑀 ) )
56 32 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
57 3 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
58 56 39 57 3jca ⊢ ( 𝜑 → ( 1 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 1 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) )
60 divcan1 ⊢ ( ( 1 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑀 ≠ 0 ) → ( ( 1 / 𝑀 ) · 𝑀 ) = 1 )
61 59 60 syl ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( ( 1 / 𝑀 ) · 𝑀 ) = 1 )
62 55 61 breqtrd ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑆 ) ≤ 1 )
63 26 62 jca ⊢ ( ( 𝜑 ∧ 𝑆 ∈ 𝑇 ) → ( 0 ≤ ( 𝑃 ‘ 𝑆 ) ∧ ( 𝑃 ‘ 𝑆 ) ≤ 1 ) )