section ‹Abelian Group›
theory AbelianGroup_ZF imports Group_ZF
begin
text‹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.
›
subsection‹Rearrangement formulae›
text‹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.
›
text‹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 {is commutative on} G"
and A2:"a∈G" "b∈G" "c∈G" "d∈G" "E∈G" "F∈G"
shows "(a⋅b)⋅(c⋅d)⋅(E⋅F) = (a⋅(d⋅F))⋅(b⋅(c⋅E))"
proof -
from A2 have "(a⋅b)⋅(c⋅d)⋅(E⋅F) = a⋅b⋅c⋅d⋅E⋅F"
using group_op_closed group_oper_assoc
by simp
also have "a⋅b⋅c⋅d⋅E⋅F = a⋅d⋅F⋅b⋅c⋅E"
proof -
from A1 A2 have "a⋅b⋅c⋅d⋅E⋅F = F⋅(a⋅b⋅c⋅d⋅E)"
using IsCommutative_def group_op_closed
by simp
also from A2 have "F⋅(a⋅b⋅c⋅d⋅E) = F⋅a⋅b⋅c⋅d⋅E"
using group_op_closed group_oper_assoc
by simp
also from A1 A2 have "F⋅a⋅b⋅c⋅d⋅E = d⋅(F⋅a⋅b⋅c)⋅E"
using IsCommutative_def group_op_closed
by simp
also from A2 have "d⋅(F⋅a⋅b⋅c)⋅E = d⋅F⋅a⋅b⋅c⋅E"
using group_op_closed group_oper_assoc
by simp
also from A1 A2 have " d⋅F⋅a⋅b⋅c⋅E = a⋅(d⋅F)⋅b⋅c⋅E"
using IsCommutative_def group_op_closed
by simp
also from A2 have "a⋅(d⋅F)⋅b⋅c⋅E = a⋅d⋅F⋅b⋅c⋅E"
using group_op_closed group_oper_assoc
by simp
finally show ?thesis by simp
qed
also from A2 have "a⋅d⋅F⋅b⋅c⋅E = (a⋅(d⋅F))⋅(b⋅(c⋅E))"
using group_op_closed group_oper_assoc
by simp
finally show ?thesis by simp
qed
text‹Another useful rearrangement.›
lemma (in group0) group0_4_L3:
assumes A1:"P {is commutative on} G"
and A2: "a∈G" "b∈G" and A3: "c∈G" "d∈G" "E∈G" "F∈G"
shows "a⋅b⋅((c⋅d)¯⋅(E⋅F)¯) = (a⋅(E⋅c)¯)⋅(b⋅(F⋅d)¯)"
proof -
from A3 have T1:
"c¯∈G" "d¯∈G" "E¯∈G" "F¯∈G" "(c⋅d)¯∈G" "(E⋅F)¯∈G"
using inverse_in_group group_op_closed
by auto
from A2 T1 have
"a⋅b⋅((c⋅d)¯⋅(E⋅F)¯) = a⋅b⋅(c⋅d)¯⋅(E⋅F)¯"
using group_op_closed group_oper_assoc
by simp
also from A2 A3 have
"a⋅b⋅(c⋅d)¯⋅(E⋅F)¯ = (a⋅b)⋅(d¯⋅c¯)⋅(F¯⋅E¯)"
using group_inv_of_two by simp
also from A1 A2 T1 have
"(a⋅b)⋅(d¯⋅c¯)⋅(F¯⋅E¯) = (a⋅(c¯⋅E¯))⋅(b⋅(d¯⋅F¯))"
using group0_4_L2 by simp
also from A2 A3 have
"(a⋅(c¯⋅E¯))⋅(b⋅(d¯⋅F¯)) = (a⋅(E⋅c)¯)⋅(b⋅(F⋅d)¯)"
using group_inv_of_two by simp
finally show ?thesis by simp
qed
text‹Some useful rearrangements for two elements of a group.›
lemma (in group0) group0_4_L4:
assumes A1:"P {is commutative on} G"
and A2: "a∈G" "b∈G"
shows
"b¯⋅a¯ = a¯⋅b¯"
"(a⋅b)¯ = a¯⋅b¯"
"(a⋅b¯)¯ = a¯⋅b"
proof -
from A2 have T1: "b¯∈G" "a¯∈G" using inverse_in_group by auto
with A1 show "b¯⋅a¯ = a¯⋅b¯" using IsCommutative_def by simp
with A2 show "(a⋅b)¯ = a¯⋅b¯" using group_inv_of_two by simp
from A2 T1 have "(a⋅b¯)¯ = (b¯)¯⋅a¯" using group_inv_of_two by simp
with A1 A2 T1 show "(a⋅b¯)¯ = a¯⋅b"
using group_inv_of_inv IsCommutative_def by simp
qed
text‹Another bunch of useful rearrangements with three elements.›
lemma (in group0) group0_4_L4A:
assumes A1: "P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G"
shows
"a⋅b⋅c = c⋅a⋅b"
"a¯⋅(b¯⋅c¯)¯ = (a⋅(b⋅c)¯)¯"
"a⋅(b⋅c)¯ = a⋅b¯⋅c¯"
"a⋅(b⋅c¯)¯ = a⋅b¯⋅c"
"a⋅b¯⋅c¯ = a⋅c¯⋅b¯"
proof -
from A1 A2 have "a⋅b⋅c = c⋅(a⋅b)"
using IsCommutative_def group_op_closed
by simp
with A2 show "a⋅b⋅c = c⋅a⋅b" using
group_op_closed group_oper_assoc
by simp
from A2 have T:
"b¯∈G" "c¯∈G" "b¯⋅c¯ ∈ G" "a⋅b ∈ G"
using inverse_in_group group_op_closed
by auto
with A1 A2 show "a¯⋅(b¯⋅c¯)¯ = (a⋅(b⋅c)¯)¯"
using group_inv_of_two IsCommutative_def
by simp
from A1 A2 T have "a⋅(b⋅c)¯ = a⋅(b¯⋅c¯)"
using group_inv_of_two IsCommutative_def by simp
with A2 T show "a⋅(b⋅c)¯ = a⋅b¯⋅c¯"
using group_oper_assoc by simp
from A1 A2 T have "a⋅(b⋅c¯)¯ = a⋅(b¯⋅(c¯)¯)"
using group_inv_of_two IsCommutative_def by simp
with A2 T show "a⋅(b⋅c¯)¯ = a⋅b¯⋅c"
using group_oper_assoc group_inv_of_inv by simp
from A1 A2 T have "a⋅b¯⋅c¯ = a⋅(c¯⋅b¯)"
using group_oper_assoc IsCommutative_def by simp
with A2 T show "a⋅b¯⋅c¯ = a⋅c¯⋅b¯"
using group_oper_assoc by simp
qed
text‹Another useful rearrangement.›
lemma (in group0) group0_4_L4B:
assumes "P {is commutative on} G"
and "a∈G" "b∈G" "c∈G"
shows "a⋅b¯⋅(b⋅c¯) = a⋅c¯"
using assms inverse_in_group group_op_closed
group0_4_L4 group_oper_assoc inv_cancel_two by simp
text‹A couple of permutations of order for three alements.›
lemma (in group0) group0_4_L4C:
assumes A1: "P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G"
shows
"a⋅b⋅c = c⋅a⋅b"
"a⋅b⋅c = a⋅(c⋅b)"
"a⋅b⋅c = c⋅(a⋅b)"
"a⋅b⋅c = c⋅b⋅a"
proof -
from A1 A2 show I: "a⋅b⋅c = c⋅a⋅b"
using group0_4_L4A by simp
also from A1 A2 have "c⋅a⋅b = a⋅c⋅b"
using IsCommutative_def by simp
also from A2 have "a⋅c⋅b = a⋅(c⋅b)"
using group_oper_assoc by simp
finally show "a⋅b⋅c = a⋅(c⋅b)" by simp
from A2 I show "a⋅b⋅c = c⋅(a⋅b)"
using group_oper_assoc by simp
also from A1 A2 have "c⋅(a⋅b) = c⋅(b⋅a)"
using IsCommutative_def by simp
also from A2 have "c⋅(b⋅a) = c⋅b⋅a"
using group_oper_assoc by simp
finally show "a⋅b⋅c = c⋅b⋅a" by simp
qed
text‹Some rearangement with three elements and inverse.›
lemma (in group0) group0_4_L4D:
assumes A1: "P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G"
shows
"a¯⋅b¯⋅c = c⋅a¯⋅b¯"
"b¯⋅a¯⋅c = c⋅a¯⋅b¯"
"(a¯⋅b⋅c)¯ = a⋅b¯⋅c¯"
proof -
from A2 have T:
"a¯ ∈ G" "b¯ ∈ G" "c¯∈G"
using inverse_in_group by auto
with A1 A2 show
"a¯⋅b¯⋅c = c⋅a¯⋅b¯"
"b¯⋅a¯⋅c = c⋅a¯⋅b¯"
using group0_4_L4A by auto
from A1 A2 T show "(a¯⋅b⋅c)¯ = a⋅b¯⋅c¯"
using group_inv_of_three group_inv_of_inv group0_4_L4C
by simp
qed
text‹Another rearrangement lemma with three elements and equation.›
lemma (in group0) group0_4_L5: assumes A1:"P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G"
and A3: "c = a⋅b¯"
shows "a = b⋅c"
proof -
from A2 A3 have "c⋅(b¯)¯ = a"
using inverse_in_group group0_2_L18
by simp
with A1 A2 show ?thesis using
group_inv_of_inv IsCommutative_def by simp
qed
text‹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 {is commutative on} G"
and A2: "a∈G" "b∈G"
shows
"a⋅b⋅a¯ = b"
"a¯⋅b⋅a = b"
"a¯⋅(b⋅a) = b"
"a⋅(b⋅a¯) = b"
proof -
from A1 A2 have
"a⋅b⋅a¯ = a¯⋅a⋅b"
using inverse_in_group group0_4_L4A by blast
also from A2 have "… = b"
using group0_2_L6 group0_2_L2 by simp
finally show "a⋅b⋅a¯ = b" by simp
from A1 A2 have
"a¯⋅b⋅a = a⋅a¯⋅b"
using inverse_in_group group0_4_L4A by blast
also from A2 have "… = b"
using group0_2_L6 group0_2_L2 by simp
finally show "a¯⋅b⋅a = b" by simp
moreover from A2 have "a¯⋅b⋅a = a¯⋅(b⋅a)"
using inverse_in_group group_oper_assoc by simp
ultimately show "a¯⋅(b⋅a) = b" by simp
from A1 A2 show "a⋅(b⋅a¯) = b"
using inverse_in_group IsCommutative_def inv_cancel_two
by simp
qed
text‹Another lemma about cancelling with two elements.›
lemma (in group0) group0_4_L6AA:
assumes A1: "P {is commutative on} G" and A2: "a∈G" "b∈G"
shows "a⋅b¯⋅a¯ = b¯"
using assms inverse_in_group group0_4_L6A
by auto
text‹Another lemma about cancelling with two elements.›
lemma (in group0) group0_4_L6AB:
assumes A1: "P {is commutative on} G" and A2: "a∈G" "b∈G"
shows
"a⋅(a⋅b)¯ = b¯"
"a⋅(b⋅a¯) = b"
proof -
from A2 have "a⋅(a⋅b)¯ = a⋅(b¯⋅a¯)"
using group_inv_of_two by simp
also from A2 have "… = a⋅b¯⋅a¯"
using inverse_in_group group_oper_assoc by simp
also from A1 A2 have "… = b¯"
using group0_4_L6AA by simp
finally show "a⋅(a⋅b)¯ = b¯" by simp
from A1 A2 have "a⋅(b⋅a¯) = a⋅(a¯⋅b)"
using inverse_in_group IsCommutative_def by simp
also from A2 have "… = b"
using inverse_in_group group_oper_assoc group0_2_L6 group0_2_L2
by simp
finally show "a⋅(b⋅a¯) = b" by simp
qed
text‹Another lemma about cancelling with two elements.›
lemma (in group0) group0_4_L6AC:
assumes "P {is commutative on} G" and "a∈G" "b∈G"
shows "a⋅(a⋅b¯)¯ = b"
using assms inverse_in_group group0_4_L6AB group_inv_of_inv
by simp
text‹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 {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G"
shows
"a⋅b⋅c⋅a¯ = b⋅c"
"a¯⋅b⋅c⋅a = b⋅c"
proof -
from A2 have
"a⋅b⋅c⋅a¯ = a⋅(b⋅c)⋅a¯"
"a¯⋅b⋅c⋅a = a¯⋅(b⋅c)⋅a"
using group_op_closed group_oper_assoc inverse_in_group
by auto
with A1 A2 show
"a⋅b⋅c⋅a¯ = b⋅c"
"a¯⋅b⋅c⋅a = b⋅c"
using group_op_closed group0_4_L6A
by auto
qed
text‹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 {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G" "d∈G"
shows "a⋅b⋅c⋅d⋅a¯ = b⋅c⋅d"
proof -
from A2 have "a⋅b⋅c⋅d⋅a¯ = a⋅(b⋅c⋅d)⋅a¯"
using group_op_closed group_oper_assoc
by simp
with A1 A2 show ?thesis
using group_op_closed group0_4_L6A
by simp
qed
text‹Another couple of useful rearrangements of three elements
and cancelling.›
lemma (in group0) group0_4_L6D:
assumes A1: "P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G"
shows
"a⋅b¯⋅(a⋅c¯)¯ = c⋅b¯"
"(a⋅c)¯⋅(b⋅c) = a¯⋅b"
"a⋅(b⋅(c⋅a¯⋅b¯)) = c"
"a⋅b⋅c¯⋅(c⋅a¯) = b"
proof -
from A2 have T:
"a¯ ∈ G" "b¯ ∈ G" "c¯ ∈ G"
"a⋅b ∈ G" "a⋅b¯ ∈ G" "c¯⋅a¯ ∈ G" "c⋅a¯ ∈ G"
using inverse_in_group group_op_closed by auto
with A1 A2 show "a⋅b¯⋅(a⋅c¯)¯ = c⋅b¯"
using group0_2_L12 group_oper_assoc group0_4_L6B
IsCommutative_def by simp
from A2 T have "(a⋅c)¯⋅(b⋅c) = c¯⋅a¯⋅b⋅c"
using group_inv_of_two group_oper_assoc by simp
also from A1 A2 T have "… = a¯⋅b"
using group0_4_L6B by simp
finally show "(a⋅c)¯⋅(b⋅c) = a¯⋅b"
by simp
from A1 A2 T show "a⋅(b⋅(c⋅a¯⋅b¯)) = c"
using group_oper_assoc group0_4_L6B group0_4_L6A
by simp
from T have "a⋅b⋅c¯⋅(c⋅a¯) = a⋅b⋅(c¯⋅(c⋅a¯))"
using group_oper_assoc by simp
also from A1 A2 T have "… = b"
using group_oper_assoc group0_2_L6 group0_2_L2 group0_4_L6A
by simp
finally show "a⋅b⋅c¯⋅(c⋅a¯) = b" by simp
qed
text‹Another useful rearrangement of three elements
and cancelling.›
lemma (in group0) group0_4_L6E:
assumes A1: "P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G"
shows
"a⋅b⋅(a⋅c)¯ = b⋅c¯"
proof -
from A2 have T: "b¯ ∈ G" "c¯ ∈ G"
using inverse_in_group by auto
with A1 A2 have
"a⋅(b¯)¯⋅(a⋅(c¯)¯)¯ = c¯⋅(b¯)¯"
using group0_4_L6D by simp
with A1 A2 T show "a⋅b⋅(a⋅c)¯ = b⋅c¯"
using group_inv_of_inv IsCommutative_def
by simp
qed
text‹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 {is commutative on} G"
and A2: "a∈G" "b∈G"
shows "a⋅b¯⋅(a⋅b)¯ = b¯⋅b¯"
proof -
from A2 have "b¯ ∈ G"
using inverse_in_group by simp
with A1 A2 have "a⋅b¯⋅(a⋅(b¯)¯)¯ = b¯⋅b¯"
using group0_4_L6D by simp
with A2 show "a⋅b¯⋅(a⋅b)¯ = b¯⋅b¯"
using group_inv_of_inv by simp
qed
text‹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 {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G" "d∈G"
shows
"a⋅b⋅c⋅d = a⋅d⋅b⋅c"
"a⋅b⋅c⋅d = a⋅c⋅(b⋅d)"
proof -
from A1 A2 have "a⋅b⋅c⋅d = d⋅(a⋅b⋅c)"
using IsCommutative_def group_op_closed
by simp
also from A2 have "… = d⋅a⋅b⋅c"
using group_op_closed group_oper_assoc
by simp
also from A1 A2 have "… = a⋅d⋅b⋅c"
using IsCommutative_def group_op_closed
by simp
finally show "a⋅b⋅c⋅d = a⋅d⋅b⋅c"
by simp
from A1 A2 have "a⋅b⋅c⋅d = c⋅(a⋅b)⋅d"
using IsCommutative_def group_op_closed
by simp
also from A2 have "… = c⋅a⋅b⋅d"
using group_op_closed group_oper_assoc
by simp
also from A1 A2 have "… = a⋅c⋅b⋅d"
using IsCommutative_def group_op_closed
by simp
also from A2 have "… = a⋅c⋅(b⋅d)"
using group_op_closed group_oper_assoc
by simp
finally show "a⋅b⋅c⋅d = a⋅c⋅(b⋅d)"
by simp
qed
text‹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 {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G" "d∈G"
shows
"a⋅b¯⋅c¯⋅d¯ = a⋅d¯⋅b¯⋅c¯"
"a⋅b⋅c⋅d¯ = a⋅d¯⋅b⋅c"
"a⋅b⋅c¯⋅d¯ = a⋅c¯⋅(b⋅d¯)"
proof -
from A2 have T: "b¯ ∈ G" "c¯ ∈ G" "d¯ ∈ G"
using inverse_in_group by auto
with A1 A2 show
"a⋅b¯⋅c¯⋅d¯ = a⋅d¯⋅b¯⋅c¯"
"a⋅b⋅c⋅d¯ = a⋅d¯⋅b⋅c"
"a⋅b⋅c¯⋅d¯ = a⋅c¯⋅(b⋅d¯)"
using rearr_ab_gr_4_elemA by auto
qed
text‹Some rearrangement lemmas with four elements.›
lemma (in group0) group0_4_L7:
assumes A1: "P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G" "d∈G"
shows
"a⋅b⋅c⋅d¯ = a⋅d¯⋅ b⋅c"
"a⋅d⋅(b⋅d⋅(c⋅d))¯ = a⋅(b⋅c)¯⋅d¯"
"a⋅(b⋅c)⋅d = a⋅b⋅d⋅c"
proof -
from A2 have T:
"b⋅c ∈ G" "d¯ ∈ G" "b¯∈G" "c¯∈G"
"d¯⋅b ∈ G" "c¯⋅d ∈ G" "(b⋅c)¯ ∈ G"
"b⋅d ∈ G" "b⋅d⋅c ∈ G" "(b⋅d⋅c)¯ ∈ G"
"a⋅d ∈ G" "b⋅c ∈ G"
using group_op_closed inverse_in_group
by auto
with A1 A2 have "a⋅b⋅c⋅d¯ = a⋅(d¯⋅b⋅c)"
using group_oper_assoc group0_4_L4A by simp
also from A2 T have "a⋅(d¯⋅b⋅c) = a⋅d¯⋅b⋅c"
using group_oper_assoc by simp
finally show "a⋅b⋅c⋅d¯ = a⋅d¯⋅ b⋅c" by simp
from A2 T have "a⋅d⋅(b⋅d⋅(c⋅d))¯ = a⋅d⋅(d¯⋅(b⋅d⋅c)¯)"
using group_oper_assoc group_inv_of_two by simp
also from A2 T have "… = a⋅(b⋅d⋅c)¯"
using group_oper_assoc inv_cancel_two by simp
also from A1 A2 have "… = a⋅(d⋅(b⋅c))¯"
using IsCommutative_def group_oper_assoc by simp
also from A2 T have "… = a⋅((b⋅c)¯⋅d¯)"
using group_inv_of_two by simp
also from A2 T have "… = a⋅(b⋅c)¯⋅d¯"
using group_oper_assoc by simp
finally show "a⋅d⋅(b⋅d⋅(c⋅d))¯ = a⋅(b⋅c)¯⋅d¯"
by simp
from A2 have "a⋅(b⋅c)⋅d = a⋅(b⋅(c⋅d))"
using group_op_closed group_oper_assoc by simp
also from A1 A2 have "… = a⋅(b⋅(d⋅c))"
using IsCommutative_def group_op_closed by simp
also from A2 have "… = a⋅b⋅d⋅c"
using group_op_closed group_oper_assoc by simp
finally show "a⋅(b⋅c)⋅d = a⋅b⋅d⋅c" by simp
qed
text‹Some other rearrangements with four elements.›
lemma (in group0) group0_4_L8:
assumes A1: "P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G" "d∈G"
shows
"a⋅(b⋅c)¯ = (a⋅d¯⋅c¯)⋅(d⋅b¯)"
"a⋅b⋅(c⋅d) = c⋅a⋅(b⋅d)"
"a⋅b⋅(c⋅d) = a⋅c⋅(b⋅d)"
"a⋅(b⋅c¯)⋅d = a⋅b⋅d⋅c¯"
"(a⋅b)⋅(c⋅d)¯⋅(b⋅d¯)¯ = a⋅c¯"
proof -
from A2 have T:
"b⋅c ∈ G" "a⋅b ∈ G" "d¯ ∈ G" "b¯∈G" "c¯∈G"
"d¯⋅b ∈ G" "c¯⋅d ∈ G" "(b⋅c)¯ ∈ G"
"a⋅b ∈ G" "(c⋅d)¯ ∈ G" "(b⋅d¯)¯ ∈ G" "d⋅b¯ ∈ G"
using group_op_closed inverse_in_group
by auto
from A2 have "a⋅(b⋅c)¯ = a⋅c¯⋅b¯" using group0_2_L14A by blast
moreover from A2 have "a⋅c¯ = (a⋅d¯)⋅(d⋅c¯)" using group0_2_L14A
by blast
ultimately have "a⋅(b⋅c)¯ = (a⋅d¯)⋅(d⋅c¯)⋅b¯" by simp
with A1 A2 T have "a⋅(b⋅c)¯= a⋅d¯⋅(c¯⋅d)⋅b¯"
using IsCommutative_def by simp
with A2 T show "a⋅(b⋅c)¯ = (a⋅d¯⋅c¯)⋅(d⋅b¯)"
using group_op_closed group_oper_assoc by simp
from A2 T have "a⋅b⋅(c⋅d) = a⋅b⋅c⋅d"
using group_oper_assoc by simp
also have "a⋅b⋅c⋅d = c⋅a⋅b⋅d"
proof -
from A1 A2 have "a⋅b⋅c⋅d = c⋅(a⋅b)⋅d"
using IsCommutative_def group_op_closed
by simp
also from A2 have "… = c⋅a⋅b⋅d"
using group_op_closed group_oper_assoc
by simp
finally show ?thesis by simp
qed
also from A2 have "c⋅a⋅b⋅d = c⋅a⋅(b⋅d)"
using group_op_closed group_oper_assoc
by simp
finally show "a⋅b⋅(c⋅d) = c⋅a⋅(b⋅d)" by simp
with A1 A2 show "a⋅b⋅(c⋅d) = a⋅c⋅(b⋅d)"
using IsCommutative_def by simp
from A1 A2 T show "a⋅(b⋅c¯)⋅d = a⋅b⋅d⋅c¯"
using group0_4_L7 by simp
from T have "(a⋅b)⋅(c⋅d)¯⋅(b⋅d¯)¯ = (a⋅b)⋅((c⋅d)¯⋅(b⋅d¯)¯)"
using group_oper_assoc by simp
also from A1 A2 T have "… = (a⋅b)⋅(c¯⋅d¯⋅(d⋅b¯))"
using group_inv_of_two group0_2_L12 IsCommutative_def
by simp
also from T have "… = (a⋅b)⋅(c¯⋅(d¯⋅(d⋅b¯)))"
using group_oper_assoc by simp
also from A1 A2 T have "… = a⋅c¯"
using group_oper_assoc group0_2_L6 group0_2_L2 IsCommutative_def
inv_cancel_two by simp
finally show "(a⋅b)⋅(c⋅d)¯⋅(b⋅d¯)¯ = a⋅c¯"
by simp
qed
text‹Some other rearrangements with four elements.›
lemma (in group0) group0_4_L8A:
assumes A1: "P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G" "d∈G"
shows
"a⋅b¯⋅(c⋅d¯) = a⋅c⋅(b¯⋅d¯)"
"a⋅b¯⋅(c⋅d¯) = a⋅c⋅b¯⋅d¯"
proof -
from A2 have
T: "a∈G" "b¯ ∈ G" "c∈G" "d¯ ∈ G"
using inverse_in_group by auto
with A1 show "a⋅b¯⋅(c⋅d¯) = a⋅c⋅(b¯⋅d¯)"
by (rule group0_4_L8)
with A2 T show "a⋅b¯⋅(c⋅d¯) = a⋅c⋅b¯⋅d¯"
using group_op_closed group_oper_assoc
by simp
qed
text‹Some rearrangements with an equation.›
lemma (in group0) group0_4_L9:
assumes A1: "P {is commutative on} G"
and A2: "a∈G" "b∈G" "c∈G" "d∈G"
and A3: "a = b⋅c¯⋅d¯"
shows
"d = b⋅a¯⋅c¯"
"d = a¯⋅b⋅c¯"
"b = a⋅d⋅c"
proof -
from A2 have T:
"a¯ ∈ G" "c¯ ∈ G" "d¯ ∈ G" "b⋅c¯ ∈ G"
using group_op_closed inverse_in_group
by auto
with A2 A3 have "a⋅(d¯)¯ = b⋅c¯"
using group0_2_L18 by simp
with A2 have "b⋅c¯ = a⋅d"
using group_inv_of_inv by simp
with A2 T have I: "a¯⋅(b⋅c¯) = d"
using group0_2_L18 by simp
with A1 A2 T show
"d = b⋅a¯⋅c¯"
"d = a¯⋅b⋅c¯"
using group_oper_assoc IsCommutative_def by auto
from A3 have "a⋅d⋅c = (b⋅c¯⋅d¯)⋅d⋅c" by simp
also from A2 T have "… = b⋅c¯⋅(d¯⋅d)⋅c"
using group_oper_assoc by simp
also from A2 T have "… = b⋅c¯⋅c"
using group0_2_L6 group0_2_L2 by simp
also from A2 T have "… = b⋅(c¯⋅c)"
using group_oper_assoc by simp
also from A2 have "… = b"
using group0_2_L6 group0_2_L2 by simp
finally have "a⋅d⋅c = b" by simp
thus "b = a⋅d⋅c" by simp
qed
end