Metamath Proof Explorer


Theorem chle0i

Description: No Hilbert closed subspace is smaller than zero. (Contributed by NM, 7-Apr-2001) (New usage is discouraged.)

Ref Expression
Hypothesis ch0le.1
|- A e. CH
Assertion chle0i
|- ( A C_ 0H <-> A = 0H )

Proof

Step Hyp Ref Expression
1 ch0le.1
 |-  A e. CH
2 chle0
 |-  ( A e. CH -> ( A C_ 0H <-> A = 0H ) )
3 1 2 ax-mp
 |-  ( A C_ 0H <-> A = 0H )