Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ipasslem8 | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
ip1i.1 | ⊢ 𝑋 = (BaseSet‘𝑈) |
ip1i.2 | ⊢ 𝐺 = ( +𝑣 ‘𝑈) |
ip1i.4 | ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) |
ip1i.7 | ⊢ 𝑃 = (·𝑖OLD‘𝑈) |
ip1i.9 | ⊢ 𝑈 ∈ CPreHilOLD |
ipasslem7.a | ⊢ 𝐴 ∈ 𝑋 |
ipasslem7.b | ⊢ 𝐵 ∈ 𝑋 |
ipasslem7.f | ⊢ 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)))) |
Ref | Expression |
---|---|
ipasslem8 | ⊢ 𝐹:ℝ⟶{0} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0cn 10855 | . 2 ⊢ 0 ∈ ℂ | |
2 | qre 12579 | . . . . . 6 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℝ) | |
3 | oveq1 7242 | . . . . . . . . 9 ⊢ (𝑤 = 𝑥 → (𝑤𝑆𝐴) = (𝑥𝑆𝐴)) | |
4 | 3 | oveq1d 7250 | . . . . . . . 8 ⊢ (𝑤 = 𝑥 → ((𝑤𝑆𝐴)𝑃𝐵) = ((𝑥𝑆𝐴)𝑃𝐵)) |
5 | oveq1 7242 | . . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝑤 · (𝐴𝑃𝐵)) = (𝑥 · (𝐴𝑃𝐵))) | |
6 | 4, 5 | oveq12d 7253 | . . . . . . 7 ⊢ (𝑤 = 𝑥 → (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))) = (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵)))) |
7 | ipasslem7.f | . . . . . . 7 ⊢ 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)))) | |
8 | ovex 7268 | . . . . . . 7 ⊢ (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵))) ∈ V | |
9 | 6, 7, 8 | fvmpt 6840 | . . . . . 6 ⊢ (𝑥 ∈ ℝ → (𝐹‘𝑥) = (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵)))) |
10 | 2, 9 | syl 17 | . . . . 5 ⊢ (𝑥 ∈ ℚ → (𝐹‘𝑥) = (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵)))) |
11 | ipasslem7.a | . . . . . 6 ⊢ 𝐴 ∈ 𝑋 | |
12 | qcn 12589 | . . . . . . . . 9 ⊢ (𝑥 ∈ ℚ → 𝑥 ∈ ℂ) | |
13 | ip1i.9 | . . . . . . . . . . 11 ⊢ 𝑈 ∈ CPreHilOLD | |
14 | 13 | phnvi 28929 | . . . . . . . . . 10 ⊢ 𝑈 ∈ NrmCVec |
15 | ip1i.1 | . . . . . . . . . . 11 ⊢ 𝑋 = (BaseSet‘𝑈) | |
16 | ip1i.4 | . . . . . . . . . . 11 ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) | |
17 | 15, 16 | nvscl 28739 | . . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (𝑥𝑆𝐴) ∈ 𝑋) |
18 | 14, 17 | mp3an1 1450 | . . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 𝐴 ∈ 𝑋) → (𝑥𝑆𝐴) ∈ 𝑋) |
19 | 12, 18 | sylan 583 | . . . . . . . 8 ⊢ ((𝑥 ∈ ℚ ∧ 𝐴 ∈ 𝑋) → (𝑥𝑆𝐴) ∈ 𝑋) |
20 | ipasslem7.b | . . . . . . . . 9 ⊢ 𝐵 ∈ 𝑋 | |
21 | ip1i.7 | . . . . . . . . . 10 ⊢ 𝑃 = (·𝑖OLD‘𝑈) | |
22 | 15, 21 | dipcl 28825 | . . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝑥𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑥𝑆𝐴)𝑃𝐵) ∈ ℂ) |
23 | 14, 20, 22 | mp3an13 1454 | . . . . . . . 8 ⊢ ((𝑥𝑆𝐴) ∈ 𝑋 → ((𝑥𝑆𝐴)𝑃𝐵) ∈ ℂ) |
24 | 19, 23 | syl 17 | . . . . . . 7 ⊢ ((𝑥 ∈ ℚ ∧ 𝐴 ∈ 𝑋) → ((𝑥𝑆𝐴)𝑃𝐵) ∈ ℂ) |
25 | ip1i.2 | . . . . . . . 8 ⊢ 𝐺 = ( +𝑣 ‘𝑈) | |
26 | 15, 25, 16, 21, 13, 20 | ipasslem5 28948 | . . . . . . 7 ⊢ ((𝑥 ∈ ℚ ∧ 𝐴 ∈ 𝑋) → ((𝑥𝑆𝐴)𝑃𝐵) = (𝑥 · (𝐴𝑃𝐵))) |
27 | 24, 26 | subeq0bd 11288 | . . . . . 6 ⊢ ((𝑥 ∈ ℚ ∧ 𝐴 ∈ 𝑋) → (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵))) = 0) |
28 | 11, 27 | mpan2 691 | . . . . 5 ⊢ (𝑥 ∈ ℚ → (((𝑥𝑆𝐴)𝑃𝐵) − (𝑥 · (𝐴𝑃𝐵))) = 0) |
29 | 10, 28 | eqtrd 2779 | . . . 4 ⊢ (𝑥 ∈ ℚ → (𝐹‘𝑥) = 0) |
30 | 29 | rgen 3074 | . . 3 ⊢ ∀𝑥 ∈ ℚ (𝐹‘𝑥) = 0 |
31 | 7 | funmpt2 6440 | . . . 4 ⊢ Fun 𝐹 |
32 | qssre 12585 | . . . . 5 ⊢ ℚ ⊆ ℝ | |
33 | ovex 7268 | . . . . . 6 ⊢ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵))) ∈ V | |
34 | 33, 7 | dmmpti 6544 | . . . . 5 ⊢ dom 𝐹 = ℝ |
35 | 32, 34 | sseqtrri 3955 | . . . 4 ⊢ ℚ ⊆ dom 𝐹 |
36 | funconstss 6898 | . . . 4 ⊢ ((Fun 𝐹 ∧ ℚ ⊆ dom 𝐹) → (∀𝑥 ∈ ℚ (𝐹‘𝑥) = 0 ↔ ℚ ⊆ (◡𝐹 “ {0}))) | |
37 | 31, 35, 36 | mp2an 692 | . . 3 ⊢ (∀𝑥 ∈ ℚ (𝐹‘𝑥) = 0 ↔ ℚ ⊆ (◡𝐹 “ {0})) |
38 | 30, 37 | mpbi 233 | . 2 ⊢ ℚ ⊆ (◡𝐹 “ {0}) |
39 | qdensere 23699 | . 2 ⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ | |
40 | eqid 2739 | . . . . 5 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld) | |
41 | 40 | cnfldhaus 23714 | . . . 4 ⊢ (TopOpen‘ℂfld) ∈ Haus |
42 | haust1 22281 | . . . 4 ⊢ ((TopOpen‘ℂfld) ∈ Haus → (TopOpen‘ℂfld) ∈ Fre) | |
43 | 41, 42 | ax-mp 5 | . . 3 ⊢ (TopOpen‘ℂfld) ∈ Fre |
44 | eqid 2739 | . . . 4 ⊢ (topGen‘ran (,)) = (topGen‘ran (,)) | |
45 | 15, 25, 16, 21, 13, 11, 20, 7, 44, 40 | ipasslem7 28949 | . . 3 ⊢ 𝐹 ∈ ((topGen‘ran (,)) Cn (TopOpen‘ℂfld)) |
46 | uniretop 23692 | . . . 4 ⊢ ℝ = ∪ (topGen‘ran (,)) | |
47 | 40 | cnfldtopon 23712 | . . . . 5 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ) |
48 | 47 | toponunii 21845 | . . . 4 ⊢ ℂ = ∪ (TopOpen‘ℂfld) |
49 | 46, 48 | dnsconst 22307 | . . 3 ⊢ ((((TopOpen‘ℂfld) ∈ Fre ∧ 𝐹 ∈ ((topGen‘ran (,)) Cn (TopOpen‘ℂfld))) ∧ (0 ∈ ℂ ∧ ℚ ⊆ (◡𝐹 “ {0}) ∧ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ)) → 𝐹:ℝ⟶{0}) |
50 | 43, 45, 49 | mpanl12 702 | . 2 ⊢ ((0 ∈ ℂ ∧ ℚ ⊆ (◡𝐹 “ {0}) ∧ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ) → 𝐹:ℝ⟶{0}) |
51 | 1, 38, 39, 50 | mp3an 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 |