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. } )