Metamath Proof Explorer


Theorem cdlemc2

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

Ref Expression
Hypotheses cdlemc2.l ˙=K
cdlemc2.j ˙=joinK
cdlemc2.m ˙=meetK
cdlemc2.a A=AtomsK
cdlemc2.h H=LHypK
cdlemc2.t T=LTrnKW
Assertion cdlemc2 KHLWHFTPA¬P˙WQA¬Q˙WFQ˙FP˙P˙Q˙W

Proof

Step Hyp Ref Expression
1 cdlemc2.l ˙=K
2 cdlemc2.j ˙=joinK
3 cdlemc2.m ˙=meetK
4 cdlemc2.a A=AtomsK
5 cdlemc2.h H=LHypK
6 cdlemc2.t T=LTrnKW
7 simp1l KHLWHFTPA¬P˙WQA¬Q˙WKHL
8 simp3ll KHLWHFTPA¬P˙WQA¬Q˙WPA
9 simp3rl KHLWHFTPA¬P˙WQA¬Q˙WQA
10 1 2 4 hlatlej2 KHLPAQAQ˙P˙Q
11 7 8 9 10 syl3anc KHLWHFTPA¬P˙WQA¬Q˙WQ˙P˙Q
12 simp1 KHLWHFTPA¬P˙WQA¬Q˙WKHLWH
13 eqid BaseK=BaseK
14 13 4 atbase QAQBaseK
15 9 14 syl KHLWHFTPA¬P˙WQA¬Q˙WQBaseK
16 simp3l KHLWHFTPA¬P˙WQA¬Q˙WPA¬P˙W
17 13 1 2 3 4 5 cdlemc1 KHLWHQBaseKPA¬P˙WP˙P˙Q˙W=P˙Q
18 12 15 16 17 syl3anc KHLWHFTPA¬P˙WQA¬Q˙WP˙P˙Q˙W=P˙Q
19 11 18 breqtrrd KHLWHFTPA¬P˙WQA¬Q˙WQ˙P˙P˙Q˙W
20 simp2 KHLWHFTPA¬P˙WQA¬Q˙WFT
21 7 hllatd KHLWHFTPA¬P˙WQA¬Q˙WKLat
22 13 4 atbase PAPBaseK
23 8 22 syl KHLWHFTPA¬P˙WQA¬Q˙WPBaseK
24 13 2 latjcl KLatPBaseKQBaseKP˙QBaseK
25 21 23 15 24 syl3anc KHLWHFTPA¬P˙WQA¬Q˙WP˙QBaseK
26 simp1r KHLWHFTPA¬P˙WQA¬Q˙WWH
27 13 5 lhpbase WHWBaseK
28 26 27 syl KHLWHFTPA¬P˙WQA¬Q˙WWBaseK
29 13 3 latmcl KLatP˙QBaseKWBaseKP˙Q˙WBaseK
30 21 25 28 29 syl3anc KHLWHFTPA¬P˙WQA¬Q˙WP˙Q˙WBaseK
31 13 2 latjcl KLatPBaseKP˙Q˙WBaseKP˙P˙Q˙WBaseK
32 21 23 30 31 syl3anc KHLWHFTPA¬P˙WQA¬Q˙WP˙P˙Q˙WBaseK
33 13 1 5 6 ltrnle KHLWHFTQBaseKP˙P˙Q˙WBaseKQ˙P˙P˙Q˙WFQ˙FP˙P˙Q˙W
34 12 20 15 32 33 syl112anc KHLWHFTPA¬P˙WQA¬Q˙WQ˙P˙P˙Q˙WFQ˙FP˙P˙Q˙W
35 19 34 mpbid KHLWHFTPA¬P˙WQA¬Q˙WFQ˙FP˙P˙Q˙W
36 13 2 5 6 ltrnj KHLWHFTPBaseKP˙Q˙WBaseKFP˙P˙Q˙W=FP˙FP˙Q˙W
37 12 20 23 30 36 syl112anc KHLWHFTPA¬P˙WQA¬Q˙WFP˙P˙Q˙W=FP˙FP˙Q˙W
38 13 1 3 latmle2 KLatP˙QBaseKWBaseKP˙Q˙W˙W
39 21 25 28 38 syl3anc KHLWHFTPA¬P˙WQA¬Q˙WP˙Q˙W˙W
40 13 1 5 6 ltrnval1 KHLWHFTP˙Q˙WBaseKP˙Q˙W˙WFP˙Q˙W=P˙Q˙W
41 12 20 30 39 40 syl112anc KHLWHFTPA¬P˙WQA¬Q˙WFP˙Q˙W=P˙Q˙W
42 41 oveq2d KHLWHFTPA¬P˙WQA¬Q˙WFP˙FP˙Q˙W=FP˙P˙Q˙W
43 37 42 eqtrd KHLWHFTPA¬P˙WQA¬Q˙WFP˙P˙Q˙W=FP˙P˙Q˙W
44 35 43 breqtrd KHLWHFTPA¬P˙WQA¬Q˙WFQ˙FP˙P˙Q˙W