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 ( 𝐴C → ( 𝐴 ∈ HAtoms ↔ 0 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ela ( 𝐴 ∈ HAtoms ↔ ( 𝐴C ∧ 0 𝐴 ) )
2 1 baib ( 𝐴C → ( 𝐴 ∈ HAtoms ↔ 0 𝐴 ) )