Metamath Proof Explorer


Theorem cdleme11j

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 14-Jun-2012)

Ref Expression
Hypotheses cdleme11.l ˙=K
cdleme11.j ˙=joinK
cdleme11.m ˙=meetK
cdleme11.a A=AtomsK
cdleme11.h H=LHypK
cdleme11.u U=P˙Q˙W
cdleme11.c C=P˙S˙W
cdleme11.d D=P˙T˙W
cdleme11.f F=S˙U˙Q˙P˙S˙W
Assertion cdleme11j KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QC˙Q˙F

Proof

Step Hyp Ref Expression
1 cdleme11.l ˙=K
2 cdleme11.j ˙=joinK
3 cdleme11.m ˙=meetK
4 cdleme11.a A=AtomsK
5 cdleme11.h H=LHypK
6 cdleme11.u U=P˙Q˙W
7 cdleme11.c C=P˙S˙W
8 cdleme11.d D=P˙T˙W
9 cdleme11.f F=S˙U˙Q˙P˙S˙W
10 simp1l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QKHL
11 simp22l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QQA
12 1 2 3 4 5 6 9 cdleme3fa KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QFA
13 1 2 4 hlatlej2 KHLQAFAF˙Q˙F
14 10 11 12 13 syl3anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QF˙Q˙F
15 simp1 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QKHLWH
16 simp21l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QPA
17 simp22 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QQA¬Q˙W
18 simp23l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QSA
19 simp3l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QPQ
20 1 2 3 4 5 6 7 6 9 cdleme11g KHLWHPAQA¬Q˙WSAPQQ˙F=Q˙C
21 15 16 17 18 19 20 syl131anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QQ˙F=Q˙C
22 14 21 breqtrd KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QF˙Q˙C
23 simp21 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QPA¬P˙W
24 simp3r KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙Q¬S˙P˙Q
25 1 2 3 4 cdleme00a KHLPAQASA¬S˙P˙QSP
26 10 16 11 18 24 25 syl131anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QSP
27 26 necomd KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QPS
28 1 2 3 4 5 7 cdleme9a KHLWHPA¬P˙WSAPSCA
29 15 23 18 27 28 syl112anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QCA
30 simp3 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QPQ¬S˙P˙Q
31 1 2 3 4 5 6 7 6 9 cdleme11h KHLWHPA¬P˙WQA¬Q˙WSAPQ¬S˙P˙QFQ
32 15 23 17 18 30 31 syl131anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QFQ
33 1 2 4 hlatexch1 KHLFACAQAFQF˙Q˙CC˙Q˙F
34 10 12 29 11 32 33 syl131anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QF˙Q˙CC˙Q˙F
35 22 34 mpd KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QC˙Q˙F