This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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