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

Metamath Proof Explorer

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 )