IsarMathLib

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

theory OrderedGroup_ZF_1 imports OrderedGroup_ZF
begin

In this theory we continue the OrderedGroup_ZF theory development.

Absolute value and the triangle inequality

The goal of this section is to prove the triangle inequality for ordered groups.

Absolute value maps \(G\) into \(G\).

lemma (in group3) OrderedGroup_ZF_3_L1:

shows \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G \)proof
let \( f = id(G^+) \)
let \( g = \text{restrict}( \text{GroupInv}(G,P),G-G^+) \)
have \( f : G^+\rightarrow G^+ \) using id_type
then have \( f : G^+\rightarrow G \) using OrderedGroup_ZF_1_L4E, fun_weaken_type
moreover
have \( g : G-G^+\rightarrow G \)proof
from ordGroupAssum have \( \text{GroupInv}(G,P) : G\rightarrow G \) using IsAnOrdGroup_def, group0_2_T2
moreover
have \( G-G^+ \subseteq G \)
ultimately show \( thesis \) using restrict_type2
qed
moreover
have \( G^+\cap (G-G^+) = 0 \)
ultimately have \( f \cup g : G^+\cup (G-G^+)\rightarrow G\cup G \) by (rule fun_disjoint_Un )
moreover
have \( G^+\cup (G-G^+) = G \) using OrderedGroup_ZF_1_L4E
ultimately show \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G \) using AbsoluteValue_def
qed

If \(a\in G^+\), then \(|a| = a\).

lemma (in group3) OrderedGroup_ZF_3_L2:

assumes A1: \( a\in G^+ \)

shows \( \vert a\vert = a \)proof
from ordGroupAssum have \( \text{GroupInv}(G,P) : G\rightarrow G \) using IsAnOrdGroup_def, group0_2_T2
with A1 show \( thesis \) using func1_1_L1, OrderedGroup_ZF_1_L4E, fun_disjoint_apply1, AbsoluteValue_def, id_conv
qed

The absolute value of the unit is the unit. In the additive totation that would be \(|0| = 0\).

lemma (in group3) OrderedGroup_ZF_3_L2A:

shows \( \vert 1 \vert = 1 \) using OrderedGroup_ZF_1_L3A, OrderedGroup_ZF_3_L2

If \(a\) is positive, then \(|a| = a\).

lemma (in group3) OrderedGroup_ZF_3_L2B:

assumes \( a\in G_+ \)

shows \( \vert a\vert = a \) using assms, PositiveSet_def, Nonnegative_def, OrderedGroup_ZF_3_L2

If \(a\in G\setminus G^+\), then \(|a| = a^{-1}\).

lemma (in group3) OrderedGroup_ZF_3_L3:

assumes A1: \( a \in G-G^+ \)

shows \( \vert a\vert = a^{-1} \)proof
have \( domain(id(G^+)) = G^+ \) using id_type, func1_1_L1
with A1 show \( thesis \) using fun_disjoint_apply2, AbsoluteValue_def, restrict
qed

For elements that not greater than the unit, the absolute value is the inverse.

lemma (in group3) OrderedGroup_ZF_3_L3A:

assumes A1: \( a\leq 1 \)

shows \( \vert a\vert = a^{-1} \)proof
{
assume \( a=1 \)
then have \( \vert a\vert = a^{-1} \) using OrderedGroup_ZF_3_L2A, OrderedGroup_ZF_1_L1, group_inv_of_one
}
moreover {
assume \( a\neq 1 \)
with A1 have \( \vert a\vert = a^{-1} \) using OrderedGroup_ZF_1_L4C, OrderedGroup_ZF_3_L3
} ultimately show \( \vert a\vert = a^{-1} \)
qed

In linearly ordered groups the absolute value of any element is in \(G^+\).

lemma (in group3) OrderedGroup_ZF_3_L3B:

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

shows \( \vert a\vert \in G^+ \)proof
{
assume \( a \in G^+ \)
then have \( \vert a\vert \in G^+ \) using OrderedGroup_ZF_3_L2
}
moreover {
assume \( a \notin G^+ \)
with A1, A2 have \( \vert a\vert \in G^+ \) using OrderedGroup_ZF_3_L3, OrderedGroup_ZF_1_L6
} ultimately show \( \vert a\vert \in G^+ \)
qed

For linearly ordered groups (where the order is total), the absolute value maps the group into the positive set.

lemma (in group3) OrderedGroup_ZF_3_L3C:

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

shows \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G^+ \)proof
have \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G \) using OrderedGroup_ZF_3_L1
moreover
from A1 have T2: \( \forall g\in G.\ \text{AbsoluteValue}(G,P,r)(g) \in G^+ \) using OrderedGroup_ZF_3_L3B
ultimately show \( thesis \) by (rule func1_1_L1A )
qed

If the absolute value is the unit, then the elemnent is the unit.

lemma (in group3) OrderedGroup_ZF_3_L3D:

assumes A1: \( a\in G \) and A2: \( \vert a\vert = 1 \)

shows \( a = 1 \)proof
{
assume \( a \in G^+ \)
with A2 have \( a = 1 \) using OrderedGroup_ZF_3_L2
}
moreover {
assume \( a \notin G^+ \)
with A1, A2 have \( a = 1 \) using OrderedGroup_ZF_3_L3, OrderedGroup_ZF_1_L1, group0_2_L8A
} ultimately show \( a = 1 \)
qed

In linearly ordered groups the unit is not greater than the absolute value of any element.

lemma (in group3) OrderedGroup_ZF_3_L3E:

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

shows \( 1 \leq \vert a\vert \) using assms, OrderedGroup_ZF_3_L3B, OrderedGroup_ZF_1_L2

If \(b\) is greater than both \(a\) and \(a^{-1}\), then \(b\) is greater than \(|a|\).

lemma (in group3) OrderedGroup_ZF_3_L4:

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

shows \( \vert a\vert \leq b \)proof
{
assume \( a\in G^+ \)
with A1 have \( \vert a\vert \leq b \) using OrderedGroup_ZF_3_L2
}
moreover {
assume \( a\notin G^+ \)
with A1, A2 have \( \vert a\vert \leq b \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_3_L3
} ultimately show \( \vert a\vert \leq b \)
qed

In linearly ordered groups \(a\leq |a|\).

lemma (in group3) OrderedGroup_ZF_3_L5:

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

shows \( a \leq \vert a\vert \)proof
{
assume \( a \in G^+ \)
with A2 have \( a \leq \vert a\vert \) using OrderedGroup_ZF_3_L2, OrderedGroup_ZF_1_L3
}
moreover {
assume \( a \notin G^+ \)
with A1, A2 have \( a \leq \vert a\vert \) using OrderedGroup_ZF_3_L3B, OrderedGroup_ZF_1_L4B
} ultimately show \( a \leq \vert a\vert \)
qed

\(a^{-1}\leq |a|\) (in additive notation it would be \(-a\leq |a|\).

lemma (in group3) OrderedGroup_ZF_3_L6:

assumes A1: \( a\in G \)

shows \( a^{-1} \leq \vert a\vert \)proof
{
assume \( a \in G^+ \)
then have T1: \( 1 \leq a \) and T2: \( \vert a\vert = a \) using OrderedGroup_ZF_1_L2, OrderedGroup_ZF_3_L2
then have \( a^{-1}\leq 1 ^{-1} \) using OrderedGroup_ZF_1_L5
then have T3: \( a^{-1}\leq 1 \) using OrderedGroup_ZF_1_L1, group_inv_of_one
from T3, T1 have \( a^{-1}\leq a \) by (rule Group_order_transitive )
with T2 have \( a^{-1} \leq \vert a\vert \)
}
moreover {
assume A2: \( a \notin G^+ \)
from A1 have \( \vert a\vert \in G \) using OrderedGroup_ZF_3_L1, apply_funtype
with ordGroupAssum have \( \vert a\vert \leq \vert a\vert \) using IsAnOrdGroup_def, IsPartOrder_def, refl_def
with A1, A2 have \( a^{-1} \leq \vert a\vert \) using OrderedGroup_ZF_3_L3
} ultimately show \( a^{-1} \leq \vert a\vert \)
qed

Some inequalities about the product of two elements of a linearly ordered group and its absolute value.

lemma (in group3) OrderedGroup_ZF_3_L6A:

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

shows \( a\cdot b \leq \vert a\vert \cdot \vert b\vert \), \( a\cdot b^{-1} \leq \vert a\vert \cdot \vert b\vert \), \( a^{-1}\cdot b \leq \vert a\vert \cdot \vert b\vert \), \( a^{-1}\cdot b^{-1} \leq \vert a\vert \cdot \vert b\vert \) using assms, OrderedGroup_ZF_3_L5, OrderedGroup_ZF_3_L6, OrderedGroup_ZF_1_L5B

\(|a^{-1}|\leq |a|\).

lemma (in group3) OrderedGroup_ZF_3_L7:

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

shows \( \vert a^{-1}\vert \leq \vert a\vert \) using assms, OrderedGroup_ZF_3_L5, OrderedGroup_ZF_1_L1, group_inv_of_inv, OrderedGroup_ZF_3_L6, OrderedGroup_ZF_3_L4

\(|a^{-1}| = |a|\).

lemma (in group3) OrderedGroup_ZF_3_L7A:

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

shows \( \vert a^{-1}\vert = \vert a\vert \)proof
from A2 have \( a^{-1}\in G \) using OrderedGroup_ZF_1_L1, inverse_in_group
with A1 have \( \vert (a^{-1})^{-1}\vert \leq \vert a^{-1}\vert \) using OrderedGroup_ZF_3_L7
with A1, A2 have \( \vert a^{-1}\vert \leq \vert a\vert \), \( \vert a\vert \leq \vert a^{-1}\vert \) using OrderedGroup_ZF_1_L1, group_inv_of_inv, OrderedGroup_ZF_3_L7
then show \( thesis \) by (rule group_order_antisym )
qed

\(|a\cdot b^{-1}| = |b\cdot a^{-1}|\). It doesn't look so strange in the additive notation: \(|a-b| = |b-a|\).

lemma (in group3) OrderedGroup_ZF_3_L7B:

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

shows \( \vert a\cdot b^{-1}\vert = \vert b\cdot a^{-1}\vert \)proof
from A1, A2 have \( \vert (a\cdot b^{-1})^{-1}\vert = \vert a\cdot b^{-1}\vert \) using OrderedGroup_ZF_1_L1, inverse_in_group, group0_2_L1, group0_1_L1, OrderedGroup_ZF_3_L7A
moreover
from A2 have \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \) using OrderedGroup_ZF_1_L1, group0_2_L12
ultimately show \( thesis \)
qed

Triangle inequality for linearly ordered abelian groups. It would be nice to drop commutativity or give an example that shows we can't do that.

theorem (in group3) OrdGroup_triangle_ineq:

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

shows \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \)proof
from A1, A2, A3 have \( a \leq \vert a\vert \), \( b \leq \vert b\vert \), \( a^{-1} \leq \vert a\vert \), \( b^{-1} \leq \vert b\vert \) using OrderedGroup_ZF_3_L5, OrderedGroup_ZF_3_L6
then have \( a\cdot b \leq \vert a\vert \cdot \vert b\vert \), \( a^{-1}\cdot b^{-1} \leq \vert a\vert \cdot \vert b\vert \) using OrderedGroup_ZF_1_L5B
with A1, A3 show \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \) using OrderedGroup_ZF_1_L1, group_inv_of_two, IsCommutative_def, OrderedGroup_ZF_3_L4
qed

