IsarMathLib

A library of formalized mathematics for Isabelle/ZF theorem proving environment

theory Group_ZF_1 imports Group_ZF
begin

In this theory we consider right and left translations and odd functions.

Translations

In this section we consider translations. Translations are maps $$T: G\rightarrow G$$ of the form $$T_g (a) = g\cdot a$$ or $$T_g (a) = a\cdot g$$. We also consider two-dimensional translations $$T_g : G\times G \rightarrow G\times G$$, where $$T_g(a,b) = (a\cdot g, b\cdot g)$$ or $$T_g(a,b) = (g\cdot a, g\cdot b)$$.

For an element $$a\in G$$ the right translation is defined a function (set of pairs) such that its value (the second element of a pair) is the value of the group operation on the first element of the pair and $$g$$. This looks a bit strange in the raw set notation, when we write a function explicitely as a set of pairs and value of the group operation on the pair $$\langle a,b \rangle$$ as $$P\langle a,b\rangle$$ instead of the usual infix $$a\cdot b$$ or $$a + b$$.

Definition

$$\text{RightTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle a,g\rangle = b\}$$

A similar definition of the left translation.

Definition

$$\text{LeftTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle g,a\rangle = b\}$$

Translations map $$G$$ into $$G$$. Two dimensional translations map $$G\times G$$ into itself.

lemma (in group0) group0_5_L1:

assumes A1: $$g\in G$$

shows $$\text{RightTranslation}(G,P,g) : G\rightarrow G$$ and $$\text{LeftTranslation}(G,P,g) : G\rightarrow G$$proof
from A1 have $$\forall a\in G.\ a\cdot g \in G$$ and $$\forall a\in G.\ g\cdot a \in G$$ using group_oper_assocA , apply_funtype
then show $$\text{RightTranslation}(G,P,g) : G\rightarrow G$$, $$\text{LeftTranslation}(G,P,g) : G\rightarrow G$$ using RightTranslation_def , LeftTranslation_def , func1_1_L11A
qed

The values of the translations are what we expect.

lemma (in group0) group0_5_L2:

assumes $$g\in G$$, $$a\in G$$

shows $$\text{RightTranslation}(G,P,g)(a) = a\cdot g$$, $$\text{LeftTranslation}(G,P,g)(a) = g\cdot a$$ using assms , group0_5_L1 , RightTranslation_def , LeftTranslation_def , func1_1_L11B

Composition of left translations is a left translation by the product.

lemma (in group0) group0_5_L4:

assumes A1: $$g\in G$$, $$h\in G$$, $$a\in G$$ and A2: $$T_g = \text{LeftTranslation}(G,P,g)$$, $$T_h = \text{LeftTranslation}(G,P,h)$$

shows $$T_g(T_h(a)) = g\cdot h\cdot a$$, $$T_g(T_h(a)) = \text{LeftTranslation}(G,P,g\cdot h)(a)$$proof
from A1 have I: $$h\cdot a\in G$$, $$g\cdot h\in G$$ using group_oper_assocA , apply_funtype
with A1, A2 show $$T_g(T_h(a)) = g\cdot h\cdot a$$ using group0_5_L2 , group_oper_assoc
with A1, A2, I show $$T_g(T_h(a)) = \text{LeftTranslation}(G,P,g\cdot h)(a)$$ using group0_5_L2 , group_oper_assoc
qed

Composition of right translations is a right translation by the product.

lemma (in group0) group0_5_L5:

assumes A1: $$g\in G$$, $$h\in G$$, $$a\in G$$ and A2: $$T_g = \text{RightTranslation}(G,P,g)$$, $$T_h = \text{RightTranslation}(G,P,h)$$

shows $$T_g(T_h(a)) = a\cdot h\cdot g$$, $$T_g(T_h(a)) = \text{RightTranslation}(G,P,h\cdot g)(a)$$proof
from A1 have I: $$a\cdot h\in G$$, $$h\cdot g \in G$$ using group_oper_assocA , apply_funtype
with A1, A2 show $$T_g(T_h(a)) = a\cdot h\cdot g$$ using group0_5_L2 , group_oper_assoc
with A1, A2, I show $$T_g(T_h(a)) = \text{RightTranslation}(G,P,h\cdot g)(a)$$ using group0_5_L2 , group_oper_assoc
qed

