Multiplication of Cross-Relation Equivalence Classes on Natural Numbers is Well-Defined

From ProofWiki
Jump to navigation Jump to search


Let $\left({\N, +}\right)$ be the semigroup of natural numbers under addition.

Let $\left({\N \times \N, \oplus}\right)$ be the (external) direct product of $\left({\N, +}\right)$ with itself, where $\oplus$ is the operation on $\N \times \N$ induced by $+$ on $\N$.

Let $\boxtimes$ be the cross-relation defined on $\N \times \N$ by:

$\left({x_1, y_1}\right) \boxtimes \left({x_2, y_2}\right) \iff x_1 + y_2 = x_2 + y_1$

Let $\left[\!\left[{x, y}\right]\!\right]$ denote the equivalence class of $\left({x, y}\right)$ under $\boxtimes$.

Let $\otimes$ be the binary operation defined on these equivalence classes as:

$\forall \left[\!\left[{a, b}\right]\!\right], \left[\!\left[{c, d}\right]\!\right] \in \N \times \N: \left[\!\left[{a, b}\right]\!\right] \otimes \left[\!\left[{c, d}\right]\!\right] = \left[\!\left[{\left({a \cdot c}\right) + \left({b \cdot d}\right), \left({a \cdot d}\right) + \left({b \cdot c}\right)}\right]\!\right]$

where $a \cdot c$ denotes natural number multiplication between $a$ and $c$.

The operation $\otimes$ on these equivalence classes is well-defined, in the sense that:

\(\displaystyle \left[\!\left[{a_1, b_1}\right]\!\right]\) \(=\) \(\displaystyle \left[\!\left[{a_2, b_2}\right]\!\right]\)
\(\displaystyle \left[\!\left[{c_1, d_1}\right]\!\right]\) \(=\) \(\displaystyle \left[\!\left[{c_2, d_2}\right]\!\right]\)
\(\displaystyle \implies \ \ \) \(\displaystyle \left[\!\left[{a_1, b_1}\right]\!\right] \otimes \left[\!\left[{c_1, d_1}\right]\!\right]\) \(=\) \(\displaystyle \left[\!\left[{a_2, b_2}\right]\!\right] \otimes \left[\!\left[{c_2, d_2}\right]\!\right]\)


Let $\left[\!\left[{a_1, b_1}\right]\!\right], \left[\!\left[{a_2, b_2}\right]\!\right], \left[\!\left[{c_1, d_1}\right]\!\right], \left[\!\left[{c_2, d_2}\right]\!\right]$ be $\boxtimes$-equivalence classes such that $\left[\!\left[{a_1, b_1}\right]\!\right] = \left[\!\left[{a_2, b_2}\right]\!\right]$ and $\left[\!\left[{c_1, d_1}\right]\!\right] = \left[\!\left[{c_2, d_2}\right]\!\right]$.


\(\displaystyle \left[\!\left[{a_1, b_1}\right]\!\right]\) \(=\) \(\displaystyle \left[\!\left[{a_2, b_2}\right]\!\right]\) Definition of Operation Induced by Direct Product
\(\, \displaystyle \land \, \) \(\displaystyle \left[\!\left[{c_1, d_1}\right]\!\right]\) \(=\) \(\displaystyle \left[\!\left[{c_2, d_2}\right]\!\right]\) Definition of Operation Induced by Direct Product
\(\displaystyle \iff \ \ \) \(\displaystyle a_1 + b_2\) \(=\) \(\displaystyle a_2 + b_1\) Definition of Cross-Relation
\(\, \displaystyle \land \, \) \(\displaystyle c_1 + d_2\) \(=\) \(\displaystyle c_2 + d_1\) Definition of Cross-Relation

Both $+$ and $\times$ are commutative and associative on $\N$. Thus:

\(\displaystyle \left({a_1 \cdot c_1 + b_1 \cdot d_1 + a_2 \cdot d_2 + b_2 \cdot c_2}\right)\) \(+\) \(\displaystyle \left({a_2 \cdot c_1 + b_2 \cdot c_1 + a_2 \cdot d_1 + b_2 \cdot d_1}\right)\)
\(\, \displaystyle = \, \) \(\displaystyle \left({a_1 + b_2}\right) \cdot c_1 + \left({b_1 + a_2}\right) \cdot d_1\) \(+\) \(\displaystyle a_2 \cdot \left({c_1 + d_2}\right) + b_2 \cdot \left({d_1 + c_2}\right)\)
\(\, \displaystyle = \, \) \(\displaystyle \left({b_1 + a_2}\right) \cdot c_1 + \left({a_1 + b_2}\right) \cdot d_1\) \(+\) \(\displaystyle a_2 \cdot \left({d_1 + c_2}\right) + b_2 \cdot \left({c_1 + d_2}\right)\) as $a_1 + b_2 = b_1 + a_2, c_1 + d_2 = d_1 + c_2$
\(\, \displaystyle = \, \) \(\displaystyle b_1 \cdot c_1 + a_2 \cdot c_1 + a_1 \cdot b_2 + a_1 \cdot d_1\) \(+\) \(\displaystyle a_2 \cdot d_1 + a_2 \cdot c_2 + b_2 \cdot c_1 + b_2 \cdot d_2\)
\(\, \displaystyle = \, \) \(\displaystyle \left({a_1 \cdot d_1 + b_1 \cdot c_1 + a_2 \cdot c_2 + b_2 \cdot d_2}\right)\) \(+\) \(\displaystyle \left({a_2 \cdot c_1 + b_2 \cdot c_1 + a_2 \cdot d_1 + b_2 \cdot d_1}\right)\)

So we have $a_1 \cdot c_1 + b_1 \cdot d_1 + a_2 \cdot d_2 + b_2 \cdot c_2 = a_1 \cdot d_1 + b_1 \cdot c_1 + a_2 \cdot c_2 + b_2 \cdot d_2$ and so, by the definition of $\boxtimes$, we have:

$\left[\!\left[{a_1 \cdot c_1 + b_1 \cdot d_1, a_1 \cdot d_1 + b_1 \cdot c_1}\right]\!\right] = \left[\!\left[{a_2 \cdot c_2 + b_2 \cdot d_2, a_2 \cdot d_2 + b_2 \cdot c_2}\right]\!\right]$

So, by the definition of integer multiplication, this leads to:

$\left[\!\left[{a_1, b_1}\right]\!\right] \otimes \left[\!\left[{c_1, d_1}\right]\!\right] = \left[\!\left[{a_2, b_2}\right]\!\right] \otimes \left[\!\left[{c_2, d_2}\right]\!\right]$

Thus integer multiplication has been shown to be well-defined.