On the equivalence relation in a right Ore domain. I'm reading about Ore domains, but am confused about the equivalence relation. 
First, suppose $D$ is a domain, which isn't assumed to be commutative, such that for any nonzero $a,b$, there is a common nonzero right multiple, that is, $ab_1=ba_1\neq 0$. Consider the set $D\times D^\times$, where $D^\times$ is the set of nonzero elements of $D$. That it is defined that $(a,b)\sim (c,d)$ if for $b_1\neq 0$ and $d_1\neq 0$ such that $bd_1=db_1$ we have $ad_1=cb_1$.
What does it mean that this is independent of the choice of $b_1$? Does it mean that for any other pair $b_2,d_2\neq 0$ such that $bd_2=db_2$, then $ad_2=cb_2$ also? If so, why is this true? I've been trying to prove this, but I'm not sure if it's even the correct assumption.
 A: The usual definition for the Ore relation matches yours, except it doesn't say "implies" it says "and": $(a,b)\sim (c,d)$ iff there exists $b',d'\in D$ such that $bb'=dd'\neq 0$ and $ab'=cd'$. (Requiring $b',d'$ to be nonzero turns out to be superfluous.)
So, you can also write the above condition as: $(a,b)\sim(c,d)$ if there exists $b_1,d_1$ such that $(ab_1,bb_1)=(cd_1,dd_1)$.
Maybe something about right Ore domains makes the two conditions equivalent, but I find this one easier to think about.
I'm a little puzzled by the "independence" comment, because it doesn't seem like independence plays any role. Two pairs are related or not, and "related in a way independent of particular choices" seems like a strange thing to tack on.
The next most important thing to do is to determine that addition and multiplication are compatible with this relation. 
*Added: * Example verification of addition being well defined
1. (a,b)~(A,B) : (as,bs)=(AS,BS)


*

*(c,d)~(C,D) : (ct,dt)=(CT,DT)

*Addition of (a,b)+(c,d): Choose x,y and form (ax+cy, bx) where bx=dy

*Addition of (A,B)+(C,D): Choose X,Y and form (AX+CY, BX) where BX=DY

*SHOW (ax+cy, bx)~(AX+CY, BX)

*Choose u, U such that bxu=BXU(=dyu=DYU)

*(ax+cy,bx)~(axu+cyu, bxu)=(axu+cyu, BXU) by #6:

*Choose v, V such that xuv=sV by (Ore): (axu+cyu, BXU)~(axuv+cyuv, BXUv)=(asV+cyuv, BXUv)

*(asV+cyuv, BXUv)=(ASV+cyuv, BXUv) by #1.

*Choose w,W such that yuvw=tW by (Ore):  (ASV+cyuv, BXUv)~(ASVw+cyuvw, BXUvw)=(ASVw+ctW, BXUvw)

*(ASVw+ctW,BXUvw)=(ASVw+CTW, BXUvw) by #2.

*We proceed to show that (A[SVw]+C[TW], B[XUvw]) proves #5

*Consider B(SVw-XUvw)=BSVw-BXUvw 
=bsVw-BXUvw by #1
=bxuvw-bxuvw by #6 and #8=0

*Since B is nonzero, we have that SVw=XUvw, and thus AS[Vw]=AX[Uvw]

*Consider D(TW-YUvw)=DTW-DYUvw
=dtW-DYUvw by #2
=dyuvw-DYUvw by #10
=dyuvw-dyuvw=0 by #6

*Since D is nonzero, we have TW=YUvw, thus CT[W]=CY[Uvw]

*Then (ax+cy, bx)~(AX+CY, BX), because 
(ax+cy, bx)~(ASVw+CTW, BXUvw) by #12
=(AX[Uvw]+CY[Uvw], BX[Uvw]) by #14 and #16
~(AX+CY, BX)
The thought of working this out for multiplication and distributivity makes me nauseous, and it would also be a bear to work it out for Ore rings which aren't domains!
