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

Metamath Proof Explorer

Theorem spansni

Description: The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 3-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis spansn.1 
|- A e. ~H
Assertion spansni 
|- ( span ` { A } ) = ( _|_ ` ( _|_ ` { A } ) )

Proof

Step Hyp Ref Expression
1 spansn.1 
 |-  A e. ~H
2 snssi 
 |-  ( A e. ~H -> { A } C_ ~H )
3 spanssoc 
 |-  ( { A } C_ ~H -> ( span ` { A } ) C_ ( _|_ ` ( _|_ ` { A } ) ) )
4 1 2 3 mp2b 
 |-  ( span ` { A } ) C_ ( _|_ ` ( _|_ ` { A } ) )
5 1 elexi 
 |-  A e. _V
6 5 snss 
 |-  ( A e. y <-> { A } C_ y )
7 shmulcl 
 |-  ( ( y e. SH /\ z e. CC /\ A e. y ) -> ( z .h A ) e. y )
8 7 3expia 
 |-  ( ( y e. SH /\ z e. CC ) -> ( A e. y -> ( z .h A ) e. y ) )
9 8 ancoms 
 |-  ( ( z e. CC /\ y e. SH ) -> ( A e. y -> ( z .h A ) e. y ) )
10 6 9 biimtrrid 
 |-  ( ( z e. CC /\ y e. SH ) -> ( { A } C_ y -> ( z .h A ) e. y ) )
11 eleq1 
 |-  ( x = ( z .h A ) -> ( x e. y <-> ( z .h A ) e. y ) )
12 11 imbi2d 
 |-  ( x = ( z .h A ) -> ( ( { A } C_ y -> x e. y ) <-> ( { A } C_ y -> ( z .h A ) e. y ) ) )
13 10 12 syl5ibrcom 
 |-  ( ( z e. CC /\ y e. SH ) -> ( x = ( z .h A ) -> ( { A } C_ y -> x e. y ) ) )
14 13 ralrimdva 
 |-  ( z e. CC -> ( x = ( z .h A ) -> A. y e. SH ( { A } C_ y -> x e. y ) ) )
15 14 rexlimiv 
 |-  ( E. z e. CC x = ( z .h A ) -> A. y e. SH ( { A } C_ y -> x e. y ) )
16 1 h1de2ci 
 |-  ( x e. ( _|_ ` ( _|_ ` { A } ) ) <-> E. z e. CC x = ( z .h A ) )
17 vex 
 |-  x e. _V
18 17 elspani 
 |-  ( { A } C_ ~H -> ( x e. ( span ` { A } ) <-> A. y e. SH ( { A } C_ y -> x e. y ) ) )
19 1 2 18 mp2b 
 |-  ( x e. ( span ` { A } ) <-> A. y e. SH ( { A } C_ y -> x e. y ) )
20 15 16 19 3imtr4i 
 |-  ( x e. ( _|_ ` ( _|_ ` { A } ) ) -> x e. ( span ` { A } ) )
21 20 ssriv 
 |-  ( _|_ ` ( _|_ ` { A } ) ) C_ ( span ` { A } )
22 4 21 eqssi 
 |-  ( span ` { A } ) = ( _|_ ` ( _|_ ` { A } ) )