avewright/proofwiki-math huggingface dataset:
Theorem: Homomorphism of Powers/Integers

Let $\struct {T_1, \odot}$ and $\struct {T_2, \oplus}$ be monoids.
Let $\phi: \struct {T_1, \odot} \to \struct {T_2, \oplus}$ be a (semigroup) homomorphism.
Let $a$ be an invertible element of $T_1$.
Let $n \in \Z$.
Let $\odot^n$ and $\oplus^n$ be as defined as in Index Laws for Monoids.
Then:
:$\forall n \in \Z: \map \phi {\map {\odot^n} a} = \map {\oplus^n} {\map \phi a}$

Proof:
By Homomorphism of Powers: Natural Numbers, we need show this only for negative $n$, that is:
:$\forall n \in \N^*: \map \phi {\map {\odot^{-n} } a} = \map {\oplus^{-n} } {\map \phi a}$
But by Homomorphism with Identity Preserves Inverses:
:$\map \phi {a^{-1} } = \paren {\map \phi a}^{-1}$
Hence by Homomorphism of Powers: Natural Numbers:
:$\map {\oplus^{-n} } {\map \phi a} = \map {\oplus^n} {\map \phi {a^{-1} } } = \map \phi {\map {\odot^n} {a^{-1} } } = \map \phi {\map {\odot^{-n} } a}$
{{qed}}
Theorem: Right Operation is Left Distributive over All Operations

Let $\struct {S, \circ, \rightarrow}$ be an algebraic structure where:
:$\rightarrow$ is the right operation
:$\circ$ is any arbitrary binary operation.
Then $\rightarrow$ is left distributive over $\circ$.

Proof:
By definition of the right operation:
{{begin-eqn}}
{{eqn | l = a \rightarrow \paren {b \circ c}
      | r = b \circ c
      | c = 
}}
{{eqn | r = \paren {a \rightarrow b} \circ \paren {a \rightarrow c}
      | c = 
}}
{{end-eqn}}
The result follows by definition of left distributivity.
{{qed}}
Theorem: Left Operation is Right Distributive over All Operations

Let $\struct {S, \circ, \leftarrow}$ be an algebraic structure where:
:$\leftarrow$ is the left operation
:$\circ$ is any arbitrary binary operation.
Then $\leftarrow$ is right distributive over $\circ$.

Proof:
{{begin-eqn}}
{{eqn | l = \forall a, b, c \in S: \paren {a \circ b} \leftarrow c
      | r = a \circ b
      | c = {{Defof|Left Operation}}
}}
{{eqn | r = \paren {a \leftarrow c} \circ \paren {b \leftarrow c}
      | c = {{Defof|Left Operation}}
}}
{{end-eqn}}
The result follows by definition of right distributivity.
{{qed}}
Theorem: Right Operation is Distributive over Idempotent Operation

Let $\struct {S, \circ, \rightarrow}$ be an algebraic structure where:
:$\rightarrow$ is the right operation
:$\circ$ is any arbitrary binary operation.
Then:
:$\rightarrow$ is distributive over $\circ$
{{iff}}
:$\circ$ is idempotent.

Proof:
From Right Operation is Left Distributive over All Operations:
:$\forall a, b, c \in S: a \rightarrow \paren {b \circ c} = \paren {a \rightarrow b} \circ \paren {a \rightarrow c}$
for all binary operations $\circ$.
It remains to show that $\rightarrow$ is right distributive over $\circ$ {{iff}} $\circ$ is idempotent.
Theorem: Left Operation is Distributive over Idempotent Operation

Let $\struct {S, \circ, \leftarrow}$ be an algebraic structure where:
:$\leftarrow$ is the left operation
:$\circ$ is any arbitrary binary operation.
Then:
:$\leftarrow$ is distributive over $\circ$
{{iff}}:
:$\circ$ is idempotent.

Proof:
From Left Operation is Right Distributive over All Operations:
:$\forall a, b, c \in S: \paren {a \circ b} \leftarrow c = \paren {a \leftarrow c} \circ \paren {b \leftarrow c}$
for all binary operations $\circ$.
It remains to show that $\leftarrow$ is left distributive over $\circ$ {{iff}} $\circ$ is idempotent.
Theorem: Integral of Characteristic Function/Corollary

