Metamath Proof Explorer

Theorem iscss

Description: The predicate "is a closed subspace" (of a pre-Hilbert space). (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 13-Oct-2015)

		Ref	Expression
	Hypotheses	cssval.o	$⊢ \underset{˙}{⊥} = ocv (W)$
		cssval.c	$⊢ C = ClSubSp (W)$
	Assertion	iscss	$⊢ W \in X \to (S \in C \leftrightarrow S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)))$

Proof

Step	Hyp	Ref	Expression
1		cssval.o	$⊢ \underset{˙}{⊥} = ocv (W)$
2		cssval.c	$⊢ C = ClSubSp (W)$
3	1 2	cssval	$⊢ W \in X \to C = \{s \| s = \underset{˙}{⊥} (\underset{˙}{⊥} (s))\}$
4	3	eleq2d	$⊢ W \in X \to (S \in C \leftrightarrow S \in \{s \| s = \underset{˙}{⊥} (\underset{˙}{⊥} (s))\})$
5		id	$⊢ S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to S = \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
6		fvex	$⊢ \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \in V$
7	5 6	eqeltrdi	$⊢ S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to S \in V$
8		id	$⊢ s = S \to s = S$
9		2fveq3	$⊢ s = S \to \underset{˙}{⊥} (\underset{˙}{⊥} (s)) = \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
10	8 9	eqeq12d	$⊢ s = S \to (s = \underset{˙}{⊥} (\underset{˙}{⊥} (s)) \leftrightarrow S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)))$
11	7 10	elab3	$⊢ S \in \{s \| s = \underset{˙}{⊥} (\underset{˙}{⊥} (s))\} \leftrightarrow S = \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
12	4 11	bitrdi	$⊢ W \in X \to (S \in C \leftrightarrow S = \underset{˙}{⊥} (\underset{˙}{⊥} (S)))$