Theorem nm1

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

	Ref	Expression
Hypotheses	nm1.n	⊢ 𝑁 = ( norm ‘ 𝑅 )
	nm1.u	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	nm1	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) → ( 𝑁 ‘ 1 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		nm1.n	⊢ 𝑁 = ( norm ‘ 𝑅 )
2		nm1.u	⊢ 1 = ( 1r ‘ 𝑅 )
3		eqid	⊢ ( AbsVal ‘ 𝑅 ) = ( AbsVal ‘ 𝑅 )
4	1 3	nrgabv	⊢ ( 𝑅 ∈ NrmRing → 𝑁 ∈ ( AbsVal ‘ 𝑅 ) )
5		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6	2 5	nzrnz	⊢ ( 𝑅 ∈ NzRing → 1 ≠ ( 0g ‘ 𝑅 ) )
7	3 2 5	abv1z	⊢ ( ( 𝑁 ∈ ( AbsVal ‘ 𝑅 ) ∧ 1 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑁 ‘ 1 ) = 1 )
8	4 6 7	syl2an	⊢ ( ( 𝑅 ∈ NrmRing ∧ 𝑅 ∈ NzRing ) → ( 𝑁 ‘ 1 ) = 1 )