Theorem ocvz

Description: The orthocomplement of the zero subspace. (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	ocvz.v	|- V = ( Base ` W )
	ocvz.o	|- ._|_ = ( ocv ` W )
	ocvz.z	|- .0. = ( 0g ` W )
Assertion	ocvz	|- ( W e. PreHil -> ( ._|_ ` { .0. } ) = V )

Proof

Step	Hyp	Ref	Expression
1		ocvz.v	|- V = ( Base ` W )
2		ocvz.o	|- ._|_ = ( ocv ` W )
3		ocvz.z	|- .0. = ( 0g ` W )
4		phllmod	|- ( W e. PreHil -> W e. LMod )
5		eqid	|- ( LSpan ` W ) = ( LSpan ` W )
6	3 5	lsp0	|- ( W e. LMod -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
7	4 6	syl	|- ( W e. PreHil -> ( ( LSpan ` W ) ` (/) ) = { .0. } )
8	7	fveq2d	|- ( W e. PreHil -> ( ._|_ ` ( ( LSpan ` W ) ` (/) ) ) = ( ._|_ ` { .0. } ) )
9		0ss	|- (/) C_ V
10	1 2 5	ocvlsp	|- ( ( W e. PreHil /\ (/) C_ V ) -> ( ._|_ ` ( ( LSpan ` W ) ` (/) ) ) = ( ._|_ ` (/) ) )
11	9 10	mpan2	|- ( W e. PreHil -> ( ._|_ ` ( ( LSpan ` W ) ` (/) ) ) = ( ._|_ ` (/) ) )
12	1 2	ocv0	|- ( ._|_ ` (/) ) = V
13	11 12	eqtrdi	|- ( W e. PreHil -> ( ._|_ ` ( ( LSpan ` W ) ` (/) ) ) = V )
14	8 13	eqtr3d	|- ( W e. PreHil -> ( ._|_ ` { .0. } ) = V )