Point free version of group0_5_L4 and group0_5_L5.

lemma (in group0) trans_comp:

assumes $$g\in G$$, $$h\in G$$

shows $$\text{RightTranslation}(G,P,g)\circ \text{RightTranslation}(G,P,h) = \text{RightTranslation}(G,P,h\cdot g)$$, $$\text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,h) = \text{LeftTranslation}(G,P,g\cdot h)$$proof
let $$T_g = \text{RightTranslation}(G,P,g)$$
let $$T_h = \text{RightTranslation}(G,P,h)$$
from assms have $$T_g:G\rightarrow G$$ and $$T_h:G\rightarrow G$$ using group0_5_L1
then have $$T_g\circ T_h:G\rightarrow G$$ using comp_fun
moreover
from assms have $$\text{RightTranslation}(G,P,h\cdot g):G\rightarrow G$$ using group_op_closed , group0_5_L1
moreover
from assms, $$T_h:G\rightarrow G$$ have $$\forall a\in G.\ (T_g\circ T_h)(a) = \text{RightTranslation}(G,P,h\cdot g)(a)$$ using comp_fun_apply , group0_5_L5
ultimately show $$T_g\circ T_h = \text{RightTranslation}(G,P,h\cdot g)$$ by (rule func_eq )
next
let $$T_g = \text{LeftTranslation}(G,P,g)$$
let $$T_h = \text{LeftTranslation}(G,P,h)$$
from assms have $$T_g:G\rightarrow G$$ and $$T_h:G\rightarrow G$$ using group0_5_L1
then have $$T_g\circ T_h:G\rightarrow G$$ using comp_fun
moreover
from assms have $$\text{LeftTranslation}(G,P,g\cdot h):G\rightarrow G$$ using group_op_closed , group0_5_L1
moreover
from assms, $$T_h:G\rightarrow G$$ have $$\forall a\in G.\ (T_g\circ T_h)(a) = \text{LeftTranslation}(G,P,g\cdot h)(a)$$ using comp_fun_apply , group0_5_L4
ultimately show $$T_g\circ T_h = \text{LeftTranslation}(G,P,g\cdot h)$$ by (rule func_eq )
qed

The image of a set under a composition of translations is the same as the image under translation by a product.

lemma (in group0) trans_comp_image:

assumes A1: $$g\in G$$, $$h\in G$$ and A2: $$T_g = \text{LeftTranslation}(G,P,g)$$, $$T_h = \text{LeftTranslation}(G,P,h)$$

shows $$T_g(T_h(A)) = \text{LeftTranslation}(G,P,g\cdot h)(A)$$proof
from A2 have $$T_g(T_h(A)) = (T_g\circ T_h)(A)$$ using image_comp
with assms show $$thesis$$ using trans_comp
qed

Another form of the image of a set under a composition of translations

lemma (in group0) group0_5_L6:

assumes A1: $$g\in G$$, $$h\in G$$ and A2: $$A\subseteq G$$ and A3: $$T_g = \text{RightTranslation}(G,P,g)$$, $$T_h = \text{RightTranslation}(G,P,h)$$

shows $$T_g(T_h(A)) = \{a\cdot h\cdot g.\ a\in A\}$$proof
from A2 have $$\forall a\in A.\ a\in G$$
from A1, A3 have $$T_g : G\rightarrow G$$, $$T_h : G\rightarrow G$$ using group0_5_L1
with assms, $$\forall a\in A.\ a\in G$$ show $$T_g(T_h(A)) = \{a\cdot h\cdot g.\ a\in A\}$$ using func1_1_L15C , group0_5_L5
qed

The translation by neutral element is the identity on group.

lemma (in group0) trans_neutral:

shows $$\text{RightTranslation}(G,P,1 ) = id(G)$$ and $$\text{LeftTranslation}(G,P,1 ) = id(G)$$proof
have $$\text{RightTranslation}(G,P,1 ):G\rightarrow G$$ and $$\forall a\in G.\ \text{RightTranslation}(G,P,1 )(a) = a$$ using group0_2_L2 , group0_5_L1 , group0_5_L2
then show $$\text{RightTranslation}(G,P,1 ) = id(G)$$ by (rule indentity_fun )
have $$\text{LeftTranslation}(G,P,1 ):G\rightarrow G$$ and $$\forall a\in G.\ \text{LeftTranslation}(G,P,1 )(a) = a$$ using group0_2_L2 , group0_5_L1 , group0_5_L2
then show $$\text{LeftTranslation}(G,P,1 ) = id(G)$$ by (rule indentity_fun )
qed

Composition of translations by an element and its inverse is identity.

lemma (in group0) trans_comp_id:

assumes $$g\in G$$

shows $$\text{RightTranslation}(G,P,g)\circ \text{RightTranslation}(G,P,g^{-1}) = id(G)$$ and $$\text{RightTranslation}(G,P,g^{-1})\circ \text{RightTranslation}(G,P,g) = id(G)$$ and $$\text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,g^{-1}) = id(G)$$ and $$\text{LeftTranslation}(G,P,g^{-1})\circ \text{LeftTranslation}(G,P,g) = id(G)$$ using assms , inverse_in_group , trans_comp , group0_2_L6 , trans_neutral

Translations are bijective.

lemma (in group0) trans_bij:

assumes $$g\in G$$

shows $$\text{RightTranslation}(G,P,g) \in \text{bij}(G,G)$$ and $$\text{LeftTranslation}(G,P,g) \in \text{bij}(G,G)$$proof
from assms have $$\text{RightTranslation}(G,P,g):G\rightarrow G$$ and $$\text{RightTranslation}(G,P,g^{-1}):G\rightarrow G$$ and $$\text{RightTranslation}(G,P,g)\circ \text{RightTranslation}(G,P,g^{-1}) = id(G)$$, $$\text{RightTranslation}(G,P,g^{-1})\circ \text{RightTranslation}(G,P,g) = id(G)$$ using inverse_in_group , group0_5_L1 , trans_comp_id
then show $$\text{RightTranslation}(G,P,g) \in \text{bij}(G,G)$$ using fg_imp_bijective
from assms have $$\text{LeftTranslation}(G,P,g):G\rightarrow G$$ and $$\text{LeftTranslation}(G,P,g^{-1}):G\rightarrow G$$ and $$\text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,g^{-1}) = id(G)$$, $$\text{LeftTranslation}(G,P,g^{-1})\circ \text{LeftTranslation}(G,P,g) = id(G)$$ using inverse_in_group , group0_5_L1 , trans_comp_id
then show $$\text{LeftTranslation}(G,P,g) \in \text{bij}(G,G)$$ using fg_imp_bijective
qed

Converse of a translation is translation by the inverse.

lemma (in group0) trans_conv_inv:

assumes $$g\in G$$

shows $$converse( \text{RightTranslation}(G,P,g)) = \text{RightTranslation}(G,P,g^{-1})$$ and $$converse( \text{LeftTranslation}(G,P,g)) = \text{LeftTranslation}(G,P,g^{-1})$$ and $$\text{LeftTranslation}(G,P,g) = converse( \text{LeftTranslation}(G,P,g^{-1}))$$ and $$\text{RightTranslation}(G,P,g) = converse( \text{RightTranslation}(G,P,g^{-1}))$$proof
from assms have $$\text{RightTranslation}(G,P,g) \in \text{bij}(G,G)$$, $$\text{RightTranslation}(G,P,g^{-1}) \in \text{bij}(G,G)$$ and $$\text{LeftTranslation}(G,P,g) \in \text{bij}(G,G)$$, $$\text{LeftTranslation}(G,P,g^{-1}) \in \text{bij}(G,G)$$ using trans_bij , inverse_in_group
moreover
from assms have $$\text{RightTranslation}(G,P,g^{-1})\circ \text{RightTranslation}(G,P,g) = id(G)$$ and $$\text{LeftTranslation}(G,P,g^{-1})\circ \text{LeftTranslation}(G,P,g) = id(G)$$ and $$\text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,g^{-1}) = id(G)$$ and $$\text{LeftTranslation}(G,P,g^{-1})\circ \text{LeftTranslation}(G,P,g) = id(G)$$ using trans_comp_id
ultimately show $$converse( \text{RightTranslation}(G,P,g)) = \text{RightTranslation}(G,P,g^{-1})$$ and $$converse( \text{LeftTranslation}(G,P,g)) = \text{LeftTranslation}(G,P,g^{-1})$$ and $$\text{LeftTranslation}(G,P,g) = converse( \text{LeftTranslation}(G,P,g^{-1}))$$ and $$\text{RightTranslation}(G,P,g) = converse( \text{RightTranslation}(G,P,g^{-1}))$$ using comp_id_conv
qed

