Metamath Proof Explorer

Theorem lhp2at0nle

Description: Inequality for 2 different atoms (or an atom and zero) under co-atom W . (Contributed by NM, 28-Jul-2013)

Ref Expression
Hypotheses lhp2at0nle.l 
|- .<_ = ( le ` K )
lhp2at0nle.j 
|- .\/ = ( join ` K )
lhp2at0nle.z 
|- .0. = ( 0. ` K )
lhp2at0nle.a 
|- A = ( Atoms ` K )
lhp2at0nle.h 
|- H = ( LHyp ` K )
Assertion lhp2at0nle 
|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> -. V .<_ ( P .\/ U ) )

Proof

Step Hyp Ref Expression
1 lhp2at0nle.l 
 |-  .<_ = ( le ` K )
2 lhp2at0nle.j 
 |-  .\/ = ( join ` K )
3 lhp2at0nle.z 
 |-  .0. = ( 0. ` K )
4 lhp2at0nle.a 
 |-  A = ( Atoms ` K )
5 lhp2at0nle.h 
 |-  H = ( LHyp ` K )
6 simpl1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U e. A ) -> ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) )
7 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U e. A ) -> U e. A )
8 simpl2r 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U e. A ) -> U .<_ W )
9 simpl3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U e. A ) -> ( V e. A /\ V .<_ W ) )
10 1 2 4 5 lhp2atnle 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( U e. A /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> -. V .<_ ( P .\/ U ) )
11 6 7 8 9 10 syl121anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U e. A ) -> -. V .<_ ( P .\/ U ) )
12 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> V .<_ W )
13 simp12r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> -. P .<_ W )
14 nbrne2 
 |-  ( ( V .<_ W /\ -. P .<_ W ) -> V =/= P )
15 12 13 14 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> V =/= P )
16 15 neneqd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> -. V = P )
17 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> K e. HL )
18 hlatl 
 |-  ( K e. HL -> K e. AtLat )
19 17 18 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> K e. AtLat )
20 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> V e. A )
21 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> P e. A )
22 1 4 atcmp 
 |-  ( ( K e. AtLat /\ V e. A /\ P e. A ) -> ( V .<_ P <-> V = P ) )
23 19 20 21 22 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( V .<_ P <-> V = P ) )
24 16 23 mtbird 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> -. V .<_ P )
25 24 adantr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U = .0. ) -> -. V .<_ P )
26 oveq2 
 |-  ( U = .0. -> ( P .\/ U ) = ( P .\/ .0. ) )
27 hlol 
 |-  ( K e. HL -> K e. OL )
28 17 27 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> K e. OL )
29 eqid 
 |-  ( Base ` K ) = ( Base ` K )
30 29 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
31 21 30 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> P e. ( Base ` K ) )
32 29 2 3 olj01 
 |-  ( ( K e. OL /\ P e. ( Base ` K ) ) -> ( P .\/ .0. ) = P )
33 28 31 32 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( P .\/ .0. ) = P )
34 26 33 sylan9eqr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U = .0. ) -> ( P .\/ U ) = P )
35 34 breq2d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U = .0. ) -> ( V .<_ ( P .\/ U ) <-> V .<_ P ) )
36 25 35 mtbird 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U = .0. ) -> -. V .<_ ( P .\/ U ) )
37 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( U e. A \/ U = .0. ) )
38 11 36 37 mpjaodan 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> -. V .<_ ( P .\/ U ) )