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

Theorem trlval2 30352
Description: The value of the trace of a lattice translation, given any atom  P not under the fiducial co-atom  W. Note: this requires only the weaker assumption  K  e.  Lat; we use  K  e.  HL for convenience. (Contributed by NM, 20-May-2012.)
Hypotheses
Ref Expression
trlval2.l  |-  .<_  =  ( le `  K )
trlval2.j  |-  .\/  =  ( join `  K )
trlval2.m  |-  ./\  =  ( meet `  K )
trlval2.a  |-  A  =  ( Atoms `  K )
trlval2.h  |-  H  =  ( LHyp `  K
)
trlval2.t  |-  T  =  ( ( LTrn `  K
) `  W )
trlval2.r  |-  R  =  ( ( trL `  K
) `  W )
Assertion
Ref Expression
trlval2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  W )
)

Proof of Theorem trlval2
Dummy variables  x  q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hllat 29553 . . 3  |-  ( K  e.  HL  ->  K  e.  Lat )
21anim1i 551 . 2  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( K  e.  Lat  /\  W  e.  H ) )
3 eqid 2283 . . . . 5  |-  ( Base `  K )  =  (
Base `  K )
4 trlval2.l . . . . 5  |-  .<_  =  ( le `  K )
5 trlval2.j . . . . 5  |-  .\/  =  ( join `  K )
6 trlval2.m . . . . 5  |-  ./\  =  ( meet `  K )
7 trlval2.a . . . . 5  |-  A  =  ( Atoms `  K )
8 trlval2.h . . . . 5  |-  H  =  ( LHyp `  K
)
9 trlval2.t . . . . 5  |-  T  =  ( ( LTrn `  K
) `  W )
10 trlval2.r . . . . 5  |-  R  =  ( ( trL `  K
) `  W )
113, 4, 5, 6, 7, 8, 9, 10trlval 30351 . . . 4  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  =  (
iota_ x  e.  ( Base `  K ) A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( (
q  .\/  ( F `  q ) )  ./\  W ) ) ) )
12113adant3 975 . . 3  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  F )  =  (
iota_ x  e.  ( Base `  K ) A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( (
q  .\/  ( F `  q ) )  ./\  W ) ) ) )
13 simp1l 979 . . . . 5  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  K  e.  Lat )
14 simp3l 983 . . . . . . 7  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  P  e.  A )
153, 7atbase 29479 . . . . . . 7  |-  ( P  e.  A  ->  P  e.  ( Base `  K
) )
1614, 15syl 15 . . . . . 6  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  P  e.  ( Base `  K )
)
173, 8, 9ltrncl 30314 . . . . . . 7  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  P  e.  ( Base `  K ) )  ->  ( F `  P )  e.  (
Base `  K )
)
1816, 17syld3an3 1227 . . . . . 6  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( F `  P )  e.  (
Base `  K )
)
193, 5latjcl 14156 . . . . . 6  |-  ( ( K  e.  Lat  /\  P  e.  ( Base `  K )  /\  ( F `  P )  e.  ( Base `  K
) )  ->  ( P  .\/  ( F `  P ) )  e.  ( Base `  K
) )
2013, 16, 18, 19syl3anc 1182 . . . . 5  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( P  .\/  ( F `  P
) )  e.  (
Base `  K )
)
21 simp1r 980 . . . . . 6  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  W  e.  H )
223, 8lhpbase 30187 . . . . . 6  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
2321, 22syl 15 . . . . 5  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  W  e.  ( Base `  K )
)
243, 6latmcl 14157 . . . . 5  |-  ( ( K  e.  Lat  /\  ( P  .\/  ( F `
 P ) )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( P  .\/  ( F `  P ) )  ./\  W )  e.  ( Base `  K ) )
