# Metamath Proof Explorer

## Theorem lhp2lt

Description: The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013)

Ref Expression
Hypotheses lhp2lt.l
lhp2lt.s
lhp2lt.j
lhp2lt.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
lhp2lt.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
Assertion lhp2lt

### Proof

Step Hyp Ref Expression
1 lhp2lt.l
2 lhp2lt.s
3 lhp2lt.j
4 lhp2lt.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 lhp2lt.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 simp2r
7 simp3r
8 simp1l
9 8 hllatd
10 simp2l
11 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
12 11 4 atbase ${⊢}{P}\in {A}\to {P}\in {\mathrm{Base}}_{{K}}$
13 10 12 syl
14 simp3l
15 11 4 atbase ${⊢}{Q}\in {A}\to {Q}\in {\mathrm{Base}}_{{K}}$
16 14 15 syl
17 simp1r
18 11 5 lhpbase ${⊢}{W}\in {H}\to {W}\in {\mathrm{Base}}_{{K}}$
19 17 18 syl
20 11 1 3 latjle12
21 9 13 16 19 20 syl13anc
22 6 7 21 mpbi2and
23 3 1 4 3dim2
24 8 10 14 23 syl3anc
25 simp11l
26 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
27 25 26 syl
28 25 hllatd
29 simp12l
30 simp13l
31 11 3 4 hlatjcl
32 25 29 30 31 syl3anc
33 simp2l
34 11 4 atbase ${⊢}{r}\in {A}\to {r}\in {\mathrm{Base}}_{{K}}$
35 33 34 syl
36 11 3 latjcl
37 28 32 35 36 syl3anc
38 simp2r
39 11 4 atbase ${⊢}{s}\in {A}\to {s}\in {\mathrm{Base}}_{{K}}$
40 38 39 syl
41 11 3 latjcl
42 28 37 40 41 syl3anc
43 eqid ${⊢}\mathrm{1.}\left({K}\right)=\mathrm{1.}\left({K}\right)$
44 eqid ${⊢}{⋖}_{{K}}={⋖}_{{K}}$
45 11 43 44 ncvr1
46 27 42 45 syl2anc
47 eqid ${⊢}\mathrm{lub}\left({K}\right)=\mathrm{lub}\left({K}\right)$
48 simpl1l
49 48 hllatd
50 simpl2l
51 simpl3l
52 48 50 51 31 syl3anc
53 simpr1l
54 53 34 syl
55 49 52 54 36 syl3anc
56 48 26 syl
57 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
58 11 47 57 op01dm ${⊢}{K}\in \mathrm{OP}\to \left({\mathrm{Base}}_{{K}}\in \mathrm{dom}\mathrm{lub}\left({K}\right)\wedge {\mathrm{Base}}_{{K}}\in \mathrm{dom}\mathrm{glb}\left({K}\right)\right)$
59 58 simpld ${⊢}{K}\in \mathrm{OP}\to {\mathrm{Base}}_{{K}}\in \mathrm{dom}\mathrm{lub}\left({K}\right)$
60 56 59 syl
61 11 47 1 43 48 55 60 ple1
62 hlpos ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Poset}$
63 48 62 syl
64 11 43 op1cl ${⊢}{K}\in \mathrm{OP}\to \mathrm{1.}\left({K}\right)\in {\mathrm{Base}}_{{K}}$
65 56 64 syl
66 simpr2l
67 11 1 3 44 4 cvr1
68 48 52 53 67 syl3anc
69 66 68 mpbid
70 simpr3
71 simpl1r
72 43 44 5 lhp1cvr ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {W}{⋖}_{{K}}\mathrm{1.}\left({K}\right)$
73 48 71 72 syl2anc
74 70 73 eqbrtrd
75 11 1 44 cvrcmp
76 63 55 65 52 69 74 75 syl132anc
77 61 76 mpbid
78 simpr2r
79 simpr1r
80 11 1 3 44 4 cvr1
81 48 55 79 80 syl3anc
82 78 81 mpbid
83 77 82 eqbrtrrd
84 83 3exp2
85 84 3imp
86 85 necon3bd
87 46 86 mpd
88 87 3exp
89 88 rexlimdvv
90 24 89 mpd
91 8 10 14 31 syl3anc
92 1 2 pltval
93 8 91 17 92 syl3anc
94 22 90 93 mpbir2and