avewright/proofwiki-math huggingface dataset:
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:
From the definition of the vector cross product:
{{:Definition:Vector Cross Product/Definition 2}}
Hence we have that:
:$\mathbf a \times \mathbf b$ is a vector whose direction is specified according to the right-hand rule
while:
:$\mathbf b \times \mathbf a$ is a vector whose direction, also specified according to the right-hand rule, is exactly the opposite of that for $\mathbf a \times \mathbf b$.
That is:
:$\mathbf a \times \mathbf b = -\mathbf b \times \mathbf a$
{{qed}}
Theorem: Projection is Surjection/General Version

For all non-empty sets $S_1, S_2, \ldots, S_j, \ldots, S_n$, the $j$th projection $\pr_j$ on $\ds \prod_{i \mathop = 1}^n S_i$ is a surjection.

Proof:
Consider the $j$th projection.
As long as none of $S_1, S_2, \ldots, S_n$ is the empty set, then:
:$\ds \forall x \in S_j: \exists \tuple {s_1, s_2, \ldots, s_{j - 1}, x, s_{j + 1}, \ldots, s_n} \in \prod_{k \mathop = 1}^n S_k: \map {\pr_j} {\tuple {s_1, s_2, \ldots, s_{j - 1}, x, s_{j + 1}, \ldots, s_n} } = x$
Hence the result.
{{qed}}
Category:Surjections
Category:Projections
5l3rmajfqriobye2joyzvi6wa0w4sww
Theorem: Canonical Injection is Monomorphism/General Result

Let $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \dotsc, \struct {S_j, \circ_j}, \dotsc, \struct {S_n, \circ_n}$ be algebraic structures with identities $e_1, e_2, \dotsc, e_j, \dotsc, e_n$ respectively.
Then the canonical injection:
:$\ds \inj_j: \struct {S_j, \circ_j} \to \prod_{i \mathop = 1}^n \struct {S_i, \circ_i}$
defined as:
:$\map {\inj_j} x = \tuple {e_1, e_2, \dotsc, e_{j - 1}, x, e_{j + 1}, \dotsc, e_n}$
is a monomorphism.

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 \struct {S_j, \circ_j}$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\inj_j} {x \circ_j y}
      | r = \tuple {e_1, e_2, \dotsc, e_{j - 1}, x \circ_j y, e_{j + 1}, \dotsc, e_n}
}}
{{eqn | r = \tuple {e_1 \circ_1 e_1, e_2 \circ_2 e_2, \dotsc, e_{j - 1} \circ_{j - 1} e_{j - 1}, x \circ_j y, e_{j + 1} \circ_{j + 1} e_{j + 1}, \dotsc, e_n \circ_n e_n}
}}
{{eqn | r = \tuple {e_1, e_2, \dotsc, e_{j - 1}, x, e_{j + 1}, \dotsc, e_n} \circ \tuple {e_1, e_2, \dotsc, e_{j - 1}, y, e_{j + 1}, \dotsc, e_n}
}}
{{eqn | r = \map {\inj_j} x \circ \map {\inj_j} y
}}
{{end-eqn}}
and the morphism property has been demonstrated to hold.
Thus $\ds \inj_j: \struct {S_j, \circ_j} \to \prod_{i \mathop = 1}^n \struct {S_i, \circ_i}$ has been shown to be an injective homomorphism and therefore a monomorphism.
{{Qed}}
Theorem: Null Space of Reduced Echelon Form

Let $\mathbf A$ be a matrix in the matrix space $\map {\MM_\R} {m, n}$ such that:
:$\mathbf A \mathbf x = \mathbf 0$
represents a homogeneous system of linear equations.
The null space of $\mathbf A$ is the same as that of the null space of the reduced row echelon form of $\mathbf A$:
:$\map {\mathrm N} {\mathbf A} = \map {\mathrm N} {\map {\mathrm {rref} } {\mathbf A} }$

Proof:
By the definition of null space:
:$\mathbf x \in \map {\mathrm N} {\mathbf A} \iff \mathbf A \mathbf x = \mathbf 0$
From {{Corollary|Row Equivalent Matrix for Homogeneous System has same Solutions}}:
:$\mathbf A \mathbf x = \mathbf 0 \iff \map {\mathrm {rref} } {\mathbf A} \mathbf x = \mathbf 0$
Hence the result, by the definition of set equality.
{{qed}}
Theorem: Null Space Contains Only Zero Vector iff Columns are Independent

