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∈T0≤h⁡t∧h⁡t≤1
stoweidlem37.2 ⊢P=t∈T⟼1M⁢∑i=1MG⁡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∈T0≤h⁡t∧h⁡t≤1
2 stoweidlem37.2 ⊢P=t∈T⟼1M⁢∑i=1MG⁡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=1M⁢∑i=1MG⁡i⁡Z
8 6 7 mpdan ⊢φ→P⁡Z=1M⁢∑i=1MG⁡i⁡Z
9 4 ffvelcdmda ⊢φ∧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∈T0≤h⁡t∧h⁡t≤1↔∀t∈T0≤G⁡i⁡t∧G⁡i⁡t≤1
17 11 16 anbi12d ⊢h=G⁡i→h⁡Z=0∧∀t∈T0≤h⁡t∧h⁡t≤1↔G⁡i⁡Z=0∧∀t∈T0≤G⁡i⁡t∧G⁡i⁡t≤1
18 17 1 elrab2 ⊢G⁡i∈Q↔G⁡i∈A∧G⁡i⁡Z=0∧∀t∈T0≤G⁡i⁡t∧G⁡i⁡t≤1
19 9 18 sylib ⊢φ∧i∈1…M→G⁡i∈A∧G⁡i⁡Z=0∧∀t∈T0≤G⁡i⁡t∧G⁡i⁡t≤1
20 19 simprld ⊢φ∧i∈1…M→G⁡i⁡Z=0
21 20 sumeq2dv ⊢φ→∑i=1MG⁡i⁡Z=∑i=1M0
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=1M0=0
25 22 23 24 mp2b ⊢∑i=1M0=0
26 21 25 eqtrdi ⊢φ→∑i=1MG⁡i⁡Z=0
27 26 oveq2d ⊢φ→1M⁢∑i=1MG⁡i⁡Z=1M⋅0
28 3 nncnd ⊢φ→M∈ℂ
29 3 nnne0d ⊢φ→M≠0
30 28 29 reccld ⊢φ→1M∈ℂ
31 30 mul01d ⊢φ→1M⋅0=0
32 8 27 31 3eqtrd ⊢φ→P⁡Z=0