IsarMathLib

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

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_fun, 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_fun, 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_fun, 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

Translation by neutral element does not move sets.

lemma (in group0) trans_neutral_image:

assumes \( V\subseteq G \)

shows \( \text{RightTranslation}(G,P,1 )(V) = V \) and \( \text{LeftTranslation}(G,P,1 )(V) = V \) using assms, trans_neutral, image_id_same

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_fun, fix_2nd_var_fun
moreover
from assms have \( \forall a\in G.\ T(a) = F(a) \) using group0_5_L2, group_oper_fun, 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_fun, fix_1st_var_fun
moreover
from assms have \( \forall a\in G.\ T(a) = F(a) \) using group0_5_L2, group_oper_fun, fix_var_val
ultimately show \( T = F \) by (rule func_eq )
qed

A lemma demonstrating what is the left translation of a set

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 lemma demonstrating what is the right translation of a set

lemma (in group0) rtrans_image:

assumes A1: \( V\subseteq G \) and A2: \( x\in G \)

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

Right and left translations of a set are subsets of the group. Interestingly, we do not have to assume the set is a subset of the group.

lemma (in group0) lrtrans_in_group:

assumes \( x\in G \)

shows \( \text{LeftTranslation}(G,P,x)(V) \subseteq G \) and \( \text{RightTranslation}(G,P,x)(V) \subseteq G \)proof
from assms have \( \text{LeftTranslation}(G,P,x):G\rightarrow G \) and \( \text{RightTranslation}(G,P,x):G\rightarrow G \) using group0_5_L1
then show \( \text{LeftTranslation}(G,P,x)(V) \subseteq G \) and \( \text{RightTranslation}(G,P,x)(V) \subseteq G \) using func1_1_L6(2)
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 left 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_fun, 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

The right translation version of image_ltrans_union The proof follows the same schema.

