Description: The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 . (Contributed by NM, 20-Jun-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lhprelat3.b | |
|
lhprelat3.l | |
||
lhprelat3.s | |
||
lhprelat3.m | |
||
lhprelat3.c | |
||
lhprelat3.h | |
||
Assertion | lhprelat3N | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lhprelat3.b | |
|
2 | lhprelat3.l | |
|
3 | lhprelat3.s | |
|
4 | lhprelat3.m | |
|
5 | lhprelat3.c | |
|
6 | lhprelat3.h | |
|
7 | simpr | |
|
8 | simpll1 | |
|
9 | eqid | |
|
10 | 1 9 | atbase | |
11 | 10 | adantl | |
12 | eqid | |
|
13 | 1 12 9 6 | lhpoc2N | |
14 | 8 11 13 | syl2anc | |
15 | 7 14 | mpbid | |
16 | 15 | adantr | |
17 | hlop | |
|
18 | 8 17 | syl | |
19 | 8 | hllatd | |
20 | simpll3 | |
|
21 | 1 12 | opoccl | |
22 | 18 11 21 | syl2anc | |
23 | 1 4 | latmcl | |
24 | 19 20 22 23 | syl3anc | |
25 | 1 12 5 | cvrcon3b | |
26 | 18 24 20 25 | syl3anc | |
27 | hlol | |
|
28 | 8 27 | syl | |
29 | eqid | |
|
30 | 1 29 4 12 | oldmm3N | |
31 | 28 20 11 30 | syl3anc | |
32 | 31 | breq2d | |
33 | 26 32 | bitr2d | |
34 | simpll2 | |
|
35 | 1 2 12 | oplecon3b | |
36 | 18 34 24 35 | syl3anc | |
37 | 31 | breq1d | |
38 | 36 37 | bitr2d | |
39 | 33 38 | anbi12d | |
40 | 39 | biimpa | |
41 | 40 | ancomd | |
42 | oveq2 | |
|
43 | 42 | breq2d | |
44 | 42 | breq1d | |
45 | 43 44 | anbi12d | |
46 | 45 | rspcev | |
47 | 16 41 46 | syl2anc | |
48 | simpl1 | |
|
49 | 48 17 | syl | |
50 | simpl3 | |
|
51 | 1 12 | opoccl | |
52 | 49 50 51 | syl2anc | |
53 | simpl2 | |
|
54 | 1 12 | opoccl | |
55 | 49 53 54 | syl2anc | |
56 | simpr | |
|
57 | 1 3 12 | opltcon3b | |
58 | 49 53 50 57 | syl3anc | |
59 | 56 58 | mpbid | |
60 | 1 2 3 29 5 9 | hlrelat3 | |
61 | 48 52 55 59 60 | syl31anc | |
62 | 47 61 | r19.29a | |