# Metamath Proof Explorer

## 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 ${⊢}{C}=\mathrm{ClSubSp}\left({W}\right)$
csslss.l ${⊢}{L}=\mathrm{LSubSp}\left({W}\right)$
Assertion csslss ${⊢}\left({W}\in \mathrm{PreHil}\wedge {S}\in {C}\right)\to {S}\in {L}$

### Proof

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