![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > hhcmpl | Structured version Visualization version GIF version |
Description: Lemma used for derivation of the completeness axiom ax-hcompl 28575 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
hhlm.1 | ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 |
hhlm.2 | ⊢ 𝐷 = (IndMet‘𝑈) |
hhlm.3 | ⊢ 𝐽 = (MetOpen‘𝐷) |
hhcmpl.c | ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥) |
Ref | Expression |
---|---|
hhcmpl | ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hhcmpl.c | . . . 4 ⊢ (𝐹 ∈ (Cau‘𝐷) → ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥) | |
2 | 1 | anim1ci 610 | . . 3 ⊢ ((𝐹 ∈ (Cau‘𝐷) ∧ 𝐹 ∈ ( ℋ ↑𝑚 ℕ)) → (𝐹 ∈ ( ℋ ↑𝑚 ℕ) ∧ ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥)) |
3 | elin 3992 | . . 3 ⊢ (𝐹 ∈ ((Cau‘𝐷) ∩ ( ℋ ↑𝑚 ℕ)) ↔ (𝐹 ∈ (Cau‘𝐷) ∧ 𝐹 ∈ ( ℋ ↑𝑚 ℕ))) | |
4 | r19.42v 3271 | . . 3 ⊢ (∃𝑥 ∈ ℋ (𝐹 ∈ ( ℋ ↑𝑚 ℕ) ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ↔ (𝐹 ∈ ( ℋ ↑𝑚 ℕ) ∧ ∃𝑥 ∈ ℋ 𝐹(⇝𝑡‘𝐽)𝑥)) | |
5 | 2, 3, 4 | 3imtr4i 284 | . 2 ⊢ (𝐹 ∈ ((Cau‘𝐷) ∩ ( ℋ ↑𝑚 ℕ)) → ∃𝑥 ∈ ℋ (𝐹 ∈ ( ℋ ↑𝑚 ℕ) ∧ 𝐹(⇝𝑡‘𝐽)𝑥)) |
6 | hhlm.1 | . . . 4 ⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 | |
7 | hhlm.2 | . . . 4 ⊢ 𝐷 = (IndMet‘𝑈) | |
8 | 6, 7 | hhcau 28571 | . . 3 ⊢ Cauchy = ((Cau‘𝐷) ∩ ( ℋ ↑𝑚 ℕ)) |
9 | 8 | eleq2i 2868 | . 2 ⊢ (𝐹 ∈ Cauchy ↔ 𝐹 ∈ ((Cau‘𝐷) ∩ ( ℋ ↑𝑚 ℕ))) |
10 | hhlm.3 | . . . . . 6 ⊢ 𝐽 = (MetOpen‘𝐷) | |
11 | 6, 7, 10 | hhlm 28572 | . . . . 5 ⊢ ⇝𝑣 = ((⇝𝑡‘𝐽) ↾ ( ℋ ↑𝑚 ℕ)) |
12 | 11 | breqi 4847 | . . . 4 ⊢ (𝐹 ⇝𝑣 𝑥 ↔ 𝐹((⇝𝑡‘𝐽) ↾ ( ℋ ↑𝑚 ℕ))𝑥) |
13 | vex 3386 | . . . . 5 ⊢ 𝑥 ∈ V | |
14 | 13 | brresi 5607 | . . . 4 ⊢ (𝐹((⇝𝑡‘𝐽) ↾ ( ℋ ↑𝑚 ℕ))𝑥 ↔ (𝐹 ∈ ( ℋ ↑𝑚 ℕ) ∧ 𝐹(⇝𝑡‘𝐽)𝑥)) |
15 | 12, 14 | bitri 267 | . . 3 ⊢ (𝐹 ⇝𝑣 𝑥 ↔ (𝐹 ∈ ( ℋ ↑𝑚 ℕ) ∧ 𝐹(⇝𝑡‘𝐽)𝑥)) |
16 | 15 | rexbii 3220 | . 2 ⊢ (∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 ↔ ∃𝑥 ∈ ℋ (𝐹 ∈ ( ℋ ↑𝑚 ℕ) ∧ 𝐹(⇝𝑡‘𝐽)𝑥)) |
17 | 5, 9, 16 | 3imtr4i 284 | 1 ⊢ (𝐹 ∈ Cauchy → ∃𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ∃wrex 3088 ∩ cin 3766 〈cop 4372 class class class wbr 4841 ↾ cres 5312 ‘cfv 6099 (class class class)co 6876 ↑𝑚 cmap 8093 ℕcn 11310 MetOpencmopn 20054 ⇝𝑡clm 21355 Cauccau 23375 IndMetcims 27962 ℋchba 28292 +ℎ cva 28293 ·ℎ csm 28294 normℎcno 28296 Cauchyccauold 28299 ⇝𝑣 chli 28300 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2375 ax-ext 2775 ax-rep 4962 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 ax-un 7181 ax-cnex 10278 ax-resscn 10279 ax-1cn 10280 ax-icn 10281 ax-addcl 10282 ax-addrcl 10283 ax-mulcl 10284 ax-mulrcl 10285 ax-mulcom 10286 ax-addass 10287 ax-mulass 10288 ax-distr 10289 ax-i2m1 10290 ax-1ne0 10291 ax-1rid 10292 ax-rnegex 10293 ax-rrecex 10294 ax-cnre 10295 ax-pre-lttri 10296 ax-pre-lttrn 10297 ax-pre-ltadd 10298 ax-pre-mulgt0 10299 ax-pre-sup 10300 ax-addf 10301 ax-mulf 10302 ax-hilex 28372 ax-hfvadd 28373 ax-hvcom 28374 ax-hvass 28375 ax-hv0cl 28376 ax-hvaddid 28377 ax-hfvmul 28378 ax-hvmulid 28379 ax-hvmulass 28380 ax-hvdistr1 28381 ax-hvdistr2 28382 ax-hvmul0 28383 ax-hfi 28452 ax-his1 28455 ax-his2 28456 ax-his3 28457 ax-his4 28458 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-nel 3073 df-ral 3092 df-rex 3093 df-reu 3094 df-rmo 3095 df-rab 3096 df-v 3385 df-sbc 3632 df-csb 3727 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-pss 3783 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-tp 4371 df-op 4373 df-uni 4627 df-iun 4710 df-br 4842 df-opab 4904 df-mpt 4921 df-tr 4944 df-id 5218 df-eprel 5223 df-po 5231 df-so 5232 df-fr 5269 df-we 5271 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-pred 5896 df-ord 5942 df-on 5943 df-lim 5944 df-suc 5945 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-f1 6104 df-fo 6105 df-f1o 6106 df-fv 6107 df-riota 6837 df-ov 6879 df-oprab 6880 df-mpt2 6881 df-om 7298 df-1st 7399 df-2nd 7400 df-wrecs 7643 df-recs 7705 df-rdg 7743 df-er 7980 df-map 8095 df-pm 8096 df-en 8194 df-dom 8195 df-sdom 8196 df-sup 8588 df-inf 8589 df-pnf 10363 df-mnf 10364 df-xr 10365 df-ltxr 10366 df-le 10367 df-sub 10556 df-neg 10557 df-div 10975 df-nn 11311 df-2 11372 df-3 11373 df-4 11374 df-n0 11577 df-z 11663 df-uz 11927 df-q 12030 df-rp 12071 df-xneg 12189 df-xadd 12190 df-xmul 12191 df-seq 13052 df-exp 13111 df-cj 14176 df-re 14177 df-im 14178 df-sqrt 14312 df-abs 14313 df-topgen 16415 df-psmet 20056 df-xmet 20057 df-met 20058 df-bl 20059 df-mopn 20060 df-top 21023 df-topon 21040 df-bases 21075 df-lm 21358 df-cau 23378 df-grpo 27864 df-gid 27865 df-ginv 27866 df-gdiv 27867 df-ablo 27916 df-vc 27930 df-nv 27963 df-va 27966 df-ba 27967 df-sm 27968 df-0v 27969 df-vs 27970 df-nmcv 27971 df-ims 27972 df-hnorm 28341 df-hvsub 28344 df-hlim 28345 df-hcau 28346 |
This theorem is referenced by: hilcompl 28574 |
Copyright terms: Public domain | W3C validator |