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	⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) ∈ Sℋ )

Proof

Step	Hyp	Ref	Expression
1		spanval	⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
2		ssrab2	⊢ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ Sℋ
3		helsh	⊢ ℋ ∈ Sℋ
4		sseq2	⊢ ( 𝑥 = ℋ → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ℋ ) )
5	4	rspcev	⊢ ( ( ℋ ∈ Sℋ ∧ 𝐴 ⊆ ℋ ) → ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
6	3 5	mpan	⊢ ( 𝐴 ⊆ ℋ → ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
7		rabn0	⊢ ( { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ≠ ∅ ↔ ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
8	6 7	sylibr	⊢ ( 𝐴 ⊆ ℋ → { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ≠ ∅ )
9		shintcl	⊢ ( ( { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ⊆ Sℋ ∧ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ≠ ∅ ) → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ∈ Sℋ )
10	2 8 9	sylancr	⊢ ( 𝐴 ⊆ ℋ → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ∈ Sℋ )
11	1 10	eqeltrd	⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) ∈ Sℋ )