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

Theorem dia2dimlem1 30533
Description: Lemma for dia2dim 30546. 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 445 . . . 4  |-  ( ph  ->  K  e.  HL )
4 dia2dimlem1.p . . . . 5  |-  ( ph  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
54simpld 445 . . . 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 29637 . . . . 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 1182 . . . 4  |-  ( ph  ->  ( R `  F
)  e.  A )
14 dia2dimlem1.u . . . . 5  |-  ( ph  ->  ( U  e.  A  /\  U  .<_  W ) )
1514simpld 445 . . . 4  |-  ( ph  ->  U  e.  A )
166simpld 445 . . . . . 6  |-  ( ph  ->  F  e.  T )
177, 8, 9, 10ltrnel 29607 . . . . . 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 1182 . . . . 5  |-  ( ph  ->  ( ( F `  P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )
1918simpld 445 . . . 4  |-  ( ph  ->  ( F `  P
)  e.  A )
20 dia2dimlem1.v . . . . 5  |-  ( ph  ->  ( V  e.  A  /\  V  .<_  W ) )
2120simpld 445 . . . 4  |-  ( ph  ->  V  e.  A )
224simprd 449 . . . . . 6  |-  ( ph  ->  -.  P  .<_  W )
237, 9, 10, 11trlle 29652 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  .<_  W )
242, 16, 23syl2anc 642 . . . . . . . 8  |-  ( ph  ->  ( R `  F
)  .<_  W )
2514simprd 449 . . . . . . . 8  |-  ( ph  ->  U  .<_  W )
26 hllat 28832 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  Lat )
273, 26syl 15 . . . . . . . . 9  |-  ( ph  ->  K  e.  Lat )
28 eqid 2284 . . . . . . . . . . 11  |-  ( Base `  K )  =  (
Base `  K )
2928, 8atbase 28758 . . . . . . . . . 10  |-  ( ( R `  F )  e.  A  ->  ( R `  F )  e.  ( Base `  K
) )
3013, 29syl 15 . . . . . . . . 9  |-  ( ph  ->  ( R `  F
)  e.  ( Base `  K ) )
3128, 8atbase 28758 . . . . . . . . . 10  |-  ( U  e.  A  ->  U  e.  ( Base `  K
) )
3215, 31syl 15 . . . . . . . . 9  |-  ( ph  ->  U  e.  ( Base `  K ) )
332simprd 449 . . . . . . . . . 10  |-  ( ph  ->  W  e.  H )
3428, 9lhpbase 29466 . . . . . . . . . 10  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
3533, 34syl 15 . . . . . . . . 9  |-  ( ph  ->  W  e.  ( Base `  K ) )
36 dia2dimlem1.j . . . . . . . . . 10  |-  .\/  =  ( join `  K )
3728, 7, 36latjle12 14164 . . . . . . . . 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 1184 . . . . . . . 8  |-  ( ph  ->  ( ( ( R `
 F )  .<_  W  /\  U  .<_  W )  <-> 
