avewright/proofwiki-math huggingface dataset:
Theorem: Power Function on Complex Numbers is Epimorphism

Let $n \in \Z_{>0}$ be a strictly positive integer.
Let $\struct {\C_{\ne 0}, \times}$ be the multiplicative group of complex numbers.
Let $f_n: \C_{\ne 0} \to \C_{\ne 0}$ be the mapping from the set of complex numbers less zero to itself defined as:
:$\forall z \in \C_{\ne 0}: \map {f_n} z = z^n$
Then $f_n: \struct {\C_{\ne 0}, \times} \to \struct {\C_{\ne 0}, \times}$ is a group epimorphism.
The kernel of $f_n$ is the set of complex $n$th roots of unity.

Proof:
From Non-Zero Complex Numbers under Multiplication form Group, $\struct {\C_{\ne 0}, \times}$ is a group.
Therefore $\struct {\C_{\ne 0}, \times}$ is closed by {{Group-axiom|0}}.
Let $w, z \in \C_{\ne 0}$.
{{begin-eqn}}
{{eqn | l = \map {f_n} {w \times z}
      | r = \paren {w \times z}^n
      | c = 
}}
{{eqn | r = w^n \times z^n
      | c = Power of Product of Commutative Elements in Group
}}
{{eqn | r = \map {f_n} w \times \map {f_n} z
      | c = 
}}
{{end-eqn}}
Thus $f_n$ is a group homomorphism.
Now suppose $w = r \paren {\cos \alpha + i \sin \alpha}$, expressing $w$ in polar form.
Then $w = \map {f_n} z$ where:
:$z = r^{1/n} \paren {\cos \dfrac \alpha n + i \sin \dfrac \alpha n}$
and so:
:$\forall w: w \in \map {f_n} {\C_{\ne 0} }$
That is, $f_n$ is a surjection.
Being a group homomorphism which is also a surjection, by definition $f_n$ is then a group epimorphism.
The kernel of $f_n$ is the set:
:$U_n = \set {e^{2 i k \pi / n}: k \in \N_n}$
which follows from Complex Roots of Unity in Exponential Form.
{{qed}}
Theorem: Real Part as Mapping is Endomorphism for Complex Addition

Let $\struct {\C, +}$ be the additive group of complex numbers.
Let $\struct {\R, +}$ be the additive group of real numbers.
Let $f: \C \to \R$ be the mapping from the complex numbers to the real numbers defined as:
:$\forall z \in \C: \map f z = \map \Re z$
where $\map \Re z$ denotes the real part of $z$.
Then $f: \struct {\C, +} \to \struct {\R, +}$ is a group epimorphism.
Its kernel is the set:
:$\map \ker f = \set {i x: x \in \R}$
of wholly imaginary numbers.

Proof:
From Real Part as Mapping is Surjection, $f$ is a surjection.
Let $z_1, z_2 \in \C$.
Let $z_1 = x_1 + i y_1, z_2 = x_2 + i y_2$.
Then:
{{begin-eqn}}
{{eqn | l = \map f {z_1 + z_2}
      | r = \map \Re {z_1 + z_2}
      | c = Definition of $f$
}}
{{eqn | r = \map \Re {x_1 + i y_1 + x_2 + i y_2}
      | c = Definition of $z_1$ and $z_2$
}}
{{eqn | r = x_1 + x_2
      | c = {{Defof|Real Part}}
}}
{{eqn | r = \map \Re {z_1} + \map \Re {z_2}
      | c = {{Defof|Real Part}}
}}
{{eqn | r = \map f {z_1} + \map f {z_2}
      | c = Definition of $f$
}}
{{end-eqn}}
So $f$ is a group homomorphism.
Thus $f$ is a surjective group homomorphism and therefore by definition a group epimorphism.
Finally:
:$\forall y \in \R: \map \Re {0 + i y} = 0$
It follows from Complex Addition Identity is Zero that: 
:$\map \ker f = \set {i x: x \in \R}$
{{qed}}
Theorem: Imaginary Part as Mapping is Endomorphism for Complex Addition

Let $\struct {\C, +}$ be the additive group of complex numbers.
Let $\struct {\R, +}$ be the additive group of real numbers.
Let $f: \C \to \R$ be the mapping from the complex numbers to the real numbers defined as:
:$\forall z \in \C: \map f z = \map \Im z$
where $\map \Im z$ denotes the imaginary part of $z$.
Then $f: \struct {\C, +} \to \struct {\R, +}$ is a group epimorphism.
Its kernel is the set:
:$\map \ker f = \R$
of (wholly) real numbers.

