IsarMathLib

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

theory AbelianGroup_ZF imports Group_ZF
begin

A group is called ``abelian`` if its operation is commutative, i.e. \(P\langle a,b \rangle = P\langle a,b \rangle\) for all group elements \(a,b\), where \(P\) is the group operation. It is customary to use the additive notation for abelian groups, so this condition is typically written as \(a+b = b+a\). We will be using multiplicative notation though (in which the commutativity condition of the operation is written as \(a\cdot b = b\cdot a\)), just to avoid the hassle of changing the notation we used for general groups.

Rearrangement formulae

This section is not interesting and should not be read. Here we will prove formulas is which right hand side uses the same factors as the left hand side, just in different order. These facts are obvious in informal math sense, but Isabelle prover is not able to derive them automatically, so we have to prove them by hand.

Proving the facts about associative and commutative operations is quite tedious in formalized mathematics. To a human the thing is simple: we can arrange the elements in any order and put parantheses wherever we want, it is all the same. However, formalizing this statement would be rather difficult (I think). The next lemma attempts a quasi-algorithmic approach to this type of problem. To prove that two expressions are equal, we first strip one from parantheses, then rearrange the elements in proper order, then put the parantheses where we want them to be. The algorithm for rearrangement is easy to describe: we keep putting the first element (from the right) that is in the wrong place at the left-most position until we get the proper arrangement. As far removing parantheses is concerned Isabelle does its job automatically.

lemma (in group0) group0_4_L2:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \), \( E\in G \), \( F\in G \)

shows \( (a\cdot b)\cdot (c\cdot d)\cdot (E\cdot F) = (a\cdot (d\cdot F))\cdot (b\cdot (c\cdot E)) \)proof
from A2 have \( (a\cdot b)\cdot (c\cdot d)\cdot (E\cdot F) = a\cdot b\cdot c\cdot d\cdot E\cdot F \) using group_op_closed, group_oper_assoc
also
have \( a\cdot b\cdot c\cdot d\cdot E\cdot F = a\cdot d\cdot F\cdot b\cdot c\cdot E \)proof
from A1, A2 have \( a\cdot b\cdot c\cdot d\cdot E\cdot F = F\cdot (a\cdot b\cdot c\cdot d\cdot E) \) using IsCommutative_def, group_op_closed
also
from A2 have \( F\cdot (a\cdot b\cdot c\cdot d\cdot E) = F\cdot a\cdot b\cdot c\cdot d\cdot E \) using group_op_closed, group_oper_assoc
also
from A1, A2 have \( F\cdot a\cdot b\cdot c\cdot d\cdot E = d\cdot (F\cdot a\cdot b\cdot c)\cdot E \) using IsCommutative_def, group_op_closed
also
from A2 have \( d\cdot (F\cdot a\cdot b\cdot c)\cdot E = d\cdot F\cdot a\cdot b\cdot c\cdot E \) using group_op_closed, group_oper_assoc
also
from A1, A2 have \( d\cdot F\cdot a\cdot b\cdot c\cdot E = a\cdot (d\cdot F)\cdot b\cdot c\cdot E \) using IsCommutative_def, group_op_closed
also
from A2 have \( a\cdot (d\cdot F)\cdot b\cdot c\cdot E = a\cdot d\cdot F\cdot b\cdot c\cdot E \) using group_op_closed, group_oper_assoc
finally show \( thesis \)
qed
also
from A2 have \( a\cdot d\cdot F\cdot b\cdot c\cdot E = (a\cdot (d\cdot F))\cdot (b\cdot (c\cdot E)) \) using group_op_closed, group_oper_assoc
finally show \( thesis \)
qed

Another useful rearrangement.

lemma (in group0) group0_4_L3:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \) and A3: \( c\in G \), \( d\in G \), \( E\in G \), \( F\in G \)

