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 C
Assertion chle0i A 0 A = 0

Proof

Step Hyp Ref Expression
1 ch0le.1 A C
2 chle0 A C A 0 A = 0
3 1 2 ax-mp A 0 A = 0