This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ C ℋ → A ∈ HAtoms ↔ 0 ℋ ⋖ ℋ A

Proof

Step Hyp Ref Expression
1 ela ⊢ A ∈ HAtoms ↔ A ∈ C ℋ ∧ 0 ℋ ⋖ ℋ A
2 1 baib ⊢ A ∈ C ℋ → A ∈ HAtoms ↔ 0 ℋ ⋖ ℋ A