shows \( a\cdot b\cdot ((c\cdot d)^{-1}\cdot (E\cdot F)^{-1}) = (a\cdot (E\cdot c)^{-1})\cdot (b\cdot (F\cdot d)^{-1}) \)proof
from A3 have T1: \( c^{-1}\in G \), \( d^{-1}\in G \), \( E^{-1}\in G \), \( F^{-1}\in G \), \( (c\cdot d)^{-1}\in G \), \( (E\cdot F)^{-1}\in G \) using inverse_in_group, group_op_closed
from A2, T1 have \( a\cdot b\cdot ((c\cdot d)^{-1}\cdot (E\cdot F)^{-1}) = a\cdot b\cdot (c\cdot d)^{-1}\cdot (E\cdot F)^{-1} \) using group_op_closed, group_oper_assoc
also
from A2, A3 have \( a\cdot b\cdot (c\cdot d)^{-1}\cdot (E\cdot F)^{-1} = (a\cdot b)\cdot (d^{-1}\cdot c^{-1})\cdot (F^{-1}\cdot E^{-1}) \) using group_inv_of_two
also
from A1, A2, T1 have \( (a\cdot b)\cdot (d^{-1}\cdot c^{-1})\cdot (F^{-1}\cdot E^{-1}) = (a\cdot (c^{-1}\cdot E^{-1}))\cdot (b\cdot (d^{-1}\cdot F^{-1})) \) using group0_4_L2
also
from A2, A3 have \( (a\cdot (c^{-1}\cdot E^{-1}))\cdot (b\cdot (d^{-1}\cdot F^{-1})) = (a\cdot (E\cdot c)^{-1})\cdot (b\cdot (F\cdot d)^{-1}) \) using group_inv_of_two
finally show \( thesis \)
qed

Some useful rearrangements for two elements of a group.

lemma (in group0) group0_4_L4:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \)

shows \( b^{-1}\cdot a^{-1} = a^{-1}\cdot b^{-1} \), \( (a\cdot b)^{-1} = a^{-1}\cdot b^{-1} \), \( (a\cdot b^{-1})^{-1} = a^{-1}\cdot b \)proof
from A2 have T1: \( b^{-1}\in G \), \( a^{-1}\in G \) using inverse_in_group
with A1 show \( b^{-1}\cdot a^{-1} = a^{-1}\cdot b^{-1} \) using IsCommutative_def
with A2 show \( (a\cdot b)^{-1} = a^{-1}\cdot b^{-1} \) using group_inv_of_two
from A2, T1 have \( (a\cdot b^{-1})^{-1} = (b^{-1})^{-1}\cdot a^{-1} \) using group_inv_of_two
with A1, A2, T1 show \( (a\cdot b^{-1})^{-1} = a^{-1}\cdot b \) using group_inv_of_inv, IsCommutative_def
qed

Another bunch of useful rearrangements with three elements.

lemma (in group0) group0_4_L4A:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot c = c\cdot a\cdot b \), \( a^{-1}\cdot (b^{-1}\cdot c^{-1})^{-1} = (a\cdot (b\cdot c)^{-1})^{-1} \), \( a\cdot (b\cdot c)^{-1} = a\cdot b^{-1}\cdot c^{-1} \), \( a\cdot (b\cdot c^{-1})^{-1} = a\cdot b^{-1}\cdot c \), \( a\cdot b^{-1}\cdot c^{-1} = a\cdot c^{-1}\cdot b^{-1} \)proof
from A1, A2 have \( a\cdot b\cdot c = c\cdot (a\cdot b) \) using IsCommutative_def, group_op_closed
with A2 show \( a\cdot b\cdot c = c\cdot a\cdot b \) using group_op_closed, group_oper_assoc
from A2 have T: \( b^{-1}\in G \), \( c^{-1}\in G \), \( b^{-1}\cdot c^{-1} \in G \), \( a\cdot b \in G \) using inverse_in_group, group_op_closed
with A1, A2 show \( a^{-1}\cdot (b^{-1}\cdot c^{-1})^{-1} = (a\cdot (b\cdot c)^{-1})^{-1} \) using group_inv_of_two, IsCommutative_def
from A1, A2, T have \( a\cdot (b\cdot c)^{-1} = a\cdot (b^{-1}\cdot c^{-1}) \) using group_inv_of_two, IsCommutative_def
with A2, T show \( a\cdot (b\cdot c)^{-1} = a\cdot b^{-1}\cdot c^{-1} \) using group_oper_assoc
from A1, A2, T have \( a\cdot (b\cdot c^{-1})^{-1} = a\cdot (b^{-1}\cdot (c^{-1})^{-1}) \) using group_inv_of_two, IsCommutative_def
with A2, T show \( a\cdot (b\cdot c^{-1})^{-1} = a\cdot b^{-1}\cdot c \) using group_oper_assoc, group_inv_of_inv
from A1, A2, T have \( a\cdot b^{-1}\cdot c^{-1} = a\cdot (c^{-1}\cdot b^{-1}) \) using group_oper_assoc, IsCommutative_def
with A2, T show \( a\cdot b^{-1}\cdot c^{-1} = a\cdot c^{-1}\cdot b^{-1} \) using group_oper_assoc
qed

Another useful rearrangement.

lemma (in group0) group0_4_L4B:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b^{-1}\cdot (b\cdot c^{-1}) = a\cdot c^{-1} \) using assms, inverse_in_group, group_op_closed, group0_4_L4, group_oper_assoc, inv_cancel_two

