Metamath Proof Explorer


Theorem ocv1

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

Ref Expression
Hypotheses ocvz.v 𝑉 = ( Base ‘ 𝑊 )
ocvz.o = ( ocv ‘ 𝑊 )
ocvz.z 0 = ( 0g𝑊 )
Assertion ocv1 ( 𝑊 ∈ PreHil → ( 𝑉 ) = { 0 } )

Proof

Step Hyp Ref Expression
1 ocvz.v 𝑉 = ( Base ‘ 𝑊 )
2 ocvz.o = ( ocv ‘ 𝑊 )
3 ocvz.z 0 = ( 0g𝑊 )
4 1 2 ocvss ( 𝑉 ) ⊆ 𝑉
5 sseqin2 ( ( 𝑉 ) ⊆ 𝑉 ↔ ( 𝑉 ∩ ( 𝑉 ) ) = ( 𝑉 ) )
6 4 5 mpbi ( 𝑉 ∩ ( 𝑉 ) ) = ( 𝑉 )
7 phllmod ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
8 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
9 1 8 lss1 ( 𝑊 ∈ LMod → 𝑉 ∈ ( LSubSp ‘ 𝑊 ) )
10 7 9 syl ( 𝑊 ∈ PreHil → 𝑉 ∈ ( LSubSp ‘ 𝑊 ) )
11 2 8 3 ocvin ( ( 𝑊 ∈ PreHil ∧ 𝑉 ∈ ( LSubSp ‘ 𝑊 ) ) → ( 𝑉 ∩ ( 𝑉 ) ) = { 0 } )
12 10 11 mpdan ( 𝑊 ∈ PreHil → ( 𝑉 ∩ ( 𝑉 ) ) = { 0 } )
13 6 12 eqtr3id ( 𝑊 ∈ PreHil → ( 𝑉 ) = { 0 } )