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	syl5bir	|- ( ( 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 } ) )