Theorem trlcl 38378

Description: Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012.)

Hypotheses

Ref	Expression
trlcl.b	⊢ 𝐵 = (Base‘𝐾)
trlcl.h	⊢ 𝐻 = (LHyp‘𝐾)
trlcl.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
trlcl.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

Assertion

Ref	Expression
trlcl	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ∈ 𝐵)

Proof of Theorem trlcl

Step	Hyp	Ref	Expression
1		eqid 2736	. . . . 5 ⊢ (le‘𝐾) = (le‘𝐾)
2		eqid 2736	. . . . 5 ⊢ (oc‘𝐾) = (oc‘𝐾)
3		eqid 2736	. . . . 5 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
4		trlcl.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
5	1, 2, 3, 4	lhpocnel 38232	. . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊))
6	5	adantr 482	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊))
7		eqid 2736	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8		eqid 2736	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
9		trlcl.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
10		trlcl.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
11	1, 7, 8, 3, 4, 9, 10	trlval2 38377	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊)) → (𝑅‘𝐹) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊))
12	6, 11	mpd3an3 1462	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊))
13		hllat 37577	. . . 4 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
14	13	ad2antrr 724	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐾 ∈ Lat)
15		hlop 37576	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
16	15	ad2antrr 724	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐾 ∈ OP)
17		trlcl.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
18	17, 4	lhpbase 38212	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
19	18	ad2antlr 725	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝑊 ∈ 𝐵)
20	17, 2	opoccl 37408	. . . . 5 ⊢ ((𝐾 ∈ OP ∧ 𝑊 ∈ 𝐵) → ((oc‘𝐾)‘𝑊) ∈ 𝐵)
21	16, 19, 20	syl2anc 585	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((oc‘𝐾)‘𝑊) ∈ 𝐵)
22	17, 4, 9	ltrncl 38339	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((oc‘𝐾)‘𝑊) ∈ 𝐵) → (𝐹‘((oc‘𝐾)‘𝑊)) ∈ 𝐵)
23	21, 22	mpd3an3 1462	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐹‘((oc‘𝐾)‘𝑊)) ∈ 𝐵)
24	17, 7	latjcl 18206	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑊) ∈ 𝐵 ∧ (𝐹‘((oc‘𝐾)‘𝑊)) ∈ 𝐵) → (((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊))) ∈ 𝐵)
25	14, 21, 23, 24	syl3anc 1371	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊))) ∈ 𝐵)
26	17, 8	latmcl 18207	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊))) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) ∈ 𝐵)
27	14, 25, 19, 26	syl3anc 1371	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) ∈ 𝐵)
28	12, 27	eqeltrd 2837	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1539   ∈ wcel 2104   class class class wbr 5081  ‘cfv 6458  (class class class)co 7307  Basecbs 16961  lecple 17018  occoc 17019  joincjn 18078  meetcmee 18079  Latclat 18198  OPcops 37386  Atomscatm 37477  HLchlt 37564  LHypclh 38198  LTrncltrn 38315  trLctrl 38372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3305  df-rab 3306  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-map 8648  df-proset 18062  df-poset 18080  df-plt 18097  df-lub 18113  df-glb 18114  df-join 18115  df-meet 18116  df-p0 18192  df-p1 18193  df-lat 18199  df-oposet 37390  df-ol 37392  df-oml 37393  df-covers 37480  df-ats 37481  df-atl 37512  df-cvlat 37536  df-hlat 37565  df-lhyp 38202  df-laut 38203  df-ldil 38318  df-ltrn 38319  df-trl 38373

This theorem is referenced by:  trljat1  38380  trljat2  38381  trlval3  38401  cdlemc3  38407  cdlemc5  38409  trlord  38783  cdlemg4c  38826  cdlemg4  38831  cdlemg6c  38834  cdlemg10c  38853  cdlemg10  38855  cdlemg12e  38861  cdlemg17dALTN  38878  cdlemg31a  38911  cdlemg31b  38912  cdlemg35  38927  cdlemg44a  38945  trljco  38954  trljco2  38955  tendoidcl  38983  tendococl  38986  tendoid  38987  tendopltp  38994  tendo0tp  39003  cdlemh1  39029  cdlemh2  39030  cdlemi1  39032  cdlemi  39034  cdlemk9  39053  cdlemk9bN  39054  cdlemkvcl  39056  cdlemk10  39057  cdlemk11  39063  cdlemk11u  39085  cdlemk37  39128  cdlemkfid1N  39135  cdlemkid1  39136  cdlemkid2  39138  cdlemk39s-id  39154  cdlemk48  39164  cdlemk50  39166  cdlemk51  39167  cdlemk52  39168  cdlemk39u  39182  tendoex  39189  dialss  39260  dia0  39266  diaglbN  39269  dia1dim  39275  dia2dimlem2  39279  dia2dimlem3  39280  dia2dimlem10  39287  cdlemm10N  39332  dib1dim  39379  diblss  39384  cdlemn2a  39410  dih1dimb  39454  dihopelvalcpre  39462  dih1  39500  dihmeetlem1N  39504  dihglblem5apreN  39505  dihglbcpreN  39514  dih1dimatlem  39543