MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  assalmod Structured version   Visualization version   GIF version

Theorem assalmod 21794
Description: An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.)
Assertion
Ref Expression
assalmod (𝑊 ∈ AssAlg → 𝑊 ∈ LMod)

Proof of Theorem assalmod
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2728 . . . 4 (Base‘𝑊) = (Base‘𝑊)
2 eqid 2728 . . . 4 (Scalar‘𝑊) = (Scalar‘𝑊)
3 eqid 2728 . . . 4 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
4 eqid 2728 . . . 4 ( ·𝑠𝑊) = ( ·𝑠𝑊)
5 eqid 2728 . . . 4 (.r𝑊) = (.r𝑊)
61, 2, 3, 4, 5isassa 21790 . . 3 (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠𝑊)𝑥)(.r𝑊)𝑦) = (𝑧( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)) ∧ (𝑥(.r𝑊)(𝑧( ·𝑠𝑊)𝑦)) = (𝑧( ·𝑠𝑊)(𝑥(.r𝑊)𝑦)))))
76simplbi 497 . 2 (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
87simpld 494 1 (𝑊 ∈ AssAlg → 𝑊 ∈ LMod)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1534  wcel 2099  wral 3058  cfv 6548  (class class class)co 7420  Basecbs 17180  .rcmulr 17234  Scalarcsca 17236   ·𝑠 cvsca 17237  Ringcrg 20173  LModclmod 20743  AssAlgcasa 21784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-assa 21787
This theorem is referenced by:  assasca  21796  assa2ass  21797  issubassa3  21799  issubassa  21800  assapropd  21805  aspval  21806  asplss  21807  ascldimul  21821  asclrhm  21823  rnascl  21824  issubassa2  21825  aspval2  21831  assamulgscmlem1  21832  assamulgscmlem2  21833  asclmulg  21835  mplmon2mul  22013  mplind  22014  matinv  22592  assaascl0  47448  assaascl1  47449
  Copyright terms: Public domain W3C validator