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

Theorem dia2dimlem2 31702
Description: Lemma for dia2dim 31714. 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 446 . . . . . . . 8  |-  ( ph  ->  K  e.  HL )
3 hllat 30000 . . . . . . . 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 446 . . . . . . . 8  |-  ( ph  ->  P  e.  A )
7 eqid 2435 . . . . . . . . 9  |-  ( Base `  K )  =  (
Base `  K )
8 dia2dimlem2.a . . . . . . . . 9  |-  A  =  ( Atoms `  K )
97, 8atbase 29926 . . . . . . . 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 446 . . . . . . . 8  |-  ( ph  ->  U  e.  A )
137, 8atbase 29926 . . . . . . . 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 14478 . . . . . . 7  |-  ( ( K  e.  Lat  /\  P  e.  ( Base `  K )  /\  U  e.  ( Base `  K
) )  ->  U  .<_  ( P  .\/  U
) )
184, 10, 14, 17syl3anc 1184 . . . . . 6  |-  ( ph  ->  U  .<_  ( P  .\/  U ) )
197, 16, 8hlatjcl 30003 . . . . . . . 8  |-  ( ( K  e.  HL  /\  P  e.  A  /\  U  e.  A )  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
202, 6, 12, 19syl3anc 1184 . . . . . . 7  |-  ( ph  ->  ( P  .\/  U
)  e.  ( Base `  K ) )
21 dia2dimlem2.m . . . . . . . 8  |-  ./\  =  ( meet `  K )
227, 15, 21latleeqm2 14497 . . . . . . 7  |-  ( ( K  e.  Lat  /\  U  e.  ( Base `  K )  /\  ( P  .\/  U )  e.  ( Base `  K
) )  ->  ( U  .<_  ( P  .\/  U )  <->  ( ( P 
.\/  U )  ./\  U )  =  U ) )
234, 14, 20, 22syl3anc 1184 . . . . . 6  |-  ( ph  ->  ( U  .<_  ( P 
.\/  U )  <->  ( ( P  .\/  U )  ./\  U )  =  U ) )
2418, 23mpbid 202 . . . . 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 30805 . . . . . . . . . 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 1184 . . . . . . . . 9  |-  ( ph  ->  ( R `  F
)  e.  A )
32 dia2dimlem2.v . . . . . . . . . 10  |-  ( ph  ->  ( V  e.  A  /\  V  .<_  W ) )
3332simpld 446 . . . . . . . . 9  |-  ( ph  ->  V  e.  A )
34 dia2dimlem2.rv . . . . . . . . 9  |-  ( ph  ->  ( R `  F
)  =/=  V )
3515, 16, 8hlatexch2 30032 . . . . . . . . 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 1197 . . . . . . . 8  |-  ( ph  ->  ( ( R `  F )  .<_  ( U 
.\/  V )  ->  U  .<_  ( ( R `
 F )  .\/  V ) ) )
3725, 36mpd 15 . . . . . . 7  |-  ( ph  ->  U  .<_  ( ( R `  F )  .\/  V ) )
3826simpld 446 . . . . . . . . . 10  |-  ( ph  ->  F  e.  T )
3915, 16, 21, 8, 27, 28, 29trlval2 30799 . . . . . . . . . 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 1184 . . . . . . . . 9  |-  ( ph  ->  ( R `  F
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  W ) )
4140oveq1d 6087 . . . . . . . 8  |-  ( ph  ->  ( ( R `  F )  .\/  V
)  =  ( ( ( P  .\/  ( F `  P )
)  ./\  W )  .\/  V ) )
4215, 8, 27, 28ltrnel 30775 . . . . . . . . . . . . 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 1184 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( F `  P )  e.  A  /\  -.  ( F `  P )  .<_  W ) )
4443simpld 446 . . . . . . . . . . 11  |-  ( ph  ->  ( F `  P
)  e.  A )
457, 16, 8hlatjcl 30003 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  -> 
( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
462, 6, 44, 45syl3anc 1184 . . . . . . . . . 10  |-  ( ph  ->  ( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
471simprd 450 . . . . . . . . . . 11  |-  ( ph  ->  W  e.  H )
487, 27lhpbase 30634 . . . . . . . . . . 11  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
4947, 48syl 16 . . . . . . . . . 10  |-  ( ph  ->  W  e.  ( Base `  K ) )
5032simprd 450 . . . . . . . . . 10  |-  ( ph  ->  V  .<_  W )
517, 15, 16, 21, 8atmod4i1 30502 . . . . . . . . . 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 1197 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P 
.\/  ( F `  P ) )  ./\  W )  .\/  V )  =  ( ( ( P  .\/  ( F `
 P ) ) 
.\/  V )  ./\  W ) )
5316, 8hlatjass 30006 . . . . . . . . . . 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 1186 . . . . . . . . . 10  |-  ( ph  ->  ( ( P  .\/  ( F `  P ) )  .\/  V )  =  ( P  .\/  ( ( F `  P )  .\/  V
) ) )
5554oveq1d 6087 . . . . . . . . 9  |-  ( ph  ->  ( ( ( P 
.\/  ( F `  P ) )  .\/  V )  ./\  W )  =  ( ( P 
.\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) )
5652, 55eqtrd 2467 . . . . . . . 8  |-  ( ph  ->  ( ( ( P 
.\/  ( F `  P ) )  ./\  W )  .\/  V )  =  ( ( P 
.\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) )
5741, 56eqtrd 2467 . . . . . . 7  |-  ( ph  ->  ( ( R `  F )  .\/  V
)  =  ( ( P  .\/  ( ( F `  P ) 
.\/  V ) ) 
./\  W ) )
5837, 57breqtrd 4228 . . . . . 6  |-  ( ph  ->  U  .<_  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) )
597, 16, 8hlatjcl 30003 . . . . . . . . . 10  |-  ( ( K  e.  HL  /\  ( F `  P )  e.  A  /\  V  e.  A )  ->  (
( F `  P
)  .\/  V )  e.  ( Base `  K
) )
602, 44, 33, 59syl3anc 1184 . . . . . . . . 9  |-  ( ph  ->  ( ( F `  P )  .\/  V
)  e.  ( Base `  K ) )
617, 16latjcl 14467 . . . . . . . . 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 1184 . . . . . . . 8  |-  ( ph  ->  ( P  .\/  (
( F `  P
)  .\/  V )
)  e.  ( Base `  K ) )
637, 21latmcl 14468 . . . . . . . 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 1184 . . . . . . 7  |-  ( ph  ->  ( ( P  .\/  ( ( F `  P )  .\/  V
) )  ./\  W
)  e.  ( Base `  K ) )
657, 15, 21latmlem2 14499 . . . . . . 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 1186 . . . . . 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 4226 . . . 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 30799 . . . . . . 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 1184 . . . . . 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 2483 . . . . . . . . 9  |-  ( ph  ->  ( G `  P
)  =  ( ( P  .\/  U ) 
./\  ( ( F `
 P )  .\/  V ) ) )
7574oveq2d 6088 . . . . . . . 8  |-  ( ph  ->  ( P  .\/  ( G `  P )
)  =  ( P 
.\/  ( ( P 
.\/  U )  ./\  ( ( F `  P )  .\/  V
) ) ) )
7675oveq1d 6087 . . . . . . 7  |-  ( ph  ->  ( ( P  .\/  ( G `  P ) )  ./\  W )  =  ( ( P 
.\/  ( ( P 
.\/  U )  ./\  ( ( F `  P )  .\/  V
) ) )  ./\  W ) )
7715, 16, 8hlatlej1 30011 . . . . . . . . . . 11  |-  ( ( K  e.  HL  /\  P  e.  A  /\  U  e.  A )  ->  P  .<_  ( P  .\/  U ) )
782, 6, 12, 77syl3anc 1184 . . . . . . . . . 10  |-  ( ph  ->  P  .<_  ( P  .\/  U ) )
797, 15, 16, 21, 8atmod3i1 30500 . . . . . . . . . 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 1197 . . . . . . . . 9  |-  ( ph  ->  ( P  .\/  (
( P  .\/  U
)  ./\  ( ( F `  P )  .\/  V ) ) )  =  ( ( P 
.\/  U )  ./\  ( P  .\/  ( ( F `  P ) 
.\/  V ) ) ) )
8180oveq1d 6087 . . . . . . . 8  |-  ( ph  ->  ( ( P  .\/  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) ) ) 
./\  W )  =  ( ( ( P 
.\/  U )  ./\  ( P  .\/  ( ( F `  P ) 
.\/  V ) ) )  ./\  W )
)
82 hlol 29998 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  OL )
832, 82syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  OL )
847, 21latmassOLD 29866 . . . . . . . . 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 1186 . . . . . . . 8  |-  ( ph  ->  ( ( ( P 
.\/  U )  ./\  ( P  .\/  ( ( F `  P ) 
.\/  V ) ) )  ./\  W )  =  ( ( P 
.\/  U )  ./\  ( ( P  .\/  ( ( F `  P )  .\/  V
) )  ./\  W
) ) )
8681, 85eqtrd 2467 . . . . . . 7  |-  ( ph  ->  ( ( P  .\/  ( ( P  .\/  U )  ./\  ( ( F `  P )  .\/  V ) ) ) 
./\  W )  =  ( ( P  .\/  U )  ./\  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) ) )
8776, 86eqtrd 2467 . . . . . 6  |-  ( ph  ->  ( ( P  .\/  ( G `  P ) )  ./\  W )  =  ( ( P 
.\/  U )  ./\  ( ( P  .\/  ( ( F `  P )  .\/  V
) )  ./\  W
) ) )
8871, 87eqtrd 2467 . . . . 5  |-  ( ph  ->  ( R `  G
)  =  ( ( P  .\/  U ) 
./\  ( ( P 
.\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) ) )
8988eqcomd 2440 . . . 4  |-  ( ph  ->  ( ( P  .\/  U )  ./\  ( ( P  .\/  ( ( F `
 P )  .\/  V ) )  ./\  W
) )  =  ( R `  G ) )
9068, 89breqtrd 4228 . . 3  |-  ( ph  ->  U  .<_  ( R `  G ) )
91 hlatl 29997 . . . . 5  |-  ( K  e.  HL  ->  K  e.  AtLat )
922, 91syl 16 . . . 4  |-  ( ph  ->  K  e.  AtLat )
93 hlop 29999 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  OP )
942, 93syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  OP )
95 eqid 2435 . . . . . . . . . 10  |-  ( 0.
`  K )  =  ( 0. `  K
)
96 eqid 2435 . . . . . . . . . 10  |-  ( lt
`  K )  =  ( lt `  K
)
9795, 96, 80ltat 29928 . . . . . . . . 9  |-  ( ( K  e.  OP  /\  U  e.  A )  ->  ( 0. `  K
) ( lt `  K ) U )
9894, 12, 97syl2anc 643 . . . . . . . 8  |-  ( ph  ->  ( 0. `  K
) ( lt `  K ) U )
99 hlpos 30002 . . . . . . . . . 10  |-  ( K  e.  HL  ->  K  e.  Poset )
1002, 99syl 16 . . . . . . . . 9  |-  ( ph  ->  K  e.  Poset )
1017, 95op0cl 29821 . . . . . . . . . 10  |-  ( K  e.  OP  ->  ( 0. `  K )  e.  ( Base `  K
) )
10294, 101syl 16 . . . . . . . . 9  |-  ( ph  ->  ( 0. `  K
)  e.  ( Base `  K ) )
1037, 27, 28, 29trlcl 30800 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  ( R `  G )  e.  (
Base `  K )
)
1041, 69, 103syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( R `  G
)  e.  ( Base `  K ) )
1057, 15, 96pltletr 14416 . . . . . . . . 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 1186 . . . . . . . 8  |-  ( ph  ->  ( ( ( 0.
`  K ) ( lt `  K ) U  /\  U  .<_  ( R `  G ) )  ->  ( 0. `  K ) ( lt
`  K ) ( R `  G ) ) )
10798, 90, 106mp2and 661 . . . . . . 7  |-  ( ph  ->  ( 0. `  K
) ( lt `  K ) ( R `
 G ) )
1087, 96, 95opltn0 29827 . . . . . . . 8  |-  ( ( K  e.  OP  /\  ( R `  G )  e.  ( Base `  K
) )  ->  (
( 0. `  K
) ( lt `  K ) ( R `
 G )  <->  ( R `  G )  =/=  ( 0. `  K ) ) )
