Metamath Proof Explorer

Theorem cvati

Description: If a Hilbert lattice element covers another, it equals the other joined with some atom. This is a consequence of the relative atomicity of Hilbert space. (Contributed by NM, 30-Nov-2004) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	chpssat.1	$⊢ A \in C_{ℋ}$
		chpssat.2	$⊢ B \in C_{ℋ}$
	Assertion	cvati	$⊢ A ⋖_{ℋ} B \to \exists x \in HAtoms A \lor_{ℋ} x = B$

Proof

Step	Hyp	Ref	Expression
1		chpssat.1	$⊢ A \in C_{ℋ}$
2		chpssat.2	$⊢ B \in C_{ℋ}$
3		cvpss	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} B \to A \subset B)$
4	1 2 3	mp2an	$⊢ A ⋖_{ℋ} B \to A \subset B$
5	1 2	chrelati	$⊢ A \subset B \to \exists x \in HAtoms (A \subset A \lor_{ℋ} x \land A \lor_{ℋ} x \subseteq B)$
6	4 5	syl	$⊢ A ⋖_{ℋ} B \to \exists x \in HAtoms (A \subset A \lor_{ℋ} x \land A \lor_{ℋ} x \subseteq B)$
7		cvnbtwn2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land A \lor_{ℋ} x \in C_{ℋ}) \to (A ⋖_{ℋ} B \to ((A \subset A \lor_{ℋ} x \land A \lor_{ℋ} x \subseteq B) \to A \lor_{ℋ} x = B))$
8	1 2 7	mp3an12	$⊢ A \lor_{ℋ} x \in C_{ℋ} \to (A ⋖_{ℋ} B \to ((A \subset A \lor_{ℋ} x \land A \lor_{ℋ} x \subseteq B) \to A \lor_{ℋ} x = B))$
9		atelch	$⊢ x \in HAtoms \to x \in C_{ℋ}$
10		chjcl	$⊢ (A \in C_{ℋ} \land x \in C_{ℋ}) \to A \lor_{ℋ} x \in C_{ℋ}$
11	1 9 10	sylancr	$⊢ x \in HAtoms \to A \lor_{ℋ} x \in C_{ℋ}$
12	8 11	syl11	$⊢ A ⋖_{ℋ} B \to (x \in HAtoms \to ((A \subset A \lor_{ℋ} x \land A \lor_{ℋ} x \subseteq B) \to A \lor_{ℋ} x = B))$
13	12	reximdvai	$⊢ A ⋖_{ℋ} B \to (\exists x \in HAtoms (A \subset A \lor_{ℋ} x \land A \lor_{ℋ} x \subseteq B) \to \exists x \in HAtoms A \lor_{ℋ} x = B)$
14	6 13	mpd	$⊢ A ⋖_{ℋ} B \to \exists x \in HAtoms A \lor_{ℋ} x = B$