Theorem csslss

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

	Ref	Expression
Hypotheses	csslss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
	csslss.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
Assertion	csslss	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ∈ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		csslss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
2		csslss.l	⊢ 𝐿 = ( LSubSp ‘ 𝑊 )
3		eqid	⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
4	3 1	cssi	⊢ ( 𝑆 ∈ 𝐶 → 𝑆 = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) )
5	4	adantl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑆 = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) )
6		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7	6 3	ocvss	⊢ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝑊 )
8	7	a1i	⊢ ( 𝑆 ∈ 𝐶 → ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝑊 ) )
9	6 3 2	ocvlss	⊢ ( ( 𝑊 ∈ PreHil ∧ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝑊 ) ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) ∈ 𝐿 )
10	8 9	sylan2	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐶 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) ∈ 𝐿 )
11	5 10	eqeltrd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ∈ 𝐿 )