IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory OrderedGroup_ZF imports Group_ZF_1 AbelianGroup_ZF Finite_ZF_1 OrderedLoop_ZF
begin

This theory file defines and shows the basic properties of (partially or linearly) ordered groups. We show that in linearly ordered groups finite sets are bounded and provide a sufficient condition for bounded sets to be finite. This allows to show in Int_ZF_IML.thy that subsets of integers are bounded iff they are finite. Some theorems proven here are properties of ordered loops rather that groups. However, for now the development is independent from the material in the OrderedLoop_ZF theory, we just import the definitions of NonnegativeSet and PositiveSet from there.

Ordered groups

This section defines ordered groups and various related notions.

An ordered group is a group equipped with a partial order that is "translation invariant", that is if \(a\leq b\) then \(a\cdot g \leq b\cdot g\) and \(g\cdot a \leq g\cdot b\).

definition

\( \text{IsAnOrdGroup}(G,P,r) \equiv \) \( ( \text{IsAgroup}(G,P) \wedge r\subseteq G\times G \wedge \text{IsPartOrder}(G,r) \wedge (\forall g\in G.\ \forall a b.\ \) \( \langle a,b\rangle \in r \longrightarrow \langle P\langle a,g\rangle ,P\langle b,g\rangle \rangle \in r \wedge \langle P\langle g,a\rangle ,P\langle g,b\rangle \rangle \in r ) ) \)

We also define the absolute value as a ZF-function that is the identity on \(G^+\) and the group inverse on the rest of the group.

definition

\( \text{AbsoluteValue}(G,P,r) \equiv id( \text{Nonnegative}(G,P,r)) \cup \) \( \text{restrict}( \text{GroupInv}(G,P),G - \text{Nonnegative}(G,P,r)) \)

The odd functions are defined as those having property \(f(a^{-1})=(f(a))^{-1}\). This looks a bit strange in the multiplicative notation, I have to admit. For linearly ordered groups a function \(f\) defined on the set of positive elements iniquely defines an odd function of the whole group. This function is called an odd extension of \(f\)

definition

\( \text{OddExtension}(G,P,r,f) \equiv \) \( (f \cup \{\langle a, \text{GroupInv}(G,P)(f( \text{GroupInv}(G,P)(a)))\rangle .\ \) \( a \in \text{GroupInv}(G,P)( \text{PositiveSet}(G,P,r))\} \cup \) \( \{\langle \text{ TheNeutralElement}(G,P),\text{ TheNeutralElement}(G,P)\rangle \}) \)

We will use a similar notation for ordered groups as for the generic groups. \( G^+ \) denotes the set of nonnegative elements (that satisfy \(1\leq a\)) and \( G_+ \) is the set of (strictly) positive elements. \( -A \) is the set inverses of elements from \(A\). I hope that using additive notation for this notion is not too shocking here. The symbol \( f^\circ \) denotes the odd extension of \(f\). For a function defined on \(G_+\) this is the unique odd function on \(G\) that is equal to \(f\) on \(G_+\).

locale group3

assumes ordGroupAssum: \( \text{IsAnOrdGroup}(G,P,r) \)

defines \( 1 \equiv \text{ TheNeutralElement}(G,P) \)

defines \( a \cdot b \equiv P\langle a,b\rangle \)

defines \( x^{-1} \equiv \text{GroupInv}(G,P)(x) \)

defines \( a \leq b \equiv \langle a,b\rangle \in r \)

defines \( a \lt b \equiv a\leq b \wedge a\neq b \)

defines \( G^+ \equiv \text{Nonnegative}(G,P,r) \)

defines \( G_+ \equiv \text{PositiveSet}(G,P,r) \)

defines \( -A \equiv \text{GroupInv}(G,P)(A) \)

defines \( \vert a\vert \equiv \text{AbsoluteValue}(G,P,r)(a) \)

defines \( f^\circ \equiv \text{OddExtension}(G,P,r,f) \)

In group3 context we can use the theorems proven in the group0 context.

lemma (in group3) OrderedGroup_ZF_1_L1:

shows \( group0(G,P) \) using ordGroupAssum, IsAnOrdGroup_def, group0_def

Ordered group (carrier) is not empty. This is a property of monoids, but it is good to have it handy in the group3 context.

lemma (in group3) OrderedGroup_ZF_1_L1A:

shows \( G\neq 0 \) using OrderedGroup_ZF_1_L1, group0_2_L1, group0_1_L3A

The next lemma is just to see the definition of the nonnegative set in our notation.

lemma (in group3) OrderedGroup_ZF_1_L2:

shows \( g\in G^+ \longleftrightarrow 1 \leq g \) using ordGroupAssum, IsAnOrdGroup_def, Nonnegative_def

The next lemma is just to see the definition of the positive set in our notation.

lemma (in group3) OrderedGroup_ZF_1_L2A:

shows \( g\in G_+ \longleftrightarrow (1 \leq g \wedge g\neq 1 ) \) using ordGroupAssum, IsAnOrdGroup_def, PositiveSet_def

For total order if \(g\) is not in \(G^{+}\), then it has to be less or equal the unit.

lemma (in group3) OrderedGroup_ZF_1_L2B:

assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G-G^+ \)

shows \( a\leq 1 \)proof
from A2 have \( a\in G \), \( 1 \in G \), \( \neg (1 \leq a) \) using OrderedGroup_ZF_1_L1, group0_2_L2, OrderedGroup_ZF_1_L2
with A1 show \( thesis \) using IsTotal_def
qed

The group order is reflexive.

lemma (in group3) OrderedGroup_ZF_1_L3:

assumes \( g\in G \)

shows \( g\leq g \) using ordGroupAssum, assms, IsAnOrdGroup_def, IsPartOrder_def, refl_def

\(1\) is nonnegative.

lemma (in group3) OrderedGroup_ZF_1_L3A:

shows \( 1 \in G^+ \) using OrderedGroup_ZF_1_L2, OrderedGroup_ZF_1_L3, OrderedGroup_ZF_1_L1, group0_2_L2

In this context \(a \leq b\) implies that both \(a\) and \(b\) belong to \(G\).

lemma (in group3) OrderedGroup_ZF_1_L4:

assumes \( a\leq b \)

shows \( a\in G \), \( b\in G \) using ordGroupAssum, assms, IsAnOrdGroup_def

Similarly in this context \(a \le b\) implies that both \(a\) and \(b\) belong to \(G\).

lemma (in group3) less_are_members:

assumes \( a \lt b \)

shows \( a\in G \), \( b\in G \) using ordGroupAssum, assms, IsAnOrdGroup_def

It is good to have transitivity handy.

lemma (in group3) Group_order_transitive:

assumes A1: \( a\leq b \), \( b\leq c \)

shows \( a\leq c \)proof
from ordGroupAssum have \( \text{trans}(r) \) using IsAnOrdGroup_def, IsPartOrder_def
moreover
from A1 have \( \langle a,b\rangle \in r \wedge \langle b,c\rangle \in r \)
ultimately have \( \langle a,c\rangle \in r \) by (rule Fol1_L3 )
thus \( thesis \)
qed

The order in an ordered group is antisymmetric.

lemma (in group3) group_order_antisym:

assumes A1: \( a\leq b \), \( b\leq a \)

shows \( a=b \)proof
from ordGroupAssum, A1 have \( \text{antisym}(r) \), \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \) using IsAnOrdGroup_def, IsPartOrder_def
then show \( a=b \) by (rule Fol1_L4 )
qed

Transitivity for the strict order: if \(a < b\) and \(b\leq c\), then \(a < c\).

lemma (in group3) OrderedGroup_ZF_1_L4A:

assumes A1: \( a \lt b \) and A2: \( b\leq c \)

shows \( a \lt c \)proof
from A1, A2 have \( a\leq b \), \( b\leq c \)
then have \( a\leq c \) by (rule Group_order_transitive )
moreover
from A1, A2 have \( a\neq c \) using group_order_antisym
ultimately show \( a \lt c \)
qed

Another version of transitivity for the strict order: if \(a\leq b\) and \(b < c\), then \(a < c\).

lemma (in group3) group_strict_ord_transit:

assumes A1: \( a\leq b \) and A2: \( b \lt c \)

shows \( a \lt c \)proof
from A1, A2 have \( a\leq b \), \( b\leq c \)
then have \( a\leq c \) by (rule Group_order_transitive )
moreover
from A1, A2 have \( a\neq c \) using group_order_antisym
ultimately show \( a \lt c \)
qed

The order is translation invariant.

lemma (in group3) ord_transl_inv:

assumes \( a\leq b \), \( c\in G \)

shows \( a\cdot c \leq b\cdot c \) and \( c\cdot a \leq c\cdot b \) using ordGroupAssum, assms unfolding IsAnOrdGroup_def

Strict order is preserved by translations.

lemma (in group3) group_strict_ord_transl_inv:

assumes \( a \lt b \) and \( c\in G \)

shows \( a\cdot c \lt b\cdot c \) and \( c\cdot a \lt c\cdot b \) using assms, ord_transl_inv, OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L1, group0_2_L19

If the group order is total, then the group is ordered linearly.

lemma (in group3) group_ord_total_is_lin:

assumes \( r \text{ is total on } G \)

shows \( \text{IsLinOrder}(G,r) \) using assms, ordGroupAssum, IsAnOrdGroup_def, Order_ZF_1_L3

For linearly ordered groups elements in the nonnegative set are greater than those in the complement.

lemma (in group3) OrderedGroup_ZF_1_L4B:

assumes \( r \text{ is total on } G \) and \( a\in G^+ \) and \( b \in G-G^+ \)

shows \( b\leq a \)proof
from assms have \( b\leq 1 \), \( 1 \leq a \) using OrderedGroup_ZF_1_L2, OrderedGroup_ZF_1_L2B
then show \( thesis \) by (rule Group_order_transitive )
qed

If \(a\leq 1\) and \(a\neq 1\), then \(a \in G\setminus G^{+}\).

lemma (in group3) OrderedGroup_ZF_1_L4C:

assumes A1: \( a\leq 1 \) and A2: \( a\neq 1 \)

