Theorem spanval

Description: Value of the linear span of a subset of Hilbert space. The span is the intersection of all subspaces constraining the subset. Definition of span in Schechter p. 276. (Contributed by NM, 2-Jun-2004) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	spanval	⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		df-span	⊢ span = ( 𝑦 ∈ 𝒫 ℋ ↦ ∩ { 𝑥 ∈ Sℋ ∣ 𝑦 ⊆ 𝑥 } )
2		sseq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 ) )
3	2	rabbidv	⊢ ( 𝑦 = 𝐴 → { 𝑥 ∈ Sℋ ∣ 𝑦 ⊆ 𝑥 } = { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
4	3	inteqd	⊢ ( 𝑦 = 𝐴 → ∩ { 𝑥 ∈ Sℋ ∣ 𝑦 ⊆ 𝑥 } = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )
5		ax-hilex	⊢ ℋ ∈ V
6	5	elpw2	⊢ ( 𝐴 ∈ 𝒫 ℋ ↔ 𝐴 ⊆ ℋ )
7	6	biimpri	⊢ ( 𝐴 ⊆ ℋ → 𝐴 ∈ 𝒫 ℋ )
8		helsh	⊢ ℋ ∈ Sℋ
9		sseq2	⊢ ( 𝑥 = ℋ → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ ℋ ) )
10	9	rspcev	⊢ ( ( ℋ ∈ Sℋ ∧ 𝐴 ⊆ ℋ ) → ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
11	8 10	mpan	⊢ ( 𝐴 ⊆ ℋ → ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 )
12		intexrab	⊢ ( ∃ 𝑥 ∈ Sℋ 𝐴 ⊆ 𝑥 ↔ ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ∈ V )
13	11 12	sylib	⊢ ( 𝐴 ⊆ ℋ → ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } ∈ V )
14	1 4 7 13	fvmptd3	⊢ ( 𝐴 ⊆ ℋ → ( span ‘ 𝐴 ) = ∩ { 𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥 } )