Metamath Proof Explorer


Theorem pjbdlni

Description: A projector is a bounded linear operator. (Contributed by NM, 3-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis pjhmop.1 HC
Assertion pjbdlni projHBndLinOp

Proof

Step Hyp Ref Expression
1 pjhmop.1 HC
2 1 pjlnopi projHLinOp
3 2fveq3 H=0normopprojH=normopproj0
4 3 eleq1d H=0normopprojHnormopproj0
5 1 pjnmopi H0normopprojH=1
6 1re 1
7 5 6 eqeltrdi H0normopprojH
8 7 adantl HCH0normopprojH
9 df-h0op 0hop=proj0
10 9 fveq2i normop0hop=normopproj0
11 nmop0 normop0hop=0
12 10 11 eqtr3i normopproj0=0
13 0re 0
14 12 13 eqeltri normopproj0
15 14 a1i HCnormopproj0
16 4 8 15 pm2.61ne HCnormopprojH
17 1 16 ax-mp normopprojH
18 elbdop2 projHBndLinOpprojHLinOpnormopprojH
19 2 17 18 mpbir2an projHBndLinOp