rlmlmod

Description: The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014)

		Ref	Expression
	Assertion	rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$

Step	Hyp	Ref	Expression
1		rlmval	$⊢ ringLMod (R) = subringAlg (R) ({Base}_{R})$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	2	subrgid	$⊢ R \in Ring \to {Base}_{R} \in SubRing (R)$
4		eqid	$⊢ subringAlg (R) ({Base}_{R}) = subringAlg (R) ({Base}_{R})$
5	4	sralmod	$⊢ {Base}_{R} \in SubRing (R) \to subringAlg (R) ({Base}_{R}) \in LMod$
6	3 5	syl	$⊢ R \in Ring \to subringAlg (R) ({Base}_{R}) \in LMod$
7	1 6	eqeltrid	$⊢ R \in Ring \to ringLMod (R) \in LMod$

Metamath Proof Explorer