Theorem lmodvscl 21068

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  +_gcplusg 17348  ._rcmulr 17349  Scalarcsca 17351   ·_𝑠 cvsca 17352  1_rcur 20326  LModclmod 21050

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-lmod 21052

This theorem is used by:  lmodvscld  21069  lmodscaf  21074  lmod0vs  21085  lmodvsmmulgdi  21087  lcomf  21091  lmodvneg1  21095  lmodvsneg  21096  lmodnegadd  21101  lmodsubvs  21108  lmodsubdi  21109  lmodsubdir  21110  lmodvsghm  21113  lmodprop2d  21114  lss1  21128  lssvsubcl  21134  lssvscl  21145  lss1d  21153  lssacs  21157  prdsvscacl  21158  lmodvsinv  21226  lmodvsinv2  21227  islmhm2  21228  0lmhm  21230  idlmhm  21231  lmhmco  21233  lmhmplusg  21234  lmhmvsca  21235  lmhmf1o  21236  lmhmpreima  21238  lmhmeql  21245  pwsdiaglmhm  21247  pwssplit3  21251  lvecvscan  21304  lvecvscan2  21305  lspsnvs  21307  lspfixed  21321  lspexch  21322  lspsolvlem  21335  lspsolv  21336  islbs2  21347  ipass  21864  ipassr  21865  phlssphl  21878  ocvlss  21891  dsmmlss  21963  frlmvscavalb  21989  frlmvplusgscavalb  21990  frlmphl  22000  uvcresum  22012  frlmssuvc2  22014  frlmup1  22017  lindfmm  22046  islindf4  22057  lindsenlbs  22070  assa2ass  22084  assapropd  22092  asclf  22102  assamulgscmlem1  22120  assamulgscmlem2  22121  mplcoe1  22259  mplmon2cl  22290  mplmon2mul  22291  mplind  22292  ply1tmcl  22504  ply1coe  22529  evl1gsummon  22596  evls1fpws  22600  evls1vsca  22604  asclply1subcl  22605  evls1maplmhm  22608  matvscl  22659  mat0dimscm  22697  matinv  22905  mply1topmatcl  23036  pm2mpmhmlem2  23050  monmat2matmon  23055  chpmat1dlem  23066  chpmat1d  23067  chpdmatlem0  23068  chfacfscmulcl  23088  cpmadugsumlemB  23105  cpmadugsumlemC  23106  cpmadugsumlemF  23107  cpmadugsumfi  23108  cpmidgsum2  23110  nlmdsdi  24913  nlmdsdir  24914  nlmmul0or  24915  nlmvscnlem2  24917  nlmvscn  24919  clmvscl  25322  cmodscmulexp  25356  cph2ass  25447  ipcau2  25468  tcphcphlem2  25470  tcphcph  25471  cphipval2  25475  4cphipval2  25476  cphipval  25477  pjthlem1  25671  mdegvscale  26307  mdegvsca  26308  plypf1  26445  ttgcontlem1  29349  lmodvslmhm  33498  eqgvscpbl  33798  qusvscpbl  33799  qusvsval  33800  imaslmod  33801  linds2eq  33822  lmhmqusker  33854  ply1degltlss  34014  gsummoncoe1fzo  34015  tngdim  34131  matdim  34133  lindsunlem  34142  lbsdiflsp0  34144  fedgmullem1  34147  fedgmullem2  34148  sitgclbn  34862  lindsadd  38375  lfl0  39946  lflsub  39948  lflmul  39949  lfl0f  39950  lfl1  39951  lfladdcl  39952  lflnegcl  39956  lflvscl  39958  lkrlss  39976  eqlkr  39980  lkrlsp  39983  lshpkrlem4  39994  lshpkrlem5  39995  lshpkrlem6  39996  lclkrlem2m  42400  lclkrlem2p  42403  lcdvscl  42486  baerlem3lem1  42588  baerlem5alem1  42589  baerlem5blem1  42590  hdmap14lem1a  42747  hdmap14lem2a  42748  hdmap14lem2N  42750  hdmap14lem3  42751  hdmap14lem4a  42752  hdmap14lem8  42756  hgmapadd  42775  hgmapmul  42776  hgmaprnlem4N  42780  hgmap11  42783  hdmapgln2  42793  hdmapinvlem3  42801  hdmapinvlem4  42802  hdmapglem7b  42809  hlhilphllem  42840  mendassa  44039  ply1mulgsum  49328  lincfsuppcl  49351  linccl  49352  lincvalsng  49354  lincvalpr  49356  lincdifsn  49362  linc1  49363  lincsum  49367  lincscm  49368  lincscmcl  49370  lincext3  49394  lindslinindimp2lem4  49399  lindslinindsimp2  49401  snlindsntor  49409  lincresunit3lem2  49418  lincresunit3  49419  zlmodzxzldeplem3  49440