Theorem shsupcl

Description: Closure of the subspace supremum of set of subsets of Hilbert space. (Contributed by NM, 26-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shsupcl	$$⊢A\subseteq 𝒫\mathscr{H}\to \mathrm{span}\left(\bigcup A\right)\in {\mathbf{S}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		uniss	$$⊢A\subseteq 𝒫\mathscr{H}\to \bigcup A\subseteq \bigcup 𝒫\mathscr{H}$$
2		unipw	$$⊢\bigcup 𝒫\mathscr{H}=\mathscr{H}$$
3	1 2	sseqtrdi	$$⊢A\subseteq 𝒫\mathscr{H}\to \bigcup A\subseteq \mathscr{H}$$
4		spancl	$$⊢\bigcup A\subseteq \mathscr{H}\to \mathrm{span}\left(\bigcup A\right)\in {\mathbf{S}}_{\mathscr{H}}$$
5	3 4	syl	$$⊢A\subseteq 𝒫\mathscr{H}\to \mathrm{span}\left(\bigcup A\right)\in {\mathbf{S}}_{\mathscr{H}}$$