Theorem ocv0

Description: The orthocomplement of the empty 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)$$
Assertion	ocv0	$$⊢\underset{\dot{}}{\perp }\left(\varnothing \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		0ss	$$⊢\varnothing \subseteq V$$
4		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
5		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
6		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
7	1 4 5 6 2	ocvval	$$⊢\varnothing \subseteq V\to \underset{\dot{}}{\perp }\left(\varnothing \right)=\left\{x\in V|\forall y\in \varnothing x{\cdot }_{𝑖}\left(W\right)y=0_{\mathrm{Scalar}\left(W\right)}\right\}$$
8	3 7	ax-mp	$$⊢\underset{\dot{}}{\perp }\left(\varnothing \right)=\left\{x\in V|\forall y\in \varnothing x{\cdot }_{𝑖}\left(W\right)y=0_{\mathrm{Scalar}\left(W\right)}\right\}$$
9		ral0	$$⊢\forall y\in \varnothing x{\cdot }_{𝑖}\left(W\right)y=0_{\mathrm{Scalar}\left(W\right)}$$
10	9	rgenw	$$⊢\forall x\in V\forall y\in \varnothing x{\cdot }_{𝑖}\left(W\right)y=0_{\mathrm{Scalar}\left(W\right)}$$
11		rabid2	$$⊢V=\left\{x\in V|\forall y\in \varnothing x{\cdot }_{𝑖}\left(W\right)y=0_{\mathrm{Scalar}\left(W\right)}\right\}\leftrightarrow \forall x\in V\forall y\in \varnothing x{\cdot }_{𝑖}\left(W\right)y=0_{\mathrm{Scalar}\left(W\right)}$$
12	10 11	mpbir	$$⊢V=\left\{x\in V|\forall y\in \varnothing x{\cdot }_{𝑖}\left(W\right)y=0_{\mathrm{Scalar}\left(W\right)}\right\}$$
13	8 12	eqtr4i	$$⊢\underset{\dot{}}{\perp }\left(\varnothing \right)=V$$