( ( R `  F )  .\/  U
)  .<_  W ) )
3924, 25, 38mpbi2and 887 . . . . . . 7  |-  ( ph  ->  ( ( R `  F )  .\/  U
)  .<_  W )
4028, 8atbase 28758 . . . . . . . . 9  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
415, 40syl 15 . . . . . . . 8  |-  ( ph  ->  P  e.  ( Base `  K ) )
4228, 36, 8hlatjcl 28835 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( R `  F )  e.  A  /\  U  e.  A )  ->  (
( R `  F
)  .\/  U )  e.  ( Base `  K
) )
433, 13, 15, 42syl3anc 1182 . . . . . . . 8  |-  ( ph  ->  ( ( R `  F )  .\/  U
)  e.  ( Base `  K ) )
4428, 7lattr 14158 . . . . . . . 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 1184 . . . . . . 7  |-  ( ph  ->  ( ( P  .<_  ( ( R `  F
)  .\/  U )  /\  ( ( R `  F )  .\/  U
)  .<_  W )  ->  P  .<_  W ) )
4639, 45mpan2d 655 . . . . . 6  |-  ( ph  ->  ( P  .<_  ( ( R `  F ) 
.\/  U )  ->  P  .<_  W ) )
4722, 46mtod 168 . . . . 5  |-  ( ph  ->  -.  P  .<_  ( ( R `  F ) 
.\/  U ) )
4820simprd 449 . . . . . . 7  |-  ( ph  ->  V  .<_  W )
4918simprd 449 . . . . . . 7  |-  ( ph  ->  -.  ( F `  P )  .<_  W )
50 nbrne2 4042 . . . . . . 7  |-  ( ( V  .<_  W  /\  -.  ( F `  P
)  .<_  W )  ->  V  =/=  ( F `  P ) )
5148, 49, 50syl2anc 642 . . . . . 6  |-  ( ph  ->  V  =/=  ( F `
 P ) )
5251necomd 2530 . . . . 5  |-  ( ph  ->  ( F `  P
)  =/=  V )
5347, 52jca 518 . . . 4  |-  ( ph  ->  ( -.  P  .<_  ( ( R `  F
)  .\/  U )  /\  ( F `  P
)  =/=  V ) )
5427adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  K  e.  Lat )
5541adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  P  e.  ( Base `  K )
)
5628, 36, 8hlatjcl 28835 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  V  e.  A  /\  U  e.  A )  ->  ( V  .\/  U
)  e.  ( Base `  K ) )
573, 21, 15, 56syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( V  .\/  U
)  e.  ( Base `  K ) )
5857adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( V  .\/  U )  e.  (
Base `  K )
)
5935adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  W  e.  ( Base `  K )
)
607, 36, 8hlatlej2 28844 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( F `  P )  e.  A  /\  V  e.  A )  ->  V  .<_  ( ( F `  P )  .\/  V
) )
613, 19, 21, 60syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  V  .<_  ( ( F `  P )  .\/  V ) )
6261adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  V  .<_  ( ( F `  P
)  .\/  V )
)
63 simpr 447 . . . . . . . . . 10  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)
6462, 63breqtrrd 4050 . . . . . . . . 9  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  V  .<_  ( P  .\/  U ) )
65 dia2dimlem1.uv . . . . . . . . . . . 12  |-  ( ph  ->  U  =/=  V )
6665necomd 2530 . . . . . . . . . . 11  |-  ( ph  ->  V  =/=  U )
677, 36, 8hlatexch2 28864 . . . . . . . . . . 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 1195 . . . . . . . . . 10  |-  ( ph  ->  ( V  .<_  ( P 
.\/  U )  ->  P  .<_  ( V  .\/  U ) ) )
6968adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( V  .<_  ( P  .\/  U
)  ->  P  .<_  ( V  .\/  U ) ) )
7064, 69mpd 14 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  P  .<_  ( V  .\/  U ) )
7128, 8atbase 28758 . . . . . . . . . . . 12  |-  ( V  e.  A  ->  V  e.  ( Base `  K
) )
7221, 71syl 15 . . . . . . . . . . 11  |-  ( ph  ->  V  e.  ( Base `  K ) )
7328, 7, 36latjle12 14164 . . . . . . . . . . 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 1184 . . . . . . . . . 10  |-  ( ph  ->  ( ( V  .<_  W  /\  U  .<_  W )  <-> 
( V  .\/  U
)  .<_  W ) )
7548, 25, 74mpbi2and 887 . . . . . . . . 9  |-  ( ph  ->  ( V  .\/  U
)  .<_  W )
7675adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( V  .\/  U )  .<_  W )
7728, 7, 54, 55, 58, 59, 70, 76lattrd 14160 . . . . . . 7  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  P  .<_  W )
7877ex 423 . . . . . 6  |-  ( ph  ->  ( ( P  .\/  U )  =  ( ( F `  P ) 
.\/  V )  ->  P  .<_  W ) )
7978necon3bd 2484 . . . . 5  |-  ( ph  ->  ( -.  P  .<_  W  ->  ( P  .\/  U )  =/=  ( ( F `  P ) 
.\/  V ) ) )
8022, 79mpd 14 . . . 4  |-  ( ph  ->  ( P  .\/  U
)  =/=  ( ( F `  P ) 
.\/  V ) )
817, 36, 8hlatlej2 28844 . . . . . . 7  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  -> 
( F `  P
)  .<_  ( P  .\/  ( F `  P ) ) )
823, 5, 19, 81syl3anc 1182 . . . . . 6  |-  ( ph  ->  ( F `  P
)  .<_  ( P  .\/  ( F `  P ) ) )
83 dia2dimlem1.m . . . . . . . . . 10  |-  ./\  =  ( meet `  K )
847, 36, 83, 8, 9, 10, 11trlval2 29631 . . . . . . . . 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 1182 . . . . . . . 8  |-  ( ph  ->  ( R `  F
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  W ) )
8685oveq2d 5836 . . . . . . 7  |-  ( ph  ->  ( P  .\/  ( R `  F )
)  =  ( P 
.\/  ( ( P 
.\/  ( F `  P ) )  ./\  W ) ) )
8728, 36, 8hlatjcl 28835 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  -> 
( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
883, 5, 19, 87syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
897, 36, 8hlatlej1 28843 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  ->  P  .<_  ( P  .\/  ( F `  P ) ) )
903, 5, 19, 89syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  P  .<_  ( P  .\/  ( F `  P
) ) )
9128, 7, 36, 83, 8atmod3i1 29332 . . . . . . . . 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 1195 . . . . . . . 8  |-  ( ph  ->  ( P  .\/  (
( P  .\/  ( F `  P )
)  ./\  W )
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  ( P  .\/  W ) ) )
93 eqid 2284 . . . . . . . . . . . 12  |-  ( 1.
`  K )  =  ( 1. `  K
)
947, 36, 93, 8, 9lhpjat2 29489 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  -> 
( P  .\/  W
)  =  ( 1.
`  K ) )
952, 4, 94syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( P  .\/  W
)  =  ( 1.
`  K ) )
9695oveq2d 5836 . . . . . . . . 9  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( P  .\/  W ) )  =  ( ( P  .\/  ( F `  P ) )  ./\  ( 1. `  K ) ) )
97 hlol 28830 . . . . . . . . . . 11  |-  ( K  e.  HL  ->  K  e.  OL )
983, 97syl 15 . . . . . . . . . 10  |-  ( ph  ->  K  e.  OL )
9928, 83, 93olm11 28696 . . . . . . . . . 10  |-  ( ( K  e.  OL  /\  ( P  .\/  ( F `
 P ) )  e.  ( Base `  K
) )  ->  (
( P  .\/  ( F `  P )
)  ./\  ( 1. `  K ) )  =  ( P  .\/  ( F `  P )
) )
10098, 88, 99syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( 1. `  K ) )  =  ( P  .\/  ( F `  P )
) )
10196, 100eqtrd 2316 . . . . . . . 8  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( P  .\/  W ) )  =  ( P  .\/  ( F `  P )
) )
10292, 101eqtrd 2316 . . . . . . 7  |-  ( ph  ->  ( P  .\/  (
( P  .\/  ( F `  P )
)  ./\  W )
)  =  ( P 
.\/  ( F `  P ) ) )
10386, 102eqtrd 2316 . . . . . 6  |-  ( ph  ->  ( P  .\/  ( R `  F )
)  =  ( P 
.\/  ( F `  P ) ) )
10482, 103breqtrrd 4050 . . . . 5  |-  ( ph  ->  ( F `  P
)  .<_  ( P  .\/  ( R `  F ) ) )
105 dia2dimlem1.rf . . . . . . 7  |-  ( ph  ->  ( R `  F
)  .<_  ( U  .\/  V ) )
10636, 8hlatjcom 28836 . . . . . . . 8  |-  ( ( K  e.  HL  /\  U  e.  A  /\  V  e.  A )  ->  ( U  .\/  V
)  =  ( V 
.\/  U ) )
1073, 15, 21, 106syl3anc 1182 . . . . . . 7  |-  ( ph  ->  ( U  .\/  V
)  =  ( V 
.\/  U ) )
108105, 107breqtrd 4048 . . . . . 6  |-  ( ph  ->  ( R `  F
)  .<_  ( V  .\/  U ) )
109 dia2dimlem1.ru . . . . . . 7  |-  ( ph  ->  ( R `  F
)  =/=  U )
1107, 36, 8hlatexch2 28864 . . . . . . 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 1195 . . . . . 6  |-  ( ph  ->  ( ( R `  F )  .<_  ( V 
.\/  U )  ->  V  .<_  ( ( R `
 F )  .\/  U ) ) )
112108, 111mpd 14 . . . . 5  |-  ( ph  ->  V  .<_  ( ( R `  F )  .\/  U ) )
113104, 112jca 518 . . . 4  |-  ( ph  ->  ( ( F `  P )  .<_  ( P 
.\/  ( R `  F ) )  /\  V  .<_  ( ( R `
 F )  .\/  U ) ) )
1147, 36, 83, 8ps-2c 28996 . . . 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 1214 . . 3  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )  e.  A )
1161, 115syl5eqel 2368 . 2  |-  ( ph  ->  Q  e.  A )
11728, 36, 8hlatjcl 28835 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  P  e.  A  /\  U  e.  A )  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
1183, 5, 15, 117syl3anc 1182 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
11928, 36, 8hlatjcl 28835 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( F `  P )  e.  A  /\  V  e.  A )  ->  (
( F `  P
)  .\/  V )  e.  ( Base `  K
) )
1203, 19, 21, 119syl3anc 1182 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F `  P )  .\/  V
)  e.  ( Base `  K ) )
12128, 7, 83latmle1 14178 . . . . . . . . . . . 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 1182 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )  .<_  ( P  .\/  U ) )
1231, 122syl5eqbr 4057 . . . . . . . . . 10  |-  ( ph  ->  Q  .<_  ( P  .\/  U ) )
12428, 8atbase 28758 . . . . . . . . . . . . 13  |-  ( Q  e.  A  ->  Q  e.  ( Base `  K
) )
125116, 124syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( Base `  K ) )
12628, 7, 83latlem12 14180 . . . . . . . . . . . 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 1184 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  .<_  ( P  .\/  U )  /\  Q  .<_  W )  <-> 
Q  .<_  ( ( P 
.\/  U )  ./\  W ) ) )
128127biimpd 198 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  .<_  ( P  .\/  U )  /\  Q  .<_  W )  ->  Q  .<_  ( ( P  .\/  U ) 
./\  W ) ) )
129123, 128mpand 656 . . . . . . . . 9  |-  ( ph  ->  ( Q  .<_  W  ->  Q  .<_  ( ( P 
.\/  U )  ./\  W ) ) )
130129imp 418 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  ( ( P  .\/  U
)  ./\  W )
)
131 eqid 2284 . . . . . . . . . . . . 13  |-  ( 0.
`  K )  =  ( 0. `  K
)
1327, 83, 131, 8, 9lhpmat 29498 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  -> 
( P  ./\  W
)  =  ( 0.
`  K ) )
1332, 4, 132syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( P  ./\  W
)  =  ( 0.
`  K ) )
134133oveq1d 5835 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  ./\  W )  .\/  U )  =  ( ( 0.
`  K )  .\/  U ) )
13528, 7, 36, 83, 8atmod4i1 29334 . . . . . . . . . . 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 1195 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  ./\  W )  .\/  U )  =  ( ( P 
.\/  U )  ./\  W ) )
13728, 36, 131olj02 28695 . . . . . . . . . . 11  |-  ( ( K  e.  OL  /\  U  e.  ( Base `  K ) )  -> 
( ( 0. `  K )  .\/  U
)  =  U )
13898, 32, 137syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( ( 0. `  K )  .\/  U
)  =  U )
139134, 136, 1383eqtr3d 2324 . . . . . . . . 9  |-  ( ph  ->  ( ( P  .\/  U )  ./\  W )  =  U )
140139adantr 451 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  ( ( P  .\/  U )  ./\  W )  =  U )
141130, 140breqtrd 4048 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  U )
142 hlatl 28829 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  AtLat )
1433, 142syl 15 . . . . . . . . 9  |-  ( ph  ->  K  e.  AtLat )
144143adantr 451 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  K  e.  AtLat
)
145116adantr 451 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  e.  A )
14615adantr 451 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  U  e.  A )
1477, 8atcmp 28780 . . . . . . . 8  |-  ( ( K  e.  AtLat  /\  Q  e.  A  /\  U  e.  A )  ->  ( Q  .<_  U  <->  Q  =  U ) )
148144, 145, 146, 147syl3anc 1182 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  ( Q  .<_  U  <->  Q  =  U
) )
149141, 148mpbid 201 . . . . . 6  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  =  U )
15028, 7, 83latmle2 14179 . . . . . . . . . . . 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 1182 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )  .<_  ( ( F `  P )  .\/  V
) )
1521, 151syl5eqbr 4057 . . . . . . . . . 10  |-  ( ph  ->  Q  .<_  ( ( F `  P )  .\/  V ) )
15328, 7, 83latlem12 14180 . . . . . . . . . . . 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 1184 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  .<_  ( ( F `  P
)  .\/  V )  /\  Q  .<_  W )  <-> 
Q  .<_  ( ( ( F `  P ) 
.\/  V )  ./\  W ) ) )
155154biimpd 198 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  .<_  ( ( F `  P
)  .\/  V )  /\  Q  .<_  W )  ->  Q  .<_  ( ( ( F `  P
)  .\/  V )  ./\  W ) ) )
156152, 155mpand 656 . . . . . . . . 9  |-  ( ph  ->  ( Q  .<_  W  ->  Q  .<_  ( ( ( F `  P ) 
.\/  V )  ./\  W ) ) )
157156imp 418 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  ( ( ( F `  P )  .\/  V
)  ./\  W )
)
1587, 83, 131, 8, 9lhpmat 29498 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( F `
 P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )  -> 
( ( F `  P )  ./\  W
)  =  ( 0.
`  K ) )
1592, 18, 158syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F `  P )  ./\  W
)  =  ( 0.
`  K ) )
160159oveq1d 5835 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 P )  ./\  W )  .\/  V )  =  ( ( 0.
`  K )  .\/  V ) )
16128, 8atbase 28758 . . . . . . . . . . . 12  |-  ( ( F `  P )  e.  A  ->  ( F `  P )  e.  ( Base `  K
) )
16219, 161syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  P
)  e.  ( Base `  K ) )
16328, 7, 36, 83, 8atmod4i1 29334 . . . . . . . . . . 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 1195 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 P )  ./\  W )  .\/  V )  =  ( ( ( F `  P ) 
.\/  V )  ./\  W ) )
16528, 36, 131olj02 28695 . . . . . . . . . . 11  |-  ( ( K  e.  OL  /\  V  e.  ( Base `  K ) )  -> 
( ( 0. `  K )  .\/  V
)  =  V )
16698, 72, 165syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( ( 0. `  K )  .\/  V
)  =  V )
167160, 164, 1663eqtr3d 2324 . . . . . . . . 9  |-  ( ph  ->  ( ( ( F `
 P )  .\/  V )  ./\  W )  =  V )
168167adantr 451 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  ( (
( F `  P
)  .\/  V )  ./\  W )  =  V )
169157, 168breqtrd 4048 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  V )
17021adantr 451 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  V  e.  A )
1717, 8atcmp 28780 . . . . . . . 8  |-  ( ( K  e.  AtLat  /\  Q  e.  A  /\  V  e.  A )  ->  ( Q  .<_  V  <->  Q  =  V ) )
172144, 145, 170, 171syl3anc 1182 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  ( Q  .<_  V  <->  Q  =  V
) )
173169, 172mpbid 201 . . . . . 6  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  =  V )
174149, 173eqtr3d 2318 . . . . 5  |-  ( (
ph  /\  Q  .<_  W )  ->  U  =  V )
175174ex 423 . . . 4  |-  ( ph  ->  ( Q  .<_  W  ->  U  =  V )
)
176175necon3ad 2483 . . 3  |-  ( ph  ->  ( U  =/=  V  ->  -.  Q  .<_  W ) )
17765, 176mpd 14 . 2  |-  ( ph  ->  -.  Q  .<_  W )
178116, 177jca 518 1  |-  ( ph  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1685    =/= wne 2447   class class class wbr 4024   ` cfv 5221  (class class class)co 5820   Basecbs 13144   lecple 13211   joincjn 14074   meetcmee 14075   0.cp0 14139   1.cp1 14140   Latclat 14147   OLcol 28643   Atomscatm 28732   AtLatcal 28733   HLchlt 28819   LHypclh 29452   LTrncltrn 29569   trLctrl 29626
This theorem is referenced by:  dia2dimlem3  30535  dia2dimlem6  30538
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-iun 3908  df-iin 3909  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-ov 5823  df-oprab 5824  df-mpt2 5825  df-1st 6084  df-2nd 6085  df-iota 6253  df-undef 6292  df-riota 6300  df-map 6770  df-poset 14076  df-plt 14088  df-lub 14104  df-glb 14105  df-join 14106  df-meet 14107  df-p0 14141  df-p1 14142  df-lat 14148  df-clat 14210  df-oposet 28645  df-ol 28647  df-oml 28648  df-covers 28735  df-ats 28736  df-atl 28767  df-cvlat 28791  df-hlat 28820  df-llines 28966  df-psubsp 28971  df-pmap 28972  df-padd 29264  df-lhyp 29456  df-laut 29457  df-ldil 29572  df-ltrn 29573  df-trl 29627
  Copyright terms: Public domain W3C validator