Metamath Proof Explorer


Theorem cdleme17b

Description: Lemma leading to cdleme17c . (Contributed by NM, 11-Oct-2012)

Ref Expression
Hypotheses cdleme17.l ˙=K
cdleme17.j ˙=joinK
cdleme17.m ˙=meetK
cdleme17.a A=AtomsK
cdleme17.h H=LHypK
cdleme17.u U=P˙Q˙W
cdleme17.f F=S˙U˙Q˙P˙S˙W
cdleme17.g G=P˙Q˙F˙P˙S˙W
cdleme17.c C=P˙S˙W
Assertion cdleme17b KHLWHPA¬P˙WQASA¬S˙P˙Q¬C˙P˙Q

Proof

Step Hyp Ref Expression
1 cdleme17.l ˙=K
2 cdleme17.j ˙=joinK
3 cdleme17.m ˙=meetK
4 cdleme17.a A=AtomsK
5 cdleme17.h H=LHypK
6 cdleme17.u U=P˙Q˙W
7 cdleme17.f F=S˙U˙Q˙P˙S˙W
8 cdleme17.g G=P˙Q˙F˙P˙S˙W
9 cdleme17.c C=P˙S˙W
10 simp33 KHLWHPA¬P˙WQASA¬S˙P˙Q¬S˙P˙Q
11 eqid BaseK=BaseK
12 simpl1l KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QKHL
13 12 hllatd KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QKLat
14 simpl32 KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QSA
15 11 4 atbase SASBaseK
16 14 15 syl KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QSBaseK
17 simpl2l KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QPA
18 11 2 4 hlatjcl KHLPASAP˙SBaseK
19 12 17 14 18 syl3anc KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QP˙SBaseK
20 simpl31 KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QQA
21 11 2 4 hlatjcl KHLPAQAP˙QBaseK
22 12 17 20 21 syl3anc KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QP˙QBaseK
23 1 2 4 hlatlej2 KHLPASAS˙P˙S
24 12 17 14 23 syl3anc KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QS˙P˙S
25 simpl1r KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QWH
26 simpl2r KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙Q¬P˙W
27 1 2 3 4 5 9 cdleme8 KHLWHPA¬P˙WSAP˙C=P˙S
28 12 25 17 26 14 27 syl221anc KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QP˙C=P˙S
29 1 2 4 hlatlej1 KHLPAQAP˙P˙Q
30 12 17 20 29 syl3anc KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QP˙P˙Q
31 simpr KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QC˙P˙Q
32 11 4 atbase PAPBaseK
33 17 32 syl KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QPBaseK
34 11 2 3 4 5 9 cdleme9b KHLPASAWHCBaseK
35 12 17 14 25 34 syl13anc KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QCBaseK
36 11 1 2 latjle12 KLatPBaseKCBaseKP˙QBaseKP˙P˙QC˙P˙QP˙C˙P˙Q
37 13 33 35 22 36 syl13anc KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QP˙P˙QC˙P˙QP˙C˙P˙Q
38 30 31 37 mpbi2and KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QP˙C˙P˙Q
39 28 38 eqbrtrrd KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QP˙S˙P˙Q
40 11 1 13 16 19 22 24 39 lattrd KHLWHPA¬P˙WQASA¬S˙P˙QC˙P˙QS˙P˙Q
41 10 40 mtand KHLWHPA¬P˙WQASA¬S˙P˙Q¬C˙P˙Q