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

Theorem dia2dimlem1 36934
Description: Lemma for dia2dim 36947. Show properties of the auxiliary atom  Q. Part of proof of Lemma M in [Crawley] p. 121 line 3. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
dia2dimlem1.l  |-  .<_  =  ( le `  K )
dia2dimlem1.j  |-  .\/  =  ( join `  K )
dia2dimlem1.m  |-  ./\  =  ( meet `  K )
dia2dimlem1.a  |-  A  =  ( Atoms `  K )
dia2dimlem1.h  |-  H  =  ( LHyp `  K
)
dia2dimlem1.t  |-  T  =  ( ( LTrn `  K
) `  W )
dia2dimlem1.r  |-  R  =  ( ( trL `  K
) `  W )
dia2dimlem1.q  |-  Q  =  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )
dia2dimlem1.k  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
dia2dimlem1.u  |-  ( ph  ->  ( U  e.  A  /\  U  .<_  W ) )
dia2dimlem1.v  |-  ( ph  ->  ( V  e.  A  /\  V  .<_  W ) )
dia2dimlem1.p  |-  ( ph  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
dia2dimlem1.f  |-  ( ph  ->  ( F  e.  T  /\  ( F `  P
)  =/=  P ) )
dia2dimlem1.rf  |-  ( ph  ->  ( R `  F
)  .<_  ( U  .\/  V ) )
dia2dimlem1.uv  |-  ( ph  ->  U  =/=  V )
dia2dimlem1.ru  |-  ( ph  ->  ( R `  F
)  =/=  U )
Assertion
Ref Expression
dia2dimlem1  |-  ( ph  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )

