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	⊢ ( 𝑅 ∈ CRing → ( ringLMod ‘ 𝑅 ) ∈ AssAlg )

Proof

Step	Hyp	Ref	Expression
1		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
2		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3	2	subrgid	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
4	1 3	syl	⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
5		rlmval	⊢ ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
6	5	sraassa	⊢ ( ( 𝑅 ∈ CRing ∧ ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) ) → ( ringLMod ‘ 𝑅 ) ∈ AssAlg )
7	4 6	mpdan	⊢ ( 𝑅 ∈ CRing → ( ringLMod ‘ 𝑅 ) ∈ AssAlg )