We can multiply the sides of an inequality with absolute value.

lemma (in group3) OrderedGroup_ZF_3_L7C:

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \), \( a\in G \), \( b\in G \) and \( \vert a\vert \leq c \), \( \vert b\vert \leq d \)

shows \( \vert a\cdot b\vert \leq c\cdot d \)proof
from assms(1,2,3,4) have \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \) using OrdGroup_triangle_ineq
moreover
from assms(5,6) have \( \vert a\vert \cdot \vert b\vert \leq c\cdot d \) using OrderedGroup_ZF_1_L5B
ultimately show \( thesis \) by (rule Group_order_transitive )
qed

A version of the OrderedGroup_ZF_3_L7C but with multiplying by the inverse.

lemma (in group3) OrderedGroup_ZF_3_L7CA:

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \vert a\vert \leq c \), \( \vert b\vert \leq d \)

shows \( \vert a\cdot b^{-1}\vert \leq c\cdot d \) using assms, OrderedGroup_ZF_1_L1, inverse_in_group, OrderedGroup_ZF_3_L7A, OrderedGroup_ZF_3_L7C

Triangle inequality with three integers.

lemma (in group3) OrdGroup_triangle_ineq3:

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

shows \( \vert a\cdot b\cdot c\vert \leq \vert a\vert \cdot \vert b\vert \cdot \vert c\vert \)proof
from A3 have T: \( a\cdot b \in G \), \( \vert c\vert \in G \) using OrderedGroup_ZF_1_L1, group_op_closed, OrderedGroup_ZF_3_L1, apply_funtype
with A1, A2, A3 have \( \vert a\cdot b\cdot c\vert \leq \vert a\cdot b\vert \cdot \vert c\vert \) using OrdGroup_triangle_ineq
moreover
from ordGroupAssum, A1, A2, A3, T have \( \vert a\cdot b\vert \cdot \vert c\vert \leq \vert a\vert \cdot \vert b\vert \cdot \vert c\vert \) using OrdGroup_triangle_ineq, IsAnOrdGroup_def
ultimately show \( \vert a\cdot b\cdot c\vert \leq \vert a\vert \cdot \vert b\vert \cdot \vert c\vert \) by (rule Group_order_transitive )
qed

Some variants of the triangle inequality.

lemma (in group3) OrderedGroup_ZF_3_L7D:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( r \text{ is total on } G \) and A3: \( a\in G \), \( b\in G \) and A4: \( \vert a\cdot b^{-1}\vert \leq c \)

shows \( \vert a\vert \leq c\cdot \vert b\vert \), \( \vert a\vert \leq \vert b\vert \cdot c \), \( c^{-1}\cdot a \leq b \), \( a\cdot c^{-1} \leq b \), \( a \leq b\cdot c \)proof
from A3, A4 have T: \( a\cdot b^{-1} \in G \), \( \vert b\vert \in G \), \( c\in G \), \( c^{-1} \in G \) using OrderedGroup_ZF_1_L1, inverse_in_group, group0_2_L1, group0_1_L1, OrderedGroup_ZF_3_L1, apply_funtype, OrderedGroup_ZF_1_L4
from A3 have \( \vert a\vert = \vert a\cdot b^{-1}\cdot b\vert \) using OrderedGroup_ZF_1_L1, inv_cancel_two
with A1, A2, A3, T have \( \vert a\vert \leq \vert a\cdot b^{-1}\vert \cdot \vert b\vert \) using OrdGroup_triangle_ineq
with T, A4 show \( \vert a\vert \leq c\cdot \vert b\vert \) using OrderedGroup_ZF_1_L5C
with T, A1 show \( \vert a\vert \leq \vert b\vert \cdot c \) using IsCommutative_def
from A2, T have \( a\cdot b^{-1} \leq \vert a\cdot b^{-1}\vert \) using OrderedGroup_ZF_3_L5
moreover
note A4
ultimately have I: \( a\cdot b^{-1} \leq c \) by (rule Group_order_transitive )
with A3 show \( c^{-1}\cdot a \leq b \) using OrderedGroup_ZF_1_L5H
with A1, A3, T show \( a\cdot c^{-1} \leq b \) using IsCommutative_def
from A1, A3, T, I show \( a \leq b\cdot c \) using OrderedGroup_ZF_1_L5H, IsCommutative_def
qed

Some more variants of the triangle inequality.

lemma (in group3) OrderedGroup_ZF_3_L7E:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( r \text{ is total on } G \) and A3: \( a\in G \), \( b\in G \) and A4: \( \vert a\cdot b^{-1}\vert \leq c \)

shows \( b\cdot c^{-1} \leq a \)proof
from A3 have \( a\cdot b^{-1} \in G \) using OrderedGroup_ZF_1_L1, inverse_in_group, group_op_closed
with A2 have \( \vert (a\cdot b^{-1})^{-1}\vert = \vert a\cdot b^{-1}\vert \) using OrderedGroup_ZF_3_L7A
moreover
from A3 have \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \) using OrderedGroup_ZF_1_L1, group0_2_L12
ultimately have \( \vert b\cdot a^{-1}\vert = \vert a\cdot b^{-1}\vert \)
with A1, A2, A3, A4 show \( b\cdot c^{-1} \leq a \) using OrderedGroup_ZF_3_L7D
qed

An application of the triangle inequality with four group elements.

lemma (in group3) OrderedGroup_ZF_3_L7F:

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