The image of a set by translation is the same as the inverse image by by the inverse element translation.

lemma (in group0) trans_image_vimage:

assumes $$g\in G$$

shows $$\text{LeftTranslation}(G,P,g)(A) = \text{LeftTranslation}(G,P,g^{-1})^{-1}(A)$$ and $$\text{RightTranslation}(G,P,g)(A) = \text{RightTranslation}(G,P,g^{-1})^{-1}(A)$$ using assms , trans_conv_inv , vimage_converse

Another way of looking at translations is that they are sections of the group operation.

lemma (in group0) trans_eq_section:

assumes $$g\in G$$

shows $$\text{RightTranslation}(G,P,g) = \text{Fix2ndVar}(P,g)$$ and $$\text{LeftTranslation}(G,P,g) = \text{Fix1stVar}(P,g)$$proof
let $$T = \text{RightTranslation}(G,P,g)$$
let $$F = \text{Fix2ndVar}(P,g)$$
from assms have $$T: G\rightarrow G$$ and $$F: G\rightarrow G$$ using group0_5_L1 , group_oper_assocA , fix_2nd_var_fun
moreover
from assms have $$\forall a\in G.\ T(a) = F(a)$$ using group0_5_L2 , group_oper_assocA , fix_var_val
ultimately show $$T = F$$ by (rule func_eq )
next
let $$T = \text{LeftTranslation}(G,P,g)$$
let $$F = \text{Fix1stVar}(P,g)$$
from assms have $$T: G\rightarrow G$$ and $$F: G\rightarrow G$$ using group0_5_L1 , group_oper_assocA , fix_1st_var_fun
moreover
from assms have $$\forall a\in G.\ T(a) = F(a)$$ using group0_5_L2 , group_oper_assocA , fix_var_val
ultimately show $$T = F$$ by (rule func_eq )
qed

lemma (in group0) ltrans_image:

assumes A1: $$V\subseteq G$$ and A2: $$x\in G$$

shows $$\text{LeftTranslation}(G,P,x)(V) = \{x\cdot v.\ v\in V\}$$proof
from assms have $$\text{LeftTranslation}(G,P,x)(V) = \{ \text{LeftTranslation}(G,P,x)(v).\ v\in V\}$$ using group0_5_L1 , func_imagedef
moreover
from assms have $$\forall v\in V.\ \text{LeftTranslation}(G,P,x)(v) = x\cdot v$$ using group0_5_L2
ultimately show $$thesis$$
qed

A technical lemma about solving equations with translations.

lemma (in group0) ltrans_inv_in:

assumes A1: $$V\subseteq G$$ and A2: $$y\in G$$ and A3: $$x \in \text{LeftTranslation}(G,P,y)( \text{GroupInv}(G,P)(V))$$

shows $$y \in \text{LeftTranslation}(G,P,x)(V)$$proof
have $$x\in G$$proof
from A2 have $$\text{LeftTranslation}(G,P,y):G\rightarrow G$$ using group0_5_L1
then have $$\text{LeftTranslation}(G,P,y)( \text{GroupInv}(G,P)(V)) \subseteq G$$ using func1_1_L6
with A3 show $$x\in G$$
qed
have $$\exists v\in V.\ x = y\cdot v^{-1}$$proof
have $$\text{GroupInv}(G,P): G\rightarrow G$$ using groupAssum , group0_2_T2
with assms obtain $$z$$ where $$z \in \text{GroupInv}(G,P)(V)$$ and $$x = y\cdot z$$ using func1_1_L6 , ltrans_image
with A1, $$\text{GroupInv}(G,P): G\rightarrow G$$ show $$thesis$$ using func_imagedef
qed
then obtain $$v$$ where $$v\in V$$ and $$x = y\cdot v^{-1}$$
with A1, A2 have $$y = x\cdot v$$ using inv_cancel_two
with assms, $$x\in G$$, $$v\in V$$ show $$thesis$$ using ltrans_image
qed

We can look at the result of interval arithmetic operation as union of translated sets.

lemma (in group0) image_ltrans_union:

