Metamath Proof Explorer


Theorem ocvz

Description: The orthocomplement of the zero subspace. (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 ocvz W PreHil ˙ 0 ˙ = V

Proof

Step Hyp Ref Expression
1 ocvz.v V = Base W
2 ocvz.o ˙ = ocv W
3 ocvz.z 0 ˙ = 0 W
4 phllmod W PreHil W LMod
5 eqid LSpan W = LSpan W
6 3 5 lsp0 W LMod LSpan W = 0 ˙
7 4 6 syl W PreHil LSpan W = 0 ˙
8 7 fveq2d W PreHil ˙ LSpan W = ˙ 0 ˙
9 0ss V
10 1 2 5 ocvlsp W PreHil V ˙ LSpan W = ˙
11 9 10 mpan2 W PreHil ˙ LSpan W = ˙
12 1 2 ocv0 ˙ = V
13 11 12 eqtrdi W PreHil ˙ LSpan W = V
14 8 13 eqtr3d W PreHil ˙ 0 ˙ = V