Metamath Proof Explorer

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 C_ ~P ~H -> ( span ` U. A ) e. SH )

Proof

Step Hyp Ref Expression
1 uniss 
 |-  ( A C_ ~P ~H -> U. A C_ U. ~P ~H )
2 unipw 
 |-  U. ~P ~H = ~H
3 1 2 sseqtrdi 
 |-  ( A C_ ~P ~H -> U. A C_ ~H )
4 spancl 
 |-  ( U. A C_ ~H -> ( span ` U. A ) e. SH )
5 3 4 syl 
 |-  ( A C_ ~P ~H -> ( span ` U. A ) e. SH )