Theorem lcdlmod 41134

Description: The dual vector space of functionals with closed kernels is a left module. (Contributed by NM, 13-Mar-2015.)

Hypotheses

Ref	Expression
lcdlmod.h	⊢ 𝐻 = (LHyp‘𝐾)
lcdlmod.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
lcdlmod.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))

Assertion

Ref	Expression
lcdlmod	⊢ (𝜑 → 𝐶 ∈ LMod)

Proof of Theorem lcdlmod

Step	Hyp	Ref	Expression
1		lcdlmod.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		lcdlmod.c	. . 3 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
3		lcdlmod.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4	1, 2, 3	lcdlvec 41133	. 2 ⊢ (𝜑 → 𝐶 ∈ LVec)
5		lveclmod 20995	. 2 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
6	4, 5	syl 17	1 ⊢ (𝜑 → 𝐶 ∈ LMod)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ‘cfv 6547  LModclmod 20747  LVecclvec 20991  HLchlt 38891  LHypclh 39526  LCDualclcd 41128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-riotaBAD 38494

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7373  df-ov 7420  df-oprab 7421  df-mpo 7422  df-of 7683  df-om 7870  df-1st 7992  df-2nd 7993  df-tpos 8230  df-undef 8277  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8723  df-map 8845  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-2 12305  df-3 12306  df-4 12307  df-5 12308  df-6 12309  df-n0 12503  df-z 12589  df-uz 12853  df-fz 13517  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-ress 17209  df-plusg 17245  df-mulr 17246  df-sca 17248  df-vsca 17249  df-0g 17422  df-mre 17565  df-mrc 17566  df-acs 17568  df-proset 18286  df-poset 18304  df-plt 18321  df-lub 18337  df-glb 18338  df-join 18339  df-meet 18340  df-p0 18416  df-p1 18417  df-lat 18423  df-clat 18490  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-submnd 18740  df-grp 18897  df-minusg 18898  df-sbg 18899  df-subg 19082  df-cntz 19272  df-oppg 19301  df-lsm 19595  df-cmn 19741  df-abl 19742  df-mgp 20079  df-rng 20097  df-ur 20126  df-ring 20179  df-oppr 20277  df-dvdsr 20300  df-unit 20301  df-invr 20331  df-dvr 20344  df-drng 20630  df-lmod 20749  df-lss 20820  df-lsp 20860  df-lvec 20992  df-lsatoms 38517  df-lshyp 38518  df-lcv 38560  df-lfl 38599  df-lkr 38627  df-ldual 38665  df-oposet 38717  df-ol 38719  df-oml 38720  df-covers 38807  df-ats 38808  df-atl 38839  df-cvlat 38863  df-hlat 38892  df-llines 39040  df-lplanes 39041  df-lvols 39042  df-lines 39043  df-psubsp 39045  df-pmap 39046  df-padd 39338  df-lhyp 39530  df-laut 39531  df-ldil 39646  df-ltrn 39647  df-trl 39701  df-tgrp 40285  df-tendo 40297  df-edring 40299  df-dveca 40545  df-disoa 40571  df-dvech 40621  df-dib 40681  df-dic 40715  df-dih 40771  df-doch 40890  df-djh 40937  df-lcdual 41129

This theorem is referenced by:  lcdvscl  41147  lcdlssvscl  41148  lcdvsass  41149  lcd0vcl  41156  lcd0vs  41157  lcdvs0N  41158  lcdvsub  41159  lcdvsubval  41160  mapdcv  41202  mapdincl  41203  mapdin  41204  mapdlsmcl  41205  mapdlsm  41206  mapdcnvatN  41208  mapdspex  41210  mapdn0  41211  mapdindp  41213  mapdpglem2  41215  mapdpglem2a  41216  mapdpglem3  41217  mapdpglem5N  41219  mapdpglem6  41220  mapdpglem8  41221  mapdpglem12  41225  mapdpglem13  41226  mapdpglem21  41234  mapdpglem30a  41237  mapdpglem30b  41238  mapdpglem27  41241  mapdpglem28  41243  mapdpglem30  41244  mapdpglem31  41245  mapdheq2  41271  mapdh6aN  41277  mapdh6bN  41279  mapdh6cN  41280  mapdh6dN  41281  mapdh6hN  41285  hdmap1l6a  41351  hdmap1l6b  41353  hdmap1l6c  41354  hdmap1l6d  41355  hdmap1l6h  41359  hdmap10  41382  hdmapeq0  41386  hdmapneg  41388  hdmap11  41390  hdmaprnlem3N  41392  hdmaprnlem3uN  41393  hdmaprnlem7N  41397  hdmaprnlem8N  41398  hdmaprnlem9N  41399  hdmaprnlem3eN  41400  hdmaprnlem16N  41404  hdmap14lem2a  41409  hdmap14lem4a  41413  hdmap14lem6  41415  hdmap14lem8  41417  hdmap14lem13  41422  hgmapval1  41435  hgmapadd  41436  hgmapmul  41437  hgmaprnlem2N  41439  hgmaprnlem4N  41441  hdmaplkr  41455