Metamath Proof Explorer


Theorem cdlemd7

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 1-Jun-2012)

Ref Expression
Hypotheses cdlemd4.l ˙=K
cdlemd4.j ˙=joinK
cdlemd4.a A=AtomsK
cdlemd4.h H=LHypK
cdlemd4.t T=LTrnKW
Assertion cdlemd7 KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPFR=GR

Proof

Step Hyp Ref Expression
1 cdlemd4.l ˙=K
2 cdlemd4.j ˙=joinK
3 cdlemd4.a A=AtomsK
4 cdlemd4.h H=LHypK
5 cdlemd4.t T=LTrnKW
6 simp1 KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPKHLWHFTGTRA
7 simp2l KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPPA¬P˙W
8 simp2r KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPQA¬Q˙W
9 simp11l KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPKHL
10 9 hllatd KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPKLat
11 simp2rl KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPQA
12 eqid BaseK=BaseK
13 12 3 atbase QAQBaseK
14 11 13 syl KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPQBaseK
15 simp2ll KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPPA
16 12 3 atbase PAPBaseK
17 15 16 syl KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPPBaseK
18 simp11 KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPKHLWH
19 simp12l KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPFT
20 12 4 5 ltrncl KHLWHFTPBaseKFPBaseK
21 18 19 17 20 syl3anc KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPFPBaseK
22 simp3r KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FP¬Q˙P˙FP
23 12 1 2 latnlej1l KLatQBaseKPBaseKFPBaseK¬Q˙P˙FPQP
24 23 necomd KLatQBaseKPBaseKFPBaseK¬Q˙P˙FPPQ
25 10 14 17 21 22 24 syl131anc KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPPQ
26 simp3l KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPFP=GP
27 simp12 KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPFTGT
28 1 2 3 4 5 cdlemd6 KHLWHFTGTPA¬P˙WQA¬Q˙W¬Q˙P˙FPFP=GPFQ=GQ
29 18 27 7 8 22 26 28 syl231anc KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPFQ=GQ
30 1 2 3 4 5 cdlemd5 KHLWHFTGTRAPA¬P˙WQA¬Q˙WPQFP=GPFQ=GQFR=GR
31 6 7 8 25 26 29 30 syl132anc KHLWHFTGTRAPA¬P˙WQA¬Q˙WFP=GP¬Q˙P˙FPFR=GR