assumes $$A\subseteq G$$, $$B\subseteq G$$

shows $$(P \text{ lifted to subsets of } G)\langle A,B\rangle = (\bigcup a\in A.\ \text{LeftTranslation}(G,P,a)(B))$$proof
from assms have I: $$(P \text{ lifted to subsets of } G)\langle A,B\rangle = \{a\cdot b .\ \langle a,b\rangle \in A\times B\}$$ using group_oper_assocA , lift_subsets_explained
{
fix $$c$$
assume $$c \in (P \text{ lifted to subsets of } G)\langle A,B\rangle$$
with I obtain $$a$$ $$b$$ where $$c = a\cdot b$$ and $$a\in A$$, $$b\in B$$
hence $$c \in \{a\cdot b.\ b\in B\}$$
moreover
from assms, $$a\in A$$ have $$\text{LeftTranslation}(G,P,a)(B) = \{a\cdot b.\ b\in B\}$$ using ltrans_image
ultimately have $$c \in \text{LeftTranslation}(G,P,a)(B)$$
with $$a\in A$$ have $$c \in (\bigcup a\in A.\ \text{LeftTranslation}(G,P,a)(B))$$
}
thus $$(P \text{ lifted to subsets of } G)\langle A,B\rangle \subseteq (\bigcup a\in A.\ \text{LeftTranslation}(G,P,a)(B))$$
{
fix $$c$$
assume $$c \in (\bigcup a\in A.\ \text{LeftTranslation}(G,P,a)(B))$$
then obtain $$a$$ where $$a\in A$$ and $$c \in \text{LeftTranslation}(G,P,a)(B)$$
moreover
from assms, $$a\in A$$ have $$\text{LeftTranslation}(G,P,a)(B) = \{a\cdot b.\ b\in B\}$$ using ltrans_image
ultimately obtain $$b$$ where $$b\in B$$ and $$c = a\cdot b$$
with I, $$a\in A$$ have $$c \in (P \text{ lifted to subsets of } G)\langle A,B\rangle$$
}
thus $$(\bigcup a\in A.\ \text{LeftTranslation}(G,P,a)(B)) \subseteq (P \text{ lifted to subsets of } G)\langle A,B\rangle$$
qed

If the neutral element belongs to a set, then an element of group belongs the translation of that set.

lemma (in group0) neut_trans_elem:

assumes A1: $$A\subseteq G$$, $$g\in G$$ and A2: $$1 \in A$$

shows $$g \in \text{LeftTranslation}(G,P,g)(A)$$proof
from assms have $$g\cdot 1 \in \text{LeftTranslation}(G,P,g)(A)$$ using ltrans_image
with A1 show $$thesis$$ using group0_2_L2
qed

The neutral element belongs to the translation of a set by the inverse of an element that belongs to it.

lemma (in group0) elem_trans_neut:

assumes A1: $$A\subseteq G$$ and A2: $$g\in A$$

shows $$1 \in \text{LeftTranslation}(G,P,g^{-1})(A)$$proof
from assms have $$g^{-1} \in G$$ using inverse_in_group
with assms have $$g^{-1}\cdot g \in \text{LeftTranslation}(G,P,g^{-1})(A)$$ using ltrans_image
moreover
from assms have $$g^{-1}\cdot g = 1$$ using group0_2_L6
ultimately show $$thesis$$
qed

Odd functions

This section is about odd functions.

Odd functions are those that commute with the group inverse: $$f(a^{-1}) = (f(a))^{-1}.$$

Definition

$$\text{IsOdd}(G,P,f) \equiv (\forall a\in G.\ f( \text{GroupInv}(G,P)(a)) = \text{GroupInv}(G,P)(f(a)) )$$

Let's see the definition of an odd function in a more readable notation.

lemma (in group0) group0_6_L1:

shows $$\text{IsOdd}(G,P,p) \longleftrightarrow ( \forall a\in G.\ p(a^{-1}) = (p(a))^{-1} )$$ using IsOdd_def

We can express the definition of an odd function in two ways.

lemma (in group0) group0_6_L2:

assumes A1: $$p : G\rightarrow G$$

