Cross-Relation Equivalence Classes on Natural Numbers are Cancellable for Addition

From ProofWiki
Jump to: navigation, 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$.

The operation $\oplus$ on these equivalence classes is cancellable, in the sense that:

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


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]\) $\quad$ by definition of operation induced by direct product $\quad$
\(\, \displaystyle \land \, \) \(\displaystyle \left[\!\left[{c_1, d_1}\right]\!\right]\) \(=\) \(\displaystyle \left[\!\left[{c_2, d_2}\right]\!\right]\) $\quad$ by definition of operation induced by direct product $\quad$
\(\displaystyle \iff \ \ \) \(\displaystyle a_1 + b_2\) \(=\) \(\displaystyle a_2 + b_1\) $\quad$ by definition of cross-relation $\quad$
\(\, \displaystyle \land \, \) \(\displaystyle c_1 + d_2\) \(=\) \(\displaystyle c_2 + d_1\) $\quad$ by definition of cross-relation $\quad$

Then we have:

\(\displaystyle \left({a_1 + c_1}\right) + \left({b_2 + d_2}\right)\) \(=\) \(\displaystyle \left({a_1 + b_2}\right) + \left({c_1 + d_2}\right)\) $\quad$ Commutativity and associativity of $+$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \left({a_2 + b_1}\right) + \left({c_2 + d_1}\right)\) $\quad$ from above: $a_1 + b_2 = a_2 + b_1, c_1 + d_2 = c_2 + d_1$ $\quad$
\(\displaystyle \) \(=\) \(\displaystyle \left({a_2 + c_2}\right) + \left({b_1 + d_1}\right)\) $\quad$ Commutativity and associativity of $+$ $\quad$
\(\displaystyle \implies \ \ \) \(\displaystyle \left({a_1 + c_1, b_1 + d_1}\right)\) \(\boxtimes\) \(\displaystyle \left({a_2 + c_2, b_2 + d_2}\right)\) $\quad$ Definition of $\boxtimes$ $\quad$
\(\displaystyle \implies \ \ \) \(\displaystyle \left({\left({a_1, b_1}\right) \oplus \left({c_1, d_1}\right)}\right)\) \(\boxtimes\) \(\displaystyle \left({\left({a_2, b_2}\right) \oplus \left({c_2, d_2}\right)}\right)\) $\quad$ Definition of $\oplus$ $\quad$