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

Proof

Step	Hyp	Ref	Expression
1		cssss.v	$⊢ V = {Base}_{W}$
2		cssss.c	$⊢ C = ClSubSp (W)$
3		ocvcss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
4	3 2	iscss	$⊢ W \in PreHil \to (S \in C \leftrightarrow S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)))$
5	4	adantr	$⊢ (W \in PreHil \land S \subseteq V) \to (S \in C \leftrightarrow S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)))$
6	1 3	ocvocv	$⊢ (W \in PreHil \land S \subseteq V) \to S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
7		eqss	$⊢ S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \leftrightarrow (S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \land \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq S)$
8	7	baib	$⊢ S \subseteq \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to (S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq S)$
9	6 8	syl	$⊢ (W \in PreHil \land S \subseteq V) \to (S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq S)$
10	5 9	bitrd	$⊢ (W \in PreHil \land S \subseteq V) \to (S \in C \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq S)$