unitnmn0

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

	Ref	Expression
Hypotheses	nminvr.n	$⊢ N = norm (R)$
	nminvr.u	$⊢ U = Unit (R)$
Assertion	unitnmn0	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (A) \neq 0$

Step	Hyp	Ref	Expression
1		nminvr.n	$⊢ N = norm (R)$
2		nminvr.u	$⊢ U = Unit (R)$
3		nrgngp	$⊢ R \in NrmRing \to R \in NrmGrp$
4	3	3ad2ant1	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to R \in NrmGrp$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	5 2	unitcl	$⊢ A \in U \to A \in {Base}_{R}$
7	6	3ad2ant3	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to A \in {Base}_{R}$
8		eqid	$⊢ 0_{R} = 0_{R}$
9	2 8	nzrunit	$⊢ (R \in NzRing \land A \in U) \to A \neq 0_{R}$
10	9	3adant1	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to A \neq 0_{R}$
11	5 1 8	nmne0	$⊢ (R \in NrmGrp \land A \in {Base}_{R} \land A \neq 0_{R}) \to N (A) \neq 0$
12	4 7 10 11	syl3anc	$⊢ (R \in NrmRing \land R \in NzRing \land A \in U) \to N (A) \neq 0$

Metamath Proof Explorer