TheoremBase

Each clause is reduced to iterated operations along an enumeration: disjoint unions by concatenating enumerations and splitting, reindexing by composing an enumeration with the bijection, products of sets by induction on the number of elements, and the interval rules by disjoint unions and shifts. Empty sets are handled by the neutral element.

Proof

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Throughout, for a finite set CC and a map u:C→Xu:C\to X we use Sums and Products over a Finite Set and over an Interval §operation and Sums and Products over a Finite Set and over an Interval §empty as follows: if C=∅C=\emptyset, then ∗x∈Cu(x)=e\mathop{\ast}\limits_{x\in C}u(x)=e; if C≠∅C\neq\emptyset, then #C∈N\#C\in\mathbb{N} by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration §nonempty, and ∗x∈Cu(x)=∗k=1#Cu(γ(k))\mathop{\ast}\limits_{x\in C}u(x)=\mathop{\ast}\limits_{k=1}^{\#C}u(\gamma(k)) for every bijection γ\gamma from [#C][\#C] onto CC. If there is a bijection from [n][n] onto CC with n∈N0n\in\mathbb{N}_{0}, then n=#Cn=\#C by The Number of Elements of a Finite Set §cardinality. For uu defined on a set containing CC, the iterated operation over CC is that of u∣Cu|_{C} by Sums and Products over a Finite Set and over an Interval §subsets, and u∣Cu|_{C} has the same values as uu on CC; we use this without comment. Finally e∗x=x∗e=xe\ast x=x\ast e=x for every x∈Xx\in X by Associative and Commutative Binary Operations, and Neutral Elements §neutral.

Singleton. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, [1]={1}[1]=\{1\}, so γ:[1]→{y}\gamma:[1]\to\{y\}, 1↦y1\mapsto y, is a bijection and #{y}=1\#\{y\}=1. By the first part of Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §recursion, applied with n=1n=1 to the map k↦f(γ(k))k\mapsto f(\gamma(k)) on [1][1], ∗k=11f(γ(k))=f(γ(1))\mathop{\ast}\limits_{k=1}^{1}f(\gamma(k))=f(\gamma(1)). Hence ∗x∈{y}f(x)=f(γ(1))=f(y)\mathop{\ast}\limits_{x\in\{y\}}f(x)=f(\gamma(1))=f(y).

Disjoint union. If A=∅A=\emptyset, then A∪B=BA\cup B=B, and the right side is e∗∗x∈Bf(x)=∗x∈Bf(x)e\ast\mathop{\ast}\limits_{x\in B}f(x)=\mathop{\ast}\limits_{x\in B}f(x), which is the left side; the case B=∅B=\emptyset is symmetric. Let AA and BB be nonempty, p=#Ap=\#A and q=#Bq=\#B, so p,q∈Np,q\in\mathbb{N}, and let α\alpha and β\beta be bijections from [p][p] onto AA and from [q][q] onto BB. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §split with m=1m=1, n=pn=p and qq in place of pp, whose hypothesis 1≤p+11\le p+1 holds as 0≤p0\le p gives 1=0+1≤p+11=0+1\le p+1 by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §laws, [p+q][p+q] is the union of the disjoint sets [p][p] and {p+1,…,p+q}\{p+1,\dots,p+q\}, and by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift with m=1m=1, n=qn=q every element of the latter is p+jp+j for exactly one j∈[q]j\in[q]; that is, j↦j+p=p+jj\mapsto j+p=p+j is a bijection from [q][q] onto {p+1,…,p+q}\{p+1,\dots,p+q\}, and we let θ\theta be its inverse, a bijection from {p+1,…,p+q}\{p+1,\dots,p+q\} onto [q][q] by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse. Define γ:[p+q]→A∪B\gamma:[p+q]\to A\cup B by γ(k)=α(k)\gamma(k)=\alpha(k) for k∈[p]k\in[p] and γ(k)=β(θ(k))\gamma(k)=\beta(\theta(k)) for the other k∈[p+q]k\in[p+q], a map by Maps Defined by Cases §cases with P(k)P(k) the property k∈[p]k\in[p]: for k∈[p]k\in[p], α(k)∈A\alpha(k)\in A, and for the other kk, k∈{p+1,…,p+q}k\in\{p+1,\dots,p+q\} and β(θ(k))∈B\beta(\theta(k))\in B. Thus γ(p+j)=β(j)\gamma(p+j)=\beta(j) for j∈[q]j\in[q]. Then γ\gamma maps [p][p] bijectively onto AA and {p+1,…,p+q}\{p+1,\dots,p+q\} bijectively onto BB. Since A∩B=∅A\cap B=\emptyset, two elements of [p+q][p+q] with the same image lie in the same one of these two pieces, so γ\gamma is injective; it is evidently surjective. Thus γ\gamma is a bijection from [p+q][p+q] onto A∪BA\cup B, and Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §splitting, applied to k↦f(γ(k))k\mapsto f(\gamma(k)), gives

