Description: Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of Kalmbach p. 153. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | spansncv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psseq1 | |
|
2 | oveq1 | |
|
3 | 2 | sseq2d | |
4 | 1 3 | anbi12d | |
5 | 2 | eqeq2d | |
6 | 4 5 | imbi12d | |
7 | psseq2 | |
|
8 | sseq1 | |
|
9 | 7 8 | anbi12d | |
10 | eqeq1 | |
|
11 | 9 10 | imbi12d | |
12 | sneq | |
|
13 | 12 | fveq2d | |
14 | 13 | oveq2d | |
15 | 14 | sseq2d | |
16 | 15 | anbi2d | |
17 | 14 | eqeq2d | |
18 | 16 17 | imbi12d | |
19 | ifchhv | |
|
20 | ifchhv | |
|
21 | ifhvhv0 | |
|
22 | 19 20 21 | spansncvi | |
23 | 6 11 18 22 | dedth3h | |