Metamath Proof Explorer


Theorem cdlemc3

Description: Part of proof of Lemma C in Crawley p. 113. (Contributed by NM, 26-May-2012)

Ref Expression
Hypotheses cdlemc3.l ˙=K
cdlemc3.j ˙=joinK
cdlemc3.m ˙=meetK
cdlemc3.a A=AtomsK
cdlemc3.h H=LHypK
cdlemc3.t T=LTrnKW
cdlemc3.r R=trLKW
Assertion cdlemc3 KHLWHFTPA¬P˙WQA¬Q˙WFP˙Q˙RFQ˙P˙FP

Proof

Step Hyp Ref Expression
1 cdlemc3.l ˙=K
2 cdlemc3.j ˙=joinK
3 cdlemc3.m ˙=meetK
4 cdlemc3.a A=AtomsK
5 cdlemc3.h H=LHypK
6 cdlemc3.t T=LTrnKW
7 cdlemc3.r R=trLKW
8 simpll KHLWHFTPA¬P˙WQA¬Q˙WKHL
9 simpl KHLWHFTPA¬P˙WQA¬Q˙WKHLWH
10 simpr1 KHLWHFTPA¬P˙WQA¬Q˙WFT
11 simpr2l KHLWHFTPA¬P˙WQA¬Q˙WPA
12 1 4 5 6 ltrnat KHLWHFTPAFPA
13 9 10 11 12 syl3anc KHLWHFTPA¬P˙WQA¬Q˙WFPA
14 simpr3l KHLWHFTPA¬P˙WQA¬Q˙WQA
15 eqid BaseK=BaseK
16 15 5 6 7 trlcl KHLWHFTRFBaseK
17 10 16 syldan KHLWHFTPA¬P˙WQA¬Q˙WRFBaseK
18 1 4 5 6 ltrnel KHLWHFTPA¬P˙WFPA¬FP˙W
19 18 3adant3r3 KHLWHFTPA¬P˙WQA¬Q˙WFPA¬FP˙W
20 1 4 5 6 7 trlnle KHLWHFTFPA¬FP˙W¬FP˙RF
21 9 10 19 20 syl3anc KHLWHFTPA¬P˙WQA¬Q˙W¬FP˙RF
22 15 1 2 4 hlexch2 KHLFPAQARFBaseK¬FP˙RFFP˙Q˙RFQ˙FP˙RF
23 8 13 14 17 21 22 syl131anc KHLWHFTPA¬P˙WQA¬Q˙WFP˙Q˙RFQ˙FP˙RF
24 1 2 4 5 6 7 trljat2 KHLWHFTPA¬P˙WFP˙RF=P˙FP
25 24 3adant3r3 KHLWHFTPA¬P˙WQA¬Q˙WFP˙RF=P˙FP
26 25 breq2d KHLWHFTPA¬P˙WQA¬Q˙WQ˙FP˙RFQ˙P˙FP
27 23 26 sylibd KHLWHFTPA¬P˙WQA¬Q˙WFP˙Q˙RFQ˙P˙FP