shows \( \vert a\cdot c^{-1}\vert \leq \vert a\cdot b\vert \cdot \vert c\cdot d\vert \cdot \vert b\cdot d^{-1}\vert \)proof
from A3 have T: \( a\cdot c^{-1} \in G \), \( a\cdot b \in G \), \( c\cdot d \in G \), \( b\cdot d^{-1} \in G \), \( (c\cdot d)^{-1} \in G \), \( (b\cdot d^{-1})^{-1} \in G \) using OrderedGroup_ZF_1_L1, inverse_in_group, group_op_closed
with A1, A2 have \( \vert (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1}\vert \leq \vert a\cdot b\vert \cdot \vert (c\cdot d)^{-1}\vert \cdot \vert (b\cdot d^{-1})^{-1}\vert \) using OrdGroup_triangle_ineq3
moreover
from A2, T have \( \vert (c\cdot d)^{-1}\vert =\vert c\cdot d\vert \) and \( \vert (b\cdot d^{-1})^{-1}\vert = \vert b\cdot d^{-1}\vert \) using OrderedGroup_ZF_3_L7A
moreover
from A1, A3 have \( (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1} \) using OrderedGroup_ZF_1_L1, group0_4_L8
ultimately show \( \vert a\cdot c^{-1}\vert \leq \vert a\cdot b\vert \cdot \vert c\cdot d\vert \cdot \vert b\cdot d^{-1}\vert \)
qed

\(|a|\leq L\) implies \(L^{-1} \leq a\) (it would be \(-L \leq a\) in the additive notation).

lemma (in group3) OrderedGroup_ZF_3_L8:

assumes A1: \( a\in G \) and A2: \( \vert a\vert \leq L \)