∗x∈A∪Bf(x)=∗k=1p+qf(γ(k))=(∗k=1pf(α(k)))∗(∗j=1qf(β(j)))=(∗x∈Af(x))∗(∗x∈Bf(x)).\mathop{\ast}\limits_{x\in A\cup B}f(x)=\mathop{\ast}\limits_{k=1}^{p+q}f(\gamma(k))=\Big(\mathop{\ast}\limits_{k=1}^{p}f(\alpha(k))\Big)\ast\Big(\mathop{\ast}\limits_{j=1}^{q}f(\beta(j))\Big)=\Big(\mathop{\ast}\limits_{x\in A}f(x)\Big)\ast\Big(\mathop{\ast}\limits_{x\in B}f(x)\Big).

Reindexing. If B=∅B=\emptyset, then A=g(B)=∅A=g(B)=\emptyset, and both sides are ee. Let B≠∅B\neq\emptyset, n=#Bn=\#B, and let β\beta be a bijection from [n][n] onto BB. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §preservation, g∘βg\circ\beta is a bijection from [n][n] onto AA, so A≠∅A\neq\emptyset and #A=n\#A=n. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition,

∗y∈Bf(g(y))=∗k=1nf(g(β(k)))=∗k=1nf((g∘β)(k))=∗x∈Af(x).\mathop{\ast}\limits_{y\in B}f(g(y))=\mathop{\ast}\limits_{k=1}^{n}f(g(\beta(k)))=\mathop{\ast}\limits_{k=1}^{n}f\big((g\circ\beta)(k)\big)=\mathop{\ast}\limits_{x\in A}f(x).

Product. First let A={a}A=\{a\} be a singleton. The map y↦(a,y)y\mapsto(a,y) from BB to {a}×B\{a\}\times B and the map (a,y)↦y(a,y)\mapsto y back are inverse to each other, so the former is a bijection by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion. Reindexing along it and the singleton clause give

∗(x,y)∈{a}×Bf(x,y)=∗y∈Bf(a,y)=∗x∈{a}(∗y∈Bf(x,y)).(1)\mathop{\ast}\limits_{(x,y)\in\{a\}\times B}f(x,y)=\mathop{\ast}\limits_{y\in B}f(a,y)=\mathop{\ast}\limits_{x\in\{a\}}\Big(\mathop{\ast}\limits_{y\in B}f(x,y)\Big).\qquad(1)

We prove the first equality of the clause. If A=∅A=\emptyset, then A×B=∅A\times B=\emptyset and both sides are ee. We prove the first equality for nonempty AA by induction from 11 on n=#An=\#A (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction), for all finite AA with #A=n\#A=n and all ff; here n∈Nn\in\mathbb{N}. If #A=1\#A=1, a bijection from [1]={1}[1]=\{1\} onto AA shows that AA is a singleton, so the claim holds by (1). Suppose it holds for nn, let #A=n+1\#A=n+1, and let α\alpha be a bijection from [n+1][n+1] onto AA. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, [n+1]=[n]∪{n+1}[n+1]=[n]\cup\{n+1\} and n+1∉[n]n+1\notin[n]. Put A′=α([n])A'=\alpha([n]) and a=α(n+1)a=\alpha(n+1). Then A=A′∪{a}A=A'\cup\{a\}, a∉A′a\notin A' as α\alpha is injective, and α∣[n]\alpha|_{[n]} is a bijection from [n][n] onto A′A', so #A′=n\#A'=n. Hence A×BA\times B is the union of the disjoint sets A′×BA'\times B and {a}×B\{a\}\times B. The disjoint-union clause, the induction hypothesis for A′A' and f∣A′×Bf|_{A'\times B}, (1), and the disjoint-union clause for A=A′∪{a}A=A'\cup\{a\} and the map x↦∗y∈Bf(x,y)x\mapsto\mathop{\ast}\limits_{y\in B}f(x,y) give

