avewright/proofwiki-math huggingface dataset:
Theorem: Composite of Group Homomorphisms is Homomorphism

Let:
:$\struct {G_1, \circ}$
:$\struct {G_2, *}$
:$\struct {G_3, \oplus}$
be groups.
Let:
:$\phi: \struct {G_1, \circ} \to \struct {G_2, *}$
:$\psi: \struct {G_2, *} \to \struct {G_3, \oplus}$
be homomorphisms.
Then the composite of $\phi$ and $\psi$ is also a homomorphism.

Proof:
A specific instance of Composite of Homomorphisms on Algebraic Structure is Homomorphism.
{{qed}}
Theorem: Composite of Group Homomorphisms is Homomorphism

Let:
:$\struct {G_1, \circ}$
:$\struct {G_2, *}$
:$\struct {G_3, \oplus}$
be groups.
Let:
:$\phi: \struct {G_1, \circ} \to \struct {G_2, *}$
:$\psi: \struct {G_2, *} \to \struct {G_3, \oplus}$
be homomorphisms.
Then the composite of $\phi$ and $\psi$ is also a homomorphism.

Proof:
So as to alleviate possible confusion over notation, let the composite of $\phi$ and $\psi$ be denoted $\psi \bullet \phi$ instead of the more usual $\psi \circ \phi$.
Then what we are trying to prove is denoted:
:$\paren {\psi \bullet \phi}: \struct {G_1, \circ} \to \struct {G_3, \oplus}$ is a homomorphism.
To prove the above is the case, we need to demonstrate that the morphism property is held by $\circ$ under $\psi \bullet \phi$.
We take two elements $x, y \in G_1$, and put them through the following wringer:
{{begin-eqn}}
{{eqn | l = \map {\paren {\psi \bullet \phi} } {x \circ y}
      | r = \map \psi {\map \phi {x \circ y} }
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map \psi {\map \phi x * \map \phi y}
      | c = {{Defof|Morphism Property}}: applied to $\circ$ under $\phi$
}}
{{eqn | r = \map \psi {\map \phi x} \oplus \map \psi {\map \phi y}
      | c = {{Defof|Morphism Property}}: applied to $*$ under $\psi$
}}
{{eqn | r = \map {\paren {\psi \bullet \phi} } x \oplus \map {\paren {\psi \bullet \phi} } y
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
Disentangling the confusing and tortuous expressions above, we (eventually) see that this shows that the morphism property is indeed held by $\circ$ under $\psi \bullet \phi$.
Thus $\paren {\psi \bullet \phi}: \struct {G_1, \circ} \to \struct {G_3, \oplus}$ is indeed a homomorphism.
{{qed}}
Theorem: Composite of Group Monomorphisms is Monomorphism

Let:
:$\struct {G_1, \circ}$
:$\struct {G_2, *}$
:$\struct {G_3, \oplus}$
be groups.
Let:
:$\phi: \struct {G_1, \circ} \to \struct {G_2, *}$
:$\psi: \struct {G_2, *} \to \struct {G_3, \oplus}$
be monomorphisms.
Then the composite of $\phi$ and $\psi$ is also a monomorphism.

Proof:
A monomorphism is a homomorphism which is also an injection.
From Composite of Group Homomorphisms is Homomorphism, $\psi \circ \phi$ is a homomorphism.
From Composite of Injections is Injection, $\psi \circ \phi$ is an injection.
{{qed}}
Theorem: Composite of Group Epimorphisms is Epimorphism

Let:
:$\struct {G_1, \odot}$
:$\struct {G_2, *}$
:$\struct {G_3, \oplus}$
be groups.
Let:
:$\phi: \struct {G_1, \odot} \to \struct {G_2, *}$
:$\psi: \struct {G_2, *} \to \struct {G_3, \oplus}$
be (group) epimorphisms.
Then the composite of $\phi$ and $\psi$ is also a (group) epimorphism.

Proof:
A group epimorphism is a group homomorphism which is also a surection.
From Composite of Group Homomorphisms is Homomorphism, $\psi \circ \phi$ is a group homomorphism.
From Composite of Surjections is Surjection, $\psi \circ \phi$ is a surection.
{{qed}}
Theorem: Composite of Group Isomorphisms is Isomorphism

Let $\struct {G_1, \circ}$, $\struct {G_2, *}$ and $\struct {G_3, \oplus}$ be groups.
Let $\phi: \struct {G_1, \circ} \to \struct {G_2, *}$ and $\psi: \struct {G_2, *} \to \struct {G_3, \oplus}$ be group isomorphisms.
Then the composite of $\psi$ with $\phi$ is also a group isomorphism.

Proof:
A group isomorphism is a group homomorphism which is also a bijection.
From Composite of Group Homomorphisms is Homomorphism, $\psi \circ \phi$ is a group homomorphism.
From Composite of Bijections is Bijection, $\psi \circ \phi$ is a bijection.
{{qed}}
Theorem: Sum of Deviations from Mean

Let $S = \set {x_1, x_2, \ldots, x_n}$ be a set of real numbers.
Let $\overline x$ denote the arithmetic mean of $S$.
Then: 
:$\ds \sum_{i \mathop = 1}^n \paren {x_i - \overline x} = 0$

Proof:
For brevity, let us write $\ds \sum$ for $\ds \sum_{i \mathop = 1}^n$.
Then:
{{begin-eqn}}
{{eqn | l = \sum \paren {x_i - \overline x}
      | r = x_1 - \overline x + x_2 - \overline x + \cdots + x_n - \overline x
      | c = {{Defof|Summation}}
}}
{{eqn | r = x_1 - \sum \frac {x_i} n + x_2 - \sum \frac {x_i} n + \cdots + x_n - \sum \frac {x_i} n
      | c = {{Defof|Arithmetic Mean}}
}}
{{eqn | r = \paren {x_1 + x_2 + \cdots + x_n} - n \paren {\sum \frac {x_i} n}
}}
{{eqn | r = \sum x_i - \sum x_i
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Identity of Group Direct Product

Let $\struct {G \times H, \circ}$ be the group direct product of the two groups $\struct {G, \circ_1}$ and $\struct {H, \circ_2}$.
Let $e_G$ be the identity for $\struct {G, \circ_1}$.
Let $e_H$ be the identity for $\struct {H, \circ_2}$.
Then $\tuple {e_G, e_H}$ is the identity for $\struct {G \times H, \circ}$.

Proof:
{{begin-eqn}}
{{eqn | l = \tuple {g, h} \circ \tuple {e_G, e_H}
      | r = \tuple {g \circ_1 e_G, h \circ_2 e_H} = \tuple {g, h}
      | c = 
}}
{{eqn | l = \tuple {e_G, e_H} \circ \tuple {g, h}
      | r = \tuple {e_G \circ_1 g, e_H \circ_2 h} = \tuple {g, h}
      | c = 
}}
{{end-eqn}}
So the identity is $\tuple {e_G, e_H}$.
{{qed}}
Theorem: Identity of Group Direct Product

Let $\struct {G \times H, \circ}$ be the group direct product of the two groups $\struct {G, \circ_1}$ and $\struct {H, \circ_2}$.
Let $e_G$ be the identity for $\struct {G, \circ_1}$.
Let $e_H$ be the identity for $\struct {H, \circ_2}$.
Then $\tuple {e_G, e_H}$ is the identity for $\struct {G \times H, \circ}$.

Proof:
A specific instance of External Direct Product Identity, where the algebraic structures in question are groups.
{{qed}}
Theorem: Inverses in Group Direct Product

Let $\struct {G \times H, \circ}$ be the group direct product of the two groups $\struct {G, \circ_1}$ and $\struct {H, \circ_2}$.
Let $g^{-1}$ be an inverse of $g \in \struct {G, \circ_1}$.
Let $h^{-1}$ be an inverse of $h \in \struct {H, \circ_2}$.
Then $\tuple {g^{-1}, h^{-1} }$ is the inverse of $\tuple {g, h} \in \struct {G \times H, \circ}$.

Proof:
Let $e_G$ be the identity for $\struct {G, \circ_1}$
Let $e_H$ be the identity for $\struct {H, \circ_2}$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {g, h} \circ \tuple {g^{-1}, h^{-1} }
      | r = \tuple {g \circ_1 g^{-1}, h \circ_2 h^{-1} }
      | c = 
}}
{{eqn | r = \tuple {e_G, e_H}
      | c = 
}}
{{eqn | r = \tuple {g^{-1} \circ_1 g, h^{-1} \circ_2 h}
      | c = 
}}
{{eqn | r = \tuple {g^{-1}, h^{-1} } \circ \tuple {g, h}
      | c = 
}}
{{end-eqn}}
So the inverse of $\tuple {g, h}$ is $\tuple {g^{-1}, h^{-1} }$.
{{qed}}
Theorem: Inverses in Group Direct Product

Let $\struct {G \times H, \circ}$ be the group direct product of the two groups $\struct {G, \circ_1}$ and $\struct {H, \circ_2}$.
Let $g^{-1}$ be an inverse of $g \in \struct {G, \circ_1}$.
Let $h^{-1}$ be an inverse of $h \in \struct {H, \circ_2}$.
Then $\tuple {g^{-1}, h^{-1} }$ is the inverse of $\tuple {g, h} \in \struct {G \times H, \circ}$.

Proof:
A specific instance of External Direct Product Inverses, where the algebraic structures in question are groups.
{{qed}}
Theorem: Associativity of Operation in Group Direct Product

Let $\struct {G \times H, \circ}$ be the group direct product of the two groups $\struct {G, \circ_1}$ and $\struct {H, \circ_2}$.
Then the operation $\circ$ in $\struct {G \times T, \circ}$ is associative.

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\tuple {g_1, h_1} \circ \tuple {g_2, h_2} } \circ \tuple {g_3, h_3}
      | r = \tuple {\paren {g_1 \circ_1 g_2} \circ_1 g_3, \paren {h_1 \circ_2 h_2} \circ_2 h_3}
      | c = 
}}
{{eqn | r = \tuple {g_1 \circ_1 g_2 \circ_1 g_3, h_1 \circ_2 h_2 \circ_2 h_3}
      | c = 
}}
{{eqn | r = \tuple {g_1 \circ_1 \paren {g_2 \circ_1 g_3}, h_1 \circ_2 \paren {h_2 \circ_2 h_3} }
      | c = 
}}
{{eqn | r = \tuple {g_1, h_1} \circ \paren {\tuple {g_2, h_2} \circ \tuple {g_3, h_3} }
      | c = 
}}
{{end-eqn}}
Thus $\circ$ is seen to be associative in $\struct {G \times H, \circ}$.
{{qed}}
Theorem: Associativity of Operation in Group Direct Product

