Metamath Proof Explorer


Theorem elatcv0

Description: A Hilbert lattice element is an atom iff it covers the zero subspace. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion elatcv0
|- ( A e. CH -> ( A e. HAtoms <-> 0H 

Proof

Step Hyp Ref Expression
1 ela
 |-  ( A e. HAtoms <-> ( A e. CH /\ 0H 
2 1 baib
 |-  ( A e. CH -> ( A e. HAtoms <-> 0H