Theorem assalmod 22081

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 2762	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2762	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
3		eqid 2762	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
4		eqid 2762	. . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
5		eqid 2762	. . . 4 ⊢ (.r‘𝑊) = (.r‘𝑊)
6	1, 2, 3, 4, 5	isassa 22077	. . 3 ⊢ (𝑊 ∈ AssAlg ↔ ((𝑊 ∈ LMod ∧ 𝑊 ∈ Ring) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑊))∀𝑥 ∈ (Base‘𝑊)∀𝑦 ∈ (Base‘𝑊)(((𝑧( ·𝑠 ‘𝑊)𝑥)(.r‘𝑊)𝑦) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)) ∧ (𝑥(.r‘𝑊)(𝑧( ·𝑠 ‘𝑊)𝑦)) = (𝑧( ·𝑠 ‘𝑊)(𝑥(.r‘𝑊)𝑦)))))
7	6	simplbi 502	. 2 ⊢ (𝑊 ∈ AssAlg → (𝑊 ∈ LMod ∧ 𝑊 ∈ Ring))
8	7	simpld 500	1 ⊢ (𝑊 ∈ AssAlg → 𝑊 ∈ LMod)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  ._rcmulr 17349  Scalarcsca 17351   ·_𝑠 cvsca 17352  Ringcrg 20378  LModclmod 21050  AssAlgcasa 22071

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-assa 22074

This theorem is used by:  assasca  22083  assa2ass  22084  assa2ass2  22085  issubassa3  22087  issubassa  22088  assapropd  22092  aspval  22093  asplss  22094  asclelbas  22104  ascldimul  22109  asclrhm  22111  rnascl  22112  issubassa2  22113  aspval2  22119  assamulgscmlem1  22120  assamulgscmlem2  22121  asclmulg  22123  mplmon2mul  22291  mplind  22292  matinv  22905  lactlmhm  34152  assalactf1o  34153  assaascl0  49319  assaascl1  49320  asclelbasALT  49940