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

Theorem stoweidlem21 45035
Description: Once the Stone Weierstrass theorem has been proven for approximating nonnegative functions, then this lemma is used to extend the result to functions with (possibly) negative values. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem21.1 Ⅎ𝑑𝐺
stoweidlem21.2 Ⅎ𝑑𝐻
stoweidlem21.3 Ⅎ𝑑𝑆
stoweidlem21.4 β„²π‘‘πœ‘
stoweidlem21.5 𝐺 = (𝑑 ∈ 𝑇 ↦ ((π»β€˜π‘‘) + 𝑆))
stoweidlem21.6 (πœ‘ β†’ 𝐹:π‘‡βŸΆβ„)
stoweidlem21.7 (πœ‘ β†’ 𝑆 ∈ ℝ)
stoweidlem21.8 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
stoweidlem21.9 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴)
stoweidlem21.10 (πœ‘ β†’ βˆ€π‘“ ∈ 𝐴 𝑓:π‘‡βŸΆβ„)
stoweidlem21.11 (πœ‘ β†’ 𝐻 ∈ 𝐴)
stoweidlem21.12 (πœ‘ β†’ βˆ€π‘‘ ∈ 𝑇 (absβ€˜((π»β€˜π‘‘) βˆ’ ((πΉβ€˜π‘‘) βˆ’ 𝑆))) < 𝐸)
Assertion
Ref Expression
stoweidlem21 (πœ‘ β†’ βˆƒπ‘“ ∈ 𝐴 βˆ€π‘‘ ∈ 𝑇 (absβ€˜((π‘“β€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸)
Distinct variable groups:   𝑓,𝑔,𝑑,𝑇   𝐴,𝑓,𝑔   𝑓,𝐸,𝑔   𝑓,𝐹,𝑔   𝑓,𝐺,𝑔   𝑓,𝐻,𝑔   πœ‘,𝑓,𝑔   𝑆,𝑔   π‘₯,𝑑,𝑇   π‘₯,𝐴   π‘₯,𝑆   πœ‘,π‘₯
Allowed substitution hints:   πœ‘(𝑑)   𝐴(𝑑)   𝑆(𝑑,𝑓)   𝐸(π‘₯,𝑑)   𝐹(π‘₯,𝑑)   𝐺(π‘₯,𝑑)   𝐻(π‘₯,𝑑)

Proof of Theorem stoweidlem21
Dummy variable 𝑠 is distinct from all other variables.
StepHypRef Expression
1 stoweidlem21.5 . . . 4 𝐺 = (𝑑 ∈ 𝑇 ↦ ((π»β€˜π‘‘) + 𝑆))
2 stoweidlem21.4 . . . . 5 β„²π‘‘πœ‘
3 stoweidlem21.7 . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ ℝ)
4 fvconst2g 7204 . . . . . . . 8 ((𝑆 ∈ ℝ ∧ 𝑑 ∈ 𝑇) β†’ ((𝑇 Γ— {𝑆})β€˜π‘‘) = 𝑆)
53, 4sylan 578 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((𝑇 Γ— {𝑆})β€˜π‘‘) = 𝑆)
65eqcomd 2736 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝑆 = ((𝑇 Γ— {𝑆})β€˜π‘‘))
76oveq2d 7427 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((π»β€˜π‘‘) + 𝑆) = ((π»β€˜π‘‘) + ((𝑇 Γ— {𝑆})β€˜π‘‘)))
82, 7mpteq2da 5245 . . . 4 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ ((π»β€˜π‘‘) + 𝑆)) = (𝑑 ∈ 𝑇 ↦ ((π»β€˜π‘‘) + ((𝑇 Γ— {𝑆})β€˜π‘‘))))
91, 8eqtrid 2782 . . 3 (πœ‘ β†’ 𝐺 = (𝑑 ∈ 𝑇 ↦ ((π»β€˜π‘‘) + ((𝑇 Γ— {𝑆})β€˜π‘‘))))
10 stoweidlem21.11 . . . 4 (πœ‘ β†’ 𝐻 ∈ 𝐴)
11 fconstmpt 5737 . . . . . 6 (𝑇 Γ— {𝑆}) = (𝑠 ∈ 𝑇 ↦ 𝑆)
12 stoweidlem21.3 . . . . . . 7 Ⅎ𝑑𝑆
13 nfcv 2901 . . . . . . 7 Ⅎ𝑠𝑆
14 eqidd 2731 . . . . . . 7 (𝑠 = 𝑑 β†’ 𝑆 = 𝑆)
1512, 13, 14cbvmpt 5258 . . . . . 6 (𝑠 ∈ 𝑇 ↦ 𝑆) = (𝑑 ∈ 𝑇 ↦ 𝑆)
1611, 15eqtri 2758 . . . . 5 (𝑇 Γ— {𝑆}) = (𝑑 ∈ 𝑇 ↦ 𝑆)
1712nfeq2 2918 . . . . . . . . . 10 Ⅎ𝑑 π‘₯ = 𝑆
18 simpl 481 . . . . . . . . . 10 ((π‘₯ = 𝑆 ∧ 𝑑 ∈ 𝑇) β†’ π‘₯ = 𝑆)
1917, 18mpteq2da 5245 . . . . . . . . 9 (π‘₯ = 𝑆 β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) = (𝑑 ∈ 𝑇 ↦ 𝑆))
2019eleq1d 2816 . . . . . . . 8 (π‘₯ = 𝑆 β†’ ((𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴 ↔ (𝑑 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴))
2120imbi2d 339 . . . . . . 7 (π‘₯ = 𝑆 β†’ ((πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴) ↔ (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴)))
22 stoweidlem21.9 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴)
2322expcom 412 . . . . . . 7 (π‘₯ ∈ ℝ β†’ (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ π‘₯) ∈ 𝐴))
2421, 23vtoclga 3565 . . . . . 6 (𝑆 ∈ ℝ β†’ (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴))
253, 24mpcom 38 . . . . 5 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ 𝑆) ∈ 𝐴)
2616, 25eqeltrid 2835 . . . 4 (πœ‘ β†’ (𝑇 Γ— {𝑆}) ∈ 𝐴)
27 stoweidlem21.8 . . . . 5 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
28 stoweidlem21.2 . . . . 5 Ⅎ𝑑𝐻
29 nfcv 2901 . . . . . 6 Ⅎ𝑑𝑇
3012nfsn 4710 . . . . . 6 Ⅎ𝑑{𝑆}
3129, 30nfxp 5708 . . . . 5 Ⅎ𝑑(𝑇 Γ— {𝑆})
3227, 28, 31stoweidlem8 45022 . . . 4 ((πœ‘ ∧ 𝐻 ∈ 𝐴 ∧ (𝑇 Γ— {𝑆}) ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π»β€˜π‘‘) + ((𝑇 Γ— {𝑆})β€˜π‘‘))) ∈ 𝐴)
3310, 26, 32mpd3an23 1461 . . 3 (πœ‘ β†’ (𝑑 ∈ 𝑇 ↦ ((π»β€˜π‘‘) + ((𝑇 Γ— {𝑆})β€˜π‘‘))) ∈ 𝐴)
349, 33eqeltrd 2831 . 2 (πœ‘ β†’ 𝐺 ∈ 𝐴)
35 simpr 483 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝑑 ∈ 𝑇)
36 stoweidlem21.10 . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘“ ∈ 𝐴 𝑓:π‘‡βŸΆβ„)
37 feq1 6697 . . . . . . . . . . . . 13 (𝑓 = 𝐻 β†’ (𝑓:π‘‡βŸΆβ„ ↔ 𝐻:π‘‡βŸΆβ„))
3837rspccva 3610 . . . . . . . . . . . 12 ((βˆ€π‘“ ∈ 𝐴 𝑓:π‘‡βŸΆβ„ ∧ 𝐻 ∈ 𝐴) β†’ 𝐻:π‘‡βŸΆβ„)
3936, 10, 38syl2anc 582 . . . . . . . . . . 11 (πœ‘ β†’ 𝐻:π‘‡βŸΆβ„)
4039ffvelcdmda 7085 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (π»β€˜π‘‘) ∈ ℝ)
413adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝑆 ∈ ℝ)
4240, 41readdcld 11247 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((π»β€˜π‘‘) + 𝑆) ∈ ℝ)
431fvmpt2 7008 . . . . . . . . 9 ((𝑑 ∈ 𝑇 ∧ ((π»β€˜π‘‘) + 𝑆) ∈ ℝ) β†’ (πΊβ€˜π‘‘) = ((π»β€˜π‘‘) + 𝑆))
4435, 42, 43syl2anc 582 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (πΊβ€˜π‘‘) = ((π»β€˜π‘‘) + 𝑆))
4544oveq1d 7426 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘)) = (((π»β€˜π‘‘) + 𝑆) βˆ’ (πΉβ€˜π‘‘)))
4640recnd 11246 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (π»β€˜π‘‘) ∈ β„‚)
47 stoweidlem21.6 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:π‘‡βŸΆβ„)
4847ffvelcdmda 7085 . . . . . . . . 9 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (πΉβ€˜π‘‘) ∈ ℝ)
4948recnd 11246 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
503recnd 11246 . . . . . . . . 9 (πœ‘ β†’ 𝑆 ∈ β„‚)
5150adantr 479 . . . . . . . 8 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ 𝑆 ∈ β„‚)
5246, 49, 51subsub3d 11605 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((π»β€˜π‘‘) βˆ’ ((πΉβ€˜π‘‘) βˆ’ 𝑆)) = (((π»β€˜π‘‘) + 𝑆) βˆ’ (πΉβ€˜π‘‘)))
5345, 52eqtr4d 2773 . . . . . 6 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ ((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘)) = ((π»β€˜π‘‘) βˆ’ ((πΉβ€˜π‘‘) βˆ’ 𝑆)))
5453fveq2d 6894 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (absβ€˜((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) = (absβ€˜((π»β€˜π‘‘) βˆ’ ((πΉβ€˜π‘‘) βˆ’ 𝑆))))
55 stoweidlem21.12 . . . . . 6 (πœ‘ β†’ βˆ€π‘‘ ∈ 𝑇 (absβ€˜((π»β€˜π‘‘) βˆ’ ((πΉβ€˜π‘‘) βˆ’ 𝑆))) < 𝐸)
5655r19.21bi 3246 . . . . 5 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (absβ€˜((π»β€˜π‘‘) βˆ’ ((πΉβ€˜π‘‘) βˆ’ 𝑆))) < 𝐸)
5754, 56eqbrtrd 5169 . . . 4 ((πœ‘ ∧ 𝑑 ∈ 𝑇) β†’ (absβ€˜((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸)
5857ex 411 . . 3 (πœ‘ β†’ (𝑑 ∈ 𝑇 β†’ (absβ€˜((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸))
592, 58ralrimi 3252 . 2 (πœ‘ β†’ βˆ€π‘‘ ∈ 𝑇 (absβ€˜((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸)
60 stoweidlem21.1 . . . . 5 Ⅎ𝑑𝐺
6160nfeq2 2918 . . . 4 Ⅎ𝑑 𝑓 = 𝐺
62 fveq1 6889 . . . . . . 7 (𝑓 = 𝐺 β†’ (π‘“β€˜π‘‘) = (πΊβ€˜π‘‘))
6362oveq1d 7426 . . . . . 6 (𝑓 = 𝐺 β†’ ((π‘“β€˜π‘‘) βˆ’ (πΉβ€˜π‘‘)) = ((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘)))
6463fveq2d 6894 . . . . 5 (𝑓 = 𝐺 β†’ (absβ€˜((π‘“β€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) = (absβ€˜((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))))
6564breq1d 5157 . . . 4 (𝑓 = 𝐺 β†’ ((absβ€˜((π‘“β€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸 ↔ (absβ€˜((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸))
6661, 65ralbid 3268 . . 3 (𝑓 = 𝐺 β†’ (βˆ€π‘‘ ∈ 𝑇 (absβ€˜((π‘“β€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸 ↔ βˆ€π‘‘ ∈ 𝑇 (absβ€˜((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸))
6766rspcev 3611 . 2 ((𝐺 ∈ 𝐴 ∧ βˆ€π‘‘ ∈ 𝑇 (absβ€˜((πΊβ€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸) β†’ βˆƒπ‘“ ∈ 𝐴 βˆ€π‘‘ ∈ 𝑇 (absβ€˜((π‘“β€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸)
6834, 59, 67syl2anc 582 1 (πœ‘ β†’ βˆƒπ‘“ ∈ 𝐴 βˆ€π‘‘ ∈ 𝑇 (absβ€˜((π‘“β€˜π‘‘) βˆ’ (πΉβ€˜π‘‘))) < 𝐸)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539  β„²wnf 1783   ∈ wcel 2104  β„²wnfc 2881  βˆ€wral 3059  βˆƒwrex 3068  {csn 4627   class class class wbr 5147   ↦ cmpt 5230   Γ— cxp 5673  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411  β„‚cc 11110  β„cr 11111   + caddc 11115   < clt 11252   βˆ’ cmin 11448  abscabs 15185
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-ltxr 11257  df-sub 11450
This theorem is referenced by:  stoweidlem62  45076
  Copyright terms: Public domain W3C validator