10994, 104, 108syl2anc 643 . . . . . . 7  |-  ( ph  ->  ( ( 0. `  K ) ( lt
`  K ) ( R `  G )  <-> 
( R `  G
)  =/=  ( 0.
`  K ) ) )
110107, 109mpbid 202 . . . . . 6  |-  ( ph  ->  ( R `  G
)  =/=  ( 0.
`  K ) )
111110neneqd 2614 . . . . 5  |-  ( ph  ->  -.  ( R `  G )  =  ( 0. `  K ) )
11295, 8, 27, 28, 29trlator0 30807 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  G  e.  T
)  ->  ( ( R `  G )  e.  A  \/  ( R `  G )  =  ( 0. `  K ) ) )
1131, 69, 112syl2anc 643 . . . . . . 7  |-  ( ph  ->  ( ( R `  G )  e.  A  \/  ( R `  G
)  =  ( 0.
`  K ) ) )
114113orcomd 378 . . . . . 6  |-  ( ph  ->  ( ( R `  G )  =  ( 0. `  K )  \/  ( R `  G )  e.  A
) )
115114ord 367 . . . . 5  |-  ( ph  ->  ( -.  ( R `
 G )  =  ( 0. `  K
)  ->  ( R `  G )  e.  A
) )
116111, 115mpd 15 . . . 4  |-  ( ph  ->  ( R `  G
)  e.  A )
11715, 8atcmp 29948 . . . 4  |-  ( ( K  e.  AtLat  /\  U  e.  A  /\  ( R `  G )  e.  A )  ->  ( U  .<_  ( R `  G )  <->  U  =  ( R `  G ) ) )
11892, 12, 116, 117syl3anc 1184 . . 3  |-  ( ph  ->  ( U  .<_  ( R `
 G )  <->  U  =  ( R `  G ) ) )
11990, 118mpbid 202 . 2  |-  ( ph  ->  U  =  ( R `
 G ) )
120119eqcomd 2440 1  |-  ( ph  ->  ( R `  G
)  =  U )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1652    e. wcel 1725    =/= wne 2598   class class class wbr 4204   ` cfv 5445  (class class class)co 6072   Basecbs 13457   lecple 13524   Posetcpo 14385   ltcplt 14386   joincjn 14389   meetcmee 14390   0.cp0 14454   Latclat 14462   OPcops 29809   OLcol 29811   Atomscatm 29900   AtLatcal 29901   HLchlt 29987   LHypclh 30620   LTrncltrn 30737   trLctrl 30794
This theorem is referenced by:  dia2dimlem5  31705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-iun 4087  df-iin 4088  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-1st 6340  df-2nd 6341  df-undef 6534  df-riota 6540  df-map 7011  df-poset 14391  df-plt 14403  df-lub 14419  df-glb 14420  df-join 14421  df-meet 14422  df-p0 14456  df-p1 14457  df-lat 14463  df-clat 14525  df-oposet 29813  df-ol 29815  df-oml 29816  df-covers 29903  df-ats 29904  df-atl 29935  df-cvlat 29959  df-hlat 29988  df-psubsp 30139  df-pmap 30140  df-padd 30432  df-lhyp 30624  df-laut 30625  df-ldil 30740  df-ltrn 30741  df-trl 30795
  Copyright terms: Public domain W3C validator