Metamath Proof Explorer

Definition df-unit

Description: Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014)

		Ref	Expression
	Assertion	df-unit	$⊢ Unit = (w \in V ⟼ {(∥_{r} (w) \cap ∥_{r} ({opp}_{r} (w)))}^{-1} [\{1_{w}\}])$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cui	$class Unit$
1		vw	$setvar w$
2		cvv	$class V$
3		cdsr	$class ∥_{r}$
4	1	cv	$setvar w$
5	4 3	cfv	$class ∥_{r} (w)$
6		coppr	$class {opp}_{r}$
7	4 6	cfv	$class {opp}_{r} (w)$
8	7 3	cfv	$class ∥_{r} ({opp}_{r} (w))$
9	5 8	cin	$class (∥_{r} (w) \cap ∥_{r} ({opp}_{r} (w)))$
10	9	ccnv	$class {(∥_{r} (w) \cap ∥_{r} ({opp}_{r} (w)))}^{-1}$
11		cur	$class 1_{r}$
12	4 11	cfv	$class 1_{w}$
13	12	csn	$class \{1_{w}\}$
14	10 13	cima	$class {(∥_{r} (w) \cap ∥_{r} ({opp}_{r} (w)))}^{-1} [\{1_{w}\}]$
15	1 2 14	cmpt	$class (w \in V ⟼ {(∥_{r} (w) \cap ∥_{r} ({opp}_{r} (w)))}^{-1} [\{1_{w}\}])$
16	0 15	wceq	$wff Unit = (w \in V ⟼ {(∥_{r} (w) \cap ∥_{r} ({opp}_{r} (w)))}^{-1} [\{1_{w}\}])$