Theorem lmodvscl 20784

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  Scalarcsca 17223   ·_𝑠 cvsca 17224  1_rcur 20090  LModclmod 20766

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-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-lmod 20768

This theorem is referenced by:  lmodvscld  20785  lmodscaf  20790  lmod0vs  20801  lmodvsmmulgdi  20803  lcomf  20807  lmodvneg1  20811  lmodvsneg  20812  lmodnegadd  20817  lmodsubvs  20824  lmodsubdi  20825  lmodsubdir  20826  lmodvsghm  20829  lmodprop2d  20830  lss1  20844  lssvsubcl  20850  lssvscl  20861  lss1d  20869  lssacs  20873  prdsvscacl  20874  lmodvsinv  20943  lmodvsinv2  20944  islmhm2  20945  0lmhm  20947  idlmhm  20948  lmhmco  20950  lmhmplusg  20951  lmhmvsca  20952  lmhmf1o  20953  lmhmpreima  20955  lmhmeql  20962  pwsdiaglmhm  20964  pwssplit3  20968  lvecvscan  21021  lvecvscan2  21022  lspsnvs  21024  lspfixed  21038  lspexch  21039  lspsolvlem  21052  lspsolv  21053  islbs2  21064  ipass  21554  ipassr  21555  phlssphl  21568  ocvlss  21581  dsmmlss  21653  frlmvscavalb  21679  frlmvplusgscavalb  21680  frlmphl  21690  uvcresum  21702  frlmssuvc2  21704  frlmup1  21707  lindfmm  21736  islindf4  21747  assa2ass  21772  assapropd  21781  asclf  21791  assamulgscmlem1  21808  assamulgscmlem2  21809  mplcoe1  21944  mplmon2cl  21975  mplmon2mul  21976  mplind  21977  ply1tmcl  22158  ply1coe  22185  evl1gsummon  22252  evls1fpws  22256  evls1vsca  22260  asclply1subcl  22261  evls1maplmhm  22264  matvscl  22318  mat0dimscm  22356  matinv  22564  mply1topmatcl  22692  pm2mpmhmlem2  22706  monmat2matmon  22711  chpmat1dlem  22722  chpmat1d  22723  chpdmatlem0  22724  chfacfscmulcl  22744  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  cpmadugsumfi  22764  cpmidgsum2  22766  nlmdsdi  24569  nlmdsdir  24570  nlmmul0or  24571  nlmvscnlem2  24573  nlmvscn  24575  clmvscl  24988  cmodscmulexp  25022  cph2ass  25113  ipcau2  25134  tcphcphlem2  25136  tcphcph  25137  cphipval2  25141  4cphipval2  25142  cphipval  25143  pjthlem1  25337  mdegvscale  25980  mdegvsca  25981  plypf1  26117  ttgcontlem1  28812  lmodvslmhm  32990  eqgvscpbl  33321  qusvscpbl  33322  qusvsval  33323  imaslmod  33324  linds2eq  33352  lmhmqusker  33388  ply1degltlss  33562  gsummoncoe1fzo  33563  tngdim  33609  matdim  33611  lindsunlem  33620  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  sitgclbn  34334  lindsadd  37607  lindsenlbs  37609  lfl0  39058  lflsub  39060  lflmul  39061  lfl0f  39062  lfl1  39063  lfladdcl  39064  lflnegcl  39068  lflvscl  39070  lkrlss  39088  eqlkr  39092  lkrlsp  39095  lshpkrlem4  39106  lshpkrlem5  39107  lshpkrlem6  39108  lclkrlem2m  41513  lclkrlem2p  41516  lcdvscl  41599  baerlem3lem1  41701  baerlem5alem1  41702  baerlem5blem1  41703  hdmap14lem1a  41860  hdmap14lem2a  41861  hdmap14lem2N  41863  hdmap14lem3  41864  hdmap14lem4a  41865  hdmap14lem8  41869  hgmapadd  41888  hgmapmul  41889  hgmaprnlem4N  41893  hgmap11  41896  hdmapgln2  41906  hdmapinvlem3  41914  hdmapinvlem4  41915  hdmapglem7b  41922  hlhilphllem  41953  mendassa  43179  ply1mulgsum  48379  lincfsuppcl  48402  linccl  48403  lincvalsng  48405  lincvalpr  48407  lincdifsn  48413  linc1  48414  lincsum  48418  lincscm  48419  lincscmcl  48421  lincext3  48445  lindslinindimp2lem4  48450  lindslinindsimp2  48452  snlindsntor  48460  lincresunit3lem2  48469  lincresunit3  48470  zlmodzxzldeplem3  48491