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 0hopLinOp

Proof

Step Hyp Ref Expression
1 0hmop 0hopHrmOp
2 hmoplin 0hopHrmOp0hopLinOp
3 1 2 ax-mp 0hopLinOp