Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem55 Structured version   Visualization version   GIF version

Theorem stoweidlem55 43984
Description: This lemma proves the existence of a function p as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90: p is in the subalgebra, such that 0 <= p <= 1, p_(t0) = 0, and p > 0 on T - U. Here Z is used to represent t0 in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem55.1 𝑡𝑈
stoweidlem55.2 𝑡𝜑
stoweidlem55.3 𝐾 = (topGen‘ran (,))
stoweidlem55.4 (𝜑𝐽 ∈ Comp)
stoweidlem55.5 𝑇 = 𝐽
stoweidlem55.6 𝐶 = (𝐽 Cn 𝐾)
stoweidlem55.7 (𝜑𝐴𝐶)
stoweidlem55.8 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
stoweidlem55.9 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem55.10 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
stoweidlem55.11 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
stoweidlem55.12 (𝜑𝑈𝐽)
stoweidlem55.13 (𝜑𝑍𝑈)
stoweidlem55.14 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
stoweidlem55.15 𝑊 = {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
Assertion
Ref Expression
stoweidlem55 (𝜑 → ∃𝑝𝐴 (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))
Distinct variable groups:   𝑓,𝑔,,𝑞,𝑡,𝑇   𝑓,𝑟,𝐴,𝑔,𝑞,𝑡   𝑥,𝑓,,𝑞,𝑡,𝑇   𝑄,𝑓,𝑔,𝑞   𝑈,𝑓,𝑔,,𝑞   𝑓,𝑍,𝑔,,𝑞,𝑡   𝜑,𝑓,𝑔,,𝑞   𝑤,𝑔,,𝑡,𝑇   𝑔,𝑊   𝐴,,𝑥   ,𝐽,𝑡,𝑤   𝑞,𝑝,𝑡,𝑇   𝐴,𝑝   𝑈,𝑝   𝑍,𝑝   𝑥,𝑟,𝑇   𝑈,𝑟,𝑥   𝜑,𝑟,𝑥   𝑡,𝐾   𝑥,𝑤,𝑄   𝑤,𝑈   𝜑,𝑤   𝑥,𝑍
Allowed substitution hints:   𝜑(𝑡,𝑝)   𝐴(𝑤)   𝐶(𝑥,𝑤,𝑡,𝑓,𝑔,,𝑟,𝑞,𝑝)   𝑄(𝑡,,𝑟,𝑝)   𝑈(𝑡)   𝐽(𝑥,𝑓,𝑔,𝑟,𝑞,𝑝)   𝐾(𝑥,𝑤,𝑓,𝑔,,𝑟,𝑞,𝑝)   𝑊(𝑥,𝑤,𝑡,𝑓,,𝑟,𝑞,𝑝)   𝑍(𝑤,𝑟)

Proof of Theorem stoweidlem55
StepHypRef Expression
1 0re 11079 . . . . 5 0 ∈ ℝ
2 stoweidlem55.10 . . . . . 6 ((𝜑𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
32stoweidlem4 43933 . . . . 5 ((𝜑 ∧ 0 ∈ ℝ) → (𝑡𝑇 ↦ 0) ∈ 𝐴)
41, 3mpan2 688 . . . 4 (𝜑 → (𝑡𝑇 ↦ 0) ∈ 𝐴)
54adantr 481 . . 3 ((𝜑 ∧ (𝑇𝑈) = ∅) → (𝑡𝑇 ↦ 0) ∈ 𝐴)
6 stoweidlem55.2 . . . . 5 𝑡𝜑
7 nfcv 2904 . . . . . . 7 𝑡𝑇
8 stoweidlem55.1 . . . . . . 7 𝑡𝑈
97, 8nfdif 4073 . . . . . 6 𝑡(𝑇𝑈)
10 nfcv 2904 . . . . . 6 𝑡
119, 10nfeq 2917 . . . . 5 𝑡(𝑇𝑈) = ∅
126, 11nfan 1901 . . . 4 𝑡(𝜑 ∧ (𝑇𝑈) = ∅)
13 0le0 12176 . . . . . . . 8 0 ≤ 0
14 0cn 11069 . . . . . . . . 9 0 ∈ ℂ
15 eqid 2736 . . . . . . . . . 10 (𝑡𝑇 ↦ 0) = (𝑡𝑇 ↦ 0)
1615fvmpt2 6943 . . . . . . . . 9 ((𝑡𝑇 ∧ 0 ∈ ℂ) → ((𝑡𝑇 ↦ 0)‘𝑡) = 0)
1714, 16mpan2 688 . . . . . . . 8 (𝑡𝑇 → ((𝑡𝑇 ↦ 0)‘𝑡) = 0)
1813, 17breqtrrid 5131 . . . . . . 7 (𝑡𝑇 → 0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡))
1918adantl 482 . . . . . 6 (((𝜑 ∧ (𝑇𝑈) = ∅) ∧ 𝑡𝑇) → 0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡))
20 0le1 11600 . . . . . . . 8 0 ≤ 1
2117, 20eqbrtrdi 5132 . . . . . . 7 (𝑡𝑇 → ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1)
2221adantl 482 . . . . . 6 (((𝜑 ∧ (𝑇𝑈) = ∅) ∧ 𝑡𝑇) → ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1)
2319, 22jca 512 . . . . 5 (((𝜑 ∧ (𝑇𝑈) = ∅) ∧ 𝑡𝑇) → (0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡) ∧ ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1))
2423ex 413 . . . 4 ((𝜑 ∧ (𝑇𝑈) = ∅) → (𝑡𝑇 → (0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡) ∧ ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1)))
2512, 24ralrimi 3236 . . 3 ((𝜑 ∧ (𝑇𝑈) = ∅) → ∀𝑡𝑇 (0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡) ∧ ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1))
26 stoweidlem55.13 . . . . . 6 (𝜑𝑍𝑈)
27 stoweidlem55.12 . . . . . 6 (𝜑𝑈𝐽)
2826, 27jca 512 . . . . 5 (𝜑 → (𝑍𝑈𝑈𝐽))
29 elunii 4858 . . . . . 6 ((𝑍𝑈𝑈𝐽) → 𝑍 𝐽)
30 stoweidlem55.5 . . . . . 6 𝑇 = 𝐽
3129, 30eleqtrrdi 2848 . . . . 5 ((𝑍𝑈𝑈𝐽) → 𝑍𝑇)
32 eqidd 2737 . . . . . 6 (𝑡 = 𝑍 → 0 = 0)
33 c0ex 11071 . . . . . 6 0 ∈ V
3432, 15, 33fvmpt 6932 . . . . 5 (𝑍𝑇 → ((𝑡𝑇 ↦ 0)‘𝑍) = 0)
3528, 31, 343syl 18 . . . 4 (𝜑 → ((𝑡𝑇 ↦ 0)‘𝑍) = 0)
3635adantr 481 . . 3 ((𝜑 ∧ (𝑇𝑈) = ∅) → ((𝑡𝑇 ↦ 0)‘𝑍) = 0)
3711rzalf 42933 . . . 4 ((𝑇𝑈) = ∅ → ∀𝑡 ∈ (𝑇𝑈)0 < ((𝑡𝑇 ↦ 0)‘𝑡))
3837adantl 482 . . 3 ((𝜑 ∧ (𝑇𝑈) = ∅) → ∀𝑡 ∈ (𝑇𝑈)0 < ((𝑡𝑇 ↦ 0)‘𝑡))
39 nfcv 2904 . . . . . . 7 𝑡𝑝
40 nfmpt1 5201 . . . . . . 7 𝑡(𝑡𝑇 ↦ 0)
4139, 40nfeq 2917 . . . . . 6 𝑡 𝑝 = (𝑡𝑇 ↦ 0)
42 fveq1 6825 . . . . . . . 8 (𝑝 = (𝑡𝑇 ↦ 0) → (𝑝𝑡) = ((𝑡𝑇 ↦ 0)‘𝑡))
4342breq2d 5105 . . . . . . 7 (𝑝 = (𝑡𝑇 ↦ 0) → (0 ≤ (𝑝𝑡) ↔ 0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡)))
4442breq1d 5103 . . . . . . 7 (𝑝 = (𝑡𝑇 ↦ 0) → ((𝑝𝑡) ≤ 1 ↔ ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1))
4543, 44anbi12d 631 . . . . . 6 (𝑝 = (𝑡𝑇 ↦ 0) → ((0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ↔ (0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡) ∧ ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1)))
4641, 45ralbid 3252 . . . . 5 (𝑝 = (𝑡𝑇 ↦ 0) → (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡) ∧ ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1)))
47 fveq1 6825 . . . . . 6 (𝑝 = (𝑡𝑇 ↦ 0) → (𝑝𝑍) = ((𝑡𝑇 ↦ 0)‘𝑍))
4847eqeq1d 2738 . . . . 5 (𝑝 = (𝑡𝑇 ↦ 0) → ((𝑝𝑍) = 0 ↔ ((𝑡𝑇 ↦ 0)‘𝑍) = 0))
4942breq2d 5105 . . . . . 6 (𝑝 = (𝑡𝑇 ↦ 0) → (0 < (𝑝𝑡) ↔ 0 < ((𝑡𝑇 ↦ 0)‘𝑡)))
5041, 49ralbid 3252 . . . . 5 (𝑝 = (𝑡𝑇 ↦ 0) → (∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡) ↔ ∀𝑡 ∈ (𝑇𝑈)0 < ((𝑡𝑇 ↦ 0)‘𝑡)))
5146, 48, 503anbi123d 1435 . . . 4 (𝑝 = (𝑡𝑇 ↦ 0) → ((∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)) ↔ (∀𝑡𝑇 (0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡) ∧ ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1) ∧ ((𝑡𝑇 ↦ 0)‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < ((𝑡𝑇 ↦ 0)‘𝑡))))
5251rspcev 3570 . . 3 (((𝑡𝑇 ↦ 0) ∈ 𝐴 ∧ (∀𝑡𝑇 (0 ≤ ((𝑡𝑇 ↦ 0)‘𝑡) ∧ ((𝑡𝑇 ↦ 0)‘𝑡) ≤ 1) ∧ ((𝑡𝑇 ↦ 0)‘𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < ((𝑡𝑇 ↦ 0)‘𝑡))) → ∃𝑝𝐴 (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))
535, 25, 36, 38, 52syl13anc 1371 . 2 ((𝜑 ∧ (𝑇𝑈) = ∅) → ∃𝑝𝐴 (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))
5411nfn 1859 . . . 4 𝑡 ¬ (𝑇𝑈) = ∅
556, 54nfan 1901 . . 3 𝑡(𝜑 ∧ ¬ (𝑇𝑈) = ∅)
56 stoweidlem55.3 . . 3 𝐾 = (topGen‘ran (,))
57 stoweidlem55.14 . . 3 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
58 stoweidlem55.15 . . 3 𝑊 = {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
59 stoweidlem55.6 . . 3 𝐶 = (𝐽 Cn 𝐾)
60 stoweidlem55.4 . . . 4 (𝜑𝐽 ∈ Comp)
6160adantr 481 . . 3 ((𝜑 ∧ ¬ (𝑇𝑈) = ∅) → 𝐽 ∈ Comp)
62 stoweidlem55.7 . . . 4 (𝜑𝐴𝐶)
6362adantr 481 . . 3 ((𝜑 ∧ ¬ (𝑇𝑈) = ∅) → 𝐴𝐶)
64 stoweidlem55.8 . . . 4 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
65643adant1r 1176 . . 3 (((𝜑 ∧ ¬ (𝑇𝑈) = ∅) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
66 stoweidlem55.9 . . . 4 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
67663adant1r 1176 . . 3 (((𝜑 ∧ ¬ (𝑇𝑈) = ∅) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
682adantlr 712 . . 3 (((𝜑 ∧ ¬ (𝑇𝑈) = ∅) ∧ 𝑥 ∈ ℝ) → (𝑡𝑇𝑥) ∈ 𝐴)
69 stoweidlem55.11 . . . 4 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
7069adantlr 712 . . 3 (((𝜑 ∧ ¬ (𝑇𝑈) = ∅) ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
7127adantr 481 . . 3 ((𝜑 ∧ ¬ (𝑇𝑈) = ∅) → 𝑈𝐽)
72 neqne 2948 . . . 4 (¬ (𝑇𝑈) = ∅ → (𝑇𝑈) ≠ ∅)
7372adantl 482 . . 3 ((𝜑 ∧ ¬ (𝑇𝑈) = ∅) → (𝑇𝑈) ≠ ∅)
7426adantr 481 . . 3 ((𝜑 ∧ ¬ (𝑇𝑈) = ∅) → 𝑍𝑈)
758, 55, 56, 57, 58, 30, 59, 61, 63, 65, 67, 68, 70, 71, 73, 74stoweidlem53 43982 . 2 ((𝜑 ∧ ¬ (𝑇𝑈) = ∅) → ∃𝑝𝐴 (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))
7653, 75pm2.61dan 810 1 (𝜑 → ∃𝑝𝐴 (∀𝑡𝑇 (0 ≤ (𝑝𝑡) ∧ (𝑝𝑡) ≤ 1) ∧ (𝑝𝑍) = 0 ∧ ∀𝑡 ∈ (𝑇𝑈)0 < (𝑝𝑡)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1086   = wceq 1540  wnf 1784  wcel 2105  wnfc 2884  wne 2940  wral 3061  wrex 3070  {crab 3403  cdif 3895  wss 3898  c0 4270   cuni 4853   class class class wbr 5093  cmpt 5176  ran crn 5622  cfv 6480  (class class class)co 7338  cc 10971  cr 10972  0cc0 10973  1c1 10974   + caddc 10976   · cmul 10978   < clt 11111  cle 11112  (,)cioo 13181  topGenctg 17246   Cn ccn 22482  Compccmp 22644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-inf2 9499  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-pre-sup 11051  ax-mulf 11053
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-tp 4579  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-iin 4945  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-se 5577  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-isom 6489  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-of 7596  df-om 7782  df-1st 7900  df-2nd 7901  df-supp 8049  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-2o 8369  df-er 8570  df-map 8689  df-ixp 8758  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-fsupp 9228  df-fi 9269  df-sup 9300  df-inf 9301  df-oi 9368  df-card 9797  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-div 11735  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-7 12143  df-8 12144  df-9 12145  df-n0 12336  df-z 12422  df-dec 12540  df-uz 12685  df-q 12791  df-rp 12833  df-xneg 12950  df-xadd 12951  df-xmul 12952  df-ioo 13185  df-ico 13187  df-icc 13188  df-fz 13342  df-fzo 13485  df-seq 13824  df-exp 13885  df-hash 14147  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-clim 15297  df-sum 15498  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-rest 17231  df-topn 17232  df-0g 17250  df-gsum 17251  df-topgen 17252  df-pt 17253  df-prds 17256  df-xrs 17311  df-qtop 17316  df-imas 17317  df-xps 17319  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-submnd 18529  df-mulg 18798  df-cntz 19020  df-cmn 19484  df-psmet 20696  df-xmet 20697  df-met 20698  df-bl 20699  df-mopn 20700  df-cnfld 20705  df-top 22150  df-topon 22167  df-topsp 22189  df-bases 22203  df-cld 22277  df-cn 22485  df-cnp 22486  df-cmp 22645  df-tx 22820  df-hmeo 23013  df-xms 23580  df-ms 23581  df-tms 23582
This theorem is referenced by:  stoweidlem56  43985
  Copyright terms: Public domain W3C validator