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 \in CRing \to ringLMod (R) \in AssAlg$

Step	Hyp	Ref	Expression
1		crngring	$⊢ R \in CRing \to R \in Ring$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	2	subrgid	$⊢ R \in Ring \to {Base}_{R} \in SubRing (R)$
4	1 3	syl	$⊢ R \in CRing \to {Base}_{R} \in SubRing (R)$
5		rlmval	$⊢ ringLMod (R) = subringAlg (R) ({Base}_{R})$
6	5	sraassa	$⊢ (R \in CRing \land {Base}_{R} \in SubRing (R)) \to ringLMod (R) \in AssAlg$
7	4 6	mpdan	$⊢ R \in CRing \to ringLMod (R) \in AssAlg$

Metamath Proof Explorer