A couple of permutations of order for three alements.

lemma (in group0) group0_4_L4C:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot c = c\cdot a\cdot b \), \( a\cdot b\cdot c = a\cdot (c\cdot b) \), \( a\cdot b\cdot c = c\cdot (a\cdot b) \), \( a\cdot b\cdot c = c\cdot b\cdot a \)proof
from A1, A2 show I: \( a\cdot b\cdot c = c\cdot a\cdot b \) using group0_4_L4A
also
from A1, A2 have \( c\cdot a\cdot b = a\cdot c\cdot b \) using IsCommutative_def
also
from A2 have \( a\cdot c\cdot b = a\cdot (c\cdot b) \) using group_oper_assoc
finally show \( a\cdot b\cdot c = a\cdot (c\cdot b) \)
from A2, I show \( a\cdot b\cdot c = c\cdot (a\cdot b) \) using group_oper_assoc
also
from A1, A2 have \( c\cdot (a\cdot b) = c\cdot (b\cdot a) \) using IsCommutative_def
also
from A2 have \( c\cdot (b\cdot a) = c\cdot b\cdot a \) using group_oper_assoc
finally show \( a\cdot b\cdot c = c\cdot b\cdot a \)
qed

Some rearangement with three elements and inverse.

lemma (in group0) group0_4_L4D:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a^{-1}\cdot b^{-1}\cdot c = c\cdot a^{-1}\cdot b^{-1} \), \( b^{-1}\cdot a^{-1}\cdot c = c\cdot a^{-1}\cdot b^{-1} \), \( (a^{-1}\cdot b\cdot c)^{-1} = a\cdot b^{-1}\cdot c^{-1} \)proof
from A2 have T: \( a^{-1} \in G \), \( b^{-1} \in G \), \( c^{-1}\in G \) using inverse_in_group
with A1, A2 show \( a^{-1}\cdot b^{-1}\cdot c = c\cdot a^{-1}\cdot b^{-1} \), \( b^{-1}\cdot a^{-1}\cdot c = c\cdot a^{-1}\cdot b^{-1} \) using group0_4_L4A
from A1, A2, T show \( (a^{-1}\cdot b\cdot c)^{-1} = a\cdot b^{-1}\cdot c^{-1} \) using group_inv_of_three, group_inv_of_inv, group0_4_L4C
qed

Another rearrangement lemma with three elements and equation.

lemma (in group0) group0_4_L5:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \) and A3: \( c = a\cdot b^{-1} \)

shows \( a = b\cdot c \)proof
from A2, A3 have \( c\cdot (b^{-1})^{-1} = a \) using inverse_in_group, group0_2_L18
with A1, A2 show \( thesis \) using group_inv_of_inv, IsCommutative_def
qed

In abelian groups we can cancel an element with its inverse even if separated by another element.

lemma (in group0) group0_4_L6A:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \)

shows \( a\cdot b\cdot a^{-1} = b \), \( a^{-1}\cdot b\cdot a = b \), \( a^{-1}\cdot (b\cdot a) = b \), \( a\cdot (b\cdot a^{-1}) = b \)proof
from A1, A2 have \( a\cdot b\cdot a^{-1} = a^{-1}\cdot a\cdot b \) using inverse_in_group, group0_4_L4A
also
from A2 have \( \ldots = b \) using group0_2_L6, group0_2_L2
finally show \( a\cdot b\cdot a^{-1} = b \)
from A1, A2 have \( a^{-1}\cdot b\cdot a = a\cdot a^{-1}\cdot b \) using inverse_in_group, group0_4_L4A
also
from A2 have \( \ldots = b \) using group0_2_L6, group0_2_L2
finally show \( a^{-1}\cdot b\cdot a = b \)
moreover
from A2 have \( a^{-1}\cdot b\cdot a = a^{-1}\cdot (b\cdot a) \) using inverse_in_group, group_oper_assoc
ultimately show \( a^{-1}\cdot (b\cdot a) = b \)
from A1, A2 show \( a\cdot (b\cdot a^{-1}) = b \) using inverse_in_group, IsCommutative_def, inv_cancel_two
qed

Another lemma about cancelling with two elements.

lemma (in group0) group0_4_L6AA:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot a^{-1} = b^{-1} \) using assms, inverse_in_group, group0_4_L6A

Another lemma about cancelling with two elements.

lemma (in group0) group0_4_L6AB:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \)

