Theorem lmodvscl 20055

Description: Closure of scalar product for a left module. (hvmulcl 29276 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 260	. 2 ⊢ (𝑊 ∈ LMod ↔ 𝑊 ∈ LMod)
2		pm4.24 563	. 2 ⊢ (𝑅 ∈ 𝐾 ↔ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾))
3		pm4.24 563	. 2 ⊢ (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉))
4		lmodvscl.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑊)
5		eqid 2738	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2738	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2738	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2738	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 20043	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))) ∧ (((𝑅(.r‘𝐹)𝑅) · 𝑋) = (𝑅 · (𝑅 · 𝑋)) ∧ ((1r‘𝐹) · 𝑋) = 𝑋)))
13	12	simpld 494	. . 3 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → ((𝑅 · 𝑋) ∈ 𝑉 ∧ (𝑅 · (𝑋(+g‘𝑊)𝑋)) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋)) ∧ ((𝑅(+g‘𝐹)𝑅) · 𝑋) = ((𝑅 · 𝑋)(+g‘𝑊)(𝑅 · 𝑋))))
14	13	simp1d 1140	. 2 ⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑅 ∈ 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (𝑅 · 𝑋) ∈ 𝑉)
15	1, 2, 3, 14	syl3anb 1159	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  +_gcplusg 16888  ._rcmulr 16889  Scalarcsca 16891   ·_𝑠 cvsca 16892  1_rcur 19652  LModclmod 20038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-lmod 20040

This theorem is referenced by:  lmodscaf  20060  lmod0vs  20071  lmodvsmmulgdi  20073  lcomf  20077  lmodvneg1  20081  lmodvsneg  20082  lmodnegadd  20087  lmodsubvs  20094  lmodsubdi  20095  lmodsubdir  20096  lmodvsghm  20099  lmodprop2d  20100  lss1  20115  lssvsubcl  20120  lssvscl  20132  lss1d  20140  lssacs  20144  prdsvscacl  20145  lmodvsinv  20213  lmodvsinv2  20214  islmhm2  20215  0lmhm  20217  idlmhm  20218  lmhmco  20220  lmhmplusg  20221  lmhmvsca  20222  lmhmf1o  20223  lmhmpreima  20225  lmhmeql  20232  pwsdiaglmhm  20234  pwssplit3  20238  lvecvscan  20288  lvecvscan2  20289  lspsnvs  20291  lspfixed  20305  lspexch  20306  lspsolvlem  20319  lspsolv  20320  islbs2  20331  ipass  20762  ipassr  20763  phlssphl  20776  ocvlss  20789  dsmmlss  20861  frlmvscavalb  20887  frlmvplusgscavalb  20888  frlmphl  20898  uvcresum  20910  frlmssuvc2  20912  frlmup1  20915  lindfmm  20944  islindf4  20955  assa2ass  20980  assapropd  20986  asclf  20996  assamulgscmlem1  21013  assamulgscmlem2  21014  mplcoe1  21148  mplmon2cl  21186  mplmon2mul  21187  mplind  21188  mhpvscacl  21254  ply1tmcl  21353  ply1coe  21377  evl1gsummon  21441  matvscl  21488  mat0dimscm  21526  matinv  21734  mply1topmatcl  21862  pm2mpmhmlem2  21876  monmat2matmon  21881  chpmat1dlem  21892  chpmat1d  21893  chpdmatlem0  21894  chfacfscmulcl  21914  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  cpmadugsumfi  21934  cpmidgsum2  21936  nlmdsdi  23751  nlmdsdir  23752  nlmmul0or  23753  nlmvscnlem2  23755  nlmvscn  23757  clmvscl  24157  cmodscmulexp  24191  cph2ass  24282  ipcau2  24303  tcphcphlem2  24305  tcphcph  24306  cphipval2  24310  4cphipval2  24311  cphipval  24312  pjthlem1  24506  mdegvscale  25145  mdegvsca  25146  plypf1  25278  ttgcontlem1  27155  lmodvslmhm  31212  eqgvscpbl  31452  qusvscpbl  31453  qusscaval  31454  imaslmod  31455  linds2eq  31477  tngdim  31598  matdim  31600  lindsunlem  31607  lbsdiflsp0  31609  fedgmullem1  31612  fedgmullem2  31613  sitgclbn  32210  lindsadd  35697  lindsenlbs  35699  lfl0  37006  lflsub  37008  lflmul  37009  lfl0f  37010  lfl1  37011  lfladdcl  37012  lflnegcl  37016  lflvscl  37018  lkrlss  37036  eqlkr  37040  lkrlsp  37043  lshpkrlem4  37054  lshpkrlem5  37055  lshpkrlem6  37056  lclkrlem2m  39460  lclkrlem2p  39463  lcdvscl  39546  baerlem3lem1  39648  baerlem5alem1  39649  baerlem5blem1  39650  hdmap14lem1a  39807  hdmap14lem2a  39808  hdmap14lem2N  39810  hdmap14lem3  39811  hdmap14lem4a  39812  hdmap14lem8  39816  hgmapadd  39835  hgmapmul  39836  hgmaprnlem4N  39840  hgmap11  39843  hdmapgln2  39853  hdmapinvlem3  39861  hdmapinvlem4  39862  hdmapglem7b  39869  hlhilphllem  39904  frlmsnic  40188  prjspvs  40370  prjspeclsp  40372  mendassa  40935  ply1mulgsum  45619  lincfsuppcl  45642  linccl  45643  lincvalsng  45645  lincvalpr  45647  lincdifsn  45653  linc1  45654  lincsum  45658  lincscm  45659  lincscmcl  45661  lincext3  45685  lindslinindimp2lem4  45690  lindslinindsimp2  45692  snlindsntor  45700  lincresunit3lem2  45709  lincresunit3  45710  zlmodzxzldeplem3  45731