shows \( a \in G-G^+ \)proof
{
assume \( a \notin G-G^+ \)
with ordGroupAssum, A1, A2 have \( False \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L2, OrderedGroup_ZF_1_L4, IsAnOrdGroup_def, IsPartOrder_def, antisym_def
}
thus \( thesis \)
qed

An element smaller than an element in \(G\setminus G^+\) is in \(G\setminus G^+\).

lemma (in group3) OrderedGroup_ZF_1_L4D:

assumes A1: \( a\in G-G^+ \) and A2: \( b\leq a \)

shows \( b\in G-G^+ \)proof
{
assume \( b \notin G - G^+ \)
with A2 have \( 1 \leq b \), \( b\leq a \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L2
then have \( 1 \leq a \) by (rule Group_order_transitive )
with A1 have \( False \) using OrderedGroup_ZF_1_L2
}
thus \( thesis \)
qed

The nonnegative set is contained in the group.

lemma (in group3) OrderedGroup_ZF_1_L4E:

shows \( G^+ \subseteq G \) using OrderedGroup_ZF_1_L2, OrderedGroup_ZF_1_L4

The positive set is contained in the nonnegative set, hence in the group.

lemma (in group3) pos_set_in_gr:

shows \( G_+ \subseteq G^+ \) and \( G_+ \subseteq G \) using OrderedGroup_ZF_1_L2A, OrderedGroup_ZF_1_L2, OrderedGroup_ZF_1_L4E

Taking the inverse on both sides reverses the inequality.

lemma (in group3) OrderedGroup_ZF_1_L5:

assumes A1: \( a\leq b \)

shows \( b^{-1}\leq a^{-1} \)proof
from A1 have T1: \( a\in G \), \( b\in G \), \( a^{-1}\in G \), \( b^{-1}\in G \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L1, inverse_in_group
with A1, ordGroupAssum have \( a\cdot a^{-1}\leq b\cdot a^{-1} \) using IsAnOrdGroup_def
with T1, ordGroupAssum have \( b^{-1}\cdot 1 \leq b^{-1}\cdot (b\cdot a^{-1}) \) using OrderedGroup_ZF_1_L1, group0_2_L6, IsAnOrdGroup_def
with T1 show \( thesis \) using OrderedGroup_ZF_1_L1, group0_2_L2, group_oper_assoc, group0_2_L6
qed

If an element is smaller that the unit, then its inverse is greater.

lemma (in group3) OrderedGroup_ZF_1_L5A:

assumes A1: \( a\leq 1 \)

shows \( 1 \leq a^{-1} \)proof
from A1 have \( 1 ^{-1}\leq a^{-1} \) using OrderedGroup_ZF_1_L5
then show \( thesis \) using OrderedGroup_ZF_1_L1, group_inv_of_one
qed

If an the inverse of an element is greater that the unit, then the element is smaller.

lemma (in group3) OrderedGroup_ZF_1_L5AA:

assumes A1: \( a\in G \) and A2: \( 1 \leq a^{-1} \)

shows \( a\leq 1 \)proof
from A2 have \( (a^{-1})^{-1}\leq 1 ^{-1} \) using OrderedGroup_ZF_1_L5
with A1 show \( a\leq 1 \) using OrderedGroup_ZF_1_L1, group_inv_of_inv, group_inv_of_one
qed

If an element is nonnegative, then the inverse is not greater that the unit. Also shows that nonnegative elements cannot be negative

lemma (in group3) OrderedGroup_ZF_1_L5AB:

assumes A1: \( 1 \leq a \)

shows \( a^{-1}\leq 1 \) and \( \neg (a\leq 1 \wedge a\neq 1 ) \)proof
from A1 have \( a^{-1}\leq 1 ^{-1} \) using OrderedGroup_ZF_1_L5
then show \( a^{-1}\leq 1 \) using OrderedGroup_ZF_1_L1, group_inv_of_one
{
assume \( a\leq 1 \) and \( a\neq 1 \)
with A1 have \( False \) using group_order_antisym
}
then show \( \neg (a\leq 1 \wedge a\neq 1 ) \)
qed

If two elements are greater or equal than the unit, then the inverse of one is not greater than the other.

lemma (in group3) OrderedGroup_ZF_1_L5AC:

assumes A1: \( 1 \leq a \), \( 1 \leq b \)

shows \( a^{-1} \leq b \)proof
from A1 have \( a^{-1}\leq 1 \), \( 1 \leq b \) using OrderedGroup_ZF_1_L5AB
then show \( a^{-1} \leq b \) by (rule Group_order_transitive )
qed

Inequalities

This section developes some simple tools to deal with inequalities.

Taking negative on both sides reverses the inequality, case with an inverse on one side.

lemma (in group3) OrderedGroup_ZF_1_L5AD:

assumes A1: \( b \in G \) and A2: \( a\leq b^{-1} \)

shows \( b \leq a^{-1} \)proof
from A2 have \( (b^{-1})^{-1} \leq a^{-1} \) using OrderedGroup_ZF_1_L5
with A1 show \( b \leq a^{-1} \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
qed

We can cancel the same element on both sides of an inequality.

lemma (in group3) OrderedGroup_ZF_1_L5AE:

assumes A1: \( a\in G \), \( b\in G \), \( c\in G \) and A2: \( a\cdot b \leq a\cdot c \)

shows \( b\leq c \)proof
from ordGroupAssum, A1, A2 have \( a^{-1}\cdot (a\cdot b) \leq a^{-1}\cdot (a\cdot c) \) using OrderedGroup_ZF_1_L1, inverse_in_group, IsAnOrdGroup_def
with A1 show \( b\leq c \) using OrderedGroup_ZF_1_L1, inv_cancel_two
qed

We can cancel the same element on both sides of an inequality, right side.

lemma (in group3) ineq_cancel_right:

assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\cdot b \leq c\cdot b \)

shows \( a\leq c \)proof
from assms(2,4) have \( (a\cdot b)\cdot b^{-1} \leq (c\cdot b)\cdot b^{-1} \) using OrderedGroup_ZF_1_L1, inverse_in_group, ord_transl_inv(1)
with assms(1,2,3) show \( a\leq c \) using OrderedGroup_ZF_1_L1, inv_cancel_two(2)
qed

We can cancel the same element on both sides of an inequality, a version with an inverse on both sides.

lemma (in group3) OrderedGroup_ZF_1_L5AF:

assumes A1: \( a\in G \), \( b\in G \), \( c\in G \) and A2: \( a\cdot b^{-1} \leq a\cdot c^{-1} \)

shows \( c\leq b \)proof
from A1, A2 have \( (c^{-1})^{-1} \leq (b^{-1})^{-1} \) using OrderedGroup_ZF_1_L1, inverse_in_group, OrderedGroup_ZF_1_L5AE, OrderedGroup_ZF_1_L5
with A1 show \( c\leq b \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
qed

Taking negative on both sides reverses the inequality, another case with an inverse on one side.

lemma (in group3) OrderedGroup_ZF_1_L5AG:

assumes A1: \( a \in G \) and A2: \( a^{-1}\leq b \)

shows \( b^{-1} \leq a \)proof
from A2 have \( b^{-1} \leq (a^{-1})^{-1} \) using OrderedGroup_ZF_1_L5
with A1 show \( b^{-1} \leq a \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
qed

We can multiply the sides of two inequalities.

lemma (in group3) OrderedGroup_ZF_1_L5B:

assumes A1: \( a\leq b \) and A2: \( c\leq d \)

shows \( a\cdot c \leq b\cdot d \)proof
from A1, A2 have \( c\in G \), \( b\in G \) using OrderedGroup_ZF_1_L4
with A1, A2, ordGroupAssum have \( a\cdot c\leq b\cdot c \), \( b\cdot c\leq b\cdot d \) using IsAnOrdGroup_def
then show \( a\cdot c \leq b\cdot d \) by (rule Group_order_transitive )
qed

We can replace first of the factors on one side of an inequality with a greater one.

lemma (in group3) OrderedGroup_ZF_1_L5C:

assumes A1: \( c\in G \) and A2: \( a\leq b\cdot c \) and A3: \( b\leq b_1 \)

shows \( a\leq b_1\cdot c \)proof
from A1, A3 have \( b\cdot c \leq b_1\cdot c \) using OrderedGroup_ZF_1_L3, OrderedGroup_ZF_1_L5B
with A2 show \( a\leq b_1\cdot c \) by (rule Group_order_transitive )
qed

We can replace second of the factors on one side of an inequality with a greater one.

lemma (in group3) OrderedGroup_ZF_1_L5D:

assumes A1: \( b\in G \) and A2: \( a \leq b\cdot c \) and A3: \( c\leq b_1 \)

shows \( a \leq b\cdot b_1 \)proof
from A1, A3 have \( b\cdot c \leq b\cdot b_1 \) using OrderedGroup_ZF_1_L3, OrderedGroup_ZF_1_L5B
with A2 show \( a\leq b\cdot b_1 \) by (rule Group_order_transitive )
qed

We can replace factors on one side of an inequality with greater ones.

lemma (in group3) OrderedGroup_ZF_1_L5E:

assumes A1: \( a \leq b\cdot c \) and A2: \( b\leq b_1 \), \( c\leq c_1 \)

shows \( a \leq b_1\cdot c_1 \)proof
from A2 have \( b\cdot c \leq b_1\cdot c_1 \) using OrderedGroup_ZF_1_L5B
with A1 show \( a\leq b_1\cdot c_1 \) by (rule Group_order_transitive )
qed

We don't decrease an element of the group by multiplying by one that is nonnegative.

lemma (in group3) OrderedGroup_ZF_1_L5F:

assumes A1: \( 1 \leq a \) and A2: \( b\in G \)

shows \( b\leq a\cdot b \), \( b\leq b\cdot a \)proof
from ordGroupAssum, A1, A2 have \( 1 \cdot b\leq a\cdot b \), \( b\cdot 1 \leq b\cdot a \) using IsAnOrdGroup_def
with A2 show \( b\leq a\cdot b \), \( b\leq b\cdot a \) using OrderedGroup_ZF_1_L1, group0_2_L2
qed

We can multiply the right hand side of an inequality by a nonnegative element.

lemma (in group3) OrderedGroup_ZF_1_L5G:

assumes A1: \( a\leq b \) and A2: \( 1 \leq c \)

shows \( a\leq b\cdot c \), \( a\leq c\cdot b \)proof
from A1, A2 have I: \( b\leq b\cdot c \) and II: \( b\leq c\cdot b \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L5F
from A1, I show \( a\leq b\cdot c \) by (rule Group_order_transitive )
from A1, II show \( a\leq c\cdot b \) by (rule Group_order_transitive )
qed

We can put two elements on the other side of inequality, changing their sign.

lemma (in group3) OrderedGroup_ZF_1_L5H:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( a\cdot b^{-1} \leq c \)

shows \( a \leq c\cdot b \), \( c^{-1}\cdot a \leq b \)proof
from A2 have T: \( c\in G \), \( c^{-1} \in G \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L1, inverse_in_group
from ordGroupAssum, A1, A2 have \( a\cdot b^{-1}\cdot b \leq c\cdot b \) using IsAnOrdGroup_def
with A1 show \( a \leq c\cdot b \) using OrderedGroup_ZF_1_L1, inv_cancel_two
with ordGroupAssum, A2, T have \( c^{-1}\cdot a \leq c^{-1}\cdot (c\cdot b) \) using IsAnOrdGroup_def
with A1, T show \( c^{-1}\cdot a \leq b \) using OrderedGroup_ZF_1_L1, inv_cancel_two
qed

We can multiply the sides of one inequality by inverse of another.

lemma (in group3) OrderedGroup_ZF_1_L5I:

assumes \( a\leq b \) and \( c\leq d \)

shows \( a\cdot d^{-1} \leq b\cdot c^{-1} \) using assms, OrderedGroup_ZF_1_L5, OrderedGroup_ZF_1_L5B

We can put an element on the other side of an inequality changing its sign, version with the inverse.

lemma (in group3) OrderedGroup_ZF_1_L5J:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( c \leq a\cdot b^{-1} \)

shows \( c\cdot b \leq a \)proof
from ordGroupAssum, A1, A2 have \( c\cdot b \leq a\cdot b^{-1}\cdot b \) using IsAnOrdGroup_def
with A1 show \( c\cdot b \leq a \) using OrderedGroup_ZF_1_L1, inv_cancel_two
qed

We can put an element on the other side of an inequality changing its sign, version with the inverse.

lemma (in group3) OrderedGroup_ZF_1_L5JA:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( c \leq a^{-1}\cdot b \)

shows \( a\cdot c\leq b \)proof
from ordGroupAssum, A1, A2 have \( a\cdot c \leq a\cdot (a^{-1}\cdot b) \) using IsAnOrdGroup_def
with A1 show \( a\cdot c\leq b \) using OrderedGroup_ZF_1_L1, inv_cancel_two
qed

A special case of OrderedGroup_ZF_1_L5J where \(c=1\).

corollary (in group3) OrderedGroup_ZF_1_L5K:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( 1 \leq a\cdot b^{-1} \)

shows \( b \leq a \)proof
from A1, A2 have \( 1 \cdot b \leq a \) using OrderedGroup_ZF_1_L5J
with A1 show \( b \leq a \) using OrderedGroup_ZF_1_L1, group0_2_L2
qed

A special case of OrderedGroup_ZF_1_L5JA where \(c=1\).

corollary (in group3) OrderedGroup_ZF_1_L5KA:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( 1 \leq a^{-1}\cdot b \)

shows \( a \leq b \)proof
from A1, A2 have \( a\cdot 1 \leq b \) using OrderedGroup_ZF_1_L5JA
with A1 show \( a \leq b \) using OrderedGroup_ZF_1_L1, group0_2_L2
qed

If the order is total, the elements that do not belong to the positive set are negative. We also show here that the group inverse of an element that does not belong to the nonnegative set does belong to the nonnegative set.

lemma (in group3) OrderedGroup_ZF_1_L6:

assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G-G^+ \)

shows \( a\leq 1 \), \( a^{-1} \in G^+ \), \( \text{restrict}( \text{GroupInv}(G,P),G-G^+)(a) \in G^+ \)proof
from A2 have T1: \( a\in G \), \( a\notin G^+ \), \( 1 \in G \) using OrderedGroup_ZF_1_L1, group0_2_L2
with A1 show \( a\leq 1 \) using OrderedGroup_ZF_1_L2, IsTotal_def
then show \( a^{-1} \in G^+ \) using OrderedGroup_ZF_1_L5A, OrderedGroup_ZF_1_L2
with A2 show \( \text{restrict}( \text{GroupInv}(G,P),G-G^+)(a) \in G^+ \) using restrict
qed

If a property is invariant with respect to taking the inverse and it is true on the nonnegative set, than it is true on the whole group.

lemma (in group3) OrderedGroup_ZF_1_L7:

assumes A1: \( r \text{ is total on } G \) and A2: \( \forall a\in G^+.\ \forall b\in G^+.\ Q(a,b) \) and A3: \( \forall a\in G.\ \forall b\in G.\ Q(a,b)\longrightarrow Q(a^{-1},b) \) and A4: \( \forall a\in G.\ \forall b\in G.\ Q(a,b)\longrightarrow Q(a,b^{-1}) \) and A5: \( a\in G \), \( b\in G \)

shows \( Q(a,b) \)proof
{
assume A6: \( a\in G^+ \)
have \( Q(a,b) \)proof
{
assume \( b\in G^+ \)
with A6, A2 have \( Q(a,b) \)
}
moreover {
assume \( b\notin G^+ \)
with A1, A2, A4, A5, A6 have \( Q(a,(b^{-1})^{-1}) \) using OrderedGroup_ZF_1_L6, OrderedGroup_ZF_1_L1, inverse_in_group
with A5 have \( Q(a,b) \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
} ultimately show \( Q(a,b) \)
qed
}
moreover {
assume \( a\notin G^+ \)
with A1, A5 have T1: \( a^{-1} \in G^+ \) using OrderedGroup_ZF_1_L6
have \( Q(a,b) \)proof
{
assume \( b\in G^+ \)
with A2, A3, A5, T1 have \( Q((a^{-1})^{-1},b) \) using OrderedGroup_ZF_1_L1, inverse_in_group
with A5 have \( Q(a,b) \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
}
moreover {
assume \( b\notin G^+ \)
with A1, A2, A3, A4, A5, T1 have \( Q((a^{-1})^{-1},(b^{-1})^{-1}) \) using OrderedGroup_ZF_1_L6, OrderedGroup_ZF_1_L1, inverse_in_group
with A5 have \( Q(a,b) \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
} ultimately show \( Q(a,b) \)
qed
} ultimately show \( Q(a,b) \)
qed

A lemma about splitting the ordered group "plane" into 6 subsets. Useful for proofs by cases.

lemma (in group3) OrdGroup_6cases:

assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \), \( b\in G \)

shows \( 1 \leq a \wedge 1 \leq b \vee a\leq 1 \wedge b\leq 1 \vee \) \( a\leq 1 \wedge 1 \leq b \wedge 1 \leq a\cdot b \vee a\leq 1 \wedge 1 \leq b \wedge a\cdot b \leq 1 \vee \) \( 1 \leq a \wedge b\leq 1 \wedge 1 \leq a\cdot b \vee 1 \leq a \wedge b\leq 1 \wedge a\cdot b \leq 1 \)proof
from A1, A2 have \( 1 \leq a \vee a\leq 1 \), \( 1 \leq b \vee b\leq 1 \), \( 1 \leq a\cdot b \vee a\cdot b \leq 1 \) using OrderedGroup_ZF_1_L1, group_op_closed, group0_2_L2, IsTotal_def
then show \( thesis \)
qed

The next lemma shows what happens when one element of a totally ordered group is not greater or equal than another.

lemma (in group3) OrderedGroup_ZF_1_L8:

assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \), \( b\in G \) and A3: \( \neg (a\leq b) \)

shows \( b \leq a \), \( a^{-1} \leq b^{-1} \), \( a\neq b \), \( b \lt a \)proof
from A1, A2, A3 show I: \( b \leq a \) using IsTotal_def
then show \( a^{-1} \leq b^{-1} \) using OrderedGroup_ZF_1_L5
from A2 have \( a \leq a \) using OrderedGroup_ZF_1_L3
with I, A3 show \( a\neq b \), \( b \lt a \)
qed

If one element is greater or equal and not equal to another, then it is not smaller or equal.

lemma (in group3) OrderedGroup_ZF_1_L8AA:

assumes A1: \( a\leq b \) and A2: \( a\neq b \)

shows \( \neg (b\leq a) \)proof
{
note A1
moreover
assume \( b\leq a \)
ultimately have \( a=b \) by (rule group_order_antisym )
with A2 have \( False \)
}
thus \( \neg (b\leq a) \)
qed

A special case of OrderedGroup_ZF_1_L8 when one of the elements is the unit.

corollary (in group3) OrderedGroup_ZF_1_L8A:

assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \) and A3: \( \neg (1 \leq a) \)

shows \( 1 \leq a^{-1} \), \( 1 \neq a \), \( a\leq 1 \)proof
from A1, A2, A3 have I: \( r \text{ is total on } G \), \( 1 \in G \), \( a\in G \), \( \neg (1 \leq a) \) using OrderedGroup_ZF_1_L1, group0_2_L2
then have \( 1 ^{-1} \leq a^{-1} \) by (rule OrderedGroup_ZF_1_L8 )
then show \( 1 \leq a^{-1} \) using OrderedGroup_ZF_1_L1, group_inv_of_one
from I show \( 1 \neq a \) by (rule OrderedGroup_ZF_1_L8 )
from A1, I show \( a\leq 1 \) using IsTotal_def
qed

A negative element can not be nonnegative.

lemma (in group3) OrderedGroup_ZF_1_L8B:

assumes A1: \( a\leq 1 \) and A2: \( a\neq 1 \)

shows \( \neg (1 \leq a) \)proof
{
assume \( 1 \leq a \)
with A1 have \( a=1 \) using group_order_antisym
with A2 have \( False \)
}
thus \( thesis \)
qed

An element is greater or equal than another iff the difference is nonpositive.

lemma (in group3) OrderedGroup_ZF_1_L9:

assumes A1: \( a\in G \), \( b\in G \)

shows \( a\leq b \longleftrightarrow a\cdot b^{-1} \leq 1 \)proof
assume \( a \leq b \)
with ordGroupAssum, A1 have \( a\cdot b^{-1} \leq b\cdot b^{-1} \) using OrderedGroup_ZF_1_L1, inverse_in_group, IsAnOrdGroup_def
with A1 show \( a\cdot b^{-1} \leq 1 \) using OrderedGroup_ZF_1_L1, group0_2_L6
next
assume A2: \( a\cdot b^{-1} \leq 1 \)
with ordGroupAssum, A1 have \( a\cdot b^{-1}\cdot b \leq 1 \cdot b \) using IsAnOrdGroup_def
with A1 show \( a \leq b \) using OrderedGroup_ZF_1_L1, inv_cancel_two, group0_2_L2
qed

We can move an element to the other side of an inequality.

lemma (in group3) OrderedGroup_ZF_1_L9A:

assumes A1: \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b \leq c \longleftrightarrow a \leq c\cdot b^{-1} \)proof
assume \( a\cdot b \leq c \)
with ordGroupAssum, A1 have \( a\cdot b\cdot b^{-1} \leq c\cdot b^{-1} \) using OrderedGroup_ZF_1_L1, inverse_in_group, IsAnOrdGroup_def
with A1 show \( a \leq c\cdot b^{-1} \) using OrderedGroup_ZF_1_L1, inv_cancel_two
next
assume \( a \leq c\cdot b^{-1} \)
with ordGroupAssum, A1 have \( a\cdot b \leq c\cdot b^{-1}\cdot b \) using OrderedGroup_ZF_1_L1, inverse_in_group, IsAnOrdGroup_def
with A1 show \( a\cdot b \leq c \) using OrderedGroup_ZF_1_L1, inv_cancel_two
qed

A one side version of the previous lemma with weaker assuptions.

lemma (in group3) OrderedGroup_ZF_1_L9B:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( a\cdot b^{-1} \leq c \)

shows \( a \leq c\cdot b \)proof
from A1, A2 have \( a\in G \), \( b^{-1}\in G \), \( c\in G \) using OrderedGroup_ZF_1_L1, inverse_in_group, OrderedGroup_ZF_1_L4
with A1, A2 show \( a \leq c\cdot b \) using OrderedGroup_ZF_1_L9A, OrderedGroup_ZF_1_L1, group_inv_of_inv
qed

We can put en element on the other side of inequality, changing its sign.

lemma (in group3) OrderedGroup_ZF_1_L9C:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( c\leq a\cdot b \)

shows \( c\cdot b^{-1} \leq a \), \( a^{-1}\cdot c \leq b \)proof
from ordGroupAssum, A1, A2 have \( c\cdot b^{-1} \leq a\cdot b\cdot b^{-1} \), \( a^{-1}\cdot c \leq a^{-1}\cdot (a\cdot b) \) using OrderedGroup_ZF_1_L1, inverse_in_group, IsAnOrdGroup_def
with A1 show \( c\cdot b^{-1} \leq a \), \( a^{-1}\cdot c \leq b \) using OrderedGroup_ZF_1_L1, inv_cancel_two
qed

If an element is greater or equal than another then the difference is nonnegative.

lemma (in group3) OrderedGroup_ZF_1_L9D:

assumes A1: \( a\leq b \)

shows \( 1 \leq b\cdot a^{-1} \)proof
from A1 have T: \( a\in G \), \( b\in G \), \( a^{-1} \in G \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L1, inverse_in_group
with ordGroupAssum, A1 have \( a\cdot a^{-1} \leq b\cdot a^{-1} \) using IsAnOrdGroup_def
with T show \( 1 \leq b\cdot a^{-1} \) using OrderedGroup_ZF_1_L1, group0_2_L6
qed

If an element is greater than another then the difference is positive.

lemma (in group3) OrderedGroup_ZF_1_L9E:

assumes A1: \( a\leq b \), \( a\neq b \)

shows \( 1 \leq b\cdot a^{-1} \), \( 1 \neq b\cdot a^{-1} \), \( b\cdot a^{-1} \in G_+ \)proof
from A1 have T: \( a\in G \), \( b\in G \) using OrderedGroup_ZF_1_L4
from A1 show I: \( 1 \leq b\cdot a^{-1} \) using OrderedGroup_ZF_1_L9D
{
assume \( b\cdot a^{-1} = 1 \)
with T have \( a=b \) using OrderedGroup_ZF_1_L1, group0_2_L11A
with A1 have \( False \)
}
then show \( 1 \neq b\cdot a^{-1} \)
then have \( b\cdot a^{-1} \neq 1 \)
with I show \( b\cdot a^{-1} \in G_+ \) using OrderedGroup_ZF_1_L2A
qed

If the difference is nonnegative, then \(a\leq b\).

lemma (in group3) OrderedGroup_ZF_1_L9F:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( 1 \leq b\cdot a^{-1} \)

shows \( a\leq b \)proof
from A1, A2 have \( 1 \cdot a \leq b \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L9A
with A1 show \( a\leq b \) using OrderedGroup_ZF_1_L1, group0_2_L2
qed

If we increase the middle term in a product, the whole product increases.

lemma (in group3) OrderedGroup_ZF_1_L10:

assumes \( a\in G \), \( b\in G \) and \( c\leq d \)

shows \( a\cdot c\cdot b \leq a\cdot d\cdot b \) using ordGroupAssum, assms, IsAnOrdGroup_def

A product of (strictly) positive elements is not the unit.

lemma (in group3) OrderedGroup_ZF_1_L11:

assumes A1: \( 1 \leq a \), \( 1 \leq b \) and A2: \( 1 \neq a \), \( 1 \neq b \)

shows \( 1 \neq a\cdot b \)proof
from A1 have T1: \( a\in G \), \( b\in G \) using OrderedGroup_ZF_1_L4
{
assume \( 1 = a\cdot b \)
with A1, T1 have \( a\leq 1 \), \( 1 \leq a \) using OrderedGroup_ZF_1_L1, group0_2_L9, OrderedGroup_ZF_1_L5AA
then have \( a = 1 \) by (rule group_order_antisym )
with A2 have \( False \)
}
then show \( 1 \neq a\cdot b \)
qed

A product of nonnegative elements is nonnegative.

lemma (in group3) OrderedGroup_ZF_1_L12:

assumes A1: \( 1 \leq a \), \( 1 \leq b \)

shows \( 1 \leq a\cdot b \)proof
from A1 have \( 1 \cdot 1 \leq a\cdot b \) using OrderedGroup_ZF_1_L5B
then show \( 1 \leq a\cdot b \) using OrderedGroup_ZF_1_L1, group0_2_L2
qed

If \(a\) is not greater than \(b\), then \(1\) is not greater than \(b\cdot a^{-1}\).

lemma (in group3) OrderedGroup_ZF_1_L12A:

assumes A1: \( a\leq b \)

shows \( 1 \leq b\cdot a^{-1} \)proof
from A1 have T: \( 1 \in G \), \( a\in G \), \( b\in G \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L1, group0_2_L2
with A1 have \( 1 \cdot a \leq b \) using OrderedGroup_ZF_1_L1, group0_2_L2
with T show \( 1 \leq b\cdot a^{-1} \) using OrderedGroup_ZF_1_L9A
qed

We can move an element to the other side of a strict inequality.

lemma (in group3) OrderedGroup_ZF_1_L12B:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( a\cdot b^{-1} \lt c \)

shows \( a \lt c\cdot b \)proof
from A1, A2 have \( a\cdot b^{-1}\cdot b \lt c\cdot b \) using group_strict_ord_transl_inv
moreover
from A1 have \( a\cdot b^{-1}\cdot b = a \) using OrderedGroup_ZF_1_L1, inv_cancel_two
ultimately show \( a \lt c\cdot b \)
qed

We can multiply the sides of two inequalities, first of them strict and we get a strict inequality.

lemma (in group3) OrderedGroup_ZF_1_L12C:

assumes A1: \( a \lt b \) and A2: \( c\leq d \)

shows \( a\cdot c \lt b\cdot d \)proof
from A1, A2 have T: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \) using OrderedGroup_ZF_1_L4
with ordGroupAssum, A2 have \( a\cdot c \leq a\cdot d \) using IsAnOrdGroup_def
moreover
from A1, T have \( a\cdot d \lt b\cdot d \) using group_strict_ord_transl_inv
ultimately show \( a\cdot c \lt b\cdot d \) by (rule group_strict_ord_transit )
qed

We can multiply the sides of two inequalities, second of them strict and we get a strict inequality.

lemma (in group3) OrderedGroup_ZF_1_L12D:

assumes A1: \( a\leq b \) and A2: \( c \lt d \)

shows \( a\cdot c \lt b\cdot d \)proof
from A1, A2 have T: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \) using OrderedGroup_ZF_1_L4
with A2 have \( a\cdot c \lt a\cdot d \) using group_strict_ord_transl_inv
moreover
from ordGroupAssum, A1, T have \( a\cdot d \leq b\cdot d \) using IsAnOrdGroup_def
ultimately show \( a\cdot c \lt b\cdot d \) by (rule OrderedGroup_ZF_1_L4A )
qed

The set of positive elements

In this section we study \( G_+ \) - the set of elements that are (strictly) greater than the unit. The most important result is that every linearly ordered group can decomposed into \(\{1\}\), \( G_+ \) and the set of those elements \(a\in G\) such that \(a^{-1}\in\)\( G_+ \). Another property of linearly ordered groups that we prove here is that if \( G_+ \)\(\neq \emptyset\), then it is infinite. This allows to show that nontrivial linearly ordered groups are infinite.

The positive set is closed under the group operation.

lemma (in group3) OrderedGroup_ZF_1_L13:

shows \( G_+ \text{ is closed under } P \)proof
{
fix \( a \) \( b \)
assume \( a\in G_+ \), \( b\in G_+ \)
then have T1: \( 1 \leq a\cdot b \) and \( 1 \neq a\cdot b \) using PositiveSet_def, OrderedGroup_ZF_1_L11, OrderedGroup_ZF_1_L12
moreover
from T1 have \( a\cdot b \in G \) using OrderedGroup_ZF_1_L4
ultimately have \( a\cdot b \in G_+ \) using PositiveSet_def
}
then show \( G_+ \text{ is closed under } P \) using IsOpClosed_def
qed

For totally ordered groups every nonunit element is positive or its inverse is positive.

lemma (in group3) OrderedGroup_ZF_1_L14:

assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \)

shows \( a=1 \vee a\in G_+ \vee a^{-1}\in G_+ \)proof
{
assume A3: \( a\neq 1 \)
moreover
from A1, A2 have \( a\leq 1 \vee 1 \leq a \) using IsTotal_def, OrderedGroup_ZF_1_L1, group0_2_L2
moreover
from A3, A2 have T1: \( a^{-1} \neq 1 \) using OrderedGroup_ZF_1_L1, group0_2_L8B
ultimately have \( a^{-1}\in G_+ \vee a\in G_+ \) using OrderedGroup_ZF_1_L5A, OrderedGroup_ZF_1_L2A
}
thus \( a=1 \vee a\in G_+ \vee a^{-1}\in G_+ \)
qed

If an element belongs to the positive set, then it is not the unit and its inverse does not belong to the positive set.

lemma (in group3) OrderedGroup_ZF_1_L15:

assumes A1: \( a\in G_+ \)

shows \( a\neq 1 \), \( a^{-1}\notin G_+ \)proof
from A1 show T1: \( a\neq 1 \) using PositiveSet_def
{
assume \( a^{-1} \in G_+ \)
with A1 have \( a\leq 1 \), \( 1 \leq a \) using OrderedGroup_ZF_1_L5AA, PositiveSet_def
then have \( a=1 \) by (rule group_order_antisym )
with T1 have \( False \)
}
then show \( a^{-1}\notin G_+ \)
qed

If \(a^{-1}\) is positive, then \(a\) can not be positive or the unit.

lemma (in group3) OrderedGroup_ZF_1_L16:

assumes A1: \( a\in G \) and A2: \( a^{-1}\in G_+ \)

shows \( a\neq 1 \), \( a\notin G_+ \)proof
from A2 have \( a^{-1}\neq 1 \), \( (a^{-1})^{-1} \notin G_+ \) using OrderedGroup_ZF_1_L15
with A1 show \( a\neq 1 \), \( a\notin G_+ \) using OrderedGroup_ZF_1_L1, group0_2_L8C, group_inv_of_inv
qed

For linearly ordered groups each element is either the unit, positive or its inverse is positive.

lemma (in group3) OrdGroup_decomp:

assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \)

shows \( \text{Exactly_1_of_3_holds} (a=1 ,a\in G_+,a^{-1}\in G_+) \)proof
from A1, A2 have \( a=1 \vee a\in G_+ \vee a^{-1}\in G_+ \) using OrderedGroup_ZF_1_L14
moreover
from A2 have \( a=1 \longrightarrow (a\notin G_+ \wedge a^{-1}\notin G_+) \) using OrderedGroup_ZF_1_L1, group_inv_of_one, PositiveSet_def
moreover
from A2 have \( a\in G_+ \longrightarrow (a\neq 1 \wedge a^{-1}\notin G_+) \) using OrderedGroup_ZF_1_L15
moreover
from A2 have \( a^{-1}\in G_+ \longrightarrow (a\neq 1 \wedge a\notin G_+) \) using OrderedGroup_ZF_1_L16
ultimately show \( \text{Exactly_1_of_3_holds} (a=1 ,a\in G_+,a^{-1}\in G_+) \) by (rule Fol1_L5 )
qed

A if \(a\) is a nonunit element that is not positive, then \(a^{-1}\) is is positive. This is useful for some proofs by cases.

lemma (in group3) OrdGroup_cases:

assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \) and A3: \( a\neq 1 \), \( a\notin G_+ \)

shows \( a^{-1} \in G_+ \)proof
from A1, A2 have \( a=1 \vee a\in G_+ \vee a^{-1}\in G_+ \) using OrderedGroup_ZF_1_L14
with A3 show \( a^{-1} \in G_+ \)
qed

Elements from \(G\setminus G_+\) are not greater that the unit.

lemma (in group3) OrderedGroup_ZF_1_L17:

assumes A1: \( r \text{ is total on } G \) and A2: \( a \in G-G_+ \)

shows \( a\leq 1 \)proof
{
assume \( a=1 \)
with A2 have \( a\leq 1 \) using OrderedGroup_ZF_1_L3
}
moreover {
assume \( a\neq 1 \)
with A1, A2 have \( a\leq 1 \) using PositiveSet_def, OrderedGroup_ZF_1_L8A
} ultimately show \( a\leq 1 \)
qed

The next lemma allows to split proofs that something holds for all \(a\in G\) into cases \(a=1\), \(a\in G_+\), \(-a\in G_+\).

lemma (in group3) OrderedGroup_ZF_1_L18:

assumes A1: \( r \text{ is total on } G \) and A2: \( b\in G \) and A3: \( Q(1 ) \) and A4: \( \forall a\in G_+.\ Q(a) \) and A5: \( \forall a\in G_+.\ Q(a^{-1}) \)

shows \( Q(b) \)proof
from A1, A2, A3, A4, A5 have \( Q(b) \vee Q((b^{-1})^{-1}) \) using OrderedGroup_ZF_1_L14
with A2 show \( Q(b) \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
qed

All elements greater or equal than an element of \( G_+ \) belong to \( G_+ \).

lemma (in group3) OrderedGroup_ZF_1_L19:

assumes A1: \( a \in G_+ \) and A2: \( a\leq b \)

shows \( b \in G_+ \)proof
from A1 have I: \( 1 \leq a \) and II: \( a\neq 1 \) using OrderedGroup_ZF_1_L2A
from I, A2 have \( 1 \leq b \) by (rule Group_order_transitive )
moreover
have \( b\neq 1 \)proof
{
assume \( b=1 \)
with I, A2 have \( 1 \leq a \), \( a\leq 1 \)
then have \( 1 =a \) by (rule group_order_antisym )
with II have \( False \)
}
then show \( b\neq 1 \)
qed
ultimately show \( b \in G_+ \) using OrderedGroup_ZF_1_L2A
qed

The inverse of an element of \( G_+ \) cannot be in \( G_+ \).

lemma (in group3) OrderedGroup_ZF_1_L20:

assumes A1: \( r \text{ is total on } G \) and A2: \( a \in G_+ \)

shows \( a^{-1} \notin G_+ \)proof
from A2 have \( a\in G \) using PositiveSet_def
with A1 have \( \text{Exactly_1_of_3_holds} (a=1 ,a\in G_+,a^{-1}\in G_+) \) using OrdGroup_decomp
with A2 show \( a^{-1} \notin G_+ \) by (rule Fol1_L7 )
qed

The set of positive elements of a nontrivial linearly ordered group is not empty.

lemma (in group3) OrderedGroup_ZF_1_L21:

assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \)

shows \( G_+ \neq 0 \)proof
have \( 1 \in G \) using OrderedGroup_ZF_1_L1, group0_2_L2
with A2 obtain \( a \) where \( a\in G \), \( a\neq 1 \)
with A1 have \( a\in G_+ \vee a^{-1}\in G_+ \) using OrderedGroup_ZF_1_L14
then show \( G_+ \neq 0 \)
qed

If \(b\in\)\( G_+ \), then \(a < a\cdot b\). Multiplying \(a\) by a positive elemnt increases \(a\).

lemma (in group3) OrderedGroup_ZF_1_L22:

assumes A1: \( a\in G \), \( b\in G_+ \)

shows \( a\leq a\cdot b \), \( a \neq a\cdot b \), \( a\cdot b \in G \)proof
from ordGroupAssum, A1 have \( a\cdot 1 \leq a\cdot b \) using OrderedGroup_ZF_1_L2A, IsAnOrdGroup_def
with A1 show \( a\leq a\cdot b \) using OrderedGroup_ZF_1_L1, group0_2_L2
then show \( a\cdot b \in G \) using OrderedGroup_ZF_1_L4
{
from A1 have \( a\in G \), \( b\in G \) using PositiveSet_def
moreover
assume \( a = a\cdot b \)
ultimately have \( b = 1 \) using OrderedGroup_ZF_1_L1, group0_2_L7
with A1 have \( False \) using PositiveSet_def
}
then show \( a \neq a\cdot b \)
qed

If \(G\) is a nontrivial linearly ordered hroup, then for every element of \(G\) we can find one in \( G_+ \) that is greater or equal.

lemma (in group3) OrderedGroup_ZF_1_L23:

assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( a\in G \)

shows \( \exists b\in G_+.\ a\leq b \)proof
{
assume A4: \( a\in G_+ \)
then have \( a\leq a \) using PositiveSet_def, OrderedGroup_ZF_1_L3
with A4 have \( \exists b\in G_+.\ a\leq b \)
}
moreover {
assume \( a\notin G_+ \)
with A1, A3 have I: \( a\leq 1 \) using OrderedGroup_ZF_1_L17
from A1, A2 obtain \( b \) where II: \( b\in G_+ \) using OrderedGroup_ZF_1_L21
then have \( 1 \leq b \) using PositiveSet_def
with I have \( a\leq b \) by (rule Group_order_transitive )
with II have \( \exists b\in G_+.\ a\leq b \)
} ultimately show \( thesis \)
qed

The \( G^+ \) is \( G_+ \) plus the unit.

lemma (in group3) OrderedGroup_ZF_1_L24:

shows \( G^+ = G_+\cup \{1 \} \) using OrderedGroup_ZF_1_L2, OrderedGroup_ZF_1_L2A, OrderedGroup_ZF_1_L3A

What is \(-G_+\), really?

lemma (in group3) OrderedGroup_ZF_1_L25:

shows \( (-G_+) = \{a^{-1}.\ a\in G_+\} \), \( (-G_+) \subseteq G \)proof
from ordGroupAssum have I: \( \text{GroupInv}(G,P) : G\rightarrow G \) using IsAnOrdGroup_def, group0_2_T2
moreover
have \( G_+ \subseteq G \) using PositiveSet_def
ultimately show \( (-G_+) = \{a^{-1}.\ a\in G_+\} \), \( (-G_+) \subseteq G \) using func_imagedef, func1_1_L6
qed

If the inverse of \(a\) is in \( G_+ \), then \(a\) is in the inverse of \( G_+ \).

lemma (in group3) OrderedGroup_ZF_1_L26:

assumes A1: \( a\in G \) and A2: \( a^{-1} \in G_+ \)

shows \( a \in (-G_+) \)proof
from A1 have \( a^{-1} \in G \), \( a = (a^{-1})^{-1} \) using OrderedGroup_ZF_1_L1, inverse_in_group, group_inv_of_inv
with A2 show \( a \in (-G_+) \) using OrderedGroup_ZF_1_L25
qed

If \(a\) is in the inverse of \( G_+ \), then its inverse is in \(G_+\).

lemma (in group3) OrderedGroup_ZF_1_L27:

assumes \( a \in (-G_+) \)

shows \( a^{-1} \in G_+ \) using assms, OrderedGroup_ZF_1_L25, PositiveSet_def, OrderedGroup_ZF_1_L1, group_inv_of_inv

A linearly ordered group can be decomposed into \(G_+\), \(\{1\}\) and \(-G_+\)

lemma (in group3) OrdGroup_decomp2:

assumes A1: \( r \text{ is total on } G \)

shows \( G = G_+ \cup (-G_+)\cup \{1 \} \), \( G_+\cap (-G_+) = 0 \), \( 1 \notin G_+\cup (-G_+) \)proof
{
fix \( a \)
assume A2: \( a\in G \)
with A1 have \( a\in G_+ \vee a^{-1}\in G_+ \vee a=1 \) using OrderedGroup_ZF_1_L14
with A2 have \( a\in G_+ \vee a\in (-G_+) \vee a=1 \) using OrderedGroup_ZF_1_L26
then have \( a \in (G_+ \cup (-G_+)\cup \{1 \}) \)
}
then have \( G \subseteq G_+ \cup (-G_+)\cup \{1 \} \)
moreover
have \( G_+ \cup (-G_+)\cup \{1 \} \subseteq G \) using OrderedGroup_ZF_1_L25, PositiveSet_def, OrderedGroup_ZF_1_L1, group0_2_L2
ultimately show \( G = G_+ \cup (-G_+)\cup \{1 \} \)
{
let \( A = G_+\cap (-G_+) \)
assume \( G_+\cap (-G_+) \neq 0 \)
then have \( A\neq 0 \)
then obtain \( a \) where \( a\in A \)
then have \( False \) using OrderedGroup_ZF_1_L15, OrderedGroup_ZF_1_L27
}
then show \( G_+\cap (-G_+) = 0 \)
show \( 1 \notin G_+\cup (-G_+) \) using OrderedGroup_ZF_1_L27, OrderedGroup_ZF_1_L1, group_inv_of_one, OrderedGroup_ZF_1_L2A
qed

If \(a\cdot b^{-1}\) is nonnegative, then \(b \leq a\). This maybe used to recover the order from the set of nonnegative elements and serve as a way to define order by prescibing that set (see the "Alternative definitions" section).

lemma (in group3) OrderedGroup_ZF_1_L28:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( a\cdot b^{-1} \in G^+ \)

shows \( b\leq a \)proof
from A2 have \( 1 \leq a\cdot b^{-1} \) using OrderedGroup_ZF_1_L2
with A1 show \( b\leq a \) using OrderedGroup_ZF_1_L5K
qed

A special case of OrderedGroup_ZF_1_L28 when \(a\cdot b^{-1}\) is positive.

corollary (in group3) OrderedGroup_ZF_1_L29:

assumes A1: \( a\in G \), \( b\in G \) and A2: \( a\cdot b^{-1} \in G_+ \)

shows \( b\leq a \), \( b\neq a \)proof
from A2 have \( 1 \leq a\cdot b^{-1} \) and I: \( a\cdot b^{-1} \neq 1 \) using OrderedGroup_ZF_1_L2A
with A1 show \( b\leq a \) using OrderedGroup_ZF_1_L5K
from A1, I show \( b\neq a \) using OrderedGroup_ZF_1_L1, group0_2_L6
qed

A bit stronger that OrderedGroup_ZF_1_L29, adds case when two elements are equal.

lemma (in group3) OrderedGroup_ZF_1_L30:

assumes \( a\in G \), \( b\in G \) and \( a=b \vee b\cdot a^{-1} \in G_+ \)

shows \( a\leq b \) using assms, OrderedGroup_ZF_1_L3, OrderedGroup_ZF_1_L29

A different take on decomposition: we can have \(a=b\) or \(a

lemma (in group3) OrderedGroup_ZF_1_L31:

assumes A1: \( r \text{ is total on } G \) and A2: \( a\in G \), \( b\in G \)

shows \( a=b \vee (a\leq b \wedge a\neq b) \vee (b\leq a \wedge b\neq a) \)proof
from A2 have \( a\cdot b^{-1} \in G \) using OrderedGroup_ZF_1_L1, inverse_in_group, group_op_closed
with A1 have \( a\cdot b^{-1} = 1 \vee a\cdot b^{-1} \in G_+ \vee (a\cdot b^{-1})^{-1} \in G_+ \) using OrderedGroup_ZF_1_L14
moreover {
assume \( a\cdot b^{-1} = 1 \)
then have \( a\cdot b^{-1}\cdot b = 1 \cdot b \)
with A2 have \( a=b \vee (a\leq b \wedge a\neq b) \vee (b\leq a \wedge b\neq a) \) using OrderedGroup_ZF_1_L1, inv_cancel_two, group0_2_L2
} moreover {
assume \( a\cdot b^{-1} \in G_+ \)
with A2 have \( a=b \vee (a\leq b \wedge a\neq b) \vee (b\leq a \wedge b\neq a) \) using OrderedGroup_ZF_1_L29
} moreover {
assume \( (a\cdot b^{-1})^{-1} \in G_+ \)
with A2 have \( b\cdot a^{-1} \in G_+ \) using OrderedGroup_ZF_1_L1, group0_2_L12
with A2 have \( a=b \vee (a\leq b \wedge a\neq b) \vee (b\leq a \wedge b\neq a) \) using OrderedGroup_ZF_1_L29
} ultimately show \( a=b \vee (a\leq b \wedge a\neq b) \vee (b\leq a \wedge b\neq a) \)
qed

Intervals and bounded sets

Intervals here are the closed intervals of the form \(\{x\in G. a\leq x \leq b \}\).

A bounded set can be translated to put it in \(G^+\) and then it is still bounded above.

lemma (in group3) OrderedGroup_ZF_2_L1:

assumes A1: \( \forall g\in A.\ L\leq g \wedge g\leq M \) and A2: \( S = \text{RightTranslation}(G,P,L^{-1}) \) and A3: \( a \in S(A) \)

shows \( a \leq M\cdot L^{-1} \), \( 1 \leq a \)proof
from A3 have \( A\neq 0 \) using func1_1_L13A
then obtain \( g \) where \( g\in A \)
with A1 have T1: \( L\in G \), \( M\in G \), \( L^{-1}\in G \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L1, inverse_in_group
with A2 have \( S : G\rightarrow G \) using OrderedGroup_ZF_1_L1, group0_5_L1
moreover
from A1 have T2: \( A\subseteq G \) using OrderedGroup_ZF_1_L4
ultimately have \( S(A) = \{S(b).\ b\in A\} \) using func_imagedef
with A3 obtain \( b \) where T3: \( b\in A \), \( a = S(b) \)
with A1, ordGroupAssum, T1 have \( b\cdot L^{-1}\leq M\cdot L^{-1} \), \( L\cdot L^{-1}\leq b\cdot L^{-1} \) using IsAnOrdGroup_def
with T3, A2, T1, T2 show \( a\leq M\cdot L^{-1} \), \( 1 \leq a \) using OrderedGroup_ZF_1_L1, group0_5_L2, group0_2_L6
qed

Every bounded set is an image of a subset of an interval that starts at \(1\).

lemma (in group3) OrderedGroup_ZF_2_L2:

assumes A1: \( \text{IsBounded}(A,r) \)

shows \( \exists B.\ \exists g\in G^+.\ \exists T\in G\rightarrow G.\ A = T(B) \wedge B \subseteq \text{Interval}(r,1 ,g) \)proof
{
assume A2: \( A=0 \)
let \( B = 0 \)
let \( g = 1 \)
let \( T = \text{ConstantFunction}(G,1 ) \)
have \( g\in G^+ \) using OrderedGroup_ZF_1_L3A
moreover
have \( T : G\rightarrow G \) using func1_3_L1, OrderedGroup_ZF_1_L1, group0_2_L2
moreover
from A2 have \( A = T(B) \)
moreover
have \( B \subseteq \text{Interval}(r,1 ,g) \)
ultimately have \( \exists B.\ \exists g\in G^+.\ \exists T\in G\rightarrow G.\ A = T(B) \wedge B \subseteq \text{Interval}(r,1 ,g) \)
}
moreover {
assume A3: \( A\neq 0 \)
with A1 have \( \exists L.\ \forall x\in A.\ L\leq x \) and \( \exists U.\ \forall x\in A.\ x\leq U \) using IsBounded_def, IsBoundedBelow_def, IsBoundedAbove_def
then obtain \( L \) \( U \) where D1: \( \forall x\in A.\ L\leq x \wedge x\leq U \)
with A3 have T1: \( A\subseteq G \) using OrderedGroup_ZF_1_L4
from A3 obtain \( a \) where \( a\in A \)
with D1 have T2: \( L\leq a \), \( a\leq U \)
then have T3: \( L\in G \), \( L^{-1}\in G \), \( U\in G \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L1, inverse_in_group
let \( T = \text{RightTranslation}(G,P,L) \)
let \( B = \text{RightTranslation}(G,P,L^{-1})(A) \)
let \( g = U\cdot L^{-1} \)
have \( g\in G^+ \)proof
from T2 have \( L\leq U \) using Group_order_transitive
with ordGroupAssum, T3 have \( L\cdot L^{-1}\leq g \) using IsAnOrdGroup_def
with T3 show \( thesis \) using OrderedGroup_ZF_1_L1, group0_2_L6, OrderedGroup_ZF_1_L2
qed
moreover
from T3 have \( T : G\rightarrow G \) using OrderedGroup_ZF_1_L1, group0_5_L1
moreover
have \( A = T(B) \)proof
from T3, T1 have \( T(B) = \{a\cdot L^{-1}\cdot L.\ a\in A\} \) using OrderedGroup_ZF_1_L1, group0_5_L6
moreover
from T3, T1 have \( \forall a\in A.\ a\cdot L^{-1}\cdot L = a\cdot (L^{-1}\cdot L) \) using OrderedGroup_ZF_1_L1, group_oper_assoc
ultimately have \( T(B) = \{a\cdot (L^{-1}\cdot L).\ a\in A\} \)
with T3 have \( T(B) = \{a\cdot 1 .\ a\in A\} \) using OrderedGroup_ZF_1_L1, group0_2_L6
moreover
from T1 have \( \forall a\in A.\ a\cdot 1 =a \) using OrderedGroup_ZF_1_L1, group0_2_L2
ultimately show \( thesis \)
qed
moreover
have \( B \subseteq \text{Interval}(r,1 ,g) \)proof
fix \( y \)
assume A4: \( y \in B \)
let \( S = \text{RightTranslation}(G,P,L^{-1}) \)
from D1 have T4: \( \forall x\in A.\ L\leq x \wedge x\leq U \)
moreover
have T5: \( S = \text{RightTranslation}(G,P,L^{-1}) \)
moreover
from A4 have T6: \( y \in S(A) \)
ultimately have \( y\leq U\cdot L^{-1} \) using OrderedGroup_ZF_2_L1
moreover
from T4, T5, T6 have \( 1 \leq y \) by (rule OrderedGroup_ZF_2_L1 )
ultimately show \( y \in \text{Interval}(r,1 ,g) \) using Interval_def
qed
ultimately have \( \exists B.\ \exists g\in G^+.\ \exists T\in G\rightarrow G.\ A = T(B) \wedge B \subseteq \text{Interval}(r,1 ,g) \)
} ultimately show \( thesis \)
qed

If every interval starting at \(1\) is finite, then every bounded set is finite. I find it interesting that this does not require the group to be linearly ordered (the order to be total).

theorem (in group3) OrderedGroup_ZF_2_T1:

assumes A1: \( \forall g\in G^+.\ \text{Interval}(r,1 ,g) \in Fin(G) \) and A2: \( \text{IsBounded}(A,r) \)

shows \( A \in Fin(G) \)proof
from A2 have \( \exists B.\ \exists g\in G^+.\ \exists T\in G\rightarrow G.\ A = T(B) \wedge B \subseteq \text{Interval}(r,1 ,g) \) using OrderedGroup_ZF_2_L2
then obtain \( B \) \( g \) \( T \) where D1: \( g\in G^+ \), \( B \subseteq \text{Interval}(r,1 ,g) \) and D2: \( T : G\rightarrow G \), \( A = T(B) \)
from D1, A1 have \( B\in Fin(G) \) using Fin_subset_lemma
with D2 show \( thesis \) using Finite1_L6A
qed

In linearly ordered groups finite sets are bounded.

theorem (in group3) ord_group_fin_bounded:

assumes \( r \text{ is total on } G \) and \( B\in Fin(G) \)

shows \( \text{IsBounded}(B,r) \) using ordGroupAssum, assms, IsAnOrdGroup_def, IsPartOrder_def, Finite_ZF_1_T1

For nontrivial linearly ordered groups if for every element \(G\) we can find one in \(A\) that is greater or equal (not necessarily strictly greater), then \(A\) can neither be finite nor bounded above.

lemma (in group3) OrderedGroup_ZF_2_L2A:

assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( \forall a\in G.\ \exists b\in A.\ a\leq b \)

shows \( \forall a\in G.\ \exists b\in A.\ a\neq b \wedge a\leq b \), \( \neg \text{IsBoundedAbove}(A,r) \), \( A \notin Fin(G) \)proof
{
fix \( a \)
from A1, A2 obtain \( c \) where \( c \in G_+ \) using OrderedGroup_ZF_1_L21
moreover
assume \( a\in G \)
ultimately have \( a\cdot c \in G \) and I: \( a \lt a\cdot c \) using OrderedGroup_ZF_1_L22
with A3 obtain \( b \) where II: \( b\in A \) and III: \( a\cdot c \leq b \)
moreover
from I, III have \( a \lt b \) by (rule OrderedGroup_ZF_1_L4A )
ultimately have \( \exists b\in A.\ a\neq b \wedge a\leq b \)
}
thus \( \forall a\in G.\ \exists b\in A.\ a\neq b \wedge a\leq b \)
with ordGroupAssum, A1 show \( \neg \text{IsBoundedAbove}(A,r) \), \( A \notin Fin(G) \) using IsAnOrdGroup_def, IsPartOrder_def, OrderedGroup_ZF_1_L1A, Order_ZF_3_L14, Finite_ZF_1_1_L3
qed

Nontrivial linearly ordered groups are infinite. Recall that \( Fin(A) \) is the collection of finite subsets of \(A\). In this lemma we show that \(G\notin\) \( Fin(G) \), that is that \(G\) is not a finite subset of itself. This is a way of saying that \(G\) is infinite. We also show that for nontrivial linearly ordered groups \( G_+ \) is infinite.

theorem (in group3) Linord_group_infinite:

assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \)

shows \( G_+ \notin Fin(G) \), \( G \notin Fin(G) \)proof
from A1, A2 show I: \( G_+ \notin Fin(G) \) using OrderedGroup_ZF_1_L23, OrderedGroup_ZF_2_L2A
{
assume \( G \in Fin(G) \)
moreover
have \( G_+ \subseteq G \) using PositiveSet_def
ultimately have \( G_+ \in Fin(G) \) using Fin_subset_lemma
with I have \( False \)
}
then show \( G \notin Fin(G) \)
qed

A property of nonempty subsets of linearly ordered groups that don't have a maximum: for any element in such subset we can find one that is strictly greater.

lemma (in group3) OrderedGroup_ZF_2_L2B:

assumes A1: \( r \text{ is total on } G \) and A2: \( A\subseteq G \) and A3: \( \neg \text{HasAmaximum}(r,A) \) and A4: \( x\in A \)

shows \( \exists y\in A.\ x \lt y \)proof
from ordGroupAssum, assms have \( \text{antisym}(r) \), \( r \text{ is total on } G \), \( A\subseteq G \), \( \neg \text{HasAmaximum}(r,A) \), \( x\in A \) using IsAnOrdGroup_def, IsPartOrder_def
then have \( \exists y\in A.\ \langle x,y\rangle \in r \wedge y\neq x \) using Order_ZF_4_L16
then show \( \exists y\in A.\ x \lt y \)
qed

In linearly ordered groups \(G\setminus G_+\) is bounded above.

lemma (in group3) OrderedGroup_ZF_2_L3:

assumes A1: \( r \text{ is total on } G \)

shows \( \text{IsBoundedAbove}(G-G_+,r) \)proof
from A1 have \( \forall a\in G-G_+.\ a\leq 1 \) using OrderedGroup_ZF_1_L17
then show \( \text{IsBoundedAbove}(G-G_+,r) \) using IsBoundedAbove_def
qed

In linearly ordered groups if \(A\cap G_+\) is finite, then \(A\) is bounded above.

lemma (in group3) OrderedGroup_ZF_2_L4:

assumes A1: \( r \text{ is total on } G \) and A2: \( A\subseteq G \) and A3: \( A \cap G_+ \in Fin(G) \)

shows \( \text{IsBoundedAbove}(A,r) \)proof
have \( A \cap (G-G_+) \subseteq G-G_+ \)
with A1 have \( \text{IsBoundedAbove}(A \cap (G-G_+),r) \) using OrderedGroup_ZF_2_L3, Order_ZF_3_L13
moreover
from A1, A3 have \( \text{IsBoundedAbove}(A \cap G_+,r) \) using ord_group_fin_bounded, IsBounded_def
moreover
from A1, ordGroupAssum have \( r \text{ is total on } G \), \( \text{trans}(r) \), \( r\subseteq G\times G \) using IsAnOrdGroup_def, IsPartOrder_def
ultimately have \( \text{IsBoundedAbove}(A \cap (G-G_+) \cup A \cap G_+,r) \) using Order_ZF_3_L3
moreover
from A2 have \( A = A \cap (G-G_+) \cup A \cap G_+ \)
ultimately show \( \text{IsBoundedAbove}(A,r) \)
qed

If a set \(-A\subseteq G\) is bounded above, then \(A\) is bounded below.

lemma (in group3) OrderedGroup_ZF_2_L5:

assumes A1: \( A\subseteq G \) and A2: \( \text{IsBoundedAbove}(-A,r) \)

shows \( \text{IsBoundedBelow}(A,r) \)proof
{
assume \( A = 0 \)
then have \( \text{IsBoundedBelow}(A,r) \) using IsBoundedBelow_def
}
moreover {
assume A3: \( A\neq 0 \)
from ordGroupAssum have I: \( \text{GroupInv}(G,P) : G\rightarrow G \) using IsAnOrdGroup_def, group0_2_T2
with A1, A2, A3 obtain \( u \) where D: \( \forall a\in (-A).\ a\leq u \) using func1_1_L15A, IsBoundedAbove_def
{
fix \( b \)
assume \( b\in A \)
with A1, I, D have \( b^{-1} \leq u \) and T: \( b\in G \) using func_imagedef
then have \( u^{-1}\leq (b^{-1})^{-1} \) using OrderedGroup_ZF_1_L5
with T have \( u^{-1}\leq b \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
}
then have \( \forall b\in A.\ \langle u^{-1},b\rangle \in r \)
then have \( \text{IsBoundedBelow}(A,r) \) using Order_ZF_3_L9
} ultimately show \( thesis \)
qed

If \(a\leq b\), then the image of the interval \(a..b\) by any function is nonempty.

lemma (in group3) OrderedGroup_ZF_2_L6:

assumes \( a\leq b \) and \( f:G\rightarrow G \)

shows \( f( \text{Interval}(r,a,b)) \neq 0 \) using ordGroupAssum, assms, OrderedGroup_ZF_1_L4, Order_ZF_2_L6, Order_ZF_2_L2A, IsAnOrdGroup_def, IsPartOrder_def, func1_1_L15A
end
Definition of IsAnOrdGroup: \( \text{IsAnOrdGroup}(G,P,r) \equiv \) \( ( \text{IsAgroup}(G,P) \wedge r\subseteq G\times G \wedge \text{IsPartOrder}(G,r) \wedge (\forall g\in G.\ \forall a b.\ \) \( \langle a,b\rangle \in r \longrightarrow \langle P\langle a,g\rangle ,P\langle b,g\rangle \rangle \in r \wedge \langle P\langle g,a\rangle ,P\langle g,b\rangle \rangle \in r ) ) \)
lemma (in group3) OrderedGroup_ZF_1_L1: shows \( group0(G,P) \)
lemma (in group0) group0_2_L1: shows \( monoid0(G,P) \)
lemma (in monoid0) group0_1_L3A: shows \( G\neq 0 \)
Definition of Nonnegative: \( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)
Definition of PositiveSet: \( \text{PositiveSet}(L,A,r) \equiv \) \( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} \)
lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
lemma (in group3) OrderedGroup_ZF_1_L2: shows \( g\in G^+ \longleftrightarrow 1 \leq g \)
Definition of IsTotal: \( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
Definition of IsPartOrder: \( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)
lemma (in group3) OrderedGroup_ZF_1_L3:

assumes \( g\in G \)

shows \( g\leq g \)
lemma Fol1_L3:

assumes \( \text{trans}(r) \) and \( \langle a,b\rangle \in r \wedge \langle b,c\rangle \in r \)

shows \( \langle a,c\rangle \in r \)
lemma Fol1_L4:

assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)

shows \( a=b \)
lemma (in group3) Group_order_transitive:

assumes \( a\leq b \), \( b\leq c \)

shows \( a\leq c \)
lemma (in group3) group_order_antisym:

assumes \( a\leq b \), \( b\leq a \)

shows \( a=b \)
lemma (in group3) ord_transl_inv:

assumes \( a\leq b \), \( c\in G \)

shows \( a\cdot c \leq b\cdot c \) and \( c\cdot a \leq c\cdot b \)
lemma (in group3) OrderedGroup_ZF_1_L4:

assumes \( a\leq b \)

shows \( a\in G \), \( b\in G \)
lemma (in group0) group0_2_L19:

assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\neq b \)

shows \( a\cdot c \neq b\cdot c \) and \( c\cdot a \neq c\cdot b \)
lemma Order_ZF_1_L3:

assumes \( \text{IsPartOrder}(X,r) \) and \( r \text{ is total on } X \)

shows \( \text{IsLinOrder}(X,r) \)
lemma (in group3) OrderedGroup_ZF_1_L2B:

assumes \( r \text{ is total on } G \) and \( a\in G-G^+ \)

shows \( a\leq 1 \)
lemma (in group3) OrderedGroup_ZF_1_L2A: shows \( g\in G_+ \longleftrightarrow (1 \leq g \wedge g\neq 1 ) \)
lemma (in group3) OrderedGroup_ZF_1_L4E: shows \( G^+ \subseteq G \)
lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)
lemma (in group0) group0_2_L6:

assumes \( x\in G \)

shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)
lemma (in group0) group_oper_assoc:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot (b\cdot c) = a\cdot b\cdot c \)
lemma (in group3) OrderedGroup_ZF_1_L5:

assumes \( a\leq b \)

shows \( b^{-1}\leq a^{-1} \)
lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
lemma (in group0) group_inv_of_inv:

assumes \( a\in G \)

shows \( a = (a^{-1})^{-1} \)
lemma (in group3) OrderedGroup_ZF_1_L5AB:

assumes \( 1 \leq a \)

shows \( a^{-1}\leq 1 \) and \( \neg (a\leq 1 \wedge a\neq 1 ) \)
lemma (in group0) inv_cancel_two:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)
lemma (in group3) ord_transl_inv:

