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

Theorem dia2dimlem2 34603
Description: Lemma for dia2dim 34615. Define a translation  G whose trace is atom  U. Part of proof of Lemma M in [Crawley] p. 121 line 4. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
dia2dimlem2.l  |-  .<_  =  ( le `  K )
dia2dimlem2.j  |-  .\/  =  ( join `  K )
dia2dimlem2.m  |-  ./\  =  ( meet `  K )
dia2dimlem2.a  |-  A  =  ( Atoms `  K )
dia2dimlem2.h  |-  H  =  ( LHyp `  K
)
dia2dimlem2.t  |-  T  =  ( ( LTrn `  K
) `  W )
dia2dimlem2.r  |-  R  =  ( ( trL `  K
) `  W )
dia2dimlem2.q  |-  Q  =  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )
dia2dimlem2.k  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
dia2dimlem2.u  |-  ( ph  ->  ( U  e.  A  /\  U  .<_  W ) )
dia2dimlem2.v  |-  ( ph  ->  ( V  e.  A  /\  V  .<_  W ) )
dia2dimlem2.p  |-  ( ph  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
dia2dimlem2.f  |-  ( ph  ->  ( F  e.  T  /\  ( F `  P
)  =/=  P ) )
dia2dimlem2.rf  |-  ( ph  ->  ( R `  F
)  .<_  ( U  .\/  V ) )
dia2dimlem2.rv  |-  ( ph  ->  ( R `  F
)  =/=  V )
dia2dimlem2.g  |-  ( ph  ->  G  e.  T )
dia2dimlem2.gv  |-  ( ph  ->  ( G `  P
)  =  Q )
Assertion
Ref Expression
dia2dimlem2  |-  ( ph  ->  ( R `  G
)  =  U )

