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 ˙=K
lhp2lt.s <˙=<K
lhp2lt.j ˙=joinK
lhp2lt.a A=AtomsK
lhp2lt.h H=LHypK
Assertion lhp2lt KHLWHPAP˙WQAQ˙WP˙Q<˙W

Proof

Step Hyp Ref Expression
1 lhp2lt.l ˙=K
2 lhp2lt.s <˙=<K
3 lhp2lt.j ˙=joinK
4 lhp2lt.a A=AtomsK
5 lhp2lt.h H=LHypK
6 simp2r KHLWHPAP˙WQAQ˙WP˙W
7 simp3r KHLWHPAP˙WQAQ˙WQ˙W
8 simp1l KHLWHPAP˙WQAQ˙WKHL
9 8 hllatd KHLWHPAP˙WQAQ˙WKLat
10 simp2l KHLWHPAP˙WQAQ˙WPA
11 eqid BaseK=BaseK
12 11 4 atbase PAPBaseK
13 10 12 syl KHLWHPAP˙WQAQ˙WPBaseK
14 simp3l KHLWHPAP˙WQAQ˙WQA
15 11 4 atbase QAQBaseK
16 14 15 syl KHLWHPAP˙WQAQ˙WQBaseK
17 simp1r KHLWHPAP˙WQAQ˙WWH
18 11 5 lhpbase WHWBaseK
19 17 18 syl KHLWHPAP˙WQAQ˙WWBaseK
20 11 1 3 latjle12 KLatPBaseKQBaseKWBaseKP˙WQ˙WP˙Q˙W
21 9 13 16 19 20 syl13anc KHLWHPAP˙WQAQ˙WP˙WQ˙WP˙Q˙W
22 6 7 21 mpbi2and KHLWHPAP˙WQAQ˙WP˙Q˙W
23 3 1 4 3dim2 KHLPAQArAsA¬r˙P˙Q¬s˙P˙Q˙r
24 8 10 14 23 syl3anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙r
25 simp11l KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rKHL
26 hlop KHLKOP
27 25 26 syl KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rKOP
28 25 hllatd KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rKLat
29 simp12l KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rPA
30 simp13l KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rQA
31 11 3 4 hlatjcl KHLPAQAP˙QBaseK
32 25 29 30 31 syl3anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙QBaseK
33 simp2l KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rrA
34 11 4 atbase rArBaseK
35 33 34 syl KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rrBaseK
36 11 3 latjcl KLatP˙QBaseKrBaseKP˙Q˙rBaseK
37 28 32 35 36 syl3anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q˙rBaseK
38 simp2r KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rsA
39 11 4 atbase sAsBaseK
40 38 39 syl KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rsBaseK
41 11 3 latjcl KLatP˙Q˙rBaseKsBaseKP˙Q˙r˙sBaseK
42 28 37 40 41 syl3anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q˙r˙sBaseK
43 eqid 1.K=1.K
44 eqid K=K
45 11 43 44 ncvr1 KOPP˙Q˙r˙sBaseK¬1.KKP˙Q˙r˙s
46 27 42 45 syl2anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙r¬1.KKP˙Q˙r˙s
47 eqid lubK=lubK
48 simpl1l KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WKHL
49 48 hllatd KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WKLat
50 simpl2l KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WPA
51 simpl3l KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WQA
52 48 50 51 31 syl3anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WP˙QBaseK
53 simpr1l KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WrA
54 53 34 syl KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WrBaseK
55 49 52 54 36 syl3anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WP˙Q˙rBaseK
56 48 26 syl KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WKOP
57 eqid glbK=glbK
58 11 47 57 op01dm KOPBaseKdomlubKBaseKdomglbK
59 58 simpld KOPBaseKdomlubK
60 56 59 syl KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WBaseKdomlubK
61 11 47 1 43 48 55 60 ple1 KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WP˙Q˙r˙1.K
62 hlpos KHLKPoset
63 48 62 syl KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WKPoset
64 11 43 op1cl KOP1.KBaseK
65 56 64 syl KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=W1.KBaseK
66 simpr2l KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=W¬r˙P˙Q
67 11 1 3 44 4 cvr1 KHLP˙QBaseKrA¬r˙P˙QP˙QKP˙Q˙r
68 48 52 53 67 syl3anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=W¬r˙P˙QP˙QKP˙Q˙r
69 66 68 mpbid KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WP˙QKP˙Q˙r
70 simpr3 KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WP˙Q=W
71 simpl1r KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WWH
72 43 44 5 lhp1cvr KHLWHWK1.K
73 48 71 72 syl2anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WWK1.K
74 70 73 eqbrtrd KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WP˙QK1.K
75 11 1 44 cvrcmp KPosetP˙Q˙rBaseK1.KBaseKP˙QBaseKP˙QKP˙Q˙rP˙QK1.KP˙Q˙r˙1.KP˙Q˙r=1.K
76 63 55 65 52 69 74 75 syl132anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WP˙Q˙r˙1.KP˙Q˙r=1.K
77 61 76 mpbid KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WP˙Q˙r=1.K
78 simpr2r KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=W¬s˙P˙Q˙r
79 simpr1r KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WsA
80 11 1 3 44 4 cvr1 KHLP˙Q˙rBaseKsA¬s˙P˙Q˙rP˙Q˙rKP˙Q˙r˙s
81 48 55 79 80 syl3anc KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=W¬s˙P˙Q˙rP˙Q˙rKP˙Q˙r˙s
82 78 81 mpbid KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=WP˙Q˙rKP˙Q˙r˙s
83 77 82 eqbrtrrd KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=W1.KKP˙Q˙r˙s
84 83 3exp2 KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=W1.KKP˙Q˙r˙s
85 84 3imp KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙Q=W1.KKP˙Q˙r˙s
86 85 necon3bd KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙r¬1.KKP˙Q˙r˙sP˙QW
87 46 86 mpd KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙QW
88 87 3exp KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙QW
89 88 rexlimdvv KHLWHPAP˙WQAQ˙WrAsA¬r˙P˙Q¬s˙P˙Q˙rP˙QW
90 24 89 mpd KHLWHPAP˙WQAQ˙WP˙QW
91 8 10 14 31 syl3anc KHLWHPAP˙WQAQ˙WP˙QBaseK
92 1 2 pltval KHLP˙QBaseKWHP˙Q<˙WP˙Q˙WP˙QW
93 8 91 17 92 syl3anc KHLWHPAP˙WQAQ˙WP˙Q<˙WP˙Q˙WP˙QW
94 22 90 93 mpbir2and KHLWHPAP˙WQAQ˙WP˙Q<˙W