MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodvsass Structured version   Unicode version

Theorem lmodvsass 17349
Description: Associative law for scalar product. (ax-hvmulass 25697 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
Hypotheses
Ref Expression
lmodvsass.v  |-  V  =  ( Base `  W
)
lmodvsass.f  |-  F  =  (Scalar `  W )
lmodvsass.s  |-  .x.  =  ( .s `  W )
lmodvsass.k  |-  K  =  ( Base `  F
)
lmodvsass.t  |-  .X.  =  ( .r `  F )
Assertion
Ref Expression
lmodvsass  |-  ( ( W  e.  LMod  /\  ( Q  e.  K  /\  R  e.  K  /\  X  e.  V )
)  ->  ( ( Q  .X.  R )  .x.  X )  =  ( Q  .x.  ( R 
.x.  X ) ) )

Proof of Theorem lmodvsass
StepHypRef Expression
1 lmodvsass.v . . . . . . . 8  |-  V  =  ( Base `  W
)
2 eqid 2467 . . . . . . . 8  |-  ( +g  `  W )  =  ( +g  `  W )
3 lmodvsass.s . . . . . . . 8  |-  .x.  =  ( .s `  W )
4 lmodvsass.f . . . . . . . 8  |-  F  =  (Scalar `  W )
5 lmodvsass.k . . . . . . . 8  |-  K  =  ( Base `  F
)
6 eqid 2467 . . . . . . . 8  |-  ( +g  `  F )  =  ( +g  `  F )
7 lmodvsass.t . . . . . . . 8  |-  .X.  =  ( .r `  F )
8 eqid 2467 . . . . . . . 8  |-  ( 1r
`  F )  =  ( 1r `  F
)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 17329 . . . . . . 7  |-  ( ( W  e.  LMod  /\  ( Q  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
) )  /\  (
( Q ( +g  `  F ) R ) 
.x.  X )  =  ( ( Q  .x.  X ) ( +g  `  W ) ( R 
.x.  X ) ) )  /\  ( ( ( Q  .X.  R
)  .x.  X )  =  ( Q  .x.  ( R  .x.  X ) )  /\  ( ( 1r `  F ) 
.x.  X )  =  X ) ) )
109simprd 463 . . . . . 6  |-  ( ( W  e.  LMod  /\  ( Q  e.  K  /\  R  e.  K )  /\  ( X  e.  V  /\  X  e.  V
) )  ->  (
( ( Q  .X.  R )  .x.  X
)  =  ( Q 
.x.  ( R  .x.  X ) )  /\  ( ( 1r `  F )  .x.  X
)  =  X ) )
1110simpld 459 . . . . 5  |-  ( ( W  e.  LMod  /\  ( Q  e.  K  /\  R  e.  K )  /\  ( X  e.  V  /\  X  e.  V
) )  ->  (
( Q  .X.  R
)  .x.  X )  =  ( Q  .x.  ( R  .x.  X ) ) )
12113expa 1196 . . . 4  |-  ( ( ( W  e.  LMod  /\  ( Q  e.  K  /\  R  e.  K
) )  /\  ( X  e.  V  /\  X  e.  V )
)  ->  ( ( Q  .X.  R )  .x.  X )  =  ( Q  .x.  ( R 
.x.  X ) ) )
1312anabsan2 820 . . 3  |-  ( ( ( W  e.  LMod  /\  ( Q  e.  K  /\  R  e.  K
) )  /\  X  e.  V )  ->  (
( Q  .X.  R
)  .x.  X )  =  ( Q  .x.  ( R  .x.  X ) ) )
1413exp42 611 . 2  |-  ( W  e.  LMod  ->  ( Q  e.  K  ->  ( R  e.  K  ->  ( X  e.  V  -> 
( ( Q  .X.  R )  .x.  X
)  =  ( Q 
.x.  ( R  .x.  X ) ) ) ) ) )
15143imp2 1211 1  |-  ( ( W  e.  LMod  /\  ( Q  e.  K  /\  R  e.  K  /\  X  e.  V )
)  ->  ( ( Q  .X.  R )  .x.  X )  =  ( Q  .x.  ( R 
.x.  X ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   ` cfv 5588  (class class class)co 6285   Basecbs 14493   +g cplusg 14558   .rcmulr 14559  Scalarcsca 14561   .scvsca 14562   1rcur 16967   LModclmod 17324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6288  df-lmod 17326
This theorem is referenced by:  lmodvs0  17358  lmodvsneg  17366  lmodsubvs  17378  lmodsubdi  17379  lmodsubdir  17380  islss3  17417  lss1d  17421  prdslmodd  17427  lmodvsinv  17494  lmhmvsca  17503  lvecvs0or  17566  lssvs0or  17568  lvecinv  17571  lspsnvs  17572  lspfixed  17586  lspsolvlem  17600  lspsolv  17601  assa2ass  17782  asclrhm  17802  assamulgscmlem2  17809  mplmon2mul  17977  frlmup1  18639  smatvscl  18833  matinv  18986  clmvsass  21414  mendlmod  30974  lincscm  32329  ldepsprlem  32371  lincresunit3lem3  32373  lincresunit3lem1  32378  lshpkrlem4  34127  lcdvsass  36621  baerlem3lem1  36721  hgmapmul  36912
  Copyright terms: Public domain W3C validator