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