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 ‘ 𝐽 ) )