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 = Base K
lhprelat3.l ˙ = K
lhprelat3.s < ˙ = < K
lhprelat3.m ˙ = meet K
lhprelat3.c C = K
lhprelat3.h H = LHyp K
Assertion lhprelat3N K HL X B Y B X < ˙ Y w H X ˙ Y ˙ w Y ˙ w C Y

Proof

Step Hyp Ref Expression
1 lhprelat3.b B = Base K
2 lhprelat3.l ˙ = K
3 lhprelat3.s < ˙ = < K
4 lhprelat3.m ˙ = meet K
5 lhprelat3.c C = K
6 lhprelat3.h H = LHyp K
7 simpr K HL X B Y B X < ˙ Y p Atoms K p Atoms K
8 simpll1 K HL X B Y B X < ˙ Y p Atoms K K HL
9 eqid Atoms K = Atoms K
10 1 9 atbase p Atoms K p B
11 10 adantl K HL X B Y B X < ˙ Y p Atoms K p B
12 eqid oc K = oc K
13 1 12 9 6 lhpoc2N K HL p B p Atoms K oc K p H
14 8 11 13 syl2anc K HL X B Y B X < ˙ Y p Atoms K p Atoms K oc K p H
15 7 14 mpbid K HL X B Y B X < ˙ Y p Atoms K oc K p H
16 15 adantr K HL X B Y B X < ˙ Y p Atoms K oc K Y C oc K Y join K p oc K Y join K p ˙ oc K X oc K p H
17 hlop K HL K OP
18 8 17 syl K HL X B Y B X < ˙ Y p Atoms K K OP
19 8 hllatd K HL X B Y B X < ˙ Y p Atoms K K Lat
20 simpll3 K HL X B Y B X < ˙ Y p Atoms K Y B
21 1 12 opoccl K OP p B oc K p B
22 18 11 21 syl2anc K HL X B Y B X < ˙ Y p Atoms K oc K p B
23 1 4 latmcl K Lat Y B oc K p B Y ˙ oc K p B
24 19 20 22 23 syl3anc K HL X B Y B X < ˙ Y p Atoms K Y ˙ oc K p B
25 1 12 5 cvrcon3b K OP Y ˙ oc K p B Y B Y ˙ oc K p C Y oc K Y C oc K Y ˙ oc K p
26 18 24 20 25 syl3anc K HL X B Y B X < ˙ Y p Atoms K Y ˙ oc K p C Y oc K Y C oc K Y ˙ oc K p
27 hlol K HL K OL
28 8 27 syl K HL X B Y B X < ˙ Y p Atoms K K OL
29 eqid join K = join K
30 1 29 4 12 oldmm3N K OL Y B p B oc K Y ˙ oc K p = oc K Y join K p
31 28 20 11 30 syl3anc K HL X B Y B X < ˙ Y p Atoms K oc K Y ˙ oc K p = oc K Y join K p
32 31 breq2d K HL X B Y B X < ˙ Y p Atoms K oc K Y C oc K Y ˙ oc K p oc K Y C oc K Y join K p
33 26 32 bitr2d K HL X B Y B X < ˙ Y p Atoms K oc K Y C oc K Y join K p Y ˙ oc K p C Y
34 simpll2 K HL X B Y B X < ˙ Y p Atoms K X B
35 1 2 12 oplecon3b K OP X B Y ˙ oc K p B X ˙ Y ˙ oc K p oc K Y ˙ oc K p ˙ oc K X
36 18 34 24 35 syl3anc K HL X B Y B X < ˙ Y p Atoms K X ˙ Y ˙ oc K p oc K Y ˙ oc K p ˙ oc K X
37 31 breq1d K HL X B Y B X < ˙ Y p Atoms K oc K Y ˙ oc K p ˙ oc K X oc K Y join K p ˙ oc K X
38 36 37 bitr2d K HL X B Y B X < ˙ Y p Atoms K oc K Y join K p ˙ oc K X X ˙ Y ˙ oc K p
39 33 38 anbi12d K HL X B Y B X < ˙ Y p Atoms K oc K Y C oc K Y join K p oc K Y join K p ˙ oc K X Y ˙ oc K p C Y X ˙ Y ˙ oc K p
40 39 biimpa K HL X B Y B X < ˙ Y p Atoms K oc K Y C oc K Y join K p oc K Y join K p ˙ oc K X Y ˙ oc K p C Y X ˙ Y ˙ oc K p
41 40 ancomd K HL X B Y B X < ˙ Y p Atoms K oc K Y C oc K Y join K p oc K Y join K p ˙ oc K X X ˙ Y ˙ oc K p Y ˙ oc K p C Y
42 oveq2 w = oc K p Y ˙ w = Y ˙ oc K p
43 42 breq2d w = oc K p X ˙ Y ˙ w X ˙ Y ˙ oc K p
44 42 breq1d w = oc K p Y ˙ w C Y Y ˙ oc K p C Y
45 43 44 anbi12d w = oc K p X ˙ Y ˙ w Y ˙ w C Y X ˙ Y ˙ oc K p Y ˙ oc K p C Y
46 45 rspcev oc K p H X ˙ Y ˙ oc K p Y ˙ oc K p C Y w H X ˙ Y ˙ w Y ˙ w C Y
47 16 41 46 syl2anc K HL X B Y B X < ˙ Y p Atoms K oc K Y C oc K Y join K p oc K Y join K p ˙ oc K X w H X ˙ Y ˙ w Y ˙ w C Y
48 simpl1 K HL X B Y B X < ˙ Y K HL
49 48 17 syl K HL X B Y B X < ˙ Y K OP
50 simpl3 K HL X B Y B X < ˙ Y Y B
51 1 12 opoccl K OP Y B oc K Y B
52 49 50 51 syl2anc K HL X B Y B X < ˙ Y oc K Y B
53 simpl2 K HL X B Y B X < ˙ Y X B
54 1 12 opoccl K OP X B oc K X B
55 49 53 54 syl2anc K HL X B Y B X < ˙ Y oc K X B
56 simpr K HL X B Y B X < ˙ Y X < ˙ Y
57 1 3 12 opltcon3b K OP X B Y B X < ˙ Y oc K Y < ˙ oc K X
58 49 53 50 57 syl3anc K HL X B Y B X < ˙ Y X < ˙ Y oc K Y < ˙ oc K X
59 56 58 mpbid K HL X B Y B X < ˙ Y oc K Y < ˙ oc K X
60 1 2 3 29 5 9 hlrelat3 K HL oc K Y B oc K X B oc K Y < ˙ oc K X p Atoms K oc K Y C oc K Y join K p oc K Y join K p ˙ oc K X
61 48 52 55 59 60 syl31anc K HL X B Y B X < ˙ Y p Atoms K oc K Y C oc K Y join K p oc K Y join K p ˙ oc K X
62 47 61 r19.29a K HL X B Y B X < ˙ Y w H X ˙ Y ˙ w Y ˙ w C Y