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

Metamath Proof Explorer

Definition df-drng

Description: Define class of all division rings. A division ring is a ring in which the set of units is exactly the nonzero elements of the ring. (Contributed by NM, 18-Oct-2012)

		Ref	Expression
	Assertion	df-drng	$⊢ DivRing = \{r \in Ring \| Unit (r) = {Base}_{r} ∖ \{0_{r}\}\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdr	$class DivRing$
1		vr	$setvar r$
2		crg	$class Ring$
3		cui	$class Unit$
4	1	cv	$setvar r$
5	4 3	cfv	$class Unit (r)$
6		cbs	$class Base$
7	4 6	cfv	$class {Base}_{r}$
8		c0g	$class 0_{𝑔}$
9	4 8	cfv	$class 0_{r}$
10	9	csn	$class \{0_{r}\}$
11	7 10	cdif	$class ({Base}_{r} ∖ \{0_{r}\})$
12	5 11	wceq	$wff Unit (r) = {Base}_{r} ∖ \{0_{r}\}$
13	12 1 2	crab	$class \{r \in Ring \| Unit (r) = {Base}_{r} ∖ \{0_{r}\}\}$
14	0 13	wceq	$wff DivRing = \{r \in Ring \| Unit (r) = {Base}_{r} ∖ \{0_{r}\}\}$