![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcdlmod | Structured version Visualization version GIF version |
Description: The dual vector space of functionals with closed kernels is a left module. (Contributed by NM, 13-Mar-2015.) |
Ref | Expression |
---|---|
lcdlmod.h | ⊢ 𝐻 = (LHyp‘𝐾) |
lcdlmod.c | ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
lcdlmod.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
Ref | Expression |
---|---|
lcdlmod | ⊢ (𝜑 → 𝐶 ∈ LMod) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcdlmod.h | . . 3 ⊢ 𝐻 = (LHyp‘𝐾) | |
2 | lcdlmod.c | . . 3 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) | |
3 | lcdlmod.k | . . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
4 | 1, 2, 3 | lcdlvec 39152 | . 2 ⊢ (𝜑 → 𝐶 ∈ LVec) |
5 | lveclmod 19931 | . 2 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod) | |
6 | 4, 5 | syl 17 | 1 ⊢ (𝜑 → 𝐶 ∈ LMod) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 400 = wceq 1539 ∈ wcel 2112 ‘cfv 6328 LModclmod 19687 LVecclvec 19927 HLchlt 36911 LHypclh 37545 LCDualclcd 39147 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5149 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-cnex 10616 ax-resscn 10617 ax-1cn 10618 ax-icn 10619 ax-addcl 10620 ax-addrcl 10621 ax-mulcl 10622 ax-mulrcl 10623 ax-mulcom 10624 ax-addass 10625 ax-mulass 10626 ax-distr 10627 ax-i2m1 10628 ax-1ne0 10629 ax-1rid 10630 ax-rnegex 10631 ax-rrecex 10632 ax-cnre 10633 ax-pre-lttri 10634 ax-pre-lttrn 10635 ax-pre-ltadd 10636 ax-pre-mulgt0 10637 ax-riotaBAD 36514 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-nel 3054 df-ral 3073 df-rex 3074 df-reu 3075 df-rmo 3076 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-pss 3873 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-tp 4520 df-op 4522 df-uni 4792 df-int 4832 df-iun 4878 df-iin 4879 df-br 5026 df-opab 5088 df-mpt 5106 df-tr 5132 df-id 5423 df-eprel 5428 df-po 5436 df-so 5437 df-fr 5476 df-we 5478 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-pred 6119 df-ord 6165 df-on 6166 df-lim 6167 df-suc 6168 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-riota 7101 df-ov 7146 df-oprab 7147 df-mpo 7148 df-of 7398 df-om 7573 df-1st 7686 df-2nd 7687 df-tpos 7895 df-undef 7942 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-1o 8105 df-oadd 8109 df-er 8292 df-map 8411 df-en 8521 df-dom 8522 df-sdom 8523 df-fin 8524 df-pnf 10700 df-mnf 10701 df-xr 10702 df-ltxr 10703 df-le 10704 df-sub 10895 df-neg 10896 df-nn 11660 df-2 11722 df-3 11723 df-4 11724 df-5 11725 df-6 11726 df-n0 11920 df-z 12006 df-uz 12268 df-fz 12925 df-struct 16528 df-ndx 16529 df-slot 16530 df-base 16532 df-sets 16533 df-ress 16534 df-plusg 16621 df-mulr 16622 df-sca 16624 df-vsca 16625 df-0g 16758 df-mre 16900 df-mrc 16901 df-acs 16903 df-proset 17589 df-poset 17607 df-plt 17619 df-lub 17635 df-glb 17636 df-join 17637 df-meet 17638 df-p0 17700 df-p1 17701 df-lat 17707 df-clat 17769 df-mgm 17903 df-sgrp 17952 df-mnd 17963 df-submnd 18008 df-grp 18157 df-minusg 18158 df-sbg 18159 df-subg 18328 df-cntz 18499 df-oppg 18526 df-lsm 18813 df-cmn 18960 df-abl 18961 df-mgp 19293 df-ur 19305 df-ring 19352 df-oppr 19429 df-dvdsr 19447 df-unit 19448 df-invr 19478 df-dvr 19489 df-drng 19557 df-lmod 19689 df-lss 19757 df-lsp 19797 df-lvec 19928 df-lsatoms 36537 df-lshyp 36538 df-lcv 36580 df-lfl 36619 df-lkr 36647 df-ldual 36685 df-oposet 36737 df-ol 36739 df-oml 36740 df-covers 36827 df-ats 36828 df-atl 36859 df-cvlat 36883 df-hlat 36912 df-llines 37059 df-lplanes 37060 df-lvols 37061 df-lines 37062 df-psubsp 37064 df-pmap 37065 df-padd 37357 df-lhyp 37549 df-laut 37550 df-ldil 37665 df-ltrn 37666 df-trl 37720 df-tgrp 38304 df-tendo 38316 df-edring 38318 df-dveca 38564 df-disoa 38590 df-dvech 38640 df-dib 38700 df-dic 38734 df-dih 38790 df-doch 38909 df-djh 38956 df-lcdual 39148 |
This theorem is referenced by: lcdvscl 39166 lcdlssvscl 39167 lcdvsass 39168 lcd0vcl 39175 lcd0vs 39176 lcdvs0N 39177 lcdvsub 39178 lcdvsubval 39179 mapdcv 39221 mapdincl 39222 mapdin 39223 mapdlsmcl 39224 mapdlsm 39225 mapdcnvatN 39227 mapdspex 39229 mapdn0 39230 mapdindp 39232 mapdpglem2 39234 mapdpglem2a 39235 mapdpglem3 39236 mapdpglem5N 39238 mapdpglem6 39239 mapdpglem8 39240 mapdpglem12 39244 mapdpglem13 39245 mapdpglem21 39253 mapdpglem30a 39256 mapdpglem30b 39257 mapdpglem27 39260 mapdpglem28 39262 mapdpglem30 39263 mapdpglem31 39264 mapdheq2 39290 mapdh6aN 39296 mapdh6bN 39298 mapdh6cN 39299 mapdh6dN 39300 mapdh6hN 39304 hdmap1l6a 39370 hdmap1l6b 39372 hdmap1l6c 39373 hdmap1l6d 39374 hdmap1l6h 39378 hdmap10 39401 hdmapeq0 39405 hdmapneg 39407 hdmap11 39409 hdmaprnlem3N 39411 hdmaprnlem3uN 39412 hdmaprnlem7N 39416 hdmaprnlem8N 39417 hdmaprnlem9N 39418 hdmaprnlem3eN 39419 hdmaprnlem16N 39423 hdmap14lem2a 39428 hdmap14lem4a 39432 hdmap14lem6 39434 hdmap14lem8 39436 hdmap14lem13 39441 hgmapval1 39454 hgmapadd 39455 hgmapmul 39456 hgmaprnlem2N 39458 hgmaprnlem4N 39460 hdmaplkr 39474 |
Copyright terms: Public domain | W3C validator |