avewright/proofwiki-math huggingface dataset:
Theorem: Left Identity while exists Left Inverse for All is Identity

Let $\struct {S, \circ}$ be a semigroup with a left identity $e_L$ such that:
:$\forall x \in S: \exists x_L: x_L \circ x = e_L$
That is, every element of $S$ has a left inverse with respect to the left identity.
Then $e_L$ is also a right identity, that is, is an identity.

Proof:
From Left Inverse for All is Right Inverse we have that:
:$x \circ x_L = e_L$
Then:
{{begin-eqn}}
{{eqn | l = x \circ e_L
      | r = x \circ \paren {x_L \circ x}
      | c = {{Defof|Left Inverse Element}}
}}
{{eqn | r = \paren {x \circ x_L} \circ x
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = e_L \circ x
      | c = Left Inverse for All is Right Inverse
}}
{{eqn | r = x
      | c = {{Defof|Left Identity}}
}}
{{end-eqn}}
So $e_L$ behaves as a right identity as well as a left identity.
That is, by definition, $e_L$ is an identity element.
{{qed}}
Theorem: Right Inverse for All is Left Inverse

Let $\struct {S, \circ}$ be a semigroup with a right identity $e_R$ such that:
:$\forall x \in S: \exists x_R: x \circ x_R = e_R$
That is, every element of $S$ has a right inverse with respect to the right identity.
Then $x_R \circ x = e_R$, that is, $x_R$ is also a left inverse with respect to the right identity.

Proof:
Let $y = x_R \circ x$. Then:
{{begin-eqn}}
{{eqn | l = y \circ e_R
      | r = y \circ \paren {y \circ y_R}
      | c = {{Defof|Right Inverse Element}}
}}
{{eqn | r = \paren {y \circ y} \circ y_R
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = y \circ y_R
      | c = Product of Semigroup Element with Right Inverse is Idempotent: $y = x_R \circ x$
}}
{{eqn | r = e_R
      | c = {{Defof|Right Inverse Element}}
}}
{{end-eqn}}
So $x_R \circ x = e_R$, and $x_R$ behaves as a left inverse as well as a right inverse with respect to the right identity.
{{qed}}
Theorem: Equal Powers of Group Element implies Finite Order

Let $\struct {G, \circ}$ be a group.
Let $g \in G$ such that $g^r = g^s$ where $r, s \in \Z: r \ne s$.
Then there exists $m \in \Z_{>0}$ such that:
:$(1): \quad g^m = e$
:$(2): \quad 0 \le i < j < m \implies g^i \ne g^j$

Proof:
{{WLOG}}, suppose that $r > s$.
From $g^r = g^s$ it follows from Powers of Group Elements that:
: $g^{r - s} = g^r g^{-s} = g^s g^{-s} = e$
Thus there exists $t \in \Z_{>0}$ such that $g^t = e$.
Let $m \in \Z_{>0}$ be the smallest such that $g^m = e$.
Suppose $0 \le i < j < m$ such that $g^i = g^j$.
Then $g^{j - i} = e$ and $0 < j - i < m$.
This contradicts the choice of $m$ as the smallest $m \in \Z_{>0}$ such that $g^m = e$.
Hence the result.
{{qed}}
Theorem: Exponential on Complex Plane is Group Homomorphism

Let $\struct {\C, +}$ be the additive group of complex numbers.
Let $\struct {\C_{\ne 0}, \times}$ be the multiplicative group of complex numbers.
Let $\exp: \struct {\C, +} \to \struct {\C_{\ne 0}, \times}$ be the mapping:
:$x \mapsto \map \exp x$
where $\exp$ is the complex exponential function.
Then $\exp$ is a group homomorphism.

Proof:
If $z \in \C$, then by the definition of the complex exponential function, $\exp$ is a mapping $\C \to \C_{\ne 0}$.
Let $z_1, z_2 \in \C$.
By Exponential of Sum:
:$\map \exp {z_1 + z_2} = \map \exp {z_1} \, \map \exp {z_2}$
Therefore $\exp: \struct {\C, +} \to \struct {\C_{\ne 0}, \times}$ is a group homomorphism.
{{qed}}
Theorem: Group Direct Product is Product in Category of Groups

Let $\mathbf{Grp}$ be the category of groups.
Let $G$ and $H$ be groups, and let $G \times H$ be their direct product.
Then $G \times H$ is a binary product of $G$ and $H$ in $\mathbf{Grp}$.

