Theorem lmodvscl 21158

Description: Closure of scalar product for a left module. (hvmulcl 31620 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 2760	. . . . 5 ⊢ (+g‘𝑊) = (+g‘𝑊)
6		lmodvscl.s	. . . . 5 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscl.f	. . . . 5 ⊢ 𝐹 = (Scalar‘𝑊)
8		lmodvscl.k	. . . . 5 ⊢ 𝐾 = (Base‘𝐹)
9		eqid 2760	. . . . 5 ⊢ (+g‘𝐹) = (+g‘𝐹)
10		eqid 2760	. . . . 5 ⊢ (.r‘𝐹) = (.r‘𝐹)
11		eqid 2760	. . . . 5 ⊢ (1r‘𝐹) = (1r‘𝐹)
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 21145	. . . 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 1569   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  Basecbs 17392  +_gcplusg 17433  ._rcmulr 17434  Scalarcsca 17436   ·_𝑠 cvsca 17437  1_rcur 20412  LModclmod 21140

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-lmod 21142

This theorem is used by:  lmodvscld  21159  lmodscaf  21164  lmod0vs  21175  lmodvsmmulgdi  21177  lcomf  21181  lmodvneg1  21185  lmodvsneg  21186  lmodnegadd  21191  lmodsubvs  21198  lmodsubdi  21199  lmodsubdir  21200  lmodvsghm  21203  lmodprop2d  21204  lss1  21218  lssvsubcl  21224  lssvscl  21235  lss1d  21243  lssacs  21247  prdsvscacl  21248  lmodvsinv  21316  lmodvsinv2  21317  islmhm2  21318  0lmhm  21320  idlmhm  21321  lmhmco  21323  lmhmplusg  21324  lmhmvsca  21325  lmhmf1o  21326  lmhmpreima  21328  lmhmeql  21335  pwsdiaglmhm  21337  pwssplit3  21341  lvecvscan  21394  lvecvscan2  21395  lspsnvs  21397  lspfixed  21411  lspexch  21412  lspsolvlem  21425  lspsolv  21426  islbs2  21437  ipass  21956  ipassr  21957  phlssphl  21970  ocvlss  21983  dsmmlss  22055  frlmvscavalb  22081  frlmvplusgscavalb  22082  frlmphl  22092  uvcresum  22104  frlmssuvc2  22106  frlmup1  22109  lindfmm  22138  islindf4  22149  lindsenlbs  22162  assa2ass  22176  assapropd  22184  asclf  22194  assamulgscmlem1  22212  assamulgscmlem2  22213  mplcoe1  22351  mplmon2cl  22382  mplmon2mul  22383  mplind  22384  ply1tmcl  22596  ply1coe  22621  evl1gsummon  22688  evls1fpws  22692  evls1vsca  22696  asclply1subcl  22697  evls1maplmhm  22700  matvscl  22751  mat0dimscm  22789  matinv  22997  mply1topmatcl  23128  pm2mpmhmlem2  23142  monmat2matmon  23147  chpmat1dlem  23158  chpmat1d  23159  chpdmatlem0  23160  chfacfscmulcl  23180  cpmadugsumlemB  23197  cpmadugsumlemC  23198  cpmadugsumlemF  23199  cpmadugsumfi  23200  cpmidgsum2  23202  nlmdsdi  25005  nlmdsdir  25006  nlmmul0or  25007  nlmvscnlem2  25009  nlmvscn  25011  clmvscl  25414  cmodscmulexp  25448  cph2ass  25539  ipcau2  25560  tcphcphlem2  25562  tcphcph  25563  cphipval2  25567  4cphipval2  25568  cphipval  25569  pjthlem1  25763  mdegvscale  26398  mdegvsca  26399  plypf1  26536  ttgcontlem1  29467  lmodvslmhm  33657  eqgvscpbl  33957  qusvscpbl  33958  qusvsval  33959  imaslmod  33960  linds2eq  33982  lmhmqusker  34014  ply1degltlss  34174  gsummoncoe1fzo  34175  tngdim  34291  matdim  34293  lindsunlem  34302  lbsdiflsp0  34304  fedgmullem1  34307  fedgmullem2  34308  sitgclbn  35021  lindsadd  38629  lfl0  40215  lflsub  40217  lflmul  40218  lfl0f  40219  lfl1  40220  lfladdcl  40221  lflnegcl  40225  lflvscl  40227  lkrlss  40245  eqlkr  40249  lkrlsp  40252  lshpkrlem4  40263  lshpkrlem5  40264  lshpkrlem6  40265  lclkrlem2m  42669  lclkrlem2p  42672  lcdvscl  42755  baerlem3lem1  42857  baerlem5alem1  42858  baerlem5blem1  42859  hdmap14lem1a  43016  hdmap14lem2a  43017  hdmap14lem2N  43019  hdmap14lem3  43020  hdmap14lem4a  43021  hdmap14lem8  43025  hgmapadd  43044  hgmapmul  43045  hgmaprnlem4N  43049  hgmap11  43052  hdmapgln2  43062  hdmapinvlem3  43070  hdmapinvlem4  43071  hdmapglem7b  43078  hlhilphllem  43109  mendassa  44285  ply1mulgsum  49595  lincfsuppcl  49618  linccl  49619  lincvalsng  49621  lincvalpr  49623  lincdifsn  49629  linc1  49630  lincsum  49634  lincscm  49635  lincscmcl  49637  lincext3  49661  lindslinindimp2lem4  49666  lindslinindsimp2  49668  snlindsntor  49676  lincresunit3lem2  49685  lincresunit3  49686  zlmodzxzldeplem3  49707