Metamath Proof Explorer

Theorem 0lnop

Description: The identically zero function is a linear Hilbert space operator. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion 0lnop 
|- 0hop e. LinOp

Proof

Step Hyp Ref Expression
1 0hmop 
 |-  0hop e. HrmOp
2 hmoplin 
 |-  ( 0hop e. HrmOp -> 0hop e. LinOp )
3 1 2 ax-mp 
 |-  0hop e. LinOp