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

Metamath Proof Explorer

Theorem chsupval

Description: The value of the supremum of a set of closed subspaces of Hilbert space. For an alternate version of the value, see chsupval2 . (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

		Ref	Expression
	Assertion	chsupval	$⊢ A \subseteq C_{ℋ} \to ⋁_{ℋ} (A) = ⊥ (⊥ (⋃ A))$

Proof

Step	Hyp	Ref	Expression
1		chsspwh	$⊢ C_{ℋ} \subseteq 𝒫 ℋ$
2		sstr2	$⊢ A \subseteq C_{ℋ} \to (C_{ℋ} \subseteq 𝒫 ℋ \to A \subseteq 𝒫 ℋ)$
3	1 2	mpi	$⊢ A \subseteq C_{ℋ} \to A \subseteq 𝒫 ℋ$
4		hsupval	$⊢ A \subseteq 𝒫 ℋ \to ⋁_{ℋ} (A) = ⊥ (⊥ (⋃ A))$
5	3 4	syl	$⊢ A \subseteq C_{ℋ} \to ⋁_{ℋ} (A) = ⊥ (⊥ (⋃ A))$