lemma (in group0) image_rtrans_union:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( (P \text{ lifted to subsets of } G)\langle A,B\rangle = (\bigcup b\in B.\ \text{RightTranslation}(G,P,b)(A)) \)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_fun, 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.\ a\in A\} \)
moreover
from assms, \( b\in B \) have \( \text{RightTranslation}(G,P,b)(A) = \{a\cdot b.\ a\in A\} \) using rtrans_image
ultimately have \( c \in \text{RightTranslation}(G,P,b)(A) \)
with \( b\in B \) have \( c \in (\bigcup b\in B.\ \text{RightTranslation}(G,P,b)(A)) \)
}
thus \( (P \text{ lifted to subsets of } G)\langle A,B\rangle \subseteq (\bigcup b\in B.\ \text{RightTranslation}(G,P,b)(A)) \)
{
fix \( c \)
assume \( c \in (\bigcup b\in B.\ \text{RightTranslation}(G,P,b)(A)) \)
then obtain \( b \) where \( b\in B \) and \( c \in \text{RightTranslation}(G,P,b)(A) \)
moreover
from assms, \( b\in B \) have \( \text{RightTranslation}(G,P,b)(A) = \{a\cdot b.\ a\in A\} \) using rtrans_image
ultimately obtain \( a \) where \( a\in A \) and \( c = a\cdot b \)
with I, \( b\in B \) have \( c \in (P \text{ lifted to subsets of } G)\langle A,B\rangle \)
}
thus \( (\bigcup b\in B.\ \text{RightTranslation}(G,P,b)(A)) \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) \), \( g \in \text{RightTranslation}(G,P,g)(A) \)proof
from assms have \( g\cdot 1 \in \text{LeftTranslation}(G,P,g)(A) \) using ltrans_image
with A1 show \( g \in \text{LeftTranslation}(G,P,g)(A) \) using group0_2_L2
from assms have \( 1 \cdot g \in \text{RightTranslation}(G,P,g)(A) \) using rtrans_image
with A1 show \( g \in \text{RightTranslation}(G,P,g)(A) \) 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) \), \( 1 \in \text{RightTranslation}(G,P,g^{-1})(A) \)proof
from assms have ginv: \( 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 \( 1 \in \text{LeftTranslation}(G,P,g^{-1})(A) \)
from ginv, assms have \( g\cdot g^{-1} \in \text{RightTranslation}(G,P,g^{-1})(A) \) using rtrans_image
moreover
from assms have \( g\cdot g^{-1} = 1 \) using group0_2_L6
ultimately show \( 1 \in \text{RightTranslation}(G,P,g^{-1})(A) \)
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

Subgroups and interval arithmetic

The section Binary operations in the func_ZF theory defines the notion of "lifting operation to subsets". In short, every binary operation \(f:X\times X \longrightarrow X \) on a set \(X\) defines an operation on the subsets of \(X\) defined by \(F(A,B) = \{ f\langle x,y \rangle | x\in A, y\in B\}\). In the group context using multiplicative notation we can write this as \(H\cdot K = \{ x\cdot y | x\in A, y\in B\}\). Similarly we can define \(H^{-1}=\{ x^{-1} | x\in H\}\). In this section we study properties of these derived operations and how they relate to the concept of subgroups.

The next locale extends the groups0 locale with notation related to interval arithmetics.

locale group4 = group0 +

defines \( A\cdot B \equiv (P \text{ lifted to subsets of } G)\langle A,B\rangle \)

defines \( A^{-1} \equiv \text{GroupInv}(G,P)(A) \)

The next lemma shows a somewhat more explicit way of defining the product of two subsets of a group.

lemma (in group4) interval_prod:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( A\cdot B = \{x\cdot y.\ \langle x,y\rangle \in A\times B\} \) using assms, group_oper_fun, lift_subsets_explained

Product of elements of subsets of the group is in the set product of those subsets

lemma (in group4) interval_prod_el:

assumes \( A\subseteq G \), \( B\subseteq G \), \( x\in A \), \( y\in B \)

shows \( x\cdot y \in A\cdot B \) using assms, interval_prod

An alternative definition of a group inverse of a set.

lemma (in group4) interval_inv:

assumes \( A\subseteq G \)

shows \( A^{-1} = \{x^{-1}.\ x\in A\} \)proof
from groupAssum have \( \text{GroupInv}(G,P):G\rightarrow G \) using group0_2_T2
with assms show \( A^{-1} = \{x^{-1}.\ x\in A\} \) using func_imagedef
qed

Group inverse of a set is a subset of the group. Interestingly we don't need to assume the set is a subset of the group.

lemma (in group4) interval_inv_cl:

shows \( A^{-1} \subseteq G \)proof
from groupAssum have \( \text{GroupInv}(G,P):G\rightarrow G \) using group0_2_T2
then show \( A^{-1} \subseteq G \) using func1_1_L6(2)
qed

The product of two subsets of a group is a subset of the group.

lemma (in group4) interval_prod_closed:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( A\cdot B \subseteq G \)proof
fix \( z \)
assume \( z \in A\cdot B \)
with assms obtain \( x \) \( y \) where \( x\in A \), \( y\in B \), \( z=x\cdot y \) using interval_prod
with assms show \( z\in G \) using group_op_closed
qed

The product of sets operation is associative.

lemma (in group4) interval_prod_assoc:

assumes \( A\subseteq G \), \( B\subseteq G \), \( C\subseteq G \)

shows \( A\cdot B\cdot C = A\cdot (B\cdot C) \)proof
from groupAssum have \( (P \text{ lifted to subsets of } G) \text{ is associative on } Pow(G) \) unfolding IsAgroup_def, IsAmonoid_def using lift_subset_assoc
with assms show \( thesis \) unfolding IsAssociative_def
qed

A simple rearrangement following from associativity of the product of sets operation.

lemma (in group4) interval_prod_rearr1:

assumes \( A\subseteq G \), \( B\subseteq G \), \( C\subseteq G \), \( D\subseteq G \)

shows \( A\cdot B\cdot (C\cdot D) = A\cdot (B\cdot C)\cdot D \)proof
from assms(1,2) have \( A\cdot B \subseteq G \) using interval_prod_closed
with assms(3,4) have \( A\cdot B\cdot (C\cdot D) = A\cdot B\cdot C\cdot D \) using interval_prod_assoc
also
from assms(1,2,3) have \( A\cdot B\cdot C\cdot D = A\cdot (B\cdot C)\cdot D \) using interval_prod_assoc
finally show \( thesis \)
qed

A subset \(A\) of the group is closed with respect to the group operation iff \(A\cdot A \subseteq A\).

lemma (in group4) subset_gr_op_cl:

assumes \( A\subseteq G \)

shows \( (A \text{ is closed under } P) \longleftrightarrow A\cdot A \subseteq A \)proof
assume \( A \text{ is closed under } P \)
{
fix \( z \)
assume \( z \in A\cdot A \)
with assms obtain \( x \) \( y \) where \( x\in A \), \( y\in A \) and \( z=x\cdot y \) using interval_prod
with \( A \text{ is closed under } P \) have \( z\in A \) unfolding IsOpClosed_def
}
thus \( A\cdot A \subseteq A \)
next
assume \( A\cdot A \subseteq A \)
{
fix \( x \) \( y \)
assume \( x\in A \), \( y\in A \)
with assms have \( x\cdot y \in A\cdot A \) using interval_prod
with \( A\cdot A \subseteq A \) have \( x\cdot y \in A \)
}
then show \( A \text{ is closed under } P \) unfolding IsOpClosed_def
qed

Inverse and square of a subgroup is this subgroup.

lemma (in group4) subgroup_inv_sq:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( H^{-1} = H \) and \( H\cdot H = H \)proof
from assms have \( H\subseteq G \) using group0_3_L2
with assms show \( H^{-1} \subseteq H \) using interval_inv, group0_3_T3A
{
fix \( x \)
assume \( x\in H \)
with assms have \( (x^{-1})^{-1} \in \{y^{-1}.\ y\in H\} \) using group0_3_T3A
moreover
from \( x\in H \), \( H\subseteq G \) have \( (x^{-1})^{-1} = x \) using group_inv_of_inv
ultimately have \( x \in \{y^{-1}.\ y\in H\} \)
with \( H\subseteq G \) have \( x \in H^{-1} \) using interval_inv
}
thus \( H \subseteq H^{-1} \)
from assms have \( H \text{ is closed under } P \) using group0_3_L6 unfolding IsOpClosed_def
with assms have \( H\cdot H \subseteq H \) using subset_gr_op_cl, group0_3_L2
moreover {
fix \( x \)
assume \( x\in H \)
with assms have \( x\in G \) using group0_3_L2
from assms, \( H\subseteq G \), \( x\in H \) have \( x\cdot 1 \in H\cdot H \) using group0_3_L5, interval_prod
with \( x\in G \) have \( x \in H\cdot H \) using group0_2_L2
}
hence \( H \subseteq H\cdot H \)
ultimately show \( H\cdot H = H \)
qed

Inverse of a product two sets is a product of inverses with the reversed order.

lemma (in group4) interval_prod_inv:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( (A\cdot B)^{-1} = \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \), \( (A\cdot B)^{-1} = \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \), \( (A\cdot B)^{-1} = (B^{-1})\cdot (A^{-1}) \)proof
from assms have \( (A\cdot B) \subseteq G \) using interval_prod_closed
then have I: \( (A\cdot B)^{-1} = \{z^{-1}.\ z\in A\cdot B\} \) using interval_inv
show II: \( (A\cdot B)^{-1} = \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)proof
{
fix \( p \)
assume \( p \in (A\cdot B)^{-1} \)
with I obtain \( z \) where \( p=z^{-1} \) and \( z\in A\cdot B \)
with assms obtain \( x \) \( y \) where \( \langle x,y\rangle \in A\times B \) and \( z=x\cdot y \) using interval_prod
with \( p=z^{-1} \) have \( p\in \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)
}
thus \( (A\cdot B)^{-1} \subseteq \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)
{
fix \( p \)
assume \( p\in \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)
then obtain \( x \) \( y \) where \( x\in A \), \( y\in B \) and \( p=(x\cdot y)^{-1} \)
with assms, \( (A\cdot B) \subseteq G \) have \( p\in (A\cdot B)^{-1} \) using interval_prod, interval_inv
}
thus \( \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \subseteq (A\cdot B)^{-1} \)
qed
have \( \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} = \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)proof
{
fix \( p \)
assume \( p \in \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)
then obtain \( x \) \( y \) where \( x\in A \), \( y\in B \) and \( p=(x\cdot y)^{-1} \)
with assms have \( y^{-1}\cdot x^{-1} = (x\cdot y)^{-1} \) using group_inv_of_two
with \( p=(x\cdot y)^{-1} \) have \( p = y^{-1}\cdot x^{-1} \)
with \( x\in A \), \( y\in B \) have \( p\in \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)
}
thus \( \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \subseteq \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)
{
fix \( p \)
assume \( p\in \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)
then obtain \( x \) \( y \) where \( x\in A \), \( y\in B \) and \( p=y^{-1}\cdot x^{-1} \)
with assms have \( p = (x\cdot y)^{-1} \) using group_inv_of_two
with \( x\in A \), \( y\in B \) have \( p \in \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)
}
thus \( \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \subseteq \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \)
qed
with II show III: \( (A\cdot B)^{-1} = \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)
have \( \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} = (B^{-1})\cdot (A^{-1}) \)proof
{
fix \( p \)
assume \( p\in \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)
then obtain \( x \) \( y \) where \( x\in A \), \( y\in B \) and \( p=y^{-1}\cdot x^{-1} \)
with assms have \( y^{-1} \in (B^{-1}) \) and \( x^{-1} \in (A^{-1}) \) using interval_inv
with \( p=y^{-1}\cdot x^{-1} \) have \( p \in (B^{-1})\cdot (A^{-1}) \) using interval_inv_cl, interval_prod
}
thus \( \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \subseteq (B^{-1})\cdot (A^{-1}) \)
{
fix \( p \)
assume \( p \in (B^{-1})\cdot (A^{-1}) \)
then obtain \( y \) \( x \) where \( y\in B^{-1} \), \( x\in A^{-1} \) and \( p=y\cdot x \) using interval_inv_cl, interval_prod
with assms obtain \( x_1 \) \( y_1 \) where \( x_1 \in A \), \( y_1 \in B \) and \( x=x_1^{-1} \), \( y=y_1^{-1} \) using interval_inv
with \( p=y\cdot x \) have \( p \in \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)
}
thus \( (B^{-1})\cdot (A^{-1}) \subseteq \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \)
qed
with III show \( (A\cdot B)^{-1} = (B^{-1})\cdot (A^{-1}) \)
qed

