This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lhp2lt

Description: The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013)

Ref Expression
Hypotheses lhp2lt.l 
|- .<_ = ( le ` K )
lhp2lt.s 
|- .< = ( lt ` K )
lhp2lt.j 
|- .\/ = ( join ` K )
lhp2lt.a 
|- A = ( Atoms ` K )
lhp2lt.h 
|- H = ( LHyp ` K )
Assertion lhp2lt 
|- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( P .\/ Q ) .< W )

Proof

Step Hyp Ref Expression
1 lhp2lt.l 
 |-  .<_ = ( le ` K )
2 lhp2lt.s 
 |-  .< = ( lt ` K )
3 lhp2lt.j 
 |-  .\/ = ( join ` K )
4 lhp2lt.a 
 |-  A = ( Atoms ` K )
5 lhp2lt.h 
 |-  H = ( LHyp ` K )
6 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> P .<_ W )
7 simp3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> Q .<_ W )
8 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> K e. HL )
9 8 hllatd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> K e. Lat )
10 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> P e. A )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 11 4 atbase 
 |-  ( P e. A -> P e. ( Base ` K ) )
13 10 12 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> P e. ( Base ` K ) )
14 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> Q e. A )
15 11 4 atbase 
 |-  ( Q e. A -> Q e. ( Base ` K ) )
16 14 15 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> Q e. ( Base ` K ) )
17 simp1r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> W e. H )
18 11 5 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
19 17 18 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> W e. ( Base ` K ) )
20 11 1 3 latjle12 
 |-  ( ( K e. Lat /\ ( P e. ( Base ` K ) /\ Q e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( P .<_ W /\ Q .<_ W ) <-> ( P .\/ Q ) .<_ W ) )
21 9 13 16 19 20 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( ( P .<_ W /\ Q .<_ W ) <-> ( P .\/ Q ) .<_ W ) )
22 6 7 21 mpbi2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( P .\/ Q ) .<_ W )
23 3 1 4 3dim2 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
24 8 10 14 23 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) )
25 simp11l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> K e. HL )
26 hlop 
 |-  ( K e. HL -> K e. OP )
