Theorem lmodvscl 19644

Description: Closure of scalar product for a left module. (hvmulcl 28796 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)

Hypotheses

Ref	Expression
lmodvscl.v	⊢ 𝑉 = (Base‘𝑊)
lmodvscl.f	⊢ 𝐹 = (Scalar‘𝑊)
lmodvscl.s	⊢ · = ( ·𝑠 ‘𝑊)
lmodvscl.k	⊢ 𝐾 = (Base‘𝐹)

Assertion

Ref	Expression
lmodvscl	⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)

Proof of Theorem lmodvscl

Step	Hyp	Ref	Expression
1		biid 264	. 2 ⊢ (𝑊 ∈ LMod ↔ 𝑊 ∈ LMod)
2		pm4.24 567	. 2 ⊢ (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾))
3		pm4.24 567	. 2 ⊢ (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
4		lmodvscl.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑊)
5		eqid 2798	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2798	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2798	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2798	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 19632	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
13	12	simpld 498	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))))
14	13	simp1d 1139	. 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
15	1, 2, 3, 14	syl3anb 1158	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ‘cfv 6324  (class class class)co 7135  Basecbs 16475  +_gcplusg 16557  ._rcmulr 16558  Scalarcsca 16560   ·_𝑠 cvsca 16561  1_rcur 19244  LModclmod 19627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-lmod 19629

This theorem is referenced by:  lmodscaf  19649  lmod0vs  19660  lmodvsmmulgdi  19662  lcomf  19666  lmodvneg1  19670  lmodvsneg  19671  lmodnegadd  19676  lmodsubvs  19683  lmodsubdi  19684  lmodsubdir  19685  lmodvsghm  19688  lmodprop2d  19689  lss1  19703  lssvsubcl  19708  lssvscl  19720  lss1d  19728  lssacs  19732  prdsvscacl  19733  lmodvsinv  19801  lmodvsinv2  19802  islmhm2  19803  0lmhm  19805  idlmhm  19806  lmhmco  19808  lmhmplusg  19809  lmhmvsca  19810  lmhmf1o  19811  lmhmpreima  19813  lmhmeql  19820  pwsdiaglmhm  19822  pwssplit3  19826  lvecvscan  19876  lvecvscan2  19877  lspsnvs  19879  lspfixed  19893  lspexch  19894  lspsolvlem  19907  lspsolv  19908  islbs2  19919  ipass  20334  ipassr  20335  phlssphl  20348  ocvlss  20361  dsmmlss  20433  frlmvscavalb  20459  frlmvplusgscavalb  20460  frlmphl  20470  uvcresum  20482  frlmssuvc2  20484  frlmup1  20487  lindfmm  20516  islindf4  20527  assa2ass  20552  assapropd  20558  asclf  20568  ascldimulOLD  20574  assamulgscmlem1  20585  assamulgscmlem2  20586  mplcoe1  20705  mplmon2cl  20739  mplmon2mul  20740  mplind  20741  mhpvscacl  20802  ply1tmcl  20901  ply1coe  20925  evl1gsummon  20989  matvscl  21036  mat0dimscm  21074  matinv  21282  mply1topmatcl  21410  pm2mpmhmlem2  21424  monmat2matmon  21429  chpmat1dlem  21440  chpmat1d  21441  chpdmatlem0  21442  chfacfscmulcl  21462  cpmadugsumlemB  21479  cpmadugsumlemC  21480  cpmadugsumlemF  21481  cpmadugsumfi  21482  cpmidgsum2  21484  nlmdsdi  23287  nlmdsdir  23288  nlmmul0or  23289  nlmvscnlem2  23291  nlmvscn  23293  clmvscl  23693  cmodscmulexp  23727  cph2ass  23818  ipcau2  23838  tcphcphlem2  23840  tcphcph  23841  cphipval2  23845  4cphipval2  23846  cphipval  23847  pjthlem1  24041  mdegvscale  24676  mdegvsca  24677  plypf1  24809  ttgcontlem1  26679  lmodvslmhm  30735  eqgvscpbl  30970  qusvscpbl  30971  qusscaval  30972  imaslmod  30973  linds2eq  30995  tngdim  31099  matdim  31101  lindsunlem  31108  lbsdiflsp0  31110  fedgmullem1  31113  fedgmullem2  31114  sitgclbn  31711  lindsadd  35050  lindsenlbs  35052  lfl0  36361  lflsub  36363  lflmul  36364  lfl0f  36365  lfl1  36366  lfladdcl  36367  lflnegcl  36371  lflvscl  36373  lkrlss  36391  eqlkr  36395  lkrlsp  36398  lshpkrlem4  36409  lshpkrlem5  36410  lshpkrlem6  36411  lclkrlem2m  38815  lclkrlem2p  38818  lcdvscl  38901  baerlem3lem1  39003  baerlem5alem1  39004  baerlem5blem1  39005  hdmap14lem1a  39162  hdmap14lem2a  39163  hdmap14lem2N  39165  hdmap14lem3  39166  hdmap14lem4a  39167  hdmap14lem8  39171  hgmapadd  39190  hgmapmul  39191  hgmaprnlem4N  39195  hgmap11  39198  hdmapgln2  39208  hdmapinvlem3  39216  hdmapinvlem4  39217  hdmapglem7b  39224  hlhilphllem  39255  frlmsnic  39453  prjspvs  39604  prjspeclsp  39606  mendassa  40138  ply1mulgsum  44798  lincfsuppcl  44822  linccl  44823  lincvalsng  44825  lincvalpr  44827  lincdifsn  44833  linc1  44834  lincsum  44838  lincscm  44839  lincscmcl  44841  lincext3  44865  lindslinindimp2lem4  44870  lindslinindsimp2  44872  snlindsntor  44880  lincresunit3lem2  44889  lincresunit3  44890  zlmodzxzldeplem3  44911