Metamath Proof Explorer

Theorem stoweidlem37

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 stoweidlem37.1 ⊢ Q = h ∈ A | h ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
stoweidlem37.2 ⊢ P = t ∈ T ⟼ 1 M ⁢ ∑ i = 1 M G ⁡ i ⁡ t
stoweidlem37.3 ⊢ φ → M ∈ ℕ
stoweidlem37.4 ⊢ φ → G : 1 … M ⟶ Q
stoweidlem37.5 ⊢ φ ∧ f ∈ A → f : T ⟶ ℝ
stoweidlem37.6 ⊢ φ → Z ∈ T
Assertion stoweidlem37 ⊢ φ → P ⁡ Z = 0

Proof

Step Hyp Ref Expression
1 stoweidlem37.1 ⊢ Q = h ∈ A | h ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
2 stoweidlem37.2 ⊢ P = t ∈ T ⟼ 1 M ⁢ ∑ i = 1 M G ⁡ i ⁡ t
3 stoweidlem37.3 ⊢ φ → M ∈ ℕ
4 stoweidlem37.4 ⊢ φ → G : 1 … M ⟶ Q
5 stoweidlem37.5 ⊢ φ ∧ f ∈ A → f : T ⟶ ℝ
6 stoweidlem37.6 ⊢ φ → Z ∈ T
7 1 2 3 4 5 stoweidlem30 ⊢ φ ∧ Z ∈ T → P ⁡ Z = 1 M ⁢ ∑ i = 1 M G ⁡ i ⁡ Z
8 6 7 mpdan ⊢ φ → P ⁡ Z = 1 M ⁢ ∑ i = 1 M G ⁡ i ⁡ Z
9 4 ffvelrnda ⊢ φ ∧ i ∈ 1 … M → G ⁡ i ∈ Q
10 fveq1 ⊢ h = G ⁡ i → h ⁡ Z = G ⁡ i ⁡ Z
11 10 eqeq1d ⊢ h = G ⁡ i → h ⁡ Z = 0 ↔ G ⁡ i ⁡ Z = 0
12 fveq1 ⊢ h = G ⁡ i → h ⁡ t = G ⁡ i ⁡ t
13 12 breq2d ⊢ h = G ⁡ i → 0 ≤ h ⁡ t ↔ 0 ≤ G ⁡ i ⁡ t
14 12 breq1d ⊢ h = G ⁡ i → h ⁡ t ≤ 1 ↔ G ⁡ i ⁡ t ≤ 1
15 13 14 anbi12d ⊢ h = G ⁡ i → 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ 0 ≤ G ⁡ i ⁡ t ∧ G ⁡ i ⁡ t ≤ 1
16 15 ralbidv ⊢ h = G ⁡ i → ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ ∀ t ∈ T 0 ≤ G ⁡ i ⁡ t ∧ G ⁡ i ⁡ t ≤ 1
17 11 16 anbi12d ⊢ h = G ⁡ i → h ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ G ⁡ i ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ G ⁡ i ⁡ t ∧ G ⁡ i ⁡ t ≤ 1
18 17 1 elrab2 ⊢ G ⁡ i ∈ Q ↔ G ⁡ i ∈ A ∧ G ⁡ i ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ G ⁡ i ⁡ t ∧ G ⁡ i ⁡ t ≤ 1
19 9 18 sylib ⊢ φ ∧ i ∈ 1 … M → G ⁡ i ∈ A ∧ G ⁡ i ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ G ⁡ i ⁡ t ∧ G ⁡ i ⁡ t ≤ 1
20 19 simprld ⊢ φ ∧ i ∈ 1 … M → G ⁡ i ⁡ Z = 0
21 20 sumeq2dv ⊢ φ → ∑ i = 1 M G ⁡ i ⁡ Z = ∑ i = 1 M 0
22 fzfi ⊢ 1 … M ∈ Fin
23 olc ⊢ 1 … M ∈ Fin → 1 … M ⊆ ℤ ≥ 1 ∨ 1 … M ∈ Fin
24 sumz ⊢ 1 … M ⊆ ℤ ≥ 1 ∨ 1 … M ∈ Fin → ∑ i = 1 M 0 = 0
25 22 23 24 mp2b ⊢ ∑ i = 1 M 0 = 0
26 21 25 eqtrdi ⊢ φ → ∑ i = 1 M G ⁡ i ⁡ Z = 0
27 26 oveq2d ⊢ φ → 1 M ⁢ ∑ i = 1 M G ⁡ i ⁡ Z = 1 M ⋅ 0
28 3 nncnd ⊢ φ → M ∈ ℂ
29 3 nnne0d ⊢ φ → M ≠ 0
30 28 29 reccld ⊢ φ → 1 M ∈ ℂ
31 30 mul01d ⊢ φ → 1 M ⋅ 0 = 0
32 8 27 31 3eqtrd ⊢ φ → P ⁡ Z = 0