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	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	ocvfval.f	$⊢ F = Scalar (W)$
	ocvfval.z	$⊢ \underset{˙}{0} = 0_{F}$
	ocvfval.o	$⊢ \underset{˙}{⊥} = ocv (W)$
Assertion	ocvi	$⊢ (A \in \underset{˙}{⊥} (S) \land B \in S) \to A \underset{˙}{,} B = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		ocvfval.v	$⊢ V = {Base}_{W}$
2		ocvfval.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
3		ocvfval.f	$⊢ F = Scalar (W)$
4		ocvfval.z	$⊢ \underset{˙}{0} = 0_{F}$
5		ocvfval.o	$⊢ \underset{˙}{⊥} = ocv (W)$
6	1 2 3 4 5	elocv	$⊢ A \in \underset{˙}{⊥} (S) \leftrightarrow (S \subseteq V \land A \in V \land \forall x \in S A \underset{˙}{,} x = \underset{˙}{0})$
7	6	simp3bi	$⊢ A \in \underset{˙}{⊥} (S) \to \forall x \in S A \underset{˙}{,} x = \underset{˙}{0}$
8		oveq2	$⊢ x = B \to A \underset{˙}{,} x = A \underset{˙}{,} B$
9	8	eqeq1d	$⊢ x = B \to (A \underset{˙}{,} x = \underset{˙}{0} \leftrightarrow A \underset{˙}{,} B = \underset{˙}{0})$
10	9	rspccva	$⊢ (\forall x \in S A \underset{˙}{,} x = \underset{˙}{0} \land B \in S) \to A \underset{˙}{,} B = \underset{˙}{0}$
11	7 10	sylan	$⊢ (A \in \underset{˙}{⊥} (S) \land B \in S) \to A \underset{˙}{,} B = \underset{˙}{0}$

Metamath Proof Explorer