Theorem lcdlmod 42217

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 42216	. 2 ⊢ (𝜑 → 𝐶 ∈ LVec)
5		lveclmod 21174	. 2 ⊢ (𝐶 ∈ LVec → 𝐶 ∈ LMod)
6	4, 5	syl 17	1 ⊢ (𝜑 → 𝐶 ∈ LMod)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1561   ∈ wcel 2143  ‘cfv 6522  LModclmod 20928  LVecclvec 21170  HLchlt 39975  LHypclh 40609  LCDualclcd 42211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719  ax-cnex 11130  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151  ax-riotaBAD 39578

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6289  df-ord 6350  df-on 6351  df-lim 6352  df-suc 6353  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-riota 7354  df-ov 7400  df-oprab 7401  df-mpo 7402  df-of 7661  df-om 7848  df-1st 7971  df-2nd 7972  df-tpos 8207  df-undef 8254  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8382  df-1o 8438  df-2o 8439  df-er 8679  df-map 8811  df-en 8929  df-dom 8930  df-sdom 8931  df-fin 8932  df-pnf 11219  df-mnf 11220  df-xr 11221  df-ltxr 11222  df-le 11223  df-sub 11417  df-neg 11418  df-nn 12212  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-6 12285  df-n0 12483  df-z 12570  df-uz 12841  df-fz 13514  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17247  df-ress 17268  df-plusg 17300  df-mulr 17301  df-sca 17303  df-vsca 17304  df-0g 17471  df-mre 17615  df-mrc 17616  df-acs 17618  df-proset 18327  df-poset 18346  df-plt 18361  df-lub 18377  df-glb 18378  df-join 18379  df-meet 18380  df-p0 18456  df-p1 18457  df-lat 18465  df-clat 18532  df-mgm 18675  df-sgrp 18754  df-mnd 18770  df-submnd 18819  df-grp 18979  df-minusg 18980  df-sbg 18981  df-subg 19166  df-cntz 19358  df-oppg 19387  df-lsm 19677  df-cmn 19823  df-abl 19824  df-mgp 20188  df-rng 20200  df-ur 20233  df-ring 20286  df-oppr 20387  df-dvdsr 20407  df-unit 20408  df-invr 20438  df-dvr 20451  df-nzr 20564  df-rlreg 20745  df-domn 20746  df-drng 20782  df-lmod 20930  df-lss 21000  df-lsp 21040  df-lvec 21171  df-lsatoms 39601  df-lshyp 39602  df-lcv 39644  df-lfl 39683  df-lkr 39711  df-ldual 39749  df-oposet 39801  df-ol 39803  df-oml 39804  df-covers 39891  df-ats 39892  df-atl 39923  df-cvlat 39947  df-hlat 39976  df-llines 40123  df-lplanes 40124  df-lvols 40125  df-lines 40126  df-psubsp 40128  df-pmap 40129  df-padd 40421  df-lhyp 40613  df-laut 40614  df-ldil 40729  df-ltrn 40730  df-trl 40784  df-tgrp 41368  df-tendo 41380  df-edring 41382  df-dveca 41628  df-disoa 41654  df-dvech 41704  df-dib 41764  df-dic 41798  df-dih 41854  df-doch 41973  df-djh 42020  df-lcdual 42212

This theorem is referenced by:  lcdvscl  42230  lcdlssvscl  42231  lcdvsass  42232  lcd0vcl  42239  lcd0vs  42240  lcdvs0N  42241  lcdvsub  42242  lcdvsubval  42243  mapdcv  42285  mapdincl  42286  mapdin  42287  mapdlsmcl  42288  mapdlsm  42289  mapdcnvatN  42291  mapdspex  42293  mapdn0  42294  mapdindp  42296  mapdpglem2  42298  mapdpglem2a  42299  mapdpglem3  42300  mapdpglem5N  42302  mapdpglem6  42303  mapdpglem8  42304  mapdpglem12  42308  mapdpglem13  42309  mapdpglem21  42317  mapdpglem30a  42320  mapdpglem30b  42321  mapdpglem27  42324  mapdpglem28  42326  mapdpglem30  42327  mapdpglem31  42328  mapdheq2  42354  mapdh6aN  42360  mapdh6bN  42362  mapdh6cN  42363  mapdh6dN  42364  mapdh6hN  42368  hdmap1l6a  42434  hdmap1l6b  42436  hdmap1l6c  42437  hdmap1l6d  42438  hdmap1l6h  42442  hdmap10  42465  hdmapeq0  42469  hdmapneg  42471  hdmap11  42473  hdmaprnlem3N  42475  hdmaprnlem3uN  42476  hdmaprnlem7N  42480  hdmaprnlem8N  42481  hdmaprnlem9N  42482  hdmaprnlem3eN  42483  hdmaprnlem16N  42487  hdmap14lem2a  42492  hdmap14lem4a  42496  hdmap14lem6  42498  hdmap14lem8  42500  hdmap14lem13  42505  hgmapval1  42518  hgmapadd  42519  hgmapmul  42520  hgmaprnlem2N  42522  hgmaprnlem4N  42524  hdmaplkr  42538