Metamath Proof Explorer


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 A span A = x S | A x

Proof

Step Hyp Ref Expression
1 df-span span = y 𝒫 x S | y x
2 sseq1 y = A y x A x
3 2 rabbidv y = A x S | y x = x S | A x
4 3 inteqd y = A x S | y x = x S | A x
5 ax-hilex V
6 5 elpw2 A 𝒫 A
7 6 biimpri A A 𝒫
8 helsh S
9 sseq2 x = A x A
10 9 rspcev S A x S A x
11 8 10 mpan A x S A x
12 intexrab x S A x x S | A x V
13 11 12 sylib A x S | A x V
14 1 4 7 13 fvmptd3 A span A = x S | A x