shows \( L^{-1}\leq a \)proof
from A1 have I: \( a^{-1} \leq \vert a\vert \) using OrderedGroup_ZF_3_L6
from I, A2 have \( a^{-1} \leq L \) by (rule Group_order_transitive )
then have \( L^{-1}\leq (a^{-1})^{-1} \) using OrderedGroup_ZF_1_L5
with A1 show \( L^{-1}\leq a \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
qed

In linearly ordered groups \(|a|\leq L\) implies \(a \leq L\) (it would be \(a \leq L\) in the additive notation).

lemma (in group3) OrderedGroup_ZF_3_L8A:

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

shows \( a\leq L \), \( 1 \leq L \)proof
from A1, A2 have I: \( a \leq \vert a\vert \) using OrderedGroup_ZF_3_L5
from I, A3 show \( a\leq L \) by (rule Group_order_transitive )
from A1, A2, A3 have \( 1 \leq \vert a\vert \), \( \vert a\vert \leq L \) using OrderedGroup_ZF_3_L3B, OrderedGroup_ZF_1_L2
then show \( 1 \leq L \) by (rule Group_order_transitive )
qed

A somewhat generalized version of the above lemma.

lemma (in group3) OrderedGroup_ZF_3_L8B:

assumes A1: \( a\in G \) and A2: \( \vert a\vert \leq L \) and A3: \( 1 \leq c \)

shows \( (L\cdot c)^{-1} \leq a \)proof
from A1, A2, A3 have \( c^{-1}\cdot L^{-1} \leq 1 \cdot a \) using OrderedGroup_ZF_3_L8, OrderedGroup_ZF_1_L5AB, OrderedGroup_ZF_1_L5B
with A1, A2, A3 show \( (L\cdot c)^{-1} \leq a \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_1_L1, group_inv_of_two, group0_2_L2
qed

If \(b\) is between \(a\) and \(a\cdot c\), then \(b\cdot a^{-1}\leq c\).

lemma (in group3) OrderedGroup_ZF_3_L8C:

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

shows \( \vert b\cdot a^{-1}\vert \leq c \)proof
from A1, A2, A3 have \( b\cdot a^{-1} \leq c \) using OrderedGroup_ZF_1_L9C, OrderedGroup_ZF_1_L4
moreover
have \( (b\cdot a^{-1})^{-1} \leq c \)proof
from A1 have T: \( a\in G \), \( b\in G \) using OrderedGroup_ZF_1_L4
with A1 have \( a\cdot b^{-1} \leq 1 \) using OrderedGroup_ZF_1_L9
moreover
from A1, A3 have \( a\leq c\cdot a \) by (rule Group_order_transitive )
with ordGroupAssum, T have \( a\cdot a^{-1} \leq c\cdot a\cdot a^{-1} \) using OrderedGroup_ZF_1_L1, inverse_in_group, IsAnOrdGroup_def
with T, A2 have \( 1 \leq c \) using OrderedGroup_ZF_1_L1, group0_2_L6, inv_cancel_two
ultimately have \( a\cdot b^{-1} \leq c \) by (rule Group_order_transitive )
with T show \( (b\cdot a^{-1})^{-1} \leq c \) using OrderedGroup_ZF_1_L1, group0_2_L12
qed
ultimately show \( \vert b\cdot a^{-1}\vert \leq c \) using OrderedGroup_ZF_3_L4
qed

For linearly ordered groups if the absolute values of elements in a set are bounded, then the set is bounded.

lemma (in group3) OrderedGroup_ZF_3_L9:

assumes A1: \( r \text{ is total on } G \) and A2: \( A\subseteq G \) and A3: \( \forall a\in A.\ \vert a\vert \leq L \)

shows \( \text{IsBounded}(A,r) \)proof
from A1, A2, A3 have \( \forall a\in A.\ a\leq L \), \( \forall a\in A.\ L^{-1}\leq a \) using OrderedGroup_ZF_3_L8, OrderedGroup_ZF_3_L8A
then show \( \text{IsBounded}(A,r) \) using IsBoundedAbove_def, IsBoundedBelow_def, IsBounded_def
qed

A slightly more general version of the previous lemma, stating the same fact for a set defined by separation.

lemma (in group3) OrderedGroup_ZF_3_L9A:

assumes A1: \( r \text{ is total on } G \) and A2: \( \forall x\in X.\ b(x)\in G \wedge \vert b(x)\vert \leq L \)

shows \( \text{IsBounded}(\{b(x).\ x\in X\},r) \)proof
from A2 have \( \{b(x).\ x\in X\} \subseteq G \), \( \forall a\in \{b(x).\ x\in X\}.\ \vert a\vert \leq L \)
with A1 show \( thesis \) using OrderedGroup_ZF_3_L9
qed

A special form of the previous lemma stating a similar fact for an image of a set by a function with values in a linearly ordered group.

lemma (in group3) OrderedGroup_ZF_3_L9B:

assumes A1: \( r \text{ is total on } G \) and A2: \( f:X\rightarrow G \) and A3: \( A\subseteq X \) and A4: \( \forall x\in A.\ \vert f(x)\vert \leq L \)

shows \( \text{IsBounded}(f(A),r) \)proof
from A2, A3, A4 have \( \forall x\in A.\ f(x) \in G \wedge \vert f(x)\vert \leq L \) using apply_funtype
with A1 have \( \text{IsBounded}(\{f(x).\ x\in A\},r) \) by (rule OrderedGroup_ZF_3_L9A )
with A2, A3 show \( \text{IsBounded}(f(A),r) \) using func_imagedef
qed

For linearly ordered groups if \(l\leq a\leq u\) then \(|a|\) is smaller than the greater of \(|l|,|u|\).

lemma (in group3) OrderedGroup_ZF_3_L10:

assumes A1: \( r \text{ is total on } G \) and A2: \( l\leq a \), \( a\leq u \)

shows \( \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \)proof
from A2 have T1: \( \vert l\vert \in G \), \( \vert a\vert \in G \), \( \vert u\vert \in G \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_3_L1, apply_funtype
{
assume A3: \( a\in G^+ \)
with A2 have \( 1 \leq a \), \( a\leq u \) using OrderedGroup_ZF_1_L2
then have \( 1 \leq u \) by (rule Group_order_transitive )
with A2, A3 have \( \vert a\vert \leq \vert u\vert \) using OrderedGroup_ZF_1_L2, OrderedGroup_ZF_3_L2
moreover
from A1, T1 have \( \vert u\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) using Order_ZF_3_L2
ultimately have \( \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) by (rule Group_order_transitive )
}
moreover {
assume A4: \( a\notin G^+ \)
with A2 have T2: \( l\in G \), \( \vert l\vert \in G \), \( \vert a\vert \in G \), \( \vert u\vert \in G \), \( a \in G-G^+ \) using OrderedGroup_ZF_1_L4, OrderedGroup_ZF_3_L1, apply_funtype
with A2 have \( l \in G-G^+ \) using OrderedGroup_ZF_1_L4D
with T2, A2 have \( \vert a\vert \leq \vert l\vert \) using OrderedGroup_ZF_3_L3, OrderedGroup_ZF_1_L5
moreover
from A1, T2 have \( \vert l\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) using Order_ZF_3_L2
ultimately have \( \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) by (rule Group_order_transitive )
} ultimately show \( thesis \)
qed

For linearly ordered groups if a set is bounded then the absolute values are bounded.

lemma (in group3) OrderedGroup_ZF_3_L10A:

assumes A1: \( r \text{ is total on } G \) and A2: \( \text{IsBounded}(A,r) \)

shows \( \exists L.\ \forall a\in A.\ \vert a\vert \leq L \)proof
{
assume \( A = 0 \)
then have \( thesis \)
}
moreover {
assume A3: \( A\neq 0 \)
with A2 have \( \exists u.\ \forall g\in A.\ g\leq u \) and \( \exists l.\ \forall g\in A.\ l\leq g \) using IsBounded_def, IsBoundedAbove_def, IsBoundedBelow_def
then obtain \( u \) \( l \) where \( \forall g\in A.\ l\leq g \wedge g\leq u \)
with A1 have \( \forall a\in A.\ \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) using OrderedGroup_ZF_3_L10
then have \( thesis \)
} ultimately show \( thesis \)
qed

A slightly more general version of the previous lemma, stating the same fact for a set defined by separation.

lemma (in group3) OrderedGroup_ZF_3_L11:

assumes \( r \text{ is total on } G \) and \( \text{IsBounded}(\{b(x).\ x\in X\},r) \)

shows \( \exists L.\ \forall x\in X.\ \vert b(x)\vert \leq L \) using assms, OrderedGroup_ZF_3_L10A

Absolute values of elements of a finite image of a nonempty set are bounded by an element of the group.

lemma (in group3) OrderedGroup_ZF_3_L11A:

assumes A1: \( r \text{ is total on } G \) and A2: \( X\neq 0 \) and A3: \( \{b(x).\ x\in X\} \in Fin(G) \)

shows \( \exists L\in G.\ \forall x\in X.\ \vert b(x)\vert \leq L \)proof
from A1, A3 have \( \exists L.\ \forall x\in X.\ \vert b(x)\vert \leq L \) using ord_group_fin_bounded, OrderedGroup_ZF_3_L11
then obtain \( L \) where I: \( \forall x\in X.\ \vert b(x)\vert \leq L \) using OrderedGroup_ZF_3_L11
from A2 obtain \( x \) where \( x\in X \)
with I show \( thesis \) using OrderedGroup_ZF_1_L4
qed

In totally ordered groups the absolute value of a nonunit element is in \( G_+ \).

lemma (in group3) OrderedGroup_ZF_3_L12:

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

shows \( \vert a\vert \in G_+ \)proof
from A1, A2 have \( \vert a\vert \in G \), \( 1 \leq \vert a\vert \) using OrderedGroup_ZF_3_L1, apply_funtype, OrderedGroup_ZF_3_L3B, OrderedGroup_ZF_1_L2
moreover
from A2, A3 have \( \vert a\vert \neq 1 \) using OrderedGroup_ZF_3_L3D
ultimately show \( \vert a\vert \in G_+ \) using PositiveSet_def
qed

Maximum absolute value of a set

Quite often when considering inequalities we prefer to talk about the absolute values instead of raw elements of a set. This section formalizes some material that is useful for that.

If a set has a maximum and minimum, then the greater of the absolute value of the maximum and minimum belongs to the image of the set by the absolute value function.

lemma (in group3) OrderedGroup_ZF_4_L1:

assumes \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( M = \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)

shows \( M \in \text{AbsoluteValue}(G,P,r)(A) \) using ordGroupAssum, assms, IsAnOrdGroup_def, IsPartOrder_def, Order_ZF_4_L3, Order_ZF_4_L4, OrderedGroup_ZF_3_L1, func_imagedef, GreaterOf_def

If a set has a maximum and minimum, then the greater of the absolute value of the maximum and minimum bounds absolute values of all elements of the set.

lemma (in group3) OrderedGroup_ZF_4_L2:

assumes A1: \( r \text{ is total on } G \) and A2: \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and A3: \( a\in A \)

shows \( \vert a\vert \leq \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)proof
from ordGroupAssum, A2, A3 have \( \text{Minimum}(r,A)\leq a \), \( a\leq \text{Maximum}(r,A) \) using IsAnOrdGroup_def, IsPartOrder_def, Order_ZF_4_L3, Order_ZF_4_L4
with A1 show \( thesis \) by (rule OrderedGroup_ZF_3_L10 )
qed

If a set has a maximum and minimum, then the greater of the absolute value of the maximum and minimum bounds absolute values of all elements of the set. In this lemma the absolute values of ekements of a set are represented as the elements of the image of the set by the absolute value function.

lemma (in group3) OrderedGroup_ZF_4_L3:

assumes \( r \text{ is total on } G \) and \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( b \in \text{AbsoluteValue}(G,P,r)(A) \)

shows \( b\leq \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \) using assms, OrderedGroup_ZF_3_L1, func_imagedef, OrderedGroup_ZF_4_L2

If a set has a maximum and minimum, then the set of absolute values also has a maximum.

lemma (in group3) OrderedGroup_ZF_4_L4:

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

shows \( \text{HasAmaximum}(r, \text{AbsoluteValue}(G,P,r)(A)) \)proof
let \( M = \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)
from A2, A3 have \( M \in \text{AbsoluteValue}(G,P,r)(A) \) using OrderedGroup_ZF_4_L1
moreover
from A1, A2, A3 have \( \forall b \in \text{AbsoluteValue}(G,P,r)(A).\ b \leq M \) using OrderedGroup_ZF_4_L3
ultimately show \( thesis \) using HasAmaximum_def
qed

If a set has a maximum and a minimum, then all absolute values are bounded by the maximum of the set of absolute values.

lemma (in group3) OrderedGroup_ZF_4_L5:

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

shows \( \vert a\vert \leq \text{Maximum}(r, \text{AbsoluteValue}(G,P,r)(A)) \)proof
from A2, A4 have \( \vert a\vert \in \text{AbsoluteValue}(G,P,r)(A) \) using OrderedGroup_ZF_3_L1, func_imagedef
with ordGroupAssum, A1, A2, A3 show \( thesis \) using IsAnOrdGroup_def, IsPartOrder_def, OrderedGroup_ZF_4_L4, Order_ZF_4_L3
qed

Alternative definitions

Sometimes it is usful to define the order by prescibing the set of positive or nonnegative elements. This section deals with two such definitions. One takes a subset \(H\) of \(G\) that is closed under the group operation, \(1\notin H\) and for every \(a\in H\) we have either \(a\in H\) or \(a^{-1}\in H\). Then the order is defined as \(a\leq b\) iff \(a=b\) or \(a^{-1}b \in H\). For abelian groups this makes a linearly ordered group. We will refer to order defined this way in the comments as the order defined by a positive set. The context used in this section is the group0 context defined in Group_ZF theory. Recall that f in that context denotes the group operation (unlike in the previous sections where the group operation was denoted P.

The order defined by a positive set is the same as the order defined by a nonnegative set.

lemma (in group0) OrderedGroup_ZF_5_L1:

assumes A1: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)

shows \( \langle a,b\rangle \in r \longleftrightarrow a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \)proof
assume \( \langle a,b\rangle \in r \)
with A1 show \( a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \) using group0_2_L6
next
assume \( a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \)
then have \( a\in G \wedge b\in G \wedge b=(a^{-1})^{-1} \vee a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \) using inverse_in_group, group0_2_L9
with A1 show \( \langle a,b\rangle \in r \) using group_inv_of_inv
qed

The relation defined by a positive set is antisymmetric.

lemma (in group0) OrderedGroup_ZF_5_L2:

assumes A1: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and A2: \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \)

shows \( \text{antisym}(r) \)proof
{
fix \( a \) \( b \)
assume A3: \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)
with A1 have T: \( a\in G \), \( b\in G \)
{
assume A4: \( a\neq b \)
with A1, A3 have \( a^{-1}\cdot b \in G \), \( a^{-1}\cdot b \in H \), \( (a^{-1}\cdot b)^{-1} \in H \) using inverse_in_group, group0_2_L1, group0_1_L1, group0_2_L12
with A2 have \( a^{-1}\cdot b = 1 \) using Xor_def
with T, A4 have \( False \) using group0_2_L11
}
then have \( a=b \)
}
then show \( \text{antisym}(r) \) by (rule antisymI )
qed

The relation defined by a positive set is transitive.

lemma (in group0) OrderedGroup_ZF_5_L3:

assumes A1: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and A2: \( H\subseteq G \), \( H \text{ is closed under } P \)

shows \( \text{trans}(r) \)proof
{
fix \( a \) \( b \) \( c \)
assume \( \langle a,b\rangle \in r \), \( \langle b,c\rangle \in r \)
with A1 have \( a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \), \( b\in G \wedge c\in G \wedge b^{-1}\cdot c \in H \cup \{1 \} \) using OrderedGroup_ZF_5_L1
with A2 have I: \( a\in G \), \( b\in G \), \( c\in G \) and \( (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \in H \cup \{1 \} \) using inverse_in_group, group0_2_L17, IsOpClosed_def
moreover
from I have \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \) by (rule group0_2_L14A )
ultimately have \( \langle a,c\rangle \in G\times G \), \( a^{-1}\cdot c \in H \cup \{1 \} \)
with A1 have \( \langle a,c\rangle \in r \) using OrderedGroup_ZF_5_L1
}
then have \( \forall a b c.\ \langle a, b\rangle \in r \wedge \langle b, c\rangle \in r \longrightarrow \langle a, c\rangle \in r \)
then show \( \text{trans}(r) \) by (rule Fol1_L2 )
qed

The relation defined by a positive set is translation invariant. With our definition this step requires the group to be abelian.

lemma (in group0) OrderedGroup_ZF_5_L4:

assumes A1: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and A2: \( P \text{ is commutative on } G \) and A3: \( \langle a,b\rangle \in r \) and A4: \( c\in G \)

shows \( \langle a\cdot c,b\cdot c\rangle \in r \wedge \langle c\cdot a,c\cdot b\rangle \in r \)proof
from A1, A3, A4 have I: \( a\in G \), \( b\in G \), \( a\cdot c \in G \), \( b\cdot c \in G \) and II: \( a^{-1}\cdot b \in H \cup \{1 \} \) using OrderedGroup_ZF_5_L1, group_op_closed
with A2, A4 have \( (a\cdot c)^{-1}\cdot (b\cdot c) \in H \cup \{1 \} \) using group0_4_L6D
with A1, I show \( \langle a\cdot c,b\cdot c\rangle \in r \) using OrderedGroup_ZF_5_L1
with A2, A4, I show \( \langle c\cdot a,c\cdot b\rangle \in r \) using IsCommutative_def
qed

If \(H\subseteq G\) is closed under the group operation \(1\notin H\) and for every \(a\in H\) we have either \(a\in H\) or \(a^{-1}\in H\), then the relation "\(\leq\)" defined by \(a\leq b \Leftrightarrow a^{-1}b \in H\) orders the group \(G\). In such order \(H\) may be the set of positive or nonnegative elements.

lemma (in group0) OrderedGroup_ZF_5_L5:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( H\subseteq G \), \( H \text{ is closed under } P \) and A3: \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \) and A4: \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)

