Up to index of Isabelle/ZF/IsarMathLib
theory OrderedGroup_ZF(* This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.
Copyright (C) 2005, 2006 Slawomir Kolodynski
This program is free software; Redistribution and use in source and binary forms,
with or without modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation and/or
other materials provided with the distribution.
3. The name of the author may not be used to endorse or promote products
derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)
header {*\isaheader{OrderedGroup\_ZF.thy}*}
theory OrderedGroup_ZF imports Group_ZF Order_ZF Finite_ZF_1
begin
text{*This theory file defines and shows the basic properties of (partially
or linearly) ordered groups. We define the set of nonnegative elements
and the absolute value function.
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 @{text "Int_ZF.thy"} that subsets of integers are
bounded iff they are finite. *}
section{*Ordered groups*}
text{*This section defines ordered groups.*}
text{*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$. We define the set of nonnegative elements
in the obvious way as $G^+ =\{x\in G: 1 \leq x\}$. $G_+$ is a
similar set, but without the unit. 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.
We also define the maximum absolute value of a set, that is the maximum
of the set $\{|x|. x\in A\}$.
The odd functions are defined as those having property
$f(a^{-1})=(f(a))^{-1}$. Looks a bit strange in the multiplicative notation.
For linearly oredered 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$.
*}
constdefs
"IsAnOrdGroup(G,P,r) ≡
(IsAgroup(G,P) ∧ r⊆G×G ∧ IsPartOrder(G,r) ∧ (∀g∈G. ∀a b.
<a,b> ∈ r --> <P`<a,g>,P`<b,g> > ∈ r ∧ <P`<g,a>,P`<g,b> > ∈ r ) )"
"Nonnegative(G,P,r) ≡ {x∈G. <TheNeutralElement(G,P),x> ∈ r}"
"PositiveSet(G,P,r) ≡
{x∈G. <TheNeutralElement(G,P),x> ∈ r ∧ TheNeutralElement(G,P)≠ x}"
"AbsoluteValue(G,P,r) ≡ id(Nonnegative(G,P,r)) ∪
restrict(GroupInv(G,P),G - Nonnegative(G,P,r))"
"OddExtension(G,P,r,f) ≡
(f ∪ {⟨a, GroupInv(G,P)`(f`(GroupInv(G,P)`(a)))⟩.
a ∈ GroupInv(G,P)``(PositiveSet(G,P,r))} ∪
{⟨TheNeutralElement(G,P),TheNeutralElement(G,P)⟩})";
(*"MaxAbs(G,P,r,A) ≡ Maximum(r,AbsoluteValue(G,P,r)``(A))"*)
text{*We will use a similar notation for ordered groups as for the generic
groups. @{text "G+"} denotes the set of nonnegative elements
(that satisfy $1\leq a$ and @{text "G+"} is the set of (strictly) positive
elements. @{text "\<sm>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 @{text "f°"} 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 =
fixes G and P and r
assumes ordGroupAssum: "IsAnOrdGroup(G,P,r)"
fixes unit ("\<one>")
defines unit_def [simp]: "\<one> ≡ TheNeutralElement(G,P)"
fixes groper (infixl "·" 70)
defines groper_def [simp]: "a · b ≡ P`<a,b>"
fixes inv ("_¯ " [90] 91)
defines inv_def [simp]: "x¯ ≡ GroupInv(G,P)`(x)"
fixes lesseq (infix "\<lsq>" 68)
defines lesseq_def [simp]: "a \<lsq> b ≡ <a,b> ∈ r"
fixes sless (infix "\<ls>" 68)
defines sless_def [simp]: "a \<ls> b ≡ a\<lsq>b ∧ a≠b"
fixes nonnegative ("G+")
defines nonnegative_def [simp]: "G+ ≡ Nonnegative(G,P,r)"
fixes positive ("G+")
defines nonnegative_def [simp]: "G+ ≡ PositiveSet(G,P,r)"
fixes setinv :: "i=>i" ("\<sm> _" 72)
defines setninv_def [simp]: "\<sm>A ≡ GroupInv(G,P)``(A)"
fixes abs ("| _ |")
defines abs_def [simp]: "|a| ≡ AbsoluteValue(G,P,r)`(a)"
fixes oddext ("_ °")
defines oddext_def [simp]: "f° ≡ OddExtension(G,P,r,f)";
text{*In @{text "group3"} context we can use the theorems proven in the
@{text "group0"} context.*}
lemma (in group3) OrderedGroup_ZF_1_L1: shows "group0(G,P)"
using ordGroupAssum IsAnOrdGroup_def group0_def by simp;
text{*Ordered group (carrier) is not empty. This is a property of
monoids, but it is good to have it handy in the @{text "group3"} context.*}
lemma (in group3) OrderedGroup_ZF_1_L1A: shows "G≠0"
using OrderedGroup_ZF_1_L1 group0.group0_2_L1 monoid0.group0_1_L3A
by blast;
text{*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∈G+ <-> \<one>\<lsq>g"
using ordGroupAssum IsAnOrdGroup_def Nonnegative_def
by auto;
text{*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∈G+ <-> (\<one>\<lsq>g ∧ g≠\<one>)"
using ordGroupAssum IsAnOrdGroup_def PositiveSet_def
by auto;
text{*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 {is total on} G" and A2: "a∈G-G+"
shows "a\<lsq>\<one>"
proof -;
from A2 have "a∈G" "¬(\<one>\<lsq>a)" using OrderedGroup_ZF_1_L2 by auto;
with A1 show ?thesis
using IsTotal_def OrderedGroup_ZF_1_L1 group0.group0_2_L2 by auto;
qed;
text{*The group order is reflexive.*}
lemma (in group3) OrderedGroup_ZF_1_L3: assumes "g∈G"
shows "g\<lsq>g"
using ordGroupAssum prems IsAnOrdGroup_def IsPartOrder_def refl_def
by simp;
text{*$1$ is nonnegative.*}
lemma (in group3) OrderedGroup_ZF_1_L3A: shows "\<one>∈G+"
using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_1_L3
OrderedGroup_ZF_1_L1 group0.group0_2_L2 by simp;
text{*In this context $a \leq b$ implies that both $a$ and $b$ belong
to $G$.*}
lemma (in group3) OrderedGroup_ZF_1_L4:
assumes "a\<lsq>b" shows "a∈G" "b∈G"
using ordGroupAssum prems IsAnOrdGroup_def by auto;
text{*It is good to have transitivity handy.*}
lemma (in group3) Group_order_transitive:
assumes A1: "a\<lsq>b" "b\<lsq>c" shows "a\<lsq>c"
proof -
from ordGroupAssum have "trans(r)"
using IsAnOrdGroup_def IsPartOrder_def
by simp
moreover from A1 have "<a,b> ∈ r ∧ <b,c> ∈ r" by simp;
ultimately have "<a,c> ∈ r" by (rule Fol1_L3);
thus ?thesis by simp;
qed;
text{*The order in an ordered group is antisymmetric.*}
lemma (in group3) group_order_antisym:
assumes A1: "a\<lsq>b" "b\<lsq>a" shows "a=b"
proof -
from ordGroupAssum A1 have
"antisym(r)" "<a,b> ∈ r" "<b,a> ∈ r"
using IsAnOrdGroup_def IsPartOrder_def by auto;
then show "a=b" by (rule Fol1_L4);
qed;
text{*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\<ls>b" and A2: "b\<lsq>c"
shows "a\<ls>c"
proof -
from A1 A2 have "a\<lsq>b" "b\<lsq>c" by auto
then have "a\<lsq>c" by (rule Group_order_transitive);
moreover from A1 A2 have "a≠c" using group_order_antisym by auto;
ultimately show "a\<ls>c" by simp
qed;
(*lemma (in group3) OrderedGroup_ZF_1_L4A:
assumes A1: "a\<lsq>b" and A2: "a≠b" and A3: "b\<lsq>c"
shows "a\<lsq>c" "a≠c"
proof -
from A1 A3 show "a\<lsq>c" by (rule Group_order_transitive);
from A1 A2 A3 show "a≠c" using group_order_antisym by auto;
qed;*)
text{*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\<lsq>b" and A2: "b\<ls>c"
shows "a\<ls>c"
proof -
from A1 A2 have "a\<lsq>b" "b\<lsq>c" by auto
then have "a\<lsq>c" by (rule Group_order_transitive)
moreover from A1 A2 have "a≠c" using group_order_antisym by auto
ultimately show "a\<ls>c" by simp
qed;
(*lemma (in group3) group_strict_ord_transit:
assumes A1: "a\<lsq>b" and A2: "b\<lsq>c" and A3: "b≠c"
shows "a\<lsq>c" "a≠c"
proof -
from A1 A2 show "a\<lsq>c" by (rule Group_order_transitive)
from A1 A2 A3 show "a≠c" using group_order_antisym by auto
qed;*)
text{*Strict order is preserved by translations.*}
lemma (in group3) group_strict_ord_transl_inv:
assumes "a\<ls>b"and "c∈G"
shows
"a·c \<ls> b·c"
"c·a \<ls> c·b"
using ordGroupAssum prems IsAnOrdGroup_def
OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 group0.group0_2_L19
by auto;
(*lemma (in group3) group_strict_ord_transl_inv:
assumes "a\<lsq>b" "a≠b" and "c∈G"
shows "a·c \<lsq> b·c" "a·c ≠ b·c"
using ordGroupAssum prems IsAnOrdGroup_def
OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 group0.group0_2_L19
by auto;*)
text{*If the group order is total, then the group is ordered linearly.*}
lemma (in group3) group_ord_total_is_lin:
assumes "r {is total on} G"
shows "IsLinOrder(G,r)"
using prems ordGroupAssum IsAnOrdGroup_def Order_ZF_1_L3
by simp;
text{*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 {is total on} G"
and "a∈G+" and "b ∈ G-G+"
shows "b\<lsq>a"
proof -;
from prems have "b\<lsq>\<one>" "\<one>\<lsq>a"
using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_1_L2B by auto;
thus ?thesis by (rule Group_order_transitive)
qed;
text{*If $a\leq 1$ and $a\neq 1$, then $a \in G\setminus G^{+}$. *}
lemma (in group3) OrderedGroup_ZF_1_L4C:
assumes A1: "a\<lsq>\<one>" and A2: "a≠\<one>"
shows "a ∈ G-G+"
proof (rule ccontr);
assume "a ∉ G-G+"
with ordGroupAssum A1 A2 show False
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L2
OrderedGroup_ZF_1_L4 IsAnOrdGroup_def IsPartOrder_def antisym_def
by auto;
qed;
text{*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∈G-G+" and A2: "b\<lsq>a"
shows "b∈G-G+"
proof (rule ccontr);
assume "b ∉ G - G+"
with A2 have "\<one>\<lsq>b" "b\<lsq>a"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L2 by auto;
then have "\<one>\<lsq>a" by (rule Group_order_transitive);
with A1 show False using OrderedGroup_ZF_1_L2 by simp;
qed;
text{*The nonnegative set is contained in the group.*}
lemma (in group3) OrderedGroup_ZF_1_L4E: shows "G+ ⊆ G"
using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_1_L4 by auto;
text{*Taking the inverse on both sides reverses the inequality.*}
lemma (in group3) OrderedGroup_ZF_1_L5:
assumes A1: "a\<lsq>b" shows "b¯\<lsq>a¯"
proof -;
from A1 have T1: "a∈G" "b∈G" "a¯∈G" "b¯∈G"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1
group0.inverse_in_group by auto;
with A1 ordGroupAssum have "a·a¯\<lsq>b·a¯" using IsAnOrdGroup_def
by simp;
with T1 ordGroupAssum have "b¯·\<one>\<lsq>b¯·(b·a¯)"
using OrderedGroup_ZF_1_L1 group0.group0_2_L6 IsAnOrdGroup_def
by simp;
with T1 show ?thesis using
OrderedGroup_ZF_1_L1 group0.group0_2_L2 group0.group_oper_assoc
group0.group0_2_L6 by simp;
qed;
text{*If an element is smaller that the unit, then its inverse is greater.*}
lemma (in group3) OrderedGroup_ZF_1_L5A:
assumes A1: "a\<lsq>\<one>" shows "\<one>\<lsq>a¯"
proof -
from A1 have "\<one>¯\<lsq>a¯" using OrderedGroup_ZF_1_L5
by simp;
then show ?thesis using OrderedGroup_ZF_1_L1 group0.group_inv_of_one
by simp;
qed;
text{*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∈G" and A2: "\<one>\<lsq>a¯"
shows "a\<lsq>\<one>"
proof -
from A2 have "(a¯)¯\<lsq>\<one>¯" using OrderedGroup_ZF_1_L5
by simp;
with A1 show "a\<lsq>\<one>"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv group0.group_inv_of_one
by simp;
qed;
text{*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: "\<one>\<lsq>a" shows "a¯\<lsq>\<one>" and "¬(a\<lsq>\<one> ∧ a≠\<one>)"
proof -
from A1 have "a¯\<lsq>\<one>¯"
using OrderedGroup_ZF_1_L5 by simp;
then show "a¯\<lsq>\<one>" using OrderedGroup_ZF_1_L1 group0.group_inv_of_one
by simp;
{ assume "a\<lsq>\<one>" and "a≠\<one>"
with A1 have False using group_order_antisym
by blast;
} then show "¬(a\<lsq>\<one> ∧ a≠\<one>)" by auto;
qed;
text{*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: "\<one>\<lsq>a" "\<one>\<lsq>b"
shows "a¯ \<lsq> b"
proof -
from A1 have "a¯\<lsq>\<one>" "\<one>\<lsq>b"
using OrderedGroup_ZF_1_L5AB by auto
then show "a¯ \<lsq> b" by (rule Group_order_transitive)
qed;
(* we probably should put the stuff about inequalities in a separate section
text{*This section developes some simple tools to deal with inequalities.*}*)
text{*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 ∈ G" and A2: "a\<lsq>b¯"
shows "b \<lsq> a¯"
proof -
from A2 have "(b¯)¯ \<lsq> a¯"
using OrderedGroup_ZF_1_L5 by simp
with A1 show "b \<lsq> a¯"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp
qed;
text{*We can cancel the same element on both sides of an inequality.*}
lemma (in group3) OrderedGroup_ZF_1_L5AE:
assumes A1: "a∈G" "b∈G" "c∈G" and A2: "a·b \<lsq> a·c"
shows "b\<lsq>c"
proof -
from ordGroupAssum A1 A2 have "a¯·(a·b) \<lsq> a¯·(a·c)"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group
IsAnOrdGroup_def by simp;
with A1 show "b\<lsq>c"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16
by simp;
qed;
text{*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∈G" "b∈G" "c∈G" and A2: "a·b¯ \<lsq> a·c¯"
shows "c\<lsq>b"
proof -
from A1 A2 have "(c¯)¯ \<lsq> (b¯)¯"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group
OrderedGroup_ZF_1_L5AE OrderedGroup_ZF_1_L5 by simp;
with A1 show "c\<lsq>b"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv by simp;
qed;
text{*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 ∈ G" and A2: "a¯\<lsq>b"
shows "b¯ \<lsq> a"
proof -
from A2 have "b¯ \<lsq> (a¯)¯"
using OrderedGroup_ZF_1_L5 by simp
with A1 show "b¯ \<lsq> a"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp
qed;
text{*We can multiply the sides of two inequalities.*}
lemma (in group3) OrderedGroup_ZF_1_L5B:
assumes A1: "a\<lsq>b" and A2: "c\<lsq>d"
shows "a·c \<lsq> b·d"
proof -;
from A1 A2 have "c∈G" "b∈G" using OrderedGroup_ZF_1_L4 by auto;
with A1 A2 ordGroupAssum have "a·c\<lsq> b·c" "b·c\<lsq>b·d"
using IsAnOrdGroup_def by auto;
then show "a·c \<lsq> b·d" by (rule Group_order_transitive);
qed;
text{*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∈G" and A2: "a\<lsq>b·c" and A3: "b\<lsq>b1"
shows "a\<lsq>b1·c"
proof -
from A1 A3 have "b·c \<lsq> b1·c"
using OrderedGroup_ZF_1_L3 OrderedGroup_ZF_1_L5B by simp;
with A2 show "a\<lsq>b1·c" by (rule Group_order_transitive);
qed;
text{*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∈G" and A2: "a \<lsq> b·c" and A3: "c\<lsq>b1"
shows "a \<lsq> b·b1"
proof -
from A1 A3 have "b·c \<lsq> b·b1"
using OrderedGroup_ZF_1_L3 OrderedGroup_ZF_1_L5B by auto;
with A2 show "a\<lsq>b·b1" by (rule Group_order_transitive);
qed;
text{*We can replace factors on one side of an inequality
with greater ones.*}
lemma (in group3) OrderedGroup_ZF_1_L5E:
assumes A1: "a \<lsq> b·c" and A2: "b\<lsq>b1" "c\<lsq>c1"
shows "a \<lsq> b1·c1"
proof -
from A2 have "b·c \<lsq> b1·c1" using OrderedGroup_ZF_1_L5B
by simp;
with A1 show "a\<lsq>b1·c1" by (rule Group_order_transitive);
qed;
text{*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: "\<one>\<lsq>a" and A2: "b∈G"
shows "b\<lsq>a·b" "b\<lsq>b·a"
proof -
from ordGroupAssum A1 A2 have
"\<one>·b\<lsq>a·b" "b·\<one>\<lsq>b·a"
using IsAnOrdGroup_def by auto;
with A2 show "b\<lsq>a·b" "b\<lsq>b·a"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2
by auto;
qed;
text{*We can multiply the right hand side of an inequality by a nonnegative
element.*}
lemma (in group3) OrderedGroup_ZF_1_L5G: assumes A1: "a\<lsq>b"
and A2: "\<one>\<lsq>c" shows "a\<lsq>b·c" "a\<lsq>c·b"
proof -
from A1 A2 have I: "b\<lsq>b·c" and II: "b\<lsq>c·b"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L5F by auto
from A1 I show "a\<lsq>b·c" by (rule Group_order_transitive);
from A1 II show "a\<lsq>c·b" by (rule Group_order_transitive);
qed;
text{*We can put two elements on the other side of inequality,
changing their sign.*}
lemma (in group3) OrderedGroup_ZF_1_L5H:
assumes A1: "a∈G" "b∈G" and A2: "a·b¯ \<lsq> c"
shows
"a \<lsq> c·b"
"c¯·a \<lsq> b"
proof -
from A2 have T: "c∈G" "c¯ ∈ G"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1
group0.inverse_in_group by auto;
from ordGroupAssum A1 A2 have "a·b¯·b \<lsq> c·b"
using IsAnOrdGroup_def by simp;
with A1 show "a \<lsq> c·b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16
by simp;
with ordGroupAssum A2 T have "c¯·a \<lsq> c¯·(c·b)"
using IsAnOrdGroup_def by simp;
with A1 T show "c¯·a \<lsq> b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16
by simp;
qed;
text{*We can multiply the sides of one inequality by inverse of another.*}
lemma (in group3) OrderedGroup_ZF_1_L5I:
assumes "a\<lsq>b" and "c\<lsq>d"
shows "a·d¯ \<lsq> b·c¯"
using prems OrderedGroup_ZF_1_L5 OrderedGroup_ZF_1_L5B
by simp;
text{*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∈G" "b∈G" and A2: "c \<lsq> a·b¯"
shows "c·b \<lsq> a"
proof -
from ordGroupAssum A1 A2 have "c·b \<lsq> a·b¯·b"
using IsAnOrdGroup_def by simp;
with A1 show "c·b \<lsq> a"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16
by simp;
qed;
text{*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∈G" "b∈G" and A2: "c \<lsq> a¯·b"
shows "a·c\<lsq> b"
proof -
from ordGroupAssum A1 A2 have "a·c \<lsq> a·(a¯·b)"
using IsAnOrdGroup_def by simp;
with A1 show "a·c\<lsq> b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16
by simp;
qed;
text{*A special case of @{text "OrderedGroup_ZF_1_L5J"} where $c=1$.*}
corollary (in group3) OrderedGroup_ZF_1_L5K:
assumes A1: "a∈G" "b∈G" and A2: "\<one> \<lsq> a·b¯"
shows "b \<lsq> a"
proof -
from A1 A2 have "\<one>·b \<lsq> a"
using OrderedGroup_ZF_1_L5J by simp;
with A1 show "b \<lsq> a"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2
by simp;
qed;
text{*A special case of @{text "OrderedGroup_ZF_1_L5JA"} where $c=1$.*}
corollary (in group3) OrderedGroup_ZF_1_L5KA:
assumes A1: "a∈G" "b∈G" and A2: "\<one> \<lsq> a¯·b"
shows "a \<lsq> b"
proof -
from A1 A2 have "a·\<one> \<lsq> b"
using OrderedGroup_ZF_1_L5JA by simp;
with A1 show "a \<lsq> b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2
by simp;
qed;
text{*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 {is total on} G" and A2: "a∈G-G+"
shows "a\<lsq>\<one>" "a¯ ∈ G+" "restrict(GroupInv(G,P),G-G+)`(a) ∈ G+"
proof -;
from A2 have T1: "a∈G" "a∉G+" "\<one>∈G"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2 by auto;
with A1 show "a\<lsq>\<one>" using OrderedGroup_ZF_1_L2 IsTotal_def
by auto;
then show "a¯ ∈ G+" using OrderedGroup_ZF_1_L5A OrderedGroup_ZF_1_L2
by simp;
with A2 show "restrict(GroupInv(G,P),G-G+)`(a) ∈ G+"
using restrict by simp;
qed;
text{*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 {is total on} G"
and A2: "∀a∈G+.∀b∈G+. Q(a,b)"
and A3: "∀a∈G.∀b∈G. Q(a,b)-->Q(a¯,b)"
and A4: "∀a∈G.∀b∈G. Q(a,b)-->Q(a,b¯)"
and A5: "a∈G" "b∈G"
shows "Q(a,b)"
proof (cases "a∈G+");
assume A6: "a∈G+" show "Q(a,b)"
proof (cases "b∈G+")
assume "b∈G+"
with A6 A2 show "Q(a,b)" by simp;
next assume "b∉G+"
with A1 A2 A4 A5 A6 have "Q(a,(b¯)¯)"
using OrderedGroup_ZF_1_L6 OrderedGroup_ZF_1_L1 group0.inverse_in_group
by simp;
with A5 show "Q(a,b)" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp;
qed;
next assume "a∉G+"
with A1 A5 have T1: "a¯ ∈ G+" using OrderedGroup_ZF_1_L6 by simp;
show "Q(a,b)"
proof (cases "b∈G+")
assume "b∈G+"
with A2 A3 A5 T1 have "Q((a¯)¯,b)"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group by simp;
with A5 show "Q(a,b)" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp;
next assume "b∉G+"
with A1 A2 A3 A4 A5 T1 have "Q((a¯)¯,(b¯)¯)"
using OrderedGroup_ZF_1_L6 OrderedGroup_ZF_1_L1 group0.inverse_in_group
by simp;
with A5 show "Q(a,b)" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp;
qed;
qed;
text{*A lemma about splitting the ordered group "plane" into 6 subsets. Useful
for proofs by cases.*}
lemma (in group3) OrdGroup_6cases: assumes A1: "r {is total on} G"
and A2: "a∈G" "b∈G"
shows
"\<one>\<lsq>a ∧ \<one>\<lsq>b ∨ a\<lsq>\<one> ∧ b\<lsq>\<one> ∨
a\<lsq>\<one> ∧ \<one>\<lsq>b ∧ \<one> \<lsq> a·b ∨ a\<lsq>\<one> ∧ \<one>\<lsq>b ∧ a·b \<lsq> \<one> ∨
\<one>\<lsq>a ∧ b\<lsq>\<one> ∧ \<one> \<lsq> a·b ∨ \<one>\<lsq>a ∧ b\<lsq>\<one> ∧ a·b \<lsq> \<one>"
proof -
from A1 A2 have
"\<one>\<lsq>a ∨ a\<lsq>\<one>"
"\<one>\<lsq>b ∨ b\<lsq>\<one>"
"\<one> \<lsq> a·b ∨ a·b \<lsq> \<one>"
using OrderedGroup_ZF_1_L1 group0.group_op_closed group0.group0_2_L2
IsTotal_def by auto;
then show ?thesis by auto;
qed;
text{*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 {is total on} G"
and A2: "a∈G" "b∈G"
and A3: "¬(a\<lsq>b)"
shows "b \<lsq> a" "a¯ \<lsq> b¯" "a≠b" "b\<ls>a"
proof -
from A1 A2 A3 show I: "b \<lsq> a" using IsTotal_def
by auto;
then show "a¯ \<lsq> b¯" using OrderedGroup_ZF_1_L5 by simp;
from A2 have "a \<lsq> a" using OrderedGroup_ZF_1_L3 by simp;
with I A3 show "a≠b" "b \<ls> a" by auto;
qed;
text{*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\<lsq>b" and A2: "a≠b"
shows "¬(b\<lsq>a)"
proof -
{ note A1
moreover assume "b\<lsq>a"
ultimately have "a=b" by (rule group_order_antisym)
with A2 have False by simp;
} thus "¬(b\<lsq>a)" by auto;
qed;
text{*A special case of @{text "OrderedGroup_ZF_1_L8"} when one of
the elements is the unit.*}
corollary (in group3) OrderedGroup_ZF_1_L8A:
assumes A1: "r {is total on} G"
and A2: "a∈G" and A3: "¬(\<one>\<lsq>a)"
shows "\<one> \<lsq> a¯" "\<one>≠a" "a\<lsq>\<one>"
proof -
from A1 A2 A3 have I:
"r {is total on} G"
"\<one>∈G" "a∈G"
"¬(\<one>\<lsq>a)"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2
by auto;
then have "\<one>¯ \<lsq> a¯"
by (rule OrderedGroup_ZF_1_L8);
then show "\<one> \<lsq> a¯"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_one by simp;
from I show "\<one>≠a" by (rule OrderedGroup_ZF_1_L8);
from A1 I show "a\<lsq>\<one>" using IsTotal_def
by auto;
qed;
text{*A negative element can not be nonnegative.*}
lemma (in group3) OrderedGroup_ZF_1_L8B:
assumes A1: "a\<lsq>\<one>" and A2: "a≠\<one>" shows "¬(\<one>\<lsq>a)"
proof -
{ assume "\<one>\<lsq>a"
with A1 have "a=\<one>" using group_order_antisym
by auto;
with A2 have False by simp;
} thus ?thesis by auto;
qed;
text{*An element is greater or equal than another iff the difference is
nonpositive.*}
lemma (in group3) OrderedGroup_ZF_1_L9:
assumes A1: "a∈G" "b∈G"
shows "a\<lsq>b <-> a·b¯ \<lsq> \<one>"
proof;
assume "a \<lsq> b"
with ordGroupAssum A1 have "a·b¯ \<lsq> b·b¯"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group
IsAnOrdGroup_def by simp;
with A1 show "a·b¯ \<lsq> \<one>"
using OrderedGroup_ZF_1_L1 group0.group0_2_L6
by simp;
next assume A2: "a·b¯ \<lsq> \<one>"
with ordGroupAssum A1 have "a·b¯·b \<lsq> \<one>·b"
using IsAnOrdGroup_def by simp;
with A1 show "a \<lsq> b"
using OrderedGroup_ZF_1_L1
group0.group0_2_L16 group0.group0_2_L2
by simp;
qed;
text{*We can move an element to the other side of an inequality.*}
lemma (in group3) OrderedGroup_ZF_1_L9A:
assumes A1: "a∈G" "b∈G" "c∈G"
shows "a·b \<lsq> c <-> a \<lsq> c·b¯"
proof
assume "a·b \<lsq> c"
with ordGroupAssum A1 have "a·b·b¯ \<lsq> c·b¯"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group IsAnOrdGroup_def
by simp;
with A1 show "a \<lsq> c·b¯"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16 by simp;
next assume "a \<lsq> c·b¯"
with ordGroupAssum A1 have "a·b \<lsq> c·b¯·b"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group IsAnOrdGroup_def
by simp;
with A1 show "a·b \<lsq> c"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16 by simp;
qed;
text{*A one side version of the previous lemma with weaker assuptions.*}
lemma (in group3) OrderedGroup_ZF_1_L9B:
assumes A1: "a∈G" "b∈G" and A2: "a·b¯ \<lsq> c"
shows "a \<lsq> c·b"
proof -
from A1 A2 have "a∈G" "b¯∈G" "c∈G"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group
OrderedGroup_ZF_1_L4 by auto;
with A1 A2 show "a \<lsq> c·b"
using OrderedGroup_ZF_1_L9A OrderedGroup_ZF_1_L1
group0.group_inv_of_inv by simp;
qed;
text{*We can put en element on the other side of inequality,
changing its sign.*}
lemma (in group3) OrderedGroup_ZF_1_L9C:
assumes A1: "a∈G" "b∈G" and A2: "c\<lsq>a·b"
shows
"c·b¯ \<lsq> a"
"a¯·c \<lsq> b"
proof -
from ordGroupAssum A1 A2 have
"c·b¯ \<lsq> a·b·b¯"
"a¯·c \<lsq> a¯·(a·b)"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group IsAnOrdGroup_def
by auto;
with A1 show
"c·b¯ \<lsq> a"
"a¯·c \<lsq> b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16
by auto;
qed;
text{*If an element is greater or equal than another then the difference is
nonnegative.*}
lemma (in group3) OrderedGroup_ZF_1_L9D: assumes A1: "a\<lsq>b"
shows "\<one> \<lsq> b·a¯"
proof -
from A1 have T: "a∈G" "b∈G" "a¯ ∈ G"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1
group0.inverse_in_group by auto
with ordGroupAssum A1 have "a·a¯ \<lsq> b·a¯"
using IsAnOrdGroup_def by simp
with T show "\<one> \<lsq> b·a¯"
using OrderedGroup_ZF_1_L1 group0.group0_2_L6
by simp
qed;
text{*If an element is greater than another then the difference is
positive.*}
lemma (in group3) OrderedGroup_ZF_1_L9E:
assumes A1: "a\<lsq>b" "a≠b"
shows "\<one> \<lsq> b·a¯" "\<one> ≠ b·a¯" "b·a¯ ∈ G+"
proof -
from A1 have T: "a∈G" "b∈G" using OrderedGroup_ZF_1_L4
by auto
from A1 show I: "\<one> \<lsq> b·a¯" using OrderedGroup_ZF_1_L9D
by simp
{ assume "b·a¯ = \<one>"
with T have "a=b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L11A
by auto;
with A1 have False by simp
} then show "\<one> ≠ b·a¯" by auto;
then have "b·a¯ ≠ \<one>" by auto;
with I show "b·a¯ ∈ G+" using OrderedGroup_ZF_1_L2A
by simp;
qed;
text{*If the difference is nonnegative, then $a\leq b$. *}
lemma (in group3) OrderedGroup_ZF_1_L9F:
assumes A1: "a∈G" "b∈G" and A2: "\<one> \<lsq> b·a¯"
shows "a\<lsq>b"
proof -
from A1 A2 have "\<one>·a \<lsq> b"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L9A
by simp;
with A1 show "a\<lsq>b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2
by simp;
qed;
text{*If we increase the middle term in a product, the whole product
increases.*}
lemma (in group3) OrderedGroup_ZF_1_L10:
assumes "a∈G" "b∈G" and "c\<lsq>d"
shows "a·c·b \<lsq> a·d·b"
using ordGroupAssum prems IsAnOrdGroup_def by simp;
text{*A product of (strictly) positive elements is not the unit.*}
lemma (in group3) OrderedGroup_ZF_1_L11:
assumes A1: "\<one>\<lsq>a" "\<one>\<lsq>b"
and A2: "\<one> ≠ a" "\<one> ≠ b"
shows "\<one> ≠ a·b"
proof -
from A1 have T1: "a∈G" "b∈G"
using OrderedGroup_ZF_1_L4 by auto;
{ assume "\<one> = a·b"
with A1 T1 have "a\<lsq>\<one>" "\<one>\<lsq>a"
using OrderedGroup_ZF_1_L1 group0.group0_2_L9 OrderedGroup_ZF_1_L5AA
by auto;
then have "a = \<one>" by (rule group_order_antisym);
with A2 have False by simp;
} then show "\<one> ≠ a·b" by auto;
qed;
text{*A product of nonnegative elements is nonnegative.*}
lemma (in group3) OrderedGroup_ZF_1_L12:
assumes A1: "\<one> \<lsq> a" "\<one> \<lsq> b"
shows "\<one> \<lsq> a·b"
proof -
from A1 have "\<one>·\<one> \<lsq> a·b"
using OrderedGroup_ZF_1_L5B by simp;
then show "\<one> \<lsq> a·b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2
by simp;
qed;
text{*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\<lsq>b" shows "\<one> \<lsq> b·a¯"
proof -
from A1 have T: "\<one> ∈ G" "a∈G" "b∈G"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1 group0.group0_2_L2
by auto;
with A1 have "\<one>·a \<lsq> b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2
by simp;
with T show "\<one> \<lsq> b·a¯" using OrderedGroup_ZF_1_L9A
by simp;
qed;
text{*We can move an element to the other side of a strict inequality.*}
lemma (in group3) OrderedGroup_ZF_1_L12B:
assumes A1: "a∈G" "b∈G" and A2: "a·b¯ \<ls> c"
shows "a \<ls> c·b"
proof -
from A1 A2 have "a·b¯·b \<ls> c·b"
using group_strict_ord_transl_inv by auto;
moreover from A1 have "a·b¯·b = a"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16
by simp
ultimately show "a \<ls> c·b"
by auto
qed;
(*lemma (in group3) OrderedGroup_ZF_1_L12B:
assumes A1: "a∈G" "b∈G" and A2: "a·b¯ \<lsq> c" "a·b¯ ≠ c"
shows "a \<lsq> c·b" "a ≠ c·b"
proof -
from A1 A2 have "a·b¯·b \<lsq> c·b" "a·b¯·b ≠ c·b"
using group_strict_ord_transl_inv by auto
moreover from A1 have "a·b¯·b = a"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16
by simp
ultimately show "a \<lsq> c·b" "a ≠ c·b"
by auto
qed;*)
text{*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\<ls>b" and A2: "c\<lsq>d"
shows "a·c \<ls> b·d"
proof -
from A1 A2 have T: "a∈G" "b∈G" "c∈G" "d∈G"
using OrderedGroup_ZF_1_L4 by auto;
with ordGroupAssum A2 have "a·c \<lsq> a·d"
using IsAnOrdGroup_def by simp;
moreover from A1 T have "a·d \<ls> b·d"
using group_strict_ord_transl_inv by simp;
ultimately show "a·c \<ls> b·d"
by (rule group_strict_ord_transit);
qed;
text{*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\<lsq>b" and A2: "c\<ls>d"
shows "a·c \<ls> b·d"
proof -
from A1 A2 have T: "a∈G" "b∈G" "c∈G" "d∈G"
using OrderedGroup_ZF_1_L4 by auto;
with A2 have "a·c \<ls> a·d"
using group_strict_ord_transl_inv by simp;
moreover from ordGroupAssum A1 T have "a·d \<lsq> b·d"
using IsAnOrdGroup_def by simp;
ultimately show "a·c \<ls> b·d"
by (rule OrderedGroup_ZF_1_L4A);
qed;
section{*The set of positive elements*}
text{*In this section we study @{text "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\}$, @{text "G+"} and the
set of those elements $a\in G$ such that $a^{-1}\in$@{text "G+"}.
Another property of linearly ordered groups that we prove here is that
if @{text "G+"}$\neq \emptyset$, then it is infinite. This allows to show
that nontrivial linearly ordered groups are infinite. *}
text{*The positive set is closed under the group operation.*}
lemma (in group3) OrderedGroup_ZF_1_L13: "G+ {is closed under} P"
proof -
{ fix a b assume "a∈G+" "b∈G+"
then have T1: "\<one> \<lsq> a·b" and "\<one> ≠ a·b"
using PositiveSet_def OrderedGroup_ZF_1_L11 OrderedGroup_ZF_1_L12
by auto;
moreover from T1 have "a·b ∈ G"
using OrderedGroup_ZF_1_L4 by simp;
ultimately have "a·b ∈ G+" using PositiveSet_def by simp;
} then show "G+ {is closed under} P" using IsOpClosed_def
by simp;
qed;
text{*For totally ordered groups every nonunit element is positive or its
inverse is positive.*}
lemma (in group3) OrderedGroup_ZF_1_L14:
assumes A1: "r {is total on} G" and A2: "a∈G"
shows "a=\<one> ∨ a∈G+ ∨ a¯∈G+"
proof -
{ assume A3: "a≠\<one>"
moreover from A1 A2 have "a\<lsq>\<one> ∨ \<one>\<lsq>a"
using IsTotal_def OrderedGroup_ZF_1_L1 group0.group0_2_L2
by simp;
moreover from A3 A2 have T1: "a¯ ≠ \<one>"
using OrderedGroup_ZF_1_L1 group0.group0_2_L8B
by simp
ultimately have "a¯∈G+ ∨ a∈G+"
using OrderedGroup_ZF_1_L5A OrderedGroup_ZF_1_L2A
by auto;
} thus "a=\<one> ∨ a∈G+ ∨ a¯∈G+" by auto;
qed;
text{*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∈G+" shows "a≠\<one>" "a¯∉G+"
proof -
from A1 show T1: "a≠\<one>" using PositiveSet_def by auto;
{ assume "a¯ ∈ G+"
with A1 have "a\<lsq>\<one>" "\<one>\<lsq>a"
using OrderedGroup_ZF_1_L5AA PositiveSet_def by auto;
then have "a=\<one>" by (rule group_order_antisym);
with T1 have False by simp;
} then show "a¯∉G+" by auto;
qed;
text{*If $a^{-1}$ is positive, then $a$ can not be positive or the unit.*}
lemma (in group3) OrderedGroup_ZF_1_L16:
assumes A1: "a∈G" and A2: "a¯∈G+" shows "a≠\<one>" "a∉G+"
proof -
from A2 have "a¯≠\<one>" "(a¯)¯ ∉ G+"
using OrderedGroup_ZF_1_L15 by auto;
with A1 show "a≠\<one>" "a∉G+"
using OrderedGroup_ZF_1_L1 group0.group0_2_L8C group0.group_inv_of_inv
by auto;
qed;
text{*For linearly ordered groups each element is either the unit,
positive or its inverse is positive.*}
lemma (in group3) OrdGroup_decomp:
assumes A1: "r {is total on} G" and A2: "a∈G"
shows "Exactly_1_of_3_holds (a=\<one>,a∈G+,a¯∈G+)"
proof -
from A1 A2 have "a=\<one> ∨ a∈G+ ∨ a¯∈G+"
using OrderedGroup_ZF_1_L14 by simp
moreover from A2 have "a=\<one> --> (a∉G+ ∧ a¯∉G+)"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_one
PositiveSet_def by simp;
moreover from A2 have "a∈G+ --> (a≠\<one> ∧ a¯∉G+)"
using OrderedGroup_ZF_1_L15 by simp;
moreover from A2 have "a¯∈G+ --> (a≠\<one> ∧ a∉G+)"
using OrderedGroup_ZF_1_L16 by simp;
ultimately show "Exactly_1_of_3_holds (a=\<one>,a∈G+,a¯∈G+)"
by (rule Fol1_L5);
qed;
text{*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 {is total on} G" and A2: "a∈G"
and A3: "a≠\<one>" "a∉G+"
shows "a¯ ∈ G+"
proof -
from A1 A2 have "a=\<one> ∨ a∈G+ ∨ a¯∈G+"
using OrderedGroup_ZF_1_L14 by simp;
with A3 show "a¯ ∈ G+" by auto;
qed;
text{*Elements from $G\setminus G_+$ are not greater that the unit.*}
lemma (in group3) OrderedGroup_ZF_1_L17:
assumes A1: "r {is total on} G" and A2: "a ∈ G-G+"
shows "a\<lsq>\<one>"
proof (cases "a = \<one>");
assume "a=\<one>"
with A2 show "a\<lsq>\<one>" using OrderedGroup_ZF_1_L3 by simp;
next assume "a≠\<one>"
with A1 A2 show "a\<lsq>\<one>"
using PositiveSet_def OrderedGroup_ZF_1_L8A
by auto;
qed;
text{*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 {is total on} G" and A2: "b∈G"
and A3: "Q(\<one>)" and A4: "∀a∈G+. Q(a)" and A5: "∀a∈G+. Q(a¯)"
shows "Q(b)"
proof -
from A1 A2 A3 A4 A5 have "Q(b) ∨ Q((b¯)¯)"
using OrderedGroup_ZF_1_L14 by auto;
with A2 show "Q(b)" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp;
qed;
text{*All elements greater or equal than an element of @{text "G+"}
belong to @{text "G+"}.*}
lemma (in group3) OrderedGroup_ZF_1_L19:
assumes A1: "a ∈ G+" and A2: "a\<lsq>b"
shows "b ∈ G+"
proof -
from A1 have I: "\<one>\<lsq>a" and II: "a≠\<one>"
using OrderedGroup_ZF_1_L2A by auto;
from I A2 have "\<one>\<lsq>b" by (rule Group_order_transitive);
moreover have "b≠\<one>"
proof -
{ assume "b=\<one>"
with I A2 have "\<one>\<lsq>a" "a\<lsq>\<one>"
by auto;
then have "\<one>=a" by (rule group_order_antisym)
with II have False by simp;
} then show "b≠\<one>" by auto;
qed;
ultimately show "b ∈ G+"
using OrderedGroup_ZF_1_L2A by simp;
qed;
text{*The inverse of an element of @{text "G+"} cannot be in @{text "G+"}.*}
lemma (in group3) OrderedGroup_ZF_1_L20:
assumes A1: "r {is total on} G" and A2: "a ∈ G+"
shows "a¯ ∉ G+"
proof -
from A2 have "a∈G" using PositiveSet_def
by simp;
with A1 have "Exactly_1_of_3_holds (a=\<one>,a∈G+,a¯∈G+)"
using OrdGroup_decomp by simp;
with A2 show "a¯ ∉ G+" by (rule Fol1_L7);
qed;
text{*The set of positive elements of a
nontrivial linearly ordered group is not empty.*}
lemma (in group3) OrderedGroup_ZF_1_L21:
assumes A1: "r {is total on} G" and A2: "G ≠ {\<one>}"
shows "G+ ≠ 0"
proof -
have "\<one> ∈ G" using OrderedGroup_ZF_1_L1 group0.group0_2_L2
by simp;
with A2 obtain a where "a∈G" "a≠\<one>" by auto;
with A1 have "a∈G+ ∨ a¯∈G+"
using OrderedGroup_ZF_1_L14 by auto;
then show "G+ ≠ 0" by auto;
qed;
text{*If $b\in$@{text "G+"}, then $a < a\cdot b$.
Multiplying $a$ by a positive elemnt increases $a$. *}
lemma (in group3) OrderedGroup_ZF_1_L22:
assumes A1: "a∈G" "b∈G+"
shows "a\<lsq>a·b" "a ≠ a·b" "a·b ∈ G"
proof -
from ordGroupAssum A1 have "a·\<one> \<lsq> a·b"
using OrderedGroup_ZF_1_L2A IsAnOrdGroup_def
by simp;
with A1 show "a\<lsq>a·b"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2
by simp;
then show "a·b ∈ G"
using OrderedGroup_ZF_1_L4 by simp;
{ from A1 have "a∈G" "b∈G"
using PositiveSet_def by auto;
moreover assume "a = a·b"
ultimately have "b = \<one>"
using OrderedGroup_ZF_1_L1 group0.group0_2_L7
by simp;
with A1 have False using PositiveSet_def
by simp;
} then show "a ≠ a·b" by auto;
qed;
text{*If $G$ is a nontrivial linearly ordered hroup,
then for every element of $G$ we can find one in @{text "G+"} that is
greater or equal.*}
lemma (in group3) OrderedGroup_ZF_1_L23:
assumes A1: "r {is total on} G" and A2: "G ≠ {\<one>}"
and A3: "a∈G"
shows "∃b∈G+. a\<lsq>b"
proof (cases "a∈G+")
assume A4: "a∈G+" then have "a\<lsq>a"
using PositiveSet_def OrderedGroup_ZF_1_L3
by simp;
with A4 show "∃b∈G+. a\<lsq>b" by auto;
next assume "a∉G+"
with A1 A3 have I: "a\<lsq>\<one>" using OrderedGroup_ZF_1_L17
by simp;
from A1 A2 obtain b where II: "b∈G+"
using OrderedGroup_ZF_1_L21 by auto;
then have "\<one>\<lsq>b" using PositiveSet_def by simp;
with I have "a\<lsq>b" by (rule Group_order_transitive);
with II show "∃b∈G+. a\<lsq>b" by auto;
qed;
text{*The @{text "G+"} is @{text "G+"} plus the unit.*}
lemma (in group3) OrderedGroup_ZF_1_L24: shows "G+ = G+∪{\<one>}"
using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_1_L2A OrderedGroup_ZF_1_L3A
by auto;
text{*What is $-G_+$, really?*}
lemma (in group3) OrderedGroup_ZF_1_L25: shows
"(\<sm>G+) = {a¯. a∈G+}"
"(\<sm>G+) ⊆ G"
proof -
from ordGroupAssum have I: "GroupInv(G,P) : G->G"
using IsAnOrdGroup_def group0_2_T2 by simp;
moreover have "G+ ⊆ G" using PositiveSet_def by auto;
ultimately show
"(\<sm>G+) = {a¯. a∈G+}"
"(\<sm>G+) ⊆ G"
using func_imagedef func1_1_L6 by auto;
qed;
text{*If the inverse of $a$ is in @{text "G+"}, then $a$ is in the inverse
of @{text "G+"}.*}
lemma (in group3) OrderedGroup_ZF_1_L26:
assumes A1: "a∈G" and A2: "a¯ ∈ G+"
shows "a ∈ (\<sm>G+)"
proof -
from A1 have "a¯ ∈ G" "a = (a¯)¯" using OrderedGroup_ZF_1_L1
group0.inverse_in_group group0.group_inv_of_inv
by auto;
with A2 show "a ∈ (\<sm>G+)" using OrderedGroup_ZF_1_L25
by auto;
qed;
text{*If $a$ is in the inverse of @{text "G+"},
then its inverse is in $G_+$.*}
lemma (in group3) OrderedGroup_ZF_1_L27:
assumes "a ∈ (\<sm>G+)"
shows "a¯ ∈ G+"
using prems OrderedGroup_ZF_1_L25 PositiveSet_def
OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by auto;
text{*A linearly ordered group can be decomposed into $G_+$, $\{1\}$ and
$-G$*}
lemma (in group3) OrdGroup_decomp2:
assumes A1: "r {is total on} G"
shows
"G = G+ ∪ (\<sm>G+)∪ {\<one>}"
"G+∩(\<sm>G+) = 0"
"\<one> ∉ G+∪(\<sm>G+)"
proof -
{ fix a assume A2: "a∈G"
with A1 have "a∈G+ ∨ a¯∈G+ ∨ a=\<one>"
using OrderedGroup_ZF_1_L14 by auto;
with A2 have "a∈G+ ∨ a∈(\<sm>G+) ∨ a=\<one>"
using OrderedGroup_ZF_1_L26 by auto;
then have "a ∈ (G+ ∪ (\<sm>G+)∪ {\<one>})"
by auto;
} then have "G ⊆ G+ ∪ (\<sm>G+)∪ {\<one>}"
by auto;
moreover have "G+ ∪ (\<sm>G+)∪ {\<one>} ⊆ G"
using OrderedGroup_ZF_1_L25 PositiveSet_def
OrderedGroup_ZF_1_L1 group0.group0_2_L2
by auto;
ultimately show "G = G+ ∪ (\<sm>G+)∪ {\<one>}" by auto
{ def DA: A ≡ "G+∩(\<sm>G+)"
assume "G+∩(\<sm>G+) ≠ 0"
with DA have "A≠0" by simp;
then obtain a where "a∈A" by auto;
with DA have False using OrderedGroup_ZF_1_L15 OrderedGroup_ZF_1_L27
by auto;
} then show "G+∩(\<sm>G+) = 0" by auto;
show "\<one> ∉ G+∪(\<sm>G+)"
using OrderedGroup_ZF_1_L27
OrderedGroup_ZF_1_L1 group0.group_inv_of_one
OrderedGroup_ZF_1_L2A by auto;
qed;
text{*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∈G" "b∈G" and A2: "a·b¯ ∈ G+"
shows "b\<lsq>a"
proof -
from A2 have "\<one> \<lsq> a·b¯" using OrderedGroup_ZF_1_L2
by simp
with A1 show "b\<lsq>a" using OrderedGroup_ZF_1_L5K
by simp;
qed
text{*A special case of @{text "OrderedGroup_ZF_1_L28"} when
$a\cdot b^{-1}$ is positive.*}
corollary (in group3) OrderedGroup_ZF_1_L29:
assumes A1: "a∈G" "b∈G" and A2: "a·b¯ ∈ G+"
shows "b\<lsq>a" "b≠a"
proof -
from A2 have "\<one> \<lsq> a·b¯" and I: "a·b¯ ≠ \<one>"
using OrderedGroup_ZF_1_L2A by auto
with A1 show "b\<lsq>a" using OrderedGroup_ZF_1_L5K
by simp;
from A1 I show "b≠a"
using OrderedGroup_ZF_1_L1 group0.group0_2_L6
by auto
qed;
text{*A bit stronger that @{text "OrderedGroup_ZF_1_L29"}, adds
case when two elements are equal.*}
lemma (in group3) OrderedGroup_ZF_1_L30:
assumes "a∈G" "b∈G" and "a=b ∨ b·a¯ ∈ G+"
shows "a\<lsq>b"
using prems OrderedGroup_ZF_1_L3 OrderedGroup_ZF_1_L29
by auto;
text{*A different take on decomposition: we can have $a=b$ or $a<b$
or $b<a$.*}
lemma (in group3) OrderedGroup_ZF_1_L31:
assumes A1: "r {is total on} G" and A2: "a∈G" "b∈G"
shows "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
proof -
from A2 have "a·b¯ ∈ G" using OrderedGroup_ZF_1_L1
group0.inverse_in_group group0.group_op_closed
by simp
with A1 have "a·b¯ = \<one> ∨ a·b¯ ∈ G+ ∨ (a·b¯)¯ ∈ G+"
using OrderedGroup_ZF_1_L14 by simp;
moreover
{ assume "a·b¯ = \<one>"
then have "a·b¯·b = \<one>·b" by simp;
with A2 have "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
using OrderedGroup_ZF_1_L1
group0.group0_2_L16 group0.group0_2_L2 by auto }
moreover
{ assume "a·b¯ ∈ G+"
with A2 have "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
using OrderedGroup_ZF_1_L29 by auto }
moreover
{ assume "(a·b¯)¯ ∈ G+"
with A2 have "b·a¯ ∈ G+" using OrderedGroup_ZF_1_L1
group0.group0_2_L12 by simp;
with A2 have "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
using OrderedGroup_ZF_1_L29 by auto }
ultimately show "a=b ∨ (a\<lsq>b ∧ a≠b) ∨ (b\<lsq>a ∧ b≠a)"
by auto;
qed;
(*text{*If $a<b$ then $b-a \in G_+$.*}
lemma (in group3) OrderedGroup_ZF_1_L32:
assumes A1: "a\<lsq>b" "a≠b" shows "b·a¯ ∈ G+"
proof -*)
section{*Intervals and bounded sets*}
text{*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: "∀g∈A. L\<lsq>g ∧ g\<lsq>M"
and A2: "S = RightTranslation(G,P,L¯)"
and A3: "a ∈ S``(A)"
shows "a \<lsq> M·L¯" "\<one>\<lsq>a"
proof -
from A3 have "A≠0" using func1_1_L13A by fast;
then obtain g where "g∈A" by auto
with A1 have T1: "L∈G" "M∈G" "L¯∈G"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1
group0.inverse_in_group by auto;
with A2 have "S : G->G" using OrderedGroup_ZF_1_L1 group0.group0_5_L1
by simp;
moreover from A1 have T2: "A⊆G" using OrderedGroup_ZF_1_L4 by auto;
ultimately have "S``(A) = {S`(b). b∈A}" using func_imagedef
by simp;
with A3 obtain b where T3: "b∈A" "a = S`(b)" by auto;
with A1 ordGroupAssum T1 have "b·L¯\<lsq>M·L¯" "L·L¯\<lsq>b·L¯"
using IsAnOrdGroup_def by auto;
with T3 A2 T1 T2 show "a\<lsq>M·L¯" "\<one>\<lsq>a"
using OrderedGroup_ZF_1_L1 group0.group0_5_L2 group0.group0_2_L6
by auto;
qed;
text{*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: "IsBounded(A,r)"
shows "∃B.∃g∈G+.∃T∈G->G. A = T``(B) ∧ B ⊆ Interval(r,\<one>,g)";
proof (cases "A=0");
assume A2: "A=0"
let ?B = "0"
let ?g = "\<one>"
let ?T = "ConstantFunction(G,\<one>)"
have "?g∈G+" using OrderedGroup_ZF_1_L3A by simp;
moreover have "?T : G->G"
using func1_3_L1 OrderedGroup_ZF_1_L1 group0.group0_2_L2 by simp;
moreover from A2 have "A = T``(?B)" by simp;
moreover have "?B ⊆ Interval(r,\<one>,?g)" by simp;
ultimately show
"∃B.∃g∈G+.∃T∈G->G. A = T``(B) ∧ B ⊆ Interval(r,\<one>,g)"
by auto;
next assume A3: "A≠0"
with A1 obtain L U where D1: "∀x∈A. L\<lsq>x ∧ x\<lsq>U "
using IsBounded_def IsBoundedBelow_def IsBoundedAbove_def
by auto;
with A3 have T1: "A⊆G" using OrderedGroup_ZF_1_L4 by auto;
from A3 obtain a where "a∈A" by auto;
with D1 have T2: "L\<lsq>a" "a\<lsq>U" by auto;
then have T3: "L∈G" "L¯∈ G" "U∈G"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1
group0.inverse_in_group by auto;
let ?T = "RightTranslation(G,P,L)"
let ?B = "RightTranslation(G,P,L¯)``(A)"
let ?g = "U·L¯"
have "?g∈G+"
proof -
from T2 have "L\<lsq>U" using Group_order_transitive by fast;
with ordGroupAssum T3 have "L·L¯\<lsq>?g"
using IsAnOrdGroup_def by simp;
with T3 show ?thesis using OrderedGroup_ZF_1_L1 group0.group0_2_L6
OrderedGroup_ZF_1_L2 by simp;
qed;
moreover from T3 have "?T : G->G"
using OrderedGroup_ZF_1_L1 group0.group0_5_L1
by simp;
moreover have "A = ?T``(?B)"
proof -;
from T3 T1 have "?T``(?B) = {a·L¯·L. a∈A}"
using OrderedGroup_ZF_1_L1 group0.group0_5_L6
by simp;
moreover from T3 T1 have "∀a∈A. a·L¯·L = a·(L¯·L)"
using OrderedGroup_ZF_1_L1 group0.group_oper_assoc by auto;
ultimately have "?T``(?B) = {a·(L¯·L). a∈A}" by simp;
with T3 have "?T``(?B) = {a·\<one>. a∈A}"
using OrderedGroup_ZF_1_L1 group0.group0_2_L6 by simp;
moreover from T1 have "∀a∈A. a·\<one>=a"
using OrderedGroup_ZF_1_L1 group0.group0_2_L2 by auto;
ultimately show ?thesis by simp
qed
moreover have "?B ⊆ Interval(r,\<one>,?g)"
proof
fix y assume A4: "y ∈ ?B"
def D2: S ≡ "RightTranslation(G,P,L¯)"
from D1 have T4: "∀x∈A. L\<lsq>x ∧ x\<lsq>U" by simp;
moreover from D2 have T5: "S = RightTranslation(G,P,L¯)"
by simp;
moreover from A4 D2 have T6: "y ∈ S``(A)" by simp;
ultimately have "y\<lsq>U·L¯" using OrderedGroup_ZF_2_L1
by blast;
moreover from T4 T5 T6 have "\<one>\<lsq>y" by (rule OrderedGroup_ZF_2_L1);
ultimately show "y ∈ Interval(r,\<one>,?g)" using Interval_def by auto;
qed;
ultimately show
"∃B.∃g∈G+.∃T∈G->G. A = T``(B) ∧ B ⊆ Interval(r,\<one>,g)"
by auto;
qed;
text{*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: "∀g∈G+. Interval(r,\<one>,g) ∈ Fin(G)"
and A2: "IsBounded(A,r)"
shows "A ∈ Fin(G)"
proof -
from A2 have
"∃B.∃g∈G+.∃T∈G->G. A = T``(B) ∧ B ⊆ Interval(r,\<one>,g)"
using OrderedGroup_ZF_2_L2 by simp;
then obtain B g T where D1: "g∈G+" "B ⊆ Interval(r,\<one>,g)"
and D2: "T : G->G" "A = T``(B)" by auto;
from D1 A1 have "B∈Fin(G)" using Fin_subset_lemma by blast;
with D2 show ?thesis using Finite1_L6A by simp;
qed;
text{*In linearly ordered groups finite sets are bounded.*}
theorem (in group3) ord_group_fin_bounded:
assumes "r {is total on} G" and "B∈Fin(G)"
shows "IsBounded(B,r)"
using ordGroupAssum prems IsAnOrdGroup_def IsPartOrder_def Finite_ZF_1_T1
by simp;
(*text{*If for every element of $G$ we can find a different one in $A$
that is greater, then the $A$ can not be finite. This is a property
of relations that are total, transitive and antisymmetric. *}
lemma (in group3) OrderedGroup_ZF_2_L2A:
assumes A1: "r {is total on} G"
and A2: "∀a∈G. ∃b∈A. a≠b ∧ a\<lsq>b"
shows "A ∉ Fin(G)"
using ordGroupAssum prems IsAnOrdGroup_def IsPartOrder_def
OrderedGroup_ZF_1_L1A Finite_ZF_1_1_L3 by simp;*)
text{*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 {is total on} G" and A2: "G ≠ {\<one>}"
and A3: "∀a∈G. ∃b∈A. a\<lsq>b"
shows
"∀a∈G. ∃b∈A. a≠b ∧ a\<lsq>b"
"¬IsBoundedAbove(A,r)"
"A ∉ Fin(G)"
proof -
{ fix a
from A1 A2 obtain c where "c ∈ G+"
using OrderedGroup_ZF_1_L21 by auto;
moreover assume "a∈G"
ultimately have
"a·c ∈ G" and I: "a \<ls> a·c"
using OrderedGroup_ZF_1_L22 by auto;
with A3 obtain b where II: "b∈A" and III: "a·c \<lsq> b"
by auto;
moreover from I III have "a\<ls>b" by (rule OrderedGroup_ZF_1_L4A);
ultimately have "∃b∈A. a≠b ∧ a\<lsq>b" by auto;
} thus "∀a∈G. ∃b∈A. a≠b ∧ a\<lsq>b" by simp;
with ordGroupAssum A1 show
"¬IsBoundedAbove(A,r)"
"A ∉ Fin(G)"
using IsAnOrdGroup_def IsPartOrder_def
OrderedGroup_ZF_1_L1A Order_ZF_3_L14 Finite_ZF_1_1_L3
by auto;
qed;
text{*Nontrivial linearly ordered groups are infinite. Recall
that @{text "Fin(A)"} is the collection of finite subsets of $A$.
In this lemma we show that $G\notin$ @{text "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
@{text "G+"} is infinite.*}
theorem (in group3) Linord_group_infinite:
assumes A1: "r {is total on} G" and A2: "G ≠ {\<one>}"
shows
"G+ ∉ Fin(G)"
"G ∉ Fin(G)"
proof -
from A1 A2 show I: "G+ ∉ Fin(G)"
using OrderedGroup_ZF_1_L23 OrderedGroup_ZF_2_L2A
by simp;
{ assume "G ∈ Fin(G)"
moreover have "G+ ⊆ G" using PositiveSet_def by auto;
ultimately have "G+ ∈ Fin(G)" using Fin_subset_lemma
by blast;
with I have False by simp
} then show "G ∉ Fin(G)" by auto;
qed;
text{*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 {is total on} G" and A2: "A⊆G" and
A3: "¬HasAmaximum(r,A)" and A4: "x∈A"
shows "∃y∈A. x\<ls>y"
proof -
from ordGroupAssum prems have
"antisym(r)"
"r {is total on} G"
"A⊆G" "¬HasAmaximum(r,A)" "x∈A"
using IsAnOrdGroup_def IsPartOrder_def
by auto;
then have "∃y∈A. ⟨x,y⟩ ∈ r ∧ y≠x"
using Order_ZF_4_L16 by simp;
then show "∃y∈A. x\<ls>y" by auto;
qed;
text{*In linearly ordered groups $G\setminus G_+$ is bounded above. *}
lemma (in group3) OrderedGroup_ZF_2_L3:
assumes A1: "r {is total on} G" shows "IsBoundedAbove(G-G+,r)"
proof -
from A1 have "∀a∈G-G+. a\<lsq>\<one>"
using OrderedGroup_ZF_1_L17 by simp;
then show "IsBoundedAbove(G-G+,r)"
using IsBoundedAbove_def by auto;
qed;
text{*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 {is total on} G" and A2: "A⊆G"
and A3: "A ∩ G+ ∈ Fin(G)"
shows "IsBoundedAbove(A,r)"
proof -
have "A ∩ (G-G+) ⊆ G-G+" by auto;
with A1 have "IsBoundedAbove(A ∩ (G-G+),r)"
using OrderedGroup_ZF_2_L3 Order_ZF_3_L13
by blast;
moreover from A1 A3 have "IsBoundedAbove(A ∩ G+,r)"
using ord_group_fin_bounded IsBounded_def
by simp;
moreover from A1 ordGroupAssum have
"r {is total on} G" "trans(r)" "r⊆G×G"
using IsAnOrdGroup_def IsPartOrder_def by auto;
ultimately have "IsBoundedAbove(A ∩ (G-G+) ∪ A ∩ G+,r)"
using Order_ZF_3_L3 by simp;
moreover from A2 have "A = A ∩ (G-G+) ∪ A ∩ G+"
by auto;
ultimately show "IsBoundedAbove(A,r)" by simp;
qed;
text{*If a set $-A\subseteq G$ is bounded above, then $A$ is bounded below.*}
lemma (in group3) OrderedGroup_ZF_2_L5:
assumes A1: "A⊆G" and A2: "IsBoundedAbove(\<sm>A,r)"
shows "IsBoundedBelow(A,r)"
proof (cases "A = 0")
assume "A = 0" show "IsBoundedBelow(A,r)"
using IsBoundedBelow_def by auto;
next assume A3: "A≠0"
from ordGroupAssum have I: "GroupInv(G,P) : G->G"
using IsAnOrdGroup_def group0_2_T2 by simp;
with A1 A2 A3 obtain u where D: "∀a∈(\<sm>A). a\<lsq>u"
using func1_1_L15A IsBoundedAbove_def by auto;
{ fix b assume "b∈A"
with A1 I D have "b¯ \<lsq> u" and T: "b∈G"
using func_imagedef by auto;
then have "u¯\<lsq>(b¯)¯" using OrderedGroup_ZF_1_L5
by simp;
with T have "u¯\<lsq>b"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp;
} then have "∀b∈A. ⟨u¯,b⟩ ∈ r" by simp;
then show "IsBoundedBelow(A,r)"
using Order_ZF_3_L9 by blast;
qed;
text{*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\<lsq>b" and "f:G->G"
shows "f``(Interval(r,a,b)) ≠ 0"
using ordGroupAssum prems OrderedGroup_ZF_1_L4
Order_ZF_2_L6 Order_ZF_2_L2A
IsAnOrdGroup_def IsPartOrder_def func1_1_L15A
by auto
section{*Absolute value and the triangle inequality*};
text{*The goal of this section is to prove the triangle inequality for
ordered groups.*};
text{*Absolute value maps $G$ into $G$.*}
lemma (in group3) OrderedGroup_ZF_3_L1:
"AbsoluteValue(G,P,r) : G->G"
proof -;
let ?f = "id(G+)"
let ?g = "restrict(GroupInv(G,P),G-G+)"
have "?f : G+->G+" using id_type by simp;
then have "?f : G+->G" using OrderedGroup_ZF_1_L4E
by (rule fun_weaken_type);
moreover have "?g : G-G+->G"
proof -;
from ordGroupAssum have "GroupInv(G,P) : G->G"
using IsAnOrdGroup_def group0_2_T2 by simp;
moreover have "G-G+ ⊆ G" by auto;
ultimately show ?thesis using restrict_type2 by simp;
qed;
moreover have "G+∩(G-G+) = 0" by blast;
ultimately have "?f ∪ ?g : G+∪(G-G+)->G∪G"
by (rule fun_disjoint_Un);
moreover have "G+∪(G-G+) = G" using OrderedGroup_ZF_1_L4E
by auto;
ultimately show "AbsoluteValue(G,P,r) : G->G"
using AbsoluteValue_def by simp;
qed;
text{*If $a\in G^+$, then $|a| = a$.*}
lemma (in group3) OrderedGroup_ZF_3_L2:
assumes A1: "a∈G+" shows "|a| = a"
proof -
from ordGroupAssum have "GroupInv(G,P) : G->G"
using IsAnOrdGroup_def group0_2_T2 by simp;
with A1 show ?thesis using
func1_1_L1 OrderedGroup_ZF_1_L4E fun_disjoint_apply1
AbsoluteValue_def id_conv by simp;
qed;
lemma (in group3) OrderedGroup_ZF_3_L2A:
shows "|\<one>| = \<one>" using OrderedGroup_ZF_1_L3A OrderedGroup_ZF_3_L2
by simp;
text{*If $a$ is positive, then $|a| = a$.*}
lemma (in group3) OrderedGroup_ZF_3_L2B:
assumes "a∈G+" shows "|a| = a"
using prems PositiveSet_def Nonnegative_def OrderedGroup_ZF_3_L2
by auto;
text{*If $a\in G\setminus G^+$, then $|a| = a^{-1}$.*}
lemma (in group3) OrderedGroup_ZF_3_L3:
assumes A1: "a ∈ G-G+" shows "|a| = a¯"
proof -
have "domain(id(G+)) = G+"
using id_type func1_1_L1 by auto;
with A1 show ?thesis using fun_disjoint_apply2 AbsoluteValue_def
restrict by simp;
qed;
text{*For elements that not greater than the unit, the absolute value is
the inverse.*}
lemma (in group3) OrderedGroup_ZF_3_L3A:
assumes A1: "a\<lsq>\<one>"
shows "|a| = a¯"
proof (cases "a=\<one>");
assume "a=\<one>" then show "|a| = a¯"
using OrderedGroup_ZF_3_L2A OrderedGroup_ZF_1_L1 group0.group_inv_of_one
by simp;
next assume "a≠\<one>"
with A1 show "|a| = a¯" using OrderedGroup_ZF_1_L4C OrderedGroup_ZF_3_L3
by simp;
qed;
text{*In linearly ordered groups the absolute value of any element
is in $G^+$.*}
lemma (in group3) OrderedGroup_ZF_3_L3B:
assumes A1: "r {is total on} G" and A2: "a∈G"
shows "|a| ∈ G+"
proof (cases "a∈G+");
assume "a ∈ G+" then show "|a| ∈ G+"
using OrderedGroup_ZF_3_L2 by simp;
next assume "a ∉ G+"
with A1 A2 show "|a| ∈ G+" using OrderedGroup_ZF_3_L3
OrderedGroup_ZF_1_L6 by simp;
qed;
text{*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 {is total on} G"
shows "AbsoluteValue(G,P,r) : G->G+"
proof-;
have "AbsoluteValue(G,P,r) : G->G" using OrderedGroup_ZF_3_L1
by simp;
moreover from A1 have T2:
"∀g∈G. AbsoluteValue(G,P,r)`(g) ∈ G+"
using OrderedGroup_ZF_3_L3B by simp;
ultimately show ?thesis by (rule func1_1_L1A);
qed;
text{*If the absolute value is the unit, then the elemnent is the unit.*}
lemma (in group3) OrderedGroup_ZF_3_L3D:
assumes A1: "a∈G" and A2: "|a| = \<one>"
shows "a = \<one>"
proof (cases "a∈G+")
assume "a ∈ G+"
with A2 show "a = \<one>" using OrderedGroup_ZF_3_L2 by simp;
next assume "a ∉ G+"
with A1 A2 show "a = \<one>" using
OrderedGroup_ZF_3_L3 OrderedGroup_ZF_1_L1 group0.group0_2_L8A
by auto;
qed;
text{*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 {is total on} G" and "a∈G"
shows "\<one> \<lsq> |a|"
using prems OrderedGroup_ZF_3_L3B OrderedGroup_ZF_1_L2 by simp;
text{*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\<lsq>b" and A2: "a¯\<lsq> b"
shows "|a|\<lsq> b"
proof (cases "a∈G+");
assume "a∈G+"
with A1 show "|a|\<lsq> b" using OrderedGroup_ZF_3_L2 by simp;
next assume "a∉G+"
with A1 A2 show "|a|\<lsq> b"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_3_L3 by simp;
qed;
text{*In linearly ordered groups $a\leq |a|$.*}
lemma (in group3) OrderedGroup_ZF_3_L5:
assumes A1: "r {is total on} G" and A2: "a∈G"
shows "a \<lsq> |a|"
proof (cases "a∈G+");
assume "a ∈ G+"
with A2 show "a \<lsq> |a|"
using OrderedGroup_ZF_3_L2 OrderedGroup_ZF_1_L3 by simp;
next assume "a ∉ G+"
with A1 A2 show "a \<lsq> |a|"
using OrderedGroup_ZF_3_L3B OrderedGroup_ZF_1_L4B by simp;
qed;
text{*$a^{-1}\leq |a|$ (in additive notation it would be $-a\leq |a|$.*}
lemma (in group3) OrderedGroup_ZF_3_L6:
assumes A1: "a∈G" shows "a¯ \<lsq> |a|"
proof (cases "a∈G+")
assume "a ∈ G+"
then have T1: "\<one>\<lsq>a" and T2: "|a| = a" using OrderedGroup_ZF_1_L2
OrderedGroup_ZF_3_L2 by auto;
then have "a¯\<lsq>\<one>¯" using OrderedGroup_ZF_1_L5 by simp;
then have T3: "a¯\<lsq>\<one>"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_one by simp;
from T3 T1 have "a¯\<lsq>a" by (rule Group_order_transitive);
with T2 show "a¯ \<lsq> |a|" by simp;
next assume A2: "a ∉ G+"
from A1 have "|a| ∈ G"
using OrderedGroup_ZF_3_L1 apply_funtype by auto;
with ordGroupAssum have "|a| \<lsq> |a|"
using IsAnOrdGroup_def IsPartOrder_def refl_def by simp;
with A1 A2 show "a¯ \<lsq> |a|" using OrderedGroup_ZF_3_L3 by simp;
qed;
text{*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 {is total on} G" and "a∈G" "b∈G"
shows
"a·b \<lsq>|a|·|b|"
"a·b¯ \<lsq>|a|·|b|"
"a¯·b \<lsq>|a|·|b|"
"a¯·b¯ \<lsq>|a|·|b|"
using prems OrderedGroup_ZF_3_L5 OrderedGroup_ZF_3_L6
OrderedGroup_ZF_1_L5B by auto;
text{*$|a^{-1}|\leq |a|$.*}
lemma (in group3) OrderedGroup_ZF_3_L7:
assumes "r {is total on} G" and "a∈G"
shows "|a¯|\<lsq>|a|"
using prems OrderedGroup_ZF_3_L5 OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
OrderedGroup_ZF_3_L6 OrderedGroup_ZF_3_L4 by simp;
text{*$|a^{-1}| = |a|$.*}
lemma (in group3) OrderedGroup_ZF_3_L7A:
assumes A1: "r {is total on} G" and A2: "a∈G"
shows "|a¯| = |a|"
proof -
from A2 have "a¯∈G" using OrderedGroup_ZF_1_L1 group0.inverse_in_group
by simp;
with A1 have "|(a¯)¯| \<lsq> |a¯|" using OrderedGroup_ZF_3_L7 by simp;
with A1 A2 have "|a¯| \<lsq> |a|" "|a| \<lsq> |a¯|"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv OrderedGroup_ZF_3_L7
by auto;
then show ?thesis by (rule group_order_antisym);
qed;
text{*$|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 {is total on} G" and A2: "a∈G" "b∈G"
shows "|a·b¯| = |b·a¯|"
proof -
from A1 A2 have "|(a·b¯)¯| = |a·b¯|" using
OrderedGroup_ZF_1_L1 group0.inverse_in_group group0.group0_2_L1
monoid0.group0_1_L1 OrderedGroup_ZF_3_L7A by simp;
moreover from A2 have "(a·b¯)¯ = b·a¯"
using OrderedGroup_ZF_1_L1 group0.group0_2_L12 by simp;
ultimately show ?thesis by simp;
qed;
text{*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 {is commutative on} G"
and A2: "r {is total on} G" and A3: "a∈G" "b∈G"
shows "|a·b| \<lsq> |a|·|b|"
proof -;
from A1 A2 A3 have
"a \<lsq> |a|" "b \<lsq> |b|" "a¯ \<lsq> |a|" "b¯ \<lsq> |b|"
using OrderedGroup_ZF_3_L5 OrderedGroup_ZF_3_L6 by auto;
then have "a·b \<lsq> |a|·|b|" "a¯·b¯ \<lsq> |a|·|b|"
using OrderedGroup_ZF_1_L5B by auto;
with A1 A3 show "|a·b| \<lsq> |a|·|b|"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_two IsCommutative_def
OrderedGroup_ZF_3_L4 by simp;
qed;
text{*We can multiply the sides of an inequality with absolute value.*}
lemma (in group3) OrderedGroup_ZF_3_L7C:
assumes A1: "P {is commutative on} G"
and A2: "r {is total on} G" and A3: "a∈G" "b∈G"
and A4: "|a| \<lsq> c" "|b| \<lsq> d"
shows "|a·b| \<lsq> c·d"
proof -
from A1 A2 A3 A4 have "|a·b| \<lsq> |a|·|b|"
using OrderedGroup_ZF_1_L4 OrdGroup_triangle_ineq
by simp;
moreover from A4 have "|a|·|b| \<lsq> c·d"
using OrderedGroup_ZF_1_L5B by simp
ultimately show ?thesis by (rule Group_order_transitive);
qed;
text{*A version of the @{text "OrderedGroup_ZF_3_L7C"}
but with multiplying by the inverse.*}
lemma (in group3) OrderedGroup_ZF_3_L7CA:
assumes "P {is commutative on} G"
and "r {is total on} G" and "a∈G" "b∈G"
and "|a| \<lsq> c" "|b| \<lsq> d"
shows "|a·b¯| \<lsq> c·d"
using prems OrderedGroup_ZF_1_L1 group0.inverse_in_group
OrderedGroup_ZF_3_L7A OrderedGroup_ZF_3_L7C by simp;
text{*Triangle inequality with three integers.*}
lemma (in group3) OrdGroup_triangle_ineq3:
assumes A1: "P {is commutative on} G"
and A2: "r {is total on} G" and A3: "a∈G" "b∈G" "c∈G"
shows "|a·b·c| \<lsq> |a|·|b|·|c|"
proof -
from A3 have T: "a·b ∈ G" "|c| ∈ G"
using OrderedGroup_ZF_1_L1 group0.group_op_closed
OrderedGroup_ZF_3_L1 apply_funtype by auto;
with A1 A2 A3 have "|a·b·c| \<lsq> |a·b|·|c|"
using OrdGroup_triangle_ineq by simp;
moreover from ordGroupAssum A1 A2 A3 T have
"|a·b|·|c| \<lsq> |a|·|b|·|c|"
using OrdGroup_triangle_ineq IsAnOrdGroup_def by simp;
ultimately show "|a·b·c| \<lsq> |a|·|b|·|c|"
by (rule Group_order_transitive);
qed;
text{*Some variants of the triangle inequality.*}
lemma (in group3) OrderedGroup_ZF_3_L7D:
assumes A1: "P {is commutative on} G"
and A2: "r {is total on} G" and A3: "a∈G" "b∈G"
and A4: "|a·b¯| \<lsq> c"
shows
"|a| \<lsq> c·|b|"
"|a| \<lsq> |b|·c"
"c¯·a \<lsq> b"
"a·c¯ \<lsq> b"
"a \<lsq> b·c"
proof -
from A3 A4 have
T: "a·b¯ ∈ G" "|b| ∈ G" "c∈G" "c¯ ∈ G"
using OrderedGroup_ZF_1_L1
group0.inverse_in_group group0.group0_2_L1 monoid0.group0_1_L1
OrderedGroup_ZF_3_L1 apply_funtype OrderedGroup_ZF_1_L4
by auto;
from A3 have "|a| = |a·b¯·b|"
using OrderedGroup_ZF_1_L1 group0.group0_2_L16
by simp;
with A1 A2 A3 T have "|a| \<lsq> |a·b¯|·|b|"
using OrdGroup_triangle_ineq by simp;
with T A4 show "|a| \<lsq> c·|b|" using OrderedGroup_ZF_1_L5C
by blast
with T A1 show "|a| \<lsq> |b|·c"
using IsCommutative_def by simp;
from A2 T have "a·b¯ \<lsq> |a·b¯|"
using OrderedGroup_ZF_3_L5 by simp
moreover from A4 have "|a·b¯| \<lsq> c" .
ultimately have I: "a·b¯ \<lsq> c"
by (rule Group_order_transitive)
with A3 show "c¯·a \<lsq> b"
using OrderedGroup_ZF_1_L5H by simp;
with A1 A3 T show "a·c¯ \<lsq> b"
using IsCommutative_def by simp;
from A1 A3 T I show "a \<lsq> b·c"
using OrderedGroup_ZF_1_L5H IsCommutative_def
by auto;
qed;
text{*Some more variants of the triangle inequality.*}
lemma (in group3) OrderedGroup_ZF_3_L7E:
assumes A1: "P {is commutative on} G"
and A2: "r {is total on} G" and A3: "a∈G" "b∈G"
and A4: "|a·b¯| \<lsq> c"
shows "b·c¯ \<lsq> a"
proof -
from A3 have "a·b¯ ∈ G"
using OrderedGroup_ZF_1_L1
group0.inverse_in_group group0.group_op_closed
by auto
with A2 have "|(a·b¯)¯| = |a·b¯|"
using OrderedGroup_ZF_3_L7A by simp
moreover from A3 have "(a·b¯)¯ = b·a¯"
using OrderedGroup_ZF_1_L1 group0.group0_2_L12
by simp;
ultimately have "|b·a¯| = |a·b¯|"
by simp
with A1 A2 A3 A4 show "b·c¯ \<lsq> a"
using OrderedGroup_ZF_3_L7D by simp;
qed;
text{*An application of the triangle inequality with four group
elements.*}
lemma (in group3) OrderedGroup_ZF_3_L7F:
assumes A1: "P {is commutative on} G"
and A2: "r {is total on} G" and
A3: "a∈G" "b∈G" "c∈G" "d∈G"
shows "|a·c¯| \<lsq> |a·b|·|c·d|·|b·d¯|"
proof -
from A3 have T:
"a·c¯ ∈ G" "a·b ∈ G" "c·d ∈ G" "b·d¯ ∈ G"
"(c·d)¯ ∈ G" "(b·d¯)¯ ∈ G"
using OrderedGroup_ZF_1_L1
group0.inverse_in_group group0.group_op_closed
by auto;
with A1 A2 have "|(a·b)·(c·d)¯·(b·d¯)¯| \<lsq> |a·b|·|(c·d)¯|·|(b·d¯)¯|"
using OrdGroup_triangle_ineq3 by simp;
moreover from A2 T have "|(c·d)¯| =|c·d|" and "|(b·d¯)¯| = |b·d¯|"
using OrderedGroup_ZF_3_L7A by auto;
moreover from A1 A3 have "(a·b)·(c·d)¯·(b·d¯)¯ = a·c¯"
using OrderedGroup_ZF_1_L1 group0.group0_4_L8
by simp;
ultimately show "|a·c¯| \<lsq> |a·b|·|c·d|·|b·d¯|"
by simp;
qed;
text{*$|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∈G" and A2: "|a|\<lsq>L"
shows
"L¯\<lsq>a"
proof -
from A1 have I: "a¯ \<lsq> |a|" using OrderedGroup_ZF_3_L6 by simp;
from I A2 have "a¯ \<lsq> L" by (rule Group_order_transitive);
then have "L¯\<lsq>(a¯)¯" using OrderedGroup_ZF_1_L5 by simp;
with A1 show "L¯\<lsq>a" using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp
qed;
text{*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 {is total on} G"
and A2: "a∈G" and A3: "|a|\<lsq>L"
shows
"a\<lsq>L"
"\<one>\<lsq>L"
proof -;
from A1 A2 have I: "a \<lsq> |a|" using OrderedGroup_ZF_3_L5 by simp;
from I A3 show "a\<lsq>L" by (rule Group_order_transitive);
from A1 A2 A3 have "\<one> \<lsq> |a|" "|a|\<lsq>L"
using OrderedGroup_ZF_3_L3B OrderedGroup_ZF_1_L2 by auto;
then show "\<one>\<lsq>L" by (rule Group_order_transitive);
qed;
text{*A somewhat generalized version of the above lemma.*}
lemma (in group3) OrderedGroup_ZF_3_L8B:
assumes A1: "a∈G" and A2: "|a|\<lsq>L" and A3: "\<one>\<lsq>c"
shows "(L·c)¯ \<lsq> a"
proof -
from A1 A2 A3 have "c¯·L¯ \<lsq> \<one>·a"
using OrderedGroup_ZF_3_L8 OrderedGroup_ZF_1_L5AB
OrderedGroup_ZF_1_L5B by simp;
with A1 A2 A3 show "(L·c)¯ \<lsq> a"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_1_L1
group0.group_inv_of_two group0.group0_2_L2
by simp;
qed;
text{*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\<lsq>b" and A2: "c∈G" and A3: "b\<lsq>c·a"
shows "|b·a¯| \<lsq> c"
proof -
from A1 A2 A3 have "b·a¯ \<lsq> c"
using OrderedGroup_ZF_1_L9C OrderedGroup_ZF_1_L4
by simp;
moreover have "(b·a¯)¯ \<lsq> c"
proof -
from A1 have T: "a∈G" "b∈G"
using OrderedGroup_ZF_1_L4 by auto;
with A1 have "a·b¯ \<lsq> \<one>"
using OrderedGroup_ZF_1_L9 by blast;
moreover
from A1 A3 have "a\<lsq>c·a"
by (rule Group_order_transitive);
with ordGroupAssum T have "a·a¯ \<lsq> c·a·a¯"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group
IsAnOrdGroup_def by simp;
with T A2 have "\<one> \<lsq> c"
using OrderedGroup_ZF_1_L1
group0.group0_2_L6 group0.group0_2_L16
by simp;
ultimately have "a·b¯ \<lsq> c"
by (rule Group_order_transitive);
with T show "(b·a¯)¯ \<lsq> c"
using OrderedGroup_ZF_1_L1 group0.group0_2_L12
by simp;
qed;
ultimately show "|b·a¯| \<lsq> c"
using OrderedGroup_ZF_3_L4 by simp;
qed;
text{*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 {is total on} G"
and A2: "A⊆G" and A3: "∀a∈A. |a| \<lsq> L"
shows "IsBounded(A,r)"
proof -;
from A1 A2 A3 have
"∀a∈A. a\<lsq>L" "∀a∈A. L¯\<lsq>a"
using OrderedGroup_ZF_3_L8 OrderedGroup_ZF_3_L8A by auto;
then show "IsBounded(A,r)" using
IsBoundedAbove_def IsBoundedBelow_def IsBounded_def
by auto;
qed;
text{* 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 {is total on} G"
and A2: "∀x∈X. b(x)∈G ∧ |b(x)|\<lsq>L"
shows "IsBounded({b(x). x∈X},r)"
proof -
from A2 have "{b(x). x∈X} ⊆ G" "∀a∈{b(x). x∈X}. |a| \<lsq> L"
by auto;
with A1 show ?thesis using OrderedGroup_ZF_3_L9 by blast;
qed;
text{*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 {is total on} G"
and A2: "f:X->G" and A3: "A⊆X"
and A4: "∀x∈A. |f`(x)| \<lsq> L"
shows "IsBounded(f``(A),r)"
proof -
from A2 A3 A4 have "∀x∈A. f`(x) ∈ G ∧ |f`(x)| \<lsq> L"
using apply_funtype by auto;
with A1 have "IsBounded({f`(x). x∈A},r)"
by (rule OrderedGroup_ZF_3_L9A);
with A2 A3 show "IsBounded(f``(A),r)"
using func_imagedef by simp;
qed;
text{*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 {is total on} G"
and A2: "l\<lsq>a" "a\<lsq>u"
shows
"|a| \<lsq> GreaterOf(r,|l|,|u|)"
proof (cases "a∈G+");
from A2 have T1: "|l| ∈ G" "|a| ∈ G" "|u| ∈ G"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_3_L1 apply_funtype
by auto;
assume A3: "a∈G+"
with A2 have "\<one>\<lsq>a" "a\<lsq>u"
using OrderedGroup_ZF_1_L2 by auto;
then have "\<one>\<lsq>u" by (rule Group_order_transitive)
with A2 A3 have "|a|\<lsq>|u|"
using OrderedGroup_ZF_1_L2 OrderedGroup_ZF_3_L2 by simp;
moreover from A1 T1 have "|u| \<lsq> GreaterOf(r,|l|,|u|)"
using Order_ZF_3_L2 by simp;
ultimately show "|a| \<lsq> GreaterOf(r,|l|,|u|)"
by (rule Group_order_transitive);
next assume A4: "a∉G+"
with A2 have T2:
"l∈G" "|l| ∈ G" "|a| ∈ G" "|u| ∈ G" "a ∈ G-G+"
using OrderedGroup_ZF_1_L4 OrderedGroup_ZF_3_L1 apply_funtype
by auto;
with A2 have "l ∈ G-G+" using OrderedGroup_ZF_1_L4D by fast;
with T2 A2 have "|a| \<lsq> |l|"
using OrderedGroup_ZF_3_L3 OrderedGroup_ZF_1_L5
by simp;
moreover from A1 T2 have "|l| \<lsq> GreaterOf(r,|l|,|u|)"
using Order_ZF_3_L2 by simp;
ultimately show "|a| \<lsq> GreaterOf(r,|l|,|u|)"
by (rule Group_order_transitive);
qed;
text{*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 {is total on} G"
and A2: "IsBounded(A,r)"
shows "∃L. ∀a∈A. |a| \<lsq> L"
proof (cases "A=0");
assume "A = 0" then show ?thesis by auto;
next assume A3: "A≠0"
with A2 obtain u l where "∀g∈A. l\<lsq>g ∧ g\<lsq>u"
using IsBounded_def IsBoundedAbove_def IsBoundedBelow_def
by auto;
with A1 have "∀a∈A. |a| \<lsq> GreaterOf(r,|l|,|u|)"
using OrderedGroup_ZF_3_L10 by simp;
then show ?thesis by auto;
qed;
text{* 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 A1: "r {is total on} G"
and A2: "IsBounded({b(x).x∈X},r)"
shows "∃L. ∀x∈X. |b(x)| \<lsq> L"
proof -
from A1 A2 show ?thesis using OrderedGroup_ZF_3_L10A
by blast;
qed;
text{*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 {is total on} G"
and A2: "X≠0" and A3: "{b(x). x∈X} ∈ Fin(G)"
shows "∃L∈G. ∀x∈X. |b(x)| \<lsq> L"
proof -
from A1 A3 have "∃L. ∀x∈X. |b(x)| \<lsq> L"
using ord_group_fin_bounded OrderedGroup_ZF_3_L11
by simp;
then obtain L where I: "∀x∈X. |b(x)| \<lsq> L"
using OrderedGroup_ZF_3_L11 by auto;
from A2 obtain x where "x∈X" by auto;
with I show ?thesis using OrderedGroup_ZF_1_L4
by blast;
qed;
text{*In totally oredered groups the absolute value of a
nonunit element is in @{text "G+"}.*}
lemma (in group3) OrderedGroup_ZF_3_L12:
assumes A1: "r {is total on} G"
and A2: "a∈G" and A3: "a≠\<one>"
shows "|a| ∈ G+"
proof -
from A1 A2 have "|a| ∈ G" "\<one> \<lsq> |a|"
using OrderedGroup_ZF_3_L1 apply_funtype
OrderedGroup_ZF_3_L3B OrderedGroup_ZF_1_L2
by auto;
moreover from A2 A3 have "|a| ≠ \<one>"
using OrderedGroup_ZF_3_L3D by auto;
ultimately show "|a| ∈ G+"
using PositiveSet_def by auto;
qed;
(*text{*If an nonnegative element is less or equal than another,
then so is its absolute value.*}
lemma (in group3) OrderedGroup_ZF_3_L13:
assumes A1: "\<one>\<lsq>a" and A2: "a\<lsq>b"
shows "|a| \<lsq> b"
proof -
from A1 have "|a| = a" using
OrderedGroup_ZF_1_L2 OrderedGroup_ZF_3_L2 by simp
with A2 show "|a| \<lsq> b" by simp
qed;*)
section{*Maximum absolute value of a set *}
text{* 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. *}
text{*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 ⊆ G"
and "HasAmaximum(r,A)" "HasAminimum(r,A)"
and "M = GreaterOf(r,|Minimum(r,A)|,|Maximum(r,A)|)"
shows "M ∈ AbsoluteValue(G,P,r)``(A)"
using ordGroupAssum prems IsAnOrdGroup_def IsPartOrder_def
Order_ZF_4_L3 Order_ZF_4_L4 OrderedGroup_ZF_3_L1
func_imagedef GreaterOf_def by auto;
text{*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 {is total on} G"
and A2: "HasAmaximum(r,A)" "HasAminimum(r,A)"
and A3: "a∈A"
shows "|a|\<lsq> GreaterOf(r,|Minimum(r,A)|,|Maximum(r,A)|)"
proof -;
from ordGroupAssum A2 A3 have
"Minimum(r,A)\<lsq> a" "a\<lsq> Maximum(r,A)"
using IsAnOrdGroup_def IsPartOrder_def Order_ZF_4_L3 Order_ZF_4_L4
by auto;
with A1 show ?thesis by (rule OrderedGroup_ZF_3_L10);
qed;
text{*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 {is total on} G" and "A ⊆ G"
and "HasAmaximum(r,A)" "HasAminimum(r,A)"
and "b ∈ AbsoluteValue(G,P,r)``(A)"
shows "b\<lsq> GreaterOf(r,|Minimum(r,A)|,|Maximum(r,A)|)"
using prems OrderedGroup_ZF_3_L1 func_imagedef OrderedGroup_ZF_4_L2
by auto;
text{*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 {is total on} G" and A2: "A ⊆ G"
and A3: "HasAmaximum(r,A)" "HasAminimum(r,A)"
shows "HasAmaximum(r,AbsoluteValue(G,P,r)``(A))"
proof -;
let ?M = "GreaterOf(r,|Minimum(r,A)|,|Maximum(r,A)|)"
from A2 A3 have "?M ∈ AbsoluteValue(G,P,r)``(A)"
using OrderedGroup_ZF_4_L1 by simp;
moreover from A1 A2 A3 have
"∀b ∈ AbsoluteValue(G,P,r)``(A). b \<lsq> ?M"
using OrderedGroup_ZF_4_L3 by simp;
ultimately show ?thesis using HasAmaximum_def by auto;
qed;
text{*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 {is total on} G" and A2: "A ⊆ G"
and A3: "HasAmaximum(r,A)" "HasAminimum(r,A)"
and A4: "a∈A"
shows "|a| \<lsq> Maximum(r,AbsoluteValue(G,P,r)``(A))"
proof -;
from A2 A4 have "|a| ∈ AbsoluteValue(G,P,r)``(A)"
using OrderedGroup_ZF_3_L1 func_imagedef by auto;
with ordGroupAssum A1 A2 A3 show ?thesis using
IsAnOrdGroup_def IsPartOrder_def OrderedGroup_ZF_4_L4
Order_ZF_4_L3 by simp;
qed;
section{*Alternative definitions*}
text{*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
@{text "group0"} context defined in @{text "Group_ZF"} theory. Recall that
@{text "f"} in that context denotes the group operation (unlike in the
previous sections where the group operation was denoted @{text "P"}.*}
text{*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 ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"
shows "⟨a,b⟩ ∈ r <-> a∈G ∧ b∈G ∧ a¯·b ∈ H ∪ {\<one>}"
proof;
assume "⟨a,b⟩ ∈ r"
with A1 show "a∈G ∧ b∈G ∧ a¯·b ∈ H ∪ {\<one>}"
using group0_2_L6 by auto;
next assume "a∈G ∧ b∈G ∧ a¯·b ∈ H ∪ {\<one>}"
then have "a∈G ∧ b∈G ∧ b=(a¯)¯ ∨ a∈G ∧ b∈G ∧ a¯·b ∈ H"
using inverse_in_group group0_2_L9 by auto;
with A1 show "⟨a,b⟩ ∈ r" using group_inv_of_inv
by auto;
qed;
text{*The relation defined by a positive set is antisymmetric.*}
lemma (in group0) OrderedGroup_ZF_5_L2:
assumes A1: "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"
and A2: "∀a∈G. a≠\<one> --> (a∈H) Xor (a¯∈H)"
shows "antisym(r)"
proof -
{ fix a b assume A3: "⟨a,b⟩ ∈ r" "⟨b,a⟩ ∈ r"
with A1 have T: "a∈G" "b∈G" by auto;
{ assume A4: "a≠b"
with A1 A3 have "a¯·b ∈ G" "a¯·b ∈ H" "(a¯·b)¯ ∈ H"
using inverse_in_group group0_2_L1 monoid0.group0_1_L1 group0_2_L12
by auto;
with A2 have "a¯·b = \<one>" using Xor_def by auto;
with T A4 have False using group0_2_L11 by auto;
} then have "a=b" by auto;
} then show "antisym(r)" by (rule antisymI);
qed;
text{*The relation defined by a positive set is transitive.*}
lemma (in group0) OrderedGroup_ZF_5_L3:
assumes A1: "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"
and A2: "H⊆G" "H {is closed under} f"
shows "trans(r)"
proof -
{ fix a b c assume "⟨a,b⟩ ∈ r" "⟨b,c⟩ ∈ r"
with A1 have
"a∈G ∧ b∈G ∧ a¯·b ∈ H ∪ {\<one>}"
"b∈G ∧ c∈G ∧ b¯·c ∈ H ∪ {\<one>}"
using OrderedGroup_ZF_5_L1 by auto;
with A2 have
I: "a∈G" "b∈G" "c∈G"
and "(a¯·b)·(b¯·c) ∈ H ∪ {\<one>}"
using inverse_in_group group0_2_L17 IsOpClosed_def
by auto
moreover from I have "a¯·c = (a¯·b)·(b¯·c)"
by (rule group0_2_L14A);
ultimately have "⟨a,c⟩ ∈ G×G" "a¯·c ∈ H ∪ {\<one>}"
by auto;
with A1 have "⟨a,c⟩ ∈ r" using OrderedGroup_ZF_5_L1
by auto;
} then have "∀ a b c. ⟨a, b⟩ ∈ r ∧ ⟨b, c⟩ ∈ r --> ⟨a, c⟩ ∈ r"
by blast;
then show "trans(r)" by (rule Fol1_L2);
qed;
text{*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 ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"
and A2: "f {is commutative on} G"
and A3: "⟨a,b⟩ ∈ r" and A4: "c∈G"
shows "⟨a·c,b·c⟩ ∈ r ∧ ⟨c·a,c·b⟩ ∈ r"
proof
from A1 A3 A4 have
I: "a∈G" "b∈G" "a·c ∈ G" "b·c ∈ G"
and II: "a¯·b ∈ H ∪ {\<one>}"
using OrderedGroup_ZF_5_L1 group_op_closed
by auto;
with A2 A4 have "(a·c)¯·(b·c) ∈ H ∪ {\<one>}"
using group0_4_L6D by simp;
with A1 I show "⟨a·c,b·c⟩ ∈ r" using OrderedGroup_ZF_5_L1
by auto;
with A2 A4 I show "⟨c·a,c·b⟩ ∈ r"
using IsCommutative_def by simp;
qed;
text{*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: "f {is commutative on} G"
and A2: "H⊆G" "H {is closed under} f"
and A3: "∀a∈G. a≠\<one> --> (a∈H) Xor (a¯∈H)"
and A4: "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"
shows
"IsAnOrdGroup(G,f,r)"
"r {is total on} G"
"Nonnegative(G,f,r) = PositiveSet(G,f,r) ∪ {\<one>}"
proof -
from groupAssum A2 A3 A4 have
"IsAgroup(G,f)" "r⊆G×G" "IsPartOrder(G,r)"
using refl_def OrderedGroup_ZF_5_L2 OrderedGroup_ZF_5_L3
IsPartOrder_def by auto
moreover from A1 A4 have
"∀g∈G. ∀a b. <a,b> ∈ r --> ⟨a·g,b·g⟩ ∈ r ∧ ⟨g·a,g·b⟩ ∈ r"
using OrderedGroup_ZF_5_L4 by blast;
ultimately show "IsAnOrdGroup(G,f,r)"
using IsAnOrdGroup_def by simp;
then show "Nonnegative(G,f,r) = PositiveSet(G,f,r) ∪ {\<one>}"
using group3_def group3.OrderedGroup_ZF_1_L24
by simp;
{ fix a b
assume T: "a∈G" "b∈G"
then have T1: "a¯·b ∈ G"
using inverse_in_group group_op_closed by simp;
{ assume "<a,b> ∉ r"
with A4 T have I: "a≠b" and II: "a¯·b ∉ H"
by auto;
from A3 T T1 I have "(a¯·b ∈ H) Xor ((a¯·b)¯ ∈ H)"
using group0_2_L11 by auto;
with A4 T II have "<b,a> ∈ r"
using Xor_def group0_2_L12 by simp;
} then have "<a,b> ∈ r ∨ <b,a> ∈ r" by auto;
} then show "r {is total on} G" using IsTotal_def
by simp;
qed;
text{*If the set defined as in @{text "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 "f {is commutative on} G"
and "H⊆G" and "\<one> ∉ H"
and "r = {p ∈ G×G. fst(p) = snd(p) ∨ fst(p)¯·snd(p) ∈ H}"
shows "PositiveSet(G,f,r) = H"
using prems group_inv_of_one group0_2_L2 PositiveSet_def
by auto;
text{*The next definition describes how we construct an order relation
from the prescribed set of positive elements.*}
constdefs
"OrderFromPosSet(G,P,H) ≡
{p ∈ G×G. fst(p) = snd(p) ∨ P`⟨GroupInv(G,P)`(fst(p)),snd(p)⟩ ∈ H }"
text{*The next theorem rephrases lemmas
@{text "OrderedGroup_ZF_5_L5"} and @{text "OrderedGroup_ZF_5_L6"}
using the definition of the order from the positive set
@{text "OrderFromPosSet"}. To simmarize, 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 "f {is commutative on} G"
and "H⊆G" "H {is closed under} f" "\<one> ∉ H"
and "∀a∈G. a≠\<one> --> (a∈H) Xor (a¯∈H)"
shows
"IsAnOrdGroup(G,f,OrderFromPosSet(G,f,H))"
"OrderFromPosSet(G,f,H) {is total on} G"
"PositiveSet(G,f,OrderFromPosSet(G,f,H)) = H"
"Nonnegative(G,f,OrderFromPosSet(G,f,H)) = H ∪ {\<one>}"
using prems OrderFromPosSet_def OrderedGroup_ZF_5_L5 OrderedGroup_ZF_5_L6
by auto;
section{*Odd Extensions*}
text{*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_+$.*}
text{*The next lemma is just to see the definition of the odd extension
in the notation used in the @{text "group1"} context.*}
lemma (in group3) OrderedGroup_ZF_6_L1:
shows "f° = f ∪ {⟨a, (f`(a¯))¯⟩. a ∈ \<sm>G+} ∪ {⟨\<one>,\<one>⟩}"
using OddExtension_def by simp;
text{*A technical lemma that states that from a function defined on
@{text "G+"} with values in $G$ we have $(f(a^{-1}))^{-1}\in G$.*}
lemma (in group3) OrderedGroup_ZF_6_L2:
assumes "f: G+->G" and "a∈\<sm>G+"
shows
"f`(a¯) ∈ G"
"(f`(a¯))¯ ∈ G"
using prems OrderedGroup_ZF_1_L27 apply_funtype
OrderedGroup_ZF_1_L1 group0.inverse_in_group
by auto;
text{*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 {is total on} G" and A2: "f: G+->G"
shows
"f° : G -> G"
"∀a∈G+. (f°)`(a) = f`(a)"
"∀a∈(\<sm>G+). (f°)`(a) = (f`(a¯))¯"
"(f°)`(\<one>) = \<one>"
proof -
from A1 A2 have I:
"f: G+->G"
"∀a∈\<sm>G+. (f`(a¯))¯ ∈ G"
"G+∩(\<sm>G+) = 0"
"\<one> ∉ G+∪(\<sm>G+)"
"f° = f ∪ {⟨a, (f`(a¯))¯⟩. a ∈ \<sm>G+} ∪ {⟨\<one>,\<one>⟩}"
using OrderedGroup_ZF_6_L2 OrdGroup_decomp2 OrderedGroup_ZF_6_L1
by auto;
then have "f°: G+ ∪ (\<sm>G+) ∪ {\<one>} ->G∪G∪{\<one>}"
by (rule func1_1_L11E);
moreover from A1 have
"G+ ∪ (\<sm>G+) ∪ {\<one>} = G"
"G∪G∪{\<one>} = G"
using OrdGroup_decomp2 OrderedGroup_ZF_1_L1 group0.group0_2_L2
by auto;
ultimately show "f° : G -> G" by simp;
from I show "∀a∈G+. (f°)`(a) = f`(a)"
by (rule func1_1_L11E);
from I show "∀a∈(\<sm>G+). (f°)`(a) = (f`(a¯))¯"
by (rule func1_1_L11E);
from I show "(f°)`(\<one>) = \<one>"
by (rule func1_1_L11E);
qed;
text{*Odd extensions are odd, of course.*}
lemma (in group3) oddext_is_odd:
assumes A1: "r {is total on} G" and A2: "f: G+->G"
and A3: "a∈G"
shows "(f°)`(a¯) = ((f°)`(a))¯"
proof -
from A1 A3 have "a∈G+ ∨ a ∈ (\<sm>G+) ∨ a=\<one>"
using OrdGroup_decomp2 by blast;
moreover
{ assume "a∈G+"
with A1 A2 have "a¯ ∈ \<sm>G+" and "(f°)`(a) = f`(a)"
using OrderedGroup_ZF_1_L25 odd_ext_props by auto;
with A1 A2 have
"(f°)`(a¯) = (f`((a¯)¯))¯" and "(f`(a))¯ = ((f°)`(a))¯"
using odd_ext_props by auto;
with A3 have "(f°)`(a¯) = ((f°)`(a))¯"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp }
moreover
{ assume A4: "a ∈ \<sm>G+"
with A1 A2 have "a¯ ∈ G+" and "(f°)`(a) = (f`(a¯))¯"
using OrderedGroup_ZF_1_L27 odd_ext_props
by auto;
with A1 A2 A4 have "(f°)`(a¯) = ((f°)`(a))¯"
using odd_ext_props OrderedGroup_ZF_6_L2
OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp; }
moreover
{ assume "a = \<one>"
with A1 A2 have "(f°)`(a¯) = ((f°)`(a))¯"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_one
odd_ext_props by simp;
}
ultimately show "(f°)`(a¯) = ((f°)`(a))¯"
by auto;
qed;
text{*Another way of saying that odd extensions are odd.*}
lemma (in group3) oddext_is_odd_alt:
assumes A1: "r {is total on} G" and A2: "f: G+->G"
and A3: "a∈G"
shows "((f°)`(a¯))¯ = (f°)`(a)"
proof -
from A1 A2 have
"f° : G -> G"
"∀a∈G. (f°)`(a¯) = ((f°)`(a))¯"
using odd_ext_props oddext_is_odd by auto
then have "∀a∈G. ((f°)`(a¯))¯ = (f°)`(a)"
using OrderedGroup_ZF_1_L1 group0.group0_6_L2 by simp;
with A3 show "((f°)`(a¯))¯ = (f°)`(a)" by simp;
qed;
section{*Functions with infinite limits*}
text{*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$.
*}
text{*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 {is total on} G" and A2: "G ≠ {\<one>}" and
A3: "f:G->G" and
A4: "∀a∈G.∃b∈G+.∀x. b\<lsq>x --> a \<lsq> f`(x)" and
A5: "A⊆G" and
A6: "IsBoundedAbove(f``(A),r)"
shows "IsBoundedAbove(A,r)"
proof -
{ assume "¬IsBoundedAbove(A,r)"
then have I: "∀u. ∃x∈A. ¬(x\<lsq>u)"
using IsBoundedAbove_def by auto;
have "∀a∈G. ∃y∈f``(A). a\<lsq>y"
proof -
{ fix a assume "a∈G"
with A4 obtain b where
II: "b∈G+" and III: "∀x. b\<lsq>x --> a \<lsq> f`(x)"
by auto;
from I obtain x where IV: "x∈A" and "¬(x\<lsq>b)"
by auto;
with A1 A5 II have
"r {is total on} G"
"x∈G" "b∈G" "¬(x\<lsq>b)"
using PositiveSet_def by auto;
with III have "a \<lsq> f`(x)"
using OrderedGroup_ZF_1_L8 by blast;
with A3 A5 IV have "∃y∈f``(A). a\<lsq>y"
using func_imagedef by auto;
} thus ?thesis by simp
qed
with A1 A2 A6 have False using OrderedGroup_ZF_2_L2A
by simp;
} thus ?thesis by auto;
qed;
text{*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 {is total on} G" and A2: "G ≠ {\<one>}" and
A3: "X≠0" and A4: "f:G->G" and
A5: "∀a∈G.∃b∈G+.∀y. b\<lsq>y --> a \<lsq> f`(y)" and
A6: "∀x∈X. b(x) ∈ G ∧ f`(b(x)) \<lsq> U"
shows "∃u.∀x∈X. b(x) \<lsq> u"
proof -
let ?A = "{b(x). x∈X}"
from A6 have I: "?A⊆G" by auto;
moreover note prems
moreover have "IsBoundedAbove(f``(?A),r)"
proof -
from A4 A6 I have "∀z∈f``(?A). ⟨z,U⟩ ∈ r"
using func_imagedef by simp;
then show "IsBoundedAbove(f``(?A),r)"
by (rule Order_ZF_3_L10);
qed;
ultimately have "IsBoundedAbove(?A,r)" using OrderedGroup_ZF_7_L1
by simp;
with A3 have "∃u.∀y∈?A. y \<lsq> u"
using IsBoundedAbove_def by simp;
then show "∃u.∀x∈X. b(x) \<lsq> u" by auto;
qed;
text{*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 @{text "OrderedGroup_ZF_7_L2"}.*}
lemma (in group3) OrderedGroup_ZF_7_L3:
assumes A1: "r {is total on} G" and A2: "G ≠ {\<one>}" and
A3: "X≠0" and A4: "f:G->G" and
A5: "∀a∈G.∃b∈G+.∀y. b\<lsq>y --> f`(y¯) \<lsq> a" and
A6: "∀x∈X. b(x) ∈ G ∧ L \<lsq> f`(b(x))"
shows "∃l.∀x∈X. l \<lsq> b(x)"
proof -
let ?g = "GroupInv(G,P) O f O GroupInv(G,P)"
from ordGroupAssum have I: "GroupInv(G,P) : G->G"
using IsAnOrdGroup_def group0_2_T2 by simp;
with A4 have II: "∀x∈G. ?g`(x) = (f`(x¯))¯"
using func1_1_L18 by simp;
note A1 A2 A3
moreover from A4 I have "?g : G->G"
using comp_fun by blast;
moreover have "∀a∈G.∃b∈G+.∀y. b\<lsq>y --> a \<lsq> ?g`(y)"
proof -
{ fix a assume A7: "a∈G"
then have "a¯ ∈ G"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group
by simp;
with A5 obtain b where
III: "b∈G+" and "∀y. b\<lsq>y --> f`(y¯) \<lsq> a¯"
by auto;
with II A7 have "∀y. b\<lsq>y --> a \<lsq> ?g`(y)"
using OrderedGroup_ZF_1_L5AD OrderedGroup_ZF_1_L4
by simp;
with III have "∃b∈G+.∀y. b\<lsq>y --> a \<lsq> ?g`(y)"
by auto;
} then show "∀a∈G.∃b∈G+.∀y. b\<lsq>y --> a \<lsq> ?g`(y)"
by simp;
qed;
moreover have "∀x∈X. b(x)¯ ∈ G ∧ ?g`(b(x)¯) \<lsq> L¯"
proof-
{ fix x assume "x∈X"
with A6 have
T: "b(x) ∈ G" "b(x)¯ ∈ G" and "L \<lsq> f`(b(x))"
using OrderedGroup_ZF_1_L1 group0.inverse_in_group
by auto;
then have "(f`(b(x)))¯ \<lsq> L¯"
using OrderedGroup_ZF_1_L5 by simp;
moreover from II T have "(f`(b(x)))¯ = ?g`(b(x)¯)"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by simp;
ultimately have "?g`(b(x)¯) \<lsq> L¯" by simp;
with T have "b(x)¯ ∈ G ∧ ?g`(b(x)¯) \<lsq> L¯"
by simp;
} then show "∀x∈X. b(x)¯ ∈ G ∧ ?g`(b(x)¯) \<lsq> L¯"
by simp;
qed;
ultimately have "∃u.∀x∈X. (b(x))¯ \<lsq> u"
by (rule OrderedGroup_ZF_7_L2);
then have "∃u.∀x∈X. u¯ \<lsq> (b(x)¯)¯"
using OrderedGroup_ZF_1_L5 by auto;
with A6 show "∃l.∀x∈X. l \<lsq> b(x)"
using OrderedGroup_ZF_1_L1 group0.group_inv_of_inv
by auto;
qed;
text{*The next lemma combines @{text "OrderedGroup_ZF_7_L2"} and
@{text "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 {is total on} G" and A2: "G ≠ {\<one>}" and
A3: "X≠0" and A4: "f:G->G" and
A5: "∀a∈G.∃b∈G+.∀y. b\<lsq>y --> a \<lsq> f`(y)" and
A6: "∀a∈G.∃b∈G+.∀y. b\<lsq>y --> f`(y¯) \<lsq> a" and
A7: "∀x∈X. b(x) ∈ G ∧ L \<lsq> f`(b(x)) ∧ f`(b(x)) \<lsq> U"
shows "∃M.∀x∈X. |b(x)| \<lsq> M"
proof -
from A7 have
I: "∀x∈X. b(x) ∈ G ∧ f`(b(x)) \<lsq> U" and
II: "∀x∈X. b(x) ∈ G ∧ L \<lsq> f`(b(x))"
by auto;
from A1 A2 A3 A4 A5 I have "∃u.∀x∈X. b(x) \<lsq> u"
by (rule OrderedGroup_ZF_7_L2);
moreover from A1 A2 A3 A4 A6 II have "∃l.∀x∈X. l \<lsq> b(x)"
by (rule OrderedGroup_ZF_7_L3);
ultimately have "∃u l. ∀x∈X. l\<lsq>b(x) ∧ b(x) \<lsq> u"
by auto;
with A1 have "∃u l.∀x∈X. |b(x)| \<lsq> GreaterOf(r,|l|,|u|)"
using OrderedGroup_ZF_3_L10 by blast;
then show "∃M.∀x∈X. |b(x)| \<lsq> M"
by auto;
qed;
end
lemma OrderedGroup_ZF_1_L1:
group3(G, P, r) ==> group0(G, P)
lemma OrderedGroup_ZF_1_L1A:
group3(G, P, r) ==> G ≠ 0
lemma OrderedGroup_ZF_1_L2:
group3(G, P, r) ==> g ∈ Nonnegative(G, P, r) <-> ⟨TheNeutralElement(G, P), g⟩ ∈ r
lemma OrderedGroup_ZF_1_L2A:
group3(G, P, r) ==> g ∈ PositiveSet(G, P, r) <-> ⟨TheNeutralElement(G, P), g⟩ ∈ r ∧ g ≠ TheNeutralElement(G, P)
lemma OrderedGroup_ZF_1_L2B:
[| group3(G, P, r); r {is total on} G; a ∈ G - Nonnegative(G, P, r) |] ==> ⟨a, TheNeutralElement(G, P)⟩ ∈ r
lemma OrderedGroup_ZF_1_L3:
[| group3(G, P, r); g ∈ G |] ==> ⟨g, g⟩ ∈ r
lemma OrderedGroup_ZF_1_L3A:
group3(G, P, r) ==> TheNeutralElement(G, P) ∈ Nonnegative(G, P, r)
lemma OrderedGroup_ZF_1_L4:
[| group3(G, P, r); ⟨a, b⟩ ∈ r |] ==> a ∈ G
[| group3(G, P, r); ⟨a, b⟩ ∈ r |] ==> b ∈ G
lemma Group_order_transitive:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; ⟨b, c⟩ ∈ r |] ==> ⟨a, c⟩ ∈ r
lemma group_order_antisym:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; ⟨b, a⟩ ∈ r |] ==> a = b
lemma OrderedGroup_ZF_1_L4A:
[| group3(G, P, r); ⟨a, b⟩ ∈ r ∧ a ≠ b; ⟨b, c⟩ ∈ r |] ==> ⟨a, c⟩ ∈ r ∧ a ≠ c
lemma group_strict_ord_transit:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; ⟨b, c⟩ ∈ r ∧ b ≠ c |] ==> ⟨a, c⟩ ∈ r ∧ a ≠ c
lemma group_strict_ord_transl_inv:
[| group3(G, P, r); ⟨a, b⟩ ∈ r ∧ a ≠ b; c ∈ G |] ==> ⟨P ` ⟨a, c⟩, P ` ⟨b, c⟩⟩ ∈ r ∧ P ` ⟨a, c⟩ ≠ P ` ⟨b, c⟩
[| group3(G, P, r); ⟨a, b⟩ ∈ r ∧ a ≠ b; c ∈ G |] ==> ⟨P ` ⟨c, a⟩, P ` ⟨c, b⟩⟩ ∈ r ∧ P ` ⟨c, a⟩ ≠ P ` ⟨c, b⟩
lemma group_ord_total_is_lin:
[| group3(G, P, r); r {is total on} G |] ==> IsLinOrder(G, r)
lemma OrderedGroup_ZF_1_L4B:
[| group3(G, P, r); r {is total on} G; a ∈ Nonnegative(G, P, r); b ∈ G - Nonnegative(G, P, r) |] ==> ⟨b, a⟩ ∈ r
lemma OrderedGroup_ZF_1_L4C:
[| group3(G, P, r); ⟨a, TheNeutralElement(G, P)⟩ ∈ r; a ≠ TheNeutralElement(G, P) |] ==> a ∈ G - Nonnegative(G, P, r)
lemma OrderedGroup_ZF_1_L4D:
[| group3(G, P, r); a ∈ G - Nonnegative(G, P, r); ⟨b, a⟩ ∈ r |] ==> b ∈ G - Nonnegative(G, P, r)
lemma OrderedGroup_ZF_1_L4E:
group3(G, P, r) ==> Nonnegative(G, P, r) ⊆ G
lemma OrderedGroup_ZF_1_L5:
[| group3(G, P, r); ⟨a, b⟩ ∈ r |] ==> ⟨GroupInv(G, P) ` b, GroupInv(G, P) ` a⟩ ∈ r
lemma OrderedGroup_ZF_1_L5A:
[| group3(G, P, r); ⟨a, TheNeutralElement(G, P)⟩ ∈ r |] ==> ⟨TheNeutralElement(G, P), GroupInv(G, P) ` a⟩ ∈ r
lemma OrderedGroup_ZF_1_L5AA:
[| group3(G, P, r); a ∈ G; ⟨TheNeutralElement(G, P), GroupInv(G, P) ` a⟩ ∈ r |] ==> ⟨a, TheNeutralElement(G, P)⟩ ∈ r
lemma OrderedGroup_ZF_1_L5AB(1):
[| group3(G, P, r); ⟨TheNeutralElement(G, P), a⟩ ∈ r |] ==> ⟨GroupInv(G, P) ` a, TheNeutralElement(G, P)⟩ ∈ r
and OrderedGroup_ZF_1_L5AB(2):
[| group3(G, P, r); ⟨TheNeutralElement(G, P), a⟩ ∈ r |] ==> ¬ (⟨a, TheNeutralElement(G, P)⟩ ∈ r ∧ a ≠ TheNeutralElement(G, P))
lemma OrderedGroup_ZF_1_L5AC:
[| group3(G, P, r); ⟨TheNeutralElement(G, P), a⟩ ∈ r; ⟨TheNeutralElement(G, P), b⟩ ∈ r |] ==> ⟨GroupInv(G, P) ` a, b⟩ ∈ r
lemma OrderedGroup_ZF_1_L5AD:
[| group3(G, P, r); b ∈ G; ⟨a, GroupInv(G, P) ` b⟩ ∈ r |] ==> ⟨b, GroupInv(G, P) ` a⟩ ∈ r
lemma OrderedGroup_ZF_1_L5AE:
[| group3(G, P, r); a ∈ G; b ∈ G; c ∈ G; ⟨P ` ⟨a, b⟩, P ` ⟨a, c⟩⟩ ∈ r |] ==> ⟨b, c⟩ ∈ r
lemma OrderedGroup_ZF_1_L5AF:
[| group3(G, P, r); a ∈ G; b ∈ G; c ∈ G; ⟨P ` ⟨a, GroupInv(G, P) ` b⟩, P ` ⟨a, GroupInv(G, P) ` c⟩⟩ ∈ r |] ==> ⟨c, b⟩ ∈ r
lemma OrderedGroup_ZF_1_L5AG:
[| group3(G, P, r); a ∈ G; ⟨GroupInv(G, P) ` a, b⟩ ∈ r |] ==> ⟨GroupInv(G, P) ` b, a⟩ ∈ r
lemma OrderedGroup_ZF_1_L5B:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; ⟨c, d⟩ ∈ r |] ==> ⟨P ` ⟨a, c⟩, P ` ⟨b, d⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L5C:
[| group3(G, P, r); c ∈ G; ⟨a, P ` ⟨b, c⟩⟩ ∈ r; ⟨b, b1⟩ ∈ r |] ==> ⟨a, P ` ⟨b1, c⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L5D:
[| group3(G, P, r); b ∈ G; ⟨a, P ` ⟨b, c⟩⟩ ∈ r; ⟨c, b1⟩ ∈ r |] ==> ⟨a, P ` ⟨b, b1⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L5E:
[| group3(G, P, r); ⟨a, P ` ⟨b, c⟩⟩ ∈ r; ⟨b, b1⟩ ∈ r; ⟨c, c1⟩ ∈ r |] ==> ⟨a, P ` ⟨b1, c1⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L5F:
[| group3(G, P, r); ⟨TheNeutralElement(G, P), a⟩ ∈ r; b ∈ G |] ==> ⟨b, P ` ⟨a, b⟩⟩ ∈ r
[| group3(G, P, r); ⟨TheNeutralElement(G, P), a⟩ ∈ r; b ∈ G |] ==> ⟨b, P ` ⟨b, a⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L5G:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; ⟨TheNeutralElement(G, P), c⟩ ∈ r |] ==> ⟨a, P ` ⟨b, c⟩⟩ ∈ r
[| group3(G, P, r); ⟨a, b⟩ ∈ r; ⟨TheNeutralElement(G, P), c⟩ ∈ r |] ==> ⟨a, P ` ⟨c, b⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L5H:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨P ` ⟨a, GroupInv(G, P) ` b⟩, c⟩ ∈ r |] ==> ⟨a, P ` ⟨c, b⟩⟩ ∈ r
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨P ` ⟨a, GroupInv(G, P) ` b⟩, c⟩ ∈ r |] ==> ⟨P ` ⟨GroupInv(G, P) ` c, a⟩, b⟩ ∈ r
lemma OrderedGroup_ZF_1_L5I:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; ⟨c, d⟩ ∈ r |] ==> ⟨P ` ⟨a, GroupInv(G, P) ` d⟩, P ` ⟨b, GroupInv(G, P) ` c⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L5J:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨c, P ` ⟨a, GroupInv(G, P) ` b⟩⟩ ∈ r |] ==> ⟨P ` ⟨c, b⟩, a⟩ ∈ r
lemma OrderedGroup_ZF_1_L5JA:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨c, P ` ⟨GroupInv(G, P) ` a, b⟩⟩ ∈ r |] ==> ⟨P ` ⟨a, c⟩, b⟩ ∈ r
corollary OrderedGroup_ZF_1_L5K:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨TheNeutralElement(G, P), P ` ⟨a, GroupInv(G, P) ` b⟩⟩ ∈ r |] ==> ⟨b, a⟩ ∈ r
corollary OrderedGroup_ZF_1_L5KA:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨TheNeutralElement(G, P), P ` ⟨GroupInv(G, P) ` a, b⟩⟩ ∈ r |] ==> ⟨a, b⟩ ∈ r
lemma OrderedGroup_ZF_1_L6:
[| group3(G, P, r); r {is total on} G; a ∈ G - Nonnegative(G, P, r) |] ==> ⟨a, TheNeutralElement(G, P)⟩ ∈ r
[| group3(G, P, r); r {is total on} G; a ∈ G - Nonnegative(G, P, r) |] ==> GroupInv(G, P) ` a ∈ Nonnegative(G, P, r)
[| group3(G, P, r); r {is total on} G; a ∈ G - Nonnegative(G, P, r) |] ==> restrict(GroupInv(G, P), G - Nonnegative(G, P, r)) ` a ∈ Nonnegative(G, P, r)
lemma OrderedGroup_ZF_1_L7:
[| group3(G, P, r); r {is total on} G; ∀a∈Nonnegative(G, P, r). ∀b∈Nonnegative(G, P, r). Q(a, b); ∀a∈G. ∀b∈G. Q(a, b) --> Q(GroupInv(G, P) ` a, b); ∀a∈G. ∀b∈G. Q(a, b) --> Q(a, GroupInv(G, P) ` b); a ∈ G; b ∈ G |] ==> Q(a, b)
lemma OrdGroup_6cases:
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G |] ==> ⟨TheNeutralElement(G, P), a⟩ ∈ r ∧ ⟨TheNeutralElement(G, P), b⟩ ∈ r ∨ ⟨a, TheNeutralElement(G, P)⟩ ∈ r ∧ ⟨b, TheNeutralElement(G, P)⟩ ∈ r ∨ ⟨a, TheNeutralElement(G, P)⟩ ∈ r ∧ ⟨TheNeutralElement(G, P), b⟩ ∈ r ∧ ⟨TheNeutralElement(G, P), P ` ⟨a, b⟩⟩ ∈ r ∨ ⟨a, TheNeutralElement(G, P)⟩ ∈ r ∧ ⟨TheNeutralElement(G, P), b⟩ ∈ r ∧ ⟨P ` ⟨a, b⟩, TheNeutralElement(G, P)⟩ ∈ r ∨ ⟨TheNeutralElement(G, P), a⟩ ∈ r ∧ ⟨b, TheNeutralElement(G, P)⟩ ∈ r ∧ ⟨TheNeutralElement(G, P), P ` ⟨a, b⟩⟩ ∈ r ∨ ⟨TheNeutralElement(G, P), a⟩ ∈ r ∧ ⟨b, TheNeutralElement(G, P)⟩ ∈ r ∧ ⟨P ` ⟨a, b⟩, TheNeutralElement(G, P)⟩ ∈ r
lemma OrderedGroup_ZF_1_L8:
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G; ⟨a, b⟩ ∉ r |] ==> ⟨b, a⟩ ∈ r
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G; ⟨a, b⟩ ∉ r |] ==> ⟨GroupInv(G, P) ` a, GroupInv(G, P) ` b⟩ ∈ r
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G; ⟨a, b⟩ ∉ r |] ==> a ≠ b
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G; ⟨a, b⟩ ∉ r |] ==> ⟨b, a⟩ ∈ r ∧ b ≠ a
lemma OrderedGroup_ZF_1_L8AA:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; a ≠ b |] ==> ⟨b, a⟩ ∉ r
corollary OrderedGroup_ZF_1_L8A:
[| group3(G, P, r); r {is total on} G; a ∈ G; ⟨TheNeutralElement(G, P), a⟩ ∉ r |] ==> ⟨TheNeutralElement(G, P), GroupInv(G, P) ` a⟩ ∈ r
[| group3(G, P, r); r {is total on} G; a ∈ G; ⟨TheNeutralElement(G, P), a⟩ ∉ r |] ==> TheNeutralElement(G, P) ≠ a
[| group3(G, P, r); r {is total on} G; a ∈ G; ⟨TheNeutralElement(G, P), a⟩ ∉ r |] ==> ⟨a, TheNeutralElement(G, P)⟩ ∈ r
lemma OrderedGroup_ZF_1_L8B:
[| group3(G, P, r); ⟨a, TheNeutralElement(G, P)⟩ ∈ r; a ≠ TheNeutralElement(G, P) |] ==> ⟨TheNeutralElement(G, P), a⟩ ∉ r
lemma OrderedGroup_ZF_1_L9:
[| group3(G, P, r); a ∈ G; b ∈ G |] ==> ⟨a, b⟩ ∈ r <-> ⟨P ` ⟨a, GroupInv(G, P) ` b⟩, TheNeutralElement(G, P)⟩ ∈ r
lemma OrderedGroup_ZF_1_L9A:
[| group3(G, P, r); a ∈ G; b ∈ G; c ∈ G |] ==> ⟨P ` ⟨a, b⟩, c⟩ ∈ r <-> ⟨a, P ` ⟨c, GroupInv(G, P) ` b⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L9B:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨P ` ⟨a, GroupInv(G, P) ` b⟩, c⟩ ∈ r |] ==> ⟨a, P ` ⟨c, b⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L9C:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨c, P ` ⟨a, b⟩⟩ ∈ r |] ==> ⟨P ` ⟨c, GroupInv(G, P) ` b⟩, a⟩ ∈ r
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨c, P ` ⟨a, b⟩⟩ ∈ r |] ==> ⟨P ` ⟨GroupInv(G, P) ` a, c⟩, b⟩ ∈ r
lemma OrderedGroup_ZF_1_L9D:
[| group3(G, P, r); ⟨a, b⟩ ∈ r |] ==> ⟨TheNeutralElement(G, P), P ` ⟨b, GroupInv(G, P) ` a⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L9E:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; a ≠ b |] ==> ⟨TheNeutralElement(G, P), P ` ⟨b, GroupInv(G, P) ` a⟩⟩ ∈ r
[| group3(G, P, r); ⟨a, b⟩ ∈ r; a ≠ b |] ==> TheNeutralElement(G, P) ≠ P ` ⟨b, GroupInv(G, P) ` a⟩
[| group3(G, P, r); ⟨a, b⟩ ∈ r; a ≠ b |] ==> P ` ⟨b, GroupInv(G, P) ` a⟩ ∈ PositiveSet(G, P, r)
lemma OrderedGroup_ZF_1_L9F:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨TheNeutralElement(G, P), P ` ⟨b, GroupInv(G, P) ` a⟩⟩ ∈ r |] ==> ⟨a, b⟩ ∈ r
lemma OrderedGroup_ZF_1_L10:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨c, d⟩ ∈ r |] ==> ⟨P ` ⟨P ` ⟨a, c⟩, b⟩, P ` ⟨P ` ⟨a, d⟩, b⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L11:
[| group3(G, P, r); ⟨TheNeutralElement(G, P), a⟩ ∈ r; ⟨TheNeutralElement(G, P), b⟩ ∈ r; TheNeutralElement(G, P) ≠ a; TheNeutralElement(G, P) ≠ b |] ==> TheNeutralElement(G, P) ≠ P ` ⟨a, b⟩
lemma OrderedGroup_ZF_1_L12:
[| group3(G, P, r); ⟨TheNeutralElement(G, P), a⟩ ∈ r; ⟨TheNeutralElement(G, P), b⟩ ∈ r |] ==> ⟨TheNeutralElement(G, P), P ` ⟨a, b⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L12A:
[| group3(G, P, r); ⟨a, b⟩ ∈ r |] ==> ⟨TheNeutralElement(G, P), P ` ⟨b, GroupInv(G, P) ` a⟩⟩ ∈ r
lemma OrderedGroup_ZF_1_L12B:
[| group3(G, P, r); a ∈ G; b ∈ G; ⟨P ` ⟨a, GroupInv(G, P) ` b⟩, c⟩ ∈ r ∧ P ` ⟨a, GroupInv(G, P) ` b⟩ ≠ c |] ==> ⟨a, P ` ⟨c, b⟩⟩ ∈ r ∧ a ≠ P ` ⟨c, b⟩
lemma OrderedGroup_ZF_1_L12C:
[| group3(G, P, r); ⟨a, b⟩ ∈ r ∧ a ≠ b; ⟨c, d⟩ ∈ r |] ==> ⟨P ` ⟨a, c⟩, P ` ⟨b, d⟩⟩ ∈ r ∧ P ` ⟨a, c⟩ ≠ P ` ⟨b, d⟩
lemma OrderedGroup_ZF_1_L12D:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; ⟨c, d⟩ ∈ r ∧ c ≠ d |] ==> ⟨P ` ⟨a, c⟩, P ` ⟨b, d⟩⟩ ∈ r ∧ P ` ⟨a, c⟩ ≠ P ` ⟨b, d⟩
lemma OrderedGroup_ZF_1_L13:
group3(G, P, r) ==> PositiveSet(G, P, r) {is closed under} P
lemma OrderedGroup_ZF_1_L14:
[| group3(G, P, r); r {is total on} G; a ∈ G |] ==> a = TheNeutralElement(G, P) ∨ a ∈ PositiveSet(G, P, r) ∨ GroupInv(G, P) ` a ∈ PositiveSet(G, P, r)
lemma OrderedGroup_ZF_1_L15:
[| group3(G, P, r); a ∈ PositiveSet(G, P, r) |] ==> a ≠ TheNeutralElement(G, P)
[| group3(G, P, r); a ∈ PositiveSet(G, P, r) |] ==> GroupInv(G, P) ` a ∉ PositiveSet(G, P, r)
lemma OrderedGroup_ZF_1_L16:
[| group3(G, P, r); a ∈ G; GroupInv(G, P) ` a ∈ PositiveSet(G, P, r) |] ==> a ≠ TheNeutralElement(G, P)
[| group3(G, P, r); a ∈ G; GroupInv(G, P) ` a ∈ PositiveSet(G, P, r) |] ==> a ∉ PositiveSet(G, P, r)
lemma OrdGroup_decomp:
[| group3(G, P, r); r {is total on} G; a ∈ G |] ==> Exactly_1_of_3_holds (a = TheNeutralElement(G, P), a ∈ PositiveSet(G, P, r), GroupInv(G, P) ` a ∈ PositiveSet(G, P, r))
lemma OrdGroup_cases:
[| group3(G, P, r); r {is total on} G; a ∈ G; a ≠ TheNeutralElement(G, P); a ∉ PositiveSet(G, P, r) |] ==> GroupInv(G, P) ` a ∈ PositiveSet(G, P, r)
lemma OrderedGroup_ZF_1_L17:
[| group3(G, P, r); r {is total on} G; a ∈ G - PositiveSet(G, P, r) |] ==> ⟨a, TheNeutralElement(G, P)⟩ ∈ r
lemma OrderedGroup_ZF_1_L18:
[| group3(G, P, r); r {is total on} G; b ∈ G; Q(TheNeutralElement(G, P)); ∀a∈PositiveSet(G, P, r). Q(a); ∀a∈PositiveSet(G, P, r). Q(GroupInv(G, P) ` a) |] ==> Q(b)
lemma OrderedGroup_ZF_1_L19:
[| group3(G, P, r); a ∈ PositiveSet(G, P, r); ⟨a, b⟩ ∈ r |] ==> b ∈ PositiveSet(G, P, r)
lemma OrderedGroup_ZF_1_L20:
[| group3(G, P, r); r {is total on} G; a ∈ PositiveSet(G, P, r) |] ==> GroupInv(G, P) ` a ∉ PositiveSet(G, P, r)
lemma OrderedGroup_ZF_1_L21:
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)} |] ==> PositiveSet(G, P, r) ≠ 0
lemma OrderedGroup_ZF_1_L22:
[| group3(G, P, r); a ∈ G; b ∈ PositiveSet(G, P, r) |] ==> ⟨a, P ` ⟨a, b⟩⟩ ∈ r
[| group3(G, P, r); a ∈ G; b ∈ PositiveSet(G, P, r) |] ==> a ≠ P ` ⟨a, b⟩
[| group3(G, P, r); a ∈ G; b ∈ PositiveSet(G, P, r) |] ==> P ` ⟨a, b⟩ ∈ G
lemma OrderedGroup_ZF_1_L23:
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)}; a ∈ G |] ==> ∃b∈PositiveSet(G, P, r). ⟨a, b⟩ ∈ r
lemma OrderedGroup_ZF_1_L24:
group3(G, P, r) ==> Nonnegative(G, P, r) = PositiveSet(G, P, r) ∪ {TheNeutralElement(G, P)}
lemma OrderedGroup_ZF_1_L25:
group3(G, P, r) ==> GroupInv(G, P) `` PositiveSet(G, P, r) = {GroupInv(G, P) ` a . a ∈ PositiveSet(G, P, r)}
group3(G, P, r) ==> GroupInv(G, P) `` PositiveSet(G, P, r) ⊆ G
lemma OrderedGroup_ZF_1_L26:
[| group3(G, P, r); a ∈ G; GroupInv(G, P) ` a ∈ PositiveSet(G, P, r) |] ==> a ∈ GroupInv(G, P) `` PositiveSet(G, P, r)
lemma OrderedGroup_ZF_1_L27:
[| group3(G, P, r); a ∈ GroupInv(G, P) `` PositiveSet(G, P, r) |] ==> GroupInv(G, P) ` a ∈ PositiveSet(G, P, r)
lemma OrdGroup_decomp2:
[| group3(G, P, r); r {is total on} G |] ==> G = PositiveSet(G, P, r) ∪ GroupInv(G, P) `` PositiveSet(G, P, r) ∪ {TheNeutralElement(G, P)}
[| group3(G, P, r); r {is total on} G |] ==> PositiveSet(G, P, r) ∩ GroupInv(G, P) `` PositiveSet(G, P, r) = 0
[| group3(G, P, r); r {is total on} G |] ==> TheNeutralElement(G, P) ∉ PositiveSet(G, P, r) ∪ GroupInv(G, P) `` PositiveSet(G, P, r)
lemma OrderedGroup_ZF_1_L28:
[| group3(G, P, r); a ∈ G; b ∈ G; P ` ⟨a, GroupInv(G, P) ` b⟩ ∈ Nonnegative(G, P, r) |] ==> ⟨b, a⟩ ∈ r
corollary OrderedGroup_ZF_1_L29:
[| group3(G, P, r); a ∈ G; b ∈ G; P ` ⟨a, GroupInv(G, P) ` b⟩ ∈ PositiveSet(G, P, r) |] ==> ⟨b, a⟩ ∈ r
[| group3(G, P, r); a ∈ G; b ∈ G; P ` ⟨a, GroupInv(G, P) ` b⟩ ∈ PositiveSet(G, P, r) |] ==> b ≠ a
lemma OrderedGroup_ZF_1_L30:
[| group3(G, P, r); a ∈ G; b ∈ G; a = b ∨ P ` ⟨b, GroupInv(G, P) ` a⟩ ∈ PositiveSet(G, P, r) |] ==> ⟨a, b⟩ ∈ r
lemma OrderedGroup_ZF_1_L31:
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G |] ==> a = b ∨ ⟨a, b⟩ ∈ r ∧ a ≠ b ∨ ⟨b, a⟩ ∈ r ∧ b ≠ a
lemma OrderedGroup_ZF_2_L1:
[| group3(G, P, r); ∀g∈A. ⟨L, g⟩ ∈ r ∧ ⟨g, M⟩ ∈ r; S = RightTranslation(G, P, GroupInv(G, P) ` L); a ∈ S `` A |] ==> ⟨a, P ` ⟨M, GroupInv(G, P) ` L⟩⟩ ∈ r
[| group3(G, P, r); ∀g∈A. ⟨L, g⟩ ∈ r ∧ ⟨g, M⟩ ∈ r; S = RightTranslation(G, P, GroupInv(G, P) ` L); a ∈ S `` A |] ==> ⟨TheNeutralElement(G, P), a⟩ ∈ r
lemma OrderedGroup_ZF_2_L2:
[| group3(G, P, r); IsBounded(A, r) |] ==> ∃B. ∃g∈Nonnegative(G, P, r). ∃T∈G -> G. A = T `` B ∧ B ⊆ Interval(r, TheNeutralElement(G, P), g)
theorem OrderedGroup_ZF_2_T1:
[| group3(G, P, r); ∀g∈Nonnegative(G, P, r). Interval(r, TheNeutralElement(G, P), g) ∈ Fin(G); IsBounded(A, r) |] ==> A ∈ Fin(G)
theorem ord_group_fin_bounded:
[| group3(G, P, r); r {is total on} G; B ∈ Fin(G) |] ==> IsBounded(B, r)
lemma OrderedGroup_ZF_2_L2A:
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)}; ∀a∈G. ∃b∈A. ⟨a, b⟩ ∈ r |] ==> ∀a∈G. ∃b∈A. a ≠ b ∧ ⟨a, b⟩ ∈ r
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)}; ∀a∈G. ∃b∈A. ⟨a, b⟩ ∈ r |] ==> ¬ IsBoundedAbove(A, r)
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)}; ∀a∈G. ∃b∈A. ⟨a, b⟩ ∈ r |] ==> A ∉ Fin(G)
theorem Linord_group_infinite:
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)} |] ==> PositiveSet(G, P, r) ∉ Fin(G)
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)} |] ==> G ∉ Fin(G)
lemma OrderedGroup_ZF_2_L2B:
[| group3(G, P, r); r {is total on} G; A ⊆ G; ¬ HasAmaximum(r, A); x ∈ A |] ==> ∃y∈A. ⟨x, y⟩ ∈ r ∧ x ≠ y
lemma OrderedGroup_ZF_2_L3:
[| group3(G, P, r); r {is total on} G |] ==> IsBoundedAbove(G - PositiveSet(G, P, r), r)
lemma OrderedGroup_ZF_2_L4:
[| group3(G, P, r); r {is total on} G; A ⊆ G; A ∩ PositiveSet(G, P, r) ∈ Fin(G) |] ==> IsBoundedAbove(A, r)
lemma OrderedGroup_ZF_2_L5:
[| group3(G, P, r); A ⊆ G; IsBoundedAbove(GroupInv(G, P) `` A, r) |] ==> IsBoundedBelow(A, r)
lemma OrderedGroup_ZF_2_L6:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; f ∈ G -> G |] ==> f `` Interval(r, a, b) ≠ 0
lemma OrderedGroup_ZF_3_L1:
group3(G, P, r) ==> AbsoluteValue(G, P, r) ∈ G -> G
lemma OrderedGroup_ZF_3_L2:
[| group3(G, P, r); a ∈ Nonnegative(G, P, r) |] ==> AbsoluteValue(G, P, r) ` a = a
lemma OrderedGroup_ZF_3_L2A:
group3(G, P, r) ==> AbsoluteValue(G, P, r) ` TheNeutralElement(G, P) = TheNeutralElement(G, P)
lemma OrderedGroup_ZF_3_L2B:
[| group3(G, P, r); a ∈ PositiveSet(G, P, r) |] ==> AbsoluteValue(G, P, r) ` a = a
lemma OrderedGroup_ZF_3_L3:
[| group3(G, P, r); a ∈ G - Nonnegative(G, P, r) |] ==> AbsoluteValue(G, P, r) ` a = GroupInv(G, P) ` a
lemma OrderedGroup_ZF_3_L3A:
[| group3(G, P, r); ⟨a, TheNeutralElement(G, P)⟩ ∈ r |] ==> AbsoluteValue(G, P, r) ` a = GroupInv(G, P) ` a
lemma OrderedGroup_ZF_3_L3B:
[| group3(G, P, r); r {is total on} G; a ∈ G |] ==> AbsoluteValue(G, P, r) ` a ∈ Nonnegative(G, P, r)
lemma OrderedGroup_ZF_3_L3C:
[| group3(G, P, r); r {is total on} G |] ==> AbsoluteValue(G, P, r) ∈ G -> Nonnegative(G, P, r)
lemma OrderedGroup_ZF_3_L3D:
[| group3(G, P, r); a ∈ G; AbsoluteValue(G, P, r) ` a = TheNeutralElement(G, P) |] ==> a = TheNeutralElement(G, P)
lemma OrderedGroup_ZF_3_L3E:
[| group3(G, P, r); r {is total on} G; a ∈ G |] ==> ⟨TheNeutralElement(G, P), AbsoluteValue(G, P, r) ` a⟩ ∈ r
lemma OrderedGroup_ZF_3_L4:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; ⟨GroupInv(G, P) ` a, b⟩ ∈ r |] ==> ⟨AbsoluteValue(G, P, r) ` a, b⟩ ∈ r
lemma OrderedGroup_ZF_3_L5:
[| group3(G, P, r); r {is total on} G; a ∈ G |] ==> ⟨a, AbsoluteValue(G, P, r) ` a⟩ ∈ r
lemma OrderedGroup_ZF_3_L6:
[| group3(G, P, r); a ∈ G |] ==> ⟨GroupInv(G, P) ` a, AbsoluteValue(G, P, r) ` a⟩ ∈ r
lemma OrderedGroup_ZF_3_L6A:
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G |] ==> ⟨P ` ⟨a, b⟩, P ` ⟨AbsoluteValue(G, P, r) ` a, AbsoluteValue(G, P, r) ` b⟩⟩ ∈ r
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G |] ==> ⟨P ` ⟨a, GroupInv(G, P) ` b⟩, P ` ⟨AbsoluteValue(G, P, r) ` a, AbsoluteValue(G, P, r) ` b⟩⟩ ∈ r
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G |] ==> ⟨P ` ⟨GroupInv(G, P) ` a, b⟩, P ` ⟨AbsoluteValue(G, P, r) ` a, AbsoluteValue(G, P, r) ` b⟩⟩ ∈ r
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G |] ==> ⟨P ` ⟨GroupInv(G, P) ` a, GroupInv(G, P) ` b⟩, P ` ⟨AbsoluteValue(G, P, r) ` a, AbsoluteValue(G, P, r) ` b⟩⟩ ∈ r
lemma OrderedGroup_ZF_3_L7:
[| group3(G, P, r); r {is total on} G; a ∈ G |] ==> ⟨AbsoluteValue(G, P, r) ` (GroupInv(G, P) ` a), AbsoluteValue(G, P, r) ` a⟩ ∈ r
lemma OrderedGroup_ZF_3_L7A:
[| group3(G, P, r); r {is total on} G; a ∈ G |] ==> AbsoluteValue(G, P, r) ` (GroupInv(G, P) ` a) = AbsoluteValue(G, P, r) ` a
lemma OrderedGroup_ZF_3_L7B:
[| group3(G, P, r); r {is total on} G; a ∈ G; b ∈ G |] ==> AbsoluteValue(G, P, r) ` (P ` ⟨a, GroupInv(G, P) ` b⟩) = AbsoluteValue(G, P, r) ` (P ` ⟨b, GroupInv(G, P) ` a⟩)
theorem OrdGroup_triangle_ineq:
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G |] ==> ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, b⟩), P ` ⟨AbsoluteValue(G, P, r) ` a, AbsoluteValue(G, P, r) ` b⟩⟩ ∈ r
lemma OrderedGroup_ZF_3_L7C:
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; ⟨AbsoluteValue(G, P, r) ` a, c⟩ ∈ r; ⟨AbsoluteValue(G, P, r) ` b, d⟩ ∈ r |] ==> ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, b⟩), P ` ⟨c, d⟩⟩ ∈ r
lemma OrderedGroup_ZF_3_L7CA:
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; ⟨AbsoluteValue(G, P, r) ` a, c⟩ ∈ r; ⟨AbsoluteValue(G, P, r) ` b, d⟩ ∈ r |] ==> ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, GroupInv(G, P) ` b⟩), P ` ⟨c, d⟩⟩ ∈ r
lemma OrdGroup_triangle_ineq3:
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; c ∈ G |] ==> ⟨AbsoluteValue(G, P, r) ` (P ` ⟨P ` ⟨a, b⟩, c⟩), P ` ⟨P ` ⟨AbsoluteValue(G, P, r) ` a, AbsoluteValue(G, P, r) ` b⟩, AbsoluteValue(G, P, r) ` c⟩⟩ ∈ r
lemma OrderedGroup_ZF_3_L7D:
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, GroupInv(G, P) ` b⟩), c⟩ ∈ r |] ==> ⟨AbsoluteValue(G, P, r) ` a, P ` ⟨c, AbsoluteValue(G, P, r) ` b⟩⟩ ∈ r
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, GroupInv(G, P) ` b⟩), c⟩ ∈ r |] ==> ⟨AbsoluteValue(G, P, r) ` a, P ` ⟨AbsoluteValue(G, P, r) ` b, c⟩⟩ ∈ r
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, GroupInv(G, P) ` b⟩), c⟩ ∈ r |] ==> ⟨P ` ⟨GroupInv(G, P) ` c, a⟩, b⟩ ∈ r
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, GroupInv(G, P) ` b⟩), c⟩ ∈ r |] ==> ⟨P ` ⟨a, GroupInv(G, P) ` c⟩, b⟩ ∈ r
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, GroupInv(G, P) ` b⟩), c⟩ ∈ r |] ==> ⟨a, P ` ⟨b, c⟩⟩ ∈ r
lemma OrderedGroup_ZF_3_L7E:
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, GroupInv(G, P) ` b⟩), c⟩ ∈ r |] ==> ⟨P ` ⟨b, GroupInv(G, P) ` c⟩, a⟩ ∈ r
lemma OrderedGroup_ZF_3_L7F:
[| group3(G, P, r); P {is commutative on} G; r {is total on} G; a ∈ G; b ∈ G; c ∈ G; d ∈ G |] ==> ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, GroupInv(G, P) ` c⟩), P ` ⟨P ` ⟨AbsoluteValue(G, P, r) ` (P ` ⟨a, b⟩), AbsoluteValue(G, P, r) ` (P ` ⟨c, d⟩)⟩, AbsoluteValue(G, P, r) ` (P ` ⟨b, GroupInv(G, P) ` d⟩)⟩⟩ ∈ r
lemma OrderedGroup_ZF_3_L8:
[| group3(G, P, r); a ∈ G; ⟨AbsoluteValue(G, P, r) ` a, L⟩ ∈ r |] ==> ⟨GroupInv(G, P) ` L, a⟩ ∈ r
lemma OrderedGroup_ZF_3_L8A:
[| group3(G, P, r); r {is total on} G; a ∈ G; ⟨AbsoluteValue(G, P, r) ` a, L⟩ ∈ r |] ==> ⟨a, L⟩ ∈ r
[| group3(G, P, r); r {is total on} G; a ∈ G; ⟨AbsoluteValue(G, P, r) ` a, L⟩ ∈ r |] ==> ⟨TheNeutralElement(G, P), L⟩ ∈ r
lemma OrderedGroup_ZF_3_L8B:
[| group3(G, P, r); a ∈ G; ⟨AbsoluteValue(G, P, r) ` a, L⟩ ∈ r; ⟨TheNeutralElement(G, P), c⟩ ∈ r |] ==> ⟨GroupInv(G, P) ` (P ` ⟨L, c⟩), a⟩ ∈ r
lemma OrderedGroup_ZF_3_L8C:
[| group3(G, P, r); ⟨a, b⟩ ∈ r; c ∈ G; ⟨b, P ` ⟨c, a⟩⟩ ∈ r |] ==> ⟨AbsoluteValue(G, P, r) ` (P ` ⟨b, GroupInv(G, P) ` a⟩), c⟩ ∈ r
lemma OrderedGroup_ZF_3_L9:
[| group3(G, P, r); r {is total on} G; A ⊆ G; ∀a∈A. ⟨AbsoluteValue(G, P, r) ` a, L⟩ ∈ r |] ==> IsBounded(A, r)
lemma OrderedGroup_ZF_3_L9A:
[| group3(G, P, r); r {is total on} G; ∀x∈X. b(x) ∈ G ∧ ⟨AbsoluteValue(G, P, r) ` b(x), L⟩ ∈ r |] ==> IsBounded({b(x) . x ∈ X}, r)
lemma OrderedGroup_ZF_3_L9B:
[| group3(G, P, r); r {is total on} G; f ∈ X -> G; A ⊆ X; ∀x∈A. ⟨AbsoluteValue(G, P, r) ` (f ` x), L⟩ ∈ r |] ==> IsBounded(f `` A, r)
lemma OrderedGroup_ZF_3_L10:
[| group3(G, P, r); r {is total on} G; ⟨l, a⟩ ∈ r; ⟨a, u⟩ ∈ r |] ==> ⟨AbsoluteValue(G, P, r) ` a, GreaterOf(r, AbsoluteValue(G, P, r) ` l, AbsoluteValue(G, P, r) ` u)⟩ ∈ r
lemma OrderedGroup_ZF_3_L10A:
[| group3(G, P, r); r {is total on} G; IsBounded(A, r) |] ==> ∃L. ∀a∈A. ⟨AbsoluteValue(G, P, r) ` a, L⟩ ∈ r
lemma OrderedGroup_ZF_3_L11:
[| group3(G, P, r); r {is total on} G; IsBounded({b(x) . x ∈ X}, r) |] ==> ∃L. ∀x∈X. ⟨AbsoluteValue(G, P, r) ` b(x), L⟩ ∈ r
lemma OrderedGroup_ZF_3_L11A:
[| group3(G, P, r); r {is total on} G; X ≠ 0; {b(x) . x ∈ X} ∈ Fin(G) |] ==> ∃L∈G. ∀x∈X. ⟨AbsoluteValue(G, P, r) ` b(x), L⟩ ∈ r
lemma OrderedGroup_ZF_3_L12:
[| group3(G, P, r); r {is total on} G; a ∈ G; a ≠ TheNeutralElement(G, P) |] ==> AbsoluteValue(G, P, r) ` a ∈ PositiveSet(G, P, r)
lemma OrderedGroup_ZF_4_L1:
[| group3(G, P, r); A ⊆ G; HasAmaximum(r, A); HasAminimum(r, A); M = GreaterOf (r, AbsoluteValue(G, P, r) ` Minimum(r, A), AbsoluteValue(G, P, r) ` Maximum(r, A)) |] ==> M ∈ AbsoluteValue(G, P, r) `` A
lemma OrderedGroup_ZF_4_L2:
[| group3(G, P, r); r {is total on} G; HasAmaximum(r, A); HasAminimum(r, A); a ∈ A |] ==> ⟨AbsoluteValue(G, P, r) ` a, GreaterOf (r, AbsoluteValue(G, P, r) ` Minimum(r, A), AbsoluteValue(G, P, r) ` Maximum(r, A))⟩ ∈ r
lemma OrderedGroup_ZF_4_L3:
[| group3(G, P, r); r {is total on} G; A ⊆ G; HasAmaximum(r, A); HasAminimum(r, A); b ∈ AbsoluteValue(G, P, r) `` A |] ==> ⟨b, GreaterOf (r, AbsoluteValue(G, P, r) ` Minimum(r, A), AbsoluteValue(G, P, r) ` Maximum(r, A))⟩ ∈ r
lemma OrderedGroup_ZF_4_L4:
[| group3(G, P, r); r {is total on} G; A ⊆ G; HasAmaximum(r, A); HasAminimum(r, A) |] ==> HasAmaximum(r, AbsoluteValue(G, P, r) `` A)
lemma OrderedGroup_ZF_4_L5:
[| group3(G, P, r); r {is total on} G; A ⊆ G; HasAmaximum(r, A); HasAminimum(r, A); a ∈ A |] ==> ⟨AbsoluteValue(G, P, r) ` a, Maximum(r, AbsoluteValue(G, P, r) `` A)⟩ ∈ r
lemma OrderedGroup_ZF_5_L1:
[| group0(G, f); r = {p ∈ G × G . fst(p) = snd(p) ∨ f ` ⟨GroupInv(G, f) ` fst(p), snd(p)⟩ ∈ H} |] ==> ⟨a, b⟩ ∈ r <-> a ∈ G ∧ b ∈ G ∧ f ` ⟨GroupInv(G, f) ` a, b⟩ ∈ H ∪ {TheNeutralElement(G, f)}
lemma OrderedGroup_ZF_5_L2:
[| group0(G, f); r = {p ∈ G × G . fst(p) = snd(p) ∨ f ` ⟨GroupInv(G, f) ` fst(p), snd(p)⟩ ∈ H}; ∀a∈G. a ≠ TheNeutralElement(G, f) --> (a ∈ H) Xor (GroupInv(G, f) ` a ∈ H) |] ==> antisym(r)
lemma OrderedGroup_ZF_5_L3:
[| group0(G, f); r = {p ∈ G × G . fst(p) = snd(p) ∨ f ` ⟨GroupInv(G, f) ` fst(p), snd(p)⟩ ∈ H}; H ⊆ G; H {is closed under} f |] ==> trans(r)
lemma OrderedGroup_ZF_5_L4:
[| group0(G, f); r = {p ∈ G × G . fst(p) = snd(p) ∨ f ` ⟨GroupInv(G, f) ` fst(p), snd(p)⟩ ∈ H}; f {is commutative on} G; ⟨a, b⟩ ∈ r; c ∈ G |] ==> ⟨f ` ⟨a, c⟩, f ` ⟨b, c⟩⟩ ∈ r ∧ ⟨f ` ⟨c, a⟩, f ` ⟨c, b⟩⟩ ∈ r
lemma OrderedGroup_ZF_5_L5:
[| group0(G, f); f {is commutative on} G; H ⊆ G; H {is closed under} f; ∀a∈G. a ≠ TheNeutralElement(G, f) --> (a ∈ H) Xor (GroupInv(G, f) ` a ∈ H); r = {p ∈ G × G . fst(p) = snd(p) ∨ f ` ⟨GroupInv(G, f) ` fst(p), snd(p)⟩ ∈ H} |] ==> IsAnOrdGroup(G, f, r)
[| group0(G, f); f {is commutative on} G; H ⊆ G; H {is closed under} f; ∀a∈G. a ≠ TheNeutralElement(G, f) --> (a ∈ H) Xor (GroupInv(G, f) ` a ∈ H); r = {p ∈ G × G . fst(p) = snd(p) ∨ f ` ⟨GroupInv(G, f) ` fst(p), snd(p)⟩ ∈ H} |] ==> r {is total on} G
[| group0(G, f); f {is commutative on} G; H ⊆ G; H {is closed under} f; ∀a∈G. a ≠ TheNeutralElement(G, f) --> (a ∈ H) Xor (GroupInv(G, f) ` a ∈ H); r = {p ∈ G × G . fst(p) = snd(p) ∨ f ` ⟨GroupInv(G, f) ` fst(p), snd(p)⟩ ∈ H} |] ==> Nonnegative(G, f, r) = PositiveSet(G, f, r) ∪ {TheNeutralElement(G, f)}
lemma OrderedGroup_ZF_5_L6:
[| group0(G, f); f {is commutative on} G; H ⊆ G; TheNeutralElement(G, f) ∉ H; r = {p ∈ G × G . fst(p) = snd(p) ∨ f ` ⟨GroupInv(G, f) ` fst(p), snd(p)⟩ ∈ H} |] ==> PositiveSet(G, f, r) = H
theorem Group_ord_by_positive_set:
[| group0(G, f); f {is commutative on} G; H ⊆ G; H {is closed under} f; TheNeutralElement(G, f) ∉ H; ∀a∈G. a ≠ TheNeutralElement(G, f) --> (a ∈ H) Xor (GroupInv(G, f) ` a ∈ H) |] ==> IsAnOrdGroup(G, f, OrderFromPosSet(G, f, H))
[| group0(G, f); f {is commutative on} G; H ⊆ G; H {is closed under} f; TheNeutralElement(G, f) ∉ H; ∀a∈G. a ≠ TheNeutralElement(G, f) --> (a ∈ H) Xor (GroupInv(G, f) ` a ∈ H) |] ==> OrderFromPosSet(G, f, H) {is total on} G
[| group0(G, f); f {is commutative on} G; H ⊆ G; H {is closed under} f; TheNeutralElement(G, f) ∉ H; ∀a∈G. a ≠ TheNeutralElement(G, f) --> (a ∈ H) Xor (GroupInv(G, f) ` a ∈ H) |] ==> PositiveSet(G, f, OrderFromPosSet(G, f, H)) = H
[| group0(G, f); f {is commutative on} G; H ⊆ G; H {is closed under} f; TheNeutralElement(G, f) ∉ H; ∀a∈G. a ≠ TheNeutralElement(G, f) --> (a ∈ H) Xor (GroupInv(G, f) ` a ∈ H) |] ==> Nonnegative(G, f, OrderFromPosSet(G, f, H)) = H ∪ {TheNeutralElement(G, f)}
lemma OrderedGroup_ZF_6_L1:
group3(G, P, r) ==> OddExtension(G, P, r, f) = f ∪ {⟨a, GroupInv(G, P) ` (f ` (GroupInv(G, P) ` a))⟩ . a ∈ GroupInv(G, P) `` PositiveSet(G, P, r)} ∪ {⟨TheNeutralElement(G, P), TheNeutralElement(G, P)⟩}
lemma OrderedGroup_ZF_6_L2:
[| group3(G, P, r); f ∈ PositiveSet(G, P, r) -> G; a ∈ GroupInv(G, P) `` PositiveSet(G, P, r) |] ==> f ` (GroupInv(G, P) ` a) ∈ G
[| group3(G, P, r); f ∈ PositiveSet(G, P, r) -> G; a ∈ GroupInv(G, P) `` PositiveSet(G, P, r) |] ==> GroupInv(G, P) ` (f ` (GroupInv(G, P) ` a)) ∈ G
lemma odd_ext_props:
[| group3(G, P, r); r {is total on} G; f ∈ PositiveSet(G, P, r) -> G |] ==> OddExtension(G, P, r, f) ∈ G -> G
[| group3(G, P, r); r {is total on} G; f ∈ PositiveSet(G, P, r) -> G |] ==> ∀a∈PositiveSet(G, P, r). OddExtension(G, P, r, f) ` a = f ` a
[| group3(G, P, r); r {is total on} G; f ∈ PositiveSet(G, P, r) -> G |] ==> ∀a∈GroupInv(G, P) `` PositiveSet(G, P, r). OddExtension(G, P, r, f) ` a = GroupInv(G, P) ` (f ` (GroupInv(G, P) ` a))
[| group3(G, P, r); r {is total on} G; f ∈ PositiveSet(G, P, r) -> G |] ==> OddExtension(G, P, r, f) ` TheNeutralElement(G, P) = TheNeutralElement(G, P)
lemma oddext_is_odd:
[| group3(G, P, r); r {is total on} G; f ∈ PositiveSet(G, P, r) -> G; a ∈ G |] ==> OddExtension(G, P, r, f) ` (GroupInv(G, P) ` a) = GroupInv(G, P) ` (OddExtension(G, P, r, f) ` a)
lemma oddext_is_odd_alt:
[| group3(G, P, r); r {is total on} G; f ∈ PositiveSet(G, P, r) -> G; a ∈ G |] ==> GroupInv(G, P) ` (OddExtension(G, P, r, f) ` (GroupInv(G, P) ` a)) = OddExtension(G, P, r, f) ` a
lemma OrderedGroup_ZF_7_L1:
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)}; f ∈ G -> G; ∀a∈G. ∃b∈PositiveSet(G, P, r). ∀x. ⟨b, x⟩ ∈ r --> ⟨a, f ` x⟩ ∈ r; A ⊆ G; IsBoundedAbove(f `` A, r) |] ==> IsBoundedAbove(A, r)
lemma OrderedGroup_ZF_7_L2:
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)}; X ≠ 0; f ∈ G -> G; ∀a∈G. ∃b∈PositiveSet(G, P, r). ∀y. ⟨b, y⟩ ∈ r --> ⟨a, f ` y⟩ ∈ r; ∀x∈X. b(x) ∈ G ∧ ⟨f ` b(x), U⟩ ∈ r |] ==> ∃u. ∀x∈X. ⟨b(x), u⟩ ∈ r
lemma OrderedGroup_ZF_7_L3:
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)}; X ≠ 0; f ∈ G -> G; ∀a∈G. ∃b∈PositiveSet(G, P, r). ∀y. ⟨b, y⟩ ∈ r --> ⟨f ` (GroupInv(G, P) ` y), a⟩ ∈ r; ∀x∈X. b(x) ∈ G ∧ ⟨L, f ` b(x)⟩ ∈ r |] ==> ∃l. ∀x∈X. ⟨l, b(x)⟩ ∈ r
lemma OrderedGroup_ZF_7_L4:
[| group3(G, P, r); r {is total on} G; G ≠ {TheNeutralElement(G, P)}; X ≠ 0; f ∈ G -> G; ∀a∈G. ∃b∈PositiveSet(G, P, r). ∀y. ⟨b, y⟩ ∈ r --> ⟨a, f ` y⟩ ∈ r; ∀a∈G. ∃b∈PositiveSet(G, P, r). ∀y. ⟨b, y⟩ ∈ r --> ⟨f ` (GroupInv(G, P) ` y), a⟩ ∈ r; ∀x∈X. b(x) ∈ G ∧ ⟨L, f ` b(x)⟩ ∈ r ∧ ⟨f ` b(x), U⟩ ∈ r |] ==> ∃M. ∀x∈X. ⟨AbsoluteValue(G, P, r) ` b(x), M⟩ ∈ r