Proof:
Let $F$ be a group.
By Direct Product of Group Homomorphisms is Homomorphism, given group homomorphisms:
:$g: F \to G, h: F \to H$
their direct product $g \times h: F \to G \times H$ is a group homomorphism.
From Projections on Direct Product of Group Homomorphisms, the following diagram is commutative:
:<nowiki>$\begin{xy}\xymatrix@L+3mu@R=3em{
&
 F
  \ar@/_/[dl]_*{g}
  \ar[d]^*{\quad g \times h}
  \ar@/^/[dr]^*{h}
\\
 G
&
 G \times H
  \ar[l]^*{\pr_1}
  \ar[r]_*{\pr_2}
&
 H
}\end{xy}$</nowiki>
By Cartesian Product is Set Product, $g \times h$ is the only mapping $F \to G \times H$ that could fit into the diagram.
Since it is also a group homomorphism, we see that the universal mapping property for the binary product is satisfied.
Thus the direct product $G \times H$ indeed is a categorical product for $G$ and $H$ in $\mathbf{Grp}$.
{{qed}}
Theorem: Product Category is Product in Category of Categories

Let $\mathbf{Cat}$ be the category of categories.
Let $\mathbf C$ and $\mathbf D$ be small categories, and let $\mathbf C \times \mathbf D$ be their product category.
Then $\mathbf C \times \mathbf D$ is a binary product of $\mathbf C$ and $\mathbf D$ in $\mathbf{Cat}$.

Proof:
Let $F: \mathbf A \to \mathbf C$ and $G: \mathbf A \to \mathbf D$ be morphisms in $\mathbf{Cat}$, i.e. functors.
Suppose $X: \mathbf A \to \mathbf C \times \mathbf D$ is a functor such that $\pr_1 \circ X = F$ and $\pr_2 \circ X = G$:
::<nowiki>$\begin{xy}\xymatrix@C=3em@R=3em@L+3mu{
&
 \mathbf A
  \ar[dl]_*{F}
  \ar[d]^*{X}
  \ar[dr]^*{G}
\\
 \mathbf C
&
 \mathbf C \times \mathbf D
  \ar[l]^*{\pr_1}
  \ar[r]_*{\pr_2}
&
 \mathbf D
}\end{xy}$</nowiki>
Here, $\pr_1$ and $\pr_2$ are projection functors.
Thus, for all objects $A$ of $\mathbf A$, it is required that:
:$\map {\pr_1} {X A} = F A$
:$\map {\pr_2} {X A} = G A$
meaning that $X A = \tuple {F A, G A}$ by definition of the objects of the product category $\mathbf C \times \mathbf D$.
Similarly, for all morphisms $f$ of $\mathbf A$, it is required that:
:$\map {\pr_1} {X f} = F f$
:$\map {\pr_2} {X f} = G f$
meaning that $X f = \tuple {F f, G f}$ by definition of the morphisms of the product category $\mathbf C \times \mathbf D$.
This uniquely determines the functor $X$, if it exists.
That this definition actually yields a functor is shown on Functor to Product Category.
Hence $\mathbf C \times \mathbf D$ is a binary product of $\mathbf C$ and $\mathbf D$ in $\mathbf{Cat}$.
{{qed}}
Theorem: Infimum is Product in Order Category

Let $\mathbf P$ be an order category whose ordering is $\preceq$.
Let $p, q \in \mathbf P_0$, and suppose that they have some infimum $r = \inf \set {p, q}$.
Then $r$ is a binary product of $p$ and $q$ in $\mathbf P$.

Proof:
Suppose that there are morphisms $l \to p$ and $l \to q$ in $\mathbf P$.
That is to say, suppose $l \preceq p$ and $l \preceq q$.
Then $l$ is a lower bound for $\set {p, q}$.
By definition of infimum, we then have:
:$l \preceq r = \inf \set {p, q}$
By definition of $\mathbf P$ as an order category, this means there is a morphism:
:$l \to r$
By definition of $\mathbf P$, this morphism is necessarily unique.
Thus $r$ satisfies the universal mapping property for the binary product of $p$ and $q$.
The result follows.
{{qed}}
Theorem: Cardinal of Union Less than Cardinal of Cartesian Product