assumes \( a\leq b \), \( c\in G \)

shows \( a\cdot c \leq b\cdot c \) and \( c\cdot a \leq c\cdot b \)
lemma (in group0) inv_cancel_two:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)
lemma (in group3) OrderedGroup_ZF_1_L5AE:

assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\cdot b \leq a\cdot c \)

shows \( b\leq c \)
lemma (in group3) OrderedGroup_ZF_1_L5B:

assumes \( a\leq b \) and \( c\leq d \)

shows \( a\cdot c \leq b\cdot d \)
lemma (in group3) OrderedGroup_ZF_1_L5F:

assumes \( 1 \leq a \) and \( b\in G \)

shows \( b\leq a\cdot b \), \( b\leq b\cdot a \)
lemma (in group3) OrderedGroup_ZF_1_L5J:

assumes \( a\in G \), \( b\in G \) and \( c \leq a\cdot b^{-1} \)

shows \( c\cdot b \leq a \)
lemma (in group3) OrderedGroup_ZF_1_L5JA:

assumes \( a\in G \), \( b\in G \) and \( c \leq a^{-1}\cdot b \)

shows \( a\cdot c\leq b \)
lemma (in group3) OrderedGroup_ZF_1_L5A:

assumes \( a\leq 1 \)

shows \( 1 \leq a^{-1} \)
lemma (in group3) OrderedGroup_ZF_1_L6:

assumes \( r \text{ is total on } G \) and \( a\in G-G^+ \)

shows \( a\leq 1 \), \( a^{-1} \in G^+ \), \( \text{restrict}( \text{GroupInv}(G,P),G-G^+)(a) \in G^+ \)
lemma (in group0) group_op_closed:

assumes \( a\in G \), \( b\in G \)

shows \( a\cdot b \in G \)
lemma (in group3) OrderedGroup_ZF_1_L8:

assumes \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \neg (a\leq b) \)

shows \( b \leq a \), \( a^{-1} \leq b^{-1} \), \( a\neq b \), \( b \lt a \)
lemma (in group3) OrderedGroup_ZF_1_L9A:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b \leq c \longleftrightarrow a \leq c\cdot b^{-1} \)
lemma (in group3) OrderedGroup_ZF_1_L9D:

assumes \( a\leq b \)

shows \( 1 \leq b\cdot a^{-1} \)
lemma (in group0) group0_2_L11A:

assumes \( a\in G \), \( b\in G \) and \( a\cdot b^{-1} = 1 \)

shows \( a=b \)
lemma (in group0) group0_2_L9:

assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = 1 \)

shows \( a = b^{-1} \) and \( b = a^{-1} \)
lemma (in group3) OrderedGroup_ZF_1_L5AA:

