![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > pjssdif2i | Structured version Visualization version GIF version |
Description: The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 31156). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
Ref | Expression |
---|---|
pjco.1 | โข ๐บ โ Cโ |
pjco.2 | โข ๐ป โ Cโ |
Ref | Expression |
---|---|
pjssdif2i | โข (๐บ โ ๐ป โ ((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjco.2 | . . . . . . . 8 โข ๐ป โ Cโ | |
2 | 1 | pjfi 30688 | . . . . . . 7 โข (projโโ๐ป): โโถ โ |
3 | pjco.1 | . . . . . . . 8 โข ๐บ โ Cโ | |
4 | 3 | pjfi 30688 | . . . . . . 7 โข (projโโ๐บ): โโถ โ |
5 | hodval 30726 | . . . . . . 7 โข (((projโโ๐ป): โโถ โ โง (projโโ๐บ): โโถ โ โง ๐ฅ โ โ) โ (((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) = (((projโโ๐ป)โ๐ฅ) โโ ((projโโ๐บ)โ๐ฅ))) | |
6 | 2, 4, 5 | mp3an12 1452 | . . . . . 6 โข (๐ฅ โ โ โ (((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) = (((projโโ๐ป)โ๐ฅ) โโ ((projโโ๐บ)โ๐ฅ))) |
7 | 6 | adantl 483 | . . . . 5 โข ((๐บ โ ๐ป โง ๐ฅ โ โ) โ (((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) = (((projโโ๐ป)โ๐ฅ) โโ ((projโโ๐บ)โ๐ฅ))) |
8 | 1, 3 | pjssmi 31149 | . . . . . 6 โข (๐ฅ โ โ โ (๐บ โ ๐ป โ (((projโโ๐ป)โ๐ฅ) โโ ((projโโ๐บ)โ๐ฅ)) = ((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ))) |
9 | 8 | impcom 409 | . . . . 5 โข ((๐บ โ ๐ป โง ๐ฅ โ โ) โ (((projโโ๐ป)โ๐ฅ) โโ ((projโโ๐บ)โ๐ฅ)) = ((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ)) |
10 | 7, 9 | eqtrd 2777 | . . . 4 โข ((๐บ โ ๐ป โง ๐ฅ โ โ) โ (((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) = ((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ)) |
11 | 10 | ralrimiva 3144 | . . 3 โข (๐บ โ ๐ป โ โ๐ฅ โ โ (((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) = ((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ)) |
12 | 2, 4 | hosubfni 30755 | . . . 4 โข ((projโโ๐ป) โop (projโโ๐บ)) Fn โ |
13 | 3 | choccli 30291 | . . . . . 6 โข (โฅโ๐บ) โ Cโ |
14 | 1, 13 | chincli 30444 | . . . . 5 โข (๐ป โฉ (โฅโ๐บ)) โ Cโ |
15 | 14 | pjfni 30685 | . . . 4 โข (projโโ(๐ป โฉ (โฅโ๐บ))) Fn โ |
16 | eqfnfv 6987 | . . . 4 โข ((((projโโ๐ป) โop (projโโ๐บ)) Fn โ โง (projโโ(๐ป โฉ (โฅโ๐บ))) Fn โ) โ (((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ))) โ โ๐ฅ โ โ (((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) = ((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ))) | |
17 | 12, 15, 16 | mp2an 691 | . . 3 โข (((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ))) โ โ๐ฅ โ โ (((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) = ((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ)) |
18 | 11, 17 | sylibr 233 | . 2 โข (๐บ โ ๐ป โ ((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ)))) |
19 | 14 | pjige0i 30674 | . . . . . 6 โข (๐ฅ โ โ โ 0 โค (((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ) ยทih ๐ฅ)) |
20 | 19 | adantl 483 | . . . . 5 โข ((((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ))) โง ๐ฅ โ โ) โ 0 โค (((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ) ยทih ๐ฅ)) |
21 | fveq1 6846 | . . . . . . 7 โข (((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ))) โ (((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) = ((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ)) | |
22 | 21 | oveq1d 7377 | . . . . . 6 โข (((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ))) โ ((((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) ยทih ๐ฅ) = (((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ) ยทih ๐ฅ)) |
23 | 22 | adantr 482 | . . . . 5 โข ((((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ))) โง ๐ฅ โ โ) โ ((((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) ยทih ๐ฅ) = (((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ) ยทih ๐ฅ)) |
24 | 20, 23 | breqtrrd 5138 | . . . 4 โข ((((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ))) โง ๐ฅ โ โ) โ 0 โค ((((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) ยทih ๐ฅ)) |
25 | 24 | ralrimiva 3144 | . . 3 โข (((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ))) โ โ๐ฅ โ โ 0 โค ((((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) ยทih ๐ฅ)) |
26 | 3, 1 | pjssposi 31156 | . . 3 โข (โ๐ฅ โ โ 0 โค ((((projโโ๐ป) โop (projโโ๐บ))โ๐ฅ) ยทih ๐ฅ) โ ๐บ โ ๐ป) |
27 | 25, 26 | sylib 217 | . 2 โข (((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ))) โ ๐บ โ ๐ป) |
28 | 18, 27 | impbii 208 | 1 โข (๐บ โ ๐ป โ ((projโโ๐ป) โop (projโโ๐บ)) = (projโโ(๐ป โฉ (โฅโ๐บ)))) |
Colors of variables: wff setvar class |
Syntax hints: โ wb 205 โง wa 397 = wceq 1542 โ wcel 2107 โwral 3065 โฉ cin 3914 โ wss 3915 class class class wbr 5110 Fn wfn 6496 โถwf 6497 โcfv 6501 (class class class)co 7362 0cc0 11058 โค cle 11197 โchba 29903 ยทih csp 29906 โโ cmv 29909 Cโ cch 29913 โฅcort 29914 projโcpjh 29921 โop chod 29924 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 ax-rep 5247 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-inf2 9584 ax-cc 10378 ax-cnex 11114 ax-resscn 11115 ax-1cn 11116 ax-icn 11117 ax-addcl 11118 ax-addrcl 11119 ax-mulcl 11120 ax-mulrcl 11121 ax-mulcom 11122 ax-addass 11123 ax-mulass 11124 ax-distr 11125 ax-i2m1 11126 ax-1ne0 11127 ax-1rid 11128 ax-rnegex 11129 ax-rrecex 11130 ax-cnre 11131 ax-pre-lttri 11132 ax-pre-lttrn 11133 ax-pre-ltadd 11134 ax-pre-mulgt0 11135 ax-pre-sup 11136 ax-addf 11137 ax-mulf 11138 ax-hilex 29983 ax-hfvadd 29984 ax-hvcom 29985 ax-hvass 29986 ax-hv0cl 29987 ax-hvaddid 29988 ax-hfvmul 29989 ax-hvmulid 29990 ax-hvmulass 29991 ax-hvdistr1 29992 ax-hvdistr2 29993 ax-hvmul0 29994 ax-hfi 30063 ax-his1 30066 ax-his2 30067 ax-his3 30068 ax-his4 30069 ax-hcompl 30186 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3066 df-rex 3075 df-rmo 3356 df-reu 3357 df-rab 3411 df-v 3450 df-sbc 3745 df-csb 3861 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-pss 3934 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4871 df-int 4913 df-iun 4961 df-iin 4962 df-br 5111 df-opab 5173 df-mpt 5194 df-tr 5228 df-id 5536 df-eprel 5542 df-po 5550 df-so 5551 df-fr 5593 df-se 5594 df-we 5595 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6258 df-ord 6325 df-on 6326 df-lim 6327 df-suc 6328 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-isom 6510 df-riota 7318 df-ov 7365 df-oprab 7366 df-mpo 7367 df-of 7622 df-om 7808 df-1st 7926 df-2nd 7927 df-supp 8098 df-frecs 8217 df-wrecs 8248 df-recs 8322 df-rdg 8361 df-1o 8417 df-2o 8418 df-oadd 8421 df-omul 8422 df-er 8655 df-map 8774 df-pm 8775 df-ixp 8843 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fsupp 9313 df-fi 9354 df-sup 9385 df-inf 9386 df-oi 9453 df-card 9882 df-acn 9885 df-pnf 11198 df-mnf 11199 df-xr 11200 df-ltxr 11201 df-le 11202 df-sub 11394 df-neg 11395 df-div 11820 df-nn 12161 df-2 12223 df-3 12224 df-4 12225 df-5 12226 df-6 12227 df-7 12228 df-8 12229 df-9 12230 df-n0 12421 df-z 12507 df-dec 12626 df-uz 12771 df-q 12881 df-rp 12923 df-xneg 13040 df-xadd 13041 df-xmul 13042 df-ioo 13275 df-ico 13277 df-icc 13278 df-fz 13432 df-fzo 13575 df-fl 13704 df-seq 13914 df-exp 13975 df-hash 14238 df-cj 14991 df-re 14992 df-im 14993 df-sqrt 15127 df-abs 15128 df-clim 15377 df-rlim 15378 df-sum 15578 df-struct 17026 df-sets 17043 df-slot 17061 df-ndx 17073 df-base 17091 df-ress 17120 df-plusg 17153 df-mulr 17154 df-starv 17155 df-sca 17156 df-vsca 17157 df-ip 17158 df-tset 17159 df-ple 17160 df-ds 17162 df-unif 17163 df-hom 17164 df-cco 17165 df-rest 17311 df-topn 17312 df-0g 17330 df-gsum 17331 df-topgen 17332 df-pt 17333 df-prds 17336 df-xrs 17391 df-qtop 17396 df-imas 17397 df-xps 17399 df-mre 17473 df-mrc 17474 df-acs 17476 df-mgm 18504 df-sgrp 18553 df-mnd 18564 df-submnd 18609 df-mulg 18880 df-cntz 19104 df-cmn 19571 df-psmet 20804 df-xmet 20805 df-met 20806 df-bl 20807 df-mopn 20808 df-fbas 20809 df-fg 20810 df-cnfld 20813 df-top 22259 df-topon 22276 df-topsp 22298 df-bases 22312 df-cld 22386 df-ntr 22387 df-cls 22388 df-nei 22465 df-cn 22594 df-cnp 22595 df-lm 22596 df-haus 22682 df-tx 22929 df-hmeo 23122 df-fil 23213 df-fm 23305 df-flim 23306 df-flf 23307 df-xms 23689 df-ms 23690 df-tms 23691 df-cfil 24635 df-cau 24636 df-cmet 24637 df-grpo 29477 df-gid 29478 df-ginv 29479 df-gdiv 29480 df-ablo 29529 df-vc 29543 df-nv 29576 df-va 29579 df-ba 29580 df-sm 29581 df-0v 29582 df-vs 29583 df-nmcv 29584 df-ims 29585 df-dip 29685 df-ssp 29706 df-ph 29797 df-cbn 29847 df-hnorm 29952 df-hba 29953 df-hvsub 29955 df-hlim 29956 df-hcau 29957 df-sh 30191 df-ch 30205 df-oc 30236 df-ch0 30237 df-shs 30292 df-pjh 30379 df-hodif 30716 |
This theorem is referenced by: pjssdif1i 31159 |
Copyright terms: Public domain | W3C validator |