Metamath Proof Explorer


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 ∧ 𝑁𝐴 ) )