assumes \( a\in G \) and \( 1 \leq a^{-1} \)

shows \( a\leq 1 \)
lemma (in group3) group_strict_ord_transl_inv:

assumes \( a \lt b \) and \( c\in G \)

shows \( a\cdot c \lt b\cdot c \) and \( c\cdot a \lt c\cdot b \)
lemma (in group3) group_strict_ord_transit:

assumes \( a\leq b \) and \( b \lt c \)

shows \( a \lt c \)
lemma (in group3) OrderedGroup_ZF_1_L4A:

assumes \( a \lt b \) and \( b\leq c \)

shows \( a \lt c \)
lemma (in group3) OrderedGroup_ZF_1_L11:

assumes \( 1 \leq a \), \( 1 \leq b \) and \( 1 \neq a \), \( 1 \neq b \)

shows \( 1 \neq a\cdot b \)
lemma (in group3) OrderedGroup_ZF_1_L12:

assumes \( 1 \leq a \), \( 1 \leq b \)

shows \( 1 \leq a\cdot b \)
Definition of IsOpClosed: \( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
lemma (in group0) group0_2_L8B:

assumes \( a\in G \) and \( a \neq 1 \)

shows \( a^{-1} \neq 1 \)
lemma (in group3) OrderedGroup_ZF_1_L15:

assumes \( a\in G_+ \)

shows \( a\neq 1 \), \( a^{-1}\notin G_+ \)
lemma (in group0) group0_2_L8C:

assumes \( a\in G \) and \( a^{-1} \neq 1 \)

shows \( a\neq 1 \)
lemma (in group3) OrderedGroup_ZF_1_L14:

assumes \( r \text{ is total on } G \) and \( a\in G \)

shows \( a=1 \vee a\in G_+ \vee a^{-1}\in G_+ \)
lemma (in group3) OrderedGroup_ZF_1_L16:

assumes \( a\in G \) and \( a^{-1}\in G_+ \)

shows \( a\neq 1 \), \( a\notin G_+ \)
lemma Fol1_L5:

assumes \( p\vee q\vee r \) and \( p \longrightarrow \neg q \wedge \neg r \) and \( q \longrightarrow \neg p \wedge \neg r \) and \( r \longrightarrow \neg p \wedge \neg q \)

shows \( \text{Exactly_1_of_3_holds} (p,q,r) \)
corollary (in group3) OrderedGroup_ZF_1_L8A:

assumes \( r \text{ is total on } G \) and \( a\in G \) and \( \neg (1 \leq a) \)

shows \( 1 \leq a^{-1} \), \( 1 \neq a \), \( a\leq 1 \)
lemma (in group3) OrdGroup_decomp:

assumes \( r \text{ is total on } G \) and \( a\in G \)

shows \( \text{Exactly_1_of_3_holds} (a=1 ,a\in G_+,a^{-1}\in G_+) \)
lemma Fol1_L7:

assumes \( q \) and \( \text{Exactly_1_of_3_holds} (p,q,r) \)

shows \( \neg r \)
lemma (in group0) group0_2_L7:

assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = a \)

