Metamath Proof Explorer

Theorem rlmnm

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

Ref Expression
Assertion rlmnm 
|- ( norm ` R ) = ( norm ` ( ringLMod ` R ) )

Proof

Step Hyp Ref Expression
1 rlmbas 
 |-  ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
2 id 
 |-  ( ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) -> ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) )
3 rlmplusg 
 |-  ( +g ` R ) = ( +g ` ( ringLMod ` R ) )
4 3 a1i 
 |-  ( ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) -> ( +g ` R ) = ( +g ` ( ringLMod ` R ) ) )
5 rlmds 
 |-  ( dist ` R ) = ( dist ` ( ringLMod ` R ) )
6 5 a1i 
 |-  ( ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) -> ( dist ` R ) = ( dist ` ( ringLMod ` R ) ) )
7 2 4 6 nmpropd 
 |-  ( ( Base ` R ) = ( Base ` ( ringLMod ` R ) ) -> ( norm ` R ) = ( norm ` ( ringLMod ` R ) ) )
8 1 7 ax-mp 
 |-  ( norm ` R ) = ( norm ` ( ringLMod ` R ) )