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

Metamath Proof Explorer

Theorem ocvcss

Description: The orthocomplement of any set is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses cssss.v ⊢ V = Base W
cssss.c ⊢ C = ClSubSp ⁡ W
ocvcss.o ⊢ ⊥ ˙ = ocv ⁡ W
Assertion ocvcss ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ S ∈ C

Proof

Step Hyp Ref Expression
1 cssss.v ⊢ V = Base W
2 cssss.c ⊢ C = ClSubSp ⁡ W
3 ocvcss.o ⊢ ⊥ ˙ = ocv ⁡ W
4 1 3 ocvocv ⊢ W ∈ PreHil ∧ S ⊆ V → S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
5 3 ocv2ss ⊢ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ S
6 4 5 syl ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ S
7 1 3 ocvss ⊢ ⊥ ˙ ⁡ S ⊆ V
8 7 a1i ⊢ S ⊆ V → ⊥ ˙ ⁡ S ⊆ V
9 1 2 3 iscss2 ⊢ W ∈ PreHil ∧ ⊥ ˙ ⁡ S ⊆ V → ⊥ ˙ ⁡ S ∈ C ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ S
10 8 9 sylan2 ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ S ∈ C ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ ⊥ ˙ ⁡ S
11 6 10 mpbird ⊢ W ∈ PreHil ∧ S ⊆ V → ⊥ ˙ ⁡ S ∈ C