Metamath Proof Explorer

Theorem cdlemg27a

Description: For use with case when ( P .\/ v ) ./\ ( Q .\/ ( RF ) ) or ( P .\/ v ) ./\ ( Q .\/ ( RF ) ) is zero, letting us establish -. z .<_ W /\ z .<_ ( P .\/ v ) via 4atex . TODO: Fix comment. (Contributed by NM, 28-May-2013)

Ref Expression
Hypotheses cdlemg12.l 
|- .<_ = ( le ` K )
cdlemg12.j 
|- .\/ = ( join ` K )
cdlemg12.m 
|- ./\ = ( meet ` K )
cdlemg12.a 
|- A = ( Atoms ` K )
cdlemg12.h 
|- H = ( LHyp ` K )
cdlemg12.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemg12b.r 
|- R = ( ( trL ` K ) ` W )
Assertion cdlemg27a 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> -. ( R ` F ) .<_ ( P .\/ z ) )

Proof

Step Hyp Ref Expression
1 cdlemg12.l 
 |-  .<_ = ( le ` K )
2 cdlemg12.j 
 |-  .\/ = ( join ` K )
3 cdlemg12.m 
 |-  ./\ = ( meet ` K )
4 cdlemg12.a 
 |-  A = ( Atoms ` K )
5 cdlemg12.h 
 |-  H = ( LHyp ` K )
6 cdlemg12.t 
 |-  T = ( ( LTrn ` K ) ` W )
7 cdlemg12b.r 
 |-  R = ( ( trL ` K ) ` W )
8 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( K e. HL /\ W e. H ) )
9 simp12 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( P e. A /\ -. P .<_ W ) )
10 simp31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> v =/= ( R ` F ) )
11 simp13 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( v e. A /\ v .<_ W ) )
12 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> F e. T )
13 simp33 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( F ` P ) =/= P )
14 1 4 5 6 7 trlat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F e. T /\ ( F ` P ) =/= P ) ) -> ( R ` F ) e. A )
15 8 9 12 13 14 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( R ` F ) e. A )
16 1 5 6 7 trlle 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) .<_ W )
17 8 12 16 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( R ` F ) .<_ W )
18 1 2 4 5 lhp2atnle 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ v =/= ( R ` F ) ) /\ ( v e. A /\ v .<_ W ) /\ ( ( R ` F ) e. A /\ ( R ` F ) .<_ W ) ) -> -. ( R ` F ) .<_ ( P .\/ v ) )
19 8 9 10 11 15 17 18 syl312anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> -. ( R ` F ) .<_ ( P .\/ v ) )
20 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> K e. HL )
21 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> P e. A )
22 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> v e. A )
23 1 2 4 hlatlej1 
 |-  ( ( K e. HL /\ P e. A /\ v e. A ) -> P .<_ ( P .\/ v ) )
24 20 21 22 23 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> P .<_ ( P .\/ v ) )
25 simp32 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> z .<_ ( P .\/ v ) )
26 20 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> K e. Lat )
27 eqid 
 |-  ( Base ` K ) = ( Base ` K )
28 27 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
29 21 28 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> P e. ( Base ` K ) )
30 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> z e. A )
31 27 4 atbase 
 |-  ( z e. A -> z e. ( Base ` K ) )
32 30 31 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> z e. ( Base ` K ) )
33 27 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ v e. A ) -> ( P .\/ v ) e. ( Base ` K ) )
34 20 21 22 33 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( P .\/ v ) e. ( Base ` K ) )
35 27 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ z e. ( Base ` K ) /\ ( P .\/ v ) e. ( Base ` K ) ) ) -> ( ( P .<_ ( P .\/ v ) /\ z .<_ ( P .\/ v ) ) <-> ( P .\/ z ) .<_ ( P .\/ v ) ) )
36 26 29 32 34 35 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( ( P .<_ ( P .\/ v ) /\ z .<_ ( P .\/ v ) ) <-> ( P .\/ z ) .<_ ( P .\/ v ) ) )
37 24 25 36 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( P .\/ z ) .<_ ( P .\/ v ) )
38 27 4 atbase 
 |-  ( ( R ` F ) e. A -> ( R ` F ) e. ( Base ` K ) )
39 15 38 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( R ` F ) e. ( Base ` K ) )
40 27 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ z e. A ) -> ( P .\/ z ) e. ( Base ` K ) )
41 20 21 30 40 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( P .\/ z ) e. ( Base ` K ) )
42 27 1 lattr 
 |-  ( ( K e. Lat /\ ( ( R ` F ) e. ( Base ` K ) /\ ( P .\/ z ) e. ( Base ` K ) /\ ( P .\/ v ) e. ( Base ` K ) ) ) -> ( ( ( R ` F ) .<_ ( P .\/ z ) /\ ( P .\/ z ) .<_ ( P .\/ v ) ) -> ( R ` F ) .<_ ( P .\/ v ) ) )
43 26 39 41 34 42 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( ( ( R ` F ) .<_ ( P .\/ z ) /\ ( P .\/ z ) .<_ ( P .\/ v ) ) -> ( R ` F ) .<_ ( P .\/ v ) ) )
44 37 43 mpan2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> ( ( R ` F ) .<_ ( P .\/ z ) -> ( R ` F ) .<_ ( P .\/ v ) ) )
45 19 44 mtod 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( v e. A /\ v .<_ W ) ) /\ ( z e. A /\ F e. T ) /\ ( v =/= ( R ` F ) /\ z .<_ ( P .\/ v ) /\ ( F ` P ) =/= P ) ) -> -. ( R ` F ) .<_ ( P .\/ z ) )