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

Metamath Proof Explorer

Theorem chjoi

Description: The join of a closed subspace and its orthocomplement. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	ch0le.1	$⊢ A \in C_{ℋ}$
	Assertion	chjoi	$⊢ A \lor_{ℋ} ⊥ (A) = ℋ$

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2	1	chssii	$⊢ A \subseteq ℋ$
3		ssjo	$⊢ A \subseteq ℋ \to A \lor_{ℋ} ⊥ (A) = ℋ$
4	2 3	ax-mp	$⊢ A \lor_{ℋ} ⊥ (A) = ℋ$