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

Metamath Proof Explorer

Theorem atnssm0

Description: The meet of a Hilbert lattice element and an incomparable atom is the zero subspace. (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	atnssm0	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (\neg B \subseteq A \leftrightarrow A \cap B = 0_{ℋ})$

Proof

Step	Hyp	Ref	Expression
1		chcv1	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (\neg B \subseteq A \leftrightarrow A ⋖_{ℋ} (A \lor_{ℋ} B))$
2		cvp	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A \cap B = 0_{ℋ} \leftrightarrow A ⋖_{ℋ} (A \lor_{ℋ} B))$
3	1 2	bitr4d	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (\neg B \subseteq A \leftrightarrow A \cap B = 0_{ℋ})$