# Metamath Proof Explorer

## Theorem ocvin

Description: An orthocomplement has trivial intersection with the original subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses ocv2ss.o
ocvin.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
ocvin.z
Assertion ocvin

### Proof

Step Hyp Ref Expression
1 ocv2ss.o
2 ocvin.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
3 ocvin.z
4 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
5 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
6 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
7 eqid ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
8 4 5 6 7 1 ocvi
9 8 ancoms
11 simpll
12 4 2 lssel ${⊢}\left({S}\in {L}\wedge {x}\in {S}\right)\to {x}\in {\mathrm{Base}}_{{W}}$
14 6 5 4 7 3 ipeq0
15 11 13 14 syl2anc
16 10 15 mpbid
17 16 ex
18 elin
19 velsn
20 17 18 19 3imtr4g
21 20 ssrdv
22 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
23 4 2 lssss ${⊢}{S}\in {L}\to {S}\subseteq {\mathrm{Base}}_{{W}}$
24 4 1 2 ocvlss
25 23 24 sylan2
26 2 lssincl
27 22 26 syl3an1
28 25 27 mpd3an3
29 3 2 lss0ss
30 22 28 29 syl2an2r
31 21 30 eqssd