Metamath Proof Explorer

Theorem stoweidlem53

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 0 < p on T \ U . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem53.1 ⊢ Ⅎ 𝑡 𝑈
stoweidlem53.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem53.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem53.4 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
stoweidlem53.5 ⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
stoweidlem53.6 ⊢ 𝑇 = ∪ 𝐽
stoweidlem53.7 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
stoweidlem53.8 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
stoweidlem53.9 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
stoweidlem53.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem53.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem53.12 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem53.13 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
stoweidlem53.14 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
stoweidlem53.15 ⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ≠ ∅ )
stoweidlem53.16 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
Assertion stoweidlem53 ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem53.1 ⊢ Ⅎ 𝑡 𝑈
2 stoweidlem53.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem53.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
4 stoweidlem53.4 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
5 stoweidlem53.5 ⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
6 stoweidlem53.6 ⊢ 𝑇 = ∪ 𝐽
7 stoweidlem53.7 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
8 stoweidlem53.8 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
9 stoweidlem53.9 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
10 stoweidlem53.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
11 stoweidlem53.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
12 stoweidlem53.12 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
13 stoweidlem53.13 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
14 stoweidlem53.14 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
15 stoweidlem53.15 ⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ≠ ∅ )
16 stoweidlem53.16 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 16 stoweidlem50 ⊢ ( 𝜑 → ∃ 𝑢 ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
18 nfv ⊢ Ⅎ 𝑡 𝑢 ∈ Fin
19 nfcv ⊢ Ⅎ 𝑡 𝑢
20 nfv ⊢ Ⅎ 𝑡 ( ℎ ‘ 𝑍 ) = 0
21 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 )
22 20 21 nfan ⊢ Ⅎ 𝑡 ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) )
23 nfcv ⊢ Ⅎ 𝑡 𝐴
24 22 23 nfrabw ⊢ Ⅎ 𝑡 { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
25 4 24 nfcxfr ⊢ Ⅎ 𝑡 𝑄
26 nfrab1 ⊢ Ⅎ 𝑡 { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) }
27 26 nfeq2 ⊢ Ⅎ 𝑡 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) }
28 25 27 nfrex ⊢ Ⅎ 𝑡 ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) }
29 nfcv ⊢ Ⅎ 𝑡 𝐽
30 28 29 nfrabw ⊢ Ⅎ 𝑡 { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
31 5 30 nfcxfr ⊢ Ⅎ 𝑡 𝑊
32 19 31 nfss ⊢ Ⅎ 𝑡 𝑢 ⊆ 𝑊
33 nfcv ⊢ Ⅎ 𝑡 𝑇
34 33 1 nfdif ⊢ Ⅎ 𝑡 ( 𝑇 ∖ 𝑈 )
35 nfcv ⊢ Ⅎ 𝑡 ∪ 𝑢
36 34 35 nfss ⊢ Ⅎ 𝑡 ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢
37 18 32 36 nf3an ⊢ Ⅎ 𝑡 ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 )
38 2 37 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
39 nfv ⊢ Ⅎ 𝑤 𝜑
40 nfv ⊢ Ⅎ 𝑤 𝑢 ∈ Fin
41 nfcv ⊢ Ⅎ 𝑤 𝑢
42 nfrab1 ⊢ Ⅎ 𝑤 { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
43 5 42 nfcxfr ⊢ Ⅎ 𝑤 𝑊
44 41 43 nfss ⊢ Ⅎ 𝑤 𝑢 ⊆ 𝑊
45 nfv ⊢ Ⅎ 𝑤 ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢
46 40 44 45 nf3an ⊢ Ⅎ 𝑤 ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 )
47 39 46 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
48 nfv ⊢ Ⅎ ℎ 𝜑
49 nfv ⊢ Ⅎ ℎ 𝑢 ∈ Fin
50 nfcv ⊢ Ⅎ ℎ 𝑢
51 nfre1 ⊢ Ⅎ ℎ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) }
52 nfcv ⊢ Ⅎ ℎ 𝐽
53 51 52 nfrabw ⊢ Ⅎ ℎ { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
54 5 53 nfcxfr ⊢ Ⅎ ℎ 𝑊
55 50 54 nfss ⊢ Ⅎ ℎ 𝑢 ⊆ 𝑊
56 nfv ⊢ Ⅎ ℎ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢
57 49 55 56 nf3an ⊢ Ⅎ ℎ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 )
58 48 57 nfan ⊢ Ⅎ ℎ ( 𝜑 ∧ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) )
59 eqid ⊢ ( 𝑤 ∈ 𝑢 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) = ( 𝑤 ∈ 𝑢 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
60 cmptop ⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top )
61 8 60 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
62 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
63 3 62 eqeltri ⊢ 𝐾 ∈ Top
64 cnfex ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 Cn 𝐾 ) ∈ V )
65 61 63 64 sylancl ⊢ ( 𝜑 → ( 𝐽 Cn 𝐾 ) ∈ V )
66 9 7 sseqtrdi ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
67 65 66 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
68 67 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → 𝐴 ∈ V )
69 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → 𝑢 ∈ Fin )
70 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → 𝑢 ⊆ 𝑊 )
71 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 )
72 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → ( 𝑇 ∖ 𝑈 ) ≠ ∅ )
73 38 47 58 4 5 59 68 69 70 71 72 stoweidlem35 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ Fin ∧ 𝑢 ⊆ 𝑊 ∧ ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑢 ) ) → ∃ 𝑚 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
74 17 73 exlimddv ⊢ ( 𝜑 → ∃ 𝑚 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
75 nfv ⊢ Ⅎ 𝑖 𝜑
76 nfv ⊢ Ⅎ 𝑖 𝑚 ∈ ℕ
77 nfv ⊢ Ⅎ 𝑖 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄
78 nfcv ⊢ Ⅎ 𝑖 ( 𝑇 ∖ 𝑈 )
79 nfre1 ⊢ Ⅎ 𝑖 ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 )
80 78 79 nfralw ⊢ Ⅎ 𝑖 ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 )
81 77 80 nfan ⊢ Ⅎ 𝑖 ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) )
82 76 81 nfan ⊢ Ⅎ 𝑖 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) )
83 75 82 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
84 nfv ⊢ Ⅎ 𝑡 𝑚 ∈ ℕ
85 nfcv ⊢ Ⅎ 𝑡 𝑞
86 nfcv ⊢ Ⅎ 𝑡 ( 1 ... 𝑚 )
87 85 86 25 nff ⊢ Ⅎ 𝑡 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄
88 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 )
89 87 88 nfan ⊢ Ⅎ 𝑡 ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) )
90 84 89 nfan ⊢ Ⅎ 𝑡 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) )
91 2 90 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
92 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑚 ) · Σ 𝑦 ∈ ( 1 ... 𝑚 ) ( ( 𝑞 ‘ 𝑦 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 / 𝑚 ) · Σ 𝑦 ∈ ( 1 ... 𝑚 ) ( ( 𝑞 ‘ 𝑦 ) ‘ 𝑡 ) ) )
93 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝑚 ∈ ℕ )
94 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 )
95 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) )
96 66 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
97 10 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
98 11 3adant1r ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
99 12 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
100 elssuni ⊢ ( 𝑈 ∈ 𝐽 → 𝑈 ⊆ ∪ 𝐽 )
101 100 6 sseqtrrdi ⊢ ( 𝑈 ∈ 𝐽 → 𝑈 ⊆ 𝑇 )
102 14 101 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝑇 )
103 102 16 sseldd ⊢ ( 𝜑 → 𝑍 ∈ 𝑇 )
104 103 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → 𝑍 ∈ 𝑇 )
105 83 91 3 4 92 93 94 95 6 96 97 98 99 104 stoweidlem44 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )
106 105 ex ⊢ ( 𝜑 → ( ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) )
107 106 exlimdvv ⊢ ( 𝜑 → ( ∃ 𝑚 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) ) )
108 74 107 mpd ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑝 ‘ 𝑡 ) ∧ ( 𝑝 ‘ 𝑡 ) ≤ 1 ) ∧ ( 𝑝 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 0 < ( 𝑝 ‘ 𝑡 ) ) )