Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdleme22b Structured version   Unicode version

Theorem cdleme22b 33827
Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t  \/ v =/= p  \/ q and s  <_ p  \/ q implies  -. t  <_ p  \/ q. (Contributed by NM, 2-Dec-2012.)
Hypotheses
Ref Expression
cdleme22.l  |-  .<_  =  ( le `  K )
cdleme22.j  |-  .\/  =  ( join `  K )
cdleme22.m  |-  ./\  =  ( meet `  K )
cdleme22.a  |-  A  =  ( Atoms `  K )
cdleme22.h  |-  H  =  ( LHyp `  K
)
Assertion
Ref Expression
cdleme22b  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  -.  T  .<_  ( P 
.\/  Q ) )

Proof of Theorem cdleme22b
StepHypRef Expression
1 simp1l 1029 . . . . 5  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  K  e.  HL )
2 simp1r1 1101 . . . . . 6  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  S  e.  A )
3 simp1r2 1102 . . . . . 6  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  T  e.  A )
4 simp1r3 1103 . . . . . 6  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  S  =/=  T )
5 cdleme22.j . . . . . . 7  |-  .\/  =  ( join `  K )
6 cdleme22.a . . . . . . 7  |-  A  =  ( Atoms `  K )
7 eqid 2422 . . . . . . 7  |-  ( LLines `  K )  =  (
LLines `  K )
85, 6, 7llni2 32996 . . . . . 6  |-  ( ( ( K  e.  HL  /\  S  e.  A  /\  T  e.  A )  /\  S  =/=  T
)  ->  ( S  .\/  T )  e.  (
LLines `  K ) )
91, 2, 3, 4, 8syl31anc 1267 . . . . 5  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( S  .\/  T
)  e.  ( LLines `  K ) )
106, 7llnneat 32998 . . . . 5  |-  ( ( K  e.  HL  /\  ( S  .\/  T )  e.  ( LLines `  K
) )  ->  -.  ( S  .\/  T )  e.  A )
111, 9, 10syl2anc 665 . . . 4  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  -.  ( S  .\/  T
)  e.  A )
12 eqid 2422 . . . . . 6  |-  ( 0.
`  K )  =  ( 0. `  K
)
1312, 7llnn0 33000 . . . . 5  |-  ( ( K  e.  HL  /\  ( S  .\/  T )  e.  ( LLines `  K
) )  ->  ( S  .\/  T )  =/=  ( 0. `  K
) )
141, 9, 13syl2anc 665 . . . 4  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( S  .\/  T
)  =/=  ( 0.
`  K ) )
1511, 14jca 534 . . 3  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( -.  ( S 
.\/  T )  e.  A  /\  ( S 
.\/  T )  =/=  ( 0. `  K
) ) )
16 df-ne 2620 . . . . 5  |-  ( ( S  .\/  T )  =/=  ( 0. `  K )  <->  -.  ( S  .\/  T )  =  ( 0. `  K
) )
1716anbi2i 698 . . . 4  |-  ( ( -.  ( S  .\/  T )  e.  A  /\  ( S  .\/  T )  =/=  ( 0. `  K ) )  <->  ( -.  ( S  .\/  T )  e.  A  /\  -.  ( S  .\/  T )  =  ( 0. `  K ) ) )
18 pm4.56 497 . . . 4  |-  ( ( -.  ( S  .\/  T )  e.  A  /\  -.  ( S  .\/  T
)  =  ( 0.
`  K ) )  <->  -.  ( ( S  .\/  T )  e.  A  \/  ( S  .\/  T )  =  ( 0. `  K ) ) )
1917, 18bitri 252 . . 3  |-  ( ( -.  ( S  .\/  T )  e.  A  /\  ( S  .\/  T )  =/=  ( 0. `  K ) )  <->  -.  (
( S  .\/  T
)  e.  A  \/  ( S  .\/  T )  =  ( 0. `  K ) ) )
2015, 19sylib 199 . 2  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  -.  ( ( S  .\/  T )  e.  A  \/  ( S  .\/  T )  =  ( 0. `  K ) ) )
21 simp3r2 1114 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  S  .<_  ( T  .\/  V ) )
22 simp3l 1033 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  V  e.  A )
23 cdleme22.l . . . . . . . . 9  |-  .<_  =  ( le `  K )
2423, 5, 6hlatlej1 32859 . . . . . . . 8  |-  ( ( K  e.  HL  /\  T  e.  A  /\  V  e.  A )  ->  T  .<_  ( T  .\/  V ) )
251, 3, 22, 24syl3anc 1264 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  T  .<_  ( T  .\/  V ) )
26 hllat 32848 . . . . . . . . 9  |-  ( K  e.  HL  ->  K  e.  Lat )
271, 26syl 17 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  K  e.  Lat )
28 eqid 2422 . . . . . . . . . 10  |-  ( Base `  K )  =  (
Base `  K )
2928, 6atbase 32774 . . . . . . . . 9  |-  ( S  e.  A  ->  S  e.  ( Base `  K
) )
302, 29syl 17 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  S  e.  ( Base `  K ) )
3128, 6atbase 32774 . . . . . . . . 9  |-  ( T  e.  A  ->  T  e.  ( Base `  K
) )
323, 31syl 17 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  T  e.  ( Base `  K ) )
3328, 5, 6hlatjcl 32851 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  T  e.  A  /\  V  e.  A )  ->  ( T  .\/  V
)  e.  ( Base `  K ) )
341, 3, 22, 33syl3anc 1264 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( T  .\/  V
)  e.  ( Base `  K ) )
3528, 23, 5latjle12 16296 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( S  e.  ( Base `  K )  /\  T  e.  ( Base `  K )  /\  ( T  .\/  V )  e.  ( Base `  K
) ) )  -> 
( ( S  .<_  ( T  .\/  V )  /\  T  .<_  ( T 
.\/  V ) )  <-> 
( S  .\/  T
)  .<_  ( T  .\/  V ) ) )
3627, 30, 32, 34, 35syl13anc 1266 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( ( S  .<_  ( T  .\/  V )  /\  T  .<_  ( T 
.\/  V ) )  <-> 
( S  .\/  T
)  .<_  ( T  .\/  V ) ) )
3721, 25, 36mpbi2and 929 . . . . . 6  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( S  .\/  T
)  .<_  ( T  .\/  V ) )
3837adantr 466 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  T  .<_  ( P  .\/  Q ) )  ->  ( S  .\/  T )  .<_  ( T  .\/  V ) )
39 simp3r3 1115 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  S  .<_  ( P  .\/  Q ) )
4039adantr 466 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  T  .<_  ( P  .\/  Q ) )  ->  S  .<_  ( P  .\/  Q
) )
41 simpr 462 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  T  .<_  ( P  .\/  Q ) )  ->  T  .<_  ( P  .\/  Q
) )
42 simp21 1038 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  P  e.  A )
43 simp22 1039 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  Q  e.  A )
4428, 5, 6hlatjcl 32851 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  P  e.  A  /\  Q  e.  A )  ->  ( P  .\/  Q
)  e.  ( Base `  K ) )
451, 42, 43, 44syl3anc 1264 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( P  .\/  Q
)  e.  ( Base `  K ) )
4628, 23, 5latjle12 16296 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( S  e.  ( Base `  K )  /\  T  e.  ( Base `  K )  /\  ( P  .\/  Q )  e.  ( Base `  K
) ) )  -> 
( ( S  .<_  ( P  .\/  Q )  /\  T  .<_  ( P 
.\/  Q ) )  <-> 
( S  .\/  T
)  .<_  ( P  .\/  Q ) ) )
4727, 30, 32, 45, 46syl13anc 1266 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( ( S  .<_  ( P  .\/  Q )  /\  T  .<_  ( P 
.\/  Q ) )  <-> 
( S  .\/  T
)  .<_  ( P  .\/  Q ) ) )
4847adantr 466 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  T  .<_  ( P  .\/  Q ) )  ->  (
( S  .<_  ( P 
.\/  Q )  /\  T  .<_  ( P  .\/  Q ) )  <->  ( S  .\/  T )  .<_  ( P 
.\/  Q ) ) )
4940, 41, 48mpbi2and 929 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  T  .<_  ( P  .\/  Q ) )  ->  ( S  .\/  T )  .<_  ( P  .\/  Q ) )
5028, 5, 6hlatjcl 32851 . . . . . . . 8  |-  ( ( K  e.  HL  /\  S  e.  A  /\  T  e.  A )  ->  ( S  .\/  T
)  e.  ( Base `  K ) )
511, 2, 3, 50syl3anc 1264 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( S  .\/  T
)  e.  ( Base `  K ) )
52 cdleme22.m . . . . . . . 8  |-  ./\  =  ( meet `  K )
5328, 23, 52latlem12 16312 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( ( S  .\/  T )  e.  ( Base `  K )  /\  ( T  .\/  V )  e.  ( Base `  K
)  /\  ( P  .\/  Q )  e.  (
Base `  K )
) )  ->  (
( ( S  .\/  T )  .<_  ( T  .\/  V )  /\  ( S  .\/  T )  .<_  ( P  .\/  Q ) )  <->  ( S  .\/  T )  .<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) ) )
5427, 51, 34, 45, 53syl13anc 1266 . . . . . 6  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( ( ( S 
.\/  T )  .<_  ( T  .\/  V )  /\  ( S  .\/  T )  .<_  ( P  .\/  Q ) )  <->  ( S  .\/  T )  .<_  ( ( T  .\/  V ) 
./\  ( P  .\/  Q ) ) ) )
5554adantr 466 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  T  .<_  ( P  .\/  Q ) )  ->  (
( ( S  .\/  T )  .<_  ( T  .\/  V )  /\  ( S  .\/  T )  .<_  ( P  .\/  Q ) )  <->  ( S  .\/  T )  .<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) ) )
5638, 49, 55mpbi2and 929 . . . 4  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  T  .<_  ( P  .\/  Q ) )  ->  ( S  .\/  T )  .<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) )
5756ex 435 . . 3  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( T  .<_  ( P 
.\/  Q )  -> 
( S  .\/  T
)  .<_  ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) ) ) )
58 hlop 32847 . . . . . . . 8  |-  ( K  e.  HL  ->  K  e.  OP )
591, 58syl 17 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  K  e.  OP )
6059adantr 466 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  ( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  e.  A  /\  ( S  .\/  T ) 
.<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) ) )  ->  K  e.  OP )
6151adantr 466 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  ( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  e.  A  /\  ( S  .\/  T ) 
.<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) ) )  ->  ( S  .\/  T )  e.  (
Base `  K )
)
62 simprl 762 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  ( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  e.  A  /\  ( S  .\/  T ) 
.<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) ) )  ->  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) )  e.  A )
63 simprr 764 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  ( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  e.  A  /\  ( S  .\/  T ) 
.<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) ) )  ->  ( S  .\/  T )  .<_  ( ( T  .\/  V ) 
./\  ( P  .\/  Q ) ) )
6428, 23, 12, 6leat3 32780 . . . . . 6  |-  ( ( ( K  e.  OP  /\  ( S  .\/  T
)  e.  ( Base `  K )  /\  (
( T  .\/  V
)  ./\  ( P  .\/  Q ) )  e.  A )  /\  ( S  .\/  T )  .<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) )  ->  ( ( S 
.\/  T )  e.  A  \/  ( S 
.\/  T )  =  ( 0. `  K
) ) )
6560, 61, 62, 63, 64syl31anc 1267 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  ( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  e.  A  /\  ( S  .\/  T ) 
.<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) ) )  ->  ( ( S  .\/  T )  e.  A  \/  ( S 
.\/  T )  =  ( 0. `  K
) ) )
6665exp32 608 . . . 4  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  e.  A  -> 
( ( S  .\/  T )  .<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) )  ->  ( ( S  .\/  T )  e.  A  \/  ( S 
.\/  T )  =  ( 0. `  K
) ) ) ) )
67 breq2 4424 . . . . . . . . 9  |-  ( ( ( T  .\/  V
)  ./\  ( P  .\/  Q ) )  =  ( 0. `  K
)  ->  ( ( S  .\/  T )  .<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) )  <->  ( S  .\/  T )  .<_  ( 0.
`  K ) ) )
6867biimpa 486 . . . . . . . 8  |-  ( ( ( ( T  .\/  V )  ./\  ( P  .\/  Q ) )  =  ( 0. `  K
)  /\  ( S  .\/  T )  .<_  ( ( T  .\/  V ) 
./\  ( P  .\/  Q ) ) )  -> 
( S  .\/  T
)  .<_  ( 0. `  K ) )
6928, 23, 12ople0 32672 . . . . . . . . 9  |-  ( ( K  e.  OP  /\  ( S  .\/  T )  e.  ( Base `  K
) )  ->  (
( S  .\/  T
)  .<_  ( 0. `  K )  <->  ( S  .\/  T )  =  ( 0. `  K ) ) )
7059, 51, 69syl2anc 665 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( ( S  .\/  T )  .<_  ( 0. `  K )  <->  ( S  .\/  T )  =  ( 0. `  K ) ) )
7168, 70syl5ib 222 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( ( ( ( T  .\/  V ) 
./\  ( P  .\/  Q ) )  =  ( 0. `  K )  /\  ( S  .\/  T )  .<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) )  ->  ( S  .\/  T )  =  ( 0. `  K
) ) )
7271imp 430 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  ( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  =  ( 0.
`  K )  /\  ( S  .\/  T ) 
.<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) ) )  ->  ( S  .\/  T )  =  ( 0. `  K ) )
7372olcd 394 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/= 
T ) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q
)  /\  ( V  e.  A  /\  (
( T  .\/  V
)  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  /\  ( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  =  ( 0.
`  K )  /\  ( S  .\/  T ) 
.<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) ) ) )  ->  ( ( S  .\/  T )  e.  A  \/  ( S 
.\/  T )  =  ( 0. `  K
) ) )
7473exp32 608 . . . 4  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  =  ( 0.
`  K )  -> 
( ( S  .\/  T )  .<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) )  ->  ( ( S  .\/  T )  e.  A  \/  ( S 
.\/  T )  =  ( 0. `  K
) ) ) ) )
75 simp3r1 1113 . . . . 5  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( T  .\/  V
)  =/=  ( P 
.\/  Q ) )
765, 52, 12, 62atmat0 33010 . . . . 5  |-  ( ( ( K  e.  HL  /\  T  e.  A  /\  V  e.  A )  /\  ( P  e.  A  /\  Q  e.  A  /\  ( T  .\/  V
)  =/=  ( P 
.\/  Q ) ) )  ->  ( (
( T  .\/  V
)  ./\  ( P  .\/  Q ) )  e.  A  \/  ( ( T  .\/  V ) 
./\  ( P  .\/  Q ) )  =  ( 0. `  K ) ) )
771, 3, 22, 42, 43, 75, 76syl33anc 1279 . . . 4  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( ( ( T 
.\/  V )  ./\  ( P  .\/  Q ) )  e.  A  \/  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) )  =  ( 0. `  K
) ) )
7866, 74, 77mpjaod 382 . . 3  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( ( S  .\/  T )  .<_  ( ( T  .\/  V )  ./\  ( P  .\/  Q ) )  ->  ( ( S  .\/  T )  e.  A  \/  ( S 
.\/  T )  =  ( 0. `  K
) ) ) )
7957, 78syld 45 . 2  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  -> 
( T  .<_  ( P 
.\/  Q )  -> 
( ( S  .\/  T )  e.  A  \/  ( S  .\/  T )  =  ( 0. `  K ) ) ) )
8020, 79mtod 180 1  |-  ( ( ( K  e.  HL  /\  ( S  e.  A  /\  T  e.  A  /\  S  =/=  T
) )  /\  ( P  e.  A  /\  Q  e.  A  /\  P  =/=  Q )  /\  ( V  e.  A  /\  ( ( T  .\/  V )  =/=  ( P 
.\/  Q )  /\  S  .<_  ( T  .\/  V )  /\  S  .<_  ( P  .\/  Q ) ) ) )  ->  -.  T  .<_  ( P 
.\/  Q ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1868    =/= wne 2618   class class class wbr 4420   ` cfv 5598  (class class class)co 6302   Basecbs 15109   lecple 15185   joincjn 16177   meetcmee 16178   0.cp0 16271   Latclat 16279   OPcops 32657   Atomscatm 32748   HLchlt 32835   LLinesclln 32975   LHypclh 33468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-preset 16161  df-poset 16179  df-plt 16192  df-lub 16208  df-glb 16209  df-join 16210  df-meet 16211  df-p0 16273  df-p1 16274  df-lat 16280  df-clat 16342  df-oposet 32661  df-ol 32663  df-oml 32664  df-covers 32751  df-ats 32752  df-atl 32783  df-cvlat 32807  df-hlat 32836  df-llines 32982
This theorem is referenced by:  cdleme22cN  33828  cdleme27a  33853
  Copyright terms: Public domain W3C validator