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 
|- H e. CH
Assertion pjbdlni 
|- ( projh ` H ) e. BndLinOp

Proof

Step Hyp Ref Expression
1 pjhmop.1 
 |-  H e. CH
2 1 pjlnopi 
 |-  ( projh ` H ) e. LinOp
3 2fveq3 
 |-  ( H = 0H -> ( normop ` ( projh ` H ) ) = ( normop ` ( projh ` 0H ) ) )
4 3 eleq1d 
 |-  ( H = 0H -> ( ( normop ` ( projh ` H ) ) e. RR <-> ( normop ` ( projh ` 0H ) ) e. RR ) )
5 1 pjnmopi 
 |-  ( H =/= 0H -> ( normop ` ( projh ` H ) ) = 1 )
6 1re 
 |-  1 e. RR
7 5 6 eqeltrdi 
 |-  ( H =/= 0H -> ( normop ` ( projh ` H ) ) e. RR )
8 7 adantl 
 |-  ( ( H e. CH /\ H =/= 0H ) -> ( normop ` ( projh ` H ) ) e. RR )
9 df-h0op 
 |-  0hop = ( projh ` 0H )
10 9 fveq2i 
 |-  ( normop ` 0hop ) = ( normop ` ( projh ` 0H ) )
11 nmop0 
 |-  ( normop ` 0hop ) = 0
12 10 11 eqtr3i 
 |-  ( normop ` ( projh ` 0H ) ) = 0
13 0re 
 |-  0 e. RR
14 12 13 eqeltri 
 |-  ( normop ` ( projh ` 0H ) ) e. RR
15 14 a1i 
 |-  ( H e. CH -> ( normop ` ( projh ` 0H ) ) e. RR )
16 4 8 15 pm2.61ne 
 |-  ( H e. CH -> ( normop ` ( projh ` H ) ) e. RR )
17 1 16 ax-mp 
 |-  ( normop ` ( projh ` H ) ) e. RR
18 elbdop2 
 |-  ( ( projh ` H ) e. BndLinOp <-> ( ( projh ` H ) e. LinOp /\ ( normop ` ( projh ` H ) ) e. RR ) )
19 2 17 18 mpbir2an 
 |-  ( projh ` H ) e. BndLinOp