Theorem rlmassa

Description: The ring module over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Assertion	rlmassa	|- ( R e. CRing -> ( ringLMod ` R ) e. AssAlg )

Proof

Step	Hyp	Ref	Expression
1		crngring	|- ( R e. CRing -> R e. Ring )
2		eqid	|- ( Base ` R ) = ( Base ` R )
3	2	subrgid	|- ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
4	1 3	syl	|- ( R e. CRing -> ( Base ` R ) e. ( SubRing ` R ) )
5		rlmval	|- ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
6	5	sraassa	|- ( ( R e. CRing /\ ( Base ` R ) e. ( SubRing ` R ) ) -> ( ringLMod ` R ) e. AssAlg )
7	4 6	mpdan	|- ( R e. CRing -> ( ringLMod ` R ) e. AssAlg )