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 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
stoweidlem15.3 ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 )
stoweidlem15.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
Assertion stoweidlem15 ( ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → ( ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ≤ 1 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem15.1 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
2 stoweidlem15.3 ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑀 ) ⟶ 𝑄 )
3 stoweidlem15.4 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
4 simpl ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) → 𝜑 )
5 2 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝑄 )
6 elrabi ⊢ ( ( 𝐺 ‘ 𝐼 ) ∈ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } → ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 )
7 6 1 eleq2s ⊢ ( ( 𝐺 ‘ 𝐼 ) ∈ 𝑄 → ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 )
8 5 7 syl ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 )
9 eleq1 ⊢ ( 𝑓 = ( 𝐺 ‘ 𝐼 ) → ( 𝑓 ∈ 𝐴 ↔ ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ) )
10 9 anbi2d ⊢ ( 𝑓 = ( 𝐺 ‘ 𝐼 ) → ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ) ) )
11 feq1 ⊢ ( 𝑓 = ( 𝐺 ‘ 𝐼 ) → ( 𝑓 : 𝑇 ⟶ ℝ ↔ ( 𝐺 ‘ 𝐼 ) : 𝑇 ⟶ ℝ ) )
12 10 11 imbi12d ⊢ ( 𝑓 = ( 𝐺 ‘ 𝐼 ) → ( ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝐼 ) : 𝑇 ⟶ ℝ ) ) )
13 12 3 vtoclg ⊢ ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 → ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝐼 ) : 𝑇 ⟶ ℝ ) )
14 8 13 syl ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝐼 ) : 𝑇 ⟶ ℝ ) )
15 4 8 14 mp2and ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝐼 ) : 𝑇 ⟶ ℝ )
16 15 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ∈ ℝ )
17 5 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ 𝐼 ) ∈ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } )
18 fveq1 ⊢ ( ℎ = ( 𝐺 ‘ 𝐼 ) → ( ℎ ‘ 𝑍 ) = ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑍 ) )
19 18 eqeq1d ⊢ ( ℎ = ( 𝐺 ‘ 𝐼 ) → ( ( ℎ ‘ 𝑍 ) = 0 ↔ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑍 ) = 0 ) )
20 fveq1 ⊢ ( ℎ = ( 𝐺 ‘ 𝐼 ) → ( ℎ ‘ 𝑡 ) = ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) )
21 20 breq2d ⊢ ( ℎ = ( 𝐺 ‘ 𝐼 ) → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ) )
22 20 breq1d ⊢ ( ℎ = ( 𝐺 ‘ 𝐼 ) → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) )
23 21 22 anbi12d ⊢ ( ℎ = ( 𝐺 ‘ 𝐼 ) → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) ) )
24 23 ralbidv ⊢ ( ℎ = ( 𝐺 ‘ 𝐼 ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) ) )
25 19 24 anbi12d ⊢ ( ℎ = ( 𝐺 ‘ 𝐼 ) → ( ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) ↔ ( ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) ) ) )
26 25 elrab ⊢ ( ( 𝐺 ‘ 𝐼 ) ∈ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } ↔ ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ∧ ( ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) ) ) )
27 17 26 sylib ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ‘ 𝐼 ) ∈ 𝐴 ∧ ( ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) ) ) )
28 27 simprd ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) ) )
29 28 simprd ⊢ ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) )
30 fveq2 ⊢ ( 𝑠 = 𝑡 → ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) = ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) )
31 30 breq2d ⊢ ( 𝑠 = 𝑡 → ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ↔ 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ) )
32 30 breq1d ⊢ ( 𝑠 = 𝑡 → ( ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ≤ 1 ↔ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) )
33 31 32 anbi12d ⊢ ( 𝑠 = 𝑡 → ( ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ≤ 1 ) ↔ ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) ) )
34 33 cbvralvw ⊢ ( ∀ 𝑠 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) )
35 fveq2 ⊢ ( 𝑠 = 𝑆 → ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) = ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) )
36 35 breq2d ⊢ ( 𝑠 = 𝑆 → ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ↔ 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ) )
37 35 breq1d ⊢ ( 𝑠 = 𝑆 → ( ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ≤ 1 ↔ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ≤ 1 ) )
38 36 37 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ≤ 1 ) ↔ ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ≤ 1 ) ) )
39 38 rspccva ⊢ ( ( ∀ 𝑠 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑠 ) ≤ 1 ) ∧ 𝑆 ∈ 𝑇 ) → ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ≤ 1 ) )
40 34 39 sylanbr ⊢ ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑡 ) ≤ 1 ) ∧ 𝑆 ∈ 𝑇 ) → ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ≤ 1 ) )
41 29 40 sylan ⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → ( 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ≤ 1 ) )
42 41 simpld ⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) )
43 41 simprd ⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ≤ 1 )
44 16 42 43 3jca ⊢ ( ( ( 𝜑 ∧ 𝐼 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑆 ∈ 𝑇 ) → ( ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ∧ ( ( 𝐺 ‘ 𝐼 ) ‘ 𝑆 ) ≤ 1 ) )