Theorem obs2ocv

Description: The double orthocomplement (closure) of an orthonormal basis is the whole space. (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	obs2ocv.o	|- ._|_ = ( ocv ` W )
	obs2ocv.v	|- V = ( Base ` W )
Assertion	obs2ocv	|- ( B e. ( OBasis ` W ) -> ( ._|_ ` ( ._|_ ` B ) ) = V )

Proof

Step	Hyp	Ref	Expression
1		obs2ocv.o	|- ._|_ = ( ocv ` W )
2		obs2ocv.v	|- V = ( Base ` W )
3		eqid	|- ( 0g ` W ) = ( 0g ` W )
4	3 1	obsocv	|- ( B e. ( OBasis ` W ) -> ( ._|_ ` B ) = { ( 0g ` W ) } )
5	4	fveq2d	|- ( B e. ( OBasis ` W ) -> ( ._|_ ` ( ._|_ ` B ) ) = ( ._|_ ` { ( 0g ` W ) } ) )
6		obsrcl	|- ( B e. ( OBasis ` W ) -> W e. PreHil )
7	2 1 3	ocvz	|- ( W e. PreHil -> ( ._|_ ` { ( 0g ` W ) } ) = V )
8	6 7	syl	|- ( B e. ( OBasis ` W ) -> ( ._|_ ` { ( 0g ` W ) } ) = V )
9	5 8	eqtrd	|- ( B e. ( OBasis ` W ) -> ( ._|_ ` ( ._|_ ` B ) ) = V )