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

Theorem lmodvsass 16006
Description: Associative law for scalar product. (ax-hvmulass 22541 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 2442 . . . . . . . 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 2442 . . . . . . . 8  |-  ( +g  `  F )  =  ( +g  `  F )
7 lmodvsass.t . . . . . . . 8  |-  .X.  =  ( .r `  F )
8 eqid 2442 . . . . . . . 8  |-  ( 1r
`  F )  =  ( 1r `  F
)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 15986 . . . . . . 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 451 . . . . . 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 447 . . . . 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 1154 . . . 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 797 . . 3  |-  ( ( ( W  e.  LMod  /\  ( Q  e.  K  /\  R  e.  K
) )  /\  X  e.  V )  ->  (
( Q  .X.  R
)  .x.  X )  =  ( Q  .x.  ( R  .x.  X ) ) )
1413exp42 596 . 2  |-  ( W  e.  LMod  ->  ( Q  e.  K  ->  ( R  e.  K  ->  ( X  e.  V  -> 
( ( Q  .X.  R )  .x.  X
)  =  ( Q 
.x.  ( R  .x.  X ) ) ) ) ) )
15143imp2 1169 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 set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937    = wceq 1653    e. wcel 1727   ` cfv 5483  (class class class)co 6110   Basecbs 13500   +g cplusg 13560   .rcmulr 13561  Scalarcsca 13563   .scvsca 13564   1rcur 15693   LModclmod 15981
This theorem is referenced by:  lmodvs0  16015  lmodvsneg  16019  lmodsubvs  16031  lmodsubdi  16032  lmodsubdir  16033  islss3  16066  lss1d  16070  prdslmodd  16076  lmodvsinv  16143  lmhmvsca  16152  lvecvs0or  16211  lssvs0or  16213  lvecinv  16216  lspsnvs  16217  lspfixed  16231  lspsolvlem  16245  lspsolv  16246  asclrhm  16431  mplmon2mul  16592  clmvsass  19143  frlmup1  27265  mendlmod  27516  lshpkrlem4  30009  lcdvsass  32503  baerlem3lem1  32603  hgmapmul  32794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-nul 4363
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-sbc 3168  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-iota 5447  df-fv 5491  df-ov 6113  df-lmod 15983
  Copyright terms: Public domain W3C validator