Metamath Proof Explorer

Theorem atcveq0

Description: A Hilbert lattice element covered by an atom must be the zero subspace. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	atcveq0	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A ⋖_{ℋ} B \leftrightarrow A = 0_{ℋ})$

Proof

Step	Hyp	Ref	Expression
1		atelch	$⊢ B \in HAtoms \to B \in C_{ℋ}$
2		cvpss	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} B \to A \subset B)$
3	1 2	sylan2	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A ⋖_{ℋ} B \to A \subset B)$
4		ch0le	$⊢ A \in C_{ℋ} \to 0_{ℋ} \subseteq A$
5	4	adantr	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to 0_{ℋ} \subseteq A$
6	3 5	jctild	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A ⋖_{ℋ} B \to (0_{ℋ} \subseteq A \land A \subset B))$
7		atcv0	$⊢ B \in HAtoms \to 0_{ℋ} ⋖_{ℋ} B$
8	7	adantr	$⊢ (B \in HAtoms \land A \in C_{ℋ}) \to 0_{ℋ} ⋖_{ℋ} B$
9		h0elch	$⊢ 0_{ℋ} \in C_{ℋ}$
10		cvnbtwn3	$⊢ (0_{ℋ} \in C_{ℋ} \land B \in C_{ℋ} \land A \in C_{ℋ}) \to (0_{ℋ} ⋖_{ℋ} B \to ((0_{ℋ} \subseteq A \land A \subset B) \to A = 0_{ℋ}))$
11	9 10	mp3an1	$⊢ (B \in C_{ℋ} \land A \in C_{ℋ}) \to (0_{ℋ} ⋖_{ℋ} B \to ((0_{ℋ} \subseteq A \land A \subset B) \to A = 0_{ℋ}))$
12	1 11	sylan	$⊢ (B \in HAtoms \land A \in C_{ℋ}) \to (0_{ℋ} ⋖_{ℋ} B \to ((0_{ℋ} \subseteq A \land A \subset B) \to A = 0_{ℋ}))$
13	8 12	mpd	$⊢ (B \in HAtoms \land A \in C_{ℋ}) \to ((0_{ℋ} \subseteq A \land A \subset B) \to A = 0_{ℋ})$
14	13	ancoms	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to ((0_{ℋ} \subseteq A \land A \subset B) \to A = 0_{ℋ})$
15	6 14	syld	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A ⋖_{ℋ} B \to A = 0_{ℋ})$
16		breq1	$⊢ A = 0_{ℋ} \to (A ⋖_{ℋ} B \leftrightarrow 0_{ℋ} ⋖_{ℋ} B)$
17	7 16	syl5ibrcom	$⊢ B \in HAtoms \to (A = 0_{ℋ} \to A ⋖_{ℋ} B)$
18	17	adantl	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A = 0_{ℋ} \to A ⋖_{ℋ} B)$
19	15 18	impbid	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A ⋖_{ℋ} B \leftrightarrow A = 0_{ℋ})$