df-invr

Description: Define multiplicative inverse. (Contributed by NM, 21-Sep-2011)

		Ref	Expression
	Assertion	df-invr	$⊢ {inv}_{r} = (r \in V ⟼ {inv}_{g} ({mulGrp}_{r} ↾_{𝑠} Unit (r)))$

Step	Hyp	Ref	Expression
0		cinvr	$class {inv}_{r}$
1		vr	$setvar r$
2		cvv	$class V$
3		cminusg	$class {inv}_{g}$
4		cmgp	$class mulGrp$
5	1	cv	$setvar r$
6	5 4	cfv	$class {mulGrp}_{r}$
7		cress	$class ↾_{𝑠}$
8		cui	$class Unit$
9	5 8	cfv	$class Unit (r)$
10	6 9 7	co	$class ({mulGrp}_{r} ↾_{𝑠} Unit (r))$
11	10 3	cfv	$class {inv}_{g} ({mulGrp}_{r} ↾_{𝑠} Unit (r))$
12	1 2 11	cmpt	$class (r \in V ⟼ {inv}_{g} ({mulGrp}_{r} ↾_{𝑠} Unit (r)))$
13	0 12	wceq	$wff {inv}_{r} = (r \in V ⟼ {inv}_{g} ({mulGrp}_{r} ↾_{𝑠} Unit (r)))$

Metamath Proof Explorer