If \(H,K\) are subgroups then \(H\cdot K\) is a subgroup iff \(H\cdot K = K\cdot H\).

theorem (in group4) prod_subgr_subgr:

assumes \( \text{IsAsubgroup}(H,P) \) and \( \text{IsAsubgroup}(K,P) \)

shows \( \text{IsAsubgroup}(H\cdot K,P) \longleftrightarrow H\cdot K = K\cdot H \)proof
assume \( \text{IsAsubgroup}(H\cdot K,P) \)
then have \( (H\cdot K)^{-1} = H\cdot K \) using subgroup_inv_sq(1)
with assms show \( H\cdot K = K\cdot H \) using group0_3_L2, interval_prod_inv, subgroup_inv_sq(1)
next
from assms have \( H\subseteq G \) and \( K\subseteq G \) using group0_3_L2
have I: \( H\cdot K \neq 0 \)proof
let \( x = 1 \)
let \( y = 1 \)
from assms have \( x\cdot y \in (H\cdot K) \) using group0_3_L5, group0_3_L2, interval_prod
thus \( thesis \)
qed
from \( H\subseteq G \), \( K\subseteq G \) have II: \( H\cdot K \subseteq G \) using interval_prod_closed
assume \( H\cdot K = K\cdot H \)
have III: \( (H\cdot K)\text{ is closed under } P \)proof
have \( (H\cdot K)\cdot (H\cdot K) = H\cdot K \)proof
from \( H\subseteq G \), \( K\subseteq G \) have \( (H\cdot K)\cdot (H\cdot K) = H\cdot (K\cdot H)\cdot K \) using interval_prod_rearr1
also
from \( H\cdot K = K\cdot H \) have \( .\ .\ .\ = H\cdot (H\cdot K)\cdot K \)
also
from \( H\subseteq G \), \( K\subseteq G \) have \( .\ .\ .\ = (H\cdot H)\cdot (K\cdot K) \) using interval_prod_rearr1
also
from assms have \( .\ .\ .\ = H\cdot K \) using subgroup_inv_sq(2)
finally show \( thesis \)
qed
with \( H\cdot K \subseteq G \) show \( thesis \) using subset_gr_op_cl
qed
have IV: \( \forall x \in H\cdot K.\ x^{-1} \in H\cdot K \)proof
{
fix \( x \)
assume \( x \in H\cdot K \)
with \( H\cdot K \subseteq G \) have \( x^{-1} \in (H\cdot K)^{-1} \) using interval_inv
with assms, \( H\subseteq G \), \( K\subseteq G \), \( H\cdot K = K\cdot H \) have \( x^{-1} \in H\cdot K \) using interval_prod_inv, subgroup_inv_sq(1)
}
thus \( thesis \)
qed
from I, II, III, IV show \( \text{IsAsubgroup}(H\cdot K,P) \) using group0_3_T3
qed
end
lemma (in group0) group_oper_fun: 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) trans_neutral: shows \( \text{RightTranslation}(G,P,1 ) = id(G) \) and \( \text{LeftTranslation}(G,P,1 ) = id(G) \)
lemma image_id_same:

assumes \( A\subseteq X \)

shows \( id(X)(A) = A \)
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_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 \)
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\} \)
lemma (in group0) rtrans_image:

assumes \( V\subseteq G \) and \( x\in G \)

shows \( \text{RightTranslation}(G,P,x)(V) = \{v\cdot x.\ v\in V\} \)
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} \)
lemma (in group4) interval_prod:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( A\cdot B = \{x\cdot y.\ \langle x,y\rangle \in A\times B\} \)
Definition of IsAgroup: \( \text{IsAgroup}(G,f) \equiv \) \( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)
Definition of IsAmonoid: \( \text{IsAmonoid}(G,f) \equiv \) \( f \text{ is associative on } G \wedge \) \( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
lemma lift_subset_assoc:

assumes \( f \text{ is associative on } X \) and \( F = f \text{ lifted to subsets of } X \)

shows \( F \text{ is associative on } Pow(X) \)
Definition of IsAssociative: \( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \) \( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \) \( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
lemma (in group4) interval_prod_closed:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( A\cdot B \subseteq G \)
lemma (in group4) interval_prod_assoc:

assumes \( A\subseteq G \), \( B\subseteq G \), \( C\subseteq G \)

shows \( A\cdot B\cdot C = A\cdot (B\cdot C) \)
Definition of IsOpClosed: \( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
lemma (in group0) group0_3_L2:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( H \subseteq G \)
lemma (in group4) interval_inv:

assumes \( A\subseteq G \)

shows \( A^{-1} = \{x^{-1}.\ x\in A\} \)
theorem (in group0) group0_3_T3A:

assumes \( \text{IsAsubgroup}(H,P) \) and \( h\in H \)

shows \( h^{-1}\in H \)
lemma (in group0) group0_3_L6:

assumes \( \text{IsAsubgroup}(H,P) \) and \( a\in H \), \( b\in H \)

shows \( a\cdot b \in H \)
lemma (in group4) subset_gr_op_cl:

assumes \( A\subseteq G \)

shows \( (A \text{ is closed under } P) \longleftrightarrow A\cdot A \subseteq A \)
lemma (in group0) group0_3_L5:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( 1 \in H \)
lemma (in group0) group_inv_of_two:

assumes \( a\in G \) and \( b\in G \)

shows \( b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} \)
lemma (in group4) interval_inv_cl: shows \( A^{-1} \subseteq G \)
lemma (in group4) subgroup_inv_sq:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( H^{-1} = H \) and \( H\cdot H = H \)
lemma (in group4) interval_prod_inv:

assumes \( A\subseteq G \), \( B\subseteq G \)

shows \( (A\cdot B)^{-1} = \{(x\cdot y)^{-1}.\ \langle x,y\rangle \in A\times B\} \), \( (A\cdot B)^{-1} = \{y^{-1}\cdot x^{-1}.\ \langle x,y\rangle \in A\times B\} \), \( (A\cdot B)^{-1} = (B^{-1})\cdot (A^{-1}) \)
lemma (in group4) interval_prod_rearr1:

assumes \( A\subseteq G \), \( B\subseteq G \), \( C\subseteq G \), \( D\subseteq G \)

shows \( A\cdot B\cdot (C\cdot D) = A\cdot (B\cdot C)\cdot D \)
lemma (in group4) subgroup_inv_sq:

assumes \( \text{IsAsubgroup}(H,P) \)

shows \( H^{-1} = H \) and \( H\cdot H = H \)
theorem (in group0) group0_3_T3:

assumes \( H\neq 0 \) and \( H\subseteq G \) and \( H \text{ is closed under } P \) and \( \forall x\in H.\ x^{-1} \in H \)

shows \( \text{IsAsubgroup}(H,P) \)