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

Theorem dia2dimlem1 31551
Description: Lemma for dia2dim 31564. 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 446 . . . 4  |-  ( ph  ->  K  e.  HL )
4 dia2dimlem1.p . . . . 5  |-  ( ph  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
54simpld 446 . . . 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 30655 . . . . 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 1184 . . . 4  |-  ( ph  ->  ( R `  F
)  e.  A )
14 dia2dimlem1.u . . . . 5  |-  ( ph  ->  ( U  e.  A  /\  U  .<_  W ) )
1514simpld 446 . . . 4  |-  ( ph  ->  U  e.  A )
166simpld 446 . . . . . 6  |-  ( ph  ->  F  e.  T )
177, 8, 9, 10ltrnel 30625 . . . . . 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 1184 . . . . 5  |-  ( ph  ->  ( ( F `  P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )
1918simpld 446 . . . 4  |-  ( ph  ->  ( F `  P
)  e.  A )
20 dia2dimlem1.v . . . . 5  |-  ( ph  ->  ( V  e.  A  /\  V  .<_  W ) )
2120simpld 446 . . . 4  |-  ( ph  ->  V  e.  A )
224simprd 450 . . . . . 6  |-  ( ph  ->  -.  P  .<_  W )
237, 9, 10, 11trlle 30670 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  .<_  W )
242, 16, 23syl2anc 643 . . . . . . . 8  |-  ( ph  ->  ( R `  F
)  .<_  W )
2514simprd 450 . . . . . . . 8  |-  ( ph  ->  U  .<_  W )
26 hllat 29850 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  Lat )
273, 26syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  Lat )
28 eqid 2408 . . . . . . . . . . 11  |-  ( Base `  K )  =  (
Base `  K )
2928, 8atbase 29776 . . . . . . . . . 10  |-  ( ( R `  F )  e.  A  ->  ( R `  F )  e.  ( Base `  K
) )
3013, 29syl 16 . . . . . . . . 9  |-  ( ph  ->  ( R `  F
)  e.  ( Base `  K ) )
3128, 8atbase 29776 . . . . . . . . . 10  |-  ( U  e.  A  ->  U  e.  ( Base `  K
) )
3215, 31syl 16 . . . . . . . . 9  |-  ( ph  ->  U  e.  ( Base `  K ) )
332simprd 450 . . . . . . . . . 10  |-  ( ph  ->  W  e.  H )
3428, 9lhpbase 30484 . . . . . . . . . 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 14450 . . . . . . . . 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 1186 . . . . . . . 8  |-  ( ph  ->  ( ( ( R `
 F )  .<_  W  /\  U  .<_  W )  <-> 
