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

Metamath Proof Explorer

Theorem csscld

Proof