Metamath Proof Explorer


Theorem assalmod

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

Ref Expression
Assertion assalmod W AssAlg W LMod

Proof

Step Hyp Ref Expression
1 eqid Base W = Base W
2 eqid Scalar W = Scalar W
3 eqid Base Scalar W = Base Scalar W
4 eqid W = W
5 eqid W = W
6 1 2 3 4 5 isassa W AssAlg W LMod W Ring Scalar W CRing z Base Scalar W x Base W y Base W z W x W y = z W x W y x W z W y = z W x W y
7 6 simplbi W AssAlg W LMod W Ring Scalar W CRing
8 7 simp1d W AssAlg W LMod