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

Metamath Proof Explorer

Theorem ocv0

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

Ref Expression
Hypotheses ocvz.v 
|- V = ( Base ` W )
ocvz.o 
|- ._|_ = ( ocv ` W )
Assertion ocv0 
|- ( ._|_ ` (/) ) = V

Proof

Step Hyp Ref Expression
1 ocvz.v 
 |-  V = ( Base ` W )
2 ocvz.o 
 |-  ._|_ = ( ocv ` W )
3 0ss 
 |-  (/) C_ V
4 eqid 
 |-  ( .i ` W ) = ( .i ` W )
5 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
6 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
7 1 4 5 6 2 ocvval 
 |-  ( (/) C_ V -> ( ._|_ ` (/) ) = { x e. V | A. y e. (/) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } )
8 3 7 ax-mp 
 |-  ( ._|_ ` (/) ) = { x e. V | A. y e. (/) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) }
9 ral0 
 |-  A. y e. (/) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) )
10 9 rgenw 
 |-  A. x e. V A. y e. (/) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) )
11 rabid2 
 |-  ( V = { x e. V | A. y e. (/) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) } <-> A. x e. V A. y e. (/) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) )
12 10 11 mpbir 
 |-  V = { x e. V | A. y e. (/) ( x ( .i ` W ) y ) = ( 0g ` ( Scalar ` W ) ) }
13 8 12 eqtr4i 
 |-  ( ._|_ ` (/) ) = V