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 ∈ T 0 ≤ 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 ∈ T 0 ≤ 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 ffvelrnda ⊢ φ ∧ I ∈ 1 … M → G ⁡ I ∈ Q
6 elrabi ⊢ G ⁡ I ∈ h ∈ A | h ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ 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 ffvelrnda ⊢ φ ∧ I ∈ 1 … M ∧ S ∈ T → G ⁡ I ⁡ S ∈ ℝ
17 5 1 eleqtrdi ⊢ φ ∧ I ∈ 1 … M → G ⁡ I ∈ h ∈ A | h ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ 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 ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ ∀ t ∈ T 0 ≤ G ⁡ I ⁡ t ∧ G ⁡ I ⁡ t ≤ 1
25 19 24 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
26 25 elrab ⊢ G ⁡ I ∈ h ∈ A | h ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ↔ G ⁡ I ∈ A ∧ G ⁡ I ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ G ⁡ I ⁡ t ∧ G ⁡ I ⁡ t ≤ 1
27 17 26 sylib ⊢ φ ∧ I ∈ 1 … M → G ⁡ I ∈ A ∧ G ⁡ I ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ G ⁡ I ⁡ t ∧ G ⁡ I ⁡ t ≤ 1
28 27 simprd ⊢ φ ∧ I ∈ 1 … M → G ⁡ I ⁡ Z = 0 ∧ ∀ t ∈ T 0 ≤ G ⁡ I ⁡ t ∧ G ⁡ I ⁡ t ≤ 1
29 28 simprd ⊢ φ ∧ I ∈ 1 … M → ∀ t ∈ T 0 ≤ 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 ∈ T 0 ≤ G ⁡ I ⁡ s ∧ G ⁡ I ⁡ s ≤ 1 ↔ ∀ t ∈ T 0 ≤ 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 ∈ T 0 ≤ G ⁡ I ⁡ s ∧ G ⁡ I ⁡ s ≤ 1 ∧ S ∈ T → 0 ≤ G ⁡ I ⁡ S ∧ G ⁡ I ⁡ S ≤ 1
40 34 39 sylanbr ⊢ ∀ t ∈ T 0 ≤ 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