Theorem lmodvscl 20809

Description: Closure of scalar product for a left module. (hvmulcl 30988 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 2731	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2731	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2731	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2731	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 20796	. . . 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 1541   ∈ wcel 2111  ‘cfv 6481  (class class class)co 7346  Basecbs 17117  +_gcplusg 17158  ._rcmulr 17159  Scalarcsca 17161   ·_𝑠 cvsca 17162  1_rcur 20097  LModclmod 20791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-lmod 20793

This theorem is referenced by:  lmodvscld  20810  lmodscaf  20815  lmod0vs  20826  lmodvsmmulgdi  20828  lcomf  20832  lmodvneg1  20836  lmodvsneg  20837  lmodnegadd  20842  lmodsubvs  20849  lmodsubdi  20850  lmodsubdir  20851  lmodvsghm  20854  lmodprop2d  20855  lss1  20869  lssvsubcl  20875  lssvscl  20886  lss1d  20894  lssacs  20898  prdsvscacl  20899  lmodvsinv  20968  lmodvsinv2  20969  islmhm2  20970  0lmhm  20972  idlmhm  20973  lmhmco  20975  lmhmplusg  20976  lmhmvsca  20977  lmhmf1o  20978  lmhmpreima  20980  lmhmeql  20987  pwsdiaglmhm  20989  pwssplit3  20993  lvecvscan  21046  lvecvscan2  21047  lspsnvs  21049  lspfixed  21063  lspexch  21064  lspsolvlem  21077  lspsolv  21078  islbs2  21089  ipass  21580  ipassr  21581  phlssphl  21594  ocvlss  21607  dsmmlss  21679  frlmvscavalb  21705  frlmvplusgscavalb  21706  frlmphl  21716  uvcresum  21728  frlmssuvc2  21730  frlmup1  21733  lindfmm  21762  islindf4  21773  assa2ass  21798  assapropd  21807  asclf  21817  assamulgscmlem1  21834  assamulgscmlem2  21835  mplcoe1  21970  mplmon2cl  22001  mplmon2mul  22002  mplind  22003  ply1tmcl  22184  ply1coe  22211  evl1gsummon  22278  evls1fpws  22282  evls1vsca  22286  asclply1subcl  22287  evls1maplmhm  22290  matvscl  22344  mat0dimscm  22382  matinv  22590  mply1topmatcl  22718  pm2mpmhmlem2  22732  monmat2matmon  22737  chpmat1dlem  22748  chpmat1d  22749  chpdmatlem0  22750  chfacfscmulcl  22770  cpmadugsumlemB  22787  cpmadugsumlemC  22788  cpmadugsumlemF  22789  cpmadugsumfi  22790  cpmidgsum2  22792  nlmdsdi  24594  nlmdsdir  24595  nlmmul0or  24596  nlmvscnlem2  24598  nlmvscn  24600  clmvscl  25013  cmodscmulexp  25047  cph2ass  25138  ipcau2  25159  tcphcphlem2  25161  tcphcph  25162  cphipval2  25166  4cphipval2  25167  cphipval  25168  pjthlem1  25362  mdegvscale  26005  mdegvsca  26006  plypf1  26142  ttgcontlem1  28861  lmodvslmhm  33025  eqgvscpbl  33310  qusvscpbl  33311  qusvsval  33312  imaslmod  33313  linds2eq  33341  lmhmqusker  33377  ply1degltlss  33552  gsummoncoe1fzo  33553  tngdim  33621  matdim  33623  lindsunlem  33632  lbsdiflsp0  33634  fedgmullem1  33637  fedgmullem2  33638  sitgclbn  34351  lindsadd  37652  lindsenlbs  37654  lfl0  39103  lflsub  39105  lflmul  39106  lfl0f  39107  lfl1  39108  lfladdcl  39109  lflnegcl  39113  lflvscl  39115  lkrlss  39133  eqlkr  39137  lkrlsp  39140  lshpkrlem4  39151  lshpkrlem5  39152  lshpkrlem6  39153  lclkrlem2m  41557  lclkrlem2p  41560  lcdvscl  41643  baerlem3lem1  41745  baerlem5alem1  41746  baerlem5blem1  41747  hdmap14lem1a  41904  hdmap14lem2a  41905  hdmap14lem2N  41907  hdmap14lem3  41908  hdmap14lem4a  41909  hdmap14lem8  41913  hgmapadd  41932  hgmapmul  41933  hgmaprnlem4N  41937  hgmap11  41940  hdmapgln2  41950  hdmapinvlem3  41958  hdmapinvlem4  41959  hdmapglem7b  41966  hlhilphllem  41997  mendassa  43222  ply1mulgsum  48421  lincfsuppcl  48444  linccl  48445  lincvalsng  48447  lincvalpr  48449  lincdifsn  48455  linc1  48456  lincsum  48460  lincscm  48461  lincscmcl  48463  lincext3  48487  lindslinindimp2lem4  48492  lindslinindsimp2  48494  snlindsntor  48502  lincresunit3lem2  48511  lincresunit3  48512  zlmodzxzldeplem3  48533