Definition df-invr

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

	Ref	Expression
Assertion	df-invr	|- invr = ( r e. _V |-> ( invg ` ( ( mulGrp ` r ) |`s ( Unit ` r ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinvr	|- invr
1		vr	|- r
2		cvv	|- _V
3		cminusg	|- invg
4		cmgp	|- mulGrp
5	1	cv	|- r
6	5 4	cfv	|- ( mulGrp ` r )
7		cress	|- |`s
8		cui	|- Unit
9	5 8	cfv	|- ( Unit ` r )
10	6 9 7	co	|- ( ( mulGrp ` r ) |`s ( Unit ` r ) )
11	10 3	cfv	|- ( invg ` ( ( mulGrp ` r ) |`s ( Unit ` r ) ) )
12	1 2 11	cmpt	|- ( r e. _V |-> ( invg ` ( ( mulGrp ` r ) |`s ( Unit ` r ) ) ) )
13	0 12	wceq	|- invr = ( r e. _V |-> ( invg ` ( ( mulGrp ` r ) |`s ( Unit ` r ) ) ) )