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_L11BComposition 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
qed
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 )
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_neutralTranslations 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
qed
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
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_converseAnother 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
qed
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 )
A lemma about translating sets.
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
qed
from assms have \( \forall v\in V.\ \text{LeftTranslation}(G,P,x)(v) = x\cdot v \) using group0_5_L2
ultimately show \( thesis \)
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
qed
from assms have \( g^{-1}\cdot g = 1 \) using group0_2_L6
ultimately show \( thesis \)
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_defWe 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} \)
This page by Slawomir Kolodynski is licensed under a Creative Commons Attribution 3.0 License. BTC: 1JzFajFtGwiKiRHbZyCB1KtASgsM1kFU2h