Metamath Proof Explorer


Theorem cdlemd3

Description: Part of proof of Lemma D in Crawley p. 113. The R =/= P requirement is not mentioned in their proof. (Contributed by NM, 29-May-2012)

Ref Expression
Hypotheses cdlemd3.l ˙=K
cdlemd3.j ˙=joinK
cdlemd3.a A=AtomsK
cdlemd3.h H=LHypK
Assertion cdlemd3 KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙Q¬R˙P˙S

Proof

Step Hyp Ref Expression
1 cdlemd3.l ˙=K
2 cdlemd3.j ˙=joinK
3 cdlemd3.a A=AtomsK
4 cdlemd3.h H=LHypK
5 simp33 KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙Q¬S˙P˙Q
6 simp1l KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QKHL
7 simp31 KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QRA
8 simp32 KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QSA
9 simp21l KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QPA
10 simp233 KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QRP
11 1 2 3 hlatexch1 KHLRASAPARPR˙P˙SS˙P˙R
12 6 7 8 9 10 11 syl131anc KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QR˙P˙SS˙P˙R
13 simp22l KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QQA
14 1 2 3 hlatlej1 KHLPAQAP˙P˙Q
15 6 9 13 14 syl3anc KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QP˙P˙Q
16 simp232 KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QR˙P˙Q
17 6 hllatd KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QKLat
18 eqid BaseK=BaseK
19 18 3 atbase PAPBaseK
20 9 19 syl KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QPBaseK
21 18 3 atbase RARBaseK
22 7 21 syl KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QRBaseK
23 18 3 atbase QAQBaseK
24 13 23 syl KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QQBaseK
25 18 2 latjcl KLatPBaseKQBaseKP˙QBaseK
26 17 20 24 25 syl3anc KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QP˙QBaseK
27 18 1 2 latjle12 KLatPBaseKRBaseKP˙QBaseKP˙P˙QR˙P˙QP˙R˙P˙Q
28 17 20 22 26 27 syl13anc KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QP˙P˙QR˙P˙QP˙R˙P˙Q
29 15 16 28 mpbi2and KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QP˙R˙P˙Q
30 18 3 atbase SASBaseK
31 8 30 syl KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QSBaseK
32 18 2 latjcl KLatPBaseKRBaseKP˙RBaseK
33 17 20 22 32 syl3anc KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QP˙RBaseK
34 18 1 lattr KLatSBaseKP˙RBaseKP˙QBaseKS˙P˙RP˙R˙P˙QS˙P˙Q
35 17 31 33 26 34 syl13anc KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QS˙P˙RP˙R˙P˙QS˙P˙Q
36 29 35 mpan2d KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QS˙P˙RS˙P˙Q
37 12 36 syld KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙QR˙P˙SS˙P˙Q
38 5 37 mtod KHLWHPA¬P˙WQA¬Q˙WPQR˙P˙QRPRASA¬S˙P˙Q¬R˙P˙S