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}=\mathrm{ClSubSp}\left({W}\right)$
csscld.j ${⊢}{J}=\mathrm{TopOpen}\left({W}\right)$
Assertion csscld ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to {S}\in \mathrm{Clsd}\left({J}\right)$

Proof

Step Hyp Ref Expression
1 csscld.c ${⊢}{C}=\mathrm{ClSubSp}\left({W}\right)$
2 csscld.j ${⊢}{J}=\mathrm{TopOpen}\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{CPreHil}\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 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
9 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
10 eqid ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
11 6 8 9 10 3 ocvval ${⊢}\mathrm{ocv}\left({W}\right)\left({S}\right)\subseteq {\mathrm{Base}}_{{W}}\to \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left({S}\right)\right)=\left\{{x}\in {\mathrm{Base}}_{{W}}|\forall {y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
12 7 11 mp1i ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left({S}\right)\right)=\left\{{x}\in {\mathrm{Base}}_{{W}}|\forall {y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
13 riinrab ${⊢}{\mathrm{Base}}_{{W}}\cap \bigcap _{{y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)}\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}=\left\{{x}\in {\mathrm{Base}}_{{W}}|\forall {y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
14 12 13 syl6eqr ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to \mathrm{ocv}\left({W}\right)\left(\mathrm{ocv}\left({W}\right)\left({S}\right)\right)={\mathrm{Base}}_{{W}}\cap \bigcap _{{y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)}\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
15 cphnlm ${⊢}{W}\in \mathrm{CPreHil}\to {W}\in \mathrm{NrmMod}$
16 15 adantr ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to {W}\in \mathrm{NrmMod}$
17 nlmngp ${⊢}{W}\in \mathrm{NrmMod}\to {W}\in \mathrm{NrmGrp}$
18 ngptps ${⊢}{W}\in \mathrm{NrmGrp}\to {W}\in \mathrm{TopSp}$
19 16 17 18 3syl ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to {W}\in \mathrm{TopSp}$
20 6 2 istps ${⊢}{W}\in \mathrm{TopSp}↔{J}\in \mathrm{TopOn}\left({\mathrm{Base}}_{{W}}\right)$
21 19 20 sylib ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to {J}\in \mathrm{TopOn}\left({\mathrm{Base}}_{{W}}\right)$
22 toponuni ${⊢}{J}\in \mathrm{TopOn}\left({\mathrm{Base}}_{{W}}\right)\to {\mathrm{Base}}_{{W}}=\bigcup {J}$
23 21 22 syl ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to {\mathrm{Base}}_{{W}}=\bigcup {J}$
24 23 ineq1d ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to {\mathrm{Base}}_{{W}}\cap \bigcap _{{y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)}\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}=\bigcup {J}\cap \bigcap _{{y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)}\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
25 5 14 24 3eqtrd ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to {S}=\bigcup {J}\cap \bigcap _{{y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)}\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
26 topontop ${⊢}{J}\in \mathrm{TopOn}\left({\mathrm{Base}}_{{W}}\right)\to {J}\in \mathrm{Top}$
27 21 26 syl ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to {J}\in \mathrm{Top}$
28 7 sseli ${⊢}{y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)\to {y}\in {\mathrm{Base}}_{{W}}$
29 fvex ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}\in \mathrm{V}$
30 eqid ${⊢}\left({x}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)=\left({x}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)$
31 30 mptiniseg ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}\in \mathrm{V}\to {\left({x}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{-1}\left[\left\{{0}_{\mathrm{Scalar}\left({W}\right)}\right\}\right]=\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
32 29 31 ax-mp ${⊢}{\left({x}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{-1}\left[\left\{{0}_{\mathrm{Scalar}\left({W}\right)}\right\}\right]=\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
33 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
34 simpll ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to {W}\in \mathrm{CPreHil}$
35 21 adantr ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to {J}\in \mathrm{TopOn}\left({\mathrm{Base}}_{{W}}\right)$
36 35 cnmptid ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to \left({x}\in {\mathrm{Base}}_{{W}}⟼{x}\right)\in \left({J}\mathrm{Cn}{J}\right)$
37 simpr ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to {y}\in {\mathrm{Base}}_{{W}}$
38 35 35 37 cnmptc ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to \left({x}\in {\mathrm{Base}}_{{W}}⟼{y}\right)\in \left({J}\mathrm{Cn}{J}\right)$
39 2 33 8 34 35 36 38 cnmpt1ip ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to \left({x}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
40 33 cnfldhaus ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}$
41 cphclm ${⊢}{W}\in \mathrm{CPreHil}\to {W}\in \mathrm{CMod}$
42 9 clm0 ${⊢}{W}\in \mathrm{CMod}\to 0={0}_{\mathrm{Scalar}\left({W}\right)}$
43 41 42 syl ${⊢}{W}\in \mathrm{CPreHil}\to 0={0}_{\mathrm{Scalar}\left({W}\right)}$
44 43 ad2antrr ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to 0={0}_{\mathrm{Scalar}\left({W}\right)}$
45 0cn ${⊢}0\in ℂ$
46 44 45 syl6eqelr ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to {0}_{\mathrm{Scalar}\left({W}\right)}\in ℂ$
47 unicntop ${⊢}ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
48 47 sncld ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Haus}\wedge {0}_{\mathrm{Scalar}\left({W}\right)}\in ℂ\right)\to \left\{{0}_{\mathrm{Scalar}\left({W}\right)}\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
49 40 46 48 sylancr ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to \left\{{0}_{\mathrm{Scalar}\left({W}\right)}\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
50 cnclima ${⊢}\left(\left({x}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)\in \left({J}\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\wedge \left\{{0}_{\mathrm{Scalar}\left({W}\right)}\right\}\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)\to {\left({x}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{-1}\left[\left\{{0}_{\mathrm{Scalar}\left({W}\right)}\right\}\right]\in \mathrm{Clsd}\left({J}\right)$
51 39 49 50 syl2anc ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to {\left({x}\in {\mathrm{Base}}_{{W}}⟼{x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{-1}\left[\left\{{0}_{\mathrm{Scalar}\left({W}\right)}\right\}\right]\in \mathrm{Clsd}\left({J}\right)$
52 32 51 eqeltrrid ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to \left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}\in \mathrm{Clsd}\left({J}\right)$
53 28 52 sylan2 ${⊢}\left(\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\wedge {y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)\right)\to \left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}\in \mathrm{Clsd}\left({J}\right)$
54 53 ralrimiva ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to \forall {y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)\phantom{\rule{.4em}{0ex}}\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}\in \mathrm{Clsd}\left({J}\right)$
55 eqid ${⊢}\bigcup {J}=\bigcup {J}$
56 55 riincld ${⊢}\left({J}\in \mathrm{Top}\wedge \forall {y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)\phantom{\rule{.4em}{0ex}}\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}\in \mathrm{Clsd}\left({J}\right)\right)\to \bigcup {J}\cap \bigcap _{{y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)}\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}\in \mathrm{Clsd}\left({J}\right)$
57 27 54 56 syl2anc ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to \bigcup {J}\cap \bigcap _{{y}\in \mathrm{ocv}\left({W}\right)\left({S}\right)}\left\{{x}\in {\mathrm{Base}}_{{W}}|{x}{\cdot }_{𝑖}\left({W}\right){y}={0}_{\mathrm{Scalar}\left({W}\right)}\right\}\in \mathrm{Clsd}\left({J}\right)$
58 25 57 eqeltrd ${⊢}\left({W}\in \mathrm{CPreHil}\wedge {S}\in {C}\right)\to {S}\in \mathrm{Clsd}\left({J}\right)$