shows \( \text{IsAnOrdGroup}(G,P,r) \), \( r \text{ is total on } G \), \( \text{Nonnegative}(G,P,r) = \text{PositiveSet}(G,P,r) \cup \{1 \} \)proof
from groupAssum, A2, A3, A4 have \( \text{IsAgroup}(G,P) \), \( r \subseteq G\times G \), \( \text{IsPartOrder}(G,r) \) using refl_def, OrderedGroup_ZF_5_L2, OrderedGroup_ZF_5_L3, IsPartOrder_def
moreover
from A1, A4 have \( \forall g\in G.\ \forall a b.\ \langle a,b\rangle \in r \longrightarrow \langle a\cdot g,b\cdot g\rangle \in r \wedge \langle g\cdot a,g\cdot b\rangle \in r \) using OrderedGroup_ZF_5_L4
ultimately show \( \text{IsAnOrdGroup}(G,P,r) \) using IsAnOrdGroup_def
then show \( \text{Nonnegative}(G,P,r) = \text{PositiveSet}(G,P,r) \cup \{1 \} \) using group3_def, OrderedGroup_ZF_1_L24
{
fix \( a \) \( b \)
assume T: \( a\in G \), \( b\in G \)
then have T1: \( a^{-1}\cdot b \in G \) using inverse_in_group, group_op_closed
{
assume \( \langle a,b\rangle \notin r \)
with A4, T have I: \( a\neq b \) and II: \( a^{-1}\cdot b \notin H \)
from A3, T, T1, I have \( (a^{-1}\cdot b \in H) \text{ Xor } ((a^{-1}\cdot b)^{-1} \in H) \) using group0_2_L11
with A4, T, II have \( \langle b,a\rangle \in r \) using Xor_def, group0_2_L12
}
then have \( \langle a,b\rangle \in r \vee \langle b,a\rangle \in r \)
}
then show \( r \text{ is total on } G \) using IsTotal_def
qed

If the set defined as in OrderedGroup_ZF_5_L4 does not contain the neutral element, then it is the positive set for the resulting order.

lemma (in group0) OrderedGroup_ZF_5_L6:

assumes \( P \text{ is commutative on } G \) and \( H\subseteq G \) and \( 1 \notin H \) and \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)

shows \( \text{PositiveSet}(G,P,r) = H \) using assms, group_inv_of_one, group0_2_L2, PositiveSet_def

The next definition describes how we construct an order relation from the prescribed set of positive elements.

definition

\( \text{OrderFromPosSet}(G,P,H) \equiv \) \( \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee P\langle \text{GroupInv}(G,P)(\text{fst}(p)),\text{snd}(p)\rangle \in H \} \)

The next theorem rephrases lemmas OrderedGroup_ZF_5_L5 and OrderedGroup_ZF_5_L6 using the definition of the order from the positive set OrderFromPosSet. To summarize, this is what it says: Suppose that \(H\subseteq G\) is a set closed under that group operation such that \(1\notin H\) and for every nonunit group element \(a\) either \(a\in H\) or \(a^{-1}\in H\). Define the order as \(a\leq b\) iff \(a=b\) or \(a^{-1}\cdot b \in H\). Then this order makes \(G\) into a linearly ordered group such \(H\) is the set of positive elements (and then of course \(H \cup \{1\}\) is the set of nonnegative elements).

theorem (in group0) Group_ord_by_positive_set:

assumes \( P \text{ is commutative on } G \) and \( H\subseteq G \), \( H \text{ is closed under } P \), \( 1 \notin H \) and \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \)

shows \( \text{IsAnOrdGroup}(G,P, \text{OrderFromPosSet}(G,P,H)) \), \( \text{OrderFromPosSet}(G,P,H) \text{ is total on } G \), \( \text{PositiveSet}(G,P, \text{OrderFromPosSet}(G,P,H)) = H \), \( \text{Nonnegative}(G,P, \text{OrderFromPosSet}(G,P,H)) = H \cup \{1 \} \) using assms, OrderFromPosSet_def, OrderedGroup_ZF_5_L5, OrderedGroup_ZF_5_L6

Odd Extensions

In this section we verify properties of odd extensions of functions defined on \(G_+\). An odd extension of a function \(f: G_+ \rightarrow G\) is a function \(f^\circ : G\rightarrow G\) defined by \(f^\circ (x) = f(x)\) if \(x\in G_+\), \(f(1) = 1\) and \(f^\circ (x) = (f(x^{-1}))^{-1}\) for \(x < 1\). Such function is the unique odd function that is equal to \(f\) when restricted to \(G_+\).

The next lemma is just to see the definition of the odd extension in the notation used in the group1 context.

lemma (in group3) OrderedGroup_ZF_6_L1:

shows \( f^\circ = f \cup \{\langle a, (f(a^{-1}))^{-1}\rangle .\ a \in -G_+\} \cup \{\langle 1 ,1 \rangle \} \) using OddExtension_def

A technical lemma that states that from a function defined on \( G_+ \) with values in \(G\) we have \((f(a^{-1}))^{-1}\in G\).

lemma (in group3) OrderedGroup_ZF_6_L2:

assumes \( f: G_+\rightarrow G \) and \( a\in -G_+ \)

shows \( f(a^{-1}) \in G \), \( (f(a^{-1}))^{-1} \in G \) using assms, OrderedGroup_ZF_1_L27, apply_funtype, OrderedGroup_ZF_1_L1, inverse_in_group

The main theorem about odd extensions. It basically says that the odd extension of a function is what we want to to be.

lemma (in group3) odd_ext_props:

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

shows \( f^\circ : G \rightarrow G \), \( \forall a\in G_+.\ (f^\circ )(a) = f(a) \), \( \forall a\in (-G_+).\ (f^\circ )(a) = (f(a^{-1}))^{-1} \), \( (f^\circ )(1 ) = 1 \)proof
from A1, A2 have I: \( f: G_+\rightarrow G \), \( \forall a\in -G_+.\ (f(a^{-1}))^{-1} \in G \), \( G_+\cap (-G_+) = 0 \), \( 1 \notin G_+\cup (-G_+) \), \( f^\circ = f \cup \{\langle a, (f(a^{-1}))^{-1}\rangle .\ a \in -G_+\} \cup \{\langle 1 ,1 \rangle \} \) using OrderedGroup_ZF_6_L2, OrdGroup_decomp2, OrderedGroup_ZF_6_L1
then have \( f^\circ : G_+ \cup (-G_+) \cup \{1 \} \rightarrow G\cup G\cup \{1 \} \) by (rule func1_1_L11E )
moreover
from A1 have \( G_+ \cup (-G_+) \cup \{1 \} = G \), \( G\cup G\cup \{1 \} = G \) using OrdGroup_decomp2, OrderedGroup_ZF_1_L1, group0_2_L2
ultimately show \( f^\circ : G \rightarrow G \)
from I show \( \forall a\in G_+.\ (f^\circ )(a) = f(a) \) by (rule func1_1_L11E )
from I show \( \forall a\in (-G_+).\ (f^\circ )(a) = (f(a^{-1}))^{-1} \) by (rule func1_1_L11E )
from I show \( (f^\circ )(1 ) = 1 \) by (rule func1_1_L11E )
qed

