Metamath Proof Explorer


Theorem 2llnma1b

Description: Generalization of 2llnma1 . (Contributed by NM, 26-Apr-2013)

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

Proof

Step Hyp Ref Expression
1 2llnma1b.b B=BaseK
2 2llnma1b.l ˙=K
3 2llnma1b.j ˙=joinK
4 2llnma1b.m ˙=meetK
5 2llnma1b.a A=AtomsK
6 hllat KHLKLat
7 6 3ad2ant1 KHLXBPAQA¬Q˙P˙XKLat
8 simp22 KHLXBPAQA¬Q˙P˙XPA
9 1 5 atbase PAPB
10 8 9 syl KHLXBPAQA¬Q˙P˙XPB
11 simp21 KHLXBPAQA¬Q˙P˙XXB
12 1 2 3 latlej1 KLatPBXBP˙P˙X
13 7 10 11 12 syl3anc KHLXBPAQA¬Q˙P˙XP˙P˙X
14 simp23 KHLXBPAQA¬Q˙P˙XQA
15 1 5 atbase QAQB
16 14 15 syl KHLXBPAQA¬Q˙P˙XQB
17 1 2 3 latlej1 KLatPBQBP˙P˙Q
18 7 10 16 17 syl3anc KHLXBPAQA¬Q˙P˙XP˙P˙Q
19 1 3 latjcl KLatPBXBP˙XB
20 7 10 11 19 syl3anc KHLXBPAQA¬Q˙P˙XP˙XB
21 simp1 KHLXBPAQA¬Q˙P˙XKHL
22 1 3 5 hlatjcl KHLPAQAP˙QB
23 21 8 14 22 syl3anc KHLXBPAQA¬Q˙P˙XP˙QB
24 1 2 4 latlem12 KLatPBP˙XBP˙QBP˙P˙XP˙P˙QP˙P˙X˙P˙Q
25 7 10 20 23 24 syl13anc KHLXBPAQA¬Q˙P˙XP˙P˙XP˙P˙QP˙P˙X˙P˙Q
26 13 18 25 mpbi2and KHLXBPAQA¬Q˙P˙XP˙P˙X˙P˙Q
27 hlatl KHLKAtLat
28 27 3ad2ant1 KHLXBPAQA¬Q˙P˙XKAtLat
29 simp3 KHLXBPAQA¬Q˙P˙X¬Q˙P˙X
30 nbrne2 P˙P˙X¬Q˙P˙XPQ
31 13 29 30 syl2anc KHLXBPAQA¬Q˙P˙XPQ
32 1 3 latjcl KLatP˙XBQBP˙X˙QB
33 7 20 16 32 syl3anc KHLXBPAQA¬Q˙P˙XP˙X˙QB
34 1 2 3 latlej1 KLatP˙XBQBP˙X˙P˙X˙Q
35 7 20 16 34 syl3anc KHLXBPAQA¬Q˙P˙XP˙X˙P˙X˙Q
36 1 2 7 10 20 33 13 35 lattrd KHLXBPAQA¬Q˙P˙XP˙P˙X˙Q
37 1 2 3 4 5 cvrat3 KHLP˙XBPAQAPQ¬Q˙P˙XP˙P˙X˙QP˙X˙P˙QA
38 37 3impia KHLP˙XBPAQAPQ¬Q˙P˙XP˙P˙X˙QP˙X˙P˙QA
39 21 20 8 14 31 29 36 38 syl133anc KHLXBPAQA¬Q˙P˙XP˙X˙P˙QA
40 2 5 atcmp KAtLatPAP˙X˙P˙QAP˙P˙X˙P˙QP=P˙X˙P˙Q
41 28 8 39 40 syl3anc KHLXBPAQA¬Q˙P˙XP˙P˙X˙P˙QP=P˙X˙P˙Q
42 26 41 mpbid KHLXBPAQA¬Q˙P˙XP=P˙X˙P˙Q
43 42 eqcomd KHLXBPAQA¬Q˙P˙XP˙X˙P˙Q=P