Theorem lcdlmod 41581

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6513  LModclmod 20772  LVecclvec 21015  HLchlt 39338  LHypclh 39973  LCDualclcd 41575

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5236  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  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 38941

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-pss 3936  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4874  df-int 4913  df-iun 4959  df-iin 4960  df-br 5110  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-pred 6276  df-ord 6337  df-on 6338  df-lim 6339  df-suc 6340  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-riota 7346  df-ov 7392  df-oprab 7393  df-mpo 7394  df-of 7655  df-om 7845  df-1st 7970  df-2nd 7971  df-tpos 8207  df-undef 8254  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8380  df-1o 8436  df-2o 8437  df-er 8673  df-map 8803  df-en 8921  df-dom 8922  df-sdom 8923  df-fin 8924  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-sub 11413  df-neg 11414  df-nn 12188  df-2 12250  df-3 12251  df-4 12252  df-5 12253  df-6 12254  df-n0 12449  df-z 12536  df-uz 12800  df-fz 13475  df-struct 17123  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17186  df-ress 17207  df-plusg 17239  df-mulr 17240  df-sca 17242  df-vsca 17243  df-0g 17410  df-mre 17553  df-mrc 17554  df-acs 17556  df-proset 18261  df-poset 18280  df-plt 18295  df-lub 18311  df-glb 18312  df-join 18313  df-meet 18314  df-p0 18390  df-p1 18391  df-lat 18397  df-clat 18464  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-submnd 18717  df-grp 18874  df-minusg 18875  df-sbg 18876  df-subg 19061  df-cntz 19255  df-oppg 19284  df-lsm 19572  df-cmn 19718  df-abl 19719  df-mgp 20056  df-rng 20068  df-ur 20097  df-ring 20150  df-oppr 20252  df-dvdsr 20272  df-unit 20273  df-invr 20303  df-dvr 20316  df-nzr 20428  df-rlreg 20609  df-domn 20610  df-drng 20646  df-lmod 20774  df-lss 20844  df-lsp 20884  df-lvec 21016  df-lsatoms 38964  df-lshyp 38965  df-lcv 39007  df-lfl 39046  df-lkr 39074  df-ldual 39112  df-oposet 39164  df-ol 39166  df-oml 39167  df-covers 39254  df-ats 39255  df-atl 39286  df-cvlat 39310  df-hlat 39339  df-llines 39487  df-lplanes 39488  df-lvols 39489  df-lines 39490  df-psubsp 39492  df-pmap 39493  df-padd 39785  df-lhyp 39977  df-laut 39978  df-ldil 40093  df-ltrn 40094  df-trl 40148  df-tgrp 40732  df-tendo 40744  df-edring 40746  df-dveca 40992  df-disoa 41018  df-dvech 41068  df-dib 41128  df-dic 41162  df-dih 41218  df-doch 41337  df-djh 41384  df-lcdual 41576

This theorem is referenced by:  lcdvscl  41594  lcdlssvscl  41595  lcdvsass  41596  lcd0vcl  41603  lcd0vs  41604  lcdvs0N  41605  lcdvsub  41606  lcdvsubval  41607  mapdcv  41649  mapdincl  41650  mapdin  41651  mapdlsmcl  41652  mapdlsm  41653  mapdcnvatN  41655  mapdspex  41657  mapdn0  41658  mapdindp  41660  mapdpglem2  41662  mapdpglem2a  41663  mapdpglem3  41664  mapdpglem5N  41666  mapdpglem6  41667  mapdpglem8  41668  mapdpglem12  41672  mapdpglem13  41673  mapdpglem21  41681  mapdpglem30a  41684  mapdpglem30b  41685  mapdpglem27  41688  mapdpglem28  41690  mapdpglem30  41691  mapdpglem31  41692  mapdheq2  41718  mapdh6aN  41724  mapdh6bN  41726  mapdh6cN  41727  mapdh6dN  41728  mapdh6hN  41732  hdmap1l6a  41798  hdmap1l6b  41800  hdmap1l6c  41801  hdmap1l6d  41802  hdmap1l6h  41806  hdmap10  41829  hdmapeq0  41833  hdmapneg  41835  hdmap11  41837  hdmaprnlem3N  41839  hdmaprnlem3uN  41840  hdmaprnlem7N  41844  hdmaprnlem8N  41845  hdmaprnlem9N  41846  hdmaprnlem3eN  41847  hdmaprnlem16N  41851  hdmap14lem2a  41856  hdmap14lem4a  41860  hdmap14lem6  41862  hdmap14lem8  41864  hdmap14lem13  41869  hgmapval1  41882  hgmapadd  41883  hgmapmul  41884  hgmaprnlem2N  41886  hgmaprnlem4N  41888  hdmaplkr  41902