Metamath Proof Explorer

Theorem ocv1

Description: The orthocomplement of the base set. (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 ocv1 
|- ( W e. PreHil -> ( ._|_ ` V ) = { .0. } )

Proof

Step Hyp Ref Expression
1 ocvz.v 
 |-  V = ( Base ` W )
2 ocvz.o 
 |-  ._|_ = ( ocv ` W )
3 ocvz.z 
 |-  .0. = ( 0g ` W )
4 1 2 ocvss 
 |-  ( ._|_ ` V ) C_ V
5 sseqin2 
 |-  ( ( ._|_ ` V ) C_ V <-> ( V i^i ( ._|_ ` V ) ) = ( ._|_ ` V ) )
6 4 5 mpbi 
 |-  ( V i^i ( ._|_ ` V ) ) = ( ._|_ ` V )
7 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
8 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 1 8 lss1 
 |-  ( W e. LMod -> V e. ( LSubSp ` W ) )
10 7 9 syl 
 |-  ( W e. PreHil -> V e. ( LSubSp ` W ) )
11 2 8 3 ocvin 
 |-  ( ( W e. PreHil /\ V e. ( LSubSp ` W ) ) -> ( V i^i ( ._|_ ` V ) ) = { .0. } )
12 10 11 mpdan 
 |-  ( W e. PreHil -> ( V i^i ( ._|_ ` V ) ) = { .0. } )
13 6 12 eqtr3id 
 |-  ( W e. PreHil -> ( ._|_ ` V ) = { .0. } )