:$\ds \int \chi_E \rd \mu = \map \mu E$
where the integral sign denotes the $\mu$-integral of $\chi_E$.

Proof:
By Integral of Characteristic Function, have:
:$\map {I_\mu} {\chi_E} = \map \mu E$
where $\map {I_\mu} {\chi_E}$ is the $\mu$-integral of $\chi_E$.
From Integral of Positive Measurable Function Extends Integral of Positive Simple Function, it also holds that:
:$\ds \int \chi_E \rd \mu = \map {I_\mu} {\chi_E}$
Combining these equalities gives the result.
{{qed}}
Theorem: Integral of Positive Measurable Function is Positive Homogeneous

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f : X \to \overline \R$ be a positive $\Sigma$-measurable function.
Let $\lambda \in \overline \R$ be an extended real number with $\lambda \ge 0$. 
Then:
:$\ds \int \lambda f \rd \mu = \lambda \int f \rd \mu$
where:
:$\lambda f$ is the pointwise $\lambda$-multiple of $f$
:The integral sign denotes $\mu$-integration
This can be summarized by saying that $\ds \int \cdot \rd \mu$ is positive homogeneous.

Proof:
Suppose that $\lambda < \infty$. 
From Measurable Function is Pointwise Limit of Simple Functions, there exists an increasing sequence $\sequence {f_n}_{n \mathop \in \N}$ of positive simple functions such that: 
:$\ds \map f x = \lim_{n \mathop \to \infty} \map {f_n} x$
From the Multiple Rule for Real Sequences, we have: 
:$\ds \lambda \map f x = \lim_{n \mathop \to \infty} \paren {\lambda \map {f_n} x}$
for each $x \in X$. 
We then have: 
{{begin-eqn}}
{{eqn	| l = \int \lambda f \rd \mu
		| r = \lim_{n \mathop \to \infty} \int \lambda f_n \rd \mu
		| c = Integral of Positive Measurable Function as Limit of Integrals of Positive Simple Functions
}}
{{eqn	| r = \lambda \lim_{n \mathop \to \infty} \int f_n \rd \mu
		| c = Integral of Positive Simple Function is Positive Homogeneous 
}}
{{eqn	| r = \lambda \int f \rd \mu
		| c = Integral of Positive Measurable Function as Limit of Integrals of Positive Simple Functions
}}
{{end-eqn}}
so we get the demand in the case $\lambda < \infty$.
Now suppose that $\lambda = \infty$. 
We can write: 
:$\ds \lambda f = \lim_{k \mathop \to \infty} k f$
Since $f \ge 0$, the sequence $\sequence {k f}_{k \mathop \in \N}$ is increasing, we have: 
:$\ds \int \lambda f \rd \mu = \lim_{k \mathop \to \infty} \int k f \rd \mu$ 
from the monotone convergence theorem.
From our earlier work, we have: 
:$\ds \int k f \rd \mu = k \int f \rd \mu$
so that: 
{{begin-eqn}}
{{eqn	| l = \int \lambda f \rd \mu
		| r = \lim_{k \to \infty} k \int f \rd \mu
}}
{{eqn	| r = \paren {\lim_{k \to \infty} k} \int f \rd \mu
}}
{{eqn	| r = \lambda \int f \rd \mu
}}
{{end-eqn}}
giving the demand in the case $\lambda = \infty$.
{{qed}}
Theorem: Linear Transformation as Matrix Product

Let $T: \R^n \to \R^m, \mathbf x \mapsto \map T {\mathbf x}$ be a linear transformation.
Then:
:$\map T {\mathbf x} = \mathbf A_T \mathbf x$
where $\mathbf A_T$ is the $m \times n$ matrix defined as:
:$\mathbf A_T = \begin {bmatrix} \map T {\mathbf e_1} & \map T {\mathbf e_2} & \cdots & \map T {\mathbf e_n} \end {bmatrix}$
where $\tuple {\mathbf e_1, \mathbf e_2, \cdots, \mathbf e_n}$ is the standard ordered basis of $\R^n$.