shows \( b=1 \)
lemma (in group3) OrderedGroup_ZF_1_L17:

assumes \( r \text{ is total on } G \) and \( a \in G-G_+ \)

shows \( a\leq 1 \)
lemma (in group3) OrderedGroup_ZF_1_L21:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \)

shows \( G_+ \neq 0 \)
lemma (in group3) OrderedGroup_ZF_1_L3A: shows \( 1 \in G^+ \)
theorem group0_2_T2:

assumes \( \text{IsAgroup}(G,f) \)

shows \( \text{GroupInv}(G,f) : G\rightarrow G \)
lemma func_imagedef:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)

shows \( f(A) = \{f(x).\ x \in A\} \)
lemma func1_1_L6:

assumes \( f:X\rightarrow Y \)

shows \( f(B) \subseteq \text{range}(f) \) and \( f(B) \subseteq Y \)
lemma (in group3) OrderedGroup_ZF_1_L25: shows \( (-G_+) = \{a^{-1}.\ a\in G_+\} \), \( (-G_+) \subseteq G \)
lemma (in group3) OrderedGroup_ZF_1_L26:

assumes \( a\in G \) and \( a^{-1} \in G_+ \)

shows \( a \in (-G_+) \)
lemma (in group3) OrderedGroup_ZF_1_L27:

