Theorem rlmnvc

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

	Ref	Expression
Assertion	rlmnvc	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → ( ringLMod ‘ 𝑅 ) ∈ NrmVec )

Proof

Step	Hyp	Ref	Expression
1		rlmnlm	⊢ ( 𝑅 ∈ NrmRing → ( ringLMod ‘ 𝑅 ) ∈ NrmMod )
2		rlmlvec	⊢ ( 𝑅 ∈ DivRing → ( ringLMod ‘ 𝑅 ) ∈ LVec )
3		isnvc	⊢ ( ( ringLMod ‘ 𝑅 ) ∈ NrmVec ↔ ( ( ringLMod ‘ 𝑅 ) ∈ NrmMod ∧ ( ringLMod ‘ 𝑅 ) ∈ LVec ) )
4	3	biimpri	⊢ ( ( ( ringLMod ‘ 𝑅 ) ∈ NrmMod ∧ ( ringLMod ‘ 𝑅 ) ∈ LVec ) → ( ringLMod ‘ 𝑅 ) ∈ NrmVec )
5	1 2 4	syl2an	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ) → ( ringLMod ‘ 𝑅 ) ∈ NrmVec )