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

Theorem trlcl 35764
Description: Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012.)
Hypotheses
Ref Expression
trlcl.b  |-  B  =  ( Base `  K
)
trlcl.h  |-  H  =  ( LHyp `  K
)
trlcl.t  |-  T  =  ( ( LTrn `  K
) `  W )
trlcl.r  |-  R  =  ( ( trL `  K
) `  W )
Assertion
Ref Expression
trlcl  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  e.  B
)

Proof of Theorem trlcl
StepHypRef Expression
1 eqid 2443 . . . . 5  |-  ( le
`  K )  =  ( le `  K
)
2 eqid 2443 . . . . 5  |-  ( oc
`  K )  =  ( oc `  K
)
3 eqid 2443 . . . . 5  |-  ( Atoms `  K )  =  (
Atoms `  K )
4 trlcl.h . . . . 5  |-  H  =  ( LHyp `  K
)
51, 2, 3, 4lhpocnel 35617 . . . 4  |-  ( ( K  e.  HL  /\  W  e.  H )  ->  ( ( ( oc
`  K ) `  W )  e.  (
Atoms `  K )  /\  -.  ( ( oc `  K ) `  W
) ( le `  K ) W ) )
65adantr 465 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( (
( oc `  K
) `  W )  e.  ( Atoms `  K )  /\  -.  ( ( oc
`  K ) `  W ) ( le
`  K ) W ) )
7 eqid 2443 . . . 4  |-  ( join `  K )  =  (
join `  K )
8 eqid 2443 . . . 4  |-  ( meet `  K )  =  (
meet `  K )
9 trlcl.t . . . 4  |-  T  =  ( ( LTrn `  K
) `  W )
10 trlcl.r . . . 4  |-  R  =  ( ( trL `  K
) `  W )
111, 7, 8, 3, 4, 9, 10trlval2 35763 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( ( oc
`  K ) `  W )  e.  (
Atoms `  K )  /\  -.  ( ( oc `  K ) `  W
) ( le `  K ) W ) )  ->  ( R `  F )  =  ( ( ( ( oc
`  K ) `  W ) ( join `  K ) ( F `
 ( ( oc
`  K ) `  W ) ) ) ( meet `  K
) W ) )
126, 11mpd3an3 1326 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  =  ( ( ( ( oc
`  K ) `  W ) ( join `  K ) ( F `
 ( ( oc
`  K ) `  W ) ) ) ( meet `  K
) W ) )
13 hllat 34963 . . . 4  |-  ( K  e.  HL  ->  K  e.  Lat )
1413ad2antrr 725 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  K  e.  Lat )
15 hlop 34962 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  OP )
1615ad2antrr 725 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  K  e.  OP )
17 trlcl.b . . . . . . 7  |-  B  =  ( Base `  K
)
1817, 4lhpbase 35597 . . . . . 6  |-  ( W  e.  H  ->  W  e.  B )
1918ad2antlr 726 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  W  e.  B )
2017, 2opoccl 34794 . . . . 5  |-  ( ( K  e.  OP  /\  W  e.  B )  ->  ( ( oc `  K ) `  W
)  e.  B )
2116, 19, 20syl2anc 661 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( ( oc `  K ) `  W )  e.  B
)
2217, 4, 9ltrncl 35724 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( oc `  K ) `  W
)  e.  B )  ->  ( F `  ( ( oc `  K ) `  W
) )  e.  B
)
2321, 22mpd3an3 1326 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( F `  ( ( oc `  K ) `  W
) )  e.  B
)
2417, 7latjcl 15660 . . . 4  |-  ( ( K  e.  Lat  /\  ( ( oc `  K ) `  W
)  e.  B  /\  ( F `  ( ( oc `  K ) `
 W ) )  e.  B )  -> 
( ( ( oc
`  K ) `  W ) ( join `  K ) ( F `
 ( ( oc
`  K ) `  W ) ) )  e.  B )
2514, 21, 23, 24syl3anc 1229 . . 3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( (
( oc `  K
) `  W )
( join `  K )
( F `  (
( oc `  K
) `  W )
) )  e.  B
)
2617, 8latmcl 15661 . . 3  |-  ( ( K  e.  Lat  /\  ( ( ( oc
`  K ) `  W ) ( join `  K ) ( F `
 ( ( oc
`  K ) `  W ) ) )  e.  B  /\  W  e.  B )  ->  (
( ( ( oc
`  K ) `  W ) ( join `  K ) ( F `
 ( ( oc
`  K ) `  W ) ) ) ( meet `  K
) W )  e.  B )
2714, 25, 19, 26syl3anc 1229 . 2  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( (
( ( oc `  K ) `  W
) ( join `  K
) ( F `  ( ( oc `  K ) `  W
) ) ) (
meet `  K ) W )  e.  B
)
2812, 27eqeltrd 2531 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  e.  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1383    e. wcel 1804   class class class wbr 4437   ` cfv 5578  (class class class)co 6281   Basecbs 14614   lecple 14686   occoc 14687   joincjn 15552   meetcmee 15553   Latclat 15654   OPcops 34772   Atomscatm 34863   HLchlt 34950   LHypclh 35583   LTrncltrn 35700   trLctrl 35758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-map 7424  df-preset 15536  df-poset 15554  df-plt 15567  df-lub 15583  df-glb 15584  df-join 15585  df-meet 15586  df-p0 15648  df-p1 15649  df-lat 15655  df-oposet 34776  df-ol 34778  df-oml 34779  df-covers 34866  df-ats 34867  df-atl 34898  df-cvlat 34922  df-hlat 34951  df-lhyp 35587  df-laut 35588  df-ldil 35703  df-ltrn 35704  df-trl 35759
This theorem is referenced by:  trljat1  35766  trljat2  35767  trlval3  35787  cdlemc3  35793  cdlemc5  35795  trlord  36170  cdlemg4c  36213  cdlemg4  36218  cdlemg6c  36221  cdlemg10c  36240  cdlemg10  36242  cdlemg12e  36248  cdlemg17dALTN  36265  cdlemg31a  36298  cdlemg31b  36299  cdlemg35  36314  cdlemg44a  36332  trljco  36341  trljco2  36342  tendoidcl  36370  tendococl  36373  tendoid  36374  tendopltp  36381  tendo0tp  36390  cdlemh1  36416  cdlemh2  36417  cdlemi1  36419  cdlemi  36421  cdlemk9  36440  cdlemk9bN  36441  cdlemkvcl  36443  cdlemk10  36444  cdlemk11  36450  cdlemk11u  36472  cdlemk37  36515  cdlemkfid1N  36522  cdlemkid1  36523  cdlemkid2  36525  cdlemk39s-id  36541  cdlemk48  36551  cdlemk50  36553  cdlemk51  36554  cdlemk52  36555  cdlemk39u  36569  tendoex  36576  dialss  36648  dia0  36654  diaglbN  36657  dia1dim  36663  dia2dimlem2  36667  dia2dimlem3  36668  dia2dimlem10  36675  cdlemm10N  36720  dib1dim  36767  diblss  36772  cdlemn2a  36798  dih1dimb  36842  dihopelvalcpre  36850  dih1  36888  dihmeetlem1N  36892  dihglblem5apreN  36893  dihglbcpreN  36902  dih1dimatlem  36931
  Copyright terms: Public domain W3C validator