![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > trlcl | Structured version Visualization version GIF version |
Description: Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012.) |
Ref | Expression |
---|---|
trlcl.b | ⊢ 𝐵 = (Base‘𝐾) |
trlcl.h | ⊢ 𝐻 = (LHyp‘𝐾) |
trlcl.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
trlcl.r | ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
trlcl | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2795 | . . . . 5 ⊢ (le‘𝐾) = (le‘𝐾) | |
2 | eqid 2795 | . . . . 5 ⊢ (oc‘𝐾) = (oc‘𝐾) | |
3 | eqid 2795 | . . . . 5 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾) | |
4 | trlcl.h | . . . . 5 ⊢ 𝐻 = (LHyp‘𝐾) | |
5 | 1, 2, 3, 4 | lhpocnel 36710 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊)) |
6 | 5 | adantr 481 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊)) |
7 | eqid 2795 | . . . 4 ⊢ (join‘𝐾) = (join‘𝐾) | |
8 | eqid 2795 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
9 | trlcl.t | . . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
10 | trlcl.r | . . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) | |
11 | 1, 7, 8, 3, 4, 9, 10 | trlval2 36855 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊)) → (𝑅‘𝐹) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊)) |
12 | 6, 11 | mpd3an3 1454 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) = ((((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊)) |
13 | hllat 36055 | . . . 4 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | |
14 | 13 | ad2antrr 722 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐾 ∈ Lat) |
15 | hlop 36054 | . . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) | |
16 | 15 | ad2antrr 722 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐾 ∈ OP) |
17 | trlcl.b | . . . . . . 7 ⊢ 𝐵 = (Base‘𝐾) | |
18 | 17, 4 | lhpbase 36690 | . . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |
19 | 18 | ad2antlr 723 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝑊 ∈ 𝐵) |
20 | 17, 2 | opoccl 35886 | . . . . 5 ⊢ ((𝐾 ∈ OP ∧ 𝑊 ∈ 𝐵) → ((oc‘𝐾)‘𝑊) ∈ 𝐵) |
21 | 16, 19, 20 | syl2anc 584 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((oc‘𝐾)‘𝑊) ∈ 𝐵) |
22 | 17, 4, 9 | ltrncl 36817 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((oc‘𝐾)‘𝑊) ∈ 𝐵) → (𝐹‘((oc‘𝐾)‘𝑊)) ∈ 𝐵) |
23 | 21, 22 | mpd3an3 1454 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐹‘((oc‘𝐾)‘𝑊)) ∈ 𝐵) |
24 | 17, 7 | latjcl 17495 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑊) ∈ 𝐵 ∧ (𝐹‘((oc‘𝐾)‘𝑊)) ∈ 𝐵) → (((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊))) ∈ 𝐵) |
25 | 14, 21, 23, 24 | syl3anc 1364 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊))) ∈ 𝐵) |
26 | 17, 8 | latmcl 17496 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ (((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊))) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → ((((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) ∈ 𝐵) |
27 | 14, 25, 19, 26 | syl3anc 1364 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((((oc‘𝐾)‘𝑊)(join‘𝐾)(𝐹‘((oc‘𝐾)‘𝑊)))(meet‘𝐾)𝑊) ∈ 𝐵) |
28 | 12, 27 | eqeltrd 2883 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2081 class class class wbr 4966 ‘cfv 6230 (class class class)co 7021 Basecbs 16317 lecple 16406 occoc 16407 joincjn 17388 meetcmee 17389 Latclat 17489 OPcops 35864 Atomscatm 35955 HLchlt 36042 LHypclh 36676 LTrncltrn 36793 trLctrl 36850 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5086 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-iun 4831 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-riota 6982 df-ov 7024 df-oprab 7025 df-mpo 7026 df-map 8263 df-proset 17372 df-poset 17390 df-plt 17402 df-lub 17418 df-glb 17419 df-join 17420 df-meet 17421 df-p0 17483 df-p1 17484 df-lat 17490 df-oposet 35868 df-ol 35870 df-oml 35871 df-covers 35958 df-ats 35959 df-atl 35990 df-cvlat 36014 df-hlat 36043 df-lhyp 36680 df-laut 36681 df-ldil 36796 df-ltrn 36797 df-trl 36851 |
This theorem is referenced by: trljat1 36858 trljat2 36859 trlval3 36879 cdlemc3 36885 cdlemc5 36887 trlord 37261 cdlemg4c 37304 cdlemg4 37309 cdlemg6c 37312 cdlemg10c 37331 cdlemg10 37333 cdlemg12e 37339 cdlemg17dALTN 37356 cdlemg31a 37389 cdlemg31b 37390 cdlemg35 37405 cdlemg44a 37423 trljco 37432 trljco2 37433 tendoidcl 37461 tendococl 37464 tendoid 37465 tendopltp 37472 tendo0tp 37481 cdlemh1 37507 cdlemh2 37508 cdlemi1 37510 cdlemi 37512 cdlemk9 37531 cdlemk9bN 37532 cdlemkvcl 37534 cdlemk10 37535 cdlemk11 37541 cdlemk11u 37563 cdlemk37 37606 cdlemkfid1N 37613 cdlemkid1 37614 cdlemkid2 37616 cdlemk39s-id 37632 cdlemk48 37642 cdlemk50 37644 cdlemk51 37645 cdlemk52 37646 cdlemk39u 37660 tendoex 37667 dialss 37738 dia0 37744 diaglbN 37747 dia1dim 37753 dia2dimlem2 37757 dia2dimlem3 37758 dia2dimlem10 37765 cdlemm10N 37810 dib1dim 37857 diblss 37862 cdlemn2a 37888 dih1dimb 37932 dihopelvalcpre 37940 dih1 37978 dihmeetlem1N 37982 dihglblem5apreN 37983 dihglbcpreN 37992 dih1dimatlem 38021 |
Copyright terms: Public domain | W3C validator |