Theorem nm1

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

	Ref	Expression
Hypotheses	nm1.n	$$⊢N=\mathrm{norm}\left(R\right)$$
	nm1.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	nm1	$$⊢\left(R\in \mathrm{NrmRing}\wedge R\in \mathrm{NzRing}\right)\to N\left(\underset{\dot{}}{1}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		nm1.n	$$⊢N=\mathrm{norm}\left(R\right)$$
2		nm1.u	$$⊢\underset{\dot{}}{1}=1_R$$
3		eqid	$$⊢\mathrm{AbsVal}\left(R\right)=\mathrm{AbsVal}\left(R\right)$$
4	1 3	nrgabv	$$⊢R\in \mathrm{NrmRing}\to N\in \mathrm{AbsVal}\left(R\right)$$
5		eqid	$$⊢0_R=0_R$$
6	2 5	nzrnz	$$⊢R\in \mathrm{NzRing}\to \underset{\dot{}}{1}\ne 0_R$$
7	3 2 5	abv1z	$$⊢\left(N\in \mathrm{AbsVal}\left(R\right)\wedge \underset{\dot{}}{1}\ne 0_R\right)\to N\left(\underset{\dot{}}{1}\right)=1$$
8	4 6 7	syl2an	$$⊢\left(R\in \mathrm{NrmRing}\wedge R\in \mathrm{NzRing}\right)\to N\left(\underset{\dot{}}{1}\right)=1$$