Proof of Theorem dia2dimlem2
StepHypRef Expression
1 dia2dimlem2.k . . . . . . . . 9  |-  ( ph  ->  ( K  e.  HL  /\  W  e.  H ) )
21simpld 459 . . . . . . . 8  |-  ( ph  ->  K  e.  HL )
3 hllat 32901 . . . . . . . 8  |-  ( K  e.  HL  ->  K  e.  Lat )
42, 3syl 16 . . . . . . 7  |-  ( ph  ->  K  e.  Lat )
5 dia2dimlem2.p . . . . . . . . 9  |-  ( ph  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
65simpld 459 . . . . . . . 8  |-  ( ph  ->  P  e.  A )
7 eqid 2438 . . . . . . . . 9  |-  ( Base `  K )  =  (
Base `  K )
8 dia2dimlem2.a . . . . . . . . 9  |-  A  =  ( Atoms `  K )
97, 8atbase 32827 . . . . . . . 8  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
106, 9syl 16 . . . . . . 7  |-  ( ph  ->  P  e.  ( Base `  K ) )
11 dia2dimlem2.u . . . . . . . . 9  |-  ( ph  ->  ( U  e.  A  /\  U  .<_  W ) )
1211simpld 459 . . . . . . . 8  |-  ( ph  ->  U  e.  A )
137, 8atbase 32827 . . . . . . . 8  |-  ( U  e.  A  ->  U  e.  ( Base `  K
) )
1412, 13syl 16 . . . . . . 7  |-  ( ph  ->  U  e.  ( Base `  K ) )
15 dia2dimlem2.l . . . . . . . 8  |-  .<_  =  ( le `  K )
16 dia2dimlem2.j . . . . . . . 8  |-  .\/  =  ( join `  K )
177, 15, 16latlej2 15223 . . . . . . 7  |-  ( ( K  e.  Lat  /\  P  e.  ( Base `  K )  /\  U  e.  ( Base `  K
) )  ->  U  .<_  ( P  .\/  U
) )
184, 10, 14, 17syl3anc 1218 . . . . . 6  |-  ( ph  ->  U  .<_  ( P  .\/  U ) )
197, 16, 8hlatjcl 32904 . . . . . . . 8  |-  ( ( K  e.  HL  /\  P  e.  A  /\  U  e.  A )  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
202, 6, 12, 19syl3anc 1218 . . . . . . 7  |-  ( ph  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
21 dia2dimlem2.m . . . . . . . 8  |-  ./\  =  ( meet `  K )
227, 15, 21latleeqm2 15242 . . . . . . 7  |-  ( ( K  e.  Lat  /\  U  e.  ( Base `  K )  /\  ( P  .\/  U )  e.  ( Base `  K
) )  ->  ( U  .<_  ( P  .\/  U )  <->  ( ( P 
.\/  U )  ./\  U )  =  U ) )
234, 14, 20, 22syl3anc 1218 . . . . . 6  |-  ( ph  ->  ( U  .<_  ( P 
.\/  U )  <->  ( ( P  .\/  U )  ./\  U )  =  U ) )
2418, 23mpbid 210 . . . . 5  |-  ( ph  ->  ( ( P  .\/  U )  ./\  U )  =  U )
25 dia2dimlem2.rf . . . . . . . 8  |-  ( ph  ->  ( R `  F
)  .<_  ( U  .\/  V ) )
26 dia2dimlem2.f . . . . . . . . . 10  |-  ( ph  ->  ( F  e.  T  /\  ( F `  P
)  =/=  P ) )
27 dia2dimlem2.h . . . . . . . . . . 11  |-  H  =  ( LHyp `  K
)
28 dia2dimlem2.t . . . . . . . . . . 11  |-  T  =  ( ( LTrn `  K
) `  W )
29 dia2dimlem2.r . . . . . . . . . . 11  |-  R  =  ( ( trL `  K
) `  W )
3015, 8, 27, 28, 29trlat 33706 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( F  e.  T  /\  ( F `  P )  =/=  P ) )  ->  ( R `  F )  e.  A
)
311, 5, 26, 30syl3anc 1218 . . . . . . . . 9  |-  ( ph  ->  ( R `  F
)  e.  A )
32 dia2dimlem2.v . . . . . . . . . 10  |-  ( ph  ->  ( V  e.  A  /\  V  .<_  W ) )
3332simpld 459 . . . . . . . . 9  |-  ( ph  ->  V  e.  A )
34 dia2dimlem2.rv . . . . . . . . 9  |-  ( ph  ->  ( R `  F
)  =/=  V )
3515, 16, 8hlatexch2 32933 . . . . . . . . 9  |-  ( ( K  e.  HL  /\  ( ( R `  F )  e.  A  /\  U  e.  A  /\  V  e.  A
)  /\  ( R `  F )  =/=  V
)  ->  ( ( R `  F )  .<_  ( U  .\/  V
)  ->  U  .<_  ( ( R `  F
)  .\/  V )
) )
362, 31, 12, 33, 34, 35syl131anc 1231 . . . . . . . 8  |-  ( ph  ->  ( ( R `  F )  .<_  ( U 
.\/  V )  ->  U  .<_  ( ( R `
 F )  .\/  V ) ) )
3725, 36mpd 15 . . . . . . 7  |-  ( ph  ->  U  .<_  ( ( R `  F )  .\/  V ) )
3826simpld 459 . . . . . . . . . 10  |-  ( ph  ->  F  e.  T )
3915, 16, 21, 8, 27, 28, 29trlval2 33700 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  W )
)
401, 38, 5, 39syl3anc 1218 . . . . . . . . 9  |-  ( ph  ->  ( R `  F
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  W ) )
4140oveq1d 6101 . . . . . . . 8  |-  ( ph  ->  ( ( R `  F )  .\/  V
)  =  ( ( ( P  .\/  ( F `  P )
)  ./\  W )  .\/  V ) )
4215, 8, 27, 28ltrnel 33676 . . . . . . . . . . . . 13  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( F `  P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )
431, 38, 5, 42syl3anc 1218 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F `  P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )
4443simpld 459 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  P
)  e.  A )
457, 16, 8hlatjcl 32904 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  -> 
( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
462, 6, 44, 45syl3anc 1218 . . . . . . . . . 10  |-  ( ph  ->  ( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
471simprd 463 . . . . . . . . . . 11  |-  ( ph  ->  W  e.  H )
487, 27lhpbase 33535 . . . . . . . . . . 11  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
4947, 48syl 16 . . . . . . . . . 10  |-  ( ph  ->  W  e.  ( Base `  K ) )
5032simprd 463 . . . . . . . . . 10  |-  ( ph  ->  V  .<_  W )
517, 15, 16, 21, 8atmod4i1 33403 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  ( V  e.  A  /\  ( P  .\/  ( F `  P )
)  e.  ( Base `  K )  /\  W  e.  ( Base `  K
) )  /\  V  .<_  W )  ->  (
( ( P  .\/  ( F `  P ) )  ./\  W )  .\/  V )  =  ( ( ( P  .\/  ( F `  P ) )  .\/  V ) 
./\  W ) )
522, 33, 46, 49, 50, 51syl131anc 1231 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P 
.\/  ( F `  P ) )  ./\  W )  .\/  V )  =  ( ( ( P  .\/  ( F `
 P ) ) 
.\/  V )  ./\  W ) )
5316, 8hlatjass 32907 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  ( F `  P
)  e.  A  /\  V  e.  A )
)  ->  ( ( P  .\/  ( F `  P ) )  .\/  V )  =  ( P 
.\/  ( ( F `
 P )  .\/  V ) ) )
542, 6, 44, 33, 53syl13anc 1220 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  .\/  V )  =  ( P  .\/  ( ( F `  P )  .\/  V
) ) )
5554oveq1d 6101 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P 
.\/  ( F `  P ) )  .\/  V )  ./\  W )  =  ( ( P 
.\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) )
5652, 55eqtrd 2470 . . . . . . . 8  |-  ( ph  ->  ( ( ( P 
.\/  ( F `  P ) )  ./\  W )  .\/  V )  =  ( ( P 
.\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) )
5741, 56eqtrd 2470 . . . . . . 7  |-  ( ph  ->  ( ( R `  F )  .\/  V
)  =  ( ( P  .\/  ( ( F `  P ) 
.\/  V ) ) 
./\  W ) )
5837, 57breqtrd 4311 . . . . . 6  |-  ( ph  ->  U  .<_  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) )
597, 16, 8hlatjcl 32904 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  ( F `  P )  e.  A  /\  V  e.  A )  ->  (
( F `  P
)  .\/  V )  e.  ( Base `  K
) )
602, 44, 33, 59syl3anc 1218 . . . . . . . . 9  |-  ( ph  ->  ( ( F `  P )  .\/  V
)  e.  ( Base `  K ) )
617, 16latjcl 15213 . . . . . . . . 9  |-  ( ( K  e.  Lat  /\  P  e.  ( Base `  K )  /\  (
( F `  P
)  .\/  V )  e.  ( Base `  K
) )  ->  ( P  .\/  ( ( F `
 P )  .\/  V ) )  e.  (
Base `  K )
)
624, 10, 60, 61syl3anc 1218 . . . . . . . 8  |-  ( ph  ->  ( P  .\/  (
( F `  P
)  .\/  V )
)  e.  ( Base `  K ) )
637, 21latmcl 15214 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( P  .\/  ( ( F `  P ) 
.\/  V ) )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
)  e.  ( Base `  K ) )
644, 62, 49, 63syl3anc 1218 . . . . . . 7  |-  ( ph  ->  ( ( P  .\/  ( ( F `  P )  .\/  V
) )  ./\  W
)  e.  ( Base `  K ) )
657, 15, 21latmlem2 15244 . . . . . . 7  |-  ( ( K  e.  Lat  /\  ( U  e.  ( Base `  K )  /\  ( ( P  .\/  ( ( F `  P )  .\/  V
) )  ./\  W
)  e.  ( Base `  K )  /\  ( P  .\/  U )  e.  ( Base `  K
) ) )  -> 
( U  .<_  ( ( P  .\/  ( ( F `  P ) 
.\/  V ) ) 
./\  W )  -> 
( ( P  .\/  U )  ./\  U )  .<_  ( ( P  .\/  U )  ./\  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) ) ) )
664, 14, 64, 20, 65syl13anc 1220 . . . . . 6  |-  ( ph  ->  ( U  .<_  ( ( P  .\/  ( ( F `  P ) 
.\/  V ) ) 
./\  W )  -> 
( ( P  .\/  U )  ./\  U )  .<_  ( ( P  .\/  U )  ./\  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) ) ) )
6758, 66mpd 15 . . . . 5  |-  ( ph  ->  ( ( P  .\/  U )  ./\  U )  .<_  ( ( P  .\/  U )  ./\  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) ) )
6824, 67eqbrtrrd 4309 . . . 4  |-  ( ph  ->  U  .<_  ( ( P  .\/  U )  ./\  ( ( P  .\/  ( ( F `  P )  .\/  V
) )  ./\  W
) ) )
69 dia2dimlem2.g . . . . . . 7  |-  ( ph  ->  G  e.  T )
7015, 16, 21, 8, 27, 28, 29trlval2 33700 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  G )  =  ( ( P  .\/  ( G `  P )
)  ./\  W )
)
711, 69, 5, 70syl3anc 1218 . . . . . 6  |-  ( ph  ->  ( R `  G
)  =  ( ( P  .\/  ( G `
 P ) ) 
./\  W ) )
72 dia2dimlem2.gv . . . . . . . . . 10  |-  ( ph  ->  ( G `  P
)  =  Q )
73 dia2dimlem2.q . . . . . . . . . 10  |-  Q  =  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) )
7472, 73syl6eq 2486 . . . . . . . . 9  |-  ( ph  ->  ( G `  P
)  =  ( ( P  .\/  U ) 
./\  ( ( F `
 P )  .\/  V ) ) )
7574oveq2d 6102 . . . . . . . 8  |-  ( ph  ->  ( P  .\/  ( G `  P )
)  =  ( P 
.\/  ( ( P 
.\/  U )  ./\  ( ( F `  P )  .\/  V
) ) ) )
7675oveq1d 6101 . . . . . . 7  |-  ( ph  ->  ( ( P  .\/  ( G `  P ) )  ./\  W )  =  ( ( P 
.\/  ( ( P 
.\/  U )  ./\  ( ( F `  P )  .\/  V
) ) )  ./\  W ) )
7715, 16, 8hlatlej1 32912 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  P  e.  A  /\  U  e.  A )  ->  P  .<_  ( P  .\/  U ) )
782, 6, 12, 77syl3anc 1218 . . . . . . . . . 10  |-  ( ph  ->  P  .<_  ( P  .\/  U ) )
797, 15, 16, 21, 8atmod3i1 33401 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  ( P  e.  A  /\  ( P  .\/  U
)  e.  ( Base `  K )  /\  (
( F `  P
)  .\/  V )  e.  ( Base `  K
) )  /\  P  .<_  ( P  .\/  U
) )  ->  ( P  .\/  ( ( P 
.\/  U )  ./\  ( ( F `  P )  .\/  V
) ) )  =  ( ( P  .\/  U )  ./\  ( P  .\/  ( ( F `  P )  .\/  V
) ) ) )
802, 6, 20, 60, 78, 79syl131anc 1231 . . . . . . . . 9  |-  ( ph  ->  ( P  .\/  (
( P  .\/  U
)  ./\  ( ( F `  P )  .\/  V ) ) )  =  ( ( P 
.\/  U )  ./\  ( P  .\/  ( ( F `  P ) 
.\/  V ) ) ) )
8180oveq1d 6101 . . . . . . . 8  |-  ( ph  ->  ( ( P  .\/  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) ) ) 
./\  W )  =  ( ( ( P 
.\/  U )  ./\  ( P  .\/  ( ( F `  P ) 
.\/  V ) ) )  ./\  W )
)
82 hlol 32899 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  OL )
832, 82syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  OL )
847, 21latmassOLD 32767 . . . . . . . . 9  |-  ( ( K  e.  OL  /\  ( ( P  .\/  U )  e.  ( Base `  K )  /\  ( P  .\/  ( ( F `
 P )  .\/  V ) )  e.  (
Base `  K )  /\  W  e.  ( Base `  K ) ) )  ->  ( (
( P  .\/  U
)  ./\  ( P  .\/  ( ( F `  P )  .\/  V
) ) )  ./\  W )  =  ( ( P  .\/  U ) 
./\  ( ( P 
.\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) ) )
8583, 20, 62, 49, 84syl13anc 1220 . . . . . . . 8  |-  ( ph  ->  ( ( ( P 
.\/  U )  ./\  ( P  .\/  ( ( F `  P ) 
.\/  V ) ) )  ./\  W )  =  ( ( P 
.\/  U )  ./\  ( ( P  .\/  ( ( F `  P )  .\/  V
) )  ./\  W
) ) )
8681, 85eqtrd 2470 . . . . . . 7  |-  ( ph  ->  ( ( P  .\/  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) ) ) 
./\  W )  =  ( ( P  .\/  U )  ./\  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) ) )
8776, 86eqtrd 2470 . . . . . 6  |-  ( ph  ->  ( ( P  .\/  ( G `  P ) )  ./\  W )  =  ( ( P 
.\/  U )  ./\  ( ( P  .\/  ( ( F `  P )  .\/  V
) )  ./\  W
) ) )
8871, 87eqtrd 2470 . . . . 5  |-  ( ph  ->  ( R `  G
)  =  ( ( P  .\/  U ) 
./\  ( ( P 
.\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) ) )
8988eqcomd 2443 . . . 4  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) )  =  ( R `  G ) )
9068, 89breqtrd 4311 . . 3  |-  ( ph  ->  U  .<_  ( R `  G ) )
91 hlatl 32898 . . . . 5  |-  ( K  e.  HL  ->  K  e.  AtLat )
922, 91syl 16 . . . 4  |-  ( ph  ->  K  e.  AtLat )
93 hlop 32900 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  OP )
942, 93syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  OP )
95 eqid 2438 . . . . . . . . . 10  |-  ( 0.
`  K )  =  ( 0. `  K
)
96 eqid 2438 . . . . . . . . . 10  |-  ( lt
`  K )  =  ( lt `  K
)
9795, 96, 80ltat 32829 . . . . . . . . 9  |-  ( ( K  e.  OP  /\  U  e.  A )  ->  ( 0. `  K
) ( lt `  K ) U )
9894, 12, 97syl2anc 661 . . . . . . . 8  |-  ( ph  ->  ( 0. `  K
) ( lt `  K ) U )
99 hlpos 32903 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  Poset )
1002, 99syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  Poset )
1017, 95op0cl 32722 . . . . . . . . . 10  |-  ( K  e.  OP  ->  ( 0. `  K )  e.  ( Base `  K
) )
10294, 101syl 16 . . . . . . . . 9  |-  ( ph  ->  ( 0. `  K
)  e.  ( Base `  K ) )
1037, 27, 28, 29trlcl 33701 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  ( R `  G )  e.  (
Base `  K )
)
1041, 69, 103syl2anc 661 . . . . . . . . 9  |-  ( ph  ->  ( R `  G
)  e.  ( Base `  K ) )
1057, 15, 96pltletr 15133 . . . . . . . . 9  |-  ( ( K  e.  Poset  /\  (
( 0. `  K
)  e.  ( Base `  K )  /\  U  e.  ( Base `  K
)  /\  ( R `  G )  e.  (
Base `  K )
) )  ->  (
( ( 0. `  K ) ( lt
`  K ) U  /\  U  .<_  ( R `
 G ) )  ->  ( 0. `  K ) ( lt
`  K ) ( R `  G ) ) )
106100, 102, 14, 104, 105syl13anc 1220 . . . . . . . 8  |-  ( ph  ->  ( ( ( 0.
`  K ) ( lt `  K ) U  /\  U  .<_  ( R `  G ) )  ->  ( 0. `  K ) ( lt
`  K ) ( R `  G ) ) )
10798, 90, 106mp2and 679 . . . . . . 7  |-  ( ph  ->  ( 0. `  K
) ( lt `  K ) ( R `
 G ) )
1087, 96, 95opltn0 32728 . . . . . . . 8  |-  ( ( K  e.  OP  /\  ( R `  G )  e.  ( Base `  K
) )  ->  (
( 0. `  K
) ( lt `  K ) ( R `
 G )  <->  ( R `  G )  =/=  ( 0. `  K ) ) )
10994, 104, 108syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( 0. `  K ) ( lt
`  K ) ( R `  G )  <-> 
( R `  G
)  =/=  ( 0.
`  K ) ) )
110107, 109mpbid 210 . . . . . 6  |-  ( ph  ->  ( R `  G
)  =/=  ( 0.
`  K ) )
111110neneqd 2619 . . . . 5  |-  ( ph  ->  -.  ( R `  G )  =  ( 0. `  K ) )
11295, 8, 27, 28, 29trlator0 33708 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  ( ( R `  G )  e.  A  \/  ( R `  G )  =  ( 0. `  K ) ) )
1131, 69, 112syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( R `  G )  e.  A  \/  ( R `  G
)  =  ( 0.
`  K ) ) )
114113orcomd 388 . . . . . 6  |-  ( ph  ->  ( ( R `  G )  =  ( 0. `  K )  \/  ( R `  G )  e.  A
) )
115114ord 377 . . . . 5  |-  ( ph  ->  ( -.  ( R `
 G )  =  ( 0. `  K
)  ->  ( R `  G )  e.  A
) )
116111, 115mpd 15 . . . 4  |-  ( ph  ->  ( R `  G
)  e.  A )
11715, 8atcmp 32849 . . . 4  |-  ( ( K  e.  AtLat  /\  U  e.  A  /\  ( R `  G )  e.  A )  ->  ( U  .<_  ( R `  G )  <->  U  =  ( R `  G ) ) )
11892, 12, 116, 117syl3anc 1218 . . 3  |-  ( ph  ->  ( U  .<_  ( R `
 G )  <->  U  =  ( R `  G ) ) )
11990, 118mpbid 210 . 2  |-  ( ph  ->  U  =  ( R `
 G ) )
120119eqcomd 2443 1  |-  ( ph  ->  ( R `  G
)  =  U )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1369    e. wcel 1756    =/= wne 2601   class class class wbr 4287   ` cfv 5413  (class class class)co 6086   Basecbs 14166   lecple 14237   Posetcpo 15102   ltcplt 15103   joincjn 15106   meetcmee 15107   0.cp0 15199   Latclat 15207   OPcops 32710   OLcol 32712   Atomscatm 32801   AtLatcal 32802   HLchlt 32888   LHypclh 33521   LTrncltrn 33638   trLctrl 33695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-iin 4169  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-1st 6572  df-2nd 6573  df-map 7208  df-poset 15108  df-plt 15120  df-lub 15136  df-glb 15137  df-join 15138  df-meet 15139  df-p0 15201  df-p1 15202  df-lat 15208  df-clat 15270  df-oposet 32714  df-ol 32716  df-oml 32717  df-covers 32804  df-ats 32805  df-atl 32836  df-cvlat 32860  df-hlat 32889  df-psubsp 33040  df-pmap 33041  df-padd 33333  df-lhyp 33525  df-laut 33526  df-ldil 33641  df-ltrn 33642  df-trl 33696
This theorem is referenced by:  dia2dimlem5  34606
  Copyright terms: Public domain W3C validator