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={\mathrm{Base}}_W$$
	ocvfval.i	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	ocvfval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	ocvfval.z	$$⊢\underset{\dot{}}{0}=0_F$$
	ocvfval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
Assertion	ocvi	$$⊢\left(A\in \underset{\dot{}}{\perp }\left(S\right)\wedge B\in S\right)\to A\underset{\dot{}}{,}B=\underset{\dot{}}{0}$$

Proof

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