Let $\mathbb F$ be a field.
Let:
{{begin-eqn}}
{{eqn | l = \mathbf A_{m \times n}
      | r = \begin{bmatrix} \mathbf a_1 & \mathbf a_2 & \cdots & \mathbf a_n \end{bmatrix}
}}
{{end-eqn}}
be a matrix over $\mathbb F$ where:
:$\forall i: 1 \le i \le n: \mathbf a_i = \begin{bmatrix} a_{1i} \\ a_{2i} \\ \vdots \\ a_{mi} \end{bmatrix} \in \mathbb F^m$
are vectors.
Then:
:$\set {\mathbf a_1, \mathbf a_2, \cdots, \mathbf a_n}$ is a linearly independent set 
{{iff}}:
:$\map {\mathrm N} {\mathbf A} = \set {\mathbf 0_{n \times 1} }$
where $\map {\mathrm N} {\mathbf A}$ is the null space of $\mathbf A$.

Proof:
Let $\mathbf x = \begin{bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end{bmatrix} \in \mathbb F^m$.
We have that:
{{begin-eqn}}
{{eqn | l = \mathbf x
      | o = \in 
      | r = \map {\mathrm N} {\mathbf A}
}}
{{eqn | ll= \leadstoandfrom
      | l = \mathbf A \mathbf x_{n \times 1}
      | r = \mathbf 0_{m \times 1}
}}
{{eqn | ll= \leadstoandfrom
      | l = \begin{bmatrix} \mathbf a_1 & \mathbf a_2 & \cdots & \mathbf a_n \end{bmatrix} \begin{bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end{bmatrix}
      | r = \begin{bmatrix} 0 \\ 0 \\ \vdots \\ 0 \end{bmatrix}
}}
{{eqn | ll= \leadstoandfrom
      | l = \sum_{k \mathop = 1}^n x_k \mathbf a_k
      | r = \mathbf 0
}}
{{end-eqn}}
Theorem: Axiom of Dependent Choice Implies Axiom of Countable Choice

The axiom of dependent choice implies the axiom of countable choice.

Proof:
Let $\sequence {S_n}_{n \mathop \in \N}$ be a sequence of non-empty sets.
Define:
:$\ds S = \bigsqcup_{n \mathop \in \N} S_n$
where $\bigsqcup$ denotes disjoint union.
Let $\RR$ be the binary endorelation on $S$ defined by:
:$\tuple {x, m} \mathrel \RR \tuple {y, n} \iff n = m + 1$
Note that $\RR$ satisfies:
:$\forall a \in S : \exists b \in S : a \mathrel \RR b$
Using the axiom of dependent choice, there exists a sequence $\sequence {y_n}_{n \mathop \in \N}$ in $S$ such that $y_n \mathrel \RR y_{n + 1}$ for all $n \in \N$.
Letting $y_n = \tuple {s_n, N_n}$ for all $n \in \N$, it follows by the definition of $\RR$ that $N_{n + 1} = N_n + 1$.
A straightforward application of mathematical induction shows that $N_n = n + N$ for some $N \in \N$.
So $s_n \in S_{n + N}$ for all $n \in \N$.
The cartesian product $S_0 \times S_1 \times \cdots \times S_{N - 1}$ is non-empty.
So there exists a finite sequence $x_0, x_1, \ldots, x_{N - 1}$ with $x_n \in S_n$ for all natural numbers $n < N$.
Now, define $x_n = s_{n - N}$ for all natural numbers $n \ge N$.
Then $x_n \in S_n$ for all $n \in \N$.
{{qed}}
{{ADC||3}}
Theorem: Axiom of Choice Implies Axiom of Dependent Choice

The axiom of choice implies the axiom of dependent choice.

Proof:
Let $\RR$ be a binary endorelation on a non-empty set $S$ such that:
:$\forall a \in S: \exists b \in S: a \mathrel \RR b$
For an element $x \in S$, define:
:$\map R x = \set {y \in S: x \mathrel \RR y}$
By assumption, $\map R x$ is non-empty for all $x \in S$.
Now, consider the indexed family of sets:
:$\family {\map R x}_{x \mathop \in S}$
Using the axiom of choice, there exists a mapping $f: S \to S$ such that:
:$\forall x \in S: \map f x \in \map R x$
That is:
:$x \mathrel \RR \map f x$
So, for any $x \in S$, the sequence:
:$\sequence {x_n}_{n \mathop \in \N} = \sequence {\map {f^n} x}_{n \mathop \in \N}$
where $f^n$ denotes the composition of $f$ with itself $n$ times, is a sequence such that:
:$x_n \mathrel \RR x_{n + 1}$
for all $n \in \N$, as desired.
{{qed}}
Theorem: Infimum of Empty Set is Greatest Element

Let $\struct {S, \preceq}$ be an ordered set.
Suppose that $\map \inf \O$, the infimum of the empty set, exists in $S$.
Then $\forall s \in S: s \preceq \map \inf \O$.
That is, $\map \inf \O$ is the greatest element of $S$.

Proof:
Observe that, vacuously, any $s \in S$ is a lower bound for $\O$.
But for any lower bound $s$ of $\O$, $s \preceq \map \inf \O$ by definition of infimum.
Hence:
:$\forall s \in S: s \preceq \map \inf \O$
{{qed}}
Theorem: Supremum of Empty Set is Smallest Element

Let $\struct {S, \preceq}$ be an ordered set.
Then:
:the supremum in $S$ of the empty set exists {{iff}} the smallest element of $S$ exists
in which case:
:$\map \sup \O$ is the smallest element of $S$

Proof:
Observe that, vacuously, any $s \in S$ is an upper bound for $\O$.
Theorem: Countable Union of Countable Sets is Countable

Let the {{Axiom-link|Countable Choice}} be accepted.
Then it can be proved that a countable union of countable sets is countable.

Proof:
Consider the countable sets $S_0, S_1, S_2, \ldots$ where $\ds S = \bigcup_{i \mathop \in \N} {S_i}$.
Assume that none of these sets have any elements in common.
Otherwise, we can consider the sets $S_0' = S_0, S_1' = S_1 \setminus S_0, S_2' = S_2 \setminus \paren {S_0 \cup S_1}, \ldots$
All of these are countable by Subset of Countable Set is Countable, and they have the same union $\ds S = \bigcup_{i \mathop \in \N} {S_i'}$.
Now we write the elements of $S_0', S_1', S_2', \ldots$ in the form of a (possibly infinite) table:
:<nowiki>$\begin{array} {*{4}c}
 {a_{00}} & {a_{01}} & {a_{02}} & \cdots \\
 {a_{10}} & {a_{11}} & {a_{12}} & \cdots \\
 {a_{20}} & {a_{21}} & {a_{22}} & \cdots \\
 \vdots  & \vdots  & \vdots & \ddots \\
\end{array}$</nowiki>
where $a_{ij}$ is the $j$th element of set $S_i$.
This table clearly contains all the elements of $\ds S = \bigcup_{i \mathop \in \N} {S_i}$.
Furthermore, we have that $\phi: S \to \N \times \N, a_{ij} \mapsto \tuple {i, j}$ is an injection.
By Cartesian Product of Countable Sets is Countable, there exists an injection $\psi: \N \times \N \to \N$.
Then $\psi \circ \phi: S \to \N$ is also an injection by Composite of Injections is Injection.
That is to say, $S$ is countable.
{{qed}}
Theorem: Countable Union of Countable Sets is Countable

Let the {{Axiom-link|Countable Choice}} be accepted.
Then it can be proved that a countable union of countable sets is countable.

Proof:
Let $\sequence {S_n}_{n \mathop \in \N}$ be a sequence of countable sets.
Define:
:$\ds S = \bigcup_{n \mathop \in \N} S_n$
For all $n \in \N$, let $\FF_n$ denote the set of all injections from $S_n$ to $\N$.
Since $S_n$ is countable, $\FF_n$ is non-empty.
Using the {{Axiom-link|Countable Choice}}, there exists a sequence $\sequence {f_n}_{n \mathop \in \N}$ such that $f_n \in \FF_n$ for all $n \in \N$.
Let $\phi: S \to \N \times \N$, where $\times$ denotes the cartesian product, be the mapping defined by:
:$\map \phi x = \tuple {n, \map {f_n} x}$
where $n$ is the (unique) smallest natural number such that $x \in S_n$.
From the Well-Ordering Principle, such an $n$ exists; hence, the mapping $\phi$ exists.
Since each $f_n$ is an injection, it (trivially) follows that $\phi$ is an injection.
Since $\N \times \N$ is countable, there exists an injection $\alpha: \N \times \N \to \N$.
From Composite of Injections is Injection, the mapping $\alpha \circ \phi: S \to \N$ is an injection.
Hence, $S$ is countable.
{{qed}}
Theorem: Countable Union of Countable Sets is Countable

Let the {{Axiom-link|Countable Choice}} be accepted.
Then it can be proved that a countable union of countable sets is countable.

Proof:
Let $\sequence {S_n}_{n \mathop \in \N}$ be a sequence of countable sets.
Define:
:$\ds S = \bigcup_{n \mathop \in \N} S_n$.
For all $n \in \N$, let $\FF_n$ be the set of all surjections from $\N$ to $S_n$.
Since $S_n$ is countable, it follows by Surjection from Natural Numbers iff Countable that $\FF_n$ is non-empty.
Using the {{Axiom-link|Countable Choice}}, there exists a sequence $\sequence {f_n}_{n \mathop \in \N}$ such that $f_n \in \FF_n$ for all $n \in \N$.
Let $\phi: \N \times \N \to S$, where $\times$ denotes the cartesian product, be the surjection defined by:
:$\map \phi {m, n} = \map {f_m} n$
Since $\N \times \N$ is countable, it follows by Surjection from Natural Numbers iff Countable that there exists a surjection $\alpha: \N \to \N \times \N$.
Since the composition of surjections is a surjection, the mapping $\phi \circ \alpha: \N \to S$ is a surjection.
By Surjection from Natural Numbers iff Countable, it follows that $S$ is countable.
{{qed}}
Theorem: Projection is Epimorphism/General Result

Let $\struct {\SS, \circ}$ be the external direct product of the algebraic structures $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \ldots, \struct {S_k, \circ_k}, \ldots, \struct {S_n, \circ_n}$.
Then:
:for each $j \in \closedint 1 n$, $\pr_j$ is an epimorphism from $\struct {\SS, \circ}$ to $\struct {S_j, \circ_j}$
where $\pr_j: \struct {\SS, \circ} \to \struct {S_j, \circ_j}$ is the $j$th projection from $\struct {\SS, \circ}$ to $\struct {S_j, \circ_j}$.

Proof:
From Projection is Surjection, $\pr_j$ is a surjection for all $j$.
We now need to show it is a homomorphism.
Let $\mathbf s, \mathbf t \in \struct {\SS, \circ}$ where $\mathbf s = \tuple {s_1, s_2, \ldots, s_j, \ldots, s_n}$ and $\mathbf t = \tuple {t_1, t_2, \ldots, t_j, \ldots, t_n}$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\pr_j} {\mathbf s \circ \mathbf t}
      | r = \map {\pr_j} {\tuple {s_1, s_2, \ldots, s_j, \ldots, s_n} \circ \tuple {t_1, t_2, \ldots, t_j, \ldots, t_n} }
      | c =  Definition of $\mathbf s$ and $\mathbf t$
}}
{{eqn | r = \map {\pr_j} {\tuple {s_1 \circ_1 t_1, s_2 \circ_2 t_2, \ldots, s_j \circ_j t_j, \ldots, s_n \circ_n t_n} }
      | c = 
}}
{{eqn | r = s_j \circ_j t_j
      | c = 
}}
{{eqn | r = \map {\pr_j} {\mathbf s} \circ_j \map {\pr_j} {\mathbf t}
      | c = 
}}
{{end-eqn}}
and thus the morphism property is demonstrated.
{{Qed}}
Theorem: External Direct Product of Projection with Canonical Injection/General Result

