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	$⊢ \underset{˙}{⊥} = ocv (W)$
Assertion	ocvcss	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (S) \in C$

Step	Hyp	Ref	Expression
1		cssss.v	$⊢ V = {Base}_{W}$
2		cssss.c	$⊢ C = ClSubSp (W)$
3		ocvcss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
4	1 3	ocvocv	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
5	3	ocv2ss	$⊢ S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (S))) \subseteq \underset{˙}{⊥} (S)$
6	4 5	syl	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (S))) \subseteq \underset{˙}{⊥} (S)$
7	1 3	ocvss	$⊢ \underset{˙}{⊥} (S) \subseteq V$
8	7	a1i	$⊢ S \subseteq V \to \underset{˙}{⊥} (S) \subseteq V$
9	1 2 3	iscss2	$⊢ (W \in PreHil \land \underset{˙}{⊥} (S) \subseteq V) \to (\underset{˙}{⊥} (S) \in C \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (S))) \subseteq \underset{˙}{⊥} (S))$
10	8 9	sylan2	$⊢ (W \in PreHil \land S \subseteq V) \to (\underset{˙}{⊥} (S) \in C \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (\underset{˙}{⊥} (S))) \subseteq \underset{˙}{⊥} (S))$
11	6 10	mpbird	$⊢ (W \in PreHil \land S \subseteq V) \to \underset{˙}{⊥} (S) \in C$

Metamath Proof Explorer