# Suprema in Ordered Group

## Theorem

Let $\struct {G, \circ, \preccurlyeq}$ be an ordered group.

Let $x, y, z \in G$ be arbitrary.

Let any one of the sets $\set {x, y}$, $\set {x \circ z, y \circ z}$ or $\set {z \circ x, z \circ y}$ admit a supremum.

Then all three sets admit a supremum, and:

 $\ds \sup \set {x \circ z, y \circ z}$ $=$ $\ds \sup \set {x, y} \circ z$ $\ds \sup \set {z \circ x, z \circ y}$ $=$ $\ds z \circ \sup \set {x, y}$

## Proof

First we recall that by definition of ordered group, $\preccurlyeq$ is compatible with $\circ$:

 $\ds \forall x, y, z \in G: \,$ $\ds x \preccurlyeq y$ $\implies$ $\ds x \circ z \preccurlyeq y \circ z$ $\ds \land \ \$ $\ds x \preccurlyeq y$ $\implies$ $\ds z \circ x \preccurlyeq z \circ y$

Let $\set {x, y}$ admit a supremum $c$.

Then by definition of supremum:

$(1): \quad c$ is an upper bound of $\set {x, y}$ in $G$
$(2): \quad c \preccurlyeq d$ for all upper bounds $d$ of $\set {x, y}$ in $S$.

Thus we have:

 $\ds x$ $\preccurlyeq$ $\ds c$ Definition of Upper Bound of Set $\, \ds \land \,$ $\ds y$ $\preccurlyeq$ $\ds c$ $\ds \leadsto \ \$ $\ds x \circ z$ $\preccurlyeq$ $\ds c \circ z$ Definition of Relation Compatible with Operation $\, \ds \land \,$ $\ds y \circ z$ $\preccurlyeq$ $\ds c \circ z$

Hence $\sup \set {x, y} \circ z$ is an upper bound of $\set {x \circ z, y \circ z}$.

Let $d$ be an upper bound of $\set {x \circ z, y \circ z}$.

Then as $G$ is a group we have that:

$d = d' \circ z$

for some $d' \in G$.

Then:

 $\ds x \circ z$ $\preccurlyeq$ $\ds d' \circ z$ Definition of Upper Bound of Set $\, \ds \land \,$ $\ds y \circ z$ $\preccurlyeq$ $\ds d' \circ z$ $\ds \leadsto \ \$ $\ds x \circ z \circ z^{-1}$ $\preccurlyeq$ $\ds d' \circ z \circ z^{-1}$ Definition of Relation Compatible with Operation $\, \ds \land \,$ $\ds y \circ z \circ z^{-1}$ $\preccurlyeq$ $\ds d' \circ z \circ z^{-1}$ $\ds \leadsto \ \$ $\ds x$ $\preccurlyeq$ $\ds d'$ Group Axiom $\text G 3$: Existence of Inverse Element $\, \ds \land \,$ $\ds y$ $\preccurlyeq$ $\ds d'$ $\ds \leadsto \ \$ $\ds c$ $\preccurlyeq$ $\ds d'$ Definition of Supremum of Set: $d'$ is an upper bound of $\set {x, y}$ $\ds \leadsto \ \$ $\ds c \circ z$ $\preccurlyeq$ $\ds d' \circ z$ Definition of Relation Compatible with Operation

Hence $\sup \set {x, y} \circ z$ is an upper bound of $\set {x \circ z, y \circ z}$ which is smaller than an arbitrary upper bound $d$ of $\set {x \circ z, y \circ z}$.

That is, $\sup \set {x, y} \circ z$ is a supremum of $\set {x \circ z, y \circ z}$.

$\Box$

Let $\set {x \circ z, y \circ z}$ admit a supremum $c$.

Then by definition of supremum:

$(1): \quad c$ is an upper bound of $\set {x \circ z, y \circ z}$ in $G$
$(2): \quad c \preccurlyeq d$ for all upper bounds $d$ of $\set {x \circ z, y \circ z}$ in $S$.

As $G$ is a group, there exists $c' \in G$ such that $c' \circ z = c$.

Thus we have:

 $\ds x \circ z$ $\preccurlyeq$ $\ds c' \circ z$ Definition of Upper Bound of Set $\, \ds \land \,$ $\ds y \circ z$ $\preccurlyeq$ $\ds c' \circ z$ $\ds \leadsto \ \$ $\ds x \circ z \circ z^{-1}$ $\preccurlyeq$ $\ds c' \circ z \circ z^{-1}$ Definition of Relation Compatible with Operation $\, \ds \land \,$ $\ds y \circ z \circ z^{-1}$ $\preccurlyeq$ $\ds c' \circ z \circ z^{-1}$ $\ds \leadsto \ \$ $\ds x$ $\preccurlyeq$ $\ds c'$ Group Axiom $\text G 3$: Existence of Inverse Element $\, \ds \land \,$ $\ds y$ $\preccurlyeq$ $\ds c'$ $\ds \leadsto \ \$ $\ds z \circ x$ $\preccurlyeq$ $\ds z \circ c'$ Definition of Relation Compatible with Operation $\, \ds \land \,$ $\ds z \circ y$ $\preccurlyeq$ $\ds z \circ c'$

