Metamath Proof Explorer

Theorem pjlnopi

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

Ref Expression
Hypothesis pjhmop.1 
|- H e. CH
Assertion pjlnopi 
|- ( projh ` H ) e. LinOp

Proof

Step Hyp Ref Expression
1 pjhmop.1 
 |-  H e. CH
2 1 pjhmopi 
 |-  ( projh ` H ) e. HrmOp
3 hmoplin 
 |-  ( ( projh ` H ) e. HrmOp -> ( projh ` H ) e. LinOp )
4 2 3 ax-mp 
 |-  ( projh ` H ) e. LinOp