# IsarMathLib

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

theory OrderedLoop_ZF imports Loop_ZF Order_ZF
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 and notation

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.

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$$

Theorems proven in the loop0 locale are valid in the loop1 locale

Sublocale loop1 < loop0

using ordLoopAssum , loop_loop0_valid unfolding IsAnOrdLoop_def

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_def

In 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_def

In 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
have $$x + z \neq y + z$$ and $$z + x \neq z + y$$proof
{
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
ultimately show $$x + z \lt y + z$$ and $$z + x \lt 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_right

We 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_left

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_def

The nonnegative set is contained in the loop.

lemma (in loop1) nonneg_subset:

shows $$L^+ \subseteq L$$ using Nonnegative_def

The positive set is contained in the loop.

lemma (in loop1) positive_subset:

shows $$L_+ \subseteq L$$ using PositiveSet_def

The 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_def

Another 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_def

The 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

A 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

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
end
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 (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$$
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 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 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 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 loop1) nonneg_definition: shows $$x \in L^+ \longleftrightarrow 0 \leq 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 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) posset_definition1: shows $$x \in L_+ \longleftrightarrow 0 \lt x$$
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$$
46
55
13
13