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

Metamath Proof Explorer

Theorem spancl

Description: The span of a subset of Hilbert space is a subspace. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spancl 
|- ( A C_ ~H -> ( span ` A ) e. SH )

Proof

Step Hyp Ref Expression
1 spanval 
 |-  ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )
2 ssrab2 
 |-  { x e. SH | A C_ x } C_ SH
3 helsh 
 |-  ~H e. SH
4 sseq2 
 |-  ( x = ~H -> ( A C_ x <-> A C_ ~H ) )
5 4 rspcev 
 |-  ( ( ~H e. SH /\ A C_ ~H ) -> E. x e. SH A C_ x )
6 3 5 mpan 
 |-  ( A C_ ~H -> E. x e. SH A C_ x )
7 rabn0 
 |-  ( { x e. SH | A C_ x } =/= (/) <-> E. x e. SH A C_ x )
8 6 7 sylibr 
 |-  ( A C_ ~H -> { x e. SH | A C_ x } =/= (/) )
9 shintcl 
 |-  ( ( { x e. SH | A C_ x } C_ SH /\ { x e. SH | A C_ x } =/= (/) ) -> |^| { x e. SH | A C_ x } e. SH )
10 2 8 9 sylancr 
 |-  ( A C_ ~H -> |^| { x e. SH | A C_ x } e. SH )
11 1 10 eqeltrd 
 |-  ( A C_ ~H -> ( span ` A ) e. SH )