# Metamath Proof Explorer

## 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
Assertion ocv0

### Proof

Step Hyp Ref Expression
1 ocvz.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 ocvz.o
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
8 3 7 ax-mp
9 ral0 ${⊢}\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}$
10 9 rgenw ${⊢}\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}$
11 rabid2 ${⊢}{V}=\left\{{x}\in {V}|\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}↔\forall {x}\in {V}\phantom{\rule{.4em}{0ex}}\forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}{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 \phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
13 8 12 eqtr4i