Metamath Proof Explorer


Theorem cdleme22g

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 6th and 7th lines on p. 115. F , G represent f(s), f(t) respectively. If s <_ t \/ v and -. s <_ p \/ q, then f(s) <_ f(t) \/ v. (Contributed by NM, 6-Dec-2012)

Ref Expression
Hypotheses cdleme22.l ˙=K
cdleme22.j ˙=joinK
cdleme22.m ˙=meetK
cdleme22.a A=AtomsK
cdleme22.h H=LHypK
cdleme22g.u U=P˙Q˙W
cdleme22g.f F=S˙U˙Q˙P˙S˙W
cdleme22g.g G=T˙U˙Q˙P˙T˙W
Assertion cdleme22g KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WF˙G˙V

Proof

Step Hyp Ref Expression
1 cdleme22.l ˙=K
2 cdleme22.j ˙=joinK
3 cdleme22.m ˙=meetK
4 cdleme22.a A=AtomsK
5 cdleme22.h H=LHypK
6 cdleme22g.u U=P˙Q˙W
7 cdleme22g.f F=S˙U˙Q˙P˙S˙W
8 cdleme22g.g G=T˙U˙Q˙P˙T˙W
9 simp11l KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WKHL
10 9 hllatd KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WKLat
11 simp11 KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WKHLWH
12 simp2l KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WPA¬P˙W
13 simp2r KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WQA¬Q˙W
14 simp31 KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WSA¬S˙W
15 simp133 KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WPQ
16 simp132 KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙W¬S˙P˙Q
17 1 2 3 4 5 6 7 cdleme3fa KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QFA
18 11 12 13 14 15 16 17 syl132anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WFA
19 simp12 KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WTA¬T˙W
20 simp131 KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙W¬T˙P˙Q
21 1 2 3 4 5 6 8 cdleme3fa KHLWHPA¬P˙WQA¬Q˙WTA¬T˙WPQ¬T˙P˙QGA
22 11 12 13 19 15 20 21 syl132anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WGA
23 eqid BaseK=BaseK
24 23 2 4 hlatjcl KHLFAGAF˙GBaseK
25 9 18 22 24 syl3anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WF˙GBaseK
26 simp11r KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WWH
27 23 5 lhpbase WHWBaseK
28 26 27 syl KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WWBaseK
29 23 1 3 latmle1 KLatF˙GBaseKWBaseKF˙G˙W˙F˙G
30 10 25 28 29 syl3anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WF˙G˙W˙F˙G
31 simp33 KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WVAV˙W
32 simp32 KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WSTS˙T˙V
33 1 2 3 4 5 cdleme22d KHLWHSA¬S˙WTA¬T˙WVAV˙WSTS˙T˙VV=S˙T˙W
34 11 14 19 31 32 33 syl131anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WV=S˙T˙W
35 simp32l KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WST
36 15 35 jca KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WPQST
37 1 2 3 4 5 6 7 8 cdleme16 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WTA¬T˙WPQST¬S˙P˙Q¬T˙P˙QS˙T˙W=F˙G˙W
38 11 12 13 14 19 36 16 20 37 syl332anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WS˙T˙W=F˙G˙W
39 34 38 eqtr2d KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WF˙G˙W=V
40 2 4 hlatjcom KHLFAGAF˙G=G˙F
41 9 18 22 40 syl3anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WF˙G=G˙F
42 30 39 41 3brtr3d KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WV˙G˙F
43 hlcvl KHLKCvLat
44 9 43 syl KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WKCvLat
45 simp33l KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WVA
46 simp33r KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WV˙W
47 1 2 3 4 5 6 8 cdleme3 KHLWHPA¬P˙WQA¬Q˙WTA¬T˙WPQ¬T˙P˙Q¬G˙W
48 11 12 13 19 15 20 47 syl132anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙W¬G˙W
49 nbrne2 V˙W¬G˙WVG
50 46 48 49 syl2anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WVG
51 1 2 4 cvlatexch1 KCvLatVAFAGAVGV˙G˙FF˙G˙V
52 44 45 18 22 50 51 syl131anc KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WV˙G˙FF˙G˙V
53 42 52 mpd KHLWHTA¬T˙W¬T˙P˙Q¬S˙P˙QPQPA¬P˙WQA¬Q˙WSA¬S˙WSTS˙T˙VVAV˙WF˙G˙V