Theorem: Infima in Ordered Group

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 an infimum.
Then all three sets admit an infimum, and:
{{begin-eqn}}
{{eqn | l = \inf \set {x \circ z, y \circ z}
      | r = \inf \set {x, y} \circ z
}}
{{eqn | l = \inf \set {z \circ x, z \circ y}
      | r = z \circ \inf \set {x, y}
}}
{{end-eqn}}

Proof:
First we recall that by definition of ordered group, $\preccurlyeq$ is compatible with $\circ$:
{{begin-eqn}}
{{eqn | q = \forall x, y, z \in G
      | l = x \preccurlyeq y
      | o = \implies
      | r = x \circ z \preccurlyeq y \circ z
}}
{{eqn | ll= \land
      | l = x \preccurlyeq y
      | o = \implies
      | r = z \circ x \preccurlyeq z \circ y
}}
{{end-eqn}}
Let $\set {x, y}$ admit an infimum $c$.
Then by definition of infimum:
:$(1): \quad c$ is a lower bound of $\set {x, y}$ in $G$
:$(2): \quad d \preccurlyeq c$ for all lower bounds $d$ of $\set {x, y}$ in $S$.
Thus we have:
{{begin-eqn}}
{{eqn | l = c
      | o = \preccurlyeq
      | r = x
      | c = {{Defof|Lower Bound of Set}}
}}
{{eqn | lo= \land
      | l = c
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = c \circ z
      | o = \preccurlyeq
      | r = x \circ z
      | c = {{Defof|Relation Compatible with Operation}}
}}
{{eqn | lo= \land
      | l = c \circ z
      | o = \preccurlyeq
      | r = y \circ z
      | c = 
}}
{{end-eqn}}
Hence $\inf \set {x, y} \circ z$ is a lower bound of $\set {x \circ z, y \circ z}$.
Let $d$ be a lower 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:
{{begin-eqn}}
{{eqn | l = d' \circ z
      | o = \preccurlyeq
      | r = x \circ z
      | c = {{Defof|Lower Bound of Set}}
}}
{{eqn | lo= \land
      | l = d' \circ z
      | o = \preccurlyeq
      | r = y \circ z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d' \circ z \circ z^{-1}
      | o = \preccurlyeq
      | r = x \circ z \circ z^{-1}
      | c = {{Defof|Relation Compatible with Operation}}
}}
{{eqn | lo= \land
      | l = d' \circ z \circ z^{-1}
      | o = \preccurlyeq
      | r = y \circ z \circ z^{-1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d'
      | o = \preccurlyeq
      | r = x
      | c = {{Group-axiom|3}}
}}
{{eqn | lo= \land
      | l = d'
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d'
      | o = \preccurlyeq
      | r = c
      | c = {{Defof|Infimum of Set}}: $d'$ is a lower bound of $\set {x, y}$
}}
{{eqn | ll= \leadsto
      | l = d' \circ z
      | o = \preccurlyeq
      | r = c \circ z
      | c = {{Defof|Relation Compatible with Operation}}
}}
{{end-eqn}}
Hence $\inf \set {x, y} \circ z$ is a lower bound of $\set {x \circ z, y \circ z}$ which is smaller than an arbitrary lower bound $d$ of $\set {x \circ z, y \circ z}$.
That is, $\inf \set {x, y} \circ z$ is an infimum of $\set {x \circ z, y \circ z}$.
{{qed|lemma}}
Let $\set {x \circ z, y \circ z}$ admit an infimum $c$.
Then by definition of infimum:
:$(1): \quad c$ is a lower bound of $\set {x \circ z, y \circ z}$ in $G$
:$(2): \quad d \preccurlyeq c$ for all lower 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:
{{begin-eqn}}
{{eqn | l = c' \circ z
      | o = \preccurlyeq
      | r = x \circ z
      | c = {{Defof|Lower Bound of Set}}
}}
{{eqn | lo= \land
      | l = c' \circ z
      | o = \preccurlyeq
      | r = y \circ z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = c' \circ z \circ z^{-1}
      | o = \preccurlyeq
      | r = x \circ z \circ z^{-1}
      | c = {{Defof|Relation Compatible with Operation}}
}}
{{eqn | lo= \land
      | l = c' \circ z \circ z^{-1}
      | o = \preccurlyeq
      | r = y \circ z \circ z^{-1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = c'
      | o = \preccurlyeq
      | r = x
      | c = {{Group-axiom|3}}
}}
{{eqn | lo= \land
      | l = c'
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z \circ c'
      | o = \preccurlyeq
      | r = z \circ x
      | c = {{Defof|Relation Compatible with Operation}}
}}
{{eqn | lo= \land
      | l = z \circ c'
      | o = \preccurlyeq
      | r = z \circ y
      | c = 
}}
{{end-eqn}}
Hence $z \circ c'$ is a lower bound of $\set {z \circ x, z \circ y}$.
Let $d$ be a lower 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:
{{begin-eqn}}
{{eqn | l = d
      | o = \preccurlyeq
      | r = z \circ x
      | c = {{Defof|Lower Bound of Set}}
}}
{{eqn | lo= \land
      | l = d
      | o = \preccurlyeq
      | r = z \circ y
      | c = 
}}
{{eqn | l = z \circ d'
      | o = \preccurlyeq
      | r = z \circ x
      | c = Definition of $d'$
}}
{{eqn | lo= \land
      | l = z \circ d'
      | o = \preccurlyeq
      | r = z \circ y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z \circ d'
      | o = \preccurlyeq
      | r = z \circ c'
      | c = {{Defof|Infimum of Set}}: $z \circ d'$ is a lower bound of $\set {z \circ x, z \circ y}$
}}
{{eqn | ll= \leadsto
      | l = d
      | o = \preccurlyeq
      | r = z \circ c'
      | c = Definition of $d'$
}}
{{end-eqn}}
Hence $z \circ c'$ is a lower bound of $\set {z \circ x, z \circ y}$ which is smaller than an arbitrary lower bound $d$ of $\set {z \circ x, z \circ y}$.
That is, $z \circ c'$ is an infimum of $\set {z \circ x, z \circ y}$.
{{qed|lemma}}
Let $\set {z \circ x, z \circ y}$ admit an infimum $c$.
Then by definition of infimum:
:$(1): \quad c$ is a lower bound of $\set {z \circ x, z \circ y}$ in $G$
:$(2): \quad d \preccurlyeq c$ for all lower 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:
{{begin-eqn}}
{{eqn | l = z \circ c'
      | o = \preccurlyeq
      | r = z \circ x
      | c = {{Defof|Lower Bound of Set}}
}}
{{eqn | lo= \land
      | l = z \circ c'
      | o = \preccurlyeq
      | r = z \circ y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z^{-1} \circ z \circ c'
      | o = \preccurlyeq
      | r = z^{-1} \circ z \circ x
      | c = {{Defof|Relation Compatible with Operation}}
}}
{{eqn | lo= \land
      | l = z^{-1} \circ z \circ c'
      | o = \preccurlyeq
      | r = z^{-1} \circ z \circ y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = c'
      | o = \preccurlyeq
      | r = x
      | c = {{Group-axiom|3}}
}}
{{eqn | lo= \land
      | l = c'
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{end-eqn}}
Hence $c'$ is a lower bound of $\set {x, y}$.
Let $d$ be a lower bound of $\set {x, y}$.
Then:
{{begin-eqn}}
{{eqn | l = d
      | o = \preccurlyeq
      | r = x
      | c = {{Defof|Lower Bound of Set}}
}}
{{eqn | lo= \land
      | l = d
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{eqn | l = z \circ d
      | o = \preccurlyeq
      | r = z \circ x
      | c = Definition of $d'$
}}
{{eqn | lo= \land
      | l = z \circ d
      | o = \preccurlyeq
      | r = z \circ y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z \circ d
      | o = \preccurlyeq
      | r = z \circ c'
      | c = {{Defof|Infimum of Set}}: $z \circ d$ is a lower bound of $\set {z \circ x, z \circ y}$
}}
{{eqn | ll= \leadsto
      | l = z^{-1} \circ z \circ d
      | o = \preccurlyeq
      | r = z^{-1} \circ z \circ c'
      | c = {{Defof|Relation Compatible with Operation}}
}}
{{eqn | ll= \leadsto
      | l = d
      | o = \preccurlyeq
      | r = c'
      | c = Definition of $d'$
}}
{{end-eqn}}
Hence $c'$ is a lower bound of $\set {x, y}$ which is smaller than an arbitrary lower bound $d$ of $\set {x, y}$.
That is, $c'$ is an infimum of $\set {x, y}$.
Hence by definition of $c'$:
:$z \circ \inf \set {x, y} = \inf \set {z \circ x, z \circ y}$
{{qed|lemma}}
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 an infimum, they all do, and:
{{begin-eqn}}
{{eqn | l = \inf \set {x \circ z, y \circ z}
      | r = \inf \set {x, y} \circ z
}}
{{eqn | l = \inf \set {z \circ x, z \circ y}
      | r = z \circ \inf \set {x, y}
}}
{{end-eqn}}
{{qed}}