Odd extensions are odd, of course.

lemma (in group3) oddext_is_odd:

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

shows \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \)proof
from A1, A3 have \( a\in G_+ \vee a \in (-G_+) \vee a=1 \) using OrdGroup_decomp2
moreover {
assume \( a\in G_+ \)
with A1, A2 have \( a^{-1} \in -G_+ \) and \( (f^\circ )(a) = f(a) \) using OrderedGroup_ZF_1_L25, odd_ext_props
with A1, A2 have \( (f^\circ )(a^{-1}) = (f((a^{-1})^{-1}))^{-1} \) and \( (f(a))^{-1} = ((f^\circ )(a))^{-1} \) using odd_ext_props
with A3 have \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
} moreover {
assume A4: \( a \in -G_+ \)
with A1, A2 have \( a^{-1} \in G_+ \) and \( (f^\circ )(a) = (f(a^{-1}))^{-1} \) using OrderedGroup_ZF_1_L27, odd_ext_props
with A1, A2, A4 have \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \) using odd_ext_props, OrderedGroup_ZF_6_L2, OrderedGroup_ZF_1_L1, group_inv_of_inv
} moreover {
assume \( a = 1 \)
with A1, A2 have \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \) using OrderedGroup_ZF_1_L1, group_inv_of_one, odd_ext_props
} ultimately show \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \)
qed

Another way of saying that odd extensions are odd.

lemma (in group3) oddext_is_odd_alt:

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

shows \( ((f^\circ )(a^{-1}))^{-1} = (f^\circ )(a) \)proof
from A1, A2 have \( f^\circ : G \rightarrow G \), \( \forall a\in G.\ (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \) using odd_ext_props, oddext_is_odd
then have \( \forall a\in G.\ ((f^\circ )(a^{-1}))^{-1} = (f^\circ )(a) \) using OrderedGroup_ZF_1_L1, group0_6_L2
with A3 show \( ((f^\circ )(a^{-1}))^{-1} = (f^\circ )(a) \)
qed

Functions with infinite limits

In this section we consider functions \(f: G\rightarrow G\) with the property that for \(f(x)\) is arbitrarily large for large enough \(x\). More precisely, for every \(a\in G\) there exist \(b\in G_+\) such that for every \(x\geq b\) we have \(f(x)\geq a\). In a sense this means that \(\lim_{x\rightarrow \infty}f(x) = \infty\), hence the title of this section. We also prove dual statements for functions such that \(\lim_{x\rightarrow -\infty}f(x) = -\infty\).

If an image of a set by a function with infinite positive limit is bounded above, then the set itself is bounded above.

lemma (in group3) OrderedGroup_ZF_7_L1:

assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( f:G\rightarrow G \) and A4: \( \forall a\in G.\ \exists b\in G_+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) and A5: \( A\subseteq G \) and A6: \( \text{IsBoundedAbove}(f(A),r) \)

shows \( \text{IsBoundedAbove}(A,r) \)proof
{
assume \( \neg \text{IsBoundedAbove}(A,r) \)
then have I: \( \forall u.\ \exists x\in A.\ \neg (x\leq u) \) using IsBoundedAbove_def
have \( \forall a\in G.\ \exists y\in f(A).\ a\leq y \)proof
{
fix \( a \)
assume \( a\in G \)
with A4 obtain \( b \) where II: \( b\in G_+ \) and III: \( \forall x.\ b\leq x \longrightarrow a \leq f(x) \)
from I obtain \( x \) where IV: \( x\in A \) and \( \neg (x\leq b) \)
with A1, A5, II have \( r \text{ is total on } G \), \( x\in G \), \( b\in G \), \( \neg (x\leq b) \) using PositiveSet_def
with III have \( a \leq f(x) \) using OrderedGroup_ZF_1_L8
with A3, A5, IV have \( \exists y\in f(A).\ a\leq y \) using func_imagedef
}
thus \( thesis \)
qed
with A1, A2, A6 have \( False \) using OrderedGroup_ZF_2_L2A
}
thus \( thesis \)
qed

If an image of a set defined by separation by a function with infinite positive limit is bounded above, then the set itself is bounded above.

lemma (in group3) OrderedGroup_ZF_7_L2:

assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( X\neq 0 \) and A4: \( f:G\rightarrow G \) and A5: \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq f(y) \) and A6: \( \forall x\in X.\ b(x) \in G \wedge f(b(x)) \leq U \)

shows \( \exists u.\ \forall x\in X.\ b(x) \leq u \)proof
let \( A = \{b(x).\ x\in X\} \)
from A6 have I: \( A\subseteq G \)
moreover
note assms
moreover
have \( \text{IsBoundedAbove}(f(A),r) \)proof
from A4, A6, I have \( \forall z\in f(A).\ \langle z,U\rangle \in r \) using func_imagedef
then show \( \text{IsBoundedAbove}(f(A),r) \) by (rule Order_ZF_3_L10 )
qed
ultimately have \( \text{IsBoundedAbove}(A,r) \) using OrderedGroup_ZF_7_L1
with A3 have \( \exists u.\ \forall y\in A.\ y \leq u \) using IsBoundedAbove_def
then show \( \exists u.\ \forall x\in X.\ b(x) \leq u \)
qed

If the image of a set defined by separation by a function with infinite negative limit is bounded below, then the set itself is bounded above. This is dual to OrderedGroup_ZF_7_L2.

lemma (in group3) OrderedGroup_ZF_7_L3:

assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( X\neq 0 \) and A4: \( f:G\rightarrow G \) and A5: \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a \) and A6: \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \)

shows \( \exists l.\ \forall x\in X.\ l \leq b(x) \)proof
let \( g = \text{GroupInv}(G,P)\circ f\circ \text{GroupInv}(G,P) \)
from ordGroupAssum have I: \( \text{GroupInv}(G,P) : G\rightarrow G \) using IsAnOrdGroup_def, group0_2_T2
with A4 have II: \( \forall x\in G.\ g(x) = (f(x^{-1}))^{-1} \) using func1_1_L18
note A1, A2, A3
moreover
from A4, I have \( g : G\rightarrow G \) using comp_fun
moreover
have \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq g(y) \)proof
{
fix \( a \)
assume A7: \( a\in G \)
then have \( a^{-1} \in G \) using OrderedGroup_ZF_1_L1, inverse_in_group
with A5 obtain \( b \) where III: \( b\in G_+ \) and \( \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a^{-1} \)
with II, A7 have \( \forall y.\ b\leq y \longrightarrow a \leq g(y) \) using OrderedGroup_ZF_1_L5AD, OrderedGroup_ZF_1_L4
with III have \( \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq g(y) \)
}
then show \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq g(y) \)
qed
moreover
have \( \forall x\in X.\ b(x)^{-1} \in G \wedge g(b(x)^{-1}) \leq L^{-1} \)proof
{
fix \( x \)
assume \( x\in X \)
with A6 have T: \( b(x) \in G \), \( b(x)^{-1} \in G \) and \( L \leq f(b(x)) \) using OrderedGroup_ZF_1_L1, inverse_in_group
then have \( (f(b(x)))^{-1} \leq L^{-1} \) using OrderedGroup_ZF_1_L5
moreover
from II, T have \( (f(b(x)))^{-1} = g(b(x)^{-1}) \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
ultimately have \( g(b(x)^{-1}) \leq L^{-1} \)
with T have \( b(x)^{-1} \in G \wedge g(b(x)^{-1}) \leq L^{-1} \)
}
then show \( \forall x\in X.\ b(x)^{-1} \in G \wedge g(b(x)^{-1}) \leq L^{-1} \)
qed
ultimately have \( \exists u.\ \forall x\in X.\ (b(x))^{-1} \leq u \) by (rule OrderedGroup_ZF_7_L2 )
then have \( \exists u.\ \forall x\in X.\ u^{-1} \leq (b(x)^{-1})^{-1} \) using OrderedGroup_ZF_1_L5
with A6 show \( \exists l.\ \forall x\in X.\ l \leq b(x) \) using OrderedGroup_ZF_1_L1, group_inv_of_inv
qed

The next lemma combines OrderedGroup_ZF_7_L2 and OrderedGroup_ZF_7_L3 to show that if an image of a set defined by separation by a function with infinite limits is bounded, then the set itself i bounded.

lemma (in group3) OrderedGroup_ZF_7_L4:

assumes A1: \( r \text{ is total on } G \) and A2: \( G \neq \{1 \} \) and A3: \( X\neq 0 \) and A4: \( f:G\rightarrow G \) and A5: \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq f(y) \) and A6: \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a \) and A7: \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \wedge f(b(x)) \leq U \)