shows $$(\forall a\in G.\ p(a^{-1}) = (p(a))^{-1}) \longleftrightarrow (\forall a\in G.\ (p(a^{-1}))^{-1} = p(a))$$proof
assume $$\forall a\in G.\ p(a^{-1}) = (p(a))^{-1}$$
with A1 show $$\forall a\in G.\ (p(a^{-1}))^{-1} = p(a)$$ using apply_funtype , group_inv_of_inv
next
assume A2: $$\forall a\in G.\ (p(a^{-1}))^{-1} = p(a)$$
{
fix $$a$$
assume $$a\in G$$
with A1, A2 have $$p(a^{-1}) \in G$$ and $$((p(a^{-1}))^{-1})^{-1} = (p(a))^{-1}$$ using apply_funtype , inverse_in_group
then have $$p(a^{-1}) = (p(a))^{-1}$$ using group_inv_of_inv
}
then show $$\forall a\in G.\ p(a^{-1}) = (p(a))^{-1}$$
qed
end
lemma (in group0) group_oper_assocA: shows $$P : G\times G\rightarrow G$$
Definition of RightTranslation: $$\text{RightTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle a,g\rangle = b\}$$
Definition of LeftTranslation: $$\text{LeftTranslation}(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle g,a\rangle = b\}$$
lemma func1_1_L11A:

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

shows $$\{\langle x,y\rangle \in X\times Y.\ b(x) = y\} : X\rightarrow Y$$
lemma (in group0) group0_5_L1:

assumes $$g\in G$$

shows $$\text{RightTranslation}(G,P,g) : G\rightarrow G$$ and $$\text{LeftTranslation}(G,P,g) : G\rightarrow G$$
lemma func1_1_L11B:

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

shows $$f(x) = b(x)$$
lemma (in group0) group0_5_L2:

assumes $$g\in G$$, $$a\in G$$

shows $$\text{RightTranslation}(G,P,g)(a) = a\cdot g$$, $$\text{LeftTranslation}(G,P,g)(a) = g\cdot a$$
lemma (in group0) group_oper_assoc:

assumes $$a\in G$$, $$b\in G$$, $$c\in G$$

shows $$a\cdot (b\cdot c) = a\cdot b\cdot c$$
lemma (in group0) group_op_closed:

assumes $$a\in G$$, $$b\in G$$

shows $$a\cdot b \in G$$
lemma (in group0) group0_5_L5:

assumes $$g\in G$$, $$h\in G$$, $$a\in G$$ and $$T_g = \text{RightTranslation}(G,P,g)$$, $$T_h = \text{RightTranslation}(G,P,h)$$

shows $$T_g(T_h(a)) = a\cdot h\cdot g$$, $$T_g(T_h(a)) = \text{RightTranslation}(G,P,h\cdot g)(a)$$
lemma func_eq:

assumes $$f: X\rightarrow Y$$, $$g: X\rightarrow Z$$ and $$\forall x\in X.\ f(x) = g(x)$$

shows $$f = g$$
lemma (in group0) group0_5_L4:

assumes $$g\in G$$, $$h\in G$$, $$a\in G$$ and $$T_g = \text{LeftTranslation}(G,P,g)$$, $$T_h = \text{LeftTranslation}(G,P,h)$$

shows $$T_g(T_h(a)) = g\cdot h\cdot a$$, $$T_g(T_h(a)) = \text{LeftTranslation}(G,P,g\cdot h)(a)$$
lemma (in group0) trans_comp:

assumes $$g\in G$$, $$h\in G$$

shows $$\text{RightTranslation}(G,P,g)\circ \text{RightTranslation}(G,P,h) = \text{RightTranslation}(G,P,h\cdot g)$$, $$\text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,h) = \text{LeftTranslation}(G,P,g\cdot h)$$
lemma func1_1_L15C:

assumes $$f:X\rightarrow Y$$ and $$g:Y\rightarrow Z$$ and $$A\subseteq X$$

shows $$g(f(A)) = \{g(f(x)).\ x\in A\}$$, $$g(f(A)) = (g\circ f)(A)$$
lemma (in group0) group0_2_L2: shows $$1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g))$$
lemma indentity_fun:

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

shows $$f = id(X)$$
lemma (in group0) inverse_in_group:

assumes $$x\in G$$

shows $$x^{-1}\in G$$
lemma (in group0) group0_2_L6:

assumes $$x\in G$$

