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 ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
csscld.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
Assertion csscld ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 csscld.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
2 csscld.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
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 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
9 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
10 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
11 6 8 9 10 3 ocvval ⊢ ( ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ⊆ ( Base ‘ 𝑊 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) = { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ∀ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
12 7 11 mp1i ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) = { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ∀ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
13 riinrab ⊢ ( ( Base ‘ 𝑊 ) ∩ ∩ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ∀ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) }
14 12 13 eqtr4di ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) = ( ( Base ‘ 𝑊 ) ∩ ∩ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
15 cphnlm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmMod )
16 15 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑊 ∈ NrmMod )
17 nlmngp ⊢ ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
18 ngptps ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ TopSp )
19 16 17 18 3syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑊 ∈ TopSp )
20 6 2 istps ⊢ ( 𝑊 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
21 19 20 sylib ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
22 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) → ( Base ‘ 𝑊 ) = ∪ 𝐽 )
23 21 22 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → ( Base ‘ 𝑊 ) = ∪ 𝐽 )
24 23 ineq1d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → ( ( Base ‘ 𝑊 ) ∩ ∩ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = ( ∪ 𝐽 ∩ ∩ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
25 5 14 24 3eqtrd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑆 = ( ∪ 𝐽 ∩ ∩ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
26 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) → 𝐽 ∈ Top )
27 21 26 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → 𝐽 ∈ Top )
28 7 sseli ⊢ ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
29 fvex ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ V
30 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) )
31 30 mptiniseg ⊢ ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ V → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) “ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
32 29 31 ax-mp ⊢ ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) “ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) = { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) }
33 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
34 simpll ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 𝑊 ∈ ℂPreHil )
35 21 adantr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) )
36 35 cnmptid ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ 𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
37 simpr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
38 35 35 37 cnmptc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ 𝑦 ) ∈ ( 𝐽 Cn 𝐽 ) )
39 2 33 8 34 35 36 38 cnmpt1ip ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) )
40 33 cnfldhaus ⊢ ( TopOpen ‘ ℂfld ) ∈ Haus
41 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
42 9 clm0 ⊢ ( 𝑊 ∈ ℂMod → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
43 41 42 syl ⊢ ( 𝑊 ∈ ℂPreHil → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
44 43 ad2antrr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
45 0cn ⊢ 0 ∈ ℂ
46 44 45 eqeltrrdi ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ℂ )
47 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
48 47 sncld ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Haus ∧ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∈ ℂ ) → { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
49 40 46 48 sylancr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
50 cnclima ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) ∈ ( 𝐽 Cn ( TopOpen ‘ ℂfld ) ) ∧ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) “ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∈ ( Clsd ‘ 𝐽 ) )
51 39 49 50 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ◡ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) ) “ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∈ ( Clsd ‘ 𝐽 ) )
52 32 51 eqeltrrid ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ 𝐽 ) )
53 28 52 sylan2 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) ∧ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) ) → { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ 𝐽 ) )
54 53 ralrimiva ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → ∀ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ 𝐽 ) )
55 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
56 55 riincld ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∩ ∩ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∈ ( Clsd ‘ 𝐽 ) )
57 27 54 56 syl2anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → ( ∪ 𝐽 ∩ ∩ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝑆 ) { 𝑥 ∈ ( Base ‘ 𝑊 ) ∣ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ∈ ( Clsd ‘ 𝐽 ) )
58 25 57 eqeltrd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )