Metamath Proof Explorer


Theorem ocv1

Description: The orthocomplement of the base set. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypotheses ocvz.v V = Base W
ocvz.o ˙ = ocv W
ocvz.z 0 ˙ = 0 W
Assertion ocv1 W PreHil ˙ V = 0 ˙

Proof

Step Hyp Ref Expression
1 ocvz.v V = Base W
2 ocvz.o ˙ = ocv W
3 ocvz.z 0 ˙ = 0 W
4 1 2 ocvss ˙ V V
5 sseqin2 ˙ V V V ˙ V = ˙ V
6 4 5 mpbi V ˙ V = ˙ V
7 phllmod W PreHil W LMod
8 eqid LSubSp W = LSubSp W
9 1 8 lss1 W LMod V LSubSp W
10 7 9 syl W PreHil V LSubSp W
11 2 8 3 ocvin W PreHil V LSubSp W V ˙ V = 0 ˙
12 10 11 mpdan W PreHil V ˙ V = 0 ˙
13 6 12 eqtr3id W PreHil ˙ V = 0 ˙