Theorem rlmlmod

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

	Ref	Expression
Assertion	rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		rlmval	⊢ ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
2		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3	2	subrgid	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
4		eqid	⊢ ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
5	4	sralmod	⊢ ( ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) → ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) ∈ LMod )
6	3 5	syl	⊢ ( 𝑅 ∈ Ring → ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) ∈ LMod )
7	1 6	eqeltrid	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )