This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )

Proof

Step Hyp Ref Expression
1 df-span 
 |-  span = ( y e. ~P ~H |-> |^| { x e. SH | y C_ x } )
2 sseq1 
 |-  ( y = A -> ( y C_ x <-> A C_ x ) )
3 2 rabbidv 
 |-  ( y = A -> { x e. SH | y C_ x } = { x e. SH | A C_ x } )
4 3 inteqd 
 |-  ( y = A -> |^| { x e. SH | y C_ x } = |^| { x e. SH | A C_ x } )
5 ax-hilex 
 |-  ~H e. _V
6 5 elpw2 
 |-  ( A e. ~P ~H <-> A C_ ~H )
7 6 biimpri 
 |-  ( A C_ ~H -> A e. ~P ~H )
8 helsh 
 |-  ~H e. SH
9 sseq2 
 |-  ( x = ~H -> ( A C_ x <-> A C_ ~H ) )
10 9 rspcev 
 |-  ( ( ~H e. SH /\ A C_ ~H ) -> E. x e. SH A C_ x )
11 8 10 mpan 
 |-  ( A C_ ~H -> E. x e. SH A C_ x )
12 intexrab 
 |-  ( E. x e. SH A C_ x <-> |^| { x e. SH | A C_ x } e. _V )
13 11 12 sylib 
 |-  ( A C_ ~H -> |^| { x e. SH | A C_ x } e. _V )
14 1 4 7 13 fvmptd3 
 |-  ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } )