This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑅 ) )