Metamath Proof Explorer

Theorem stoweidlem52

Description: There exists a neighborhood V as in Lemma 1 of BrosowskiDeutsh p. 90. Here Z is used to represent t_0 in the paper, and v is used to represent V in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem52.1 ⊢ Ⅎ 𝑡 𝑈
stoweidlem52.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem52.3 ⊢ Ⅎ 𝑡 𝑃
stoweidlem52.4 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem52.5 ⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
stoweidlem52.7 ⊢ 𝑇 = ∪ 𝐽
stoweidlem52.8 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
stoweidlem52.9 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
stoweidlem52.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem52.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem52.12 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
stoweidlem52.13 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
stoweidlem52.14 ⊢ ( 𝜑 → 𝐷 < 1 )
stoweidlem52.15 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
stoweidlem52.16 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
stoweidlem52.17 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
stoweidlem52.18 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
stoweidlem52.19 ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) = 0 )
stoweidlem52.20 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
Assertion stoweidlem52 ( 𝜑 → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem52.1 ⊢ Ⅎ 𝑡 𝑈
2 stoweidlem52.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem52.3 ⊢ Ⅎ 𝑡 𝑃
4 stoweidlem52.4 ⊢ 𝐾 = ( topGen ‘ ran (,) )
5 stoweidlem52.5 ⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
6 stoweidlem52.7 ⊢ 𝑇 = ∪ 𝐽
7 stoweidlem52.8 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
8 stoweidlem52.9 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
9 stoweidlem52.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
10 stoweidlem52.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
11 stoweidlem52.12 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
12 stoweidlem52.13 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
13 stoweidlem52.14 ⊢ ( 𝜑 → 𝐷 < 1 )
14 stoweidlem52.15 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
15 stoweidlem52.16 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
16 stoweidlem52.17 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
17 stoweidlem52.18 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
18 stoweidlem52.19 ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) = 0 )
19 stoweidlem52.20 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
20 nfcv ⊢ Ⅎ 𝑡 ( 𝐷 / 2 )
21 12 rpred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
22 21 rehalfcld ⊢ ( 𝜑 → ( 𝐷 / 2 ) ∈ ℝ )
23 22 rexrd ⊢ ( 𝜑 → ( 𝐷 / 2 ) ∈ ℝ* )
24 8 7 sseqtrdi ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
25 24 16 sseldd ⊢ ( 𝜑 → 𝑃 ∈ ( 𝐽 Cn 𝐾 ) )
26 20 3 2 4 6 5 23 25 rfcnpre2 ⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
27 elssuni ⊢ ( 𝑈 ∈ 𝐽 → 𝑈 ⊆ ∪ 𝐽 )
28 14 27 syl ⊢ ( 𝜑 → 𝑈 ⊆ ∪ 𝐽 )
29 28 6 sseqtrrdi ⊢ ( 𝜑 → 𝑈 ⊆ 𝑇 )
30 29 15 sseldd ⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
31 2re ⊢ 2 ∈ ℝ
32 31 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
33 12 rpgt0d ⊢ ( 𝜑 → 0 < 𝐷 )
34 2pos ⊢ 0 < 2
35 34 a1i ⊢ ( 𝜑 → 0 < 2 )
36 21 32 33 35 divgt0d ⊢ ( 𝜑 → 0 < ( 𝐷 / 2 ) )
37 18 36 eqbrtrd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑍 ) < ( 𝐷 / 2 ) )
38 nfcv ⊢ Ⅎ 𝑡 𝑍
39 nfcv ⊢ Ⅎ 𝑡 𝑇
40 3 38 nffv ⊢ Ⅎ 𝑡 ( 𝑃 ‘ 𝑍 )
41 nfcv ⊢ Ⅎ 𝑡 <
42 40 41 20 nfbr ⊢ Ⅎ 𝑡 ( 𝑃 ‘ 𝑍 ) < ( 𝐷 / 2 )
43 fveq2 ⊢ ( 𝑡 = 𝑍 → ( 𝑃 ‘ 𝑡 ) = ( 𝑃 ‘ 𝑍 ) )
44 43 breq1d ⊢ ( 𝑡 = 𝑍 → ( ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) ↔ ( 𝑃 ‘ 𝑍 ) < ( 𝐷 / 2 ) ) )
45 38 39 42 44 elrabf ⊢ ( 𝑍 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) } ↔ ( 𝑍 ∈ 𝑇 ∧ ( 𝑃 ‘ 𝑍 ) < ( 𝐷 / 2 ) ) )
46 30 37 45 sylanbrc ⊢ ( 𝜑 → 𝑍 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) } )
47 46 5 eleqtrrdi ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
48 nfrab1 ⊢ Ⅎ 𝑡 { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
49 5 48 nfcxfr ⊢ Ⅎ 𝑡 𝑉
50 8 16 sseldd ⊢ ( 𝜑 → 𝑃 ∈ 𝐶 )
51 4 6 7 50 fcnre ⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝑃 : 𝑇 ⟶ ℝ )
53 5 rabeq2i ⊢ ( 𝑡 ∈ 𝑉 ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) ) )
54 53 biimpi ⊢ ( 𝑡 ∈ 𝑉 → ( 𝑡 ∈ 𝑇 ∧ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) ) )
55 54 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑡 ∈ 𝑇 ∧ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) ) )
56 55 simpld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝑡 ∈ 𝑇 )
57 52 56 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
58 22 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐷 / 2 ) ∈ ℝ )
59 21 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝐷 ∈ ℝ )
60 55 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) )
61 halfpos ⊢ ( 𝐷 ∈ ℝ → ( 0 < 𝐷 ↔ ( 𝐷 / 2 ) < 𝐷 ) )
62 21 61 syl ⊢ ( 𝜑 → ( 0 < 𝐷 ↔ ( 𝐷 / 2 ) < 𝐷 ) )
63 33 62 mpbid ⊢ ( 𝜑 → ( 𝐷 / 2 ) < 𝐷 )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐷 / 2 ) < 𝐷 )
65 57 58 59 60 64 lttrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) < 𝐷 )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ( 𝑃 ‘ 𝑡 ) < 𝐷 )
67 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → 𝐷 ∈ ℝ )
68 57 adantr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
69 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
70 56 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ( 𝑡 ∈ 𝑇 ∧ ¬ 𝑡 ∈ 𝑈 ) )
71 eldif ⊢ ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ↔ ( 𝑡 ∈ 𝑇 ∧ ¬ 𝑡 ∈ 𝑈 ) )
72 70 71 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) )
73 rsp ⊢ ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) → ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) → 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) ) )
74 69 72 73 sylc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
75 67 68 74 lensymd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) ∧ ¬ 𝑡 ∈ 𝑈 ) → ¬ ( 𝑃 ‘ 𝑡 ) < 𝐷 )
76 66 75 condan ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝑡 ∈ 𝑈 )
77 76 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑉 → 𝑡 ∈ 𝑈 ) )
78 2 49 1 77 ssrd ⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
79 nfv ⊢ Ⅎ 𝑡 𝑒 ∈ ℝ+
80 2 79 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑒 ∈ ℝ+ )
81 nfv ⊢ Ⅎ 𝑡 𝑦 ∈ 𝐴
82 80 81 nfan ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 )
83 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 )
84 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 )
85 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒
86 83 84 85 nf3an ⊢ Ⅎ 𝑡 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 )
87 82 86 nfan ⊢ Ⅎ 𝑡 ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) )
88 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( 𝑦 ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( 𝑦 ‘ 𝑡 ) ) )
89 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ 1 ) = ( 𝑡 ∈ 𝑇 ↦ 1 )
90 ssrab2 ⊢ { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) } ⊆ 𝑇
91 5 90 eqsstri ⊢ 𝑉 ⊆ 𝑇
92 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → 𝑦 ∈ 𝐴 )
93 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → 𝜑 )
94 8 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐶 )
95 4 6 7 94 fcnre ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 : 𝑇 ⟶ ℝ )
96 93 92 95 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → 𝑦 : 𝑇 ⟶ ℝ )
97 8 sselda ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 ∈ 𝐶 )
98 4 6 7 97 fcnre ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
99 93 98 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
100 93 9 syl3an1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
101 93 10 syl3an1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
102 93 11 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
103 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → 𝑒 ∈ ℝ+ )
104 simpr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) )
105 simpr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) )
106 simpr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 )
107 87 88 89 91 92 96 99 100 101 102 103 104 105 106 stoweidlem41 ⊢ ( ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐴 ) ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) )
108 12 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝐷 ∈ ℝ+ )
109 13 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝐷 < 1 )
110 16 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑃 ∈ 𝐴 )
111 51 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑃 : 𝑇 ⟶ ℝ )
112 17 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
113 19 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
114 98 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
115 9 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
116 10 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
117 11 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑎 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑎 ) ∈ 𝐴 )
118 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ+ )
119 3 80 5 108 109 110 111 112 113 114 115 116 117 118 stoweidlem49 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝑒 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝑒 ) )
120 107 119 r19.29a ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) )
121 120 ralrimiva ⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) )
122 47 78 121 jca31 ⊢ ( 𝜑 → ( ( 𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
123 eleq2 ⊢ ( 𝑣 = 𝑉 → ( 𝑍 ∈ 𝑣 ↔ 𝑍 ∈ 𝑉 ) )
124 sseq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 ⊆ 𝑈 ↔ 𝑉 ⊆ 𝑈 ) )
125 123 124 anbi12d ⊢ ( 𝑣 = 𝑉 → ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ↔ ( 𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈 ) ) )
126 nfcv ⊢ Ⅎ 𝑡 𝑣
127 126 49 raleqf ⊢ ( 𝑣 = 𝑉 → ( ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ↔ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ) )
128 127 3anbi2d ⊢ ( 𝑣 = 𝑉 → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
129 128 rexbidv ⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
130 129 ralbidv ⊢ ( 𝑣 = 𝑉 → ( ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
131 125 130 anbi12d ⊢ ( 𝑣 = 𝑉 → ( ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) ↔ ( ( 𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) ) )
132 131 rspcev ⊢ ( ( 𝑉 ∈ 𝐽 ∧ ( ( 𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) ) → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )
133 26 122 132 syl2anc ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝐽 ( ( 𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈 ) ∧ ∀ 𝑒 ∈ ℝ+ ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑣 ( 𝑥 ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( 𝑥 ‘ 𝑡 ) ) ) )