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

Theorem lmodvsass 18051
Description: Associative law for scalar product. (ax-hvmulass 26495 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 2429 . . . . . . . 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 2429 . . . . . . . 8  |-  ( +g  `  F )  =  ( +g  `  F )
7 lmodvsass.t . . . . . . . 8  |-  .X.  =  ( .r `  F )
8 eqid 2429 . . . . . . . 8  |-  ( 1r
`  F )  =  ( 1r `  F
)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 18031 . . . . . . 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 464 . . . . . 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 460 . . . . 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 1205 . . . 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 829 . . 3  |-  ( ( ( W  e.  LMod  /\  ( Q  e.  K  /\  R  e.  K
) )  /\  X  e.  V )  ->  (
( Q  .X.  R
)  .x.  X )  =  ( Q  .x.  ( R  .x.  X ) ) )
1413exp42 614 . 2  |-  ( W  e.  LMod  ->  ( Q  e.  K  ->  ( R  e.  K  ->  ( X  e.  V  -> 
( ( Q  .X.  R )  .x.  X
)  =  ( Q 
.x.  ( R  .x.  X ) ) ) ) ) )
15143imp2 1220 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 370    /\ w3a 982    = wceq 1437    e. wcel 1870   ` cfv 5601  (class class class)co 6305   Basecbs 15084   +g cplusg 15152   .rcmulr 15153  Scalarcsca 15155   .scvsca 15156   1rcur 17670   LModclmod 18026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308  df-lmod 18028
This theorem is referenced by:  lmodvs0  18060  lmodvsneg  18067  lmodsubvs  18079  lmodsubdi  18080  lmodsubdir  18081  islss3  18117  lss1d  18121  prdslmodd  18127  lmodvsinv  18194  lmhmvsca  18203  lvecvs0or  18266  lssvs0or  18268  lvecinv  18271  lspsnvs  18272  lspfixed  18286  lspsolvlem  18300  lspsolv  18301  assa2ass  18481  asclrhm  18501  assamulgscmlem2  18508  mplmon2mul  18659  frlmup1  19287  smatvscl  19480  matinv  19633  clmvsass  22011  lshpkrlem4  32388  lcdvsass  34884  baerlem3lem1  34984  hgmapmul  35175  mendlmod  35758  lincscm  38992  ldepsprlem  39034  lincresunit3lem3  39036  lincresunit3lem1  39041
  Copyright terms: Public domain W3C validator