In the Monoid_ZF_1 theory we consider multiplicities of \(n\cdot x\) of monoid elements, i.e. special cases of expressions of the form \(x_1\oplus x_2\oplus\dots\oplus x_n\) where \(x_i=x\) for \(i=1..n\). In the group context where we usually use multiplicative notation this translates to the "power" \(x^n\) where \(n\in \mathbb{N}\), see also section "Product of a list of group elements" in the Group_ZF theory. In the group setting the notion of raising an element to natural power can be naturally generalized to the notion of raising an element to an integer power.
The integer power is defined in terms of natural powers of an element and its inverse. In this section we study properties of expressions \((x^n)\cdot(x^{-1})^k\), where \(x\) is a group element and \(n,k\) are natural numbers.
The natural power of \(x\) multiplied by the same power of \(x^{-1}\) cancel out to give the neutral element of the group.
lemma (in group0) nat_pow_inv_cancel:
assumes \( n\in nat \), \( x\in G \)
shows \( x^{n}\cdot (x^{-1})^{n} = 1 \)proofThe natural power of \(x^{-1}\) multiplied by the same power of \(x\) cancel out to give the neutral element of the group. Same as nat_pow_inv_cancel written with \(x^{-1}\) instead of \(x\).
lemma (in group0) nat_pow_inv_cancel1:
assumes \( n\in nat \), \( x\in G \)
shows \( (x^{-1})^{n}\cdot x^{n} = 1 \)proofIf \(k\leq n\) are natural numbers and \(x\) an element of the group, then \(x^n\cdot (x^{-1})^k = x^(k-n)\).
lemma (in group0) nat_pow_cancel_less:
assumes \( n\in nat \), \( k\leq n \), \( x\in G \)
shows \( x^{n}\cdot (x^{-1})^{k} = x^{n - k} \)proofIf \(k\leq n\) are natural numbers and \(x\) an element of the group, then \((x^{-1})^n\cdot x^k = (x^{-1})^(k-n)\).
lemma (in group0) nat_pow_cancel_less1:
assumes \( n\in nat \), \( k\leq n \), \( x\in G \)
shows \( (x^{-1})^{n}\cdot x^{k} = (x^{-1})^{n - k} \)proofIf \(k\leq n\) are natural numbers and \(x\) an element of the group, then \(x^k\cdot (x^{-1})^n = (x^{-1})^(k-n)\).
lemma (in group0) nat_pow_cancel_more:
assumes \( n\in nat \), \( k\leq n \), \( x\in G \)
shows \( (x^{-1})^{k}\cdot x^{n} = x^{n - k} \)proofIf \(k\leq n\) are natural numbers and \(x\) an element of the group, then \((x^{-1})^k\cdot x^n = x^(k-n)\).
lemma (in group0) nat_pow_cancel_more1:
assumes \( n\in nat \), \( k\leq n \), \( x\in G \)
shows \( x^{k}\cdot (x^{-1})^{n} = (x^{-1})^{n - k} \)proofIn this section we introduce notation basic properties of integer power in group context. The goal is to show that the power homomorphism property: if \(x\) is an element of the group and \(n,m\) are integers then \(x^{n+m}=x^n\cdot x^m\).
We extend the group0 context with some notation from int0 context. We also define notation for the integer power \( x^{z} \). The difficulty there is that in ZF set theory nonnegative integers and natural numbers are different things. However, standard Isabelle/ZF defines a meta-function nat_of that we can use to convert one into the other. Hence, we define the integer power \( x^{z} \) as \(x\) raised to the corresponding natural power if \(z\) is a nonnegative and \(x^{-1}\) raised to natural power corresponding to \(-z\) otherwise.
locale group_int0 = group0 +
defines \( \mathbb{Z} \equiv int \)
defines \( a + b \equiv IntegerAddition\langle a,b\rangle \)
defines \( - a \equiv \text{GroupInv}(\mathbb{Z} ,IntegerAddition)(a) \)
defines \( a - b \equiv a + ( - b) \)
defines \( 0 \equiv \text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition) \)
defines \( \mathbb{Z} ^+ \equiv \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder) \)
defines \( m \leq n \equiv \langle m,n\rangle \in IntegerOrder \)
defines \( a \lt b \equiv a\leq b \wedge a\neq b \)
defines \( x^{z} \equiv (\text{if } 0 \leq z\text{ then }x\text{ else }x^{-1})^{| z|_N } \)
If \(x\) is an element of the group and \(z_1,z_2\) are nonnegative integers then \(x^{z_1+z_2}=x^{z_1}\cdot x^{z_2}\), i.e. the power homomorphism property holds.
lemma (in group_int0) powz_hom_nneg_nneg:
assumes \( 0 \leq z_1 \), \( 0 \leq z_2 \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, add_nonneg_ints(1,2), nat_mult_addIf \(x\) is an element of the group and \(z_1,z_2\) are negative integers then the power homomorphism property holds.
lemma (in group_int0) powz_hom_neg_neg:
assumes \( z_1 \lt 0 \), \( z_2 \lt 0 \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, neg_not_nonneg, add_neg_ints(1,2), inverse_in_group, nat_mult_addWhen the integers are of different signs we further split into cases depending on which magnitude is greater. If \(x\) is an element of the group and \(z_1\) is nonnegative, \(z_2\) is negative and \(|z_2|\leq |z_1|\) then the power homomorphism property holds. The proof of this lemma is presented with more detail than necessary, to show the schema of the proofs of the remaining lemmas that we let Isabelle prove automatically.
lemma (in group_int0) powz_hom_nneg_neg1:
assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_2 \right|_N \leq \left| z_1 \right|_N \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)proofIf \(x\) is an element of the group and \(z_1\) is nonnegative, \(z_2\) is negative and \(|z_1|<|z_2|\) then the power homomorphism property holds.
lemma (in group_int0) powz_hom_nneg_neg2:
assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_1 \right|_N \lt \left| z_2 \right|_N \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, add_nonneg_neg2, neg_not_nonneg, leI, nat_pow_cancel_more1If \(x\) is an element of the group and \(z_1\) is negative, \(z_2\) is nonnegative and \(|z_1|\leq |z_2|\) then the power homomorphism property holds.
lemma (in group_int0) powz_hom_neg_nneg1:
assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_1 \right|_N \leq \left| z_2 \right|_N \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, add_neg_nonneg1, nat_pow_cancel_more, neg_not_nonnegIf \(x\) is an element of the group and \(z_1\) is negative, \(z_2\) is nonnegative and \(|z_2| < |z_1|\) then the power homomorphism property holds.
lemma (in group_int0) powz_hom_neg_nneg2:
assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_2 \right|_N \lt \left| z_1 \right|_N \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, add_neg_nonneg2, neg_not_nonneg, leI, nat_pow_cancel_less1The next theorem collects the results from the above lemmas to show the power homomorphism property holds for any pair of integer numbers and any group element.
theorem (in group_int0) powz_hom_prop:
assumes \( z_1\in \mathbb{Z} \), \( z_2\in \mathbb{Z} \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)proofassumes \( x\in G \)
shows \( x^{-1}\in G \)assumes \( n\in nat \), \( x\in G \)
shows \( x^{n + 1} = x^{n}\cdot x \) and \( x^{n + 1} = x\cdot x^{n} \)assumes \( n\in nat \), \( x\in G \)
shows \( n\cdot x \in G \)assumes \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)
shows \( a\oplus b\oplus (c\oplus d) = a\oplus (b\oplus c)\oplus d \)assumes \( x\in G \)
shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(k + 1) \)
shows \( P(n) \)assumes \( n\in nat \), \( x\in G \)
shows \( x^{n}\cdot (x^{-1})^{n} = 1 \)assumes \( a\in G \)
shows \( a = (a^{-1})^{-1} \)assumes \( n\in nat \), \( k\leq n \)
shows \( k\in nat \)assumes \( n\in nat \), \( m\in nat \), \( x\in G \)
shows \( (n + m)\cdot x = n\cdot x \oplus m\cdot x \)assumes \( a\in G \), \( b\in G \), \( c\in G \)
shows \( a\cdot (b\cdot c) = a\cdot b\cdot c \)assumes \( n\in nat \), \( k\leq n \), \( x\in G \)
shows \( x^{n}\cdot (x^{-1})^{k} = x^{n - k} \)assumes \( n\in nat \), \( x\in G \)
shows \( (x^{-1})^{n}\cdot x^{n} = 1 \)assumes \( n\in nat \), \( k\leq n \), \( x\in G \)
shows \( (x^{-1})^{k}\cdot x^{n} = x^{n - k} \)assumes \( 0 \leq z_1 \), \( 0 \leq z_2 \)
shows \( 0 \leq z_1 + z_2 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N + \left| z_2 \right|_N \), \( z_1 + z_2 = \$\!\#\! (\left| z_1 \right|_N + \left| z_2 \right|_N ) \)assumes \( m \lt 0 \)
shows \( \neg ( 0 \leq m) \)assumes \( z_1 \lt 0 \), \( z_2 \lt 0 \)
shows \( z_1 + z_2 \lt 0 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N + \left| z_2 \right|_N \), \( z_1 + z_2 = \ \$\!-\!(\$\!\#\!(\left| z_1 \right|_N + \left| z_2 \right|_N )) \)assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_2 \right|_N \leq \left| z_1 \right|_N \)
shows \( 0 \leq z_1 + z_2 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N - \left| z_2 \right|_N \), \( z_1 + z_2 = \$\!\#\!(\left| z_1 \right|_N - \left| z_2 \right|_N ) \)assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_2 \right|_N \leq \left| z_1 \right|_N \)
shows \( 0 \leq z_1 + z_2 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N - \left| z_2 \right|_N \), \( z_1 + z_2 = \$\!\#\!(\left| z_1 \right|_N - \left| z_2 \right|_N ) \)assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_1 \right|_N \lt \left| z_2 \right|_N \)
shows \( z_1 + z_2 \lt 0 \), \( \left| z_1 + z_2 \right|_N = \left| z_2 \right|_N - \left| z_1 \right|_N \), \( z_1 + z_2 = \ \$\!-\!(\$\!\#\!(\left| z_2 \right|_N - \left| z_1 \right|_N )) \)assumes \( n\in nat \), \( k\leq n \), \( x\in G \)
shows \( x^{k}\cdot (x^{-1})^{n} = (x^{-1})^{n - k} \)assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_1 \right|_N \leq \left| z_2 \right|_N \)
shows \( 0 \leq z_1 + z_2 \), \( \left| z_1 + z_2 \right|_N = \left| z_2 \right|_N - \left| z_1 \right|_N \), \( z_1 + z_2 = \$\!\#\!(\left| z_2 \right|_N - \left| z_1 \right|_N ) \)assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_2 \right|_N \lt \left| z_1 \right|_N \)
shows \( z_1 + z_2 \lt 0 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N - \left| z_2 \right|_N \), \( z_1 + z_2 = \ \$\!-\!(\$\!\#\!(\left| z_1 \right|_N - \left| z_2 \right|_N )) \)assumes \( n\in nat \), \( k\leq n \), \( x\in G \)
shows \( (x^{-1})^{n}\cdot x^{k} = (x^{-1})^{n - k} \)assumes \( z_1\in \mathbb{Z} \), \( z_2\in \mathbb{Z} \)
shows \( ( 0 \leq z_1 \wedge 0 \leq z_2) \vee (z_1 \lt 0 \wedge z_2 \lt 0 ) \vee \) \( ( 0 \leq z_1 \wedge z_2 \lt 0 \wedge \left| z_2 \right|_N \leq \left| z_1 \right|_N ) \vee \) \( ( 0 \leq z_1 \wedge z_2 \lt 0 \wedge \left| z_1 \right|_N \lt \left| z_2 \right|_N ) \vee \) \( (z_1 \lt 0 \wedge 0 \leq z_2 \wedge \left| z_1 \right|_N \leq \left| z_2 \right|_N ) \vee \) \( (z_1 \lt 0 \wedge 0 \leq z_2 \wedge \left| z_2 \right|_N \lt \left| z_1 \right|_N ) \)assumes \( 0 \leq z_1 \), \( 0 \leq z_2 \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)assumes \( z_1 \lt 0 \), \( z_2 \lt 0 \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_2 \right|_N \leq \left| z_1 \right|_N \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_1 \right|_N \lt \left| z_2 \right|_N \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_1 \right|_N \leq \left| z_2 \right|_N \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_2 \right|_N \lt \left| z_1 \right|_N \), \( x\in G \)
shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)