Theorem lmodvscl 18880

Description: Closure of scalar product for a left module. (hvmulcl 27870 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)

Hypotheses

Ref	Expression
lmodvscl.v	|- V = ( Base ` W )
lmodvscl.f	|- F = (Scalar ` W )
lmodvscl.s	|- .x. = ( .s ` W )
lmodvscl.k	|- K = ( Base ` F )

Assertion

Ref	Expression
lmodvscl	|- ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V )

Proof of Theorem lmodvscl

Step	Hyp	Ref	Expression
1		biid 251	. 2 |- ( W e. LMod <-> W e. LMod )
2		pm4.24 675	. 2 |- ( R e. K <-> ( R e. K /\ R e. K ) )
3		pm4.24 675	. 2 |- ( X e. V <-> ( X e. V /\ X e. V ) )
4		lmodvscl.v	. . . . 5 |- V = ( Base ` W )
5		eqid 2622	. . . . 5 |- ( +g ` W ) = ( +g ` W )
6		lmodvscl.s	. . . . 5 |- .x. = ( .s ` W )
7		lmodvscl.f	. . . . 5 |- F = (Scalar ` W )
8		lmodvscl.k	. . . . 5 |- K = ( Base ` F )
9		eqid 2622	. . . . 5 |- ( +g ` F ) = ( +g ` F )
10		eqid 2622	. . . . 5 |- ( .r ` F ) = ( .r ` F )
11		eqid 2622	. . . . 5 |- ( 1r ` F ) = ( 1r ` F )
12	4, 5, 6, 7, 8, 9, 10, 11	lmodlema 18868	. . . 4 |- ( ( W e. LMod /\ ( R e. K /\ R e. K ) /\ ( X e. V /\ X e. V ) ) -> ( ( ( R .x. X ) e. V /\ ( R .x. ( X ( +g ` W ) X ) ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) ) /\ ( ( ( R ( .r ` F ) R ) .x. X ) = ( R .x. ( R .x. X ) ) /\ ( ( 1r ` F ) .x. X ) = X ) ) )
13	12	simpld 475	. . 3 |- ( ( W e. LMod /\ ( R e. K /\ R e. K ) /\ ( X e. V /\ X e. V ) ) -> ( ( R .x. X ) e. V /\ ( R .x. ( X ( +g ` W ) X ) ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) ) )
14	13	simp1d 1073	. 2 |- ( ( W e. LMod /\ ( R e. K /\ R e. K ) /\ ( X e. V /\ X e. V ) ) -> ( R .x. X ) e. V )
15	1, 2, 3, 14	syl3anb 1369	1 |- ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   ` cfv 5888  (class class class)co 6650   Basecbs 15857   +g cplusg 15941   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   1rcur 18501   LModclmod 18863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-lmod 18865

This theorem is referenced by:  lmodscaf  18885  lmod0vs  18896  lmodvsmmulgdi  18898  lcomf  18902  lmodvneg1  18906  lmodvsneg  18907  lmodnegadd  18912  lmodsubvs  18919  lmodsubdi  18920  lmodsubdir  18921  lmodvsghm  18924  lmodprop2d  18925  lss1  18939  lssvsubcl  18944  lssvscl  18955  lss1d  18963  lssacs  18967  prdsvscacl  18968  lmodvsinv  19036  lmodvsinv2  19037  islmhm2  19038  0lmhm  19040  idlmhm  19041  lmhmco  19043  lmhmplusg  19044  lmhmvsca  19045  lmhmf1o  19046  lmhmpreima  19048  lmhmeql  19055  pwsdiaglmhm  19057  pwssplit3  19061  lvecvscan  19111  lvecvscan2  19112  lspsnvs  19114  lspfixed  19128  lspexch  19129  lspsolvlem  19142  lspsolv  19143  islbs2  19154  assa2ass  19322  assapropd  19327  asclf  19337  asclrhm  19342  assamulgscmlem1  19348  assamulgscmlem2  19349  mplcoe1  19465  mplmon2cl  19500  mplmon2mul  19501  mplind  19502  ply1tmcl  19642  ply1coe  19666  evl1gsummon  19729  ipass  19990  ipassr  19991  ocvlss  20016  dsmmlss  20088  frlmphl  20120  uvcresum  20132  frlmssuvc2  20134  frlmup1  20137  lindfmm  20166  islindf4  20177  matvscl  20237  mat0dimscm  20275  matinv  20483  mply1topmatcl  20610  pm2mpmhmlem2  20624  monmat2matmon  20629  chpmat1dlem  20640  chpmat1d  20641  chpdmatlem0  20642  chfacfscmulcl  20662  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  cpmadugsumfi  20682  cpmidgsum2  20684  nlmdsdi  22485  nlmdsdir  22486  nlmmul0or  22487  nlmvscnlem2  22489  nlmvscn  22491  clmvscl  22888  cmodscmulexp  22922  cph2ass  23013  ipcau2  23033  tchcphlem2  23035  tchcph  23036  cphipval2  23040  4cphipval2  23041  cphipval  23042  pjthlem1  23208  mdegvscale  23835  mdegvsca  23836  plypf1  23968  ttgcontlem1  25765  sitgclbn  30405  lindsenlbs  33404  lfl0  34352  lflsub  34354  lflmul  34355  lfl0f  34356  lfl1  34357  lfladdcl  34358  lflnegcl  34362  lflvscl  34364  lkrlss  34382  eqlkr  34386  lkrlsp  34389  lshpkrlem4  34400  lshpkrlem5  34401  lshpkrlem6  34402  lclkrlem2m  36808  lclkrlem2p  36811  lcdvscl  36894  baerlem3lem1  36996  baerlem5alem1  36997  baerlem5blem1  36998  hdmap14lem1a  37158  hdmap14lem2a  37159  hdmap14lem2N  37161  hdmap14lem3  37162  hdmap14lem4a  37163  hdmap14lem8  37167  hgmapadd  37186  hgmapmul  37187  hgmaprnlem4N  37191  hgmap11  37194  hdmapgln2  37204  hdmapinvlem3  37212  hdmapinvlem4  37213  hdmapglem7b  37220  hlhilphllem  37251  mendassa  37764  ply1mulgsum  42178  lincfsuppcl  42202  linccl  42203  lincvalsng  42205  lincvalpr  42207  lincdifsn  42213  linc1  42214  lincsum  42218  lincscm  42219  lincscmcl  42221  lincext3  42245  lindslinindimp2lem4  42250  lindslinindsimp2  42252  snlindsntor  42260  lincresunit3lem2  42269  lincresunit3  42270  zlmodzxzldeplem3  42291