Theorem rlmnm

Description: The norm function in the ring module. (Contributed by AV, 9-Oct-2021)

	Ref	Expression
Assertion	rlmnm	⊢ ( norm ‘ 𝑅 ) = ( norm ‘ ( ringLMod ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rlmbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
2		id	⊢ ( ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) )
3		rlmplusg	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
4	3	a1i	⊢ ( ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) ) )
5		rlmds	⊢ ( dist ‘ 𝑅 ) = ( dist ‘ ( ringLMod ‘ 𝑅 ) )
6	5	a1i	⊢ ( ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) → ( dist ‘ 𝑅 ) = ( dist ‘ ( ringLMod ‘ 𝑅 ) ) )
7	2 4 6	nmpropd	⊢ ( ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) → ( norm ‘ 𝑅 ) = ( norm ‘ ( ringLMod ‘ 𝑅 ) ) )
8	1 7	ax-mp	⊢ ( norm ‘ 𝑅 ) = ( norm ‘ ( ringLMod ‘ 𝑅 ) )