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 ⁡ 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 ⊢ + R = + ringLMod ⁡ R
4 3 a1i ⊢ Base R = Base ringLMod ⁡ R → + R = + 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