Proof:
Let $\mathbf x = \begin {bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end {bmatrix}$.
Let $\mathbf I_n$ be the unit matrix of order $n$.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf x_{n \times 1}
      | r = \mathbf I_n \mathbf x_{n \times 1}
      | c = {{Defof|Left Identity}}
}}
{{eqn | r = \begin {bmatrix} 1 & 0 & \cdots & 0 \\ 0 & 1 & \cdots & 0 \\ \vdots & \vdots & \ddots & \vdots \\ 0 & 0 & \cdots & 1 \\ \end{bmatrix}\begin{bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end {bmatrix}
      | c = Unit Matrix is Identity:Lemma
}}
{{eqn | r = \begin {bmatrix} \mathbf e_1 & \mathbf e_2 & \cdots & \mathbf e_n \end {bmatrix} \begin {bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end {bmatrix}
      | c = {{Defof|Standard Ordered Basis on Vector Space}}
}}
{{eqn | r = \sum_{i \mathop = 1}^n \mathbf e_i x_i
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{eqn | l = \map T {\mathbf x}
      | r = \map T {\sum_{i \mathop =1}^n \mathbf e_i x_i}
}}
{{eqn | r = \sum_{i \mathop = 1}^n \map T {\mathbf e_i} x_i
      | c = {{Defof|Linear Transformation on Vector Space}}
}}
{{eqn | r = \begin {bmatrix} \map T {\mathbf e_1} & \map T {\mathbf e_2} & \cdots & \map T {\mathbf e_n} \end {bmatrix} \begin {bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end {bmatrix}
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{end-eqn}}
That $\mathbf A_T$ is $m \times n$ follows from each $\map T {\mathbf e_i}$ being an element of $\R^m$ and thus having $m$ rows.
{{qed}}
Theorem: Integral of Positive Measurable Function is Additive

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f : X \to \overline \R$ and $g : X \to \overline \R$ be positive $\Sigma$-measurable functions.
Then:
:$\ds \int \paren {f + g} \rd \mu = \int f \rd \mu + \int g \rd \mu$
where:
:$f + g$ is the pointwise sum of $f$ and $g$
:the integral sign denotes $\mu$-integration
This can be summarized by saying that $\ds \int \cdot \rd \mu$ is additive.

Proof:
We are given that $f : X \to \overline \R$ and $g : X \to \overline \R$ is a positive $\Sigma$-measurable functions, which is {{afortiori}} a measurable function, so we can apply Measurable Function is Pointwise Limit of Simple Functions.
From Measurable Function is Pointwise Limit of Simple Functions, there exists an increasing sequence $\sequence {f_n}_{n \mathop \in \N}$ of positive simple functions such that: 
:$\ds \map f x = \lim_{n \mathop \to \infty} \map {f_n} x$
for each $x \in X$. 
Similarly, there exists an increasing sequence $\sequence {g_n}_{n \mathop \in \N}$ of positive simple functions such that: 
:$\ds \map g x = \lim_{n \mathop \to \infty} \map {g_n} x$
for each $x \in X$. 
From the Sum Rule for Real Sequences, we have: 
:$\ds \map f x + \map g x = \lim_{n \mathop \to \infty} \paren {\map {f_n} x + \map {g_n} x}$
for each $x \in X$.
We then have: 
{{begin-eqn}}
{{eqn	| l = \int \paren {f + g} \rd \mu
		| r = \lim_{n \mathop \to \infty} \int \paren {f_n + g_n} \rd \mu
		| c = Integral of Positive Measurable Function as Limit of Integrals of Positive Simple Functions
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \paren {\int f_n \rd \mu + \int g_n \rd \mu}
		| c = Integral of Positive Simple Function is Additive
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \int f_n \rd \mu + \lim_{n \mathop \to \infty} \int g_n \rd \mu
		| c = Sum Rule for Real Sequences
}}
{{eqn	| r = \int f \rd \mu + \int g \rd \mu
		| c = Integral of Positive Measurable Function as Limit of Integrals of Positive Simple Functions
}}
{{end-eqn}}
{{qed}}
Theorem: Integral of Positive Simple Function is Increasing

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f, g: X \to \R$, $f, g \in \EE^+$ be positive simple functions.
Suppose that:
: $f \le g$
where $\le$ denotes pointwise inequality.
Then:
:$\map {I_\mu} f \le \map {I_\mu} g$
where $I_\mu$ denotes $\mu$-integration
This can be summarized by saying that $I_\mu$ is an increasing mapping.

Proof:
Note that: 
:$g - f \ge 0$ 
From Scalar Multiple of Simple Function is Simple Function and Pointwise Sum of Simple Functions is Simple Function, we then have that: 
:$g - f \in \EE^+$ 
Write: 
:$g = f + \paren {g - f}$ 
From Integral of Positive Simple Function is Additive, we then have: 
:$\map {I_\mu} g = \map {I_\mu} f + \map {I_\mu} {g - f}$ 
Since: 
:$\map {I_\mu} {g - f} \ge 0$ 
we obtain: 
:$\map {I_\mu} f \le \map {I_\mu} g$
{{qed}}
Theorem: Integral of Positive Measurable Function is Monotone

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f, g: X \to \overline \R$ be positive $\Sigma$-measurable functions.
Suppose that $f \le g$, where $\le$ denotes pointwise inequality.
Then:
:$\ds \int f \rd \mu \le \int g \rd \mu$
where the integral sign denotes $\mu$-integration.
This can be summarized by saying that $\ds \int \cdot \rd \mu$ is monotone.

Proof:
By the definition of $\mu$-integration, we have: 
:$\ds \int f \rd \mu = \sup \set {\map {I_\mu} h: h \le f, h \in \EE^+}$
and:
:$\ds \int g \rd \mu = \sup \set {\map {I_\mu} h : h \le g, h \in \EE^+}$
where:
:$\EE^+$ denotes the space of positive simple functions
:$\map {I_\mu} g$ denotes the $\mu$-integral of the positive simple function $g$.
Since $f \le g$:
:if $h \in \EE^+$ satisfies $h \le f$ then it satisfies $h \le g$.
So:
:$\set {\map {I_\mu} h: h \le f, h \in \EE^+} \subseteq \set {\map {I_\mu} h : h \le g, h \in \EE^+}$
From Supremum of Subset, we therefore have: 
:$\sup \set {\map {I_\mu} h: h \le f, h \in \EE^+} \le \sup \set {\map {I_\mu} h : h \le g, h \in \EE^+}$
That is: 
:$\ds \int f \rd \mu \le \int g \rd \mu$
{{qed}}
Theorem: Matrix Multiplication is Homogeneous of Degree 1

Let $\mathbf A$ be an $m \times n$ matrix and $\mathbf B$ be an $n \times p$ matrix.
Let $\lambda$ be a scalar in a field $\mathbb F$.
Then, the multiplication of these matrices is homogenous of degree one:
:$\mathbf A \paren {\lambda \mathbf B} = \lambda \paren {\mathbf A \mathbf B}$

Proof:
Let $\mathbf A = \sqbrk a_{m n}, \mathbf B = \sqbrk b_{n p}$.
Let $i \in \closedint 1 m$.
Let $j \in \closedint 1 p$.
{{begin-eqn}}
{{eqn | l = \left[ \lambda \mathbf A \mathbf B \right]_{i j}
      | r = \lambda \sum_{k \mathop = 1}^n a_{i k} b_{k j}
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n a_{i k} \paren {\lambda b_{k j} }
}}
{{eqn | r = \left[ \mathbf A \paren {\lambda \mathbf B} \right]_{i j}
      | c = {{Defof|Matrix Product (Conventional)}} and {{Defof|Matrix Scalar Product}}
}}
{{end-eqn}}
{{qed}}
Category:Conventional Matrix Multiplication
jobfixadxesetswvbkbkmqe07ppk7wn
Theorem: Integral of Series of Positive Measurable Functions

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\sequence {f_n}_{n \mathop \in \N} \in \MM_{\overline \R}^+$, $f_n: X \to \overline \R$ be a sequence of positive measurable functions.
Let $\ds \sum_{n \mathop \in \N} f_n: X \to \overline \R$ be the pointwise series of the $f_n$.
Then:
:$\ds \int \sum_{n \mathop \in \N} f_n \rd \mu = \sum_{n \mathop \in \N} \int f_n \rd \mu$
where the integral sign denotes $\mu$-integration.

Proof:
Define the sequence $\sequence {g_N}_{n \mathop \in \N}$ of functions $g_N : X \to \overline \R$ by: 
:$\ds \map {g_N} x = \sum_{n \mathop = 1}^N \map {f_n} x$ 
Since $f_n \ge 0$ for each $n$, we have: 
{{begin-eqn}}
{{eqn	| l = \map {g_{N + 1} } x
		| r = \sum_{n \mathop = 1}^{N + 1} \map {f_n} x
}}
{{eqn	| r = \sum_{n \mathop = 1}^N \map {f_n} x + \map {f_{N + 1} } x
}}
{{eqn	| o = \ge
		| r = \sum_{n \mathop = 1}^N \map {f_n} x
}}
{{eqn	| r = \map {g_N} x
}}
{{end-eqn}}
So $\sequence {g_N}_{N \mathop \in \N}$ is increasing. 
From Pointwise Sum of Measurable Functions is Measurable: General Result, we have that: 
:$g_N$ is $\Sigma$-measurable for each $N$. 
So, from the monotone convergence theorem, we have: 
:$\ds \lim_{N \mathop \to \infty} \int g_N \rd \mu = \int \paren {\lim_{N \mathop \to \infty} g_N} \rd \mu$
From the definition of infinite series, we have: 
:$\ds \lim_{N \mathop \to \infty} g_N = \sum_{n \mathop = 1}^\infty f_n$ 
So, we have: 
:$\ds \lim_{N \mathop \to \infty} \int g_N \rd \mu = \int \paren {\sum_{n \mathop = 1}^\infty f_n} \rd \mu$ 
Manipulating the {{LHS}}, we have: 
{{begin-eqn}}
{{eqn	| l = \lim_{N \mathop \to \infty} \int g_N \rd \mu
		| r = \lim_{N \mathop \to \infty} \int \paren {\sum_{n \mathop = 1}^N f_n} \rd \mu
}}
{{eqn	| r = \lim_{N \mathop \to \infty} \sum_{n \mathop = 1}^N \paren {\int f_n \rd \mu}
		| c = Integral of Positive Measurable Function is Additive
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \paren {\int f_n \rd \mu}
		| c = {{Defof|Real Series}}
}}
{{end-eqn}}
So:
:$\ds \sum_{n \mathop = 1}^\infty \paren {\int f_n \rd \mu} = \int \paren {\sum_{n \mathop = 1}^\infty f_n} \rd \mu$
{{qed}}
Theorem: Integral with respect to Dirac Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $x \in X$, and let $\delta_x$ be the Dirac measure at $x$.
Let $f \in \MM _{\overline \R}, f: X \to \overline \R$ be a measurable function.
Then:
:$\ds \int f \rd \delta_x = \map f x$
where the integral sign denotes the $\delta_x$-integral.

Proof:
Define the constant function $g : X \to \overline \R$ by: 
:$\map g {x'} = \map f x$
for each $x' \in X$. 
From Constant Function is Measurable, we have: 
:$g$ is $\Sigma$-measurable. 
From Measurable Functions Determine Measurable Sets:
:$\set {x' \in X : \map g {x'} \ne \map f {x'} } \in \Sigma$
Further: 
:$x \not \in \set {x' \in X : \map g {x'} \ne \map f {x'} }$
So from the definition of the Dirac measure, we have:
:$\map {\delta_x} {\set {x' \in X : \map g {x'} \ne \map f {x'} } } = 0$
So:
:$g = f$ $\delta_x$-almost everywhere.
From A.E. Equal Positive Measurable Functions have Equal Integrals: Corollary 1, we have: 
:$\ds \int g \rd \delta_x = \int f \rd \delta_x$ 
We finally have:
{{begin-eqn}}
{{eqn	| l = \int g \rd \delta_x
		| r = \map f x \int \chi_X \rd \delta_x
		| c = Integral of Integrable Function is Homogeneous
}}
{{eqn	| r = \map f x \map {\delta_x} X
		| c = Integral of Characteristic Function: Corollary
}}
{{eqn	| r = \map f x
}}
{{end-eqn}}
{{qed}}
Theorem: Integral with respect to Dirac Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $x \in X$, and let $\delta_x$ be the Dirac measure at $x$.
Let $f \in \MM _{\overline \R}, f: X \to \overline \R$ be a measurable function.
Then:
:$\ds \int f \rd \delta_x = \map f x$
where the integral sign denotes the $\delta_x$-integral.

Proof:
We first prove the result for positive simple functions.
Let $g : X \to \R$ be a positive simple function.
From Simple Function has Standard Representation, there exists:
:a finite sequence $a_1, \ldots, a_n$ of real numbers
:a partition $E_0, E_1, \ldots, E_n$ of $X$ into $\Sigma$-measurable sets
such that: 
:$\ds g = \sum_{i \mathop = 0}^n a_i \chi_{E_i}$
Then, from the definition of the $\delta_x$-integral of a positive simple function:
:$\ds \int g \rd \delta_x = \sum_{i \mathop = 1}^n a_i \map {\delta_x} {E_i}$
Since $E_0, E_1, \ldots, E_n$ is a partition of $X$, precisely one contains $x$. 
That is, $x \in E_i$ for precisely one $i$. 
Then:
:$\map {\delta_x} {E_j} = 0$ for $i \ne j$
leaving:
:$\ds \int g \rd \delta_x = a_i$
Note that: 
:$\ds \map g x = \sum_{j \mathop = 0}^n a_j \map {\chi_{E_j} } x$
and $\map {\chi_{E_j} } x = 1$ {{iff}} $j = i$, so we have: 
:$\map g x = a_i$
So we have: 
:$\ds \int g \rd \delta_x = \map g x$ 
for positive simple functions $g$.
Now consider a positive $\Sigma$-measurable function $f : X \to \overline \R_{\ge 0}$. 
From Measurable Function is Pointwise Limit of Simple Functions, there exists an increasing sequence $\sequence {f_n}_{n \mathop \in \N}$ of positive simple functions such that: 
:$\ds \map f x = \lim_{n \mathop \to \infty} \map {f_n} x$
for each $x \in X$.
For each $n \in \N$, we have: 
:$\ds \int f_n \rd \delta_x = \map {f_n} x$
from our previous work. 
From the Integral of Positive Measurable Function as Limit of Integrals of Positive Simple Functions, we have: 
:$\ds \int f \rd \delta_x = \lim_{n \mathop \to \infty} \int f_n \rd \delta_x$
That is: 
:$\ds \int f \rd \delta_x = \lim_{n \mathop \to \infty} \map {f_n} x = \map f x$
Now consider an arbitrary $\Sigma$-measurable function $f : X \to \overline \R$. 
From Function Measurable iff Positive and Negative Parts Measurable, we have: 
:$f^+$ and $f^-$ are $\Sigma$-measurable.
Now, if $\map f x \ge 0$, we have:
:$\map {f^+} x = \map f x$
and:
:$\map {f^-} x = 0$
So:
:$\ds \int f^+ \rd \delta_x = \map f x$
and:
:$\ds \int f^- \rd \delta_x = 0$
giving:
{{begin-eqn}}
{{eqn | l = \int f \rd \delta_x 
      | r = \int f^+ \rd \delta_x - \int f^- \rd \delta_x
      | c = {{Defof|Integral of Measure-Integrable Function}}
}}
{{eqn | r = \map f x - 0
}}
{{eqn | r = \map f x
}}
{{end-eqn}}
If $\map f x < 0$, then we have: 
:$\map {f^+} x = 0$
and:
:$\map {f^-} x = -\map f x$
so that: 
:$\ds \int f^+ \rd \delta_x = 0$
and:
:$\ds \int f^- \rd \delta_x = -\map f x$
Then we have:
{{begin-eqn}}
{{eqn | l = \int f \rd \delta_x 
      | r = \int f^+ \rd \delta_x - \int f^- \rd \delta_x
      | c = {{Defof|Integral of Measure-Integrable Function}}
}}
{{eqn | r = 0 - \paren {-\map f x}
}}
{{eqn | r = \map f x
}}
{{end-eqn}}
Hence the demand.
{{qed}}
Theorem: Integral with respect to Discrete Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $X$. 
Let $\ds \mu = \sum_{n \mathop \in \N} \lambda_n \delta_{x_n}$ be a discrete measure on $\struct {X, \Sigma}$.
Let $f \in \MM_{\overline \R}^+, f: X \to \overline \R$ be a positive measurable function.
Then:
:$\ds \int f \rd \mu = \sum_{n \mathop \in \N} \lambda_n \map f {x_n}$
where the integral sign denotes $\mu$-integration.

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \int f \rd \mu
		| r = \sum_{n \mathop \in \N} \lambda_n \int f \rd \delta_{x_n}
		| c = Integral with respect to Series of Measures
}}
{{eqn	| r = \sum_{n \mathop \in \N} \lambda_n \map f {x_n}
		| c = Integral with respect to Dirac Measure
}}
{{end-eqn}}
{{qed}}
Theorem: Matrix Product as Linear Transformation

Let:
{{begin-eqn}}
{{eqn | l = \mathbf A_{m \times n}
      | r = \begin {bmatrix} a_{11} & a_{12} & \cdots & a_{1n} \\ a_{21} & a_{22} & \cdots & a_{2n} \\ \vdots & \vdots & \ddots & \vdots \\ a_{m1} & a_{m2} & \cdots & a_{mn} \\ \end {bmatrix}
}}
{{eqn | l = \mathbf x_{n \times 1}
      | r = \begin {bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end {bmatrix}
}}
{{eqn | l = \mathbf y_{n \times 1}
      | r = \begin {bmatrix} y_1 \\ y_2 \\ \vdots \\ y_n \end {bmatrix}
}}
{{end-eqn}}
be matrices where each column is an element of a real vector space.
Let $T$ be the mapping:
:$T: \R^m \to \R^n, \mathbf x \mapsto \mathbf A \mathbf x$
Then $T$ is a linear transformation.

Proof:
From Matrix Multiplication is Homogeneous of Degree $1$:
:$\forall \lambda \in \mathbb F \in \set {\R, \C}: \mathbf A \paren {\lambda \mathbf x} = \lambda \paren {\mathbf A \mathbf x}$
From Matrix Multiplication Distributes over Matrix Addition:
:$\forall \mathbf x, \mathbf y \in \R^m: \mathbf A \paren {\mathbf x + \mathbf y} = \mathbf A \mathbf x + \mathbf A \mathbf y$
Hence the result, from the definition of linear transformation.
{{qed}}
Theorem: Linear Transformation Maps Zero Vector to Zero Vector

Let $\mathbf V$ be a vector space, with zero $\mathbf 0$.
Likewise let $\mathbf V\,'$ be another vector space, with zero $\mathbf 0'$.
Let $T: \mathbf V \to \mathbf V\,'$ be a linear transformation.
Then:
:$T: \mathbf 0 \mapsto \mathbf 0'$

Proof:
From the vector space axioms we have that $\exists \mathbf 0 \in \mathbf V$.
It remains to be proved that $\map T {\mathbf 0} = \mathbf 0'$:
{{begin-eqn}}
{{eqn | l = \map T {\mathbf 0}
      | r = \map T {\mathbf 0 + \mathbf 0}
}}
{{eqn | r = \map T {\mathbf 0} + \map T {\mathbf 0}
      | c = {{Defof|Linear Transformation on Vector Space}}
}}
{{eqn | ll= \leadsto
      | l = \mathbf 0'
      | r = \map T {\mathbf 0}
      | c = subtracting $\map T {\mathbf 0}$ from both sides
}}
{{end-eqn}}
{{qed}}
Theorem: Linear Transformation Maps Zero Vector to Zero Vector

Let $\mathbf V$ be a vector space, with zero $\mathbf 0$.
Likewise let $\mathbf V\,'$ be another vector space, with zero $\mathbf 0'$.
Let $T: \mathbf V \to \mathbf V\,'$ be a linear transformation.
Then:
:$T: \mathbf 0 \mapsto \mathbf 0'$

Proof:
From the vector space axioms we have that $\exists \mathbf 0 \in \mathbf V$.
What remains is to prove that $\map T {\mathbf 0} = \mathbf 0'$:
{{begin-eqn}}
{{eqn | l = \map T {\mathbf 0}
      | r = \map T {0 \, \mathbf 0}
      | c = Zero Vector Scaled is Zero Vector
}}
{{eqn | r = 0 \, \map T {\mathbf 0}
      | c = {{Defof|Linear Transformation on Vector Space}}
}}
{{eqn | r = \mathbf 0'
      | c = Vector Scaled by Zero is Zero Vector
}}
{{end-eqn}}
{{qed}}
Theorem: Infimum of Subset Product in Ordered Group

Let $\struct {G, \circ, \preceq}$ be an ordered group.
Let subsets $A$ and $B$ of $G$ admit infima in $G$.
Then:
:$\map \inf {A \circ_\PP B} = \inf A \circ \inf B$
where $\circ_\PP$ denotes subset product.

Proof:
This follows from Supremum of Subset Product in Ordered Group and the Duality Principle.
{{qed}}