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 𝐶 = ( 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 ∧ 𝑆𝐶 ) → 𝑆𝐿 )