Definition df-dvdsr 17807

Description: Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through ( ||_r ` (opp<sub>r</sub> ` R ) ). (Contributed by Mario Carneiro, 1-Dec-2014.)

Assertion

Ref	Expression
df-dvdsr	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )

Distinct variable group:   x, w, y, z

Detailed syntax breakdown of Definition df-dvdsr

Step	Hyp	Ref	Expression
1		cdsr 17804	. 2 class ||r
2		vw	. . 3 setvar w
3		cvv 3017	. . 3 class _V
4		vx	. . . . . . 7 setvar x
5	4	cv 1436	. . . . . 6 class x
6	2	cv 1436	. . . . . . 7 class w
7		cbs 15059	. . . . . . 7 class Base
8	6, 7	cfv 5539	. . . . . 6 class ( Base ` w )
9	5, 8	wcel 1872	. . . . 5 wff x e. ( Base ` w )
10		vz	. . . . . . . . 9 setvar z
11	10	cv 1436	. . . . . . . 8 class z
12		cmulr 15129	. . . . . . . . 9 class .r
13	6, 12	cfv 5539	. . . . . . . 8 class ( .r ` w )
14	11, 5, 13	co 6244	. . . . . . 7 class ( z ( .r ` w ) x )
15		vy	. . . . . . . 8 setvar y
16	15	cv 1436	. . . . . . 7 class y
17	14, 16	wceq 1437	. . . . . 6 wff ( z ( .r ` w ) x ) = y
18	17, 10, 8	wrex 2710	. . . . 5 wff E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y
19	9, 18	wa 370	. . . 4 wff ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y )
20	19, 4, 15	copab 4419	. . 3 class { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) }
21	2, 3, 20	cmpt 4420	. 2 class ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
22	1, 21	wceq 1437	1 wff ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )

This definition is referenced by:  reldvdsr  17810  dvdsrval  17811