∗(x,y)∈A×Bf(x,y)=(∗x∈A′∗y∈Bf(x,y))∗(∗x∈{a}∗y∈Bf(x,y))=∗x∈A(∗y∈Bf(x,y)).\mathop{\ast}\limits_{(x,y)\in A\times B}f(x,y)=\Big(\mathop{\ast}\limits_{x\in A'}\mathop{\ast}\limits_{y\in B}f(x,y)\Big)\ast\Big(\mathop{\ast}\limits_{x\in\{a\}}\mathop{\ast}\limits_{y\in B}f(x,y)\Big)=\mathop{\ast}\limits_{x\in A}\Big(\mathop{\ast}\limits_{y\in B}f(x,y)\Big).

So the claim holds for n+1n+1. This proves the first equality for every finite AA.

For the second equality, the map τ:B×A→A×B\tau:B\times A\to A\times B, (y,x)↦(x,y)(y,x)\mapsto(x,y), is a bijection by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion, the corresponding map A×B→B×AA\times B\to B\times A being its inverse. Reindexing along τ\tau, and then the first equality with the roles of AA and BB exchanged, applied to f∘τf\circ\tau, give

∗(x,y)∈A×Bf(x,y)=∗(y,x)∈B×Af(x,y)=∗y∈B(∗x∈Af(x,y)).\mathop{\ast}\limits_{(x,y)\in A\times B}f(x,y)=\mathop{\ast}\limits_{(y,x)\in B\times A}f(x,y)=\mathop{\ast}\limits_{y\in B}\Big(\mathop{\ast}\limits_{x\in A}f(x,y)\Big).

Termwise. If A=∅A=\emptyset, both sides are e=e∗ee=e\ast e. Otherwise, with n=#An=\#A and a bijection γ\gamma from [n][n] onto AA, Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §termwise applied to k↦f(γ(k))k\mapsto f(\gamma(k)) and k↦g(γ(k))k\mapsto g(\gamma(k)) gives

∗x∈A(f(x)∗g(x))=∗k=1n(f(γ(k))∗g(γ(k)))=(∗k=1nf(γ(k)))∗(∗k=1ng(γ(k)))=(∗x∈Af(x))∗(∗x∈Ag(x)).\mathop{\ast}\limits_{x\in A}\big(f(x)\ast g(x)\big)=\mathop{\ast}\limits_{k=1}^{n}\big(f(\gamma(k))\ast g(\gamma(k))\big)=\Big(\mathop{\ast}\limits_{k=1}^{n}f(\gamma(k))\Big)\ast\Big(\mathop{\ast}\limits_{k=1}^{n}g(\gamma(k))\Big)=\Big(\mathop{\ast}\limits_{x\in A}f(x)\Big)\ast\Big(\mathop{\ast}\limits_{x\in A}g(x)\Big).

Homomorphism. If A=∅A=\emptyset, the left side is φ(e)=e′\varphi(e)=e', which is the right side. Otherwise, with n=#An=\#A and a bijection γ\gamma from [n][n] onto AA, used for both ∗\ast and ⋄\diamond, Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §homomorphism gives

φ(∗x∈Af(x))=φ(∗k=1nf(γ(k)))=⋄k=1nφ(f(γ(k)))=⋄x∈Aφ(f(x)).\varphi\Big(\mathop{\ast}\limits_{x\in A}f(x)\Big)=\varphi\Big(\mathop{\ast}\limits_{k=1}^{n}f(\gamma(k))\Big)=\mathop{\diamond}\limits_{k=1}^{n}\varphi(f(\gamma(k)))=\mathop{\diamond}\limits_{x\in A}\varphi(f(x)).

Interval recursion. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §split with p=1p=1, whose hypothesis m≤n+1m\le n+1 is assumed, {m,…,n+1}\{m,\dots,n+1\} is the union of the disjoint sets {m,…,n}\{m,\dots,n\} and {n+1,…,n+1}={n+1}\{n+1,\dots,n+1\}=\{n+1\}. By Sums and Products over a Finite Set and over an Interval §intervals and the disjoint-union and singleton clauses,

∗k=mn+1ak=(∗k∈{m,…,n}ak)∗(∗k∈{n+1}ak)=(∗k=mnak)∗an+1.\mathop{\ast}\limits_{k=m}^{n+1}a_{k}=\Big(\mathop{\ast}\limits_{k\in\{m,\dots,n\}}a_{k}\Big)\ast\Big(\mathop{\ast}\limits_{k\in\{n+1\}}a_{k}\Big)=\Big(\mathop{\ast}\limits_{k=m}^{n}a_{k}\Big)\ast a_{n+1}.

Interval shift. Let I={m,…,n}I=\{m,\dots,n\} and J={m+p,…,n+p}J=\{m+p,\dots,n+p\}, both finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §naturals. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift, s:I→Js:I\to J, k↦k+pk\mapsto k+p, is a bijection. In particular k+p∈Jk+p\in J for every k∈Ik\in I, so k↦ak+pk\mapsto a_{k+p} is a map from II to XX, and both sides of the clause are defined by Sums and Products over a Finite Set and over an Interval §intervals, since ∗\ast has the neutral element ee; this covers the case m>nm>n, in which I=∅I=\emptyset and J=s(I)=∅J=s(I)=\emptyset, so that both sides equal ee. Let b=a∣J:J→Xb=a|_{J}:J\to X, so that b(s(k))=ak+pb(s(k))=a_{k+p} for k∈Ik\in I. By Sums and Products over a Finite Set and over an Interval §intervals and the reindexing clause applied to the bijection s:I→Js:I\to J and the map bb,

∗k=mnak+p=∗k∈Ib(s(k))=∗j∈Jb(j)=∗k=m+pn+pak.\mathop{\ast}\limits_{k=m}^{n}a_{k+p}=\mathop{\ast}\limits_{k\in I}b(s(k))=\mathop{\ast}\limits_{j\in J}b(j)=\mathop{\ast}\limits_{k=m+p}^{n+p}a_{k}.

Citations

Loading…

Dependencies

Uses0

Loading…

Comments

Log in to comment.

Loading…