Definition df-dvdsr

Description: Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through ( ||r( oppRR ) ) . (Contributed by Mario Carneiro, 1-Dec-2014)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdsr	|- ||r
1		vw	|- w
2		cvv	|- _V
3		vx	|- x
4		vy	|- y
5	3	cv	|- x
6		cbs	|- Base
7	1	cv	|- w
8	7 6	cfv	|- ( Base ` w )
9	5 8	wcel	|- x e. ( Base ` w )
10		vz	|- z
11	10	cv	|- z
12		cmulr	|- .r
13	7 12	cfv	|- ( .r ` w )
14	11 5 13	co	|- ( z ( .r ` w ) x )
15	4	cv	|- y
16	14 15	wceq	|- ( z ( .r ` w ) x ) = y
17	16 10 8	wrex	|- E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y
18	9 17	wa	|- ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y )
19	18 3 4	copab	|- { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) }
20	1 2 19	cmpt	|- ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
21	0 20	wceq	|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )