Metamath Proof Explorer

Theorem stoweidlem15

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

Ref Expression
Hypotheses stoweidlem15.1 ⊢Q=h∈A|h⁡Z=0∧∀t∈T0≤h⁡t∧h⁡t≤1
stoweidlem15.3 ⊢φ→G:1…M⟶Q
stoweidlem15.4 ⊢φ∧f∈A→f:T⟶ℝ
Assertion stoweidlem15 ⊢φ∧I∈1…M∧S∈T→G⁡I⁡S∈ℝ∧0≤G⁡I⁡S∧G⁡I⁡S≤1

Proof

Step Hyp Ref Expression
1 stoweidlem15.1 ⊢Q=h∈A|h⁡Z=0∧∀t∈T0≤h⁡t∧h⁡t≤1
2 stoweidlem15.3 ⊢φ→G:1…M⟶Q
3 stoweidlem15.4 ⊢φ∧f∈A→f:T⟶ℝ
4 simpl ⊢φ∧I∈1…M→φ
5 2 ffvelcdmda ⊢φ∧I∈1…M→G⁡I∈Q
6 elrabi ⊢G⁡I∈h∈A|h⁡Z=0∧∀t∈T0≤h⁡t∧h⁡t≤1→G⁡I∈A
7 6 1 eleq2s ⊢G⁡I∈Q→G⁡I∈A
8 5 7 syl ⊢φ∧I∈1…M→G⁡I∈A
9 eleq1 ⊢f=G⁡I→f∈A↔G⁡I∈A
10 9 anbi2d ⊢f=G⁡I→φ∧f∈A↔φ∧G⁡I∈A
11 feq1 ⊢f=G⁡I→f:T⟶ℝ↔G⁡I:T⟶ℝ
12 10 11 imbi12d ⊢f=G⁡I→φ∧f∈A→f:T⟶ℝ↔φ∧G⁡I∈A→G⁡I:T⟶ℝ
13 12 3 vtoclg ⊢G⁡I∈A→φ∧G⁡I∈A→G⁡I:T⟶ℝ
14 8 13 syl ⊢φ∧I∈1…M→φ∧G⁡I∈A→G⁡I:T⟶ℝ
15 4 8 14 mp2and ⊢φ∧I∈1…M→G⁡I:T⟶ℝ
16 15 ffvelcdmda ⊢φ∧I∈1…M∧S∈T→G⁡I⁡S∈ℝ
17 5 1 eleqtrdi ⊢φ∧I∈1…M→G⁡I∈h∈A|h⁡Z=0∧∀t∈T0≤h⁡t∧h⁡t≤1
18 fveq1 ⊢h=G⁡I→h⁡Z=G⁡I⁡Z
19 18 eqeq1d ⊢h=G⁡I→h⁡Z=0↔G⁡I⁡Z=0
20 fveq1 ⊢h=G⁡I→h⁡t=G⁡I⁡t
21 20 breq2d ⊢h=G⁡I→0≤h⁡t↔0≤G⁡I⁡t
22 20 breq1d ⊢h=G⁡I→h⁡t≤1↔G⁡I⁡t≤1
23 21 22 anbi12d ⊢h=G⁡I→0≤h⁡t∧h⁡t≤1↔0≤G⁡I⁡t∧G⁡I⁡t≤1
24 23 ralbidv ⊢h=G⁡I→∀t∈T0≤h⁡t∧h⁡t≤1↔∀t∈T0≤G⁡I⁡t∧G⁡I⁡t≤1
25 19 24 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
26 25 elrab ⊢G⁡I∈h∈A|h⁡Z=0∧∀t∈T0≤h⁡t∧h⁡t≤1↔G⁡I∈A∧G⁡I⁡Z=0∧∀t∈T0≤G⁡I⁡t∧G⁡I⁡t≤1
27 17 26 sylib ⊢φ∧I∈1…M→G⁡I∈A∧G⁡I⁡Z=0∧∀t∈T0≤G⁡I⁡t∧G⁡I⁡t≤1
28 27 simprd ⊢φ∧I∈1…M→G⁡I⁡Z=0∧∀t∈T0≤G⁡I⁡t∧G⁡I⁡t≤1
29 28 simprd ⊢φ∧I∈1…M→∀t∈T0≤G⁡I⁡t∧G⁡I⁡t≤1
30 fveq2 ⊢s=t→G⁡I⁡s=G⁡I⁡t
31 30 breq2d ⊢s=t→0≤G⁡I⁡s↔0≤G⁡I⁡t
32 30 breq1d ⊢s=t→G⁡I⁡s≤1↔G⁡I⁡t≤1
33 31 32 anbi12d ⊢s=t→0≤G⁡I⁡s∧G⁡I⁡s≤1↔0≤G⁡I⁡t∧G⁡I⁡t≤1
34 33 cbvralvw ⊢∀s∈T0≤G⁡I⁡s∧G⁡I⁡s≤1↔∀t∈T0≤G⁡I⁡t∧G⁡I⁡t≤1
35 fveq2 ⊢s=S→G⁡I⁡s=G⁡I⁡S
36 35 breq2d ⊢s=S→0≤G⁡I⁡s↔0≤G⁡I⁡S
37 35 breq1d ⊢s=S→G⁡I⁡s≤1↔G⁡I⁡S≤1
38 36 37 anbi12d ⊢s=S→0≤G⁡I⁡s∧G⁡I⁡s≤1↔0≤G⁡I⁡S∧G⁡I⁡S≤1
39 38 rspccva ⊢∀s∈T0≤G⁡I⁡s∧G⁡I⁡s≤1∧S∈T→0≤G⁡I⁡S∧G⁡I⁡S≤1
40 34 39 sylanbr ⊢∀t∈T0≤G⁡I⁡t∧G⁡I⁡t≤1∧S∈T→0≤G⁡I⁡S∧G⁡I⁡S≤1
41 29 40 sylan ⊢φ∧I∈1…M∧S∈T→0≤G⁡I⁡S∧G⁡I⁡S≤1
42 41 simpld ⊢φ∧I∈1…M∧S∈T→0≤G⁡I⁡S
43 41 simprd ⊢φ∧I∈1…M∧S∈T→G⁡I⁡S≤1
44 16 42 43 3jca ⊢φ∧I∈1…M∧S∈T→G⁡I⁡S∈ℝ∧0≤G⁡I⁡S∧G⁡I⁡S≤1