Let $\struct {G \times H, \circ}$ be the group direct product of the two groups $\struct {G, \circ_1}$ and $\struct {H, \circ_2}$.
Then the operation $\circ$ in $\struct {G \times T, \circ}$ is associative.

Proof:
By definition of group, both $\circ_1$ and $\circ_2$ are associative operations.
The result follows from External Direct Product Associativity, where the algebraic structures in question are groups.
{{qed}}
Theorem: Anticommutativity of External Direct Product

Let $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$ be algebraic structures where $S$ and $T$ both have at least two distinct elements.
Let $\struct {S \times T, \circ}$ be their external direct product.
Then $\struct {S \times T, \circ}$ is anticommutative {{iff}} at least one of $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$ is.

Proof:
=== Sufficient Condition ===
Suppose $\struct {S \times T, \circ}$ is anticommutative and neither $\struct {S, \circ_1}$ nor $\struct {T, \circ_2}$ is.
Then for some distinct $a, b \in S$:
:$a \circ_1 b = b \circ_1 a$
Similarly, for some distinct $c, d \in T$:
:$c \circ_2 d = d \circ_2 c$
Then we compute by definition of $\circ$ in the external direct product:
:$\tuple {a, c} \circ \tuple {b, d} = \tuple {a \circ_1 b, c \circ_2 d}$
:$\tuple {b, d} \circ \tuple {a, c} = \tuple {b \circ_1 a, d \circ_2 c}$
So: 
:$\tuple {a, c} \circ \tuple {b, d} = \tuple {b, d} \circ \tuple {a, c}$
which contradicts our assumption that $\struct {S \times T, \circ}$ was anticommutative.
Hence at least one of $\struct {S, \circ_1}$ and $\struct {T, \circ_2}$ is anticommutative.
{{qed|lemma}}
Theorem: Projection on Group Direct Product is Epimorphism

Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups.
Let $\struct {G, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$.
Then:
:$\pr_1$ is an epimorphism from $\struct {G, \circ}$ to $\struct {G_1, \circ_1}$
:$\pr_2$ is an epimorphism from $\struct {G, \circ}$ to $\struct {G_2, \circ_2}$
where $\pr_1$ and $\pr_2$ are the first and second projection respectively of $\struct {G, \circ}$.

Proof:
From Projection is Surjection, $\pr_1$ and $\pr_2$ are surjections.
We now need to show they are homomorphisms.
Let $g, h \in \struct {G, \circ}$ where $g = \tuple {g_1, g_2}$ and $h = \tuple {h_1, h_2}$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\pr_1} {g \circ h}
      | r = \map {\pr_1} {\tuple {g_1, g_2} \circ \tuple {h_1, h_2} }
      | c = 
}}
{{eqn | r = \map {\pr_1} {\tuple {g_1 \circ_1 h_1, g_2 \circ_2 h_2} }
      | c = 
}}
{{eqn | r = g_1 \circ_1 h_1
      | c = 
}}
{{eqn | r = \map {\pr_1} g \circ_1 \map {\pr_1} h
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \map {\pr_2} {g \circ h}
      | r = \map {\pr_2} {\tuple {g_1, g_2} \circ \tuple {h_1, h_2} }
      | c = 
}}
{{eqn | r = \map {\pr_2} {\tuple {g_1 \circ_1 h_1, g_2 \circ_2 h_2} }
      | c = 
}}
{{eqn | r = g_2 \circ_2 h_2
      | c = 
}}
{{eqn | r = \map {\pr_2} g \circ_2 \map {\pr_2} h
      | c = 
}}
{{end-eqn}}
and thus the morphism property is demonstrated for both $\pr_1$ and $\pr_2$.
{{Qed}}
Theorem: Projection on Group Direct Product is Epimorphism

Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups.
Let $\struct {G, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$.
Then:
:$\pr_1$ is an epimorphism from $\struct {G, \circ}$ to $\struct {G_1, \circ_1}$
:$\pr_2$ is an epimorphism from $\struct {G, \circ}$ to $\struct {G_2, \circ_2}$
where $\pr_1$ and $\pr_2$ are the first and second projection respectively of $\struct {G, \circ}$.

Proof:
A specific instance of Projection is Epimorphism, where the algebraic structures in question are groups.
{{qed}}
Theorem: Canonical Injection on Group Direct Product is Monomorphism

Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups with identities $e_1, e_2$ respectively.
Let $\struct {G_1 \times G_2, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$
Then the canonical injections:
:$\inj_1: \struct {G_1, \circ_1} \to \struct {G_1, \circ_1} \times \struct {G_2, \circ_2}: \forall x \in G_1: \map {\inj_1} x = \tuple {x, e_2}$
:$\inj_2: \struct {G_2, \circ_2} \to \struct {G_1, \circ_1} \times \struct {G_2, \circ_2}: \forall x \in G_2: \map {\inj_2} x = \tuple {e_1, x}$
are group monomorphisms.

Proof:
From Canonical Injection is Injection we have that the canonical injections are in fact injective.
It remains to prove the morphism property.
Let $x, y \in G_1$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\inj_1} {x \circ_1 y}
      | r = \tuple {x \circ_1 y, e_2}
      | c = Definition of $\inj_1$
}}
{{eqn | r = \tuple {x \circ_1 y, e_2 \circ_2 e_2}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \tuple {x, e_2} \circ \tuple {y, e_2}
      | c = {{Defof|Group Direct Product}}
}}
{{eqn | r = \map {\inj_1} x \circ \map {\inj_1} y
      | c = Definition of $\inj_1$
}}
{{end-eqn}}
and the morphism property has been demonstrated to hold for $\inj_1$.
Thus $\inj_1: \struct {G_1, \circ_1} \to \struct {G_1, \circ_1} \times \struct {G_2, \circ_2}$ has been shown to be an injective group homomorphism and therefore a group monomorphism.
The same argument applies to $\inj_2$.
{{Qed}}
Theorem: Canonical Injection on Group Direct Product is Monomorphism

Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups with identities $e_1, e_2$ respectively.
Let $\struct {G_1 \times G_2, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$
Then the canonical injections:
:$\inj_1: \struct {G_1, \circ_1} \to \struct {G_1, \circ_1} \times \struct {G_2, \circ_2}: \forall x \in G_1: \map {\inj_1} x = \tuple {x, e_2}$
:$\inj_2: \struct {G_2, \circ_2} \to \struct {G_1, \circ_1} \times \struct {G_2, \circ_2}: \forall x \in G_2: \map {\inj_2} x = \tuple {e_1, x}$
are group monomorphisms.

Proof:
A specific instance of Canonical Injection is Monomorphism, where the algebraic structures in question are groups.
{{qed}}
Theorem: Canonical Injection is Right Inverse of Projection

Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups with identity elements $e_1$ and $e_2$ respectively.
Let $\struct {G_1 \times G_2, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$
Let:
:$\pr_1: \struct {G_1 \times G_2, \circ} \to \struct {G_1, \circ_1}$ be the first projection from $\struct {G_1 \times G_2, \circ}$ to $\struct {G_1, \circ_1}$
:$\pr_2: \struct {G_1 \times G_2, \circ} \to \struct {G_2, \circ_2}$ be the second projection from $\struct {G_1 \times G_2, \circ}$ to $\struct {G_2, \circ_2}$.
Let:
:$\inj_1: \struct {G_1, \circ_1} \to \struct {G_1 \times G_2, \circ}$ be the canonical injection from $\struct {G_1, \circ_1}$ to $\struct {G_1 \times G_2, \circ}$
:$\inj_2: \struct {G_2, \circ_2} \to \struct {G_1 \times G_2, \circ}$ be the canonical injection from $\struct {G_2, \circ_2}$ to $\struct {G_1 \times G_2, \circ}$.
Then:
:$(1): \quad \pr_1 \circ \inj_1 = I_{G_1}$
:$(2): \quad \pr_2 \circ \inj_2 = I_{G_2}$
where $I_{G_1}$ and $I_{G_2}$ are the identity mappings on $G_1$ and $G_2$ respectively.

Proof:
This is a specific instance of External Direct Product of Projection with Canonical Injection, where the algebraic structures in question are groups.
{{qed}}
Theorem: Image of Canonical Injection is Kernel of Projection

Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups with identity elements $e_1$ and $e_2$ respectively.
Let $\struct {G_1 \times G_2, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$
Let:
:$\pr_1: \struct {G_1 \times G_2, \circ} \to \struct {G_1, \circ_1}$ be the first projection from $\struct {G_1 \times G_2, \circ}$ to $\struct {G_1, \circ_1}$
:$\pr_2: \struct {G_1 \times G_2, \circ} \to \struct {G_2, \circ_2}$ be the second projection from $\struct {G_1 \times G_2, \circ}$ to $\struct {G_2, \circ_2}$.
Let:
:$\inj_1: \struct {G_1, \circ_1} \to \struct {G_1 \times G_2, \circ}$ be the canonical injection from $\struct {G_1, \circ_1}$ to $\struct {G_1 \times G_2, \circ}$
:$\inj_2: \struct {G_2, \circ_2} \to \struct {G_1 \times G_2, \circ}$ be the canonical injection from $\struct {G_2, \circ_2}$ to $\struct {G_1 \times G_2, \circ}$.
Then:
:$(1): \quad \Img {\inj_1} = \map \ker {\pr_2}$
:$(2): \quad \Img {\inj_2} = \map \ker {\pr_1}$
That is:
:the image of the (first) canonical injection is the kernel of the second projection
:the image of the (second) canonical injection is the kernel of the first projection.

Proof:
The canonical injection $\inj_1: \struct {G_1, \circ_1} \to \struct {G_1 \times G_2, \circ}$ is defined as:
:$\forall x \in G_1: \map {\inj_1} x = \tuple {x, e_2}$
Thus:
:$\Img {\inj_1} = \set {\tuple {x, e_2}: x \in G_1}$
The second projection $\pr_2: \struct {G_1 \times G_2, \circ} \to \struct {G_2, \circ_2}$ is defined as:
:$\forall \tuple {x, y} \in G_1 \times G_2: \map {\pr_2} {x, y} = y$
Thus by definition of kernel:
:$\map \ker {\pr_2} = \map {\pr_2^{-1} } {e_2} = \set {\tuple {x, e_2}: x \in G_1}$
As can be seen:
:$\Img {\inj_1} = \map \ker {\pr_2}$
Similarly:
:$\Img {\inj_2} = \set {\tuple {e_1, y}: y \in G_2}$
:$\map \ker {\pr_1} = \map {\pr_1^{-1} } {e_1} = \set {\tuple {e_1, y}: y \in G_2}$
Hence the result.
{{qed}}
Theorem: Image of Canonical Injection is Normal Subgroup

Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups with identity elements $e_1$ and $e_2$ respectively.
Let $\struct {G_1 \times G_2, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$.
Let:
:$\inj_1: \struct {G_1, \circ_1} \to \struct {G_1 \times G_2, \circ}$ be the canonical injection from $\struct {G_1, \circ_1}$ to $\struct {G_1 \times G_2, \circ}$
:$\inj_2: \struct {G_2, \circ_2} \to \struct {G_1 \times G_2, \circ}$ be the canonical injection from $\struct {G_2, \circ_2}$ to $\struct {G_1 \times G_2, \circ}$.
Then:
:$(1): \quad \Img {\inj_1} \lhd \struct {G_1 \times G_2, \circ}$
:$(2): \quad \Img {\inj_2} \lhd \struct {G_1 \times G_2, \circ}$
That is, the images of the canonical injections are normal subgroups of the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$.

Proof:
From Image of Canonical Injection is Kernel of Projection:
:$\Img {\inj_1} = \map \ker {\pr_2}$
:$\Img {\inj_2} = \map \ker {\pr_1}$
That is:
:the image of the (first) canonical injection is the kernel of the second projection
:the image of the (second) canonical injection is the kernel of the first projection.
The domain of the projections is $G_1 \times G_2$, by definition.
The result follows from Kernel is Normal Subgroup of Domain.
{{qed}}
Theorem: Direct Product of Group Homomorphisms is Homomorphism

Let $\struct {G, \circ}, \struct {H_1, *_1}$ and $\struct {H_2, *_2}$ be groups.
Let $\struct {H_1 \times H_2, *}$ be the group direct product of $H_1$ and $H_2$.
Let $f_1: G \to H_1$ and $f_2: G \to H_2$ be group homomorphisms.
Let $f_1 \times f_2: g \to H_1 \times H_2$ be the direct product of $f_1$ and $f_2$.
Then $f_1 \times f_2$ is a group homomorphism.

Proof:
The direct product of $f_1$ and $f_2$ $f_1 \times f_2: g \to H_1 \times H_2$ is defined as:
:$\forall g \in G: \map {\paren {f_1 \times f_2} } g = \tuple {\map {f_1} g, \map {f_2} g}$
From External Direct Product of Groups is Group, the group direct product $H_1 \times H_2$ is a group.
It remains to be shown that $f_1 \times f_2$ fulfils the morphism property.
Let $g, h \in G$.
Then:
{{begin-eqn}}
{{eqn | o = 
      | r = \map {\paren {f_1 \times f_2} } g * \map {\paren {f_1 \times f_2} } h
      | c = 
}}
{{eqn | r = \tuple {\map {f_1} g, \map {f_2} g} * \tuple {\map {f_1} h, \map {f_2} h}
      | c = {{Defof|Direct Product of Group Homomorphisms|Direct Product of $f_1$ and $f_2$}}
}}
{{eqn | r = \tuple {\map {f_1} g *_1 \map {f_1} h, \map {f_2} g *_2 \map {f_2} h}
      | c = {{Defof|Group Direct Product|Group Direct Product}} $\struct {H_1 \times H_2, *}$
}}
{{eqn | r = \tuple {\map {f_1} {g \circ h}, \map {f_2} {g \circ h} }
      | c = $f_1$ and $f_2$ are Group Homomorphisms
}}
{{eqn | r = \map {\paren {f_1 \times f_2} } {g \circ h}
      | c = {{Defof|Direct Product of Group Homomorphisms|Direct Product of $f_1$ and $f_2$}}
}}
{{end-eqn}}
{{qed}}
Theorem: Projections on Direct Product of Group Homomorphisms

Let $G, H_1$ and $H_2$ be groups.
Let $H_1 \times H_2$ be the group direct product of $H_1$ and $H_2$.
Let $f_1: G \to H_1$ and $f_2: G \to H_2$ be group homomorphisms.
Let $f_1 \times f_2: g \to H_1 \times H_2$ be the direct product of $f_1$ and $f_2$.
Let:
:$\pr_1: H_1 \times H_2 \to H_1$ be the first projection from $H_1 \times H_2$ to $H_1$
:$\pr_2: H_1 \times H_2 \to H_2$ be the second projection from $H_1 \times H_2$ to $H_2$.
Then:
:$(1) \quad \pr_1 \circ \paren {f_1 \times f_2} = f_1$
:$(2) \quad \pr_2 \circ \paren {f_1 \times f_2} = f_2$
where $\circ$ is the operation of composition of mappings.

Proof:
The proof of $(2)$ follows exactly the same lines as the proof of $(1)$, so the proof of $(1)$ only will be shown here.
Theorem: Gaussian Integers form Subgroup of Complex Numbers under Addition

The set of Gaussian integers $\Z \sqbrk i$, under the operation of complex addition, forms a subgroup of the set of additive group of complex numbers $\struct {\C, +}$.

Proof:
We will use the One-Step Subgroup Test.
This is valid, as the Gaussian integers are a subset of the complex numbers.
We note that $\Z \sqbrk i$ is not empty, as (for example) $0 + 0 i \in \Z \sqbrk i$.
Let $a + b i, c + d i \in \Z \sqbrk i$.
Then we have $-\paren {c + d i} = -c - d i$, and so:
{{begin-eqn}}
{{eqn | l = \paren {a + b i} + \paren {-\paren {c + d i} }
      | r = \paren {a + b i} + \paren {- c - d i}
      | c = 
}}
{{eqn | r = \paren {a + \paren {-c} } + \paren {b + \paren {-d} } i
      | c = 
}}
{{eqn | r = \paren {a - c} + \paren {b - d} i
      | c = 
}}
{{end-eqn}}
We have that $a, b, c, d \in \Z$ and $\Z$ is an integral domain.
Therefore by definition $\Z$ is a ring.
So it follows that $a - c \in \Z$ and $b - d \in \Z$, and hence $\paren {a - c} + \paren {b - d} i \in \Z \sqbrk i$.
So by the One-Step Subgroup Test, $\Z \sqbrk i$ is a subgroup of $\struct {\C, +}$.
{{qed}}
Theorem: Pointwise Addition on Real-Valued Functions is Associative

Let $f, g, h: S \to \R$ be real-valued functions.
Let $f + g: S \to \R$ denote the pointwise sum of $f$ and $g$.
Then:
:$\paren {f + g} + h = f + \paren {g + h}$

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f + g} + h} } x
      | r = \paren {\map f x + \map g x} + \map h x
      | c = {{Defof|Pointwise Addition of Real-Valued Functions}}
}}
{{eqn | r = \map f x + \paren {\map g x + \map h x}
      | c = Real Addition is Associative
}}
{{eqn | r = \map {\paren {f + \paren {g + h} } } x
      | c = {{Defof|Pointwise Addition of Real-Valued Functions}}
}}
{{end-eqn}}
{{qed}}
Category:Pointwise Addition is Associative
Category:Real Addition
100k7hob3euvtbnvyx76xhb89q4o6xa
Theorem: Pointwise Addition is Associative

Let $S$ be a non-empty set.
Let $\mathbb F$ be one of the standard number sets: $\Z, \Q, \R$ or $\C$.
Let $f, g, h: S \to \mathbb F$ be functions.
Let $f + g: S \to \mathbb F$ denote the pointwise sum of $f$ and $g$.
Then:
:$\paren {f + g} + h = f + \paren {g + h}$
That is, pointwise addition is associative.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {\paren {f + g} + h} } x
      | r = \paren {\map f x + \map g x} + \map h x
      | c = {{Defof|Pointwise Addition}}
}}
{{eqn | r = \map f x + \paren {\map g x + \map h x}
      | c = Associative Law of Addition
}}
{{eqn | r = \map {\paren {f + \paren {g + h} } } x
      | c = {{Defof|Pointwise Addition}}
}}
{{end-eqn}}
{{qed}}