shows \( a\cdot (a\cdot b)^{-1} = b^{-1} \), \( a\cdot (b\cdot a^{-1}) = b \)proof
from A2 have \( a\cdot (a\cdot b)^{-1} = a\cdot (b^{-1}\cdot a^{-1}) \) using group_inv_of_two
also
from A2 have \( \ldots = a\cdot b^{-1}\cdot a^{-1} \) using inverse_in_group, group_oper_assoc
also
from A1, A2 have \( \ldots = b^{-1} \) using group0_4_L6AA
finally show \( a\cdot (a\cdot b)^{-1} = b^{-1} \)
from A1, A2 have \( a\cdot (b\cdot a^{-1}) = a\cdot (a^{-1}\cdot b) \) using inverse_in_group, IsCommutative_def
also
from A2 have \( \ldots = b \) using inverse_in_group, group_oper_assoc, group0_2_L6, group0_2_L2
finally show \( a\cdot (b\cdot a^{-1}) = b \)
qed

Another lemma about cancelling with two elements.

lemma (in group0) group0_4_L6AC:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \)

shows \( a\cdot (a\cdot b^{-1})^{-1} = b \) using assms, inverse_in_group, group0_4_L6AB, group_inv_of_inv

In abelian groups we can cancel an element with its inverse even if separated by two other elements.

lemma (in group0) group0_4_L6B:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot c\cdot a^{-1} = b\cdot c \), \( a^{-1}\cdot b\cdot c\cdot a = b\cdot c \)proof
from A2 have \( a\cdot b\cdot c\cdot a^{-1} = a\cdot (b\cdot c)\cdot a^{-1} \), \( a^{-1}\cdot b\cdot c\cdot a = a^{-1}\cdot (b\cdot c)\cdot a \) using group_op_closed, group_oper_assoc, inverse_in_group
with A1, A2 show \( a\cdot b\cdot c\cdot a^{-1} = b\cdot c \), \( a^{-1}\cdot b\cdot c\cdot a = b\cdot c \) using group_op_closed, group0_4_L6A
qed

In abelian groups we can cancel an element with its inverse even if separated by three other elements.

lemma (in group0) group0_4_L6C:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b\cdot c\cdot d\cdot a^{-1} = b\cdot c\cdot d \)proof
from A2 have \( a\cdot b\cdot c\cdot d\cdot a^{-1} = a\cdot (b\cdot c\cdot d)\cdot a^{-1} \) using group_op_closed, group_oper_assoc
with A1, A2 show \( thesis \) using group_op_closed, group0_4_L6A
qed

Another couple of useful rearrangements of three elements and cancelling.

lemma (in group0) group0_4_L6D:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b^{-1}\cdot (a\cdot c^{-1})^{-1} = c\cdot b^{-1} \), \( (a\cdot c)^{-1}\cdot (b\cdot c) = a^{-1}\cdot b \), \( a\cdot (b\cdot (c\cdot a^{-1}\cdot b^{-1})) = c \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot a^{-1}) = b \)proof
from A2 have T: \( a^{-1} \in G \), \( b^{-1} \in G \), \( c^{-1} \in G \), \( a\cdot b \in G \), \( a\cdot b^{-1} \in G \), \( c^{-1}\cdot a^{-1} \in G \), \( c\cdot a^{-1} \in G \) using inverse_in_group, group_op_closed
with A1, A2 show \( a\cdot b^{-1}\cdot (a\cdot c^{-1})^{-1} = c\cdot b^{-1} \) using group0_2_L12, group_oper_assoc, group0_4_L6B, IsCommutative_def
from A2, T have \( (a\cdot c)^{-1}\cdot (b\cdot c) = c^{-1}\cdot a^{-1}\cdot b\cdot c \) using group_inv_of_two, group_oper_assoc
also
from A1, A2, T have \( \ldots = a^{-1}\cdot b \) using group0_4_L6B
finally show \( (a\cdot c)^{-1}\cdot (b\cdot c) = a^{-1}\cdot b \)
from A1, A2, T show \( a\cdot (b\cdot (c\cdot a^{-1}\cdot b^{-1})) = c \) using group_oper_assoc, group0_4_L6B, group0_4_L6A
from T have \( a\cdot b\cdot c^{-1}\cdot (c\cdot a^{-1}) = a\cdot b\cdot (c^{-1}\cdot (c\cdot a^{-1})) \) using group_oper_assoc
also
from A1, A2, T have \( \ldots = b \) using group_oper_assoc, group0_2_L6, group0_2_L2, group0_4_L6A
finally show \( a\cdot b\cdot c^{-1}\cdot (c\cdot a^{-1}) = b \)
qed

Another useful rearrangement of three elements and cancelling.