Let $S$ and $T$ be sets that are equivalent to their cardinal numbers.
Let $\card S$ denote the cardinal number of $S$.
Let $\card S > 1$ and $\card T > 1$.
Then:
:$\card {S \cup T} \le \card {S \times T}$

Proof:
Let $x_1$ and $x_2$ be distinct elements of $S$.
Let $y_1$ and $y_2$ be distinct elements of $T$.
Define the mapping $f : S \times T \to S \cup T$ as follows:
$\quad\map f {x, y} = \begin {cases}
y &: x = x_1 \\
x_1 &: x = x_2 \land y = y_1 \\
x &: \text {otherwise}
\end {cases}$
If $x \in S$, then we have that either $x = x_1$ or $x \ne x_1$.
If $x \ne x_1$, then $\map f {x, y_2} = x$ by the definition of $f$.
If $x = x_1$, then $\map f {x_2, y_1} = x_1$ by the definition of $f$.
If $y \in S$, then we have that:
:$\map f {x_1, y} = y$ by the definition of $f$.
Therefore, it follows that $f : S \times T \to S \cup T$ is a surjection.
Thus by Surjection iff Cardinal Inequality:
:$\card {S \cup T} \le \card {S \times T}$
{{qed}}
Theorem: Cardinal Product Equinumerous to Ordinal Product

Let $S$ and $T$ be sets that are equivalent to their cardinal numbers.
Let $\card S$ denote the cardinal number of $S$.
Let $\cdot$ denote ordinal multiplication and let $\times$ denote the Cartesian product.
Then:
:$S \times T \sim \card S \cdot \card T$

