Definition df-invr

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

	Ref	Expression
Assertion	df-invr	$$⊢{inv}_r=\left(r\in \mathrm{V}⟼{inv}_g\left({\mathrm{mulGrp}}_r{\upharpoonright }_{𝑠}\mathrm{Unit}\left(r\right)\right)\right)$$

Detailed syntax breakdown

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