lemma (in group0) group0_4_L6E:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot (a\cdot c)^{-1} = b\cdot c^{-1} \)proof
from A2 have T: \( b^{-1} \in G \), \( c^{-1} \in G \) using inverse_in_group
with A1, A2 have \( a\cdot (b^{-1})^{-1}\cdot (a\cdot (c^{-1})^{-1})^{-1} = c^{-1}\cdot (b^{-1})^{-1} \) using group0_4_L6D
with A1, A2, T show \( a\cdot b\cdot (a\cdot c)^{-1} = b\cdot c^{-1} \) using group_inv_of_inv, IsCommutative_def
qed

A rearrangement with two elements and canceelling, special case of group0_4_L6D when \(c=b^{-1}\).

lemma (in group0) group0_4_L6F:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot (a\cdot b)^{-1} = b^{-1}\cdot b^{-1} \)proof
from A2 have \( b^{-1} \in G \) using inverse_in_group
with A1, A2 have \( a\cdot b^{-1}\cdot (a\cdot (b^{-1})^{-1})^{-1} = b^{-1}\cdot b^{-1} \) using group0_4_L6D
with A2 show \( a\cdot b^{-1}\cdot (a\cdot b)^{-1} = b^{-1}\cdot b^{-1} \) using group_inv_of_inv
qed

Some other rearrangements with four elements. The algorithm for proof as in group0_4_L2 works very well here.

lemma (in group0) rearr_ab_gr_4_elemA:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b\cdot c\cdot d = a\cdot d\cdot b\cdot c \), \( a\cdot b\cdot c\cdot d = a\cdot c\cdot (b\cdot d) \)proof
from A1, A2 have \( a\cdot b\cdot c\cdot d = d\cdot (a\cdot b\cdot c) \) using IsCommutative_def, group_op_closed
also
from A2 have \( \ldots = d\cdot a\cdot b\cdot c \) using group_op_closed, group_oper_assoc
also
from A1, A2 have \( \ldots = a\cdot d\cdot b\cdot c \) using IsCommutative_def, group_op_closed
finally show \( a\cdot b\cdot c\cdot d = a\cdot d\cdot b\cdot c \)
from A1, A2 have \( a\cdot b\cdot c\cdot d = c\cdot (a\cdot b)\cdot d \) using IsCommutative_def, group_op_closed
also
from A2 have \( \ldots = c\cdot a\cdot b\cdot d \) using group_op_closed, group_oper_assoc
also
from A1, A2 have \( \ldots = a\cdot c\cdot b\cdot d \) using IsCommutative_def, group_op_closed
also
from A2 have \( \ldots = a\cdot c\cdot (b\cdot d) \) using group_op_closed, group_oper_assoc
finally show \( a\cdot b\cdot c\cdot d = a\cdot c\cdot (b\cdot d) \)
qed

Some rearrangements with four elements and inverse that are applications of rearr_ab_gr_4_elem

lemma (in group0) rearr_ab_gr_4_elemB:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b^{-1}\cdot c^{-1}\cdot d^{-1} = a\cdot d^{-1}\cdot b^{-1}\cdot c^{-1} \), \( a\cdot b\cdot c\cdot d^{-1} = a\cdot d^{-1}\cdot b\cdot c \), \( a\cdot b\cdot c^{-1}\cdot d^{-1} = a\cdot c^{-1}\cdot (b\cdot d^{-1}) \)proof
from A2 have T: \( b^{-1} \in G \), \( c^{-1} \in G \), \( d^{-1} \in G \) using inverse_in_group
with A1, A2 show \( a\cdot b^{-1}\cdot c^{-1}\cdot d^{-1} = a\cdot d^{-1}\cdot b^{-1}\cdot c^{-1} \), \( a\cdot b\cdot c\cdot d^{-1} = a\cdot d^{-1}\cdot b\cdot c \), \( a\cdot b\cdot c^{-1}\cdot d^{-1} = a\cdot c^{-1}\cdot (b\cdot d^{-1}) \) using rearr_ab_gr_4_elemA
qed

Some rearrangement lemmas with four elements.

