Definition df-dvr

Description: Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014)

	Ref	Expression
Assertion	df-dvr	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. ( Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdvr	|- /r
1		vr	|- r
2		cvv	|- _V
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- r
6	5 4	cfv	|- ( Base ` r )
7		vy	|- y
8		cui	|- Unit
9	5 8	cfv	|- ( Unit ` r )
10	3	cv	|- x
11		cmulr	|- .r
12	5 11	cfv	|- ( .r ` r )
13		cinvr	|- invr
14	5 13	cfv	|- ( invr ` r )
15	7	cv	|- y
16	15 14	cfv	|- ( ( invr ` r ) ` y )
17	10 16 12	co	|- ( x ( .r ` r ) ( ( invr ` r ) ` y ) )
18	3 7 6 9 17	cmpo	|- ( x e. ( Base ` r ) , y e. ( Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) )
19	1 2 18	cmpt	|- ( r e. _V |-> ( x e. ( Base ` r ) , y e. ( Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
20	0 19	wceq	|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. ( Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )