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 = ( norm ` R )
	nm1.u	|- .1. = ( 1r ` R )
Assertion	nm1	|- ( ( R e. NrmRing /\ R e. NzRing ) -> ( N ` .1. ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		nm1.n	|- N = ( norm ` R )
2		nm1.u	|- .1. = ( 1r ` R )
3		eqid	|- ( AbsVal ` R ) = ( AbsVal ` R )
4	1 3	nrgabv	|- ( R e. NrmRing -> N e. ( AbsVal ` R ) )
5		eqid	|- ( 0g ` R ) = ( 0g ` R )
6	2 5	nzrnz	|- ( R e. NzRing -> .1. =/= ( 0g ` R ) )
7	3 2 5	abv1z	|- ( ( N e. ( AbsVal ` R ) /\ .1. =/= ( 0g ` R ) ) -> ( N ` .1. ) = 1 )
8	4 6 7	syl2an	|- ( ( R e. NrmRing /\ R e. NzRing ) -> ( N ` .1. ) = 1 )