2513, 20, 23, 24syl3anc 1182 . . . 4  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( ( P  .\/  ( F `  P ) )  ./\  W )  e.  ( Base `  K ) )
26 simp13l 1070 . . . . . . 7  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( P  .\/  ( F `
 P ) ) 
./\  W )  e.  ( Base `  K
)  /\  x  e.  ( Base `  K )
)  ->  P  e.  A )
27 simp13r 1071 . . . . . . 7  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( P  .\/  ( F `
 P ) ) 
./\  W )  e.  ( Base `  K
)  /\  x  e.  ( Base `  K )
)  ->  -.  P  .<_  W )
28 breq1 4026 . . . . . . . . . . 11  |-  ( q  =  P  ->  (
q  .<_  W  <->  P  .<_  W ) )
2928notbid 285 . . . . . . . . . 10  |-  ( q  =  P  ->  ( -.  q  .<_  W  <->  -.  P  .<_  W ) )
30 id 19 . . . . . . . . . . . . 13  |-  ( q  =  P  ->  q  =  P )
31 fveq2 5525 . . . . . . . . . . . . 13  |-  ( q  =  P  ->  ( F `  q )  =  ( F `  P ) )
3230, 31oveq12d 5876 . . . . . . . . . . . 12  |-  ( q  =  P  ->  (
q  .\/  ( F `  q ) )  =  ( P  .\/  ( F `  P )
) )
3332oveq1d 5873 . . . . . . . . . . 11  |-  ( q  =  P  ->  (
( q  .\/  ( F `  q )
)  ./\  W )  =  ( ( P 
.\/  ( F `  P ) )  ./\  W ) )
3433eqeq2d 2294 . . . . . . . . . 10  |-  ( q  =  P  ->  (
x  =  ( ( q  .\/  ( F `
 q ) ) 
./\  W )  <->  x  =  ( ( P  .\/  ( F `  P ) )  ./\  W )
) )
3529, 34imbi12d 311 . . . . . . . . 9  |-  ( q  =  P  ->  (
( -.  q  .<_  W  ->  x  =  ( ( q  .\/  ( F `  q )
)  ./\  W )
)  <->  ( -.  P  .<_  W  ->  x  =  ( ( P  .\/  ( F `  P ) )  ./\  W )
) ) )
3635rspcv 2880 . . . . . . . 8  |-  ( P  e.  A  ->  ( A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( ( q  .\/  ( F `  q )
)  ./\  W )
)  ->  ( -.  P  .<_  W  ->  x  =  ( ( P 
.\/  ( F `  P ) )  ./\  W ) ) ) )
3736com23 72 . . . . . . 7  |-  ( P  e.  A  ->  ( -.  P  .<_  W  -> 
( A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( ( q  .\/  ( F `  q ) )  ./\  W )
)  ->  x  =  ( ( P  .\/  ( F `  P ) )  ./\  W )
) ) )
3826, 27, 37sylc 56 . . . . . 6  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( P  .\/  ( F `
 P ) ) 
./\  W )  e.  ( Base `  K
)  /\  x  e.  ( Base `  K )
)  ->  ( A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( (
q  .\/  ( F `  q ) )  ./\  W ) )  ->  x  =  ( ( P 
.\/  ( F `  P ) )  ./\  W ) ) )
39 simp11 985 . . . . . . . . . . . 12  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  -.  q  .<_  W  /\  q  e.  A )  ->  ( K  e.  Lat  /\  W  e.  H ) )
40 simp12 986 . . . . . . . . . . . 12  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  -.  q  .<_  W  /\  q  e.  A )  ->  F  e.  T )
41 simp13l 1070 . . . . . . . . . . . 12  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  -.  q  .<_  W  /\  q  e.  A )  ->  P  e.  A )
42 simp13r 1071 . . . . . . . . . . . 12  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  -.  q  .<_  W  /\  q  e.  A )  ->  -.  P  .<_  W )
43 simp3 957 . . . . . . . . . . . 12  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  -.  q  .<_  W  /\  q  e.  A )  ->  q  e.  A )
44 simp2 956 . . . . . . . . . . . 12  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  -.  q  .<_  W  /\  q  e.  A )  ->  -.  q  .<_  W )
454, 5, 6, 7, 8, 9ltrnu 30310 . . . . . . . . . . . 12  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( q  e.  A  /\  -.  q  .<_  W ) )  -> 
( ( P  .\/  ( F `  P ) )  ./\  W )  =  ( ( q 
.\/  ( F `  q ) )  ./\  W ) )
4639, 40, 41, 42, 43, 44, 45syl222anc 1198 . . . . . . . . . . 11  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  -.  q  .<_  W  /\  q  e.  A )  ->  (
( P  .\/  ( F `  P )
)  ./\  W )  =  ( ( q 
.\/  ( F `  q ) )  ./\  W ) )
47 eqeq2 2292 . . . . . . . . . . . 12  |-  ( ( ( P  .\/  ( F `  P )
)  ./\  W )  =  ( ( q 
.\/  ( F `  q ) )  ./\  W )  ->  ( x  =  ( ( P 
.\/  ( F `  P ) )  ./\  W )  <->  x  =  (
( q  .\/  ( F `  q )
)  ./\  W )
) )
4847biimpd 198 . . . . . . . . . . 11  |-  ( ( ( P  .\/  ( F `  P )
)  ./\  W )  =  ( ( q 
.\/  ( F `  q ) )  ./\  W )  ->  ( x  =  ( ( P 
.\/  ( F `  P ) )  ./\  W )  ->  x  =  ( ( q  .\/  ( F `  q ) )  ./\  W )
) )
4946, 48syl 15 . . . . . . . . . 10  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  -.  q  .<_  W  /\  q  e.  A )  ->  (
x  =  ( ( P  .\/  ( F `
 P ) ) 
./\  W )  ->  x  =  ( (
q  .\/  ( F `  q ) )  ./\  W ) ) )
50493exp 1150 . . . . . . . . 9  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( -.  q  .<_  W  ->  (
q  e.  A  -> 
( x  =  ( ( P  .\/  ( F `  P )
)  ./\  W )  ->  x  =  ( ( q  .\/  ( F `
 q ) ) 
./\  W ) ) ) ) )
5150com24 81 . . . . . . . 8  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( x  =  ( ( P 
.\/  ( F `  P ) )  ./\  W )  ->  ( q  e.  A  ->  ( -.  q  .<_  W  ->  x  =  ( ( q 
.\/  ( F `  q ) )  ./\  W ) ) ) ) )
5251ralrimdv 2632 . . . . . . 7  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( x  =  ( ( P 
.\/  ( F `  P ) )  ./\  W )  ->  A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( ( q 
.\/  ( F `  q ) )  ./\  W ) ) ) )
53523ad2ant1 976 . . . . . 6  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( P  .\/  ( F `
 P ) ) 
./\  W )  e.  ( Base `  K
)  /\  x  e.  ( Base `  K )
)  ->  ( x  =  ( ( P 
.\/  ( F `  P ) )  ./\  W )  ->  A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( ( q 
.\/  ( F `  q ) )  ./\  W ) ) ) )
5438, 53impbid 183 . . . . 5  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( P  .\/  ( F `
 P ) ) 
./\  W )  e.  ( Base `  K
)  /\  x  e.  ( Base `  K )
)  ->  ( A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( (
q  .\/  ( F `  q ) )  ./\  W ) )  <->  x  =  ( ( P  .\/  ( F `  P ) )  ./\  W )
) )
5554riota5OLD 6331 . . . 4  |-  ( ( ( ( K  e. 
Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  /\  ( ( P  .\/  ( F `
 P ) ) 
./\  W )  e.  ( Base `  K
) )  ->  ( iota_ x  e.  ( Base `  K ) A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( ( q 
.\/  ( F `  q ) )  ./\  W ) ) )  =  ( ( P  .\/  ( F `  P ) )  ./\  W )
)
5625, 55mpdan 649 . . 3  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( iota_ x  e.  ( Base `  K
) A. q  e.  A  ( -.  q  .<_  W  ->  x  =  ( ( q  .\/  ( F `  q ) )  ./\  W )
) )  =  ( ( P  .\/  ( F `  P )
)  ./\  W )
)
5712, 56eqtrd 2315 . 2  |-  ( ( ( K  e.  Lat  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  W )
)
582, 57syl3an1 1215 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  W )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543   class class class wbr 4023   ` cfv 5255  (class class class)co 5858   iota_crio 6297   Basecbs 13148   lecple 13215   joincjn 14078   meetcmee 14079   Latclat 14151   Atomscatm 29453   HLchlt 29540   LHypclh 30173   LTrncltrn 30290   trLctrl 30347
This theorem is referenced by:  trlcl  30353  trlcnv  30354  trljat1  30355  trljat2  30356  trlat  30358  trl0  30359  trlle  30373  trlval3  30376  trlval5  30378  cdlemd6  30392  cdlemf  30752  cdlemg4a  30797  cdlemg4b1  30798  cdlemg4b2  30799  cdlemg4  30806  cdlemg11b  30831  cdlemg13a  30840  cdlemg13  30841  cdlemg17a  30850  cdlemg17dN  30852  cdlemg17e  30854  cdlemg17f  30855  trlcoabs2N  30911  trlcolem  30915  cdlemg42  30918  cdlemg43  30919  cdlemi1  31007  cdlemk4  31023  cdlemk39  31105  dia2dimlem1  31254  dia2dimlem2  31255  dia2dimlem3  31256  cdlemm10N  31308  cdlemn2  31385  cdlemn10  31396  dihjatcclem3  31610
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 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
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 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-riota 6304  df-map 6774  df-lat 14152  df-ats 29457  df-atl 29488  df-cvlat 29512  df-hlat 29541  df-lhyp 30177  df-laut 30178  df-ldil 30293  df-ltrn 30294  df-trl 30348
  Copyright terms: Public domain W3C validator