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 ) )