Metamath Proof Explorer

Theorem spanss2

Description: A subset of Hilbert space is included in its span. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion spanss2 
|- ( A C_ ~H -> A C_ ( span ` A ) )

Proof

Step Hyp Ref Expression
1 ssintub 
 |-  A C_ |^| { x e. SH | A C_ x }
2 spanval 
 |-  ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )
3 1 2 sseqtrrid 
 |-  ( A C_ ~H -> A C_ ( span ` A ) )