Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > choccl | Structured version Visualization version GIF version |
Description: Closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
Ref | Expression |
---|---|
choccl | ⊢ (𝐴 ∈ Cℋ → (⊥‘𝐴) ∈ Cℋ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chsh 29573 | . 2 ⊢ (𝐴 ∈ Cℋ → 𝐴 ∈ Sℋ ) | |
2 | shoccl 29654 | . 2 ⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ∈ Cℋ ) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐴 ∈ Cℋ → (⊥‘𝐴) ∈ Cℋ ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ‘cfv 6428 Sℋ csh 29277 Cℋ cch 29278 ⊥cort 29279 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5210 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7580 ax-inf2 9388 ax-cnex 10916 ax-resscn 10917 ax-1cn 10918 ax-icn 10919 ax-addcl 10920 ax-addrcl 10921 ax-mulcl 10922 ax-mulrcl 10923 ax-mulcom 10924 ax-addass 10925 ax-mulass 10926 ax-distr 10927 ax-i2m1 10928 ax-1ne0 10929 ax-1rid 10930 ax-rnegex 10931 ax-rrecex 10932 ax-cnre 10933 ax-pre-lttri 10934 ax-pre-lttrn 10935 ax-pre-ltadd 10936 ax-pre-mulgt0 10937 ax-pre-sup 10938 ax-addf 10939 ax-mulf 10940 ax-hilex 29348 ax-hfvadd 29349 ax-hvcom 29350 ax-hvass 29351 ax-hv0cl 29352 ax-hvaddid 29353 ax-hfvmul 29354 ax-hvmulid 29355 ax-hvmulass 29356 ax-hvdistr1 29357 ax-hvdistr2 29358 ax-hvmul0 29359 ax-hfi 29428 ax-his1 29431 ax-his2 29432 ax-his3 29433 ax-his4 29434 ax-hcompl 29551 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3433 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4259 df-if 4462 df-pw 4537 df-sn 4564 df-pr 4566 df-tp 4568 df-op 4570 df-uni 4842 df-int 4882 df-iun 4928 df-iin 4929 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5486 df-eprel 5492 df-po 5500 df-so 5501 df-fr 5541 df-se 5542 df-we 5543 df-xp 5592 df-rel 5593 df-cnv 5594 df-co 5595 df-dm 5596 df-rn 5597 df-res 5598 df-ima 5599 df-pred 6197 df-ord 6264 df-on 6265 df-lim 6266 df-suc 6267 df-iota 6386 df-fun 6430 df-fn 6431 df-f 6432 df-f1 6433 df-fo 6434 df-f1o 6435 df-fv 6436 df-isom 6437 df-riota 7226 df-ov 7272 df-oprab 7273 df-mpo 7274 df-of 7525 df-om 7705 df-1st 7822 df-2nd 7823 df-supp 7967 df-frecs 8086 df-wrecs 8117 df-recs 8191 df-rdg 8230 df-1o 8286 df-2o 8287 df-er 8487 df-map 8606 df-pm 8607 df-ixp 8675 df-en 8723 df-dom 8724 df-sdom 8725 df-fin 8726 df-fsupp 9118 df-fi 9159 df-sup 9190 df-inf 9191 df-oi 9258 df-card 9686 df-pnf 11000 df-mnf 11001 df-xr 11002 df-ltxr 11003 df-le 11004 df-sub 11196 df-neg 11197 df-div 11622 df-nn 11963 df-2 12025 df-3 12026 df-4 12027 df-5 12028 df-6 12029 df-7 12030 df-8 12031 df-9 12032 df-n0 12223 df-z 12309 df-dec 12427 df-uz 12572 df-q 12678 df-rp 12720 df-xneg 12837 df-xadd 12838 df-xmul 12839 df-ioo 13072 df-icc 13075 df-fz 13229 df-fzo 13372 df-seq 13711 df-exp 13772 df-hash 14034 df-cj 14799 df-re 14800 df-im 14801 df-sqrt 14935 df-abs 14936 df-clim 15186 df-sum 15387 df-struct 16837 df-sets 16854 df-slot 16872 df-ndx 16884 df-base 16902 df-ress 16931 df-plusg 16964 df-mulr 16965 df-starv 16966 df-sca 16967 df-vsca 16968 df-ip 16969 df-tset 16970 df-ple 16971 df-ds 16973 df-unif 16974 df-hom 16975 df-cco 16976 df-rest 17122 df-topn 17123 df-0g 17141 df-gsum 17142 df-topgen 17143 df-pt 17144 df-prds 17147 df-xrs 17202 df-qtop 17207 df-imas 17208 df-xps 17210 df-mre 17284 df-mrc 17285 df-acs 17287 df-mgm 18315 df-sgrp 18364 df-mnd 18375 df-submnd 18420 df-mulg 18690 df-cntz 18912 df-cmn 19377 df-psmet 20578 df-xmet 20579 df-met 20580 df-bl 20581 df-mopn 20582 df-cnfld 20587 df-top 22032 df-topon 22049 df-topsp 22071 df-bases 22085 df-cn 22367 df-cnp 22368 df-lm 22369 df-haus 22455 df-tx 22702 df-hmeo 22895 df-xms 23462 df-ms 23463 df-tms 23464 df-cau 24409 df-grpo 28842 df-gid 28843 df-ginv 28844 df-gdiv 28845 df-ablo 28894 df-vc 28908 df-nv 28941 df-va 28944 df-ba 28945 df-sm 28946 df-0v 28947 df-vs 28948 df-nmcv 28949 df-ims 28950 df-dip 29050 df-hnorm 29317 df-hvsub 29320 df-hlim 29321 df-hcau 29322 df-sh 29556 df-ch 29570 df-oc 29601 |
This theorem is referenced by: choccli 29656 pjhtheu2 29765 pjpjpre 29768 pjpjhth 29774 pjop 29776 pjpo 29777 pjoccl 29782 chssoc 29845 chsscon1 29850 chpsscon1 29853 chpsscon2 29854 chdmm2 29875 chdmm3 29876 chdmm4 29877 chdmj1 29878 chdmj2 29879 chdmj3 29880 chdmj4 29881 spansnch 29909 pjspansn 29926 cmcm2 29965 fh1 29967 fh2 29968 cm2j 29969 pjorthi 30018 pjo 30020 pjocvec 30046 hstoc 30571 hstnmoc 30572 hstle1 30575 hst1h 30576 hstle 30579 hstoh 30581 cvcon3 30633 dmdmd 30649 mddmd 30650 ssdmd1 30662 ssdmd2 30663 cvdmd 30686 h1da 30698 atom1d 30702 chirredlem1 30739 chirredlem2 30740 dmdsym 30762 |
Copyright terms: Public domain | W3C validator |