Metamath Proof Explorer


Theorem spanid

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

Ref Expression
Assertion spanid ( 𝐴S → ( span ‘ 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 shss ( 𝐴S𝐴 ⊆ ℋ )
2 spanval ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = { 𝑥S𝐴𝑥 } )
3 1 2 syl ( 𝐴S → ( span ‘ 𝐴 ) = { 𝑥S𝐴𝑥 } )
4 intmin ( 𝐴S { 𝑥S𝐴𝑥 } = 𝐴 )
5 3 4 eqtrd ( 𝐴S → ( span ‘ 𝐴 ) = 𝐴 )