# Product of Absolute Values on Ordered Integral Domain

## Theorem

Let $\struct {D, +, \times, \le}$ be an ordered integral domain whose zero is denoted by $0_D$.

For all $a \in D$, let $\size a$ denote the absolute value of $a$.

Then:

$\size a \times \size b = \size {a \times b}$

## Proof

Let $P$ be the (strict) positivity property on $D$.

Let $<$ be the (strict) total ordering defined on $D$ as:

$a < b \iff a \le b \land a \ne b$

Let $N$ be the strict negativity property on $D$.

We consider all possibilities in turn.

$(1): \quad a = 0_D$ or $b = 0_D$

In this case, both the left hand side $\size a \times \size b$ and the right hand side are equal to zero.

So:

$\size a \times \size b = \size {a \times b}$

$(2): \quad \map P a, \map P b$

First:

 $\displaystyle \map P a, \map P b$ $\leadsto$ $\displaystyle \size a = a, \size b = b$ Definition of Absolute Value on Ordered Integral Domain $\displaystyle$ $\leadsto$ $\displaystyle \size a \times \size b = a \times b$

Then:

 $\displaystyle \map P a, \map P b$ $\leadsto$ $\displaystyle \map P {a \times b}$ Strict Positivity Property: $(P \, 2)$ $\displaystyle$ $\leadsto$ $\displaystyle \size {a \times b} = a \times b$ Definition of Absolute Value on Ordered Integral Domain

So:

$\size a \times \size b = \size {a \times b}$

$(3): \quad \map P a, \map N b$

First:

 $\displaystyle \map P a, \map N b$ $\leadsto$ $\displaystyle \size a = a, \size b = -b$ Definition of Absolute Value on Ordered Integral Domain $\displaystyle$ $\leadsto$ $\displaystyle \size a \times \size b = -a \times b$ Product with Ring Negative

Then:

 $\displaystyle \map P a, \map N b$ $\leadsto$ $\displaystyle \map N {a \times b}$ Properties of Strict Negativity: $(5)$ $\displaystyle$ $\leadsto$ $\displaystyle \map P {-a \times b}$ Definition of Strict Negativity Property $\displaystyle$ $\leadsto$ $\displaystyle \size {a \times b} = -a \times b$ Definition of Absolute Value on Ordered Integral Domain

So:

$\size a \times \size b = \size {a \times b}$

Similarly $\map N a, \map P b$.

$(4): \quad \map N a, \map N b$

First:

 $\displaystyle \map N a, \map N b$ $\leadsto$ $\displaystyle \size a = -a, \size b = -b$ Definition of Absolute Value on Ordered Integral Domain $\displaystyle$ $\leadsto$ $\displaystyle \size a \times \size b = a \times b$ Product of Ring Negatives

Then:

 $\displaystyle \map N a, \map N b$ $\leadsto$ $\displaystyle \map P {a \times b}$ Properties of Strict Negativity: $(4)$ $\displaystyle$ $\leadsto$ $\displaystyle \map P {a \times b}$ Definition of Strict Negativity Property $\displaystyle$ $\leadsto$ $\displaystyle \size {a \times b} = a \times b$ Definition of Absolute Value on Ordered Integral Domain

So:

$\size a \times \size b = \size {a \times b}$

In all cases the result holds.

$\blacksquare$