Theorem nmmul

Description: The norm of a product in a normed ring. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	nmmul.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
	nmmul.n	⊢ 𝑁 = ( norm ‘ 𝑅 )
	nmmul.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	nmmul	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmmul.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
2		nmmul.n	⊢ 𝑁 = ( norm ‘ 𝑅 )
3		nmmul.t	⊢ · = ( .r ‘ 𝑅 )
4		eqid	⊢ ( AbsVal ‘ 𝑅 ) = ( AbsVal ‘ 𝑅 )
5	2 4	nrgabv	⊢ ( 𝑅 ∈ NrmRing → 𝑁 ∈ ( AbsVal ‘ 𝑅 ) )
6	4 1 3	abvmul	⊢ ( ( 𝑁 ∈ ( AbsVal ‘ 𝑅 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )
7	5 6	syl3an1	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝑁 ‘ 𝐴 ) · ( 𝑁 ‘ 𝐵 ) ) )