27 25 26 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> K e. OP )
28 25 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> K e. Lat )
29 simp12l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> P e. A )
30 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> Q e. A )
31 11 3 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
32 25 29 30 31 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
33 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> r e. A )
34 11 4 atbase 
 |-  ( r e. A -> r e. ( Base ` K ) )
35 33 34 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> r e. ( Base ` K ) )
36 11 3 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ r e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ r ) e. ( Base ` K ) )
37 28 32 35 36 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> ( ( P .\/ Q ) .\/ r ) e. ( Base ` K ) )
38 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> s e. A )
39 11 4 atbase 
 |-  ( s e. A -> s e. ( Base ` K ) )
40 38 39 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> s e. ( Base ` K ) )
41 11 3 latjcl 
 |-  ( ( K e. Lat /\ ( ( P .\/ Q ) .\/ r ) e. ( Base ` K ) /\ s e. ( Base ` K ) ) -> ( ( ( P .\/ Q ) .\/ r ) .\/ s ) e. ( Base ` K ) )
42 28 37 40 41 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> ( ( ( P .\/ Q ) .\/ r ) .\/ s ) e. ( Base ` K ) )
43 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
44 eqid 
 |-  (
45 11 43 44 ncvr1 
 |-  ( ( K e. OP /\ ( ( ( P .\/ Q ) .\/ r ) .\/ s ) e. ( Base ` K ) ) -> -. ( 1. ` K ) (
46 27 42 45 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> -. ( 1. ` K ) (
47 eqid 
 |-  ( lub ` K ) = ( lub ` K )
48 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> K e. HL )
49 48 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> K e. Lat )
50 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> P e. A )
51 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> Q e. A )
52 48 50 51 31 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
53 simpr1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> r e. A )
54 53 34 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> r e. ( Base ` K ) )
55 49 52 54 36 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( ( P .\/ Q ) .\/ r ) e. ( Base ` K ) )
56 48 26 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> K e. OP )
57 eqid 
 |-  ( glb ` K ) = ( glb ` K )
58 11 47 57 op01dm 
 |-  ( K e. OP -> ( ( Base ` K ) e. dom ( lub ` K ) /\ ( Base ` K ) e. dom ( glb ` K ) ) )
59 58 simpld 
 |-  ( K e. OP -> ( Base ` K ) e. dom ( lub ` K ) )
60 56 59 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( Base ` K ) e. dom ( lub ` K ) )
61 11 47 1 43 48 55 60 ple1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( ( P .\/ Q ) .\/ r ) .<_ ( 1. ` K ) )
62 hlpos 
 |-  ( K e. HL -> K e. Poset )
63 48 62 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> K e. Poset )
64 11 43 op1cl 
 |-  ( K e. OP -> ( 1. ` K ) e. ( Base ` K ) )
65 56 64 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( 1. ` K ) e. ( Base ` K ) )
66 simpr2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> -. r .<_ ( P .\/ Q ) )
67 11 1 3 44 4 cvr1 
 |-  ( ( K e. HL /\ ( P .\/ Q ) e. ( Base ` K ) /\ r e. A ) -> ( -. r .<_ ( P .\/ Q ) <-> ( P .\/ Q ) (
68 48 52 53 67 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( -. r .<_ ( P .\/ Q ) <-> ( P .\/ Q ) (
69 66 68 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( P .\/ Q ) (
70 simpr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( P .\/ Q ) = W )
71 simpl1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> W e. H )
72 43 44 5 lhp1cvr 
 |-  ( ( K e. HL /\ W e. H ) -> W (
73 48 71 72 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> W (
74 70 73 eqbrtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( P .\/ Q ) (
75 11 1 44 cvrcmp 
 |-  ( ( K e. Poset /\ ( ( ( P .\/ Q ) .\/ r ) e. ( Base ` K ) /\ ( 1. ` K ) e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) /\ ( ( P .\/ Q ) (  ( ( ( P .\/ Q ) .\/ r ) .<_ ( 1. ` K ) <-> ( ( P .\/ Q ) .\/ r ) = ( 1. ` K ) ) )
76 63 55 65 52 69 74 75 syl132anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( ( ( P .\/ Q ) .\/ r ) .<_ ( 1. ` K ) <-> ( ( P .\/ Q ) .\/ r ) = ( 1. ` K ) ) )
77 61 76 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( ( P .\/ Q ) .\/ r ) = ( 1. ` K ) )
78 simpr2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> -. s .<_ ( ( P .\/ Q ) .\/ r ) )
79 simpr1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> s e. A )
80 11 1 3 44 4 cvr1 
 |-  ( ( K e. HL /\ ( ( P .\/ Q ) .\/ r ) e. ( Base ` K ) /\ s e. A ) -> ( -. s .<_ ( ( P .\/ Q ) .\/ r ) <-> ( ( P .\/ Q ) .\/ r ) (
81 48 55 79 80 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( -. s .<_ ( ( P .\/ Q ) .\/ r ) <-> ( ( P .\/ Q ) .\/ r ) (
82 78 81 mpbid 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( ( P .\/ Q ) .\/ r ) (
83 77 82 eqbrtrrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) /\ ( P .\/ Q ) = W ) ) -> ( 1. ` K ) (
84 83 3exp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( ( r e. A /\ s e. A ) -> ( ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) -> ( ( P .\/ Q ) = W -> ( 1. ` K ) (
85 84 3imp 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> ( ( P .\/ Q ) = W -> ( 1. ` K ) (
86 85 necon3bd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> ( -. ( 1. ` K ) (  ( P .\/ Q ) =/= W ) )
87 46 86 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) /\ ( r e. A /\ s e. A ) /\ ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) ) -> ( P .\/ Q ) =/= W )
88 87 3exp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( ( r e. A /\ s e. A ) -> ( ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) -> ( P .\/ Q ) =/= W ) ) )
89 88 rexlimdvv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( E. r e. A E. s e. A ( -. r .<_ ( P .\/ Q ) /\ -. s .<_ ( ( P .\/ Q ) .\/ r ) ) -> ( P .\/ Q ) =/= W ) )
90 24 89 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( P .\/ Q ) =/= W )
91 8 10 14 31 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
92 1 2 pltval 
 |-  ( ( K e. HL /\ ( P .\/ Q ) e. ( Base ` K ) /\ W e. H ) -> ( ( P .\/ Q ) .< W <-> ( ( P .\/ Q ) .<_ W /\ ( P .\/ Q ) =/= W ) ) )
93 8 91 17 92 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( ( P .\/ Q ) .< W <-> ( ( P .\/ Q ) .<_ W /\ ( P .\/ Q ) =/= W ) ) )
94 22 90 93 mpbir2and 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( P .\/ Q ) .< W )