This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ V = Base W
ocvss.o ⊢ ⊥ ˙ = ocv ⁡ W
Assertion ocvss ⊢ ⊥ ˙ ⁡ S ⊆ V

Proof

Step Hyp Ref Expression
1 ocvss.v ⊢ V = Base W
2 ocvss.o ⊢ ⊥ ˙ = ocv ⁡ W
3 eqid ⊢ ⋅ 𝑖 ⁡ W = ⋅ 𝑖 ⁡ W
4 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
5 eqid ⊢ 0 Scalar ⁡ W = 0 Scalar ⁡ W
6 1 3 4 5 2 elocv ⊢ x ∈ ⊥ ˙ ⁡ S ↔ S ⊆ V ∧ x ∈ V ∧ ∀ y ∈ S x ⋅ 𝑖 ⁡ W y = 0 Scalar ⁡ W
7 6 simp2bi ⊢ x ∈ ⊥ ˙ ⁡ S → x ∈ V
8 7 ssriv ⊢ ⊥ ˙ ⁡ S ⊆ V