Metamath Proof Explorer


Theorem 2atjm

Description: The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012)

Ref Expression
Hypotheses 2atjm.b B=BaseK
2atjm.l ˙=K
2atjm.j ˙=joinK
2atjm.m ˙=meetK
2atjm.a A=AtomsK
Assertion 2atjm KHLPAQAXBP˙X¬Q˙XP˙Q˙X=P

Proof

Step Hyp Ref Expression
1 2atjm.b B=BaseK
2 2atjm.l ˙=K
3 2atjm.j ˙=joinK
4 2atjm.m ˙=meetK
5 2atjm.a A=AtomsK
6 hllat KHLKLat
7 6 3ad2ant1 KHLPAQAXBP˙X¬Q˙XKLat
8 simp21 KHLPAQAXBP˙X¬Q˙XPA
9 1 5 atbase PAPB
10 8 9 syl KHLPAQAXBP˙X¬Q˙XPB
11 simp22 KHLPAQAXBP˙X¬Q˙XQA
12 1 5 atbase QAQB
13 11 12 syl KHLPAQAXBP˙X¬Q˙XQB
14 1 2 3 latlej1 KLatPBQBP˙P˙Q
15 7 10 13 14 syl3anc KHLPAQAXBP˙X¬Q˙XP˙P˙Q
16 simp3l KHLPAQAXBP˙X¬Q˙XP˙X
17 simp1 KHLPAQAXBP˙X¬Q˙XKHL
18 1 3 5 hlatjcl KHLPAQAP˙QB
19 17 8 11 18 syl3anc KHLPAQAXBP˙X¬Q˙XP˙QB
20 simp23 KHLPAQAXBP˙X¬Q˙XXB
21 1 2 4 latlem12 KLatPBP˙QBXBP˙P˙QP˙XP˙P˙Q˙X
22 7 10 19 20 21 syl13anc KHLPAQAXBP˙X¬Q˙XP˙P˙QP˙XP˙P˙Q˙X
23 15 16 22 mpbi2and KHLPAQAXBP˙X¬Q˙XP˙P˙Q˙X
24 hlatl KHLKAtLat
25 24 3ad2ant1 KHLPAQAXBP˙X¬Q˙XKAtLat
26 1 4 latmcom KLatP˙QBXBP˙Q˙X=X˙P˙Q
27 7 19 20 26 syl3anc KHLPAQAXBP˙X¬Q˙XP˙Q˙X=X˙P˙Q
28 20 8 11 3jca KHLPAQAXBP˙X¬Q˙XXBPAQA
29 nbrne2 P˙X¬Q˙XPQ
30 29 3ad2ant3 KHLPAQAXBP˙X¬Q˙XPQ
31 simp3r KHLPAQAXBP˙X¬Q˙X¬Q˙X
32 1 3 latjcl KLatXBQBX˙QB
33 7 20 13 32 syl3anc KHLPAQAXBP˙X¬Q˙XX˙QB
34 1 2 3 latlej1 KLatXBQBX˙X˙Q
35 7 20 13 34 syl3anc KHLPAQAXBP˙X¬Q˙XX˙X˙Q
36 1 2 7 10 20 33 16 35 lattrd KHLPAQAXBP˙X¬Q˙XP˙X˙Q
37 1 2 3 4 5 cvrat3 KHLXBPAQAPQ¬Q˙XP˙X˙QX˙P˙QA
38 37 imp KHLXBPAQAPQ¬Q˙XP˙X˙QX˙P˙QA
39 17 28 30 31 36 38 syl23anc KHLPAQAXBP˙X¬Q˙XX˙P˙QA
40 27 39 eqeltrd KHLPAQAXBP˙X¬Q˙XP˙Q˙XA
41 2 5 atcmp KAtLatPAP˙Q˙XAP˙P˙Q˙XP=P˙Q˙X
42 25 8 40 41 syl3anc KHLPAQAXBP˙X¬Q˙XP˙P˙Q˙XP=P˙Q˙X
43 23 42 mpbid KHLPAQAXBP˙X¬Q˙XP=P˙Q˙X
44 43 eqcomd KHLPAQAXBP˙X¬Q˙XP˙Q˙X=P