# IsarMathLib

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

theory Loop_ZF imports Quasigroup_ZF
begin

This theory specifies the definition and proves basic properites of loops. Loops are very similar to groups, the only property that is missing is associativity of the operation.

### Definitions and notation

In this section we define the notions of identity element and left and right inverse.

A loop is a quasigroup with an identity elemen.

Definition

$$\text{IsAloop}(G,A) \equiv \text{IsAquasigroup}(G,A) \wedge (\exists e\in G.\ \forall x\in G.\ A\langle e,x\rangle = x \wedge A\langle x,e\rangle = x)$$

The neutral element for a binary operation $$A:G\times G \rightarrow G$$ is defined as the only element $$e$$ of $$G$$ such that $$A\langle x,e\rangle = x$$ and $$A\langle e,x\rangle = x$$ for all $$x\in G$$. Note that although the loop definition guarantees the existence of (some) such element(s) at this point we do not know if this element is unique. We can define this notion h ere but it will become usable only after we prove uniqueness.

Definition

$$\text{ TheNeutralElement}(G,f) \equiv$$ $$( \text{The } e.\ e\in G \wedge (\forall g\in G.\ f\langle e,g\rangle = g \wedge f\langle g,e\rangle = g))$$

We will reuse the notation defined in the quasigroup0 locale, just adding the assumption about the existence of a neutral element and notation for it.

Locale loop0 = quasigroup0 +

assumes ex_ident: $$\exists e\in G.\ \forall x\in G.\ e\cdot x = x \wedge x\cdot e = x$$

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

In the loop context the pair $$(G,A)$$ forms a loop.

lemma (in loop0) is_loop:

shows $$\text{IsAloop}(G,A)$$ unfolding IsAloop_def using ex_ident , qgroupassum

If we know that a pair $$(G,A)$$ forms a loop then the assumptions of the loop0 locale hold.

lemma loop_loop0_valid:

assumes $$\text{IsAloop}(G,A)$$

shows $$loop0(G,A)$$ using assms unfolding IsAloop_def , loop0_axioms_def , quasigroup0_def , loop0_def

The neutral element is unique in the loop.

lemma (in loop0) neut_uniq_loop:

shows $$\exists !e.\ e\in G \wedge (\forall x\in G.\ e\cdot x = x \wedge x\cdot e = x)$$proof
from ex_ident show $$\exists e.\ e \in G \wedge (\forall x\in G.\ e \cdot x = x \wedge x \cdot e = x)$$
next
fix $$e$$ $$y$$
assume $$e \in G \wedge (\forall x\in G.\ e \cdot x = x \wedge x \cdot e = x)$$, $$y \in G \wedge (\forall x\in G.\ y \cdot x = x \wedge x \cdot y = x)$$
then have $$e\cdot y =y$$ and $$e\cdot y = e$$
thus $$e=y$$
qed

The neutral element as defined in the loop0 locale is indeed neutral.

lemma (in loop0) neut_props_loop:

shows $$1 \in G$$ and $$\forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x$$proof
let $$n = \text{The } e.\ e\in G \wedge (\forall x\in G.\ e\cdot x = x \wedge x\cdot e = x)$$
have $$1 = \text{ TheNeutralElement}(G,A)$$
then have $$1 = n$$ unfolding TheNeutralElement_def
moreover
have $$n\in G \wedge (\forall x\in G.\ n\cdot x = x \wedge x\cdot n = x)$$ using neut_uniq_loop , theI
ultimately show $$1 \in G$$ and $$\forall x\in G.\ 1 \cdot x = x \wedge x\cdot 1 = x$$
qed

Every element of a loop has unique left and right inverse (which need not be the same). Here we define the left inverse as a function on $$G$$.

Definition

$$\text{LeftInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle y,x\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\}$$

Definition of the right inverse as a function on $$G$$:

Definition

$$\text{RightInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle x,y\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\}$$

In a loop $$G$$ right and left inverses are functions on $$G$$.

lemma (in loop0) lr_inv_fun:

