Definition df-invr

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

	Ref	Expression
Assertion	df-invr	⊢ invr = ( 𝑟 ∈ V ↦ ( invg ‘ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinvr	⊢ invr
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		cminusg	⊢ invg
4		cmgp	⊢ mulGrp
5	1	cv	⊢ 𝑟
6	5 4	cfv	⊢ ( mulGrp ‘ 𝑟 )
7		cress	⊢ ↾s
8		cui	⊢ Unit
9	5 8	cfv	⊢ ( Unit ‘ 𝑟 )
10	6 9 7	co	⊢ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) )
11	10 3	cfv	⊢ ( invg ‘ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) )
12	1 2 11	cmpt	⊢ ( 𝑟 ∈ V ↦ ( invg ‘ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ) )
13	0 12	wceq	⊢ invr = ( 𝑟 ∈ V ↦ ( invg ‘ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ) )