Metamath Proof Explorer


Theorem csscld

Description: A "closed subspace" in a subcomplex pre-Hilbert space is actually closed in the topology induced by the norm, thus justifying the terminology "closed subspace". (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses csscld.c C = ClSubSp W
csscld.j J = TopOpen W
Assertion csscld W CPreHil S C S Clsd J

Proof

Step Hyp Ref Expression
1 csscld.c C = ClSubSp W
2 csscld.j J = TopOpen W
3 eqid ocv W = ocv W
4 3 1 cssi S C S = ocv W ocv W S
5 4 adantl W CPreHil S C S = ocv W ocv W S
6 eqid Base W = Base W
7 6 3 ocvss ocv W S Base W
8 eqid 𝑖 W = 𝑖 W
9 eqid Scalar W = Scalar W
10 eqid 0 Scalar W = 0 Scalar W
11 6 8 9 10 3 ocvval ocv W S Base W ocv W ocv W S = x Base W | y ocv W S x 𝑖 W y = 0 Scalar W
12 7 11 mp1i W CPreHil S C ocv W ocv W S = x Base W | y ocv W S x 𝑖 W y = 0 Scalar W
13 riinrab Base W y ocv W S x Base W | x 𝑖 W y = 0 Scalar W = x Base W | y ocv W S x 𝑖 W y = 0 Scalar W
14 12 13 eqtr4di W CPreHil S C ocv W ocv W S = Base W y ocv W S x Base W | x 𝑖 W y = 0 Scalar W
15 cphnlm W CPreHil W NrmMod
16 15 adantr W CPreHil S C W NrmMod
17 nlmngp W NrmMod W NrmGrp
18 ngptps W NrmGrp W TopSp
19 16 17 18 3syl W CPreHil S C W TopSp
20 6 2 istps W TopSp J TopOn Base W
21 19 20 sylib W CPreHil S C J TopOn Base W
22 toponuni J TopOn Base W Base W = J
23 21 22 syl W CPreHil S C Base W = J
24 23 ineq1d W CPreHil S C Base W y ocv W S x Base W | x 𝑖 W y = 0 Scalar W = J y ocv W S x Base W | x 𝑖 W y = 0 Scalar W
25 5 14 24 3eqtrd W CPreHil S C S = J y ocv W S x Base W | x 𝑖 W y = 0 Scalar W
26 topontop J TopOn Base W J Top
27 21 26 syl W CPreHil S C J Top
28 7 sseli y ocv W S y Base W
29 fvex 0 Scalar W V
30 eqid x Base W x 𝑖 W y = x Base W x 𝑖 W y
31 30 mptiniseg 0 Scalar W V x Base W x 𝑖 W y -1 0 Scalar W = x Base W | x 𝑖 W y = 0 Scalar W
32 29 31 ax-mp x Base W x 𝑖 W y -1 0 Scalar W = x Base W | x 𝑖 W y = 0 Scalar W
33 eqid TopOpen fld = TopOpen fld
34 simpll W CPreHil S C y Base W W CPreHil
35 21 adantr W CPreHil S C y Base W J TopOn Base W
36 35 cnmptid W CPreHil S C y Base W x Base W x J Cn J
37 simpr W CPreHil S C y Base W y Base W
38 35 35 37 cnmptc W CPreHil S C y Base W x Base W y J Cn J
39 2 33 8 34 35 36 38 cnmpt1ip W CPreHil S C y Base W x Base W x 𝑖 W y J Cn TopOpen fld
40 33 cnfldhaus TopOpen fld Haus
41 cphclm W CPreHil W CMod
42 9 clm0 W CMod 0 = 0 Scalar W
43 41 42 syl W CPreHil 0 = 0 Scalar W
44 43 ad2antrr W CPreHil S C y Base W 0 = 0 Scalar W
45 0cn 0
46 44 45 eqeltrrdi W CPreHil S C y Base W 0 Scalar W
47 unicntop = TopOpen fld
48 47 sncld TopOpen fld Haus 0 Scalar W 0 Scalar W Clsd TopOpen fld
49 40 46 48 sylancr W CPreHil S C y Base W 0 Scalar W Clsd TopOpen fld
50 cnclima x Base W x 𝑖 W y J Cn TopOpen fld 0 Scalar W Clsd TopOpen fld x Base W x 𝑖 W y -1 0 Scalar W Clsd J
51 39 49 50 syl2anc W CPreHil S C y Base W x Base W x 𝑖 W y -1 0 Scalar W Clsd J
52 32 51 eqeltrrid W CPreHil S C y Base W x Base W | x 𝑖 W y = 0 Scalar W Clsd J
53 28 52 sylan2 W CPreHil S C y ocv W S x Base W | x 𝑖 W y = 0 Scalar W Clsd J
54 53 ralrimiva W CPreHil S C y ocv W S x Base W | x 𝑖 W y = 0 Scalar W Clsd J
55 eqid J = J
56 55 riincld J Top y ocv W S x Base W | x 𝑖 W y = 0 Scalar W Clsd J J y ocv W S x Base W | x 𝑖 W y = 0 Scalar W Clsd J
57 27 54 56 syl2anc W CPreHil S C J y ocv W S x Base W | x 𝑖 W y = 0 Scalar W Clsd J
58 25 57 eqeltrd W CPreHil S C S Clsd J