Theorem nmmul

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

	Ref	Expression
Hypotheses	nmmul.x	$$⊢X={\mathrm{Base}}_R$$
	nmmul.n	$$⊢N=\mathrm{norm}\left(R\right)$$
	nmmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	nmmul	$$⊢\left(R\in \mathrm{NrmRing}\wedge A\in X\wedge B\in X\right)\to N\left(A\underset{\dot{}}{·}B\right)=N\left(A\right)N\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmmul.x	$$⊢X={\mathrm{Base}}_R$$
2		nmmul.n	$$⊢N=\mathrm{norm}\left(R\right)$$
3		nmmul.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		eqid	$$⊢\mathrm{AbsVal}\left(R\right)=\mathrm{AbsVal}\left(R\right)$$
5	2 4	nrgabv	$$⊢R\in \mathrm{NrmRing}\to N\in \mathrm{AbsVal}\left(R\right)$$
6	4 1 3	abvmul	$$⊢\left(N\in \mathrm{AbsVal}\left(R\right)\wedge A\in X\wedge B\in X\right)\to N\left(A\underset{\dot{}}{·}B\right)=N\left(A\right)N\left(B\right)$$
7	5 6	syl3an1	$$⊢\left(R\in \mathrm{NrmRing}\wedge A\in X\wedge B\in X\right)\to N\left(A\underset{\dot{}}{·}B\right)=N\left(A\right)N\left(B\right)$$