Metamath Proof Explorer


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 0C

Proof

Step Hyp Ref Expression
1 ax-hv0cl 0
2 snssi 00
3 1 2 ax-mp 0
4 1 elexi 0V
5 4 snid 00
6 3 5 pm3.2i 000
7 velsn x0x=0
8 velsn y0y=0
9 oveq12 x=0y=0x+y=0+0
10 1 hvaddid2i 0+0=0
11 9 10 eqtrdi x=0y=0x+y=0
12 ovex x+yV
13 12 elsn x+y0x+y=0
14 11 13 sylibr x=0y=0x+y0
15 7 8 14 syl2anb x0y0x+y0
16 15 rgen2 x0y0x+y0
17 oveq2 y=0xy=x0
18 hvmul0 xx0=0
19 17 18 sylan9eqr xy=0xy=0
20 ovex xyV
21 20 elsn xy0xy=0
22 19 21 sylibr xy=0xy0
23 8 22 sylan2b xy0xy0
24 23 rgen2 xy0xy0
25 16 24 pm3.2i x0y0x+y0xy0xy0
26 issh2 0S000x0y0x+y0xy0xy0
27 6 25 26 mpbir2an 0S
28 4 fconst2 f:0f=×0
29 hlim0 ×0v0
30 breq1 f=×0fv0×0v0
31 29 30 mpbiri f=×0fv0
32 28 31 sylbi f:0fv0
33 hlimuni fv0fvx0=x
34 33 eleq1d fv0fvx00x0
35 32 34 sylan f:0fvx00x0
36 5 35 mpbii f:0fvxx0
37 36 gen2 fxf:0fvxx0
38 isch2 0C0Sfxf:0fvxx0
39 27 37 38 mpbir2an 0C