shows \( \exists M.\ \forall x\in X.\ \vert b(x)\vert \leq M \)proof
from A7 have I: \( \forall x\in X.\ b(x) \in G \wedge f(b(x)) \leq U \) and II: \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \)
from A1, A2, A3, A4, A5, I have \( \exists u.\ \forall x\in X.\ b(x) \leq u \) by (rule OrderedGroup_ZF_7_L2 )
moreover
from A1, A2, A3, A4, A6, II have \( \exists l.\ \forall x\in X.\ l \leq b(x) \) by (rule OrderedGroup_ZF_7_L3 )
ultimately have \( \exists u l.\ \forall x\in X.\ l\leq b(x) \wedge b(x) \leq u \)
with A1 have \( \exists u l.\ \forall x\in X.\ \vert b(x)\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \) using OrderedGroup_ZF_3_L10
then show \( \exists M.\ \forall x\in X.\ \vert b(x)\vert \leq M \)
qed
end
lemma (in group3) OrderedGroup_ZF_1_L4E: shows \( G^+ \subseteq G \)
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 ) ) \)
theorem group0_2_T2:

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

shows \( \text{GroupInv}(G,f) : G\rightarrow G \)
Definition of AbsoluteValue: \( \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)) \)
lemma func1_1_L1:

assumes \( f:A\rightarrow C \)

shows \( domain(f) = A \)
lemma (in group3) OrderedGroup_ZF_1_L3A: shows \( 1 \in G^+ \)
lemma (in group3) OrderedGroup_ZF_3_L2:

assumes \( a\in G^+ \)

shows \( \vert a\vert = a \)
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\} \)
Definition of Nonnegative: \( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)
lemma (in group3) OrderedGroup_ZF_3_L2A: shows \( \vert 1 \vert = 1 \)
lemma (in group3) OrderedGroup_ZF_1_L1: shows \( group0(G,P) \)
lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
lemma (in group3) OrderedGroup_ZF_1_L4C:

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

shows \( a \in G-G^+ \)
lemma (in group3) OrderedGroup_ZF_3_L3:

assumes \( a \in G-G^+ \)

shows \( \vert a\vert = 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 group3) OrderedGroup_ZF_3_L1: shows \( \text{AbsoluteValue}(G,P,r) : G\rightarrow G \)
lemma (in group3) OrderedGroup_ZF_3_L3B:

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

shows \( \vert a\vert \in G^+ \)
lemma func1_1_L1A:

assumes \( f:X\rightarrow Y \) and \( \forall x\in X.\ f(x) \in Z \)

shows \( f:X\rightarrow Z \)
lemma (in group0) group0_2_L8A:

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

shows \( a = 1 \)
lemma (in group3) OrderedGroup_ZF_1_L2: shows \( g\in G^+ \longleftrightarrow 1 \leq g \)
lemma (in group3) OrderedGroup_ZF_1_L4:

assumes \( a\leq b \)

shows \( a\in G \), \( b\in G \)
lemma (in group3) OrderedGroup_ZF_1_L3:

assumes \( g\in G \)

shows \( g\leq g \)
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 \)
lemma (in group3) OrderedGroup_ZF_1_L5:

assumes \( a\leq b \)

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

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

shows \( a\leq c \)
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_3_L5:

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

shows \( a \leq \vert a\vert \)
lemma (in group3) OrderedGroup_ZF_3_L6:

assumes \( a\in G \)

shows \( a^{-1} \leq \vert a\vert \)
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 group0) group_inv_of_inv:

assumes \( a\in G \)

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

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

shows \( \vert a\vert \leq b \)
lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)
lemma (in group3) OrderedGroup_ZF_3_L7:

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

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

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

shows \( a=b \)
lemma (in group0) group0_2_L1: shows \( monoid0(G,P) \)
lemma (in monoid0) group0_1_L1:

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

shows \( a\oplus b \in G \)
lemma (in group3) OrderedGroup_ZF_3_L7A:

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

shows \( \vert a^{-1}\vert = \vert a\vert \)
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 (in group0) group_inv_of_two:

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

shows \( b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} \)
Definition of IsCommutative: \( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
theorem (in group3) OrdGroup_triangle_ineq:

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

shows \( \vert a\cdot b\vert \leq \vert a\vert \cdot \vert b\vert \)
lemma (in group3) OrderedGroup_ZF_3_L7C:

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \), \( a\in G \), \( b\in G \) and \( \vert a\vert \leq c \), \( \vert b\vert \leq d \)

shows \( \vert a\cdot b\vert \leq c\cdot d \)
lemma (in group0) group_op_closed:

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

shows \( a\cdot b \in G \)
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_L5C:

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

shows \( a\leq b_1\cdot c \)
lemma (in group3) OrderedGroup_ZF_1_L5H:

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

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

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \) and \( \vert a\cdot b^{-1}\vert \leq c \)

shows \( \vert a\vert \leq c\cdot \vert b\vert \), \( \vert a\vert \leq \vert b\vert \cdot c \), \( c^{-1}\cdot a \leq b \), \( a\cdot c^{-1} \leq b \), \( a \leq b\cdot c \)
lemma (in group3) OrdGroup_triangle_ineq3:

assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( \vert a\cdot b\cdot c\vert \leq \vert a\vert \cdot \vert b\vert \cdot \vert c\vert \)
lemma (in group0) group0_4_L8:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

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

assumes \( a\in G \) and \( \vert a\vert \leq L \)

shows \( L^{-1}\leq a \)
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) 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_L9C:

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

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

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

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

assumes \( x\in G \)

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

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

shows \( a\leq L \), \( 1 \leq L \)
Definition of IsBoundedAbove: \( \text{IsBoundedAbove}(A,r) \equiv ( A=0 \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in 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 IsBounded: \( \text{IsBounded}(A,r) \equiv ( \text{IsBoundedAbove}(A,r) \wedge \text{IsBoundedBelow}(A,r)) \)
lemma (in group3) OrderedGroup_ZF_3_L9:

assumes \( r \text{ is total on } G \) and \( A\subseteq G \) and \( \forall a\in A.\ \vert a\vert \leq L \)

shows \( \text{IsBounded}(A,r) \)
lemma (in group3) OrderedGroup_ZF_3_L9A:

assumes \( r \text{ is total on } G \) and \( \forall x\in X.\ b(x)\in G \wedge \vert b(x)\vert \leq L \)

shows \( \text{IsBounded}(\{b(x).\ x\in X\},r) \)
lemma func_imagedef:

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

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

assumes \( r \text{ is total on } X \) and \( x\in X \), \( y\in X \)

shows \( \langle x, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle y, \text{GreaterOf}(r,x,y)\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),x\rangle \in r \), \( \langle \text{SmallerOf}(r,x,y),y\rangle \in r \)
lemma (in group3) OrderedGroup_ZF_1_L4D:

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

shows \( b\in G-G^+ \)
lemma (in group3) OrderedGroup_ZF_3_L10:

assumes \( r \text{ is total on } G \) and \( l\leq a \), \( a\leq u \)

shows \( \vert a\vert \leq \text{GreaterOf}(r,\vert l\vert ,\vert u\vert ) \)
lemma (in group3) OrderedGroup_ZF_3_L10A:

assumes \( r \text{ is total on } G \) and \( \text{IsBounded}(A,r) \)

shows \( \exists L.\ \forall a\in A.\ \vert a\vert \leq L \)
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 (in group3) OrderedGroup_ZF_3_L11:

assumes \( r \text{ is total on } G \) and \( \text{IsBounded}(\{b(x).\ x\in X\},r) \)

shows \( \exists L.\ \forall x\in X.\ \vert b(x)\vert \leq L \)
lemma (in group3) OrderedGroup_ZF_3_L3D:

assumes \( a\in G \) and \( \vert a\vert = 1 \)

shows \( a = 1 \)
lemma Order_ZF_4_L3:

assumes \( \text{antisym}(r) \) and \( \text{HasAmaximum}(r,A) \)

shows \( \text{Maximum}(r,A) \in A \), \( \forall x\in A.\ \langle x, \text{Maximum}(r,A)\rangle \in r \)
lemma Order_ZF_4_L4:

assumes \( \text{antisym}(r) \) and \( \text{HasAminimum}(r,A) \)

shows \( \text{Minimum}(r,A) \in A \), \( \forall x\in A.\ \langle \text{Minimum}(r,A),x\rangle \in r \)
Definition of GreaterOf: \( \text{GreaterOf}(r,a,b) \equiv (\text{if }\langle a,b\rangle \in r\text{ then }b\text{ else }a) \)
lemma (in group3) OrderedGroup_ZF_4_L2:

assumes \( r \text{ is total on } G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( a\in A \)

shows \( \vert a\vert \leq \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)
lemma (in group3) OrderedGroup_ZF_4_L1:

assumes \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( M = \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)

shows \( M \in \text{AbsoluteValue}(G,P,r)(A) \)
lemma (in group3) OrderedGroup_ZF_4_L3:

assumes \( r \text{ is total on } G \) and \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \) and \( b \in \text{AbsoluteValue}(G,P,r)(A) \)

shows \( b\leq \text{GreaterOf}(r,\vert \text{Minimum}(r,A)\vert ,\vert \text{Maximum}(r,A)\vert ) \)
Definition of HasAmaximum: \( \text{HasAmaximum}(r,A) \equiv \exists M\in A.\ \forall x\in A.\ \langle x,M\rangle \in r \)
lemma (in group3) OrderedGroup_ZF_4_L4:

assumes \( r \text{ is total on } G \) and \( A \subseteq G \) and \( \text{HasAmaximum}(r,A) \), \( \text{HasAminimum}(r,A) \)

shows \( \text{HasAmaximum}(r, \text{AbsoluteValue}(G,P,r)(A)) \)
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} \)
Definition of Xor: \( p \text{ Xor } q \equiv (p\vee q) \wedge \neg (p \wedge q) \)
lemma (in group0) group0_2_L11:

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

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

