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

Metamath Proof Explorer

Theorem shlubi

Description: Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shlub.1	$⊢ A \in S_{ℋ}$
	shlub.2	$⊢ B \in S_{ℋ}$
	shlub.3	$⊢ C \in C_{ℋ}$
Assertion	shlubi	$⊢ (A \subseteq C \land B \subseteq C) \leftrightarrow A \lor_{ℋ} B \subseteq C$

Proof

Step	Hyp	Ref	Expression
1		shlub.1	$⊢ A \in S_{ℋ}$
2		shlub.2	$⊢ B \in S_{ℋ}$
3		shlub.3	$⊢ C \in C_{ℋ}$
4		shlub	$⊢ (A \in S_{ℋ} \land B \in S_{ℋ} \land C \in C_{ℋ}) \to ((A \subseteq C \land B \subseteq C) \leftrightarrow A \lor_{ℋ} B \subseteq C)$
5	1 2 3 4	mp3an	$⊢ (A \subseteq C \land B \subseteq C) \leftrightarrow A \lor_{ℋ} B \subseteq C$