![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > choccli | Structured version Visualization version GIF version |
Description: Closure of Cℋ orthocomplement. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
choccl.1 | ⊢ 𝐴 ∈ Cℋ |
Ref | Expression |
---|---|
choccli | ⊢ (⊥‘𝐴) ∈ Cℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | choccl.1 | . 2 ⊢ 𝐴 ∈ Cℋ | |
2 | choccl 31329 | . 2 ⊢ (𝐴 ∈ Cℋ → (⊥‘𝐴) ∈ Cℋ ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (⊥‘𝐴) ∈ Cℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2103 ‘cfv 6572 Cℋ cch 30952 ⊥cort 30953 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-10 2136 ax-11 2153 ax-12 2173 ax-ext 2705 ax-rep 5306 ax-sep 5320 ax-nul 5327 ax-pow 5386 ax-pr 5450 ax-un 7766 ax-inf2 9706 ax-cnex 11236 ax-resscn 11237 ax-1cn 11238 ax-icn 11239 ax-addcl 11240 ax-addrcl 11241 ax-mulcl 11242 ax-mulrcl 11243 ax-mulcom 11244 ax-addass 11245 ax-mulass 11246 ax-distr 11247 ax-i2m1 11248 ax-1ne0 11249 ax-1rid 11250 ax-rnegex 11251 ax-rrecex 11252 ax-cnre 11253 ax-pre-lttri 11254 ax-pre-lttrn 11255 ax-pre-ltadd 11256 ax-pre-mulgt0 11257 ax-pre-sup 11258 ax-addf 11259 ax-mulf 11260 ax-hilex 31022 ax-hfvadd 31023 ax-hvcom 31024 ax-hvass 31025 ax-hv0cl 31026 ax-hvaddid 31027 ax-hfvmul 31028 ax-hvmulid 31029 ax-hvmulass 31030 ax-hvdistr1 31031 ax-hvdistr2 31032 ax-hvmul0 31033 ax-hfi 31102 ax-his1 31105 ax-his2 31106 ax-his3 31107 ax-his4 31108 ax-hcompl 31225 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2890 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-rmo 3383 df-reu 3384 df-rab 3439 df-v 3484 df-sbc 3799 df-csb 3916 df-dif 3973 df-un 3975 df-in 3977 df-ss 3987 df-pss 3990 df-nul 4348 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4973 df-iun 5021 df-iin 5022 df-br 5170 df-opab 5232 df-mpt 5253 df-tr 5287 df-id 5597 df-eprel 5603 df-po 5611 df-so 5612 df-fr 5654 df-se 5655 df-we 5656 df-xp 5705 df-rel 5706 df-cnv 5707 df-co 5708 df-dm 5709 df-rn 5710 df-res 5711 df-ima 5712 df-pred 6331 df-ord 6397 df-on 6398 df-lim 6399 df-suc 6400 df-iota 6524 df-fun 6574 df-fn 6575 df-f 6576 df-f1 6577 df-fo 6578 df-f1o 6579 df-fv 6580 df-isom 6581 df-riota 7401 df-ov 7448 df-oprab 7449 df-mpo 7450 df-of 7710 df-om 7900 df-1st 8026 df-2nd 8027 df-supp 8198 df-frecs 8318 df-wrecs 8349 df-recs 8423 df-rdg 8462 df-1o 8518 df-2o 8519 df-er 8759 df-map 8882 df-pm 8883 df-ixp 8952 df-en 9000 df-dom 9001 df-sdom 9002 df-fin 9003 df-fsupp 9428 df-fi 9476 df-sup 9507 df-inf 9508 df-oi 9575 df-card 10004 df-pnf 11322 df-mnf 11323 df-xr 11324 df-ltxr 11325 df-le 11326 df-sub 11518 df-neg 11519 df-div 11944 df-nn 12290 df-2 12352 df-3 12353 df-4 12354 df-5 12355 df-6 12356 df-7 12357 df-8 12358 df-9 12359 df-n0 12550 df-z 12636 df-dec 12755 df-uz 12900 df-q 13010 df-rp 13054 df-xneg 13171 df-xadd 13172 df-xmul 13173 df-ioo 13407 df-icc 13410 df-fz 13564 df-fzo 13708 df-seq 14049 df-exp 14109 df-hash 14376 df-cj 15144 df-re 15145 df-im 15146 df-sqrt 15280 df-abs 15281 df-clim 15530 df-sum 15731 df-struct 17189 df-sets 17206 df-slot 17224 df-ndx 17236 df-base 17254 df-ress 17283 df-plusg 17319 df-mulr 17320 df-starv 17321 df-sca 17322 df-vsca 17323 df-ip 17324 df-tset 17325 df-ple 17326 df-ds 17328 df-unif 17329 df-hom 17330 df-cco 17331 df-rest 17477 df-topn 17478 df-0g 17496 df-gsum 17497 df-topgen 17498 df-pt 17499 df-prds 17502 df-xrs 17557 df-qtop 17562 df-imas 17563 df-xps 17565 df-mre 17639 df-mrc 17640 df-acs 17642 df-mgm 18673 df-sgrp 18752 df-mnd 18768 df-submnd 18814 df-mulg 19103 df-cntz 19352 df-cmn 19819 df-psmet 21374 df-xmet 21375 df-met 21376 df-bl 21377 df-mopn 21378 df-cnfld 21383 df-top 22914 df-topon 22931 df-topsp 22953 df-bases 22967 df-cn 23249 df-cnp 23250 df-lm 23251 df-haus 23337 df-tx 23584 df-hmeo 23777 df-xms 24344 df-ms 24345 df-tms 24346 df-cau 25302 df-grpo 30516 df-gid 30517 df-ginv 30518 df-gdiv 30519 df-ablo 30568 df-vc 30582 df-nv 30615 df-va 30618 df-ba 30619 df-sm 30620 df-0v 30621 df-vs 30622 df-nmcv 30623 df-ims 30624 df-dip 30724 df-hnorm 30991 df-hvsub 30994 df-hlim 30995 df-hcau 30996 df-sh 31230 df-ch 31244 df-oc 31275 |
This theorem is referenced by: pjoc1i 31454 pjoc2i 31461 chsscon3i 31484 chsscon1i 31485 chdmm1i 31500 chdmm2i 31501 chdmm3i 31502 chdmm4i 31503 chdmj1i 31504 chdmj2i 31505 chdmj3i 31506 chdmj4i 31507 sshhococi 31569 h1de2bi 31577 h1de2ctlem 31578 h1de2ci 31579 spanunsni 31602 pjoml2i 31608 pjoml3i 31609 pjoml4i 31610 pjoml6i 31612 cmcmlem 31614 cmcm2i 31616 cmcm3i 31617 cmcm4i 31618 cmbr2i 31619 cmbr3i 31623 cmbr4i 31624 cm0 31632 fh3i 31646 fh4i 31647 cm2mi 31649 qlax5i 31654 qlaxr3i 31659 osumcori 31666 osumcor2i 31667 spansnji 31669 3oalem5 31689 3oalem6 31690 3oai 31691 pjcompi 31695 pjadjii 31697 pjaddii 31698 pjmulii 31700 pjss2i 31703 pjssmii 31704 pjssge0ii 31705 pjcji 31707 pjocini 31721 pjds3i 31736 pjnormi 31744 pjpythi 31745 pjneli 31746 mayetes3i 31752 riesz3i 32085 pjnormssi 32191 pjssdif2i 32197 pjssdif1i 32198 pjimai 32199 pjoccoi 32201 pjtoi 32202 pjoci 32203 pjclem1 32218 pjci 32223 hst0 32256 sto1i 32259 sto2i 32260 stlei 32263 stji1i 32265 golem1 32294 golem2 32295 goeqi 32296 stcltrlem1 32299 stcltrlem2 32300 mdsldmd1i 32354 hatomistici 32385 cvexchi 32392 atomli 32405 atordi 32407 chirredlem4 32416 chirredi 32417 mdsymi 32434 cmmdi 32439 cmdmdi 32440 mdoc1i 32448 mdoc2i 32449 dmdoc1i 32450 dmdoc2i 32451 mdcompli 32452 dmdcompli 32453 mddmdin0i 32454 |
Copyright terms: Public domain | W3C validator |