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 ‘ 𝐴 ) = 𝐴 )