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

Metamath Proof Explorer

Theorem ocvi

Description: Property of a member of the orthocomplement of a subset. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ocvfval.v 
|- V = ( Base ` W )
ocvfval.i 
|- ., = ( .i ` W )
ocvfval.f 
|- F = ( Scalar ` W )
ocvfval.z 
|- .0. = ( 0g ` F )
ocvfval.o 
|- ._|_ = ( ocv ` W )
Assertion ocvi 
|- ( ( A e. ( ._|_ ` S ) /\ B e. S ) -> ( A ., B ) = .0. )

Proof

Step Hyp Ref Expression
1 ocvfval.v 
 |-  V = ( Base ` W )
2 ocvfval.i 
 |-  ., = ( .i ` W )
3 ocvfval.f 
 |-  F = ( Scalar ` W )
4 ocvfval.z 
 |-  .0. = ( 0g ` F )
5 ocvfval.o 
 |-  ._|_ = ( ocv ` W )
6 1 2 3 4 5 elocv 
 |-  ( A e. ( ._|_ ` S ) <-> ( S C_ V /\ A e. V /\ A. x e. S ( A ., x ) = .0. ) )
7 6 simp3bi 
 |-  ( A e. ( ._|_ ` S ) -> A. x e. S ( A ., x ) = .0. )
8 oveq2 
 |-  ( x = B -> ( A ., x ) = ( A ., B ) )
9 8 eqeq1d 
 |-  ( x = B -> ( ( A ., x ) = .0. <-> ( A ., B ) = .0. ) )
10 9 rspccva 
 |-  ( ( A. x e. S ( A ., x ) = .0. /\ B e. S ) -> ( A ., B ) = .0. )
11 7 10 sylan 
 |-  ( ( A e. ( ._|_ ` S ) /\ B e. S ) -> ( A ., B ) = .0. )