begin
This theory file is about properties of loops (the algebraic structures introduced in IsarMathLib in the Loop_ZF theory) with an additional order relation that is in a way compatible with the loop's binary operation. The oldest reference I have found on the subject is \cite{Zelinski1948}.
Definition, notation and basic properties
An ordered loop \((G,A)\) is a loop with a partial order relation r that is "translation invariant" with respect to the loop operation \(A\).
A triple \((G,A,r)\) is an ordered loop if \((G,A)\) is a loop and \(r\) is a relation on \(G\) (i.e. a subset of \(G\times G\) with is a partial order and for all elements \(x,y,z \in G\) the condition \(\langle x,y\rangle \in r\) is equivalent to both \(\langle A\langle x,z\rangle, A\langle x,z\rangle\rangle \in r\) and \(\langle A\langle z,x\rangle, A\langle z,x\rangle\rangle \in r\). This looks a bit awkward in the basic set theory notation, but using the additive notation for the group operation and \(x\leq y\) to instead of \(\langle x,y \rangle \in r\) this just means that \(x\leq y\) if and only if \(x+z\leq y+z\) and \(x\leq y\) if and only if \(z+x\leq z+y\).
definition
\( \text{IsAnOrdLoop}(L,A,r) \equiv \) \( \text{IsAloop}(L,A) \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \forall z\in L.\ \) \( ((\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ))) \)
We define the set of nonnegative elements in the obvious way as \(L^+ =\{x\in L: 0 \leq x\}\).
definition
\( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)
The \( \text{PositiveSet}(L,A,r) \) is a set similar to \( \text{Nonnegative}(L,A,r) \), but without the neutral element. What we call the positive set here is sometimes called "the positive cone" of an ordered loop.
definition
\( \text{PositiveSet}(L,A,r) \equiv \) \( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} \)
We will use the additive notation for ordered loops.
locale loop1
assumes ordLoopAssum: \( \text{IsAnOrdLoop}(L,A,r) \)
defines \( 0 \equiv \text{ TheNeutralElement}(L,A) \)
defines \( x + y \equiv A\langle x,y\rangle \)
defines \( x \leq y \equiv \langle x,y\rangle \in r \)
defines \( x \lt y \equiv x\leq y \wedge x\neq y \)
defines \( L^+ \equiv \text{Nonnegative}(L,A,r) \)
defines \( L_+ \equiv \text{PositiveSet}(L,A,r) \)
defines \( - x + y \equiv \text{ LeftDiv}(L,A)\langle x,y\rangle \)
defines \( x - y \equiv \text{ RightDiv}(L,A)\langle y,x\rangle \)
defines \( \sum s \equiv \text{Fold}(A, 0 ,s) \)
defines \( n\cdot x \equiv \sum \{\langle k,x\rangle .\ k\in n\} \)
Theorems proven in the loop0 locale are valid in the loop1 locale
sublocale loop1 < loop0
using ordLoopAssum, loop_loop0_valid unfolding IsAnOrdLoop_def
The notation \(-x+y\) and \(x-y\) denotes left and right division, resp. These two operations are closed in a loop, see lemma lrdiv_binop in the Quasigroup_ZF theory. The next lemma reiterates that fact using the notation of the loop1 context.
lemma (in loop1) left_right_sub_closed:
assumes \( x\in L \), \( y\in L \)
shows \( ( - x + y) \in L \) and \( x - y \in L \)proof from qgroupassum have \( \text{ LeftDiv}(L,A):L\times L \rightarrow L \) and \( \text{ RightDiv}(L,A):L\times L \rightarrow L \) using lrdiv_binop
with assms show \( ( - x + y) \in L \) and \( x - y \in L \) using apply_funtype
qed
In this context \(x \leq y\) implies that both \(x\) and \(y\) belong to \(L\).
lemma (in loop1) lsq_members:
assumes \( x\leq y \)
shows \( x\in L \) and \( y\in L \) using ordLoopAssum, assms, IsAnOrdLoop_defIn this context \(x < y\) implies that both \(x\) and \(y\) belong to \(L\).
lemma (in loop1) less_members:
assumes \( x \lt y \)
shows \( x\in L \) and \( y\in L \) using ordLoopAssum, assms, IsAnOrdLoop_defIn an ordered loop the order is translation invariant.
lemma (in loop1) ord_trans_inv:
assumes \( x\leq y \), \( z\in L \)
shows \( x + z \leq y + z \) and \( z + x \leq z + y \)proof from ordLoopAssum, assms have \( (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ) \) using lsq_members unfolding IsAnOrdLoop_def
with assms(1) show \( x + z \leq y + z \) and \( z + x \leq z + y \)
qed
In an ordered loop the strict order is translation invariant.
lemma (in loop1) strict_ord_trans_inv:
assumes \( x \lt y \), \( z\in L \)
shows \( x + z \lt y + z \) and \( z + x \lt z + y \)proof from assms have \( x + z \leq y + z \) and \( z + x \leq z + y \) using ord_trans_inv
moreover
qed
have \( x + z \neq y + z \) and \( z + x \neq z + y \)proof
ultimately show \( x + z \lt y + z \) and \( z + x \lt z + y \)
{
}
}
assume \( x + z = y + z \)
with assms have \( x=y \) using less_members, qg_cancel_right
with assms(1) have \( False \)
thus \( x + z \neq y + z \)
{
assume \( z + x = z + y \)
with assms have \( x=y \) using less_members, qg_cancel_left
with assms(1) have \( False \)
thus \( z + x \neq z + y \)
qed
We can cancel an element from both sides of an inequality on the right side.
lemma (in loop1) ineq_cancel_right:
assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( x + z \leq y + z \)
shows \( x\leq y \)proof from ordLoopAssum, assms(1,2,3) have \( \langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r \) unfolding IsAnOrdLoop_def
with assms(4) show \( x\leq y \)
qed
We can cancel an element from both sides of a strict inequality on the right side.
lemma (in loop1) strict_ineq_cancel_right:
assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( x + z \lt y + z \)
shows \( x \lt y \) using assms, ineq_cancel_rightWe can cancel an element from both sides of an inequality on the left side.
lemma (in loop1) ineq_cancel_left:
assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \leq z + y \)
shows \( x\leq y \)proof from ordLoopAssum, assms(1,2,3) have \( \langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r \) unfolding IsAnOrdLoop_def
with assms(4) show \( x\leq y \)
qed
We can cancel an element from both sides of a strict inequality on the left side.
lemma (in loop1) strict_ineq_cancel_left:
assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \lt z + y \)
shows \( x \lt y \) using assms, ineq_cancel_leftWe can subtract a loop element from both sides of inequality both on the left side and right.
lemma (in loop1) ineq_subtr_from_sides:
assumes \( x\leq y \), \( z\in L \)
shows \( x - z \leq y - z \) and \( ( - z + x) \leq - z + y \)proof from assms have T: \( x - z\in L \), \( y - z\in L \), \( ( - z + x)\in L \), \( ( - z + y)\in L \) and \( x = (x - z) + z \), \( y = (y - z) + z \) and \( x = z + ( - z + x) \), \( y = z + ( - z + y) \) using lsq_members, lrdiv_props(2,3,5,6)
with assms(1) have \( (x - z) + z \leq (y - z) + z \) and \( z + ( - z + x) \leq z + ( - z + y) \)
with assms(2), T show \( x - z \leq y - z \) and \( ( - z + x) \leq - z + y \) using ineq_cancel_left, ineq_cancel_right
qed
We can subtract a loop element from both sides of of a strict inequality both on the left side and right.
lemma (in loop1) strict_ineq_subtr:
assumes \( x \lt y \), \( z\in L \)
shows \( x - z \lt y - z \) and \( ( - z + x) \lt - z + y \)proof from assms have T: \( x - z\in L \), \( y - z\in L \), \( ( - z + x)\in L \), \( ( - z + y)\in L \) and \( x = (x - z) + z \), \( y = (y - z) + z \) and \( x = z + ( - z + x) \), \( y = z + ( - z + y) \) using less_members, lrdiv_props(2,3,5,6)
with assms(1) have \( (x - z) + z \lt (y - z) + z \) and \( z + ( - z + x) \lt z + ( - z + y) \)
with assms(2), T show \( x - z \lt y - z \) and \( ( - z + x) \lt - z + y \) using strict_ineq_cancel_left, strict_ineq_cancel_right
qed
We can move an element to the other side of a strict inequality with three loop elements - right side variant.
lemma (in loop1) strict_ineq_move_side_right:
assumes \( x\in L \), \( y\in L \), \( x + y \lt z \)
shows \( x \lt z - y \)proof from assms(2,3) have \( (x + y) - y \lt z - y \) using strict_ineq_subtr
with assms(1,2) show \( x \lt z - y \) using lrdiv_ident(1)
qed
We can move an element to the other side of an inequality with three loop elements - right side variant.
lemma (in loop1) ineq_move_side_right:
assumes \( x\in L \), \( y\in L \), \( x + y\leq z \)
shows \( x\leq z - y \) using assms, ineq_subtr_from_sides, lrdiv_ident(1)The definition of the nonnegative set in the notation used in the loop1 locale:
lemma (in loop1) nonneg_definition:
shows \( x \in L^+ \longleftrightarrow 0 \leq x \) using ordLoopAssum, IsAnOrdLoop_def, Nonnegative_defThe nonnegative set is contained in the loop.
lemma (in loop1) nonneg_subset:
shows \( L^+ \subseteq L \) using Nonnegative_defThe positive set is contained in the loop.
lemma (in loop1) positive_subset:
shows \( L_+ \subseteq L \) using PositiveSet_defThe definition of the positive set in the notation used in the loop1 locale:
lemma (in loop1) posset_definition:
shows \( x \in L_+ \longleftrightarrow ( 0 \leq x \wedge x\neq 0 ) \) using ordLoopAssum, IsAnOrdLoop_def, PositiveSet_defAnother form of the definition of the positive set in the notation used in the loop1 locale:
lemma (in loop1) posset_definition1:
shows \( x \in L_+ \longleftrightarrow 0 \lt x \) using ordLoopAssum, IsAnOrdLoop_def, PositiveSet_defThe order in an ordered loop is antisymmeric.
lemma (in loop1) loop_ord_antisym:
assumes \( x\leq y \) and \( y\leq x \)
shows \( x=y \)proof from ordLoopAssum, assms have \( \text{antisym}(r) \), \( \langle x,y\rangle \in r \), \( \langle y,x\rangle \in r \) unfolding IsAnOrdLoop_def, IsPartOrder_def
then show \( x=y \) by (rule Fol1_L4 )
qed
The loop order is transitive.
lemma (in loop1) loop_ord_trans:
assumes \( x\leq y \) and \( y\leq z \)
shows \( x\leq z \)proof from ordLoopAssum, assms have \( \text{trans}(r) \) and \( \langle x,y\rangle \in r \wedge \langle y,z\rangle \in r \) unfolding IsAnOrdLoop_def, IsPartOrder_def
then have \( \langle x,z\rangle \in r \) by (rule Fol1_L3 )
thus \( thesis \)
qed
The loop order is reflexive.
lemma (in loop1) loop_ord_refl:
assumes \( x\in L \)
shows \( x\leq x \) using assms, ordLoopAssum unfolding IsAnOrdLoop_def, IsPartOrder_def, refl_defThe neutral element is nonnegative.
lemma (in loop1) loop_zero_nonneg:
shows \( 0 \in L^+ \) using neut_props_loop(1), loop_ord_refl, nonneg_definitionA form of mixed transitivity for the strict order:
lemma (in loop1) loop_strict_ord_trans:
assumes \( x\leq y \) and \( y \lt z \)
shows \( x \lt z \)proof from assms have \( x\leq y \) and \( y\leq z \)
then have \( x\leq z \) by (rule loop_ord_trans )
with assms show \( x \lt z \) using loop_ord_antisym
qed
Another form of mixed transitivity for the strict order:
lemma (in loop1) loop_strict_ord_trans1:
assumes \( x \lt y \) and \( y\leq z \)
shows \( x \lt z \)proof from assms have \( x\leq y \) and \( y\leq z \)
then have \( x\leq z \) by (rule loop_ord_trans )
with assms show \( x \lt z \) using loop_ord_antisym
qed
Yet another form of mixed transitivity for the strict order:
lemma (in loop1) loop_strict_ord_trans2:
assumes \( x \lt y \) and \( y \lt z \)
shows \( x \lt z \)proof from assms have \( x\leq y \) and \( y\leq z \)
then have \( x\leq z \) by (rule loop_ord_trans )
with assms show \( x \lt z \) using loop_ord_antisym
qed
We can move an element to the other side of an inequality. Well, not exactly, but our notation creates an illusion to that effect.
lemma (in loop1) lsq_other_side:
assumes \( x\leq y \)
shows \( 0 \leq - x + y \), \( ( - x + y) \in L^+ \), \( 0 \leq y - x \), \( (y - x) \in L^+ \)proof from assms have \( x\in L \), \( y\in L \), \( 0 \in L \), \( ( - x + y) \in L \), \( (y - x) \in L \) using lsq_members, neut_props_loop(1), lrdiv_props(2,5)
then have \( x = x + 0 \) and \( y = x + ( - x + y) \) using neut_props_loop(2), lrdiv_props(6)
with assms have \( x + 0 \leq x + ( - x + y) \)
with \( x\in L \), \( 0 \in L \), \( ( - x + y) \in L \) show \( 0 \leq - x + y \) using ineq_cancel_left
then show \( ( - x + y) \in L^+ \) using nonneg_definition
from \( x\in L \), \( y\in L \) have \( x = 0 + x \) and \( y = (y - x) + x \) using neut_props_loop(2), lrdiv_props(3)
with assms have \( 0 + x \leq (y - x) + x \)
with \( x\in L \), \( 0 \in L \), \( (y - x) \in L \) show \( 0 \leq y - x \) using ineq_cancel_right
then show \( (y - x) \in L^+ \) using nonneg_definition
qed
We can move an element to the other side of a strict inequality.
lemma (in loop1) ls_other_side:
assumes \( x \lt y \)
shows \( 0 \lt - x + y \), \( ( - x + y) \in L_+ \), \( 0 \lt y - x \), \( (y - x) \in L_+ \)proof from assms have \( x\in L \), \( y\in L \), \( 0 \in L \), \( ( - x + y) \in L \), \( (y - x) \in L \) using lsq_members, neut_props_loop(1), lrdiv_props(2,5)
then have \( x = x + 0 \) and \( y = x + ( - x + y) \) using neut_props_loop(2), lrdiv_props(6)
with assms have \( x + 0 \lt x + ( - x + y) \)
with \( x\in L \), \( 0 \in L \), \( ( - x + y) \in L \) show \( 0 \lt - x + y \) using strict_ineq_cancel_left
then show \( ( - x + y) \in L_+ \) using posset_definition1
from \( x\in L \), \( y\in L \) have \( x = 0 + x \) and \( y = (y - x) + x \) using neut_props_loop(2), lrdiv_props(3)
with assms have \( 0 + x \lt (y - x) + x \)
with \( x\in L \), \( 0 \in L \), \( (y - x) \in L \) show \( 0 \lt y - x \) using strict_ineq_cancel_right
then show \( (y - x) \in L_+ \) using posset_definition1
qed
We can add sides of inequalities.
lemma (in loop1) add_ineq:
assumes \( x\leq y \), \( z\leq t \)
shows \( x + z \leq y + t \)proof from assms have \( x + z \leq y + z \) using lsq_members(1), ord_trans_inv(1)
with assms show \( thesis \) using lsq_members(2), ord_trans_inv(2), loop_ord_trans
qed
We can add sides of strict inequalities. The proof uses a lemma that relies on the antisymmetry of the order relation.
lemma (in loop1) add_ineq_strict:
assumes \( x \lt y \), \( z \lt t \)
shows \( x + z \lt y + t \)proof from assms have \( x + z \lt y + z \) using less_members(1), strict_ord_trans_inv(1)
moreover
qed
from assms have \( y + z \lt y + t \) using less_members(2), strict_ord_trans_inv(2)
ultimately show \( thesis \) by (rule loop_strict_ord_trans2 )
We can add sides of inequalities one of which is strict.
lemma (in loop1) add_ineq_strict1:
assumes \( x\leq y \), \( z \lt t \)
shows \( x + z \lt y + t \) and \( z + x \lt t + y \)proof from assms have \( x + z \leq y + z \) using less_members(1), ord_trans_inv(1)
with assms show \( x + z \lt y + t \) using lsq_members(2), strict_ord_trans_inv(2), loop_strict_ord_trans
from assms have \( z + x \lt t + x \) using lsq_members(1), strict_ord_trans_inv(1)
with assms show \( z + x \lt t + y \) using less_members(2), ord_trans_inv(2), loop_strict_ord_trans1
qed
Subtracting a positive element decreases the value, while adding a positive element increases the value.
lemma (in loop1) add_subtract_pos:
assumes \( x\in L \), \( 0 \lt y \)
shows \( x - y \lt x \), \( ( - y + x) \lt x \), \( x \lt x + y \), \( x \lt y + x \)proof from assms(2) have \( y\in L \) using less_members(2)
from assms(1) have \( x\leq x \) using ordLoopAssum unfolding IsAnOrdLoop_def, IsPartOrder_def, refl_def
with assms(2) have \( x + 0 \lt x + y \) using add_ineq_strict1(1)
with assms, \( y\in L \) show \( x - y \lt x \) using neut_props_loop(2), lrdiv_props(3), lrdiv_props(2), strict_ineq_cancel_right
from assms(2), \( x\leq x \) have \( 0 + x \lt y + x \) using add_ineq_strict1(2)
with assms, \( y\in L \) show \( ( - y + x) \lt x \) using neut_props_loop(2), lrdiv_props(6), lrdiv_props(5), strict_ineq_cancel_left
from assms(1), \( x + 0 \lt x + y \), \( 0 + x \lt y + x \) show \( x \lt x + y \), \( x \lt y + x \) using neut_props_loop(2)
qed
In an ordered loop if the order relation down-directs the set of positive elements \(L_+\) then \(L_+\) is a down-directed set (see Order_ZF for definitions of those related but different notions).
lemma (in loop1) down_directs_directed:
assumes \( r \text{ down-directs } L_+ \)
shows \( \text{IsDownDirectedSet}(L_+,r) \) using ordLoopAssum, assms, positive_subset, down_directs_subset unfolding IsAnOrdLoop_defCompletness vs Archimedean property
For ordered fields the completeness of the order implies the Archimedean property: for every two positive elements there is a natural number \(n\) such that \(y < n x\). In 1891 Otto Stolz "succeeded in proving that the positive cone of a Dedekind complete ordered abelian group is Archimedean". In this section we consider the relation between the completeness of the order and the Archimedean property of the positive set of an ordered loop (not necessarily abelian).
Multiples of a positive element are positive.
lemma (in loop1) mults_pos_pos:
assumes \( 0 \lt x \), \( n\in nat\setminus \{0\} \)
shows \( 0 \lt n\cdot x \)proof from assms(1) have \( x\in L \) using less_members(2)
{
fix \( m \)
assume \( m\in nat \)
from \( x\in L \) have \( (0 + 1)\cdot x = 0\cdot x + x \) using loop_pow_mult_one
with assms(1), \( x\in L \) have \( 0 \lt (0 + 1)\cdot x \) using loop_zero_pow, neut_props_loop(2)
{
fix \( j \)
assume \( j\in nat \) and \( 0 \lt (j + 1)\cdot x \)
from \( x\in L \) have I: \( (j + 1 + 1)\cdot x = (j + 1)\cdot x + x \) using loop_pow_mult_one
from assms(1), \( x\in L \), \( j\in nat \) have \( (j + 1)\cdot x \lt (j + 1)\cdot x + x \) using loop_prod_type, add_subtract_pos(3)
with I have \( (j + 1)\cdot x \lt (j + 1 + 1)\cdot x \)
with \( 0 \lt (j + 1)\cdot x \) have \( 0 \lt (j + 1 + 1)\cdot x \) using loop_strict_ord_trans2
hence \( \forall j\in nat.\ 0 \lt (j + 1)\cdot x \longrightarrow 0 \lt (j + 1 + 1)\cdot x \)
with \( m\in nat \), \( 0 \lt (0 + 1)\cdot x \) have \( 0 \lt (m + 1)\cdot x \) by (rule ind_on_nat1 )
hence \( \forall m\in nat.\ 0 \lt (m + 1)\cdot x \)
with assms(2) show \( 0 \lt n\cdot x \) using nat_not0_succ
qed
If the order is complete and \(x\) is a positive element of a n ordered loop, then the set \(\{n\cdot x: n\in \mathbb{N}, n\neq 0\}\) is not bounded above.
lemma (in loop1) nat_mult_not_bounded:
assumes \( r \text{ is complete } \) and \( 0 \lt x \)
shows \( \neg \text{IsBoundedAbove}(\{n\cdot x.\ n\in nat\setminus \{0\}\},r) \)proof let \( M = \{n\cdot x.\ n\in nat\setminus \{0\}\} \)
{
assume C: \( \text{IsBoundedAbove}(M,r) \)
let \( S = \text{Supremum}(r,M) \)
from ordLoopAssum, assms(1) have I: \( r\subseteq L\times L \), \( \text{antisym}(r) \), \( r \text{ is complete } \), \( M\neq \emptyset \) using loop_not_empty unfolding IsAnOrdLoop_def, IsPartOrder_def
from I, C have \( S\in L \) using compl_bounded_sup_props(1)
from I, C have \( \forall y\in M.\ \langle y,S\rangle \in r \) by (rule compl_bounded_sup_props )
hence II: \( \forall n\in nat\setminus \{0\}.\ n\cdot x\leq S \)
{
fix \( n \)
assume \( n\in nat\setminus \{0\} \)
then have \( n + 1 \in nat\setminus \{0\} \)
with assms(2), II, \( n\in nat\setminus \{0\} \) have \( n\cdot x\leq S - x \) using less_members(2), loop_pow_mult_one, loop_prod_type, ineq_move_side_right
hence \( \forall y\in M.\ \langle y,S - x\rangle \in r \)
with \( \text{antisym}(r) \), assms(1), \( M\neq \emptyset \) have \( \langle S,S - x\rangle \in r \) by (rule compl_sup_leq_up_bnd )
hence \( S\leq S - x \)
from assms(2), \( S\in L \) have \( S - x \lt S \) using add_subtract_pos(1)
with \( S\leq S - x \) have \( False \) using loop_strict_ord_trans
thus \( thesis \)
qed
We say that a nonempty subset \(A\) of a ordered loop is Archimedean if for any two elements \(x,y\) of \(A\) there is a non-zero natural number \(n\) such that \(n\cdot x\) exceeds \(y\).
definition (in loop1)
\( B \text{ is Archimedean } \equiv B\neq \emptyset \wedge (\forall x\in B.\ \forall y\in B.\ \exists n\in nat\setminus \{0\}.\ y \lt n\cdot x) \)
If the order of the loop is complete and total on the positive set, then the positive set is Archimedean.
theorem (in loop1) loop_pos_set_archimedean:
assumes \( L_+\neq \emptyset \), \( r \text{ is complete } \) and \( r \text{ is total on } L_+ \)
shows \( L_+ \text{ is Archimedean } \)proof{
}
fix \( x \) \( y \)
assume \( x\in L_+ \), \( y\in L_+ \)
then have \( 0 \lt x \) and \( y\in L \) using posset_definition1, positive_subset
let \( M = \{n\cdot x.\ n\in nat\setminus \{0\}\} \)
from assms(1,2), \( 0 \lt x \) have \( \neg (\exists u.\ \forall z\in M.\ z\leq u) \) using nat_mult_not_bounded, IsBoundedAbove_def
then obtain \( z \) where \( z\in M \) and \( \neg (z\leq y) \)
from \( z\in M \) obtain \( n \) where \( n\in nat\setminus \{0\} \) and \( z=n\cdot x \)
from \( z=n\cdot x \), \( \neg (z\leq y) \) have \( \neg (n\cdot x\leq y) \)
from \( 0 \lt x \), \( n\in nat\setminus \{0\} \) have \( n\cdot x \in L_+ \) using mults_pos_pos, posset_definition
with assms(3), \( y\in L_+ \), \( \neg (n\cdot x\leq y) \), \( n\in nat\setminus \{0\} \) have \( \exists n\in nat\setminus \{0\}.\ y \lt n\cdot x \) unfolding IsTotal_def
with assms(1) show \( L_+ \text{ is Archimedean } \) unfolding IsArchimedean_def
qed
end
lemma loop_loop0_valid:
assumes \( \text{IsAloop}(G,A) \)
shows \( loop0(G,A) \)Definition of IsAnOrdLoop:
\( \text{IsAnOrdLoop}(L,A,r) \equiv \)
\( \text{IsAloop}(L,A) \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \forall z\in L.\ \)
\( ((\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ))) \)
lemma lrdiv_binop:
assumes \( \text{IsAquasigroup}(G,A) \)
shows \( \text{ LeftDiv}(G,A):G\times G\rightarrow G \) and \( \text{ RightDiv}(G,A):G\times G\rightarrow G \) lemma (in loop1) lsq_members:
assumes \( x\leq y \)
shows \( x\in L \) and \( y\in L \) lemma (in loop1) ord_trans_inv:
assumes \( x\leq y \), \( z\in L \)
shows \( x + z \leq y + z \) and \( z + x \leq z + y \) lemma (in loop1) less_members:
assumes \( x \lt y \)
shows \( x\in L \) and \( y\in L \) lemma (in quasigroup0) qg_cancel_right:
assumes \( x\in G \), \( y\in G \), \( z\in G \) and \( y\cdot x = z\cdot x \)
shows \( y=z \) lemma (in quasigroup0) qg_cancel_left:
assumes \( x\in G \), \( y\in G \), \( z\in G \) and \( x\cdot y = x\cdot z \)
shows \( y=z \) lemma (in group3) ineq_cancel_right:
assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\cdot b \leq c\cdot b \)
shows \( a\leq c \) lemma (in loop1) ineq_cancel_left:
assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \leq z + y \)
shows \( x\leq y \) lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in loop1) strict_ineq_cancel_left:
assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \lt z + y \)
shows \( x \lt y \) lemma (in loop1) strict_ineq_cancel_right:
assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( x + z \lt y + z \)
shows \( x \lt y \) lemma (in loop1) strict_ineq_subtr:
assumes \( x \lt y \), \( z\in L \)
shows \( x - z \lt y - z \) and \( ( - z + x) \lt - z + y \) lemma (in quasigroup0) lrdiv_ident:
assumes \( x\in G \), \( y\in G \)
shows \( (y\cdot x)/ x = y \) and \( x\backslash (x\cdot y) = y \) lemma (in loop1) ineq_subtr_from_sides:
assumes \( x\leq y \), \( z\in L \)
shows \( x - z \leq y - z \) and \( ( - z + x) \leq - z + y \)Definition of Nonnegative:
\( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)
Definition of PositiveSet:
\( \text{PositiveSet}(L,A,r) \equiv \)
\( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} \)
Definition of IsPartOrder:
\( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)
lemma Fol1_L4:
assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)
shows \( a=b \) lemma Fol1_L3:
assumes \( \text{trans}(r) \) and \( \langle a,b\rangle \in r \wedge \langle b,c\rangle \in r \)
shows \( \langle a,c\rangle \in r \) lemma (in loop0) neut_props_loop: shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)
lemma (in loop1) loop_ord_refl:
assumes \( x\in L \)
shows \( x\leq x \) lemma (in loop1) nonneg_definition: shows \( x \in L^+ \longleftrightarrow 0 \leq x \)
lemma (in loop1) loop_ord_trans:
assumes \( x\leq y \) and \( y\leq z \)
shows \( x\leq z \) lemma (in loop1) loop_ord_antisym:
assumes \( x\leq y \) and \( y\leq x \)
shows \( x=y \) lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in loop0) neut_props_loop: shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)
lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in loop1) posset_definition1: shows \( x \in L_+ \longleftrightarrow 0 \lt x \)
lemma (in loop1) lsq_members:
assumes \( x\leq y \)
shows \( x\in L \) and \( y\in L \) lemma (in loop1) ord_trans_inv:
assumes \( x\leq y \), \( z\in L \)
shows \( x + z \leq y + z \) and \( z + x \leq z + y \) lemma (in loop1) lsq_members:
assumes \( x\leq y \)
shows \( x\in L \) and \( y\in L \) lemma (in loop1) ord_trans_inv:
assumes \( x\leq y \), \( z\in L \)
shows \( x + z \leq y + z \) and \( z + x \leq z + y \) lemma (in loop1) less_members:
assumes \( x \lt y \)
shows \( x\in L \) and \( y\in L \) lemma (in loop1) strict_ord_trans_inv:
assumes \( x \lt y \), \( z\in L \)
shows \( x + z \lt y + z \) and \( z + x \lt z + y \) lemma (in loop1) less_members:
assumes \( x \lt y \)
shows \( x\in L \) and \( y\in L \) lemma (in loop1) strict_ord_trans_inv:
assumes \( x \lt y \), \( z\in L \)
shows \( x + z \lt y + z \) and \( z + x \lt z + y \) lemma (in loop1) loop_strict_ord_trans2:
assumes \( x \lt y \) and \( y \lt z \)
shows \( x \lt z \) lemma (in loop1) loop_strict_ord_trans:
assumes \( x\leq y \) and \( y \lt z \)
shows \( x \lt z \) lemma (in loop1) loop_strict_ord_trans1:
assumes \( x \lt y \) and \( y\leq z \)
shows \( x \lt z \) lemma (in loop1) add_ineq_strict1:
assumes \( x\leq y \), \( z \lt t \)
shows \( x + z \lt y + t \) and \( z + x \lt t + y \) lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in loop1) add_ineq_strict1:
assumes \( x\leq y \), \( z \lt t \)
shows \( x + z \lt y + t \) and \( z + x \lt t + y \) lemma (in quasigroup0) lrdiv_props:
assumes \( x\in G \), \( y\in G \)
shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \) lemma (in loop1) positive_subset: shows \( L_+ \subseteq L \)
lemma down_directs_subset:
assumes \( r \text{ down-directs } A \), \( \text{IsPartOrder}(X,r) \), \( A\subseteq X \)
shows \( \text{IsDownDirectedSet}(A,r) \) lemma (in loop0) loop_pow_mult_one:
assumes \( n\in nat \), \( x\in G \)
shows \( x^{n + 1} = x^{n}\cdot x \) corollary (in loop0) loop_zero_pow: shows \( x^{0} = 1 \)
lemma (in loop0) loop_prod_type:
assumes \( n\in nat \), \( x\in G \)
shows \( x^{n} \in G \) lemma (in loop1) add_subtract_pos:
assumes \( x\in L \), \( 0 \lt y \)
shows \( x - y \lt x \), \( ( - y + x) \lt x \), \( x \lt x + y \), \( x \lt y + x \) lemma ind_on_nat1:
assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(k + 1) \)
shows \( P(n) \) lemma nat_not0_succ:
assumes \( n\in nat \), \( n\neq 0 \)
shows \( \exists m\in nat.\ n = m + 1 \) corollary (in loop0) loop_not_empty: shows \( G\neq \emptyset \)
lemma compl_bounded_sup_props:
assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( r \text{ is complete } \) and \( A\neq 0 \), \( \text{IsBoundedAbove}(A,r) \)
shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \) lemma compl_bounded_sup_props:
assumes \( r \subseteq X\times X \), \( \text{antisym}(r) \), \( r \text{ is complete } \) and \( A\neq 0 \), \( \text{IsBoundedAbove}(A,r) \)
shows \( \text{Supremum}(r,A) \in X \) and \( \forall x\in A.\ \langle x, \text{Supremum}(r,A)\rangle \in r \) lemma (in loop1) ineq_move_side_right:
assumes \( x\in L \), \( y\in L \), \( x + y\leq z \)
shows \( x\leq z - y \) lemma compl_sup_leq_up_bnd:
assumes \( \text{antisym}(r) \), \( r \text{ is complete } \), \( A\neq \emptyset \), \( \forall a\in A.\ \langle a,u\rangle \in r \)
shows \( \langle \text{Supremum}(r,A),u\rangle \in r \) lemma (in loop1) add_subtract_pos:
assumes \( x\in L \), \( 0 \lt y \)
shows \( x - y \lt x \), \( ( - y + x) \lt x \), \( x \lt x + y \), \( x \lt y + x \) lemma (in loop1) nat_mult_not_bounded:
assumes \( r \text{ is complete } \) and \( 0 \lt x \)
shows \( \neg \text{IsBoundedAbove}(\{n\cdot x.\ n\in nat\setminus \{0\}\},r) \)Definition of IsBoundedAbove:
\( \text{IsBoundedAbove}(A,r) \equiv ( A=\emptyset \vee (\exists u.\ \forall x\in A.\ \langle x,u\rangle \in r)) \)
lemma (in loop1) mults_pos_pos:
assumes \( 0 \lt x \), \( n\in nat\setminus \{0\} \)
shows \( 0 \lt n\cdot x \) lemma (in loop1) posset_definition: shows \( x \in L_+ \longleftrightarrow ( 0 \leq x \wedge x\neq 0 ) \)
Definition of IsTotal:
\( r \text{ is total on } X \equiv (\forall a\in X.\ \forall b\in X.\ \langle a,b\rangle \in r \vee \langle b,a\rangle \in r) \)
Definition of IsArchimedean:
\( B \text{ is Archimedean } \equiv B\neq \emptyset \wedge (\forall x\in B.\ \forall y\in B.\ \exists n\in nat\setminus \{0\}.\ y \lt n\cdot x) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8