MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ipasslem8 Structured version   Visualization version   GIF version

Theorem ipasslem8 28950
Description: Lemma for ipassi 28954. By ipasslem5 28948, 𝐹 is 0 for all ; since it is continuous and is dense in by qdensere2 23726, we conclude 𝐹 is 0 for all . (Contributed by NM, 24-Aug-2007.) (Revised by Mario Carneiro, 6-May-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
ip1i.1 𝑋 = (BaseSet‘𝑈)
ip1i.2 𝐺 = ( +𝑣𝑈)
ip1i.4 𝑆 = ( ·𝑠OLD𝑈)
ip1i.7 𝑃 = (·𝑖OLD𝑈)
ip1i.9 𝑈 ∈ CPreHilOLD
ipasslem7.a 𝐴𝑋
ipasslem7.b 𝐵𝑋
ipasslem7.f 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))))
Assertion
Ref Expression
ipasslem8 𝐹:ℝ⟶{0}
Distinct variable groups:   𝑤,𝐵   𝑤,𝑃   𝑤,𝑆   𝑤,𝑈   𝑤,𝑋   𝑤,𝐴
Allowed substitution hints:   𝐹(𝑤)   𝐺(𝑤)

Proof of Theorem ipasslem8
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 0cn 10855 . 2 0 ∈ ℂ
2 qre 12579 . . . . . 6 (𝑥 ∈ ℚ → 𝑥 ∈ ℝ)
3 oveq1 7242 . . . . . . . . 9 (𝑤 = 𝑥 → (𝑤𝑆𝐴) = (𝑥𝑆𝐴))
43oveq1d 7250 . . . . . . . 8 (𝑤 = 𝑥 → ((𝑤𝑆𝐴)𝑃𝐵) = ((𝑥𝑆𝐴)𝑃𝐵))
5 oveq1 7242 . . . . . . . 8 (𝑤 = 𝑥 → (𝑤 · (𝐴𝑃𝐵)) = (𝑥 · (𝐴𝑃𝐵)))
64, 5oveq12d 7253 . . . . . . 7 (𝑤 = 𝑥 → (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))) = (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵))))
7 ipasslem7.f . . . . . . 7 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))))
8 ovex 7268 . . . . . . 7 (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵))) ∈ V
96, 7, 8fvmpt 6840 . . . . . 6 (𝑥 ∈ ℝ → (𝐹𝑥) = (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵))))
102, 9syl 17 . . . . 5 (𝑥 ∈ ℚ → (𝐹𝑥) = (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵))))
11 ipasslem7.a . . . . . 6 𝐴𝑋
12 qcn 12589 . . . . . . . . 9 (𝑥 ∈ ℚ → 𝑥 ∈ ℂ)
13 ip1i.9 . . . . . . . . . . 11 𝑈 ∈ CPreHilOLD
1413phnvi 28929 . . . . . . . . . 10 𝑈 ∈ NrmCVec
15 ip1i.1 . . . . . . . . . . 11 𝑋 = (BaseSet‘𝑈)
16 ip1i.4 . . . . . . . . . . 11 𝑆 = ( ·𝑠OLD𝑈)
1715, 16nvscl 28739 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝐴𝑋) → (𝑥𝑆𝐴) ∈ 𝑋)
1814, 17mp3an1 1450 . . . . . . . . 9 ((𝑥 ∈ ℂ ∧ 𝐴𝑋) → (𝑥𝑆𝐴) ∈ 𝑋)
1912, 18sylan 583 . . . . . . . 8 ((𝑥 ∈ ℚ ∧ 𝐴𝑋) → (𝑥𝑆𝐴) ∈ 𝑋)
20 ipasslem7.b . . . . . . . . 9 𝐵𝑋
21 ip1i.7 . . . . . . . . . 10 𝑃 = (·𝑖OLD𝑈)
2215, 21dipcl 28825 . . . . . . . . 9 ((𝑈 ∈ NrmCVec ∧ (𝑥𝑆𝐴) ∈ 𝑋𝐵𝑋) → ((𝑥𝑆𝐴)𝑃𝐵) ∈ ℂ)
2314, 20, 22mp3an13 1454 . . . . . . . 8 ((𝑥𝑆𝐴) ∈ 𝑋 → ((𝑥𝑆𝐴)𝑃𝐵) ∈ ℂ)
2419, 23syl 17 . . . . . . 7 ((𝑥 ∈ ℚ ∧ 𝐴𝑋) → ((𝑥𝑆𝐴)𝑃𝐵) ∈ ℂ)
25 ip1i.2 . . . . . . . 8 𝐺 = ( +𝑣𝑈)
2615, 25, 16, 21, 13, 20ipasslem5 28948 . . . . . . 7 ((𝑥 ∈ ℚ ∧ 𝐴𝑋) → ((𝑥𝑆𝐴)𝑃𝐵) = (𝑥 · (𝐴𝑃𝐵)))
2724, 26subeq0bd 11288 . . . . . 6 ((𝑥 ∈ ℚ ∧ 𝐴𝑋) → (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵))) = 0)
2811, 27mpan2 691 . . . . 5 (𝑥 ∈ ℚ → (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵))) = 0)
2910, 28eqtrd 2779 . . . 4 (𝑥 ∈ ℚ → (𝐹𝑥) = 0)
3029rgen 3074 . . 3 𝑥 ∈ ℚ (𝐹𝑥) = 0
317funmpt2 6440 . . . 4 Fun 𝐹
32 qssre 12585 . . . . 5 ℚ ⊆ ℝ
33 ovex 7268 . . . . . 6 (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))) ∈ V
3433, 7dmmpti 6544 . . . . 5 dom 𝐹 = ℝ
3532, 34sseqtrri 3955 . . . 4 ℚ ⊆ dom 𝐹
36 funconstss 6898 . . . 4 ((Fun 𝐹 ∧ ℚ ⊆ dom 𝐹) → (∀𝑥 ∈ ℚ (𝐹𝑥) = 0 ↔ ℚ ⊆ (𝐹 “ {0})))
3731, 35, 36mp2an 692 . . 3 (∀𝑥 ∈ ℚ (𝐹𝑥) = 0 ↔ ℚ ⊆ (𝐹 “ {0}))
3830, 37mpbi 233 . 2 ℚ ⊆ (𝐹 “ {0})
39 qdensere 23699 . 2 ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ
40 eqid 2739 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4140cnfldhaus 23714 . . . 4 (TopOpen‘ℂfld) ∈ Haus
42 haust1 22281 . . . 4 ((TopOpen‘ℂfld) ∈ Haus → (TopOpen‘ℂfld) ∈ Fre)
4341, 42ax-mp 5 . . 3 (TopOpen‘ℂfld) ∈ Fre
44 eqid 2739 . . . 4 (topGen‘ran (,)) = (topGen‘ran (,))
4515, 25, 16, 21, 13, 11, 20, 7, 44, 40ipasslem7 28949 . . 3 𝐹 ∈ ((topGen‘ran (,)) Cn (TopOpen‘ℂfld))
46 uniretop 23692 . . . 4 ℝ = (topGen‘ran (,))
4740cnfldtopon 23712 . . . . 5 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
4847toponunii 21845 . . . 4 ℂ = (TopOpen‘ℂfld)
4946, 48dnsconst 22307 . . 3 ((((TopOpen‘ℂfld) ∈ Fre ∧ 𝐹 ∈ ((topGen‘ran (,)) Cn (TopOpen‘ℂfld))) ∧ (0 ∈ ℂ ∧ ℚ ⊆ (𝐹 “ {0}) ∧ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ)) → 𝐹:ℝ⟶{0})
5043, 45, 49mpanl12 702 . 2 ((0 ∈ ℂ ∧ ℚ ⊆ (𝐹 “ {0}) ∧ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ) → 𝐹:ℝ⟶{0})
511, 38, 39, 50mp3an 1463 1 𝐹:ℝ⟶{0}
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  w3a 1089   = wceq 1543  wcel 2112  wral 3064  wss 3883  {csn 4558  cmpt 5152  ccnv 5568  dom cdm 5569  ran crn 5570  cima 5572  Fun wfun 6395  wf 6397  cfv 6401  (class class class)co 7235  cc 10757  cr 10758  0cc0 10759   · cmul 10764  cmin 11092  cq 12574  (,)cioo 12965  TopOpenctopn 16959  topGenctg 16975  fldccnfld 20396  clsccl 21947   Cn ccn 22153  Frect1 22236  Hauscha 22237  NrmCVeccnv 28697   +𝑣 cpv 28698  BaseSetcba 28699   ·𝑠OLD cns 28700  ·𝑖OLDcdip 28813  CPreHilOLDccphlo 28925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5196  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545  ax-inf2 9286  ax-cnex 10815  ax-resscn 10816  ax-1cn 10817  ax-icn 10818  ax-addcl 10819  ax-addrcl 10820  ax-mulcl 10821  ax-mulrcl 10822  ax-mulcom 10823  ax-addass 10824  ax-mulass 10825  ax-distr 10826  ax-i2m1 10827  ax-1ne0 10828  ax-1rid 10829  ax-rnegex 10830  ax-rrecex 10831  ax-cnre 10832  ax-pre-lttri 10833  ax-pre-lttrn 10834  ax-pre-ltadd 10835  ax-pre-mulgt0 10836  ax-pre-sup 10837  ax-addf 10838  ax-mulf 10839
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-se 5528  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-pred 6179  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-isom 6410  df-riota 7192  df-ov 7238  df-oprab 7239  df-mpo 7240  df-of 7491  df-om 7667  df-1st 7783  df-2nd 7784  df-supp 7928  df-wrecs 8071  df-recs 8132  df-rdg 8170  df-1o 8226  df-2o 8227  df-er 8415  df-map 8534  df-ixp 8603  df-en 8651  df-dom 8652  df-sdom 8653  df-fin 8654  df-fsupp 9016  df-fi 9057  df-sup 9088  df-inf 9089  df-oi 9156  df-card 9585  df-pnf 10899  df-mnf 10900  df-xr 10901  df-ltxr 10902  df-le 10903  df-sub 11094  df-neg 11095  df-div 11520  df-nn 11861  df-2 11923  df-3 11924  df-4 11925  df-5 11926  df-6 11927  df-7 11928  df-8 11929  df-9 11930  df-n0 12121  df-z 12207  df-dec 12324  df-uz 12469  df-q 12575  df-rp 12617  df-xneg 12734  df-xadd 12735  df-xmul 12736  df-ioo 12969  df-icc 12972  df-fz 13126  df-fzo 13269  df-seq 13607  df-exp 13668  df-hash 13930  df-cj 14695  df-re 14696  df-im 14697  df-sqrt 14831  df-abs 14832  df-clim 15082  df-sum 15283  df-struct 16733  df-sets 16750  df-slot 16768  df-ndx 16778  df-base 16794  df-ress 16818  df-plusg 16848  df-mulr 16849  df-starv 16850  df-sca 16851  df-vsca 16852  df-ip 16853  df-tset 16854  df-ple 16855  df-ds 16857  df-unif 16858  df-hom 16859  df-cco 16860  df-rest 16960  df-topn 16961  df-0g 16979  df-gsum 16980  df-topgen 16981  df-pt 16982  df-prds 16985  df-xrs 17040  df-qtop 17045  df-imas 17046  df-xps 17048  df-mre 17122  df-mrc 17123  df-acs 17125  df-mgm 18147  df-sgrp 18196  df-mnd 18207  df-submnd 18252  df-mulg 18522  df-cntz 18744  df-cmn 19205  df-psmet 20388  df-xmet 20389  df-met 20390  df-bl 20391  df-mopn 20392  df-cnfld 20397  df-top 21823  df-topon 21840  df-topsp 21862  df-bases 21875  df-cld 21948  df-ntr 21949  df-cls 21950  df-cn 22156  df-cnp 22157  df-t1 22243  df-haus 22244  df-tx 22491  df-hmeo 22684  df-xms 23250  df-ms 23251  df-tms 23252  df-grpo 28606  df-gid 28607  df-ginv 28608  df-gdiv 28609  df-ablo 28658  df-vc 28672  df-nv 28705  df-va 28708  df-ba 28709  df-sm 28710  df-0v 28711  df-vs 28712  df-nmcv 28713  df-ims 28714  df-dip 28814  df-ph 28926
This theorem is referenced by:  ipasslem9  28951
  Copyright terms: Public domain W3C validator