Proof:
Let $f: S \to \card S$ and $g: T \to \card T$ be bijections.
Let $\cdot$ denote ordinal multiplication, while $\times$ shall denote the Cartesian product.
Define the function $F$ to be:
:$\forall x \in S, y \in T: \map F {x, y} = \card S \cdot \map g y + \map f x$
Suppose $\map F {x_1, y_1} = \map F {x_2, y_2}$.
{{begin-eqn}}
{{eqn | l = \card S \cdot \map g {y_1} + \map f {x_1}
      | r = \card S \cdot \map g {y_2} + \map f {x_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f {x_1}, \map f {x_2}
      | o = \in
      | r = \card S
      | c = {{Defof|Mapping}} $f$
}}
{{eqn | ll= \leadsto
      | l = \map f {x_1}
      | r = \map f {x_2}
      | c = Division Theorem for Ordinals
}}
{{eqn | lo = \land
      | l = \map g {y_1}
      | r = \map g {y_2}
}}
{{eqn | ll= \leadsto
      | l = x_1
      | r = x_2
      | c = {{Defof|Bijection}}
}}
{{eqn | lo= \land
      | l = y_1
      | r = y_2
}}
{{end-eqn}}
It follows that $F: S \times T \to \card S \cdot \card T$ is a injection.
{{qed|lemma}}
Furthermore, take any $z \in \card S \cdot \card T$.
By Division Theorem for Ordinals, it follows that:
:$z = \card S \cdot a + b$ for some unique $a$ and $b \in \card S$.
Moreover, $a \in \card T$ since otherwise, this would contradict the fact that $z \in \card S \cdot \card T$.
Therefore, $a = \map f x$ for some $x \in S$ and $b = \map g y$ for some $y \in T$.
Thus, $F : S \times T \to \card S \cdot \card T$ is a surjection.
{{qed|lemma}}
Therefore, $F : S \times T \to \card S \cdot \card T$ is a bijection.
By Condition for Set Equivalent to Cardinal Number, it follows that:
:$S \times T \sim \card S \cdot \card T$
{{qed}}
Category:Cardinals
Category:Ordinal Arithmetic
oodwmkhliesjk445gl70vdqsi7jbzbf
Theorem: Product of Finite Sets is Finite

Let $S$ and $T$ be finite sets.
Then $S \times T$ is a finite set.

Proof:
By the definition of Cartesian product:
:$S \times T = \set {\tuple {s, t}: s \in S, t \in T}$
Then by definition of set union:
:$S \times T = \ds \bigcup_{s \mathop \in S} \set s \times T$
Also, the mapping $g_s: \set s \times T \to T$ defined by:
:$\map {g_s} {s, t} = t$
is a bijection.
Therefore, since $T$ is finite, so is $\set s \times T$ for all $s \in S$.
Since $S$ is finite, the result follows from Finite Union of Finite Sets is Finite.
{{qed}}
Theorem: Product of Finite Sets is Finite

Let $S$ and $T$ be finite sets.
Then $S \times T$ is a finite set.

Proof:
Let $\card S$ denote the cardinal number of $S$.
Let $\cdot$ denote ordinal multiplication.
By Cardinal Product Equinumerous to Ordinal Product, it follows that $S \times T \sim \card S \cdot \card T$.
But then $\card S$ and $\card T$ are members of the minimally inductive set.
Therefore, $\card S \cdot \card T \in \omega$ by Natural Number Multiplication is Closed.
Since $S \times T$ is equinumerous to a member of the minimally inductive set, it follows that $S \times T$ is finite.
{{qed}}
Theorem: Union of Finite Sets is Finite

Let $S$ and $T$ be finite sets.
Then $S \cup T$ is a finite set.

Proof:
The proof proceeds by induction.
Let $S$ be a finite set with cardinality $n$.
If $n = 0$ then $S = \O$, so $\bigcup S = \O$, which is finite.
Suppose that an arbitrary finite set with cardinality $n$ of finite sets has a finite union.
Let $S$ have cardinality $n^+$.
Then there is a bijection $f: n^+ \to S$.
Then:
:$\ds \bigcup S = \bigcup_{k \mathop \in n^+} \map f k = \bigcup_{k \mathop \in n} \map f k \cup \map f n$
{{explain|Explain in detail.}}
By Union of Finite Sets is Finite, $\bigcup S$ is finite.
{{qed}}
Theorem: Union of Finite Sets is Finite

Let $S$ and $T$ be finite sets.
Then $S \cup T$ is a finite set.

Proof:
Let $S = \set {A_1, \ldots, A_n}$ such that $A_k$ is finite $\forall k = 1, \ldots, n$.
Set:
: $m = \max \set {\card {A_1}, \ldots, \card {A_n} }$
Then:
: $\ds \card {\bigcup_{k \mathop = 1}^n A_k} \le \sum_{k \mathop = 1}^n \card {A_k} \le \sum_{k \mathop = 1}^n m = n m$
{{explain|needs to invoke a link to result that shows $\card {\bigcup_{k \mathop {{=}} 1}^n A_k} \le \sum_{k \mathop {{=}} 1}^n \card {A_k}$}}
Hence the result.
{{qed}}
Theorem: Union of Finite Sets is Finite

Let $S$ and $T$ be finite sets.
Then $S \cup T$ is a finite set.

Proof:
If $S$ or $T$ is empty, the result is trivial.
Otherwise, let $f: \N_{<n} \to S$ and $g: \N_{<m} \to T$ be bijections, where $\N_{<n}$ is an initial segment of $\N$.
Now define $h: \N_{< n + m} \to S \cup T$ by:
:$\map h i = \begin{cases} \map f i : & \text {if $i < n$} \\ \map g {i - n} : & \text{if $i \ge n$} \end{cases}$
By Set Finite iff Surjection from Initial Segment of Natural Numbers, it suffices to show that $h$ is surjective.
Let $s \in S$.
Then:
{{begin-eqn}}
{{eqn | l = \map h {\map {f^{-1} } s}
      | r = \map f {\map {f^{-1} } s}
      | c = as $\map {f^{-1} } s \in \N_{<n}$
}}
{{eqn | r = s
      | c = Definition of $f^{-1}$
}}
{{end-eqn}}
Next let $t \in T$. 
We have that:
:$n + \map {g^{-1} } t < n + m$
so that:
:$n + \map {g^{-1} } t \in \N_{< n + m}$
Then:
{{begin-eqn}}
{{eqn | l = \map h { n + \map {g^{-1} } t}
      | r = \map g {n + \map {g^{-1} } t - n}
      | c = as $\map {g^{-1} } t \ge 0$ and so $n + \map {g^{-1} } t \ge n$
}}
{{eqn | r = \map g {\map {g^{-1} } t}
}}
{{eqn | r = t
      | c = Definition of $g^{-1}$
}}
{{end-eqn}}
Thus it has been shown that for all $s \in S$ and $t \in T$, there exists an element of $\N_{< n + m}$ which maps to it.
So by definition of set union, for all $x \in S \cup T$:
:$\exists y \in \N_{< n + m}: \map h y = x$
Hence, by definition, $h$ is a surjection.
Therefore $S \cup T$ is finite.
{{qed}}
Theorem: Union of Finite Sets is Finite

Let $S$ and $T$ be finite sets.
Then $S \cup T$ is a finite set.

Proof:
Note that $\card {S \cup T} \le \card {S \times T}$ by Cardinal of Union Less than Cardinal of Cartesian Product.
The theorem follows from the fact that $S \times T$ is finite by Product of Finite Sets is Finite.
{{qed}}
Theorem: Ordinal is Finite iff Natural Number

Let $x$ be an ordinal.
Then $x$ is a finite set {{iff}} $x$ is an element of the minimally inductive set.

Proof:
$x$ is finite {{iff}} $x \sim \N_n$ for some $n \in \N$, by definition.
But $x$ is an ordinal, and by definition, it is equal to its initial segment.
By definition of the von Neumann construction of natural numbers, it follows that $x \sim n$ for some $n$.
By Finite Ordinal is equal to Natural Number, it follows that $x$ is equal to $n$.
Thus, $x$ is an element of the minimally inductive set.
{{qed}}
Theorem: Cardinal Inequality implies Ordinal Inequality

Let $T$ be a set.
Let $\card T$ denote the cardinal number of $T$.
Let $x$ be an ordinal.
Then:
:$x < \card T \iff \card x < \card T$

Proof:
=== Sufficient Condition ===
By Cardinal Number Less than Ordinal, it follows that $\card x \le x$.
So if $x < \card T$, then $\card x < \card T$.
{{qed|lemma}}
Theorem: Cardinal Number Plus One Less than Cardinal Product

Let $x$ be an ordinal such that $x > 1$.
Then:
:$\card {x + 1} \le \card {x \times x}$
Where $\times$ denotes the Cartesian product.

Proof:
Since $x > 1$, then $0 < x$ and $1 < x$.
Define the function $f: x + 1 \to x \times x$ as follows:
:$\map f y = \begin{cases}
\tuple {y, 0} &: y < x \\
\tuple {0, 1} &: y = x
\end{cases}$
If $\map f y = \map f z$, then $y = z$ by cases.
Theorem: Non-Finite Cardinal is equal to Cardinal Product

Let $\omega$ denote the minimally inductive set.
Let $x$ be an ordinal such that $x \ge \omega$.
Then:
:$\card x = \card {x \times x}$
where $\times$ denotes the Cartesian product.

Proof:
The proof shall proceed by Transfinite Induction on $x$.
Let:
:$\forall y \in x: y < \omega \lor \card y = \card {y \times y}$
There are two cases:
Theorem: Permutation is Cyclic iff At Most One Non-Trivial Orbit

Let $S$ be a set.
Let $\rho: S \to S$ be a permutation on $S$.
Then:
:$\rho$ is a cyclic permutation
{{iff}}:
:$S$ has no more than one orbit under $\rho$ with more than one element.

Proof:
=== Necessary Condition ===
{{ProofWanted}}
Theorem: Infinite Ramsey's Theorem implies Finite Ramsey's Theorem

:$\forall l, n, r \in \N: \exists m \in \N: m \to \left({l}\right)_r^n$
where $\alpha \to \left({\beta}\right)^n_r$ means that:
:for any assignment of $r$-colors to the $n$-subsets of $\alpha$
::there is a particular color $\gamma$ and a subset $X$ of $\alpha$ of size $\beta$ such that all $n$-subsets of $X$ are $\gamma$.

Proof:
{{AimForCont}} there is a $l$ such that:
:$\forall m \in \N: m \nrightarrow \left({l}\right)_r^n$
Let $\hat{K_i}$ denote a hypergraph on $i$ vertices where all possible $n$-subsets of the vertices are the hyperedges.
Let $G$ be a hypergraph with vertices $V = \left\{ {v_i: i \in \N}\right\}$.
Let the hyperedges of $G <$ be enumerated by:
:$E = \left\{ {E_i: E_i \subset \N, \left\vert{E_i}\right\vert = n}\right\}$
{{explain|What does $G <$ mean?}}
We construct a (rooted) tree $T$ as follows:
$(1): \quad$ First introduce a root node $r t$.
$(2): \quad$ Each node is allowed to have at most $r<$ children which correspond to the $r$-colors, subject to it satisfying the criteria:
{{explain|What does $r <$ mean?}}
:::A child is always labeled by one among the $r$-colors.
:::Let the colors be denoted $c_1, c_2, \ldots, c_r$.
$(3): \quad$ A child $c_i$ is '''permitted''' {{iff}} its introduction creates a path of some finite length $k$ starting from the root.
:::So, if the hyperedges $E_1, E_2, \ldots, E_k$ are colored by the colors used in the path in the same order, then the corresponding subgraph of $G$ does not contain a monochromatic $\hat{K_l}$.
:::For example: if the introduction of a child $c_i$ creates the $k$ length path $r t, c_a, c_b, \ldots, c_i$ and the hyperedges $E_1, E_2, \ldots, E_k$ when colored $c_a, c_b, \ldots, c_i$ do not contain a monochromatic $\hat{K_l}$, the child $c_i$ is permitted to be added to $T$.
Note that for all $m$, there always exists a coloring of $\hat{K_m}$ such that no monochromatic $\hat{K_l}$ exists within.
Thus the situation that a child cannot be added to any vertex at a given level $k$ cannot arise.
For we can always take a coloring of $\hat{K_{k+n}}$ containing no monochromatic $\hat{K_l}$.
Since any $k$ hyperedges in it would yield a sequence of colors already existing in $T$, we know which vertex to add the child to.
We give the child the color corresponding to any other edge.
Hence we can forever keep adding children and so $T$ is infinite.
It is also obvious that each level $k$ of $T$ has at most $r^k<$ vertices.
So each level is finite.
By König's Tree Lemma there will be an infinite path $P$ in $T$.
$P$ provides a $r$-coloring of $G$ that contains no monochromatic $\hat{K_i}$.
Hence $P$ contains no monochromatic infinite hypergraph.
This contradicts the Infinite Ramsey's Theorem.
The result follows by Proof by Contradiction.
{{qed}}
Category:Ramsey Theory
395v9fu5l1ys7ixrqgimfyxdxsvz4wr
Theorem: Identity Morphism of Product

Let $\mathbf C$ be a metacategory.
Let $C$ and $D$ be objects of $\mathbf C$, and let $C \times D$ be a binary product for $C$ and $D$.
Then:
:$\operatorname{id}_{\paren {C \mathop \times D} } = \operatorname{id}_C \times \operatorname{id}_D$
where $\operatorname{id}$ denotes an identity morphism, and $\times$ signifies a product of morphisms.

Proof:
By definition of the product morphism $\operatorname{id}_C \times \operatorname{id}_D$, it is the unique morphism making:
$\quad\quad \begin{xy}\xymatrix@+1em@L+5px{
C
\ar[d]_*+{\operatorname{id}_C}
&
C \times D
\ar[l]_*+{\pr_1}
\ar[r]^*+{\pr_2}
\ar@{-->}[d]^*+{\operatorname{id}_C \times \operatorname{id}_D}
&
D
\ar[d]^*+{\operatorname{id}_D}
\\
C
&
C \times D
\ar[l]^*+{\pr_1}
\ar[r]_*+{\pr_2}
&
D
}\end{xy}$
a commutative diagram.
It is immediate by the behaviour of identity morphisms that $\operatorname{id}_{\paren {C \mathop \times D} }$ is the unique morphism sought.
{{qed}}
Category:Morphisms
qa6fw7gsi3ga1hpm1xopso6tzy6gy56
Theorem: Cartesian Product Preserves Cardinality

Let $R$, $S$, and $T$ be sets.
Suppose that $S$ is equivalent to $T$.
Then:
:$R \times S \sim R \times T$
:$S \times R \sim T \times R$

Proof:
Since $S$ and $T$ are equivalent, there exists a bijection $f: S \to T$.
Let $g: T \to S$ be the inverse of $f$; its existence is assured by Bijection iff Left and Right Inverse.
Define $\hat f: R \times S \to R \times T$ by:
:$\map {\hat f} {r, s} := \tuple {r, \map f s}$
Next, define $\hat g: R \times T \to R \times S$ by:
:$\map {\hat g} {r, t} := \tuple {r, \map g t}$
Then, for all $\tuple {r, s} \in R \times S$:
{{begin-eqn}}
{{eqn | l = \hat g \circ \map {\hat f} {r, s}
      | r = \map {\hat g} {r, \map f s}
}}
{{eqn | r = \tuple {r, \map g {\map f s} }
}}
{{eqn | r = \tuple {r, s}
      | c = $g$ is the inverse of $f$
}}
{{end-eqn}}
Similarly, for all $\tuple {r, t} \in R \times T$:
{{begin-eqn}}
{{eqn | l = \hat f \circ \map {\hat g} {r, s}
      | r = \map {\hat f} {r, \map g s}
}}
{{eqn | r = \tuple {r, \map f {\map g s} }
}}
{{eqn | r = \tuple {r, s}
      | c = $g$ is the inverse of $f$
}}
{{end-eqn}}
Thus, it follows that $\hat g$ is a inverse for $\hat f$.
From Bijection iff Left and Right Inverse, we conclude $\hat f$ is a bijection.
Hence $R \times S \sim R \times T$, by definition of set equivalence.
And {{mutatis}}, the other relation also follows.
{{qed}}
Category:Cartesian Product
o9ro01qf0oemsdd05q6ldg4hcl34kzc
Theorem: Product of Composite Morphisms

Let $\mathbf C$ be a metacategory.
Let $f \times f': A \times A' \to B \times B'$ and $g \times g': B \times B' \to C \times C'$ be two composable products of morphisms in $\mathbf C$.
Then:
:$\paren {g \circ f} \times \paren {g' \circ f'} = \paren {g \times g'} \circ \paren {f \times f'}$
where $\times$ signifies product of morphisms.

Proof:
The situation is efficiently captured in the following commutative diagram:
$\quad\quad \begin{xy}
<-5em,0em>*+{A}            = "A",
<0em,0em>*+{A \times A'}   = "P",
<5em,0em>*+{A'}            = "A2",
<-5em,-5em>*+{B}           = "B",
<0em,-5em>*+{B \times B'}  = "Q",
<5em,-5em>*+{B'}           = "B2",
<-5em,-10em>*+{C}          = "C",
<0em,-10em>*+{C \times C'} = "R",
<5em,-10em>*+{C'}          = "C2",
"P";"A"  **@{-} ?>*@{>} ?*!/^.8em/{\pr_1},
"P";"A2" **@{-} ?>*@{>} ?*!/_.8em/{\pr_2},
"Q";"B"  **@{-} ?>*@{>} ?*!/^.8em/{\pr_1},
"Q";"B2" **@{-} ?>*@{>} ?*!/_.8em/{\pr_2},
"R";"C"  **@{-} ?>*@{>} ?*!/_.8em/{\pr_1},
"R";"C2" **@{-} ?>*@{>} ?*!/^.8em/{\pr_2},
"A";"B"   **@{-} ?>*@{>}  ?*!/^.8em/{f},
"A2";"B2" **@{-} ?>*@{>}  ?*!/_.8em/{f'},
"P";"Q"   **@{--} ?>*@{>} ?*!/_1.4em/{f \times f'},
"B";"C"   **@{-} ?>*@{>}  ?*!/^.8em/{g},
"B2";"C2" **@{-} ?>*@{>}  ?*!/_.8em/{g'},
"Q";"R"   **@{--} ?>*@{>} ?*!/_1.4em/{g \times g'},
\end{xy}$
The result is immediate from deleting the $B$s:
$\quad\quad \begin{xy}
<-5em,0em>*+{A}            = "A",
<0em,0em>*+{A \times A'}   = "P",
<5em,0em>*+{A'}            = "A2",
<-5em,-10em>*+{C}          = "C",
<0em,-10em>*+{C \times C'} = "R",
<5em,-10em>*+{C'}          = "C2",
"P";"A"  **@{-} ?>*@{>} ?*!/^.8em/{\pr_1},
"P";"A2" **@{-} ?>*@{>} ?*!/_.8em/{\pr_2},
"R";"C"  **@{-} ?>*@{>} ?*!/_.8em/{\pr_1},
"R";"C2" **@{-} ?>*@{>} ?*!/^.8em/{\pr_2},
"A";"C"   **@{-} ?>*@{>}  ?*!/^1.1em/{g \circ f},
"A2";"C2" **@{-} ?>*@{>}  ?*!/_1.3em/{g' \circ f'},
"P";"R"   **@{--} ?>*@{>} ?*!/_2em/{\paren {g \circ f} \times \\ \paren {g' \circ f'} },
\end{xy}$
The uniqueness of $\paren {g \circ f} \times \paren {g' \circ f'}$ implies it equals $\paren {g \times g'} \circ \paren {f \times f'}$.
{{qed}}
Category:Product Categories
Category:Morphisms
7zigrh1us4elua8j4fgh9kvhqel1fbr