Theorem pjhcli 31577

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 31560	. 2 ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) ∈ ℋ)
3	1, 2	mpan 700	1 ⊢ (𝐴 ∈ ℋ → ((projℎ‘𝐻)‘𝐴) ∈ ℋ)

Syntax hints:   → wi 4   ∈ wcel 2141  ‘cfv 6515   ℋchba 31078   C_ℋ cch 31088  proj_ℎcpjh 31096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-inf2 9589  ax-cc 10385  ax-cnex 11122  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142  ax-pre-mulgt0 11143  ax-pre-sup 11144  ax-addf 11145  ax-mulf 11146  ax-hilex 31158  ax-hfvadd 31159  ax-hvcom 31160  ax-hvass 31161  ax-hv0cl 31162  ax-hvaddid 31163  ax-hfvmul 31164  ax-hvmulid 31165  ax-hvmulass 31166  ax-hvdistr1 31167  ax-hvdistr2 31168  ax-hvmul0 31169  ax-hfi 31238  ax-his1 31241  ax-his2 31242  ax-his3 31243  ax-his4 31244  ax-hcompl 31361

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-int 4903  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-se 5597  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-isom 6524  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7841  df-1st 7964  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-1o 8430  df-2o 8431  df-oadd 8434  df-omul 8435  df-er 8671  df-map 8803  df-pm 8804  df-en 8921  df-dom 8922  df-sdom 8923  df-fin 8924  df-fi 9350  df-sup 9381  df-inf 9382  df-oi 9451  df-card 9890  df-acn 9893  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215  df-sub 11409  df-neg 11410  df-div 11838  df-nn 12204  df-2 12273  df-3 12274  df-4 12275  df-n0 12475  df-z 12562  df-uz 12833  df-q 12943  df-rp 12987  df-xneg 13107  df-xadd 13108  df-xmul 13109  df-ico 13348  df-icc 13349  df-fz 13506  df-fl 13795  df-seq 14008  df-exp 14068  df-cj 15116  df-re 15117  df-im 15118  df-sqrt 15252  df-abs 15253  df-clim 15505  df-rlim 15506  df-rest 17441  df-topgen 17462  df-psmet 21403  df-xmet 21404  df-met 21405  df-bl 21406  df-mopn 21407  df-fbas 21408  df-fg 21409  df-top 22941  df-topon 22958  df-bases 22993  df-cld 23066  df-ntr 23067  df-cls 23068  df-nei 23145  df-lm 23276  df-haus 23362  df-fil 23893  df-fm 23985  df-flim 23986  df-flf 23987  df-cfil 25304  df-cau 25305  df-cmet 25306  df-grpo 30652  df-gid 30653  df-ginv 30654  df-gdiv 30655  df-ablo 30704  df-vc 30718  df-nv 30751  df-va 30754  df-ba 30755  df-sm 30756  df-0v 30757  df-vs 30758  df-nmcv 30759  df-ims 30760  df-ssp 30881  df-ph 30972  df-cbn 31022  df-hnorm 31127  df-hba 31128  df-hvsub 31130  df-hlim 31131  df-hcau 31132  df-sh 31366  df-ch 31380  df-oc 31411  df-ch0 31412  df-shs 31467  df-pjh 31554

This theorem is referenced by:  pjhclii  31581  pjige0i  31849  mayete3i  31887  ho0val  31909  pjnmopi  32307  pjcocli  32318  pjadjcoi  32320  pjss2coi  32323  pjnormssi  32327  pjorthcoi  32328  pjssposi  32331  pjadj2coi  32363  pj2cocli  32364  pjs14i  32369  strlem5  32414  jplem1  32427