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 ) )