![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > leop | Structured version Visualization version GIF version |
Description: Ordering relation for operators. Definition of positive operator ordering in [Kreyszig] p. 470. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.) |
Ref | Expression |
---|---|
leop | โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐ โคop ๐ โ โ๐ฅ โ โ 0 โค (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leopg 31657 | . 2 โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐ โคop ๐ โ ((๐ โop ๐) โ HrmOp โง โ๐ฅ โ โ 0 โค (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ)))) | |
2 | hmopd 31557 | . . . 4 โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐ โop ๐) โ HrmOp) | |
3 | 2 | ancoms 458 | . . 3 โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐ โop ๐) โ HrmOp) |
4 | 3 | biantrurd 532 | . 2 โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (โ๐ฅ โ โ 0 โค (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ) โ ((๐ โop ๐) โ HrmOp โง โ๐ฅ โ โ 0 โค (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ)))) |
5 | 1, 4 | bitr4d 282 | 1 โข ((๐ โ HrmOp โง ๐ โ HrmOp) โ (๐ โคop ๐ โ โ๐ฅ โ โ 0 โค (((๐ โop ๐)โ๐ฅ) ยทih ๐ฅ))) |
Colors of variables: wff setvar class |
Syntax hints: โ wi 4 โ wb 205 โง wa 395 โ wcel 2105 โwral 3060 class class class wbr 5148 โcfv 6543 (class class class)co 7412 0cc0 11116 โค cle 11256 โchba 30454 ยทih csp 30457 โop chod 30475 HrmOpcho 30485 โคop cleo 30493 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-inf2 9642 ax-cc 10436 ax-cnex 11172 ax-resscn 11173 ax-1cn 11174 ax-icn 11175 ax-addcl 11176 ax-addrcl 11177 ax-mulcl 11178 ax-mulrcl 11179 ax-mulcom 11180 ax-addass 11181 ax-mulass 11182 ax-distr 11183 ax-i2m1 11184 ax-1ne0 11185 ax-1rid 11186 ax-rnegex 11187 ax-rrecex 11188 ax-cnre 11189 ax-pre-lttri 11190 ax-pre-lttrn 11191 ax-pre-ltadd 11192 ax-pre-mulgt0 11193 ax-pre-sup 11194 ax-addf 11195 ax-mulf 11196 ax-hilex 30534 ax-hfvadd 30535 ax-hvcom 30536 ax-hvass 30537 ax-hv0cl 30538 ax-hvaddid 30539 ax-hfvmul 30540 ax-hvmulid 30541 ax-hvmulass 30542 ax-hvdistr1 30543 ax-hvdistr2 30544 ax-hvmul0 30545 ax-hfi 30614 ax-his1 30617 ax-his2 30618 ax-his3 30619 ax-his4 30620 ax-hcompl 30737 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7674 df-om 7860 df-1st 7979 df-2nd 7980 df-supp 8152 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-1o 8472 df-2o 8473 df-oadd 8476 df-omul 8477 df-er 8709 df-map 8828 df-pm 8829 df-ixp 8898 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fsupp 9368 df-fi 9412 df-sup 9443 df-inf 9444 df-oi 9511 df-card 9940 df-acn 9943 df-pnf 11257 df-mnf 11258 df-xr 11259 df-ltxr 11260 df-le 11261 df-sub 11453 df-neg 11454 df-div 11879 df-nn 12220 df-2 12282 df-3 12283 df-4 12284 df-5 12285 df-6 12286 df-7 12287 df-8 12288 df-9 12289 df-n0 12480 df-z 12566 df-dec 12685 df-uz 12830 df-q 12940 df-rp 12982 df-xneg 13099 df-xadd 13100 df-xmul 13101 df-ioo 13335 df-ico 13337 df-icc 13338 df-fz 13492 df-fzo 13635 df-fl 13764 df-seq 13974 df-exp 14035 df-hash 14298 df-cj 15053 df-re 15054 df-im 15055 df-sqrt 15189 df-abs 15190 df-clim 15439 df-rlim 15440 df-sum 15640 df-struct 17087 df-sets 17104 df-slot 17122 df-ndx 17134 df-base 17152 df-ress 17181 df-plusg 17217 df-mulr 17218 df-starv 17219 df-sca 17220 df-vsca 17221 df-ip 17222 df-tset 17223 df-ple 17224 df-ds 17226 df-unif 17227 df-hom 17228 df-cco 17229 df-rest 17375 df-topn 17376 df-0g 17394 df-gsum 17395 df-topgen 17396 df-pt 17397 df-prds 17400 df-xrs 17455 df-qtop 17460 df-imas 17461 df-xps 17463 df-mre 17537 df-mrc 17538 df-acs 17540 df-mgm 18568 df-sgrp 18647 df-mnd 18663 df-submnd 18709 df-mulg 18991 df-cntz 19226 df-cmn 19695 df-psmet 21140 df-xmet 21141 df-met 21142 df-bl 21143 df-mopn 21144 df-fbas 21145 df-fg 21146 df-cnfld 21149 df-top 22629 df-topon 22646 df-topsp 22668 df-bases 22682 df-cld 22756 df-ntr 22757 df-cls 22758 df-nei 22835 df-cn 22964 df-cnp 22965 df-lm 22966 df-haus 23052 df-tx 23299 df-hmeo 23492 df-fil 23583 df-fm 23675 df-flim 23676 df-flf 23677 df-xms 24059 df-ms 24060 df-tms 24061 df-cfil 25016 df-cau 25017 df-cmet 25018 df-grpo 30028 df-gid 30029 df-ginv 30030 df-gdiv 30031 df-ablo 30080 df-vc 30094 df-nv 30127 df-va 30130 df-ba 30131 df-sm 30132 df-0v 30133 df-vs 30134 df-nmcv 30135 df-ims 30136 df-dip 30236 df-ssp 30257 df-ph 30348 df-cbn 30398 df-hnorm 30503 df-hba 30504 df-hvsub 30506 df-hlim 30507 df-hcau 30508 df-sh 30742 df-ch 30756 df-oc 30787 df-ch0 30788 df-shs 30843 df-pjh 30930 df-hosum 31265 df-homul 31266 df-hodif 31267 df-h0op 31283 df-hmop 31379 df-leop 31387 |
This theorem is referenced by: leop2 31659 leop3 31660 leoppos 31661 leoprf 31663 |
Copyright terms: Public domain | W3C validator |