( ( R `  F )  .\/  U
)  .<_  W ) )
3924, 25, 38mpbi2and 888 . . . . . . 7  |-  ( ph  ->  ( ( R `  F )  .\/  U
)  .<_  W )
4028, 8atbase 29776 . . . . . . . . 9  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
415, 40syl 16 . . . . . . . 8  |-  ( ph  ->  P  e.  ( Base `  K ) )
4228, 36, 8hlatjcl 29853 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( R `  F )  e.  A  /\  U  e.  A )  ->  (
( R `  F
)  .\/  U )  e.  ( Base `  K
) )
433, 13, 15, 42syl3anc 1184 . . . . . . . 8  |-  ( ph  ->  ( ( R `  F )  .\/  U
)  e.  ( Base `  K ) )
4428, 7lattr 14444 . . . . . . . 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 1186 . . . . . . 7  |-  ( ph  ->  ( ( P  .<_  ( ( R `  F
)  .\/  U )  /\  ( ( R `  F )  .\/  U
)  .<_  W )  ->  P  .<_  W ) )
4639, 45mpan2d 656 . . . . . 6  |-  ( ph  ->  ( P  .<_  ( ( R `  F ) 
.\/  U )  ->  P  .<_  W ) )
4722, 46mtod 170 . . . . 5  |-  ( ph  ->  -.  P  .<_  ( ( R `  F ) 
.\/  U ) )
4820simprd 450 . . . . . . 7  |-  ( ph  ->  V  .<_  W )
4918simprd 450 . . . . . . 7  |-  ( ph  ->  -.  ( F `  P )  .<_  W )
50 nbrne2 4194 . . . . . . 7  |-  ( ( V  .<_  W  /\  -.  ( F `  P
)  .<_  W )  ->  V  =/=  ( F `  P ) )
5148, 49, 50syl2anc 643 . . . . . 6  |-  ( ph  ->  V  =/=  ( F `
 P ) )
5251necomd 2654 . . . . 5  |-  ( ph  ->  ( F `  P
)  =/=  V )
5347, 52jca 519 . . . 4  |-  ( ph  ->  ( -.  P  .<_  ( ( R `  F
)  .\/  U )  /\  ( F `  P
)  =/=  V ) )
5427adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  K  e.  Lat )
5541adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  P  e.  ( Base `  K )
)
5628, 36, 8hlatjcl 29853 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  V  e.  A  /\  U  e.  A )  ->  ( V  .\/  U
)  e.  ( Base `  K ) )
573, 21, 15, 56syl3anc 1184 . . . . . . . . 9  |-  ( ph  ->  ( V  .\/  U
)  e.  ( Base `  K ) )
5857adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( V  .\/  U )  e.  (
Base `  K )
)
5935adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  W  e.  ( Base `  K )
)
607, 36, 8hlatlej2 29862 . . . . . . . . . . . 12  |-  ( ( K  e.  HL  /\  ( F `  P )  e.  A  /\  V  e.  A )  ->  V  .<_  ( ( F `  P )  .\/  V
) )
613, 19, 21, 60syl3anc 1184 . . . . . . . . . . 11  |-  ( ph  ->  V  .<_  ( ( F `  P )  .\/  V ) )
6261adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  V  .<_  ( ( F `  P
)  .\/  V )
)
63 simpr 448 . . . . . . . . . 10  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)
6462, 63breqtrrd 4202 . . . . . . . . 9  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  V  .<_  ( P  .\/  U ) )
65 dia2dimlem1.uv . . . . . . . . . . . 12  |-  ( ph  ->  U  =/=  V )
6665necomd 2654 . . . . . . . . . . 11  |-  ( ph  ->  V  =/=  U )
677, 36, 8hlatexch2 29882 . . . . . . . . . . 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 1197 . . . . . . . . . 10  |-  ( ph  ->  ( V  .<_  ( P 
.\/  U )  ->  P  .<_  ( V  .\/  U ) ) )
6968adantr 452 . . . . . . . . 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 29776 . . . . . . . . . . . 12  |-  ( V  e.  A  ->  V  e.  ( Base `  K
) )
7221, 71syl 16 . . . . . . . . . . 11  |-  ( ph  ->  V  e.  ( Base `  K ) )
7328, 7, 36latjle12 14450 . . . . . . . . . . 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 1186 . . . . . . . . . 10  |-  ( ph  ->  ( ( V  .<_  W  /\  U  .<_  W )  <-> 
( V  .\/  U
)  .<_  W ) )
7548, 25, 74mpbi2and 888 . . . . . . . . 9  |-  ( ph  ->  ( V  .\/  U
)  .<_  W )
7675adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  ( V  .\/  U )  .<_  W )
7728, 7, 54, 55, 58, 59, 70, 76lattrd 14446 . . . . . . 7  |-  ( (
ph  /\  ( P  .\/  U )  =  ( ( F `  P
)  .\/  V )
)  ->  P  .<_  W )
7877ex 424 . . . . . 6  |-  ( ph  ->  ( ( P  .\/  U )  =  ( ( F `  P ) 
.\/  V )  ->  P  .<_  W ) )
7978necon3bd 2608 . . . . 5  |-  ( ph  ->  ( -.  P  .<_  W  ->  ( P  .\/  U )  =/=  ( ( F `  P ) 
.\/  V ) ) )
8022, 79mpd 15 . . . 4  |-  ( ph  ->  ( P  .\/  U
)  =/=  ( ( F `  P ) 
.\/  V ) )
817, 36, 8hlatlej2 29862 . . . . . . 7  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  -> 
( F `  P
)  .<_  ( P  .\/  ( F `  P ) ) )
823, 5, 19, 81syl3anc 1184 . . . . . 6  |-  ( ph  ->  ( F `  P
)  .<_  ( P  .\/  ( F `  P ) ) )
83 dia2dimlem1.m . . . . . . . . . 10  |-  ./\  =  ( meet `  K )
847, 36, 83, 8, 9, 10, 11trlval2 30649 . . . . . . . . 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 1184 . . . . . . . 8  |-  ( ph  ->  ( R `  F
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  W ) )
8685oveq2d 6060 . . . . . . 7  |-  ( ph  ->  ( P  .\/  ( R `  F )
)  =  ( P 
.\/  ( ( P 
.\/  ( F `  P ) )  ./\  W ) ) )
8728, 36, 8hlatjcl 29853 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  -> 
( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
883, 5, 19, 87syl3anc 1184 . . . . . . . . 9  |-  ( ph  ->  ( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
897, 36, 8hlatlej1 29861 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  ->  P  .<_  ( P  .\/  ( F `  P ) ) )
903, 5, 19, 89syl3anc 1184 . . . . . . . . 9  |-  ( ph  ->  P  .<_  ( P  .\/  ( F `  P
) ) )
9128, 7, 36, 83, 8atmod3i1 30350 . . . . . . . . 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 1197 . . . . . . . 8  |-  ( ph  ->  ( P  .\/  (
( P  .\/  ( F `  P )
)  ./\  W )
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  ( P  .\/  W ) ) )
93 eqid 2408 . . . . . . . . . . . 12  |-  ( 1.
`  K )  =  ( 1. `  K
)
947, 36, 93, 8, 9lhpjat2 30507 . . . . . . . . . . 11  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  -> 
( P  .\/  W
)  =  ( 1.
`  K ) )
952, 4, 94syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( P  .\/  W
)  =  ( 1.
`  K ) )
9695oveq2d 6060 . . . . . . . . 9  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( P  .\/  W ) )  =  ( ( P  .\/  ( F `  P ) )  ./\  ( 1. `  K ) ) )
97 hlol 29848 . . . . . . . . . . 11  |-  ( K  e.  HL  ->  K  e.  OL )
983, 97syl 16 . . . . . . . . . 10  |-  ( ph  ->  K  e.  OL )
9928, 83, 93olm11 29714 . . . . . . . . . 10  |-  ( ( K  e.  OL  /\  ( P  .\/  ( F `
 P ) )  e.  ( Base `  K
) )  ->  (
( P  .\/  ( F `  P )
)  ./\  ( 1. `  K ) )  =  ( P  .\/  ( F `  P )
) )
10098, 88, 99syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( 1. `  K ) )  =  ( P  .\/  ( F `  P )
) )
10196, 100eqtrd 2440 . . . . . . . 8  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( P  .\/  W ) )  =  ( P  .\/  ( F `  P )
) )
10292, 101eqtrd 2440 . . . . . . 7  |-  ( ph  ->  ( P  .\/  (
( P  .\/  ( F `  P )
)  ./\  W )
)  =  ( P 
.\/  ( F `  P ) ) )
10386, 102eqtrd 2440 . . . . . 6  |-  ( ph  ->  ( P  .\/  ( R `  F )
)  =  ( P 
.\/  ( F `  P ) ) )
10482, 103breqtrrd 4202 . . . . 5  |-  ( ph  ->  ( F `  P
)  .<_  ( P  .\/  ( R `  F ) ) )
105 dia2dimlem1.rf . . . . . . 7  |-  ( ph  ->  ( R `  F
)  .<_  ( U  .\/  V ) )
10636, 8hlatjcom 29854 . . . . . . . 8  |-  ( ( K  e.  HL  /\  U  e.  A  /\  V  e.  A )  ->  ( U  .\/  V
)  =  ( V 
.\/  U ) )
1073, 15, 21, 106syl3anc 1184 . . . . . . 7  |-  ( ph  ->  ( U  .\/  V
)  =  ( V 
.\/  U ) )
108105, 107breqtrd 4200 . . . . . 6  |-  ( ph  ->  ( R `  F
)  .<_  ( V  .\/  U ) )
109 dia2dimlem1.ru . . . . . . 7  |-  ( ph  ->  ( R `  F
)  =/=  U )
1107, 36, 8hlatexch2 29882 . . . . . . 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 1197 . . . . . 6  |-  ( ph  ->  ( ( R `  F )  .<_  ( V 
.\/  U )  ->  V  .<_  ( ( R `
 F )  .\/  U ) ) )
