Metamath Proof Explorer


Theorem assalmod

Description: An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014)

Ref Expression
Assertion assalmod WAssAlgWLMod

Proof

Step Hyp Ref Expression
1 eqid BaseW=BaseW
2 eqid ScalarW=ScalarW
3 eqid BaseScalarW=BaseScalarW
4 eqid W=W
5 eqid W=W
6 1 2 3 4 5 isassa WAssAlgWLModWRingScalarWCRingzBaseScalarWxBaseWyBaseWzWxWy=zWxWyxWzWy=zWxWy
7 6 simplbi WAssAlgWLModWRingScalarWCRing
8 7 simp1d WAssAlgWLMod