assumes \( a \in (-G_+) \)

shows \( a^{-1} \in G_+ \)
corollary (in group3) OrderedGroup_ZF_1_L5K:

assumes \( a\in G \), \( b\in G \) and \( 1 \leq a\cdot b^{-1} \)

shows \( b \leq a \)
corollary (in group3) OrderedGroup_ZF_1_L29:

assumes \( a\in G \), \( b\in G \) and \( a\cdot b^{-1} \in G_+ \)

shows \( b\leq a \), \( b\neq a \)
lemma (in group0) group0_2_L12:

assumes \( a\in G \), \( b\in G \)

shows \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \)
lemma func1_1_L13A:

assumes \( f(A)\neq \emptyset \)

shows \( A\neq \emptyset \)
lemma (in group0) group0_5_L1:

assumes \( g\in G \)

shows \( \text{RightTranslation}(G,P,g) : G\rightarrow G \) and \( \text{LeftTranslation}(G,P,g) : G\rightarrow G \)
lemma (in group0) group0_5_L2:

assumes \( g\in G \), \( a\in G \)

shows \( \text{RightTranslation}(G,P,g)(a) = a\cdot g \), \( \text{LeftTranslation}(G,P,g)(a) = g\cdot a \)
lemma func1_3_L1:

assumes \( c\in Y \)

