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