shows $$\text{LeftInv}(G,A):G\rightarrow G$$, $$\text{RightInv}(G,A):G\rightarrow G$$ unfolding LeftInv_def , RightInv_def using neut_props_loop , lrdiv_props(1,4) , ZF1_1_L9 , ZF_fun_from_total

Right and left inverses have desired properties.

lemma (in loop0) lr_inv_props:

assumes $$x\in G$$

shows $$\text{LeftInv}(G,A)(x) \in G$$, $$( \text{LeftInv}(G,A)(x))\cdot x = 1$$, $$\text{RightInv}(G,A)(x) \in G$$, $$x\cdot ( \text{RightInv}(G,A)(x)) = 1$$proof
from assms show $$\text{LeftInv}(G,A)(x) \in G$$ and $$\text{RightInv}(G,A)(x) \in G$$ using lr_inv_fun , apply_funtype
from assms have $$\exists !y.\ y\in G \wedge y\cdot x = 1$$ using neut_props_loop(1) , lrdiv_props(1)
then have $$(\bigcup \{y\in G.\ y\cdot x = 1 \})\cdot x = 1$$ by (rule ZF1_1_L9 )
with assms show $$( \text{LeftInv}(G,A)(x))\cdot x = 1$$ using lr_inv_fun(1) , ZF_fun_from_tot_val unfolding LeftInv_def
from assms have $$\exists !y.\ y\in G \wedge x\cdot y = 1$$ using neut_props_loop(1) , lrdiv_props(4)
then have $$x\cdot (\bigcup \{y\in G.\ x\cdot y = 1 \}) = 1$$ by (rule ZF1_1_L9 )
with assms show $$x\cdot ( \text{RightInv}(G,A)(x)) = 1$$ using lr_inv_fun(2) , ZF_fun_from_tot_val unfolding RightInv_def
qed
end
Definition of IsAloop: $$\text{IsAloop}(G,A) \equiv \text{IsAquasigroup}(G,A) \wedge (\exists e\in G.\ \forall x\in G.\ A\langle e,x\rangle = x \wedge A\langle x,e\rangle = x)$$
Definition of TheNeutralElement: $$\text{ TheNeutralElement}(G,f) \equiv$$ $$( \text{The } e.\ e\in G \wedge (\forall g\in G.\ f\langle e,g\rangle = g \wedge f\langle g,e\rangle = g))$$
lemma (in loop0) neut_uniq_loop: shows $$\exists !e.\ e\in G \wedge (\forall x\in G.\ e\cdot x = x \wedge x\cdot e = x)$$
Definition of LeftInv: $$\text{LeftInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle y,x\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\}$$
Definition of RightInv: $$\text{RightInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle x,y\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\}$$
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 ZF1_1_L9:

assumes $$\exists ! x.\ x\in A \wedge \phi (x)$$

shows $$\exists a.\ \{x\in A.\ \phi (x)\} = \{a\}$$, $$\bigcup \{x\in A.\ \phi (x)\} \in A$$, $$\phi (\bigcup \{x\in A.\ \phi (x)\})$$
lemma ZF_fun_from_total:

assumes $$\forall x\in X.\ b(x) \in Y$$

shows $$\{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y$$
lemma (in loop0) lr_inv_fun: shows $$\text{LeftInv}(G,A):G\rightarrow G$$, $$\text{RightInv}(G,A):G\rightarrow G$$
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) lr_inv_fun: shows $$\text{LeftInv}(G,A):G\rightarrow G$$, $$\text{RightInv}(G,A):G\rightarrow G$$
lemma ZF_fun_from_tot_val:

assumes $$f:X\rightarrow Y$$, $$x\in X$$ and $$f = \{\langle x,b(x)\rangle .\ x\in X\}$$

shows $$f(x) = b(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) lr_inv_fun: shows $$\text{LeftInv}(G,A):G\rightarrow G$$, $$\text{RightInv}(G,A):G\rightarrow G$$
18
23
3
3