Theorem hsn0elch

Description: The zero subspace belongs to the set of closed subspaces of Hilbert space. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	hsn0elch	$$⊢\left\{0_{ℎ}\right\}\in {\mathbf{C}}_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
2		snssi	$$⊢0_{ℎ}\in \mathscr{H}\to \left\{0_{ℎ}\right\}\subseteq \mathscr{H}$$
3	1 2	ax-mp	$$⊢\left\{0_{ℎ}\right\}\subseteq \mathscr{H}$$
4	1	elexi	$$⊢0_{ℎ}\in \mathrm{V}$$
5	4	snid	$$⊢0_{ℎ}\in \left\{0_{ℎ}\right\}$$
6	3 5	pm3.2i	$$⊢\left(\left\{0_{ℎ}\right\}\subseteq \mathscr{H}\wedge 0_{ℎ}\in \left\{0_{ℎ}\right\}\right)$$
7		velsn	$$⊢x\in \left\{0_{ℎ}\right\}\leftrightarrow x=0_{ℎ}$$
8		velsn	$$⊢y\in \left\{0_{ℎ}\right\}\leftrightarrow y=0_{ℎ}$$
9		oveq12	$$⊢\left(x=0_{ℎ}\wedge y=0_{ℎ}\right)\to x{+}_{ℎ}y=0_{ℎ}{+}_{ℎ}{0}_{ℎ}$$
10	1	hvaddid2i	$$⊢0_{ℎ}{+}_{ℎ}{0}_{ℎ}=0_{ℎ}$$
11	9 10	eqtrdi	$$⊢\left(x=0_{ℎ}\wedge y=0_{ℎ}\right)\to x{+}_{ℎ}y=0_{ℎ}$$
12		ovex	$$⊢x{+}_{ℎ}y\in \mathrm{V}$$
13	12	elsn	$$⊢x{+}_{ℎ}y\in \left\{0_{ℎ}\right\}\leftrightarrow x{+}_{ℎ}y=0_{ℎ}$$
14	11 13	sylibr	$$⊢\left(x=0_{ℎ}\wedge y=0_{ℎ}\right)\to x{+}_{ℎ}y\in \left\{0_{ℎ}\right\}$$
15	7 8 14	syl2anb	$$⊢\left(x\in \left\{0_{ℎ}\right\}\wedge y\in \left\{0_{ℎ}\right\}\right)\to x{+}_{ℎ}y\in \left\{0_{ℎ}\right\}$$
16	15	rgen2	$$⊢\forall x\in \left\{0_{ℎ}\right\}\forall y\in \left\{0_{ℎ}\right\}x{+}_{ℎ}y\in \left\{0_{ℎ}\right\}$$
17		oveq2	$$⊢y=0_{ℎ}\to x{\cdot }_{ℎ}y=x{\cdot }_{ℎ}{0}_{ℎ}$$
18		hvmul0	$$⊢x\in ℂ\to x{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
19	17 18	sylan9eqr	$$⊢\left(x\in ℂ\wedge y=0_{ℎ}\right)\to x{\cdot }_{ℎ}y=0_{ℎ}$$
20		ovex	$$⊢x{\cdot }_{ℎ}y\in \mathrm{V}$$
21	20	elsn	$$⊢x{\cdot }_{ℎ}y\in \left\{0_{ℎ}\right\}\leftrightarrow x{\cdot }_{ℎ}y=0_{ℎ}$$
22	19 21	sylibr	$$⊢\left(x\in ℂ\wedge y=0_{ℎ}\right)\to x{\cdot }_{ℎ}y\in \left\{0_{ℎ}\right\}$$
23	8 22	sylan2b	$$⊢\left(x\in ℂ\wedge y\in \left\{0_{ℎ}\right\}\right)\to x{\cdot }_{ℎ}y\in \left\{0_{ℎ}\right\}$$
24	23	rgen2	$$⊢\forall x\in ℂ\forall y\in \left\{0_{ℎ}\right\}x{\cdot }_{ℎ}y\in \left\{0_{ℎ}\right\}$$
25	16 24	pm3.2i	$$⊢\left(\forall x\in \left\{0_{ℎ}\right\}\forall y\in \left\{0_{ℎ}\right\}x{+}_{ℎ}y\in \left\{0_{ℎ}\right\}\wedge \forall x\in ℂ\forall y\in \left\{0_{ℎ}\right\}x{\cdot }_{ℎ}y\in \left\{0_{ℎ}\right\}\right)$$
26		issh2	$$⊢\left\{0_{ℎ}\right\}\in {\mathbf{S}}_{\mathscr{H}}\leftrightarrow \left(\left(\left\{0_{ℎ}\right\}\subseteq \mathscr{H}\wedge 0_{ℎ}\in \left\{0_{ℎ}\right\}\right)\wedge \left(\forall x\in \left\{0_{ℎ}\right\}\forall y\in \left\{0_{ℎ}\right\}x{+}_{ℎ}y\in \left\{0_{ℎ}\right\}\wedge \forall x\in ℂ\forall y\in \left\{0_{ℎ}\right\}x{\cdot }_{ℎ}y\in \left\{0_{ℎ}\right\}\right)\right)$$
27	6 25 26	mpbir2an	$$⊢\left\{0_{ℎ}\right\}\in {\mathbf{S}}_{\mathscr{H}}$$
28	4	fconst2	$$⊢f:\mathbb{N}⟶\left\{0_{ℎ}\right\}\leftrightarrow f=\mathbb{N}\times \left\{0_{ℎ}\right\}$$
29		hlim0	$$⊢\left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{v}{⇝}{0}_{ℎ}$$
30		breq1	$$⊢f=\mathbb{N}\times \left\{0_{ℎ}\right\}\to \left(f\underset{v}{⇝}{0}_{ℎ}\leftrightarrow \left(\mathbb{N}\times \left\{0_{ℎ}\right\}\right)\underset{v}{⇝}{0}_{ℎ}\right)$$
31	29 30	mpbiri	$$⊢f=\mathbb{N}\times \left\{0_{ℎ}\right\}\to f\underset{v}{⇝}{0}_{ℎ}$$
32	28 31	sylbi	$$⊢f:\mathbb{N}⟶\left\{0_{ℎ}\right\}\to f\underset{v}{⇝}{0}_{ℎ}$$
33		hlimuni	$$⊢\left(f\underset{v}{⇝}{0}_{ℎ}\wedge f\underset{v}{⇝}x\right)\to 0_{ℎ}=x$$
34	33	eleq1d	$$⊢\left(f\underset{v}{⇝}{0}_{ℎ}\wedge f\underset{v}{⇝}x\right)\to \left(0_{ℎ}\in \left\{0_{ℎ}\right\}\leftrightarrow x\in \left\{0_{ℎ}\right\}\right)$$
35	32 34	sylan	$$⊢\left(f:\mathbb{N}⟶\left\{0_{ℎ}\right\}\wedge f\underset{v}{⇝}x\right)\to \left(0_{ℎ}\in \left\{0_{ℎ}\right\}\leftrightarrow x\in \left\{0_{ℎ}\right\}\right)$$
36	5 35	mpbii	$$⊢\left(f:\mathbb{N}⟶\left\{0_{ℎ}\right\}\wedge f\underset{v}{⇝}x\right)\to x\in \left\{0_{ℎ}\right\}$$
37	36	gen2	$$⊢\forall f\forall x\left(\left(f:\mathbb{N}⟶\left\{0_{ℎ}\right\}\wedge f\underset{v}{⇝}x\right)\to x\in \left\{0_{ℎ}\right\}\right)$$
38		isch2	$$⊢\left\{0_{ℎ}\right\}\in {\mathbf{C}}_{\mathscr{H}}\leftrightarrow \left(\left\{0_{ℎ}\right\}\in {\mathbf{S}}_{\mathscr{H}}\wedge \forall f\forall x\left(\left(f:\mathbb{N}⟶\left\{0_{ℎ}\right\}\wedge f\underset{v}{⇝}x\right)\to x\in \left\{0_{ℎ}\right\}\right)\right)$$
39	27 37 38	mpbir2an	$$⊢\left\{0_{ℎ}\right\}\in {\mathbf{C}}_{\mathscr{H}}$$