lemma (in group0) group0_4_L7:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b\cdot c\cdot d^{-1} = a\cdot d^{-1}\cdot b\cdot c \), \( a\cdot d\cdot (b\cdot d\cdot (c\cdot d))^{-1} = a\cdot (b\cdot c)^{-1}\cdot d^{-1} \), \( a\cdot (b\cdot c)\cdot d = a\cdot b\cdot d\cdot c \)proof
from A2 have T: \( b\cdot c \in G \), \( d^{-1} \in G \), \( b^{-1}\in G \), \( c^{-1}\in G \), \( d^{-1}\cdot b \in G \), \( c^{-1}\cdot d \in G \), \( (b\cdot c)^{-1} \in G \), \( b\cdot d \in G \), \( b\cdot d\cdot c \in G \), \( (b\cdot d\cdot c)^{-1} \in G \), \( a\cdot d \in G \), \( b\cdot c \in G \) using group_op_closed, inverse_in_group
with A1, A2 have \( a\cdot b\cdot c\cdot d^{-1} = a\cdot (d^{-1}\cdot b\cdot c) \) using group_oper_assoc, group0_4_L4A
also
from A2, T have \( a\cdot (d^{-1}\cdot b\cdot c) = a\cdot d^{-1}\cdot b\cdot c \) using group_oper_assoc
finally show \( a\cdot b\cdot c\cdot d^{-1} = a\cdot d^{-1}\cdot b\cdot c \)
from A2, T have \( a\cdot d\cdot (b\cdot d\cdot (c\cdot d))^{-1} = a\cdot d\cdot (d^{-1}\cdot (b\cdot d\cdot c)^{-1}) \) using group_oper_assoc, group_inv_of_two
also
from A2, T have \( \ldots = a\cdot (b\cdot d\cdot c)^{-1} \) using group_oper_assoc, inv_cancel_two
also
from A1, A2 have \( \ldots = a\cdot (d\cdot (b\cdot c))^{-1} \) using IsCommutative_def, group_oper_assoc
also
from A2, T have \( \ldots = a\cdot ((b\cdot c)^{-1}\cdot d^{-1}) \) using group_inv_of_two
also
from A2, T have \( \ldots = a\cdot (b\cdot c)^{-1}\cdot d^{-1} \) using group_oper_assoc
finally show \( a\cdot d\cdot (b\cdot d\cdot (c\cdot d))^{-1} = a\cdot (b\cdot c)^{-1}\cdot d^{-1} \)
from A2 have \( a\cdot (b\cdot c)\cdot d = a\cdot (b\cdot (c\cdot d)) \) using group_op_closed, group_oper_assoc
also
from A1, A2 have \( \ldots = a\cdot (b\cdot (d\cdot c)) \) using IsCommutative_def, group_op_closed
also
from A2 have \( \ldots = a\cdot b\cdot d\cdot c \) using group_op_closed, group_oper_assoc
finally show \( a\cdot (b\cdot c)\cdot d = a\cdot b\cdot d\cdot c \)
qed

Some other rearrangements with four elements.

