![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > HSE Home > Th. List > pjo | Unicode version |
Description: The orthogonal projection. Lemma 4.4(i) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
pjo |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjch1 23125 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantl 453 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | axpjpj 22875 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqtr2d 2437 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | helch 22699 |
. . . . . 6
![]() ![]() ![]() ![]() | |
6 | 5 | pjcli 22872 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | adantl 453 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | pjhcl 22856 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | choccl 22761 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | pjhcl 22856 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | sylan 458 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | hvsubadd 22532 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | 7, 8, 11, 12 | syl3anc 1184 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 4, 13 | mpbird 224 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 14 | eqcomd 2409 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: pjsslem 23134 ho0val 23206 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cc 8271 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024 ax-addf 9025 ax-mulf 9026 ax-hilex 22455 ax-hfvadd 22456 ax-hvcom 22457 ax-hvass 22458 ax-hv0cl 22459 ax-hvaddid 22460 ax-hfvmul 22461 ax-hvmulid 22462 ax-hvmulass 22463 ax-hvdistr1 22464 ax-hvdistr2 22465 ax-hvmul0 22466 ax-hfi 22534 ax-his1 22537 ax-his2 22538 ax-his3 22539 ax-his4 22540 ax-hcompl 22657 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-of 6264 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-omul 6688 df-er 6864 df-map 6979 df-pm 6980 df-ixp 7023 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-sup 7404 df-oi 7435 df-card 7782 df-acn 7785 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-q 10531 df-rp 10569 df-xneg 10666 df-xadd 10667 df-xmul 10668 df-ioo 10876 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-fl 11157 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-rlim 12238 df-sum 12435 df-struct 13426 df-ndx 13427 df-slot 13428 df-base 13429 df-sets 13430 df-ress 13431 df-plusg 13497 df-mulr 13498 df-starv 13499 df-sca 13500 df-vsca 13501 df-tset 13503 df-ple 13504 df-ds 13506 df-unif 13507 df-hom 13508 df-cco 13509 df-rest 13605 df-topn 13606 df-topgen 13622 df-pt 13623 df-prds 13626 df-xrs 13681 df-0g 13682 df-gsum 13683 df-qtop 13688 df-imas 13689 df-xps 13691 df-mre 13766 df-mrc 13767 df-acs 13769 df-mnd 14645 df-submnd 14694 df-mulg 14770 df-cntz 15071 df-cmn 15369 df-psmet 16649 df-xmet 16650 df-met 16651 df-bl 16652 df-mopn 16653 df-fbas 16654 df-fg 16655 df-cnfld 16659 df-top 16918 df-bases 16920 df-topon 16921 df-topsp 16922 df-cld 17038 df-ntr 17039 df-cls 17040 df-nei 17117 df-cn 17245 df-cnp 17246 df-lm 17247 df-haus 17333 df-tx 17547 df-hmeo 17740 df-fil 17831 df-fm 17923 df-flim 17924 df-flf 17925 df-xms 18303 df-ms 18304 df-tms 18305 df-cfil 19161 df-cau 19162 df-cmet 19163 df-grpo 21732 df-gid 21733 df-ginv 21734 df-gdiv 21735 df-ablo 21823 df-subgo 21843 df-vc 21978 df-nv 22024 df-va 22027 df-ba 22028 df-sm 22029 df-0v 22030 df-vs 22031 df-nmcv 22032 df-ims 22033 df-dip 22150 df-ssp 22174 df-ph 22267 df-cbn 22318 df-hnorm 22424 df-hba 22425 df-hvsub 22427 df-hlim 22428 df-hcau 22429 df-sh 22662 df-ch 22677 df-oc 22707 df-ch0 22708 df-shs 22763 df-pjh 22850 |
Copyright terms: Public domain | W3C validator |