Metamath Proof Explorer

Theorem iscss2

Description: It is sufficient to prove that the double orthocomplement is a subset of the target set to show that the 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 iscss2 ⊢ W ∈ PreHil ∧ S ⊆ V → S ∈ C ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ S

Proof

Step Hyp Ref Expression
1 cssss.v ⊢ V = Base W
2 cssss.c ⊢ C = ClSubSp ⁡ W
3 ocvcss.o ⊢ ⊥ ˙ = ocv ⁡ W
4 3 2 iscss ⊢ W ∈ PreHil → S ∈ C ↔ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
5 4 adantr ⊢ W ∈ PreHil ∧ S ⊆ V → S ∈ C ↔ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
6 1 3 ocvocv ⊢ W ∈ PreHil ∧ S ⊆ V → S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S
7 eqss ⊢ S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ↔ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ S
8 7 baib ⊢ S ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S → S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ S
9 6 8 syl ⊢ W ∈ PreHil ∧ S ⊆ V → S = ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ S
10 5 9 bitrd ⊢ W ∈ PreHil ∧ S ⊆ V → S ∈ C ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ S ⊆ S