Theorem assalmod 21991

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  Ringcrg 20316  LModclmod 20962  AssAlgcasa 21981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-assa 21984

This theorem is referenced by:  assasca  21993  assa2ass  21994  assa2ass2  21995  issubassa3  21997  issubassa  21998  assapropd  22002  aspval  22003  asplss  22004  asclelbas  22014  ascldimul  22019  asclrhm  22021  rnascl  22022  issubassa2  22023  aspval2  22029  assamulgscmlem1  22030  assamulgscmlem2  22031  asclmulg  22033  mplmon2mul  22201  mplind  22202  matinv  22815  lactlmhm  34005  assalactf1o  34006  assaascl0  49144  assaascl1  49145  asclelbasALT  49767