shows \( \text{ConstantFunction}(X,c) : X\rightarrow Y \)
Definition of IsBounded: \( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
Definition of IsBoundedBelow: \( \text{IsBoundedBelow}(A,r) \equiv (A=0 \vee (\exists l.\ \forall x\in A.\ \langle l,x\rangle \in r)) \)
Definition of IsBoundedAbove: \( \text{IsBoundedAbove}(A,r) \equiv ( A=0 \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in r)) \)
lemma (in group0) group0_5_L6:

assumes \( g\in G \), \( h\in G \) and \( A\subseteq G \) and \( T_g = \text{RightTranslation}(G,P,g) \), \( T_h = \text{RightTranslation}(G,P,h) \)

shows \( T_g(T_h(A)) = \{a\cdot h\cdot g.\ a\in A\} \)
lemma (in group3) OrderedGroup_ZF_2_L1:

assumes \( \forall g\in A.\ L\leq g \wedge g\leq M \) and \( S = \text{RightTranslation}(G,P,L^{-1}) \) and \( a \in S(A) \)

shows \( a \leq M\cdot L^{-1} \), \( 1 \leq a \)
Definition of Interval: \( \text{Interval}(r,a,b) \equiv r\{a\} \cap r^{-1}\{b\} \)
lemma (in group3) OrderedGroup_ZF_2_L2:

assumes \( \text{IsBounded}(A,r) \)

shows \( \exists B.\ \exists g\in G^+.\ \exists T\in G\rightarrow G.\ A = T(B) \wedge B \subseteq \text{Interval}(r,1 ,g) \)
lemma Finite1_L6A:

assumes \( f:X\rightarrow Y \) and \( N \in Fin(X) \)

shows \( f(N) \in Fin(Y) \)
theorem Finite_ZF_1_T1:

assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( B\in Fin(X) \)

shows \( \text{IsBounded}(B,r) \)
lemma (in group3) OrderedGroup_ZF_1_L22:

assumes \( a\in G \), \( b\in G_+ \)

shows \( a\leq a\cdot b \), \( a \neq a\cdot b \), \( a\cdot b \in G \)
lemma (in group3) OrderedGroup_ZF_1_L1A: shows \( G\neq 0 \)
lemma Order_ZF_3_L14:

assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{antisym}(r) \) and \( r \subseteq X\times X \) and \( X\neq 0 \) and \( \forall x\in X.\ \exists a\in A.\ x\neq a \wedge \langle x,a\rangle \in r \)

shows \( \neg \text{IsBoundedAbove}(A,r) \)
lemma Finite_ZF_1_1_L3:

assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{antisym}(r) \) and \( r \subseteq X\times X \) and \( X\neq 0 \) and \( \forall x\in X.\ \exists a\in A.\ x\neq a \wedge \langle x,a\rangle \in r \)

shows \( A \notin Fin(X) \)
lemma (in group3) OrderedGroup_ZF_1_L23:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( a\in G \)

shows \( \exists b\in G_+.\ a\leq b \)
lemma (in group3) OrderedGroup_ZF_2_L2A:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( \forall a\in G.\ \exists b\in A.\ a\leq b \)

shows \( \forall a\in G.\ \exists b\in A.\ a\neq b \wedge a\leq b \), \( \neg \text{IsBoundedAbove}(A,r) \), \( A \notin Fin(G) \)
lemma Order_ZF_4_L16:

assumes \( \text{antisym}(r) \) and \( r \text{ is total on } X \) and \( A\subseteq X \) and \( \neg \text{HasAmaximum}(r,A) \) and \( x\in A \)

shows \( \exists y\in A.\ \langle x,y\rangle \in r \wedge y\neq x \)
lemma (in group3) OrderedGroup_ZF_2_L3:

assumes \( r \text{ is total on } G \)

shows \( \text{IsBoundedAbove}(G-G_+,r) \)
lemma Order_ZF_3_L13:

assumes \( \text{IsBoundedAbove}(A,r) \) and \( B\subseteq A \)

shows \( \text{IsBoundedAbove}(B,r) \)
theorem (in group3) ord_group_fin_bounded:

assumes \( r \text{ is total on } G \) and \( B\in Fin(G) \)

shows \( \text{IsBounded}(B,r) \)
lemma Order_ZF_3_L3:

assumes \( r \text{ is total on } X \) and \( \text{trans}(r) \) and \( \text{IsBoundedAbove}(A,r) \), \( \text{IsBoundedAbove}(B,r) \) and \( r \subseteq X\times X \)

shows \( \text{IsBoundedAbove}(A\cup B,r) \)
lemma func1_1_L15A:

assumes \( f: X\rightarrow Y \) and \( A\subseteq X \) and \( A\neq \emptyset \)

shows \( f(A) \neq \emptyset \)
lemma Order_ZF_3_L9:

assumes \( \forall a\in A.\ \langle l,a\rangle \in r \)

shows \( \text{IsBoundedBelow}(A,r) \)
lemma Order_ZF_2_L6:

assumes \( r \subseteq X\times X \)

shows \( \text{Interval}(r,a,b) \subseteq X \)
lemma Order_ZF_2_L2A:

assumes \( \text{refl}(X,r) \) and \( a\in X \), \( b\in X \) and \( \langle a,b\rangle \in r \)

shows \( \text{Interval}(r,a,b) \neq 0 \)