Let $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \dotsc, \struct {S_j, \circ_j}, \dotsc, \struct {S_n, \circ_n}$ be algebraic structures with identities $e_1, e_2, \dotsc, e_j, \dotsc, e_n$ respectively.
Let $\ds \struct {S, \circ} = \prod_{i \mathop = 1}^n \struct {S_i, \circ_i}$ be the external direct product of $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \dotsc, \struct {S_j, \circ_j}, \dotsc, \struct {S_n, \circ_n}$.
Let $\pr_j: \struct {S, \circ} \to \struct {S_j, \circ_j}$ be the $j$th projection from $\struct {S, \circ}$ to $\struct {S_j, \circ_j}$.
Let $\inj_j: \struct {S_j, \circ_j} \to \struct {S, \circ}$ be the canonical injection from $\struct {S_j, \circ_j}$ to $\struct {S, \circ}$.
Then:
:$\pr_j \circ \inj_j = I_{S_j}$
where $I_{S_j}$ is the identity mapping from $S_j$ to $S_j$.

Proof:
Let $\ds \tuple {s_1, s_2, \dotsc, s_{j - 1}, s_j, s_{j + 1}, \dotsc, s_n} \in \prod_{i \mathop = 1}^n \struct {S_i, \circ_i}$.
So:
:$s_j \in S_j$
From the definition of the canonical injection:
:$\map {\inj_j} {s_j} = \tuple {e_1, e_2, \dotsc, e_{j - 1}, s_j, e_{j + 1}, \dotsc, e_n}$
So from the definition of the $j$th projection:
:$\map {\pr_j} {e_1, e_2, \dotsc, e_{j - 1}, s_j, e_{j + 1}, \dotsc, e_n} = s_j$
Thus:
:$\map {\pr_j \circ \inj_j} {s_j} = s_j$
and the result follows from the definition of the identity mapping.
{{qed}}
Theorem: Extended Real Addition is Commutative