lemma (in group0) group0_4_L8:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot (b\cdot c)^{-1} = (a\cdot d^{-1}\cdot c^{-1})\cdot (d\cdot b^{-1}) \), \( a\cdot b\cdot (c\cdot d) = c\cdot a\cdot (b\cdot d) \), \( a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d) \), \( a\cdot (b\cdot c^{-1})\cdot d = a\cdot b\cdot d\cdot c^{-1} \), \( (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1} \)proof
from A2 have T: \( b\cdot c \in G \), \( a\cdot b \in G \), \( d^{-1} \in G \), \( b^{-1}\in G \), \( c^{-1}\in G \), \( d^{-1}\cdot b \in G \), \( c^{-1}\cdot d \in G \), \( (b\cdot c)^{-1} \in G \), \( a\cdot b \in G \), \( (c\cdot d)^{-1} \in G \), \( (b\cdot d^{-1})^{-1} \in G \), \( d\cdot b^{-1} \in G \) using group_op_closed, inverse_in_group
from A2 have \( a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1} \) using group0_2_L14A
moreover
from A2 have \( a\cdot c^{-1} = (a\cdot d^{-1})\cdot (d\cdot c^{-1}) \) using group0_2_L14A
ultimately have \( a\cdot (b\cdot c)^{-1} = (a\cdot d^{-1})\cdot (d\cdot c^{-1})\cdot b^{-1} \)
with A1, A2, T have \( a\cdot (b\cdot c)^{-1}= a\cdot d^{-1}\cdot (c^{-1}\cdot d)\cdot b^{-1} \) using IsCommutative_def
with A2, T show \( a\cdot (b\cdot c)^{-1} = (a\cdot d^{-1}\cdot c^{-1})\cdot (d\cdot b^{-1}) \) using group_op_closed, group_oper_assoc
from A2, T have \( a\cdot b\cdot (c\cdot d) = a\cdot b\cdot c\cdot d \) using group_oper_assoc
also
have \( a\cdot b\cdot c\cdot d = c\cdot a\cdot b\cdot d \)proof
from A1, A2 have \( a\cdot b\cdot c\cdot d = c\cdot (a\cdot b)\cdot d \) using IsCommutative_def, group_op_closed
also
from A2 have \( \ldots = c\cdot a\cdot b\cdot d \) using group_op_closed, group_oper_assoc
finally show \( thesis \)
qed
also
from A2 have \( c\cdot a\cdot b\cdot d = c\cdot a\cdot (b\cdot d) \) using group_op_closed, group_oper_assoc
finally show \( a\cdot b\cdot (c\cdot d) = c\cdot a\cdot (b\cdot d) \)
with A1, A2 show \( a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d) \) using IsCommutative_def
from A1, A2, T show \( a\cdot (b\cdot c^{-1})\cdot d = a\cdot b\cdot d\cdot c^{-1} \) using group0_4_L7
from T have \( (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = (a\cdot b)\cdot ((c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1}) \) using group_oper_assoc
also
from A1, A2, T have \( \ldots = (a\cdot b)\cdot (c^{-1}\cdot d^{-1}\cdot (d\cdot b^{-1})) \) using group_inv_of_two, group0_2_L12, IsCommutative_def
also
from T have \( \ldots = (a\cdot b)\cdot (c^{-1}\cdot (d^{-1}\cdot (d\cdot b^{-1}))) \) using group_oper_assoc
also
from A1, A2, T have \( \ldots = a\cdot c^{-1} \) using group_oper_assoc, group0_2_L6, group0_2_L2, IsCommutative_def, inv_cancel_two
finally show \( (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1} \)
qed

Some other rearrangements with four elements.

lemma (in group0) group0_4_L8A:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b^{-1}\cdot (c\cdot d^{-1}) = a\cdot c\cdot (b^{-1}\cdot d^{-1}) \), \( a\cdot b^{-1}\cdot (c\cdot d^{-1}) = a\cdot c\cdot b^{-1}\cdot d^{-1} \)proof
from A2 have T: \( a\in G \), \( b^{-1} \in G \), \( c\in G \), \( d^{-1} \in G \) using inverse_in_group
with A1 show \( a\cdot b^{-1}\cdot (c\cdot d^{-1}) = a\cdot c\cdot (b^{-1}\cdot d^{-1}) \) by (rule group0_4_L8 )
with A2, T show \( a\cdot b^{-1}\cdot (c\cdot d^{-1}) = a\cdot c\cdot b^{-1}\cdot d^{-1} \) using group_op_closed, group_oper_assoc
qed

Some rearrangements with an equation.

lemma (in group0) group0_4_L9:

assumes A1: \( P \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \) and A3: \( a = b\cdot c^{-1}\cdot d^{-1} \)

shows \( d = b\cdot a^{-1}\cdot c^{-1} \), \( d = a^{-1}\cdot b\cdot c^{-1} \), \( b = a\cdot d\cdot c \)proof
from A2 have T: \( a^{-1} \in G \), \( c^{-1} \in G \), \( d^{-1} \in G \), \( b\cdot c^{-1} \in G \) using group_op_closed, inverse_in_group
with A2, A3 have \( a\cdot (d^{-1})^{-1} = b\cdot c^{-1} \) using group0_2_L18
with A2 have \( b\cdot c^{-1} = a\cdot d \) using group_inv_of_inv
with A2, T have I: \( a^{-1}\cdot (b\cdot c^{-1}) = d \) using group0_2_L18
with A1, A2, T show \( d = b\cdot a^{-1}\cdot c^{-1} \), \( d = a^{-1}\cdot b\cdot c^{-1} \) using group_oper_assoc, IsCommutative_def
from A3 have \( a\cdot d\cdot c = (b\cdot c^{-1}\cdot d^{-1})\cdot d\cdot c \)
also
from A2, T have \( \ldots = b\cdot c^{-1}\cdot (d^{-1}\cdot d)\cdot c \) using group_oper_assoc
also
from A2, T have \( \ldots = b\cdot c^{-1}\cdot c \) using group0_2_L6, group0_2_L2
also
from A2, T have \( \ldots = b\cdot (c^{-1}\cdot c) \) using group_oper_assoc
also
from A2 have \( \ldots = b \) using group0_2_L6, group0_2_L2
finally have \( a\cdot d\cdot c = b \)
thus \( b = a\cdot d\cdot c \)
qed
end
lemma (in group0) group_op_closed:

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

shows \( a\cdot b \in G \)
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 \)
Definition of IsCommutative: \( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)
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 group0) group0_4_L2:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \), \( E\in G \), \( F\in G \)

