Theorem pjhcli 31675

Description: Closure of a projection in Hilbert space. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.)

Hypothesis

Ref	Expression
pjcl.1	⊢ 𝐻 ∈ Cℋ

Assertion

Ref	Expression
pjhcli	⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ ℋ)

Proof of Theorem pjhcli

Step	Hyp	Ref	Expression
1		pjcl.1	. 2 ⊢ 𝐻 ∈ Cℋ
2		pjhcl 31658	. 2 ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ ℋ)
3	1, 2	mpan 702	1 ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ ℋ)

Syntax hints:   → wi 4   ∈ wcel 2145  ‘cfv 6525   ℋchba 31176   C_ℋ cch 31186  proj_ℎcpjh 31194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5231  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-inf2 9598  ax-cc 10407  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165  ax-pre-sup 11166  ax-addf 11167  ax-mulf 11168  ax-hilex 31256  ax-hfvadd 31257  ax-hvcom 31258  ax-hvass 31259  ax-hv0cl 31260  ax-hvaddid 31261  ax-hfvmul 31262  ax-hvmulid 31263  ax-hvmulass 31264  ax-hvdistr1 31265  ax-hvdistr2 31266  ax-hvmul0 31267  ax-hfi 31336  ax-his1 31339  ax-his2 31340  ax-his3 31341  ax-his4 31342  ax-hcompl 31459

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5105  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6291  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-isom 6534  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-2o 8442  df-oadd 8445  df-omul 8446  df-er 8682  df-map 8814  df-pm 8815  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-fi 9359  df-sup 9390  df-inf 9391  df-oi 9460  df-card 9913  df-acn 9916  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-div 11860  df-nn 12222  df-2 12291  df-3 12292  df-4 12293  df-n0 12493  df-z 12580  df-uz 12851  df-q 12961  df-rp 13005  df-xneg 13125  df-xadd 13126  df-xmul 13127  df-ico 13366  df-icc 13367  df-fz 13524  df-fl 13813  df-seq 14026  df-exp 14086  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15527  df-rlim 15528  df-rest 17463  df-topgen 17484  df-psmet 21471  df-xmet 21472  df-met 21473  df-bl 21474  df-mopn 21475  df-fbas 21476  df-fg 21477  df-top 23008  df-topon 23025  df-bases 23060  df-cld 23133  df-ntr 23134  df-cls 23135  df-nei 23212  df-lm 23343  df-haus 23429  df-fil 23960  df-fm 24052  df-flim 24053  df-flf 24054  df-cfil 25371  df-cau 25372  df-cmet 25373  df-grpo 30750  df-gid 30751  df-ginv 30752  df-gdiv 30753  df-ablo 30802  df-vc 30816  df-nv 30849  df-va 30852  df-ba 30853  df-sm 30854  df-0v 30855  df-vs 30856  df-nmcv 30857  df-ims 30858  df-ssp 30979  df-ph 31070  df-cbn 31120  df-hnorm 31225  df-hba 31226  df-hvsub 31228  df-hlim 31229  df-hcau 31230  df-sh 31464  df-ch 31478  df-oc 31509  df-ch0 31510  df-shs 31565  df-pjh 31652

This theorem is referenced by:  pjhclii  31679  pjige0i  31947  mayete3i  31985  ho0val  32007  pjnmopi  32405  pjcocli  32416  pjadjcoi  32418  pjss2coi  32421  pjnormssi  32425  pjorthcoi  32426  pjssposi  32429  pjadj2coi  32461  pj2cocli  32462  pjs14i  32467  strlem5  32512  jplem1  32525