Metamath Proof Explorer


Theorem cdleme3b

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . (Contributed by NM, 6-Jun-2012)

Ref Expression
Hypotheses cdleme1.l ˙=K
cdleme1.j ˙=joinK
cdleme1.m ˙=meetK
cdleme1.a A=AtomsK
cdleme1.h H=LHypK
cdleme1.u U=P˙Q˙W
cdleme1.f F=R˙U˙Q˙P˙R˙W
Assertion cdleme3b KHLWHPA¬P˙WQAPQRA¬R˙WFR

Proof

Step Hyp Ref Expression
1 cdleme1.l ˙=K
2 cdleme1.j ˙=joinK
3 cdleme1.m ˙=meetK
4 cdleme1.a A=AtomsK
5 cdleme1.h H=LHypK
6 cdleme1.u U=P˙Q˙W
7 cdleme1.f F=R˙U˙Q˙P˙R˙W
8 simpll KHLWHPA¬P˙WQAPQRA¬R˙WKHL
9 simpr3l KHLWHPA¬P˙WQAPQRA¬R˙WRA
10 eqid BaseK=BaseK
11 10 4 atbase RARBaseK
12 9 11 syl KHLWHPA¬P˙WQAPQRA¬R˙WRBaseK
13 hllat KHLKLat
14 13 ad2antrr KHLWHPA¬P˙WQAPQRA¬R˙WKLat
15 1 2 3 4 5 6 lhpat2 KHLWHPA¬P˙WQAPQUA
16 15 3adant3r3 KHLWHPA¬P˙WQAPQRA¬R˙WUA
17 10 4 atbase UAUBaseK
18 16 17 syl KHLWHPA¬P˙WQAPQRA¬R˙WUBaseK
19 10 2 latjcl KLatRBaseKUBaseKR˙UBaseK
20 14 12 18 19 syl3anc KHLWHPA¬P˙WQAPQRA¬R˙WR˙UBaseK
21 simpr2l KHLWHPA¬P˙WQAPQRA¬R˙WQA
22 10 4 atbase QAQBaseK
23 21 22 syl KHLWHPA¬P˙WQAPQRA¬R˙WQBaseK
24 simpr1l KHLWHPA¬P˙WQAPQRA¬R˙WPA
25 10 4 atbase PAPBaseK
26 24 25 syl KHLWHPA¬P˙WQAPQRA¬R˙WPBaseK
27 10 2 latjcl KLatPBaseKRBaseKP˙RBaseK
28 14 26 12 27 syl3anc KHLWHPA¬P˙WQAPQRA¬R˙WP˙RBaseK
29 10 5 lhpbase WHWBaseK
30 29 ad2antlr KHLWHPA¬P˙WQAPQRA¬R˙WWBaseK
31 10 3 latmcl KLatP˙RBaseKWBaseKP˙R˙WBaseK
32 14 28 30 31 syl3anc KHLWHPA¬P˙WQAPQRA¬R˙WP˙R˙WBaseK
33 10 2 latjcl KLatQBaseKP˙R˙WBaseKQ˙P˙R˙WBaseK
34 14 23 32 33 syl3anc KHLWHPA¬P˙WQAPQRA¬R˙WQ˙P˙R˙WBaseK
35 10 3 latmcl KLatR˙UBaseKQ˙P˙R˙WBaseKR˙U˙Q˙P˙R˙WBaseK
36 14 20 34 35 syl3anc KHLWHPA¬P˙WQAPQRA¬R˙WR˙U˙Q˙P˙R˙WBaseK
37 7 36 eqeltrid KHLWHPA¬P˙WQAPQRA¬R˙WFBaseK
38 10 2 latjcl KLatRBaseKFBaseKR˙FBaseK
39 14 12 37 38 syl3anc KHLWHPA¬P˙WQAPQRA¬R˙WR˙FBaseK
40 10 2 latjcl KLatPBaseKQBaseKP˙QBaseK
41 14 26 23 40 syl3anc KHLWHPA¬P˙WQAPQRA¬R˙WP˙QBaseK
42 10 1 3 latmle2 KLatP˙QBaseKWBaseKP˙Q˙W˙W
43 14 41 30 42 syl3anc KHLWHPA¬P˙WQAPQRA¬R˙WP˙Q˙W˙W
44 6 43 eqbrtrid KHLWHPA¬P˙WQAPQRA¬R˙WU˙W
45 simpr3r KHLWHPA¬P˙WQAPQRA¬R˙W¬R˙W
46 nbrne2 U˙W¬R˙WUR
47 44 45 46 syl2anc KHLWHPA¬P˙WQAPQRA¬R˙WUR
48 47 necomd KHLWHPA¬P˙WQAPQRA¬R˙WRU
49 eqid K=K
50 2 49 4 atcvr1 KHLRAUARURKR˙U
51 8 9 16 50 syl3anc KHLWHPA¬P˙WQAPQRA¬R˙WRURKR˙U
52 48 51 mpbid KHLWHPA¬P˙WQAPQRA¬R˙WRKR˙U
53 simpr3 KHLWHPA¬P˙WQAPQRA¬R˙WRA¬R˙W
54 24 21 53 3jca KHLWHPA¬P˙WQAPQRA¬R˙WPAQARA¬R˙W
55 1 2 3 4 5 6 7 cdleme1 KHLWHPAQARA¬R˙WR˙F=R˙U
56 54 55 syldan KHLWHPA¬P˙WQAPQRA¬R˙WR˙F=R˙U
57 52 56 breqtrrd KHLWHPA¬P˙WQAPQRA¬R˙WRKR˙F
58 10 49 cvrne KHLRBaseKR˙FBaseKRKR˙FRR˙F
59 8 12 39 57 58 syl31anc KHLWHPA¬P˙WQAPQRA¬R˙WRR˙F
60 oveq2 F=RR˙F=R˙R
61 60 adantl KHLWHPA¬P˙WQAPQRA¬R˙WF=RR˙F=R˙R
62 2 4 hlatjidm KHLRAR˙R=R
63 8 9 62 syl2anc KHLWHPA¬P˙WQAPQRA¬R˙WR˙R=R
64 63 adantr KHLWHPA¬P˙WQAPQRA¬R˙WF=RR˙R=R
65 61 64 eqtr2d KHLWHPA¬P˙WQAPQRA¬R˙WF=RR=R˙F
66 65 ex KHLWHPA¬P˙WQAPQRA¬R˙WF=RR=R˙F
67 66 necon3d KHLWHPA¬P˙WQAPQRA¬R˙WRR˙FFR
68 59 67 mpd KHLWHPA¬P˙WQAPQRA¬R˙WFR