Theorem assalmod 21795

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.

Step	Hyp	Ref	Expression
1		eqid 2731	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2731	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
3		eqid 2731	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
4		eqid 2731	. . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
5		eqid 2731	. . . 4 ⊢ (.r‘𝑊) = (.r‘𝑊)
6	1, 2, 3, 4, 5	isassa 21791	. . 3 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑧( ·𝑠 ‘𝑊)𝑦)) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))))
7	6	simplbi 497	. 2 ⊢ (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
8	7	simpld 494	1 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ‘cfv 6481  (class class class)co 7346  Basecbs 17117  ._rcmulr 17159  Scalarcsca 17161   ·_𝑠 cvsca 17162  Ringcrg 20149  LModclmod 20791  AssAlgcasa 21785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-assa 21788

This theorem is referenced by:  assasca  21797  assa2ass  21798  assa2ass2  21799  issubassa3  21801  issubassa  21802  assapropd  21807  aspval  21808  asplss  21809  ascldimul  21823  asclrhm  21825  rnascl  21826  issubassa2  21827  aspval2  21833  assamulgscmlem1  21834  assamulgscmlem2  21835  asclmulg  21837  mplmon2mul  22002  mplind  22003  matinv  22590  lactlmhm  33642  assalactf1o  33643  assaascl0  48411  assaascl1  48412  asclelbas  49036  asclelbasALT  49037