assumes \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)

shows \( \langle a,b\rangle \in r \longleftrightarrow a\in G \wedge b\in G \wedge a^{-1}\cdot b \in H \cup \{1 \} \)
lemma (in group0) group0_2_L17:

assumes \( H\subseteq G \) and \( H \text{ is closed under } P \)

shows \( (H \cup \{1 \}) \text{ is closed under } P \)
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_L14A:

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

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

assumes \( \forall x y z.\ \langle x, y\rangle \in r \wedge \langle y, z\rangle \in r \longrightarrow \langle x, z\rangle \in r \)

shows \( \text{trans}(r) \)
lemma (in group0) group0_4_L6D:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b^{-1}\cdot (a\cdot c^{-1})^{-1} = c\cdot b^{-1} \), \( (a\cdot c)^{-1}\cdot (b\cdot c) = a^{-1}\cdot b \), \( a\cdot (b\cdot (c\cdot a^{-1}\cdot b^{-1})) = c \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot a^{-1}) = b \)
lemma (in group0) OrderedGroup_ZF_5_L2:

assumes \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \)

shows \( \text{antisym}(r) \)
lemma (in group0) OrderedGroup_ZF_5_L3:

assumes \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and \( H\subseteq G \), \( H \text{ is closed under } P \)

shows \( \text{trans}(r) \)
lemma (in group0) OrderedGroup_ZF_5_L4:

assumes \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \) and \( P \text{ is commutative on } G \) and \( \langle a,b\rangle \in r \) and \( c\in G \)

shows \( \langle a\cdot c,b\cdot c\rangle \in r \wedge \langle c\cdot a,c\cdot b\rangle \in r \)
lemma (in group3) OrderedGroup_ZF_1_L24: shows \( G^+ = G_+\cup \{1 \} \)
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 OrderFromPosSet: \( \text{OrderFromPosSet}(G,P,H) \equiv \) \( \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee P\langle \text{GroupInv}(G,P)(\text{fst}(p)),\text{snd}(p)\rangle \in H \} \)
lemma (in group0) OrderedGroup_ZF_5_L5:

assumes \( P \text{ is commutative on } G \) and \( H\subseteq G \), \( H \text{ is closed under } P \) and \( \forall a\in G.\ a\neq 1 \longrightarrow (a\in H) \text{ Xor } (a^{-1}\in H) \) and \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)

shows \( \text{IsAnOrdGroup}(G,P,r) \), \( r \text{ is total on } G \), \( \text{Nonnegative}(G,P,r) = \text{PositiveSet}(G,P,r) \cup \{1 \} \)
lemma (in group0) OrderedGroup_ZF_5_L6:

assumes \( P \text{ is commutative on } G \) and \( H\subseteq G \) and \( 1 \notin H \) and \( r = \{p \in G\times G.\ \text{fst}(p) = \text{snd}(p) \vee \text{fst}(p)^{-1}\cdot \text{snd}(p) \in H\} \)

shows \( \text{PositiveSet}(G,P,r) = H \)
Definition of OddExtension: \( \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 \}) \)
lemma (in group3) OrderedGroup_ZF_1_L27:

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

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

assumes \( f: G_+\rightarrow G \) and \( a\in -G_+ \)

shows \( f(a^{-1}) \in G \), \( (f(a^{-1}))^{-1} \in G \)
lemma (in group3) OrdGroup_decomp2:

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

shows \( G = G_+ \cup (-G_+)\cup \{1 \} \), \( G_+\cap (-G_+) = 0 \), \( 1 \notin G_+\cup (-G_+) \)
lemma (in group3) OrderedGroup_ZF_6_L1: shows \( f^\circ = f \cup \{\langle a, (f(a^{-1}))^{-1}\rangle .\ a \in -G_+\} \cup \{\langle 1 ,1 \rangle \} \)
lemma func1_1_L11E:

assumes \( f:X\rightarrow Y \) and \( \forall x\in A.\ b(x)\in B \) and \( X\cap A = \emptyset \) and \( a \notin X\cup A \) and \( g = f \cup \{\langle x,b(x)\rangle .\ x\in A\} \cup \{\langle a,c\rangle \} \)

shows \( g : X\cup A\cup \{a\} \rightarrow Y\cup B\cup \{c\} \), \( \forall x\in X.\ g(x) = f(x) \), \( \forall x\in A.\ g(x) = b(x) \), \( g(a) = c \)
lemma (in group3) OrderedGroup_ZF_1_L25: shows \( (-G_+) = \{a^{-1}.\ a\in G_+\} \), \( (-G_+) \subseteq G \)
lemma (in group3) odd_ext_props:

assumes \( r \text{ is total on } G \) and \( f: G_+\rightarrow G \)

shows \( f^\circ : G \rightarrow G \), \( \forall a\in G_+.\ (f^\circ )(a) = f(a) \), \( \forall a\in (-G_+).\ (f^\circ )(a) = (f(a^{-1}))^{-1} \), \( (f^\circ )(1 ) = 1 \)
lemma (in group3) oddext_is_odd:

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

shows \( (f^\circ )(a^{-1}) = ((f^\circ )(a))^{-1} \)
lemma (in group0) group0_6_L2:

assumes \( p : G\rightarrow G \)

shows \( (\forall a\in G.\ p(a^{-1}) = (p(a))^{-1}) \longleftrightarrow (\forall a\in G.\ (p(a^{-1}))^{-1} = p(a)) \)
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_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_3_L10:

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

shows \( \text{IsBoundedAbove}(A,r) \)
lemma (in group3) OrderedGroup_ZF_7_L1:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall x.\ b\leq x \longrightarrow a \leq f(x) \) and \( A\subseteq G \) and \( \text{IsBoundedAbove}(f(A),r) \)

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

assumes \( f:A\rightarrow B \), \( g:B\rightarrow C \), \( h:C\rightarrow D \) and \( x\in A \)

shows \( (h\circ g\circ f)(x) \in D \), \( (h\circ g\circ f)(x) = h(g(f(x))) \)
lemma (in group3) OrderedGroup_ZF_1_L5AD:

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

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

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( X\neq 0 \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow a \leq f(y) \) and \( \forall x\in X.\ b(x) \in G \wedge f(b(x)) \leq U \)

shows \( \exists u.\ \forall x\in X.\ b(x) \leq u \)
lemma (in group3) OrderedGroup_ZF_7_L3:

assumes \( r \text{ is total on } G \) and \( G \neq \{1 \} \) and \( X\neq 0 \) and \( f:G\rightarrow G \) and \( \forall a\in G.\ \exists b\in G_+.\ \forall y.\ b\leq y \longrightarrow f(y^{-1}) \leq a \) and \( \forall x\in X.\ b(x) \in G \wedge L \leq f(b(x)) \)

shows \( \exists l.\ \forall x\in X.\ l \leq b(x) \)