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	$$⊢{\parallel }_r=\left(w\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(x\in {\mathrm{Base}}_w\wedge \exists z\in {\mathrm{Base}}_{w}z{\cdot }_{w}x=y\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdsr	$$class{\parallel }_r$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		vy	$$setvary$$
5	3	cv	$$setvarx$$
6		cbs	$$class\mathrm{Base}$$
7	1	cv	$$setvarw$$
8	7 6	cfv	$$class{\mathrm{Base}}_w$$
9	5 8	wcel	$$wffx\in {\mathrm{Base}}_w$$
10		vz	$$setvarz$$
11	10	cv	$$setvarz$$
12		cmulr	$$class{\cdot }_{𝑟}$$
13	7 12	cfv	$$class{\cdot }_w$$
14	11 5 13	co	$$class\left(z{\cdot }_{w}x\right)$$
15	4	cv	$$setvary$$
16	14 15	wceq	$$wffz{\cdot }_{w}x=y$$
17	16 10 8	wrex	$$wff\exists z\in {\mathrm{Base}}_{w}z{\cdot }_{w}x=y$$
18	9 17	wa	$$wff\left(x\in {\mathrm{Base}}_w\wedge \exists z\in {\mathrm{Base}}_{w}z{\cdot }_{w}x=y\right)$$
19	18 3 4	copab	$$class\left\{⟨x,y⟩|\left(x\in {\mathrm{Base}}_w\wedge \exists z\in {\mathrm{Base}}_{w}z{\cdot }_{w}x=y\right)\right\}$$
20	1 2 19	cmpt	$$class\left(w\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(x\in {\mathrm{Base}}_w\wedge \exists z\in {\mathrm{Base}}_{w}z{\cdot }_{w}x=y\right)\right\}\right)$$
21	0 20	wceq	$$wff{\parallel }_r=\left(w\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(x\in {\mathrm{Base}}_w\wedge \exists z\in {\mathrm{Base}}_{w}z{\cdot }_{w}x=y\right)\right\}\right)$$