Proof:
From Imaginary Part as Mapping is Surjection, $f$ is a surjection.
Let $z_1, z_2 \in \C$.
Let $z_1 = x_1 + i y_1, z_2 = x_2 + i y_2$.
Then:
{{begin-eqn}}
{{eqn | l = \map f {z_1 + z_2}
      | r = \map \Im {z_1 + z_2}
      | c = Definition of $f$
}}
{{eqn | r = \map \Im {x_1 + i y_1 + x_2 + i y_2}
      | c = Definition of $z_1$ and $z_2$
}}
{{eqn | r = y_1 + y_2
      | c = {{Defof|Imaginary Part}}
}}
{{eqn | r = \map \Im {z_1} + \map \Im {z_2}
      | c = {{Defof|Imaginary Part}}
}}
{{eqn | r = \map f {z_1} + \map f {z_2}
      | c = Definition of $f$
}}
{{end-eqn}}
So $f$ is a group homomorphism.
Thus $f$ is a surjective group homomorphism and therefore by definition a group epimorphism.
Finally:
:$\forall y \in \R: \map \Im {x + 0 i} = 0 i = 0$
It follows from Complex Addition Identity is Zero that: 
:$\map \ker f = \set {x: x \in \R} = \R$
{{qed}}
Theorem: Reduced Echelon Matrix is Unique

Every $m \times n$ matrix is row equivalent to exactly one $m \times n$ reduced echelon matrix.
That is, the reduced echelon form of a matrix is unique.

Proof:
=== Proof of Existence ===
Proved in Matrix is Row Equivalent to Reduced Echelon Matrix.
{{qed|lemma}}
Theorem: Measure of Set Difference with Subset

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $S, T \in \Sigma$ be such that $S \subseteq T$, and suppose that $\mu \paren S < +\infty$.
Then:
:$\mu \paren {T \setminus S} = \mu \paren T - \mu \paren S$
where $T \setminus S$ denotes set difference.

Proof:
{{begin-eqn}}
{{eqn | l = T
      | r = \paren {T \setminus S} \cup \paren {T \cap S}
      | c = Set Difference Union Intersection
}}
{{eqn | r = \paren {T \setminus S} \cup S
      | c = Intersection with Subset is Subset
}}
{{eqn | ll= \leadsto
      | l = \mu \paren T
      | r = \mu \paren {T \setminus S} + \mu \paren S
      | c = Measure is Finitely Additive Function, Set Difference Intersection with Second Set is Empty Set
}}
{{eqn | ll= \leadsto
      | l = \mu \paren T - \mu \paren S
      | r = \mu \paren {T \setminus S})
      | c = Subtraction defined as $\mu \paren S < +\infty$
}}
{{end-eqn}}
{{qed}}
Theorem: Subset of Codomain is Superset of Image of Preimage

Let $f: S \to T$ be a mapping.
Then:
:$B \subseteq T \implies \paren {f \circ f^{-1} } \sqbrk B \subseteq B$
where:
:$f \sqbrk B$ denotes the image of $B$ under $f$
:$f^{-1}$ denotes the inverse of $f$
:$f \circ f^{-1}$ denotes composition of $f$ and $f^{-1}$.
This can be expressed in the language and notation of direct image mappings and inverse image mappings as:
:$\forall B \in \powerset T: \map {\paren {f^\to \circ f^\gets} } B \subseteq B$

Proof:
From Image of Preimage under Mapping:
: $B \subseteq T \implies \left({f \circ f^{-1} }\right) \left[{B}\right] = B \cap f \left[{S}\right]$
The result follows from Intersection is Subset.
{{qed}}
Theorem: Subset of Codomain is Superset of Image of Preimage

Let $f: S \to T$ be a mapping.
Then:
:$B \subseteq T \implies \paren {f \circ f^{-1} } \sqbrk B \subseteq B$
where:
:$f \sqbrk B$ denotes the image of $B$ under $f$
:$f^{-1}$ denotes the inverse of $f$
:$f \circ f^{-1}$ denotes composition of $f$ and $f^{-1}$.
This can be expressed in the language and notation of direct image mappings and inverse image mappings as:
:$\forall B \in \powerset T: \map {\paren {f^\to \circ f^\gets} } B \subseteq B$