Extended real addition $+_{\overline{\R}}$ is commutative.
That is, for all $x, y \in \overline{\R}$:
:$x +_{\overline{\R}} y = y +_{\overline{\R}} x$
whenever at least one of the sides is defined.

Proof:
When $x,y \in \R$, then $x +_{\overline{\R}} y = y +_{\overline{\R}} x$ follows from Real Addition is Commutative.
The remaining cases where the expressions are defined, are already imposed in the definition of $+_{\overline{\R}}$.
{{qed}}
Category:Extended Real Numbers
re0bgbsugf5tynnbcvx6y0icrntr5fa
Theorem: Extended Real Addition is Associative

Extended real addition $+_{\overline{\R}}$ is commutative.
That is, for all $x, y, z \in \overline \R$:
:$(1): \quad x +_{\overline \R} \paren {y +_{\overline \R} z} = \paren {x +_{\overline \R} y} +_{\overline \R} z$
whenever at least one of the sides is defined.

Proof:
When $x, y, z \in \R$, then $(1)$ follows from Real Addition is Associative.
From the definition of $+_{\overline \R}$, it follows that either expression in $(1)$ is defined {{iff}} at most one of $+\infty$ and $-\infty$ occurs.
The case where neither occurs is already covered above; now assume that $+\infty$ occurs (the case with $-\infty$ is similar).
By Extended Real Addition is Commutative, it suffices to consider the cases $x = +\infty$ and $y = +\infty$.
Suppose $x = +\infty$.
Then as $y \ne -\infty$ and $z \ne -\infty$, it follows that $\paren {+\infty} +_{\overline \R} y = +\infty$, and $\paren {+\infty} +_{\overline \R} z = +\infty$.
Hence the {{RHS}} in $(1)$ equals $+\infty$.
But $y +_{\overline \R} z \ne -\infty$ as well, and so the {{LHS}} also equals $+\infty$.
Now suppose $y = +\infty$.
Then, again, $x +_{\overline \R} \paren {+\infty} = +\infty$ and $\paren {+\infty} +_{\overline \R} z = +\infty$.
The result follows by applying these two equalities in the appropriate order on both the {{LHS}} and the {{RHS}} of $(1)$.
Hence the result, from Proof by Cases.
{{qed}}
Category:Extended Real Numbers
fos8oaezxu9vvearil6srl078nafuvv
Theorem: Extended Real Multiplication is Commutative