shows \( (a\cdot b)\cdot (c\cdot d)\cdot (E\cdot F) = (a\cdot (d\cdot F))\cdot (b\cdot (c\cdot E)) \)
lemma (in group0) group_inv_of_inv:

assumes \( a\in G \)

shows \( a = (a^{-1})^{-1} \)
lemma (in group0) group0_4_L4:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \)

shows \( b^{-1}\cdot a^{-1} = a^{-1}\cdot b^{-1} \), \( (a\cdot b)^{-1} = a^{-1}\cdot b^{-1} \), \( (a\cdot b^{-1})^{-1} = a^{-1}\cdot b \)
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 (in group0) group0_4_L4A:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot c = c\cdot a\cdot b \), \( a^{-1}\cdot (b^{-1}\cdot c^{-1})^{-1} = (a\cdot (b\cdot c)^{-1})^{-1} \), \( a\cdot (b\cdot c)^{-1} = a\cdot b^{-1}\cdot c^{-1} \), \( a\cdot (b\cdot c^{-1})^{-1} = a\cdot b^{-1}\cdot c \), \( a\cdot b^{-1}\cdot c^{-1} = a\cdot c^{-1}\cdot b^{-1} \)
lemma (in group0) group_inv_of_three:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (a\cdot b)^{-1} \), \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot (b^{-1}\cdot a^{-1}) \), \( (a\cdot b\cdot c)^{-1} = c^{-1}\cdot b^{-1}\cdot a^{-1} \)
lemma (in group0) group0_4_L4C:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot c = c\cdot a\cdot b \), \( a\cdot b\cdot c = a\cdot (c\cdot b) \), \( a\cdot b\cdot c = c\cdot (a\cdot b) \), \( a\cdot b\cdot c = c\cdot b\cdot a \)
lemma (in group0) group0_2_L18:

assumes \( a\in G \), \( b\in G \) and \( c = a\cdot b \)

shows \( c\cdot b^{-1} = a \), \( a^{-1}\cdot c = b \)
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) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
lemma (in group0) group0_4_L6A:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \)

shows \( a\cdot b\cdot a^{-1} = b \), \( a^{-1}\cdot b\cdot a = b \), \( a^{-1}\cdot (b\cdot a) = b \), \( a\cdot (b\cdot a^{-1}) = b \)
lemma (in group0) group0_4_L6AA:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \)

shows \( a\cdot b^{-1}\cdot a^{-1} = b^{-1} \)
lemma (in group0) group0_4_L6AB:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \)

shows \( a\cdot (a\cdot b)^{-1} = b^{-1} \), \( a\cdot (b\cdot a^{-1}) = b \)
lemma (in group0) group0_2_L12:

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

shows \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \)
lemma (in group0) group0_4_L6B:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot c\cdot a^{-1} = b\cdot c \), \( a^{-1}\cdot b\cdot c\cdot a = b\cdot c \)
lemma (in group0) group0_4_L6D:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b^{-1}\cdot (a\cdot c^{-1})^{-1} = c\cdot b^{-1} \), \( (a\cdot c)^{-1}\cdot (b\cdot c) = a^{-1}\cdot b \), \( a\cdot (b\cdot (c\cdot a^{-1}\cdot b^{-1})) = c \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot a^{-1}) = b \)
lemma (in group0) rearr_ab_gr_4_elemA:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b\cdot c\cdot d = a\cdot d\cdot b\cdot c \), \( a\cdot b\cdot c\cdot d = a\cdot c\cdot (b\cdot d) \)
lemma (in group0) group0_2_L14A:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \), \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \), \( a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1} \), \( a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1} \), \( (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1} \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a \), \( a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b \)
lemma (in group0) group0_4_L7:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b\cdot c\cdot d^{-1} = a\cdot d^{-1}\cdot b\cdot c \), \( a\cdot d\cdot (b\cdot d\cdot (c\cdot d))^{-1} = a\cdot (b\cdot c)^{-1}\cdot d^{-1} \), \( a\cdot (b\cdot c)\cdot d = a\cdot b\cdot d\cdot c \)
lemma (in group0) group0_4_L8:

assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot (b\cdot c)^{-1} = (a\cdot d^{-1}\cdot c^{-1})\cdot (d\cdot b^{-1}) \), \( a\cdot b\cdot (c\cdot d) = c\cdot a\cdot (b\cdot d) \), \( a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d) \), \( a\cdot (b\cdot c^{-1})\cdot d = a\cdot b\cdot d\cdot c^{-1} \), \( (a\cdot b)\cdot (c\cdot d)^{-1}\cdot (b\cdot d^{-1})^{-1} = a\cdot c^{-1} \)