Proof:
Let $y \in B$.
Then:
:$\exists x \in S: y = f \left({x}\right)$
Therefore by definition of preimage of subset:
:$\exists x \in f^{-1} \left[{B}\right]$
It follows by definition of image of subset that:
:$y \in f \left[{f^{-1} \left[{B}\right]}\right]$
Thus by definition of composition $f$ with $f^{-1}$:
:$y \in \left({f \circ f^{-1}}\right) \left[{B}\right]$
The result follows by definition of subset.
{{qed}}
Theorem: Subset of Codomain is Superset of Image of Preimage

Let $f: S \to T$ be a mapping.
Then:
:$B \subseteq T \implies \paren {f \circ f^{-1} } \sqbrk B \subseteq B$
where:
:$f \sqbrk B$ denotes the image of $B$ under $f$
:$f^{-1}$ denotes the inverse of $f$
:$f \circ f^{-1}$ denotes composition of $f$ and $f^{-1}$.
This can be expressed in the language and notation of direct image mappings and inverse image mappings as:
:$\forall B \in \powerset T: \map {\paren {f^\to \circ f^\gets} } B \subseteq B$

Proof:
Let $B \subseteq T$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \paren {f \circ f^{-1} } \sqbrk B
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = f \sqbrk {f^{-1} \sqbrk B}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | ll= \leadsto
      | q = \exists x \in f^{-1} \sqbrk B
      | l = \map f x
      | r = y
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = B
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{end-eqn}}
So by definition of subset:
:$B \subseteq T \implies \paren {f \circ f^{-1} } \sqbrk B \subseteq B$
{{qed}}
Theorem: Ordering on Extended Real Numbers is Ordering

Denote with $\le$ the usual ordering on the extended real numbers $\overline \R$.
Then $\le$ is an ordering, and so $\overline \R$ is an ordered set.

Proof:
=== Transitive ===
Let $a, b, c \in \overline \R$.
Suppose that $a \le b$ and $b \le c$.
If $c = +\infty$, then by the definition of $\le$, $a \le c$.
If $b = +\infty$, then by Positive Infinity is Maximal, $b = c$, so $a \le c$.
If $a = +\infty$, then applying Positive Infinity is Maximal twice yields $a \le c$.
The cases for $a$, $b$, or $c$ being $-\infty$ are similar.
The only remaining case is that $a, b, c \in \R$.
Since $\le$ is transitive on $\R$, $a \le c$.
{{qed|lemma}}
Theorem: Ordering on Extended Real Numbers is Total Ordering

Let $\le$ denote the ordering on the extended real numbers $\overline \R$.
Then $\le$ is a total ordering, and so $\overline \R$ is a toset.

Proof:
{{ProofWanted}}
Category:Usual Ordering on Extended Real Numbers
0xw3mdk4joabiju4q94c91ov1lkxfiv
Theorem: Extended Real Number Space is Compact

The extended real number space is compact.

Proof:
{{ProofWanted|opens at each infinity, and a closed, bounded area remains}}
Category:Extended Real Number Space
r328iv05o9wxczee89g4akd3wy7jays
Theorem: Euclidean Space is Subspace of Extended Real Number Space

Let $\struct {\overline \R, \tau}$ be the extended real number space.
Then $\tau {\restriction_\R}$, the subspace topology on $\R$, is the Euclidean topology.
That is, Euclidean $1$-space is a subspace of the extended real number space.

Proof:
{{ProofWanted}}
Category:Extended Real Number Space
Category:Real Euclidean Spaces
0tb3hq0nyqarqlg8426ymnurzcg75kg
Theorem: Transcendental Slope

The slope of a line may be transcendental.

Proof:
The slope form of any number $x$ may be produced by: 
{{begin-eqn}}
{{eqn|l = {\mathrm m}
     |r = \frac {x} {1}
     |c = (Slope Form of $x$)
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn|l = {\mathrm m}
     |r = {x}
     |c = 
}}
{{end-eqn}}
If $x$ is transcendental, then the slope of a line $\mathrm m$ is transcendental.
Theorem: Lagrange's Formula

Let $\mathbf a$, $\mathbf b$ and $\mathbf c$ be vectors in a vector space $\mathbf V$ of $3$ dimensions.
Then:
:$\mathbf a \times \paren {\mathbf b \times \mathbf c} = \paren {\mathbf a \cdot \mathbf c} \mathbf b - \paren {\mathbf a \cdot \mathbf b} \mathbf c$

Proof:
Let $\mathbf a$, $\mathbf b$ and $\mathbf c$ be embedded in a Cartesian $3$-space:
:$\mathbf a = \begin{bmatrix} a_x \\ a_y \\ a_z \end{bmatrix}$, $\mathbf b = \begin{bmatrix} b_x \\ b_y \\ b_z \end{bmatrix}$, $\mathbf c = \begin{bmatrix} c_x \\ c_y \\ c_z \end{bmatrix}$
{{begin-eqn}}
{{eqn | l = \mathbf b \times \mathbf c
      | r = \begin {bmatrix} b_x \\ b_y \\ b_z \end {bmatrix} \times \begin {bmatrix} c_x \\ c_y \\ c_z \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} b_y c_z - b_z c_y \\ b_z c_x - b_x c_z \\ b_x c_y - b_y c_x \end {bmatrix}
      | c = {{Defof|Vector Cross Product}}
}}
{{eqn | l = \mathbf a \times \paren {\mathbf b \times \mathbf c}
      | r = \begin {bmatrix} a_x \\ a_y \\ a_z \end {bmatrix} \times \begin {bmatrix} b_y c_z - b_z c_y \\ b_z c_x - b_x c_z \\ b_x c_y - b_y c_x \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} a_y b_x c_y - a_y b_y c_x - a_z b_z c_x + a_z b_x c_z \\ a_z b_y c_z - a_z b_z c_y - a_x b_x c_y + a_x b_y c_x \\ a_x b_z c_x - a_x b_x c_z - a_y b_y c_z + a_y b_z c_y \end {bmatrix}
      | c = {{Defof|Vector Cross Product}}
}}
{{eqn | r = \begin {bmatrix} a_y b_x c_y - a_y b_y c_x - a_z b_z c_x + a_z b_x c_z + a_x b_x c_x - a_x b_x c_x \\ a_z b_y c_z - a_z b_z c_y - a_x b_x c_y + a_x b_y c_x + a_y b_y c_y - a_y b_y c_y \\ a_x b_z c_x - a_x b_x c_z - a_y b_y c_z + a_y b_z c_y + a_z b_z c_z - a_z b_z c_z \end {bmatrix}
      | c = adding $0 = a_i b_i c_i - a_i b_i c_i$ to each entry
}}
{{eqn | r = \begin {bmatrix} b_x \paren {a_y c_y + a_z c_z  + a_x  c_x} - c_x \paren {a_y b_y + a_z b_z + a_x b_x} \\ b_y \paren {a_z c_z + a_x c_x + a_y c_y} - c_y \paren {a_z b_z + a_x b_x + a_y c_y} \\ b_z \paren {a_x c_x + a_y c_y + a_z c_z} - c_z \paren {a_x b_x + a_y b_y + a_z c_z} \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} b_x \paren {\mathbf a \cdot \mathbf c} - c_x \paren {\mathbf a \cdot \mathbf b} \\ b_y \paren {\mathbf a \cdot \mathbf c} - c_y \paren {\mathbf a \cdot \mathbf b} \\ b_z \paren {\mathbf a \cdot \mathbf c} - c_z \paren {\mathbf a \cdot \mathbf b} \end {bmatrix}
     | c = {{Defof|Dot Product}}
}}
{{eqn | r = \paren {\mathbf a \cdot \mathbf c} \begin {bmatrix} b_x \\ b_y \\ b_z \end {bmatrix} - \paren {\mathbf a \cdot \mathbf b} \begin {bmatrix} c_x \\ c_y \\ c_z \end {bmatrix}
}}
{{eqn | r = \paren {\mathbf a \cdot \mathbf c} \mathbf b - \paren {\mathbf a \cdot \mathbf b} \mathbf c
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Joseph Louis Lagrange|cat = Lagrange}}
Theorem: Isomorphism of External Direct Products/General Result