112108, 111mpd 15 . . . . 5  |-  ( ph  ->  V  .<_  ( ( R `  F )  .\/  U ) )
113104, 112jca 519 . . . 4  |-  ( ph  ->  ( ( F `  P )  .<_  ( P 
.\/  ( R `  F ) )  /\  V  .<_  ( ( R `
 F )  .\/  U ) ) )
1147, 36, 83, 8ps-2c 30014 . . . 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 1216 . . 3  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )  e.  A )
1161, 115syl5eqel 2492 . 2  |-  ( ph  ->  Q  e.  A )
11728, 36, 8hlatjcl 29853 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  P  e.  A  /\  U  e.  A )  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
1183, 5, 15, 117syl3anc 1184 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
11928, 36, 8hlatjcl 29853 . . . . . . . . . . . . 13  |-  ( ( K  e.  HL  /\  ( F `  P )  e.  A  /\  V  e.  A )  ->  (
( F `  P
)  .\/  V )  e.  ( Base `  K
) )
1203, 19, 21, 119syl3anc 1184 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F `  P )  .\/  V
)  e.  ( Base `  K ) )
12128, 7, 83latmle1 14464 . . . . . . . . . . . 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 1184 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )  .<_  ( P  .\/  U ) )
1231, 122syl5eqbr 4209 . . . . . . . . . 10  |-  ( ph  ->  Q  .<_  ( P  .\/  U ) )
12428, 8atbase 29776 . . . . . . . . . . . . 13  |-  ( Q  e.  A  ->  Q  e.  ( Base `  K
) )
125116, 124syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( Base `  K ) )
12628, 7, 83latlem12 14466 . . . . . . . . . . . 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 1186 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  .<_  ( P  .\/  U )  /\  Q  .<_  W )  <-> 
Q  .<_  ( ( P 
.\/  U )  ./\  W ) ) )
128127biimpd 199 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  .<_  ( P  .\/  U )  /\  Q  .<_  W )  ->  Q  .<_  ( ( P  .\/  U ) 
./\  W ) ) )
129123, 128mpand 657 . . . . . . . . 9  |-  ( ph  ->  ( Q  .<_  W  ->  Q  .<_  ( ( P 
.\/  U )  ./\  W ) ) )
130129imp 419 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  ( ( P  .\/  U
)  ./\  W )
)
131 eqid 2408 . . . . . . . . . . . . 13  |-  ( 0.
`  K )  =  ( 0. `  K
)
1327, 83, 131, 8, 9lhpmat 30516 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  -> 
( P  ./\  W
)  =  ( 0.
`  K ) )
1332, 4, 132syl2anc 643 . . . . . . . . . . 11  |-  ( ph  ->  ( P  ./\  W
)  =  ( 0.
`  K ) )
134133oveq1d 6059 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  ./\  W )  .\/  U )  =  ( ( 0.
`  K )  .\/  U ) )
13528, 7, 36, 83, 8atmod4i1 30352 . . . . . . . . . . 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 1197 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  ./\  W )  .\/  U )  =  ( ( P 
.\/  U )  ./\  W ) )
13728, 36, 131olj02 29713 . . . . . . . . . . 11  |-  ( ( K  e.  OL  /\  U  e.  ( Base `  K ) )  -> 
( ( 0. `  K )  .\/  U
)  =  U )
13898, 32, 137syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( ( 0. `  K )  .\/  U
)  =  U )
139134, 136, 1383eqtr3d 2448 . . . . . . . . 9  |-  ( ph  ->  ( ( P  .\/  U )  ./\  W )  =  U )
140139adantr 452 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  ( ( P  .\/  U )  ./\  W )  =  U )
141130, 140breqtrd 4200 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  U )
142 hlatl 29847 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  AtLat )
1433, 142syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  AtLat )
144143adantr 452 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  K  e.  AtLat
)
145116adantr 452 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  e.  A )
14615adantr 452 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  U  e.  A )
1477, 8atcmp 29798 . . . . . . . 8  |-  ( ( K  e.  AtLat  /\  Q  e.  A  /\  U  e.  A )  ->  ( Q  .<_  U  <->  Q  =  U ) )
148144, 145, 146, 147syl3anc 1184 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  ( Q  .<_  U  <->  Q  =  U
) )
149141, 148mpbid 202 . . . . . 6  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  =  U )
15028, 7, 83latmle2 14465 . . . . . . . . . . . 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 1184 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )  .<_  ( ( F `  P )  .\/  V
) )
1521, 151syl5eqbr 4209 . . . . . . . . . 10  |-  ( ph  ->  Q  .<_  ( ( F `  P )  .\/  V ) )
15328, 7, 83latlem12 14466 . . . . . . . . . . . 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 1186 . . . . . . . . . . 11  |-  ( ph  ->  ( ( Q  .<_  ( ( F `  P
)  .\/  V )  /\  Q  .<_  W )  <-> 
Q  .<_  ( ( ( F `  P ) 
.\/  V )  ./\  W ) ) )
155154biimpd 199 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  .<_  ( ( F `  P
)  .\/  V )  /\  Q  .<_  W )  ->  Q  .<_  ( ( ( F `  P
)  .\/  V )  ./\  W ) ) )
156152, 155mpand 657 . . . . . . . . 9  |-  ( ph  ->  ( Q  .<_  W  ->  Q  .<_  ( ( ( F `  P ) 
.\/  V )  ./\  W ) ) )
157156imp 419 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  ( ( ( F `  P )  .\/  V
)  ./\  W )
)
1587, 83, 131, 8, 9lhpmat 30516 . . . . . . . . . . . 12  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( ( F `
 P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )  -> 
( ( F `  P )  ./\  W
)  =  ( 0.
`  K ) )
1592, 18, 158syl2anc 643 . . . . . . . . . . 11  |-  ( ph  ->  ( ( F `  P )  ./\  W
)  =  ( 0.
`  K ) )
160159oveq1d 6059 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 P )  ./\  W )  .\/  V )  =  ( ( 0.
`  K )  .\/  V ) )
16128, 8atbase 29776 . . . . . . . . . . . 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 30352 . . . . . . . . . . 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 1197 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( F `
 P )  ./\  W )  .\/  V )  =  ( ( ( F `  P ) 
.\/  V )  ./\  W ) )
16528, 36, 131olj02 29713 . . . . . . . . . . 11  |-  ( ( K  e.  OL  /\  V  e.  ( Base `  K ) )  -> 
( ( 0. `  K )  .\/  V
)  =  V )
16698, 72, 165syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( ( 0. `  K )  .\/  V
)  =  V )
167160, 164, 1663eqtr3d 2448 . . . . . . . . 9  |-  ( ph  ->  ( ( ( F `
 P )  .\/  V )  ./\  W )  =  V )
168167adantr 452 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  ( (
( F `  P
)  .\/  V )  ./\  W )  =  V )
169157, 168breqtrd 4200 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  .<_  V )
17021adantr 452 . . . . . . . 8  |-  ( (
ph  /\  Q  .<_  W )  ->  V  e.  A )
1717, 8atcmp 29798 . . . . . . . 8  |-  ( ( K  e.  AtLat  /\  Q  e.  A  /\  V  e.  A )  ->  ( Q  .<_  V  <->  Q  =  V ) )
172144, 145, 170, 171syl3anc 1184 . . . . . . 7  |-  ( (
ph  /\  Q  .<_  W )  ->  ( Q  .<_  V  <->  Q  =  V
) )
173169, 172mpbid 202 . . . . . 6  |-  ( (
ph  /\  Q  .<_  W )  ->  Q  =  V )
174149, 173eqtr3d 2442 . . . . 5  |-  ( (
ph  /\  Q  .<_  W )  ->  U  =  V )
175174ex 424 . . . 4  |-  ( ph  ->  ( Q  .<_  W  ->  U  =  V )
)
176175necon3ad 2607 . . 3  |-  ( ph  ->  ( U  =/=  V  ->  -.  Q  .<_  W ) )
17765, 176mpd 15 . 2  |-  ( ph  ->  -.  Q  .<_  W )
178116, 177jca 519 1  |-  ( ph  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721    =/= wne 2571   class class class wbr 4176   ` cfv 5417  (class class class)co 6044   Basecbs 13428   lecple 13495   joincjn 14360   meetcmee 14361   0.cp0 14425   1.cp1 14426   Latclat 14433   OLcol 29661   Atomscatm 29750   AtLatcal 29751   HLchlt 29837   LHypclh 30470   LTrncltrn 30587   trLctrl 30644
This theorem is referenced by:  dia2dimlem3  31553  dia2dimlem6  31556
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-rep 4284  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-nel 2574  df-ral 2675  df-rex 2676  df-reu 2677  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-iun 4059  df-iin 4060  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-1st 6312  df-2nd 6313  df-undef 6506  df-riota 6512  df-map 6983  df-poset 14362  df-plt 14374  df-lub 14390  df-glb 14391  df-join 14392  df-meet 14393  df-p0 14427  df-p1 14428  df-lat 14434  df-clat 14496  df-oposet 29663  df-ol 29665  df-oml 29666  df-covers 29753  df-ats 29754  df-atl 29785  df-cvlat 29809  df-hlat 29838  df-llines 29984  df-psubsp 29989  df-pmap 29990  df-padd 30282  df-lhyp 30474  df-laut 30475  df-ldil 30590  df-ltrn 30591  df-trl 30645
  Copyright terms: Public domain W3C validator