csslss

Description: A closed subspace of a pre-Hilbert space is a linear subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

Step	Hyp	Ref	Expression
1		csslss.c	$⊢ C = ClSubSp (W)$
2		csslss.l	$⊢ L = LSubSp (W)$
3		eqid	$⊢ ocv (W) = ocv (W)$
4	3 1	cssi	$⊢ S \in C \to S = ocv (W) (ocv (W) (S))$
5	4	adantl	$⊢ (W \in PreHil \land S \in C) \to S = ocv (W) (ocv (W) (S))$
6		eqid	$⊢ {Base}_{W} = {Base}_{W}$
7	6 3	ocvss	$⊢ ocv (W) (S) \subseteq {Base}_{W}$
8	7	a1i	$⊢ S \in C \to ocv (W) (S) \subseteq {Base}_{W}$
9	6 3 2	ocvlss	$⊢ (W \in PreHil \land ocv (W) (S) \subseteq {Base}_{W}) \to ocv (W) (ocv (W) (S)) \in L$
10	8 9	sylan2	$⊢ (W \in PreHil \land S \in C) \to ocv (W) (ocv (W) (S)) \in L$
11	5 10	eqeltrd	$⊢ (W \in PreHil \land S \in C) \to S \in L$

Metamath Proof Explorer