Description: Hilbert space has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of Kalmbach p. 153. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | spansncv2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spansncv | |
|
2 | 1 | 3exp | |
3 | 2 | com23 | |
4 | 3 | imp | |
5 | 4 | ralrimiv | |
6 | 5 | anim2i | |
7 | 6 | expcom | |
8 | spansnch | |
|
9 | chnle | |
|
10 | 8 9 | sylan2 | |
11 | chjcl | |
|
12 | 8 11 | sylan2 | |
13 | cvbr2 | |
|
14 | 12 13 | syldan | |
15 | 7 10 14 | 3imtr4d | |