Let:
:$(1): \quad \ds \struct {S, \circ} = \prod_{k \mathop = 1}^n S_k = \struct {S_1, \circ_1} \times \struct {S_2, \circ_2} \times \cdots \times \struct {S_n, \circ_n}$
:$(2): \quad \ds \struct {T, \ast} = \prod_{k \mathop = 1}^n T_k = \struct {T_1, \ast_1} \times \struct {T_2, \ast_2} \times \cdots \times \struct {T_n, \ast_n}$
be external direct products of algebraic structures.
Let $\phi_k: \struct {S_k, \circ_k} \to \struct {T_k, \ast_k}$ be an isomorphism for each $k \in \closedint 1 n$.
Then:
:$\phi: \struct {s_1, \ldots, s_n} \to \struct {\map {\phi_1} {s_1}, \ldots, \map {\phi_n} {s_n} }$
is an isomorphism from $\struct {S, \circ}$ to $\struct {T, \ast}$.

Proof:
By definition of isomorphism, each $\phi_k$ is a homomorphism which is a bijection.
From Cartesian Product of Bijections is Bijection: General Result, $\phi$ is a bijection.
From Homomorphism of External Direct Products: General Result, $\phi$ is a homomorphism.
Hence the result.
{{qed}}
Theorem: External Direct Product of Groups is Group/Finite Product

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

Proof:
Let $\struct {G_1, \circ_1}, \struct {G_2, \circ_2}, \ldots, \struct {G_n, \circ_n}$ be groups.
Let $\ds \struct {G, \circ} = \prod_{k \mathop = 1}^n G_k$ be the external direct product of $\struct {G_1, \circ_1}, \struct {G_2, \circ_2}, \ldots, \struct {G_n, \circ_n}$.
Taking the group axioms in turn:
Theorem: External Direct Product Inverses/General Result

Let $\ds \struct {\SS, \circ} = \prod_{k \mathop = 1}^n S_k$ be the external direct product of the algebraic structures $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \ldots, \struct {S_n, \circ_n}$.
Let $\tuple {x_1, x_2, \ldots, x_n} \in S$.
Let $y_k$ be an inverse of $x_k$ in $\struct {S_k, \circ_k}$ for each of $k \in \N^*_n$.
Then $\tuple {y_1, y_2, \ldots, y_n}$ is the inverse of $\tuple {x_1, x_2, \ldots, x_n} \in \SS$ in $\struct {\SS, \circ}$.

Proof:
Let $e_1, e_2, \ldots, e_n$ be the identity elements of $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \ldots, \struct {S_n, \circ_n}$ respectively.
Let $x := \tuple {x_1, x_2, \ldots, x_n}$.
Let $y := \tuple {x_1, x_2, \ldots, x_n}$.
From External Direct Product Identity, $e := \tuple {e_1, e_2, \ldots, e_n}$ is the identity element of $\SS$.
Then:
{{begin-eqn}}
{{eqn | l = x \circ y
      | r = \tuple {x_1, x_2, \ldots, x_n} \circ \tuple {y_1, y_2, \ldots, y_n}
      | c = 
}}
{{eqn | r = \tuple {x_1 \circ_1 y_1, x_2 \circ_2 y_2, \ldots, x_n \circ_n y_n}
      | c = {{Defof|External Direct Product|subdef = General Definition}}
}}
{{eqn | r = \tuple {e_1, e_2, \ldots, e_n}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = e
      | c = External Direct Product Identity
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = y \circ x
      | r = \tuple {y_1, y_2, \ldots, y_n} \circ \tuple {x_1, x_2, \ldots, x_n}
      | c = 
}}
{{eqn | r = \tuple {y_1 \circ_1 x_1, y_2 \circ_2 x_2, \ldots, y_n \circ_n x_n}
      | c = {{Defof|External Direct Product|subdef = General Definition}}
}}
{{eqn | r = \tuple {e_1, e_2, \ldots, e_n}
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = e
      | c = External Direct Product Identity
}}
{{end-eqn}}
{{qed}}
Theorem: External Direct Product Identity/General Result

Let $\ds \struct {\SS, \circ} = \prod_{k \mathop = 1}^n S_k$ be the external direct product of the algebraic structures $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \ldots, \struct {S_n, \circ_n}$.
Let $e_1, e_2, \ldots, e_n$ be the identity elements of $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \ldots, \struct {S_n, \circ_n}$ respectively.
Then $\tuple {e_1, e_2, \ldots, e_n}$ is the identity element of $\struct {\SS, \circ}$.

