Theorem rlmnlm

Description: The ring module over a normed ring is a normed module. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Assertion	rlmnlm	⊢ ( 𝑅 ∈ NrmRing → ( ringLMod ‘ 𝑅 ) ∈ NrmMod )

Proof

Step	Hyp	Ref	Expression
1		nrgring	⊢ ( 𝑅 ∈ NrmRing → 𝑅 ∈ Ring )
2		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3	2	subrgid	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
4	1 3	syl	⊢ ( 𝑅 ∈ NrmRing → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
5		rlmval	⊢ ( ringLMod ‘ 𝑅 ) = ( ( subringAlg ‘ 𝑅 ) ‘ ( Base ‘ 𝑅 ) )
6	5	sranlm	⊢ ( ( 𝑅 ∈ NrmRing ∧ ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) ) → ( ringLMod ‘ 𝑅 ) ∈ NrmMod )
7	4 6	mpdan	⊢ ( 𝑅 ∈ NrmRing → ( ringLMod ‘ 𝑅 ) ∈ NrmMod )