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 = \{w \in NrmGrp \| norm (w) \in AbsVal (w)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnrg	$class NrmRing$
1		vw	$setvar w$
2		cngp	$class NrmGrp$
3		cnm	$class norm$
4	1	cv	$setvar w$
5	4 3	cfv	$class norm (w)$
6		cabv	$class AbsVal$
7	4 6	cfv	$class AbsVal (w)$
8	5 7	wcel	$wff norm (w) \in AbsVal (w)$
9	8 1 2	crab	$class \{w \in NrmGrp \| norm (w) \in AbsVal (w)\}$
10	0 9	wceq	$wff NrmRing = \{w \in NrmGrp \| norm (w) \in AbsVal (w)\}$