Theorem isnrg

Description: A normed ring is a ring with a norm that makes it into a normed group, and such that the norm is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	isnrg.1	⊢ 𝑁 = ( norm ‘ 𝑅 )
	isnrg.2	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
Assertion	isnrg	⊢ ( 𝑅 ∈ NrmRing ↔ ( 𝑅 ∈ NrmGrp ∧ 𝑁 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isnrg.1	⊢ 𝑁 = ( norm ‘ 𝑅 )
2		isnrg.2	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
3		fveq2	⊢ ( 𝑟 = 𝑅 → ( norm ‘ 𝑟 ) = ( norm ‘ 𝑅 ) )
4	3 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( norm ‘ 𝑟 ) = 𝑁 )
5		fveq2	⊢ ( 𝑟 = 𝑅 → ( AbsVal ‘ 𝑟 ) = ( AbsVal ‘ 𝑅 ) )
6	5 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( AbsVal ‘ 𝑟 ) = 𝐴 )
7	4 6	eleq12d	⊢ ( 𝑟 = 𝑅 → ( ( norm ‘ 𝑟 ) ∈ ( AbsVal ‘ 𝑟 ) ↔ 𝑁 ∈ 𝐴 ) )
8		df-nrg	⊢ NrmRing = { 𝑟 ∈ NrmGrp ∣ ( norm ‘ 𝑟 ) ∈ ( AbsVal ‘ 𝑟 ) }
9	7 8	elrab2	⊢ ( 𝑅 ∈ NrmRing ↔ ( 𝑅 ∈ NrmGrp ∧ 𝑁 ∈ 𝐴 ) )