Proof of Theorem dia2dimlem1
StepHypRef Expression
1 dia2dimlem1.q . . 3  |-  Q  =  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )
2 dia2dimlem1.k . . . . 5  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
32simpld 459 . . . 4  |-  ( ph  ->  K  e.  HL )
4 dia2dimlem1.p . . . . 5  |-  ( ph  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
54simpld 459 . . . 4  |-  ( ph  ->  P  e.  A )
6 dia2dimlem1.f . . . . 5  |-  ( ph  ->  ( F  e.  T  /\  ( F `  P
)  =/=  P ) )
7 dia2dimlem1.l . . . . . 6  |-  .<_  =  ( le `  K )
8 dia2dimlem1.a . . . . . 6  |-  A  =  ( Atoms `  K )
9 dia2dimlem1.h . . . . . 6  |-  H  =  ( LHyp `  K
)
10 dia2dimlem1.t . . . . . 6  |-  T  =  ( ( LTrn `  K
) `  W )
11 dia2dimlem1.r . . . . . 6  |-  R  =  ( ( trL `  K
) `  W )
127, 8, 9, 10, 11trlat 36037 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( F  e.  T  /\  ( F `  P )  =/=  P ) )  ->  ( R `  F )  e.  A
)
132, 4, 6, 12syl3anc 1228 . . . 4  |-  ( ph  ->  ( R `  F
)  e.  A )
14 dia2dimlem1.u . . . . 5  |-  ( ph  ->  ( U  e.  A  /\  U  .<_  W ) )
1514simpld 459 . . . 4  |-  ( ph  ->  U  e.  A )
166simpld 459 . . . . . 6  |-  ( ph  ->  F  e.  T )
177, 8, 9, 10ltrnel 36006 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( F `  P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )
182, 16, 4, 17syl3anc 1228 . . . . 5  |-  ( ph  ->  ( ( F `  P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )
1918simpld 459 . . . 4  |-  ( ph  ->  ( F `  P
)  e.  A )
20 dia2dimlem1.v . . . . 5  |-  ( ph  ->  ( V  e.  A  /\  V  .<_  W ) )
2120simpld 459 . . . 4  |-  ( ph  ->  V  e.  A )
224simprd 463 . . . . . 6  |-  ( ph  ->  -.  P  .<_  W )
237, 9, 10, 11trlle 36052 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  .<_  W )
242, 16, 23syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( R `  F
)  .<_  W )
2514simprd 463 . . . . . . . 8  |-  ( ph  ->  U  .<_  W )
26 hllat 35231 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  Lat )
273, 26syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  Lat )
28 eqid 2457 . . . . . . . . . . 11  |-  ( Base `  K )  =  (
Base `  K )
2928, 8atbase 35157 . . . . . . . . . 10  |-  ( ( R `  F )  e.  A  ->  ( R `  F )  e.  ( Base `  K
) )
3013, 29syl 16 . . . . . . . . 9  |-  ( ph  ->  ( R `  F
)  e.  ( Base `  K ) )
3128, 8atbase 35157 . . . . . . . . . 10  |-  ( U  e.  A  ->  U  e.  ( Base `  K
) )
3215, 31syl 16 . . . . . . . . 9  |-  ( ph  ->  U  e.  ( Base `  K ) )
332simprd 463 . . . . . . . . . 10  |-  ( ph  ->  W  e.  H )
3428, 9lhpbase 35865 . . . . . . . . . 10  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
3533, 34syl 16 . . . . . . . . 9  |-  ( ph  ->  W  e.  ( Base `  K ) )
36 dia2dimlem1.j . . . . . . . . . 10  |-  .\/  =  ( join `  K )
3728, 7, 36latjle12 15819 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  ( ( R `  F )  e.  (
Base `  K )  /\  U  e.  ( Base `  K )  /\  W  e.  ( Base `  K ) ) )  ->  ( ( ( R `  F ) 
.<_  W  /\  U  .<_  W )  <->  ( ( R `
 F )  .\/  U )  .<_  W )
)
3827, 30, 32, 35, 37syl13anc 1230 . . . . . . . 8  |-  ( ph  ->  ( ( ( R `
 F )  .<_  W  /\  U  .<_  W )  <-> 
( ( R `  F )  .\/  U
)  .<_  W ) )
3924, 25, 38mpbi2and 921 . . . . . . 7  |-  ( ph  ->  ( ( R `  F )  .\/  U
)  .<_  W )
4028, 8atbase 35157 . . . . . . . . 9  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
415, 40syl 16 . . . . . . . 8  |-  ( ph  ->  P  e.  ( Base `  K ) )
4228, 36, 8hlatjcl 35234 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( R `  F )  e.  A  /\  U  e.  A )  ->  (
( R `  F
)  .\/  U )  e.  ( Base `  K
) )
433, 13, 15, 42syl3anc 1228 . . . . . . . 8  |-  ( ph  ->  ( ( R `  F )  .\/  U
)  e.  ( Base `  K ) )
4428, 7lattr 15813 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( P  e.  ( Base `  K )  /\  ( ( R `  F )  .\/  U
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) ) )  -> 
( ( P  .<_  ( ( R `  F
)  .\/  U )  /\  ( ( R `  F )  .\/  U
)  .<_  W )  ->  P  .<_  W ) )
4527, 41, 43, 35, 44syl13anc 1230 . . . . . . 7  |-  ( ph  ->  ( ( P  .<_  ( ( R `  F
)  .\/  U )  /\  ( ( R `  F )  .\/  U
)  .<_  W )  ->  P  .<_  W ) )
4639, 45mpan2d 674 . . . . . 6  |-  ( ph  ->  ( P  .<_  ( ( R `  F ) 
.\/  U )  ->  P  .<_  W ) )
4722, 46mtod 177 . . . . 5  |-  ( ph  ->  -.  P  .<_  ( ( R `  F ) 
.\/  U ) )
4820simprd 463 . . . . . . 7  |-  ( ph  ->  V  .<_  W )
4918simprd 463 . . . . . . 7  |-  ( ph  ->  -.  ( F `  P )  .<_  W )
50 nbrne2 4474 . . . . . . 7  |-  ( ( V  .<_  W  /\  -.  ( F `  P
)  .<_  W )  ->  V  =/=  ( F `  P ) )
5148, 49, 50syl2anc 661 . . . . . 6  |-  ( ph  ->  V  =/=  ( F `
 P ) )
5251necomd 2728 . . . . 5  |-  ( ph  ->  ( F `  P
)  =/=  V )
5347, 52jca 532 . . . 4  |-  ( ph  ->  ( -.  P  .<_  ( ( R `  F
)  .\/  U )  /\  ( F `  P
)  =/=  V ) )
5427adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  K  e.  Lat )
5541adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  P  e.  ( Base `  K )
)
5628, 36, 8hlatjcl 35234 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  V  e.  A  /\  U  e.  A )  ->  ( V  .\/  U
)  e.  ( Base `  K ) )
573, 21, 15, 56syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  ( V  .\/  U
)  e.  ( Base `  K ) )
5857adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( V  .\/  U )  e.  (
Base `  K )
)
5935adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  W  e.  ( Base `  K )
)
607, 36, 8hlatlej2 35243 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( F `  P )  e.  A  /\  V  e.  A )  ->  V  .<_  ( ( F `  P )  .\/  V
) )
613, 19, 21, 60syl3anc 1228 . . . . . . . . . . 11  |-  ( ph  ->  V  .<_  ( ( F `  P )  .\/  V ) )
6261adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  V  .<_  ( ( F `  P
)  .\/  V )
)
63 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)
6462, 63breqtrrd 4482 . . . . . . . . 9  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  V  .<_  ( P  .\/  U ) )
65 dia2dimlem1.uv . . . . . . . . . . . 12  |-  ( ph  ->  U  =/=  V )
6665necomd 2728 . . . . . . . . . . 11  |-  ( ph  ->  V  =/=  U )
677, 36, 8hlatexch2 35263 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( V  e.  A  /\  P  e.  A  /\  U  e.  A
)  /\  V  =/=  U )  ->  ( V  .<_  ( P  .\/  U
)  ->  P  .<_  ( V  .\/  U ) ) )
683, 21, 5, 15, 66, 67syl131anc 1241 . . . . . . . . . 10  |-  ( ph  ->  ( V  .<_  ( P 
.\/  U )  ->  P  .<_  ( V  .\/  U ) ) )
6968adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( V  .<_  ( P  .\/  U
)  ->  P  .<_  ( V  .\/  U ) ) )
7064, 69mpd 15 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  P  .<_  ( V  .\/  U ) )
7128, 8atbase 35157 . . . . . . . . . . . 12  |-  ( V  e.  A  ->  V  e.  ( Base `  K
) )
7221, 71syl 16 . . . . . . . . . . 11  |-  ( ph  ->  V  e.  ( Base `  K ) )
7328, 7, 36latjle12 15819 . . . . . . . . . . 11  |-  ( ( K  e.  Lat  /\  ( V  e.  ( Base `  K )  /\  U  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) ) )  -> 
( ( V  .<_  W  /\  U  .<_  W )  <-> 
( V  .\/  U
)  .<_  W ) )
7427, 72, 32, 35, 73syl13anc 1230 . . . . . . . . . 10  |-  ( ph  ->  ( ( V  .<_  W  /\  U  .<_  W )  <-> 
( V  .\/  U
)  .<_  W ) )
7548, 25, 74mpbi2and 921 . . . . . . . . 9  |-  ( ph  ->  ( V  .\/  U
)  .<_  W )
7675adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( V  .\/  U )  .<_  W )
7728, 7, 54, 55, 58, 59, 70, 76lattrd 15815 . . . . . . 7  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  P  .<_  W )
7877ex 434 . . . . . 6  |-  ( ph  ->  ( ( P  .\/  U )  =  ( ( F `  P ) 
.\/  V )  ->  P  .<_  W ) )
7978necon3bd 2669 . . . . 5  |-  ( ph  ->  ( -.  P  .<_  W  ->  ( P  .\/  U )  =/=  ( ( F `  P ) 
.\/  V ) ) )
8022, 79mpd 15 . . . 4  |-  ( ph  ->  ( P  .\/  U
)  =/=  ( ( F `  P ) 
.\/  V ) )
817, 36, 8hlatlej2 35243 . . . . . . 7  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  -> 
( F `  P
)  .<_  ( P  .\/  ( F `  P ) ) )
823, 5, 19, 81syl3anc 1228 . . . . . 6  |-  ( ph  ->  ( F `  P
)  .<_  ( P  .\/  ( F `  P ) ) )
83 dia2dimlem1.m . . . . . . . . . 10  |-  ./\  =  ( meet `  K )
847, 36, 83, 8, 9, 10, 11trlval2 36031 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  W )
)
852, 16, 4, 84syl3anc 1228 . . . . . . . 8  |-  ( ph  ->  ( R `  F
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  W ) )
8685oveq2d 6312 . . . . . . 7  |-  ( ph  ->  ( P  .\/  ( R `  F )
)  =  ( P 
.\/  ( ( P 
.\/  ( F `  P ) )  ./\  W ) ) )
8728, 36, 8hlatjcl 35234 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  -> 
( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
883, 5, 19, 87syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  ( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
897, 36, 8hlatlej1 35242 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  ->  P  .<_  ( P  .\/  ( F `  P ) ) )
903, 5, 19, 89syl3anc 1228 . . . . . . . . 9  |-  ( ph  ->  P  .<_  ( P  .\/  ( F `  P
) ) )
9128, 7, 36, 83, 8atmod3i1 35731 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  ( P  .\/  ( F `  P )
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  /\  P  .<_  ( P  .\/  ( F `  P )
) )  ->  ( P  .\/  ( ( P 
.\/  ( F `  P ) )  ./\  W ) )  =  ( ( P  .\/  ( F `  P )
)  ./\  ( P  .\/  W ) ) )
923, 5, 88, 35, 90, 91syl131anc 1241 . . . . . . . 8  |-  ( ph  ->  ( P  .\/  (
( P  .\/  ( F `  P )
)  ./\  W )
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  ( P  .\/  W ) ) )
93 eqid 2457 . . . . . . . . . . . 12  |-  ( 1.
`  K )  =  ( 1. `  K
)
947, 36, 93, 8, 9lhpjat2 35888 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  -> 
( P  .\/  W
)  =  ( 1.
`  K ) )
952, 4, 94syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( P  .\/  W
)  =  ( 1.
`  K ) )
9695oveq2d 6312 . . . . . . . . 9  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( P  .\/  W ) )  =  ( ( P  .\/  ( F `  P ) )  ./\  ( 1. `  K ) ) )
97 hlol 35229 . . . . . . . . . . 11  |-  ( K  e.  HL  ->  K  e.  OL )
983, 97syl 16 . . . . . . . . . 10  |-  ( ph  ->  K  e.  OL )
9928, 83, 93olm11 35095 . . . . . . . . . 10  |-  ( ( K  e.  OL  /\  ( P  .\/  ( F `
 P ) )  e.  ( Base `  K
) )  ->  (
( P  .\/  ( F `  P )
)  ./\  ( 1. `  K ) )  =  ( P  .\/  ( F `  P )
) )
10098, 88, 99syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( 1. `  K ) )  =  ( P  .\/  ( F `  P )
) )
10196, 100eqtrd 2498 . . . . . . . 8  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( P  .\/  W ) )  =  ( P  .\/  ( F `  P )
) )
10292, 101eqtrd 2498 . . . . . . 7  |-  ( ph  ->  ( P  .\/  (
( P  .\/  ( F `  P )
)  ./\  W )
)  =  ( P 
.\/  ( F `  P ) ) )
10386, 102eqtrd 2498 . . . . . 6  |-  ( ph  ->  ( P  .\/  ( R `  F )
)  =  ( P 
.\/  ( F `  P ) ) )
10482, 103breqtrrd 4482 . . . . 5  |-  ( ph  ->  ( F `  P
)  .<_  ( P  .\/  ( R `  F ) ) )
105 dia2dimlem1.rf . . . . . . 7  |-  ( ph  ->  ( R `  F
)  .<_  ( U  .\/  V ) )
10636, 8hlatjcom 35235 . . . . . . . 8  |-  ( ( K  e.  HL  /\  U  e.  A  /\  V  e.  A )  ->  ( U  .\/  V
)  =  ( V 
.\/  U ) )
1073, 15, 21, 106syl3anc 1228 . . . . . . 7  |-  ( ph  ->  ( U  .\/  V
)  =  ( V 
.\/  U ) )
108105, 107breqtrd 4480 . . . . . 6  |-  ( ph  ->  ( R `  F
)  .<_  ( V  .\/  U ) )
109 dia2dimlem1.ru . . . . . . 7  |-  ( ph  ->  ( R `  F
)  =/=  U )
1107, 36, 8hlatexch2 35263 . . . . . . 7  |-  ( ( K  e.  HL  /\  ( ( R `  F )  e.  A  /\  V  e.  A  /\  U  e.  A
)  /\  ( R `  F )  =/=  U
)  ->  ( ( R `  F )  .<_  ( V  .\/  U
)  ->  V  .<_  ( ( R `  F
)  .\/  U )
) )
1113, 13, 21, 15, 109, 110syl131anc 1241 . . . . . 6  |-  ( ph  ->  ( ( R `  F )  .<_  ( V 
.\/  U )  ->  V  .<_  ( ( R `
 F )  .\/  U ) ) )
112108, 111mpd 15 . . . . 5  |-  ( ph  ->  V  .<_  ( ( R `  F )  .\/  U ) )
113104, 112jca 532 . . . 4  |-  ( ph  ->  ( ( F `  P )  .<_  ( P 
.\/  ( R `  F ) )  /\  V  .<_  ( ( R `
 F )  .\/  U ) ) )
1147, 36, 83, 8ps-2c 35395 . . . 4  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  ( R `  F )  e.  A )  /\  ( U  e.  A  /\  ( F `  P
)  e.  A  /\  V  e.  A )  /\  ( ( -.  P  .<_  ( ( R `  F )  .\/  U
)  /\  ( F `  P )  =/=  V
)  /\  ( P  .\/  U )  =/=  (
( F `  P
)  .\/  V )  /\  ( ( F `  P )  .<_  ( P 
.\/  ( R `  F ) )  /\  V  .<_  ( ( R `
 F )  .\/  U ) ) ) )  ->  ( ( P 
.\/  U )  ./\  ( ( F `  P )  .\/  V
) )  e.  A
)
1153, 5, 13, 15, 19, 21, 53, 80, 113, 114syl333anc 1260 . . 3  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )  e.  A )
1161, 115syl5eqel 2549 . 2  |-  ( ph  ->  Q  e.  A )
11728, 36, 8hlatjcl 35234 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  P  e.  A  /\  U  e.  A )  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
1183, 5, 15, 117syl3anc 1228 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
11928, 36, 8hlatjcl 35234 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( F `  P )  e.  A  /\  V  e.  A )  ->  (
( F `  P
)  .\/  V )  e.  ( Base `  K
) )
1203, 19, 21, 119syl3anc 1228 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F `  P )  .\/  V
)  e.  ( Base `  K ) )
12128, 7, 83latmle1 15833 . . . . . . . . . . . 12  |-  ( ( K  e.  Lat  /\  ( P  .\/  U )  e.  ( Base `  K
)  /\  ( ( F `  P )  .\/  V )  e.  (
Base `  K )
)  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V
) )  .<_  ( P 
.\/  U ) )
12227, 118, 120, 121syl3anc 1228 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )  .<_  ( P  .\/  U ) )
1231, 122syl5eqbr 4489 . . . . . . . . . 10  |-  ( ph  ->  Q  .<_  ( P  .\/  U ) )
12428, 8atbase 35157 . . . . . . . . . . . . 13  |-  ( Q  e.  A  ->  Q  e.  ( Base `  K
) )
125116, 124syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( Base `  K ) )
12628, 7, 83latlem12 15835 . . . . . . . . . . . 12  |-  ( ( K  e.  Lat  /\  ( Q  e.  ( Base `  K )  /\  ( P  .\/  U )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
) )  ->  (
( Q  .<_  ( P 
.\/  U )  /\  Q  .<_  W )  <->  Q  .<_  ( ( P  .\/  U
)  ./\  W )
) )
12727, 125, 118, 35, 126syl13anc 1230 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  .<_  ( P  .\/  U )  /\  Q  .<_  W )  <-> 
Q  .<_  ( ( P 
.\/  U )  ./\  W ) ) )
128127biimpd 207 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  .<_  ( P  .\/  U )  /\  Q  .<_  W )  ->  Q  .<_  ( ( P  .\/  U ) 
./\  W ) ) )
129123, 128mpand 675 . . . . . . . . 9  |-  ( ph  ->  ( Q  .<_  W  ->  Q  .<_  ( ( P 
.\/  U )  ./\  W ) ) )
130129imp 429 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  ( ( P  .\/  U
)  ./\  W )
)
131 eqid 2457 . . . . . . . . . . . . 13  |-  ( 0.
`  K )  =  ( 0. `  K
)
1327, 83, 131, 8, 9lhpmat 35897 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  -> 
( P  ./\  W
)  =  ( 0.
`  K ) )
1332, 4, 132syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( P  ./\  W
)  =  ( 0.
`  K ) )
134133oveq1d 6311 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  ./\  W )  .\/  U )  =  ( ( 0.
`  K )  .\/  U ) )
13528, 7, 36, 83, 8atmod4i1 35733 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( U  e.  A  /\  P  e.  ( Base `  K )  /\  W  e.  ( Base `  K ) )  /\  U  .<_  W )  -> 
( ( P  ./\  W )  .\/  U )  =  ( ( P 
.\/  U )  ./\  W ) )
1363, 15, 41, 35, 25, 135syl131anc 1241 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  ./\  W )  .\/  U )  =  ( ( P 
.\/  U )  ./\  W ) )
13728, 36, 131olj02 35094 . . . . . . . . . . 11  |-  ( ( K  e.  OL  /\  U  e.  ( Base `  K ) )  -> 
( ( 0. `  K )  .\/  U
)  =  U )
13898, 32, 137syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( 0. `  K )  .\/  U
)  =  U )
139134, 136, 1383eqtr3d 2506 . . . . . . . . 9  |-  ( ph  ->  ( ( P  .\/  U )  ./\  W )  =  U )
140139adantr 465 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  ( ( P  .\/  U )  ./\  W )  =  U )
141130, 140breqtrd 4480 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  U )
142 hlatl 35228 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  AtLat )
1433, 142syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  AtLat )
144143adantr 465 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  K  e.  AtLat
)
145116adantr 465 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  e.  A )
14615adantr 465 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  U  e.  A )
1477, 8atcmp 35179 . . . . . . . 8  |-  ( ( K  e.  AtLat  /\  Q  e.  A  /\  U  e.  A )  ->  ( Q  .<_  U  <->  Q  =  U ) )
148144, 145, 146, 147syl3anc 1228 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  ( Q  .<_  U  <->  Q  =  U
) )
149141, 148mpbid 210 . . . . . 6  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  =  U )
15028, 7, 83latmle2 15834 . . . . . . . . . . . 12  |-  ( ( K  e.  Lat  /\  ( P  .\/  U )  e.  ( Base `  K
)  /\  ( ( F `  P )  .\/  V )  e.  (
Base `  K )
)  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V
) )  .<_  ( ( F `  P ) 
.\/  V ) )
15127, 118, 120, 150syl3anc 1228 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )  .<_  ( ( F `  P )  .\/  V
) )
1521, 151syl5eqbr 4489 . . . . . . . . . 10  |-  ( ph  ->  Q  .<_  ( ( F `  P )  .\/  V ) )
15328, 7, 83latlem12 15835 . . . . . . . . . . . 12  |-  ( ( K  e.  Lat  /\  ( Q  e.  ( Base `  K )  /\  ( ( F `  P )  .\/  V
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) ) )  -> 
( ( Q  .<_  ( ( F `  P
)  .\/  V )  /\  Q  .<_  W )  <-> 
Q  .<_  ( ( ( F `  P ) 
.\/  V )  ./\  W ) ) )
15427, 125, 120, 35, 153syl13anc 1230 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  .<_  ( ( F `  P
)  .\/  V )  /\  Q  .<_  W )  <-> 
Q  .<_  ( ( ( F `  P ) 
.\/  V )  ./\  W ) ) )
155154biimpd 207 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  .<_  ( ( F `  P
)  .\/  V )  /\  Q  .<_  W )  ->  Q  .<_  ( ( ( F `  P
)  .\/  V )  ./\  W ) ) )
156152, 155mpand 675 . . . . . . . . 9  |-  ( ph  ->  ( Q  .<_  W  ->  Q  .<_  ( ( ( F `  P ) 
.\/  V )  ./\  W ) ) )
157156imp 429 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  ( ( ( F `  P )  .\/  V
)  ./\  W )
)
1587, 83, 131, 8, 9lhpmat 35897 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( F `
 P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )  -> 
( ( F `  P )  ./\  W
)  =  ( 0.
`  K ) )
1592, 18, 158syl2anc 661 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F `  P )  ./\  W
)  =  ( 0.
`  K ) )
160159oveq1d 6311 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 P )  ./\  W )  .\/  V )  =  ( ( 0.
`  K )  .\/  V ) )
16128, 8atbase 35157 . . . . . . . . . . . 12  |-  ( ( F `  P )  e.  A  ->  ( F `  P )  e.  ( Base `  K
) )
16219, 161syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  P
)  e.  ( Base `  K ) )
16328, 7, 36, 83, 8atmod4i1 35733 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( V  e.  A  /\  ( F `  P
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  /\  V  .<_  W )  ->  (
( ( F `  P )  ./\  W
)  .\/  V )  =  ( ( ( F `  P ) 
.\/  V )  ./\  W ) )
1643, 21, 162, 35, 48, 163syl131anc 1241 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 P )  ./\  W )  .\/  V )  =  ( ( ( F `  P ) 
.\/  V )  ./\  W ) )
16528, 36, 131olj02 35094 . . . . . . . . . . 11  |-  ( ( K  e.  OL  /\  V  e.  ( Base `  K ) )  -> 
( ( 0. `  K )  .\/  V
)  =  V )
16698, 72, 165syl2anc 661 . . . . . . . . . 10  |-  ( ph  ->  ( ( 0. `  K )  .\/  V
)  =  V )
167160, 164, 1663eqtr3d 2506 . . . . . . . . 9  |-  ( ph  ->  ( ( ( F `
 P )  .\/  V )  ./\  W )  =  V )
168167adantr 465 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  ( (
( F `  P
)  .\/  V )  ./\  W )  =  V )
169157, 168breqtrd 4480 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  V )
17021adantr 465 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  V  e.  A )
1717, 8atcmp 35179 . . . . . . . 8  |-  ( ( K  e.  AtLat  /\  Q  e.  A  /\  V  e.  A )  ->  ( Q  .<_  V  <->  Q  =  V ) )
172144, 145, 170, 171syl3anc 1228 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  ( Q  .<_  V  <->  Q  =  V
) )
173169, 172mpbid 210 . . . . . 6  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  =  V )
174149, 173eqtr3d 2500 . . . . 5  |-  ( (
ph  /\  Q  .<_  W )  ->  U  =  V )
175174ex 434 . . . 4  |-  ( ph  ->  ( Q  .<_  W  ->  U  =  V )
)
176175necon3ad 2667 . . 3  |-  ( ph  ->  ( U  =/=  V  ->  -.  Q  .<_  W ) )
17765, 176mpd 15 . 2  |-  ( ph  ->  -.  Q  .<_  W )
178116, 177jca 532 1  |-  ( ph  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1395    e. wcel 1819    =/= wne 2652   class class class wbr 4456   ` cfv 5594  (class class class)co 6296   Basecbs 14644   lecple 14719   joincjn 15700   meetcmee 15701   0.cp0 15794   1.cp1 15795   Latclat 15802   OLcol 35042   Atomscatm 35131   AtLatcal 35132   HLchlt 35218   LHypclh 35851   LTrncltrn 35968   trLctrl 36026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-iun 4334  df-iin 4335  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-1st 6799  df-2nd 6800  df-map 7440  df-preset 15684  df-poset 15702  df-plt 15715  df-lub 15731  df-glb 15732  df-join 15733  df-meet 15734  df-p0 15796  df-p1 15797  df-lat 15803  df-clat 15865  df-oposet 35044  df-ol 35046  df-oml 35047  df-covers 35134  df-ats 35135  df-atl 35166  df-cvlat 35190  df-hlat 35219  df-llines 35365  df-psubsp 35370  df-pmap 35371  df-padd 35663  df-lhyp 35855  df-laut 35856  df-ldil 35971  df-ltrn 35972  df-trl 36027
This theorem is referenced by:  dia2dimlem3  36936  dia2dimlem6  36939
  Copyright terms: Public domain W3C validator