This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-nrg

Description: A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion df-nrg NrmRing = { 𝑤 ∈ NrmGrp ∣ ( norm ‘ 𝑤 ) ∈ ( AbsVal ‘ 𝑤 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnrg ⊢ NrmRing
1 vw ⊢ 𝑤
2 cngp ⊢ NrmGrp
3 cnm ⊢ norm
4 1 cv ⊢ 𝑤
5 4 3 cfv ⊢ ( norm ‘ 𝑤 )
6 cabv ⊢ AbsVal
7 4 6 cfv ⊢ ( AbsVal ‘ 𝑤 )
8 5 7 wcel ⊢ ( norm ‘ 𝑤 ) ∈ ( AbsVal ‘ 𝑤 )
9 8 1 2 crab ⊢ { 𝑤 ∈ NrmGrp ∣ ( norm ‘ 𝑤 ) ∈ ( AbsVal ‘ 𝑤 ) }
10 0 9 wceq ⊢ NrmRing = { 𝑤 ∈ NrmGrp ∣ ( norm ‘ 𝑤 ) ∈ ( AbsVal ‘ 𝑤 ) }