Theorem ocvz

Description: The orthocomplement of the zero subspace. (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	ocvz	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{\perp }\left(\left\{\underset{\dot{}}{0}\right\}\right)=V$$

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		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
5		eqid	$$⊢\mathrm{LSpan}\left(W\right)=\mathrm{LSpan}\left(W\right)$$
6	3 5	lsp0	$$⊢W\in \mathrm{LMod}\to \mathrm{LSpan}\left(W\right)\left(\varnothing \right)=\left\{\underset{\dot{}}{0}\right\}$$
7	4 6	syl	$$⊢W\in \mathrm{PreHil}\to \mathrm{LSpan}\left(W\right)\left(\varnothing \right)=\left\{\underset{\dot{}}{0}\right\}$$
8	7	fveq2d	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(W\right)\left(\varnothing \right)\right)=\underset{\dot{}}{\perp }\left(\left\{\underset{\dot{}}{0}\right\}\right)$$
9		0ss	$$⊢\varnothing \subseteq V$$
10	1 2 5	ocvlsp	$$⊢\left(W\in \mathrm{PreHil}\wedge \varnothing \subseteq V\right)\to \underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(W\right)\left(\varnothing \right)\right)=\underset{\dot{}}{\perp }\left(\varnothing \right)$$
11	9 10	mpan2	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(W\right)\left(\varnothing \right)\right)=\underset{\dot{}}{\perp }\left(\varnothing \right)$$
12	1 2	ocv0	$$⊢\underset{\dot{}}{\perp }\left(\varnothing \right)=V$$
13	11 12	eqtrdi	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{\perp }\left(\mathrm{LSpan}\left(W\right)\left(\varnothing \right)\right)=V$$
14	8 13	eqtr3d	$$⊢W\in \mathrm{PreHil}\to \underset{\dot{}}{\perp }\left(\left\{\underset{\dot{}}{0}\right\}\right)=V$$