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

Theorem lmodvsass 15747
Description: Associative law for scalar product. (ax-hvmulass 21695 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 2358 . . . . . . . 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 2358 . . . . . . . 8  |-  ( +g  `  F )  =  ( +g  `  F )
7 lmodvsass.t . . . . . . . 8  |-  .X.  =  ( .r `  F )
8 eqid 2358 . . . . . . . 8  |-  ( 1r
`  F )  =  ( 1r `  F
)
91, 2, 3, 4, 5, 6, 7, 8lmodlema 15725 . . . . . . 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 449 . . . . . 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 445 . . . . 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 1151 . . . 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 795 . . 3  |-  ( ( ( W  e.  LMod  /\  ( Q  e.  K  /\  R  e.  K
) )  /\  X  e.  V )  ->  (
( Q  .X.  R
)  .x.  X )  =  ( Q  .x.  ( R  .x.  X ) ) )
1413exp42 594 . 2  |-  ( W  e.  LMod  ->  ( Q  e.  K  ->  ( R  e.  K  ->  ( X  e.  V  -> 
( ( Q  .X.  R )  .x.  X
)  =  ( Q 
.x.  ( R  .x.  X ) ) ) ) ) )
15143imp2 1166 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 358    /\ w3a 934    = wceq 1642    e. wcel 1710   ` cfv 5334  (class class class)co 5942   Basecbs 13239   +g cplusg 13299   .rcmulr 13300  Scalarcsca 13302   .scvsca 13303   1rcur 15432   LModclmod 15720
This theorem is referenced by:  lmodvsassOLD  15748  lmodvs0  15757  lmodvsneg  15762  lmodsubvs  15774  lmodsubdi  15775  lmodsubdir  15776  islss3  15809  lss1d  15813  prdslmodd  15819  lmodvsinv  15886  lmhmvsca  15895  lvecvs0or  15954  lssvs0or  15956  lvecinv  15959  lspsnvs  15960  lspfixed  15974  lspsolvlem  15988  lspsolv  15989  asclrhm  16174  mplmon2mul  16335  clmvsass  18683  frlmup1  26573  mendlmod  26824  lshpkrlem4  29355  lcdvsass  31849  baerlem3lem1  31949  hgmapmul  32140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-nul 4228
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-iota 5298  df-fv 5342  df-ov 5945  df-lmod 15722
  Copyright terms: Public domain W3C validator