shows $$x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1$$
lemma (in group0) trans_neutral: shows $$\text{RightTranslation}(G,P,1 ) = id(G)$$ and $$\text{LeftTranslation}(G,P,1 ) = id(G)$$
lemma (in group0) trans_comp_id:

assumes $$g\in G$$

shows $$\text{RightTranslation}(G,P,g)\circ \text{RightTranslation}(G,P,g^{-1}) = id(G)$$ and $$\text{RightTranslation}(G,P,g^{-1})\circ \text{RightTranslation}(G,P,g) = id(G)$$ and $$\text{LeftTranslation}(G,P,g)\circ \text{LeftTranslation}(G,P,g^{-1}) = id(G)$$ and $$\text{LeftTranslation}(G,P,g^{-1})\circ \text{LeftTranslation}(G,P,g) = id(G)$$
lemma (in group0) trans_bij:

assumes $$g\in G$$

shows $$\text{RightTranslation}(G,P,g) \in \text{bij}(G,G)$$ and $$\text{LeftTranslation}(G,P,g) \in \text{bij}(G,G)$$
lemma comp_id_conv:

assumes $$a \in \text{bij}(A,B)$$, $$b \in \text{bij}(B,A)$$ and $$b\circ a = id(A)$$

shows $$a = converse(b)$$ and $$b = converse(a)$$
lemma (in group0) trans_conv_inv:

assumes $$g\in G$$

shows $$converse( \text{RightTranslation}(G,P,g)) = \text{RightTranslation}(G,P,g^{-1})$$ and $$converse( \text{LeftTranslation}(G,P,g)) = \text{LeftTranslation}(G,P,g^{-1})$$ and $$\text{LeftTranslation}(G,P,g) = converse( \text{LeftTranslation}(G,P,g^{-1}))$$ and $$\text{RightTranslation}(G,P,g) = converse( \text{RightTranslation}(G,P,g^{-1}))$$
lemma vimage_converse: shows $$r^{-1}(A) = converse(r)(A)$$
lemma fix_2nd_var_fun:

assumes $$f : X\times Y \rightarrow Z$$ and $$y\in Y$$

shows $$\text{Fix2ndVar}(f,y) : X \rightarrow Z$$
lemma fix_var_val:

assumes $$f : X\times Y \rightarrow Z$$ and $$x\in X$$, $$y\in Y$$

shows $$\text{Fix1stVar}(f,x)(y) = f\langle x,y\rangle$$, $$\text{Fix2ndVar}(f,y)(x) = f\langle x,y\rangle$$
lemma fix_1st_var_fun:

assumes $$f : X\times Y \rightarrow Z$$ and $$x\in X$$

shows $$\text{Fix1stVar}(f,x) : Y \rightarrow Z$$
lemma func_imagedef:

assumes $$f:X\rightarrow Y$$ and $$A\subseteq X$$

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

assumes $$f:X\rightarrow Y$$

shows $$f(B) \subseteq \text{range}(f)$$ and $$f(B) \subseteq Y$$
theorem group0_2_T2:

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

shows $$\text{GroupInv}(G,f) : G\rightarrow G$$
lemma (in group0) ltrans_image:

assumes $$V\subseteq G$$ and $$x\in G$$

shows $$\text{LeftTranslation}(G,P,x)(V) = \{x\cdot v.\ v\in V\}$$
lemma (in group0) inv_cancel_two:

assumes $$a\in G$$, $$b\in G$$

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

assumes $$f : X\times X \rightarrow Y$$ and $$A \subseteq X$$, $$B \subseteq X$$ and $$F = f \text{ lifted to subsets of } X$$

shows $$F\langle A,B\rangle \subseteq Y$$ and $$F\langle A,B\rangle = f(A\times B)$$, $$F\langle A,B\rangle = \{f(p).\ p \in A\times B\}$$, $$F\langle A,B\rangle = \{f\langle x,y\rangle .\ \langle x,y\rangle \in A\times B\}$$
Definition of IsOdd: $$\text{IsOdd}(G,P,f) \equiv (\forall a\in G.\ f( \text{GroupInv}(G,P)(a)) = \text{GroupInv}(G,P)(f(a)) )$$
lemma (in group0) group_inv_of_inv:

assumes $$a\in G$$

shows $$a = (a^{-1})^{-1}$$
95
94
21
21