Extended real multiplication $\times_{\overline \R}$ is commutative.
That is, for all $x, y \in \overline \R$:
:$x \times_{\overline \R} y = y \times_{\overline \R} x$

Proof:
Let $x, y \in \R$.
Then from Real Multiplication is Commutative:
:$x \times_{\overline \R} y = y \times_{\overline \R} x$
The remaining cases are explicitly imposed in the definition of $\times_{\overline \R}$.
{{qed}}
Category:Extended Real Numbers
ers5dtbwrqxqxdxuunybf70906gsovl
Theorem: Extended Real Multiplication is Associative

Extended real multiplication $\cdot_{\overline \R}$ is commutative.
That is, for all $x, y, z \in \overline \R$:
:$(1): \quad x \cdot_{\overline \R} \left({y \cdot_{\overline \R} z}\right) = \left({x \cdot_{\overline \R} y}\right) \cdot_{\overline \R} z$

Proof:
When $x, y, z \in \R$, then $(1)$ follows from Real Multiplication is Associative.
Next, the cases where at least one of $+\infty$ and $-\infty$ occurs need to be dealt with.
{{ProofWanted|when someone thinks of a nice way to deal with the case distinctions, go ahead}}
Category:Extended Real Numbers
42pagy9miv7xxla3wtfi3au46flcowq
Theorem: Extended Real Numbers under Multiplication form Monoid

Denote with $\overline \R$ the extended real numbers.
Denote with $\cdot_{\overline \R}$ the extended real multiplication.
The algebraic structure $\struct {\overline \R, \cdot_{\overline \R} }$ is a monoid.

Proof:
Checking the axioms for a monoid in turn:
Theorem: Extended Real Numbers under Multiplication form Commutative Monoid

Denote with $\overline \R$ the extended real numbers.
Denote with $\cdot_{\overline \R}$ the extended real multiplication.
The algebraic structure $\struct {\overline \R, \cdot_{\overline \R} }$ is a commutative monoid.

Proof:
By Extended Real Numbers under Multiplication form Monoid, $\struct {\overline \R, \cdot_{\overline \R} }$ is a monoid.
By Extended Real Multiplication is Commutative, $\cdot_{\overline \R}$ is commutative.
Hence $\struct {\overline \R, \cdot_{\overline \R} }$ is a commutative monoid.
{{qed}}
Category:Extended Real Numbers
Category:Examples of Commutative Monoids
fqyc6hw34plys8gs6g1wmw9vlzvurh1
Theorem: Translation in Euclidean Space is Measurable Mapping

Let $\BB$ be the Borel $\sigma$-algebra on $\R^n$.
Let $\mathbf x \in \R^n$, and denote with $\tau_{\mathbf x}: \R^n \to \R^n$ translation by $\mathbf x$.
Then $\tau_{\mathbf x}$ is $\BB \, / \, \BB$-measurable.

Proof:
By Characterization of Euclidean Borel Sigma-Algebra, $\BB = \map \sigma {\JJ_{ho}^n}$.
Here, $\JJ_{ho}^n$ is the set of half-open $n$-rectangles, and $\sigma$ denotes generated $\sigma$-algebra.
Now, for any half-open $n$-rectangle $\horectr {\mathbf a} {\mathbf b}$, it is trivial that:
:$\map {\tau_{\mathbf x}^{-1} } {\horectr {\mathbf a} {\mathbf b} } = \horectr {\mathbf a + \mathbf x} {\mathbf b + \mathbf x}$
That is, the preimage of a half-open $n$-rectangle under $\tau_{\mathbf x}$ is again a half-open $n$-rectangle.
In particular, since $\JJ_{ho}^n \subseteq \map \sigma {\JJ_{ho}^n} = \BB$, Mapping Measurable iff Measurable on Generator applies.
Thus it follows that $\tau_{\mathbf x}$ is $\BB \, / \, \BB$-measurable.
{{qed}}
Theorem: Conditions for Internal Group Direct Product

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $H$ and $K$ be subgroups of $G$.
Let the mapping $\phi: H \times K \to G$ defined as:
:$\forall h \in H, k \in K: \map \phi {h, k} = h \circ k$
be a group isomorphism from the cartesian product $\struct {H, \circ {\restriction_H} } \times \struct {K, \circ {\restriction_K} }$ onto $\struct {G, \circ}$.
Then $G$ is the internal group direct product of $H$ and $K$ {{iff}}:
:$(1): \quad \forall h \in H, k \in K: h \circ k = k \circ h$
:$(2): \quad G = H \circ K$
:$(3): \quad H \cap K = \set e$

