Metamath Proof Explorer


Theorem rlmnm

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

Ref Expression
Assertion rlmnm normR=normringLModR

Proof

Step Hyp Ref Expression
1 rlmbas BaseR=BaseringLModR
2 id BaseR=BaseringLModRBaseR=BaseringLModR
3 rlmplusg +R=+ringLModR
4 3 a1i BaseR=BaseringLModR+R=+ringLModR
5 rlmds distR=distringLModR
6 5 a1i BaseR=BaseringLModRdistR=distringLModR
7 2 4 6 nmpropd BaseR=BaseringLModRnormR=normringLModR
8 1 7 ax-mp normR=normringLModR