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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-hv0cl | |
|
2 | snssi | |
|
3 | 1 2 | ax-mp | |
4 | 1 | elexi | |
5 | 4 | snid | |
6 | 3 5 | pm3.2i | |
7 | velsn | |
|
8 | velsn | |
|
9 | oveq12 | |
|
10 | 1 | hvaddid2i | |
11 | 9 10 | eqtrdi | |
12 | ovex | |
|
13 | 12 | elsn | |
14 | 11 13 | sylibr | |
15 | 7 8 14 | syl2anb | |
16 | 15 | rgen2 | |
17 | oveq2 | |
|
18 | hvmul0 | |
|
19 | 17 18 | sylan9eqr | |
20 | ovex | |
|
21 | 20 | elsn | |
22 | 19 21 | sylibr | |
23 | 8 22 | sylan2b | |
24 | 23 | rgen2 | |
25 | 16 24 | pm3.2i | |
26 | issh2 | |
|
27 | 6 25 26 | mpbir2an | |
28 | 4 | fconst2 | |
29 | hlim0 | |
|
30 | breq1 | |
|
31 | 29 30 | mpbiri | |
32 | 28 31 | sylbi | |
33 | hlimuni | |
|
34 | 33 | eleq1d | |
35 | 32 34 | sylan | |
36 | 5 35 | mpbii | |
37 | 36 | gen2 | |
38 | isch2 | |
|
39 | 27 37 38 | mpbir2an | |