Metamath Proof Explorer


Theorem ocvss

Description: The orthocomplement of a subset is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ocvss.v 𝑉 = ( Base ‘ 𝑊 )
ocvss.o = ( ocv ‘ 𝑊 )
Assertion ocvss ( 𝑆 ) ⊆ 𝑉

Proof

Step Hyp Ref Expression
1 ocvss.v 𝑉 = ( Base ‘ 𝑊 )
2 ocvss.o = ( ocv ‘ 𝑊 )
3 eqid ( ·𝑖𝑊 ) = ( ·𝑖𝑊 )
4 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5 eqid ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
6 1 3 4 5 2 elocv ( 𝑥 ∈ ( 𝑆 ) ↔ ( 𝑆𝑉𝑥𝑉 ∧ ∀ 𝑦𝑆 ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
7 6 simp2bi ( 𝑥 ∈ ( 𝑆 ) → 𝑥𝑉 )
8 7 ssriv ( 𝑆 ) ⊆ 𝑉