Hence $z \circ c'$ is an upper bound of $\set {z \circ x, z \circ y}$.

Let $d$ be an upper bound of $\set {z \circ x, z \circ y}$.

As $G$ is a group, there exists $d' \in G$ such that $z \circ d' = d$.

Then:

 $\ds z \circ x$ $\preccurlyeq$ $\ds d$ Definition of Upper Bound of Set $\, \ds \land \,$ $\ds z \circ y$ $\preccurlyeq$ $\ds d$ $\ds z \circ x$ $\preccurlyeq$ $\ds z \circ d'$ Definition of $d'$ $\, \ds \land \,$ $\ds z \circ y$ $\preccurlyeq$ $\ds z \circ d'$ $\ds \leadsto \ \$ $\ds z \circ c'$ $\preccurlyeq$ $\ds z \circ d'$ Definition of Supremum of Set: $z \circ d'$ is an upper bound of $\set {z \circ x, z \circ y}$ $\ds \leadsto \ \$ $\ds z \circ c'$ $\preccurlyeq$ $\ds d$ Definition of $d'$

Hence $z \circ c'$ is an upper bound of $\set {z \circ x, z \circ y}$ which is smaller than an arbitrary upper bound $d$ of $\set {z \circ x, z \circ y}$.

That is, $z \circ c'$ is a supremum of $\set {z \circ x, z \circ y}$.

$\Box$

Let $\set {z \circ x, z \circ y}$ admit a supremum $c$.

Then by definition of supremum:

$(1): \quad c$ is an upper bound of $\set {z \circ x, z \circ y}$ in $G$
$(2): \quad c \preccurlyeq d$ for all upper bounds $d$ of $\set {z \circ x, z \circ y}$ in $S$.

As $G$ is a group, there exists $c' \in G$ such that $z \circ c' = c$.

Thus we have:

 $\ds z \circ x$ $\preccurlyeq$ $\ds z \circ c'$ Definition of Upper Bound of Set $\, \ds \land \,$ $\ds z \circ y$ $\preccurlyeq$ $\ds z \circ c'$ $\ds \leadsto \ \$ $\ds z^{-1} \circ z \circ x$ $\preccurlyeq$ $\ds z^{-1} \circ z \circ c'$ Definition of Relation Compatible with Operation $\, \ds \land \,$ $\ds z^{-1} \circ z \circ y$ $\preccurlyeq$ $\ds z^{-1} \circ z \circ c'$ $\ds \leadsto \ \$ $\ds x$ $\preccurlyeq$ $\ds c'$ Group Axiom $\text G 3$: Existence of Inverse Element $\, \ds \land \,$ $\ds y$ $\preccurlyeq$ $\ds c'$

Hence $c'$ is an upper bound of $\set {x, y}$.

Let $d$ be an upper bound of $\set {x, y}$.

Then:

 $\ds x$ $\preccurlyeq$ $\ds d$ Definition of Upper Bound of Set $\, \ds \land \,$ $\ds y$ $\preccurlyeq$ $\ds d$ $\ds z \circ x$ $\preccurlyeq$ $\ds z \circ d$ Definition of $d'$ $\, \ds \land \,$ $\ds z \circ y$ $\preccurlyeq$ $\ds z \circ d$ $\ds \leadsto \ \$ $\ds z \circ c'$ $\preccurlyeq$ $\ds z \circ d$ Definition of Supremum of Set: $z \circ d$ is an upper bound of $\set {z \circ x, z \circ y}$ $\ds \leadsto \ \$ $\ds z^{-1} \circ z \circ c'$ $\preccurlyeq$ $\ds z^{-1} \circ z \circ d$ Definition of Relation Compatible with Operation $\ds \leadsto \ \$ $\ds c'$ $\preccurlyeq$ $\ds d$ Definition of $d'$

Hence $c'$ is an upper bound of $\set {x, y}$ which is smaller than an arbitrary upper bound $d$ of $\set {x, y}$.

That is, $c'$ is a supremum of $\set {x, y}$.

Hence by definition:

$z \circ \sup \set {x, y} = \sup \set {z \circ x, z \circ y}$

$\Box$

Thus we have shown that if any of the three sets $\set {x, y}$, $\set {x \circ z, y \circ z}$ or $\set {z \circ x, z \circ y}$ admit a supremum, they all do, and:

 $\ds \sup \set {x \circ z, y \circ z}$ $=$ $\ds \sup \set {x, y} \circ z$ $\ds \sup \set {z \circ x, z \circ y}$ $=$ $\ds z \circ \sup \set {x, y}$

$\blacksquare$