Metamath Proof Explorer


Theorem lhprelat3N

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 B=BaseK
lhprelat3.l ˙=K
lhprelat3.s <˙=<K
lhprelat3.m ˙=meetK
lhprelat3.c C=K
lhprelat3.h H=LHypK
Assertion lhprelat3N KHLXBYBX<˙YwHX˙Y˙wY˙wCY

Proof

Step Hyp Ref Expression
1 lhprelat3.b B=BaseK
2 lhprelat3.l ˙=K
3 lhprelat3.s <˙=<K
4 lhprelat3.m ˙=meetK
5 lhprelat3.c C=K
6 lhprelat3.h H=LHypK
7 simpr KHLXBYBX<˙YpAtomsKpAtomsK
8 simpll1 KHLXBYBX<˙YpAtomsKKHL
9 eqid AtomsK=AtomsK
10 1 9 atbase pAtomsKpB
11 10 adantl KHLXBYBX<˙YpAtomsKpB
12 eqid ocK=ocK
13 1 12 9 6 lhpoc2N KHLpBpAtomsKocKpH
14 8 11 13 syl2anc KHLXBYBX<˙YpAtomsKpAtomsKocKpH
15 7 14 mpbid KHLXBYBX<˙YpAtomsKocKpH
16 15 adantr KHLXBYBX<˙YpAtomsKocKYCocKYjoinKpocKYjoinKp˙ocKXocKpH
17 hlop KHLKOP
18 8 17 syl KHLXBYBX<˙YpAtomsKKOP
19 8 hllatd KHLXBYBX<˙YpAtomsKKLat
20 simpll3 KHLXBYBX<˙YpAtomsKYB
21 1 12 opoccl KOPpBocKpB
22 18 11 21 syl2anc KHLXBYBX<˙YpAtomsKocKpB
23 1 4 latmcl KLatYBocKpBY˙ocKpB
24 19 20 22 23 syl3anc KHLXBYBX<˙YpAtomsKY˙ocKpB
25 1 12 5 cvrcon3b KOPY˙ocKpBYBY˙ocKpCYocKYCocKY˙ocKp
26 18 24 20 25 syl3anc KHLXBYBX<˙YpAtomsKY˙ocKpCYocKYCocKY˙ocKp
27 hlol KHLKOL
28 8 27 syl KHLXBYBX<˙YpAtomsKKOL
29 eqid joinK=joinK
30 1 29 4 12 oldmm3N KOLYBpBocKY˙ocKp=ocKYjoinKp
31 28 20 11 30 syl3anc KHLXBYBX<˙YpAtomsKocKY˙ocKp=ocKYjoinKp
32 31 breq2d KHLXBYBX<˙YpAtomsKocKYCocKY˙ocKpocKYCocKYjoinKp
33 26 32 bitr2d KHLXBYBX<˙YpAtomsKocKYCocKYjoinKpY˙ocKpCY
34 simpll2 KHLXBYBX<˙YpAtomsKXB
35 1 2 12 oplecon3b KOPXBY˙ocKpBX˙Y˙ocKpocKY˙ocKp˙ocKX
36 18 34 24 35 syl3anc KHLXBYBX<˙YpAtomsKX˙Y˙ocKpocKY˙ocKp˙ocKX
37 31 breq1d KHLXBYBX<˙YpAtomsKocKY˙ocKp˙ocKXocKYjoinKp˙ocKX
38 36 37 bitr2d KHLXBYBX<˙YpAtomsKocKYjoinKp˙ocKXX˙Y˙ocKp
39 33 38 anbi12d KHLXBYBX<˙YpAtomsKocKYCocKYjoinKpocKYjoinKp˙ocKXY˙ocKpCYX˙Y˙ocKp
40 39 biimpa KHLXBYBX<˙YpAtomsKocKYCocKYjoinKpocKYjoinKp˙ocKXY˙ocKpCYX˙Y˙ocKp
41 40 ancomd KHLXBYBX<˙YpAtomsKocKYCocKYjoinKpocKYjoinKp˙ocKXX˙Y˙ocKpY˙ocKpCY
42 oveq2 w=ocKpY˙w=Y˙ocKp
43 42 breq2d w=ocKpX˙Y˙wX˙Y˙ocKp
44 42 breq1d w=ocKpY˙wCYY˙ocKpCY
45 43 44 anbi12d w=ocKpX˙Y˙wY˙wCYX˙Y˙ocKpY˙ocKpCY
46 45 rspcev ocKpHX˙Y˙ocKpY˙ocKpCYwHX˙Y˙wY˙wCY
47 16 41 46 syl2anc KHLXBYBX<˙YpAtomsKocKYCocKYjoinKpocKYjoinKp˙ocKXwHX˙Y˙wY˙wCY
48 simpl1 KHLXBYBX<˙YKHL
49 48 17 syl KHLXBYBX<˙YKOP
50 simpl3 KHLXBYBX<˙YYB
51 1 12 opoccl KOPYBocKYB
52 49 50 51 syl2anc KHLXBYBX<˙YocKYB
53 simpl2 KHLXBYBX<˙YXB
54 1 12 opoccl KOPXBocKXB
55 49 53 54 syl2anc KHLXBYBX<˙YocKXB
56 simpr KHLXBYBX<˙YX<˙Y
57 1 3 12 opltcon3b KOPXBYBX<˙YocKY<˙ocKX
58 49 53 50 57 syl3anc KHLXBYBX<˙YX<˙YocKY<˙ocKX
59 56 58 mpbid KHLXBYBX<˙YocKY<˙ocKX
60 1 2 3 29 5 9 hlrelat3 KHLocKYBocKXBocKY<˙ocKXpAtomsKocKYCocKYjoinKpocKYjoinKp˙ocKX
61 48 52 55 59 60 syl31anc KHLXBYBX<˙YpAtomsKocKYCocKYjoinKpocKYjoinKp˙ocKX
62 47 61 r19.29a KHLXBYBX<˙YwHX˙Y˙wY˙wCY