Metamath Proof Explorer


Theorem cmslsschl

Description: A complete linear subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by AV, 8-Oct-2022)

Ref Expression
Hypotheses cmslsschl.x X = W 𝑠 U
cmslsschl.s S = LSubSp W
Assertion cmslsschl W ℂHil X CMetSp U S X ℂHil

Proof

Step Hyp Ref Expression
1 cmslsschl.x X = W 𝑠 U
2 cmslsschl.s S = LSubSp W
3 hlbn W ℂHil W Ban
4 bnnvc W Ban W NrmVec
5 3 4 syl W ℂHil W NrmVec
6 5 3ad2ant1 W ℂHil X CMetSp U S W NrmVec
7 eqid Scalar W = Scalar W
8 7 bnsca W Ban Scalar W CMetSp
9 3 8 syl W ℂHil Scalar W CMetSp
10 9 3ad2ant1 W ℂHil X CMetSp U S Scalar W CMetSp
11 3simpc W ℂHil X CMetSp U S X CMetSp U S
12 1 2 cmslssbn W NrmVec Scalar W CMetSp X CMetSp U S X Ban
13 6 10 11 12 syl21anc W ℂHil X CMetSp U S X Ban
14 hlcph W ℂHil W CPreHil
15 1 2 cphsscph W CPreHil U S X CPreHil
16 14 15 sylan W ℂHil U S X CPreHil
17 16 3adant2 W ℂHil X CMetSp U S X CPreHil
18 ishl X ℂHil X Ban X CPreHil
19 13 17 18 sylanbrc W ℂHil X CMetSp U S X ℂHil