Proof:
=== Necessary Condition ===
Let the mapping $\phi: H \times K \to G$ defined as:
:$\forall h \in H, k \in K: \map \phi {h, k} = h \circ k$
be a group isomorphism from the cartesian product $\struct {H, \circ {\restriction_H} } \times \struct {K, \circ {\restriction_K} }$ onto $\struct {G, \circ}$.
Let the symbol $\circ$ also be used for the operation induced on $H \times K$ by $\circ {\restriction_H}$ and $\circ {\restriction_K}$.
;$(1): \quad \forall h \in H, k \in K: h \circ k = k \circ h$:
This follows directly from Internal Group Direct Product Commutativity.
{{qed|lemma}}
;$(2): \quad G = H \circ K$
This follows directly from Codomain of Internal Direct Isomorphism is Subset Product of Factors.
{{qed|lemma}}
;$(3): \quad H \cap K = \set e$
Let $z \in H \cap K$.
From Intersection of Subgroups is Subgroup, $z^{-1} \in H \cap K$.
So $\tuple {z, z^{-1} } \in H \times K$ and so:
:$\map \phi {z, z^{-1} } = z \circ z^{-1} = e = \map \phi {e, e}$
We have by definition that $\phi$ is a (group) isomorphism, therefore a bijection and so an injection.
So, as $\phi$ is injection, we have that:
:$\tuple {z, z^{-1} } = \tuple {e, e}$
and therefore $z = e$.
{{qed|lemma}}
Theorem: Internal Group Direct Product Commutativity/General Result

Let $\struct {G, \circ}$ be the internal group direct product of $H_1, H_2, \ldots, H_n$.
Let $h_i$ and $h_j$ be elements of $H_i$ and $H_j$ respectively, $i \ne j$.
Then $h_i \circ h_j = h_j \circ h_i$.

Proof:
Let $g = h_i \circ h_j \circ h_i^{-1} \circ h_j^{-1}$.
From the Internal Direct Product Theorem: General Result, $H_i$ and $H_j$ are normal in $G$.
Hence $h_i \circ h_j \circ h_i^{-1} \in H_j$ and thus $g \in H_j$.
Similarly, $g \in H_i$ and thus $g \in H_i \cap H_j$.
But:
{{begin-eqn}}
{{eqn | l = H_i \cap H_j
      | r = \set e
      | c = 
}}
{{eqn | ll= \leadsto
      | l = g
      | r = h_i \circ h_j \circ h_i^{-1} \circ h_j^{-1}
      | c = 
}}
{{eqn | r = e
      | c = 
}}
{{eqn | ll= \leadsto
      | l = h_i \circ h_j \circ h_i^{-1}
      | r = h_j
      | c = 
}}
{{eqn | ll= \leadsto
      | l = h_i \circ h_j
      | r = h_j \circ h_i
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Pre-Image Sigma-Algebra on Codomain is Sigma-Algebra

Let $X, X'$ be sets, and let $f: X \to X'$ be a mapping.
Let $\Sigma$ be a $\sigma$-algebra on $X$.
Denote with $\Sigma'$ the pre-image $\sigma$-algebra on the domain of $f$.
Then $\Sigma'$ is a $\sigma$-algebra on $X'$.

Proof:
Verify the axioms for a $\sigma$-algebra in turn:
Theorem: Mapping Measurable iff Measurable on Generator

Let $\struct {X, \Sigma}$ and $\struct {X', \Sigma'}$ be measurable spaces.
Suppose that $\Sigma'$ is generated by $\GG'$.
Then a mapping $f: X \to X'$ is $\Sigma \, / \, \Sigma'$-measurable {{iff}}:
:$\forall G' \in \GG': \map {f^{-1} } {G'} \in \Sigma$
That is, {{iff}} the preimage of every generator under $f$ is a measurable set.

Proof:
=== Necessary Condition ===
Let $f$ be $\Sigma \, / \, \Sigma'$-measurable.
By definition of generated $\sigma$-algebra $\GG' \subseteq \Sigma'$.
Hence, in particular, $f$ satisfies:
:$\forall G' \in \GG': \map {f^{-1} } {G'} \in \Sigma$
{{qed|lemma}}