# External Direct Product of Groups is Group

## Theorem

Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups whose identity elements are $e_1$ and $e_2$ respectively.

Let $\struct {G_1 \times G_2, \circ}$ be the external direct product of $G_1$ and $G_2$.

Then $\struct {G_1 \times G_2, \circ}$ is a group whose identity element is $\tuple {e_1, e_2}$.

### Finite Product

The external direct product of a finite sequence of groups is itself a group.

## Proof

Taking the group axioms in turn:

### Group Axiom $\text G 0$: Closure

From External Direct Product Closure it follows that $\struct {G_1 \times G_2, \circ}$ is closed.

$\Box$

### Group Axiom $\text G 1$: Associativity

From External Direct Product Associativity it follows that $\circ$ is associative on $G_1 \times G_2$.

$\Box$

### Group Axiom $\text G 2$: Existence of Identity Element

From External Direct Product Identity it follows that $\tuple {e_1, e_2}$ is the identity element of $\struct {G_1 \times G_2, \circ}$.

$\Box$

### Group Axiom $\text G 3$: Existence of Inverse Element

From External Direct Product Inverses it follows that $\tuple {g_1^{-1}, g_2^{-1} }$ is the inverse element of $\tuple {g_1, g_2}$ in $\struct {G_1 \times G_2, \circ}$.

$\Box$

All group axioms are fulfilled, and so $\struct {G_1 \times G_2, \circ}$ is a group whose identity element is $\tuple {e_1, e_2}$.

$\blacksquare$