Theorem ocv1

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

	Ref	Expression
Hypotheses	ocvz.v	$$⊢V={\mathrm{Base}}_W$$
	ocvz.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
	ocvz.z	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	ocv1	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{\perp }\left(V\right)=\left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ocvz.v	$$⊢V={\mathrm{Base}}_W$$
2		ocvz.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
3		ocvz.z	$$⊢\underset{\dot{}}{0}=0_W$$
4	1 2	ocvss	$$⊢\underset{\dot{}}{\perp }\left(V\right)\subseteq V$$
5		sseqin2	$$⊢\underset{\dot{}}{\perp }\left(V\right)\subseteq V\leftrightarrow V\cap \underset{\dot{}}{\perp }\left(V\right)=\underset{\dot{}}{\perp }\left(V\right)$$
6	4 5	mpbi	$$⊢V\cap \underset{\dot{}}{\perp }\left(V\right)=\underset{\dot{}}{\perp }\left(V\right)$$
7		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
8		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
9	1 8	lss1	$$⊢W\in \mathrm{LMod}\to V\in \mathrm{LSubSp}\left(W\right)$$
10	7 9	syl	$$⊢W\in \mathrm{PreHil}\to V\in \mathrm{LSubSp}\left(W\right)$$
11	2 8 3	ocvin	$$⊢\left(W\in \mathrm{PreHil}\wedge V\in \mathrm{LSubSp}\left(W\right)\right)\to V\cap \underset{\dot{}}{\perp }\left(V\right)=\left\{\underset{\dot{}}{0}\right\}$$
12	10 11	mpdan	$$⊢W\in \mathrm{PreHil}\to V\cap \underset{\dot{}}{\perp }\left(V\right)=\left\{\underset{\dot{}}{0}\right\}$$
13	6 12	syl5eqr	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{\perp }\left(V\right)=\left\{\underset{\dot{}}{0}\right\}$$