This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {Base}_{R}$
	nmmul.n	$⊢ N = norm (R)$
	nmmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	nmmul	$⊢ (R \in NrmRing \land A \in X \land B \in X) \to N (A \underset{˙}{\cdot} B) = N (A) N (B)$

Step	Hyp	Ref	Expression
1		nmmul.x	$⊢ X = {Base}_{R}$
2		nmmul.n	$⊢ N = norm (R)$
3		nmmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		eqid	$⊢ AbsVal (R) = AbsVal (R)$
5	2 4	nrgabv	$⊢ R \in NrmRing \to N \in AbsVal (R)$
6	4 1 3	abvmul	$⊢ (N \in AbsVal (R) \land A \in X \land B \in X) \to N (A \underset{˙}{\cdot} B) = N (A) N (B)$
7	5 6	syl3an1	$⊢ (R \in NrmRing \land A \in X \land B \in X) \to N (A \underset{˙}{\cdot} B) = N (A) N (B)$