# Metamath Proof Explorer

## Theorem ocvocv

Description: A set is contained in its double orthocomplement. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ocvss.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
ocvss.o
Assertion ocvocv

### Proof

Step Hyp Ref Expression
1 ocvss.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 ocvss.o
3 1 2 ocvss
4 3 a1i
5 simpr ${⊢}\left({W}\in \mathrm{PreHil}\wedge {S}\subseteq {V}\right)\to {S}\subseteq {V}$
6 5 sselda ${⊢}\left(\left({W}\in \mathrm{PreHil}\wedge {S}\subseteq {V}\right)\wedge {x}\in {S}\right)\to {x}\in {V}$
7 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
8 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
9 eqid ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
10 1 7 8 9 2 ocvi
11 10 ancoms
16 8 7 1 9 iporthcom ${⊢}\left({W}\in \mathrm{PreHil}\wedge {y}\in {V}\wedge {x}\in {V}\right)\to \left({y}{\cdot }_{𝑖}\left({W}\right){x}={0}_{\mathrm{Scalar}\left({W}\right)}↔{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right)$