Proof:
Let $s := \tuple {s_1, s_2, \ldots, s_n}$ be an arbitrary element of $\struct {S_1, \circ_1} \times \struct {S_2, \circ_2} \times \cdots \times \struct {S_n, \circ_n}$.
Let $e := \tuple {e_1, e_2, \ldots, e_n}$.
Then:
{{begin-eqn}}
{{eqn | l = s \circ e
      | r = \tuple {s_1, s_2, \ldots, s_n} \circ \tuple {e_1, e_2, \ldots, e_n}
      | c = 
}}
{{eqn | r = \tuple {s_1 \circ_1 e_1, s_2 \circ_2 e_2, \ldots, s_n \circ_n e_n}
      | c = {{Defof|External Direct Product|subdef = General Definition}}
}}
{{eqn | r = \tuple {s_1, s_2, \ldots, s_n}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = s
      | c = Definition of $s$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = e \circ s
      | r = \tuple {e_1, e_2, \ldots, e_n} \circ \tuple {s_1, s_2, \ldots, s_n}
      | c = 
}}
{{eqn | r = \tuple {e_1 \circ_1 s_1, e_2 \circ_2 s_2, \ldots, e_n \circ_n s_n}
      | c = {{Defof|External Direct Product|subdef = General Definition}}
}}
{{eqn | r = \tuple {s_1, s_2, \ldots, s_n}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = s
      | c = Definition of $s$
}}
{{end-eqn}}
{{qed}}
Theorem: External Direct Product Commutativity/General Result

Let $\ds \struct {S, \circ} = \prod_{k \mathop = 1}^n S_k$ be the external direct product of the algebraic structures $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \ldots, \struct {S_n, \circ_n}$.
If $\circ_1, \ldots, \circ_n$ are all commutative, then so is $\circ$.

Proof:
Suppose that, for all $k \in \N^*_n$, $\circ_k$ is commutative.
Let $\tuple {s_1, s_2, \ldots, s_n}$ and $\tuple {t_1, t_2, \ldots, t_n}$ be elements of $\struct {S_1, \circ_1} \times \struct {S_2, \circ_2} \times \cdots \times \struct {S_n, \circ_n}$.
{{begin-eqn}}
{{eqn | l = \tuple {s_1, s_2, \ldots, s_n} \circ \tuple {t_1, t_2, \ldots, t_n}
      | r = \tuple {s_1 \circ_1 t_1, s_2 \circ_2 t_2, \ldots, s_n \circ_n t_n}
      | c = {{Defof|Operation Induced by Direct Product}}
}}
{{eqn | r = \tuple {t_1 \circ_1 s_1, t_2 \circ_2 s_2, \ldots, t_n \circ_n s_n}
      | c = {{Defof|Commutative Operation}}
}}
{{eqn | r = \tuple {t_1, t_2, \ldots, t_n} \circ \tuple {s_1, s_2, \ldots, s_n}
      | c = {{Defof|Operation Induced by Direct Product}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: External Direct Product Associativity/General Result

Let $\ds \struct {S, \circ} = \prod_{k \mathop = 1}^n S_k$ be the external direct product of the algebraic structures $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \ldots, \struct {S_n, \circ_n}$.
If $\circ_1, \ldots, \circ_n$ are all associative, then so is $\circ$.

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:If $\circ_1, \ldots, \circ_n$ are all associative, then so is the external direct product $\circ$ of $\circ_1, \ldots, \circ_n$.
Theorem: Vector Cross Product is not Associative

The vector cross product is ''not'' associative.
That is, in general:
:$\mathbf a \times \paren {\mathbf b \times \mathbf c} \ne \paren {\mathbf a \times \mathbf b} \times \mathbf c$
for $\mathbf a, \mathbf b, \mathbf c \in \R^3$.

Proof:
Proof by Counterexample:
Let:
{{begin-eqn}}
{{eqn | l = \mathbf a
      | r = \begin {bmatrix} 1 \\ 0 \\ 0 \end {bmatrix}
}}
{{eqn | l = \mathbf b
      | r = \begin {bmatrix} 1 \\ 1 \\ 0 \end {bmatrix}
}}
{{eqn | l = \mathbf c
      | r = \begin {bmatrix} 1 \\ 1 \\ 1 \end {bmatrix}
}}
{{end-eqn}}
be vectors in the real Euclidean space $\R^3$.
{{begin-eqn}}
{{eqn | l = \mathbf a \times \paren {\mathbf b \times \mathbf c}
      | r = \mathbf a \times \paren {\begin {bmatrix} 1 \\ 1 \\ 0 \end {bmatrix} \times \begin {bmatrix} 1 \\ 1 \\ 1 \end {bmatrix} }
}}
{{eqn | r = \mathbf a \times \begin {bmatrix} 1 \\ -1 \\ 0 \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} 1 \\ 0 \\ 0 \end {bmatrix} \times \begin {bmatrix} 1 \\ -1 \\ 0 \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} 0 \\ 0 \\ -1 \end {bmatrix}
}}
{{eqn | l = \paren {\mathbf a \times \mathbf b} \times \mathbf c
      | r = \paren {\begin {bmatrix} 1 \\ 0 \\ 0 \end {bmatrix} \times \begin {bmatrix} 1 \\ 1 \\ 0 \end {bmatrix} } \times \mathbf c
}}
{{eqn | r = \begin {bmatrix} 0 \\ 0 \\ 1 \end {bmatrix} \times \mathbf c
}}
{{eqn | r = \begin {bmatrix} 0 \\ 0 \\ 1 \end {bmatrix} \times \begin {bmatrix} 1 \\ 1 \\ 1 \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} -1 \\ 1 \\ 0 \end {bmatrix}
}}
{{end-eqn}}
{{qed}}
Theorem: Vector Cross Product is Anticommutative

The vector cross product is anticommutative:
:$\forall \mathbf a, \mathbf b \in \R^3: \mathbf a \times \mathbf b = -\paren {\mathbf b \times \mathbf a}$

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf b \times \mathbf a
      | r = \begin {bmatrix} b_i \\ b_j \\ b_k \end {bmatrix} \times \begin {bmatrix} a_i \\ a_j \\ a_k \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} b_j a_k - a_j b_k \\ b_k a_i - b_i a_k \\ b_i a_j - a_i b_j \end {bmatrix}
}}
{{eqn | l = \mathbf a \times \mathbf b
      | r = \begin {bmatrix} a_i \\ a_j \\ a_k \end {bmatrix} \times \begin {bmatrix} b_i \\ b_j \\ b_k \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} a_j b_k - a_k b_j \\ a_k b_i - a_i b_k \\ a_i b_j - a_j b_i \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} -\paren {a_k b_j - a_j b_k} \\ -\paren {a_i b_k - a_k b_i} \\ -\paren {a_j b_i - a_i b_j} \end {bmatrix}
}}
{{eqn | r = -1 \begin {bmatrix} b_j a_k - a_j b_k \\ b_k a_i - b_i a_k \\ b_i a_j - a_i b_j \end {bmatrix}
}}
{{eqn | r = -\paren {\mathbf b \times \mathbf a}
}}
{{end-eqn}}
{{qed}}
Theorem: Vector Cross Product is Anticommutative

The vector cross product is anticommutative:
:$\forall \mathbf a, \mathbf b \in \R^3: \mathbf a \times \mathbf b = -\paren {\mathbf b \times \mathbf a}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\mathbf a + \mathbf b} \times \paren {\mathbf a + \mathbf b}
      | r = \mathbf a \times \mathbf a + \mathbf a \times \mathbf b + \mathbf b \times \mathbf a + \mathbf b \times \mathbf b
      | c = Vector Cross Product Operator is Bilinear
}}
{{eqn | l = 0
      | r = 0 + \mathbf a \times \mathbf b + \mathbf b \times \mathbf a + 0
      | c = Cross Product of Vector with Itself is Zero
}}
{{eqn | l = \mathbf a \times \mathbf b
      | r = -\paren {\mathbf b \times \mathbf a}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Vector Cross Product is Anticommutative

The vector cross product is anticommutative:
:$\forall \mathbf a, \mathbf b \in \R^3: \mathbf a \times \mathbf b = -\paren {\mathbf b \times \mathbf a}$

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf a \times \mathbf b
      | r = \begin {vmatrix} \mathbf i & \mathbf j & \mathbf k \\ a_i & a_j & a_k \\ b_i & b_j & b_k \end {vmatrix}
      | c = {{Defof|Vector Cross Product}}
}}
{{eqn | r = -\begin {vmatrix} \mathbf i & \mathbf j & \mathbf k \\ b_i & b_j & b_k \\ a_i & a_j & a_k \end {vmatrix}
      | c = Determinant with Rows Transposed
}}
{{eqn | r = -\paren {\mathbf b \times \mathbf a}
      | c = {{Defof|Vector Cross Product}}
}}
{{end-eqn}}
{{qed}}