Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > pjfi | Structured version Visualization version GIF version |
Description: The mapping of a projection. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
Ref | Expression |
---|---|
pjfn.1 | ⊢ 𝐻 ∈ Cℋ |
Ref | Expression |
---|---|
pjfi | ⊢ (projℎ‘𝐻): ℋ⟶ ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pjfn.1 | . . 3 ⊢ 𝐻 ∈ Cℋ | |
2 | 1 | pjfni 29628 | . 2 ⊢ (projℎ‘𝐻) Fn ℋ |
3 | 1 | pjrni 29629 | . . 3 ⊢ ran (projℎ‘𝐻) = 𝐻 |
4 | 1 | chssii 29158 | . . 3 ⊢ 𝐻 ⊆ ℋ |
5 | 3, 4 | eqsstri 3909 | . 2 ⊢ ran (projℎ‘𝐻) ⊆ ℋ |
6 | df-f 6337 | . 2 ⊢ ((projℎ‘𝐻): ℋ⟶ ℋ ↔ ((projℎ‘𝐻) Fn ℋ ∧ ran (projℎ‘𝐻) ⊆ ℋ)) | |
7 | 2, 5, 6 | mpbir2an 711 | 1 ⊢ (projℎ‘𝐻): ℋ⟶ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 ⊆ wss 3841 ran crn 5520 Fn wfn 6328 ⟶wf 6329 ‘cfv 6333 ℋchba 28846 Cℋ cch 28856 projℎcpjh 28864 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5151 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-inf2 9170 ax-cc 9928 ax-cnex 10664 ax-resscn 10665 ax-1cn 10666 ax-icn 10667 ax-addcl 10668 ax-addrcl 10669 ax-mulcl 10670 ax-mulrcl 10671 ax-mulcom 10672 ax-addass 10673 ax-mulass 10674 ax-distr 10675 ax-i2m1 10676 ax-1ne0 10677 ax-1rid 10678 ax-rnegex 10679 ax-rrecex 10680 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 ax-pre-ltadd 10684 ax-pre-mulgt0 10685 ax-pre-sup 10686 ax-addf 10687 ax-mulf 10688 ax-hilex 28926 ax-hfvadd 28927 ax-hvcom 28928 ax-hvass 28929 ax-hv0cl 28930 ax-hvaddid 28931 ax-hfvmul 28932 ax-hvmulid 28933 ax-hvmulass 28934 ax-hvdistr1 28935 ax-hvdistr2 28936 ax-hvmul0 28937 ax-hfi 29006 ax-his1 29009 ax-his2 29010 ax-his3 29011 ax-his4 29012 ax-hcompl 29129 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-int 4834 df-iun 4880 df-iin 4881 df-br 5028 df-opab 5090 df-mpt 5108 df-tr 5134 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6123 df-ord 6169 df-on 6170 df-lim 6171 df-suc 6172 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-isom 6342 df-riota 7121 df-ov 7167 df-oprab 7168 df-mpo 7169 df-of 7419 df-om 7594 df-1st 7707 df-2nd 7708 df-supp 7850 df-wrecs 7969 df-recs 8030 df-rdg 8068 df-1o 8124 df-2o 8125 df-oadd 8128 df-omul 8129 df-er 8313 df-map 8432 df-pm 8433 df-ixp 8501 df-en 8549 df-dom 8550 df-sdom 8551 df-fin 8552 df-fsupp 8900 df-fi 8941 df-sup 8972 df-inf 8973 df-oi 9040 df-card 9434 df-acn 9437 df-pnf 10748 df-mnf 10749 df-xr 10750 df-ltxr 10751 df-le 10752 df-sub 10943 df-neg 10944 df-div 11369 df-nn 11710 df-2 11772 df-3 11773 df-4 11774 df-5 11775 df-6 11776 df-7 11777 df-8 11778 df-9 11779 df-n0 11970 df-z 12056 df-dec 12173 df-uz 12318 df-q 12424 df-rp 12466 df-xneg 12583 df-xadd 12584 df-xmul 12585 df-ioo 12818 df-ico 12820 df-icc 12821 df-fz 12975 df-fzo 13118 df-fl 13246 df-seq 13454 df-exp 13515 df-hash 13776 df-cj 14541 df-re 14542 df-im 14543 df-sqrt 14677 df-abs 14678 df-clim 14928 df-rlim 14929 df-sum 15129 df-struct 16581 df-ndx 16582 df-slot 16583 df-base 16585 df-sets 16586 df-ress 16587 df-plusg 16674 df-mulr 16675 df-starv 16676 df-sca 16677 df-vsca 16678 df-ip 16679 df-tset 16680 df-ple 16681 df-ds 16683 df-unif 16684 df-hom 16685 df-cco 16686 df-rest 16792 df-topn 16793 df-0g 16811 df-gsum 16812 df-topgen 16813 df-pt 16814 df-prds 16817 df-xrs 16871 df-qtop 16876 df-imas 16877 df-xps 16879 df-mre 16953 df-mrc 16954 df-acs 16956 df-mgm 17961 df-sgrp 18010 df-mnd 18021 df-submnd 18066 df-mulg 18336 df-cntz 18558 df-cmn 19019 df-psmet 20202 df-xmet 20203 df-met 20204 df-bl 20205 df-mopn 20206 df-fbas 20207 df-fg 20208 df-cnfld 20211 df-top 21638 df-topon 21655 df-topsp 21677 df-bases 21690 df-cld 21763 df-ntr 21764 df-cls 21765 df-nei 21842 df-cn 21971 df-cnp 21972 df-lm 21973 df-haus 22059 df-tx 22306 df-hmeo 22499 df-fil 22590 df-fm 22682 df-flim 22683 df-flf 22684 df-xms 23066 df-ms 23067 df-tms 23068 df-cfil 24000 df-cau 24001 df-cmet 24002 df-grpo 28420 df-gid 28421 df-ginv 28422 df-gdiv 28423 df-ablo 28472 df-vc 28486 df-nv 28519 df-va 28522 df-ba 28523 df-sm 28524 df-0v 28525 df-vs 28526 df-nmcv 28527 df-ims 28528 df-dip 28628 df-ssp 28649 df-ph 28740 df-cbn 28790 df-hnorm 28895 df-hba 28896 df-hvsub 28898 df-hlim 28899 df-hcau 28900 df-sh 29134 df-ch 29148 df-oc 29179 df-ch0 29180 df-shs 29235 df-pjh 29322 |
This theorem is referenced by: ho0f 29678 hoid1i 29716 hoid1ri 29717 pjhmopi 30073 pjnmopi 30075 pjsdii 30082 pjddii 30083 pjcoi 30085 pjcohcli 30087 pjcofni 30089 pjss1coi 30090 pjss2coi 30091 pjorthcoi 30096 pjscji 30097 pjssposi 30099 pjssdif2i 30101 pjtoi 30106 pjoci 30107 pjclem1 30122 pjclem3 30124 pjclem4 30126 pjci 30127 pjcohocli 30130 pjadj2coi 30131 pj2cocli 30132 pj3lem1 30133 pj3si 30134 pj3cor1i 30136 |
Copyright terms: Public domain | W3C validator |