avewright/proofwiki-math huggingface dataset:
Theorem: Equivalence of Definitions of P-adic Integer/Definition 2 Implies Definition 1

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the valued field of $p$-adic numbers for some prime $p$. 
That is, such that:
:$\Q_p$ is the field of $p$-adic numbers
:$\norm {\,\cdot\,}_p$ is the $p$-adic norm on $\Q_p$.
Let $x \in \Q_p$ such that the canonical expansion of $x$ contains only positive powers of $p$.
Then:
:$\norm x_p \le 1$

Proof:
Let the canonical expansion of $x$ contain only positive powers of $p$.
That is:
:$x = \ds \sum_{n \mathop = 0}^\infty d_n p^n : \forall n \in \N : 0 \le d_n < p$
==== Case 1 : $\forall n \in \N : d_n = 0$ ====
Let: 
:$\forall n \in \N : d_n = 0$
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = \sum_{n \mathop = 0}^\infty 0 * p^n
      | c = {{Defof|Canonical P-adic Expansion}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty 0
}}
{{eqn | r = 0
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \norm x_p 
      | r = \norm 0_p
}}
{{eqn | r = 0
}}
{{eqn | o = < 
      | r = 1
}}
{{end-eqn}}
{{qed|lemma}}
==== Case 2 : $\exists n \in \N : d_n > 0$ ====
Let:
:$\exists n \in \N : d_n > 0$
Let:
:$l = \min \set {i: i \ge 0 \land d_i \ne 0}$
Hence:
:$l \ge 0$
Thus:
{{begin-eqn}}
{{eqn | l = \norm x_p 
      | r = p^{-l}
      | c = P-adic Norm of P-adic Expansion is determined by First Nonzero Coefficient
}}
{{eqn | o = \le 
      | r = p^0
}}
{{eqn | r = 1
}}
{{end-eqn}}
Theorem: Sequence of P-adic Integers has Convergent Subsequence

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $\sequence{x_n}$ be a sequence of $p$-adic integers.
Then:
:there exists a convergent subsequence $\sequence {x_{n_r} }_{r \mathop \in \N}$ of $\sequence{x_n}$

Proof:
=== Lemma 1 ===
{{:Sequence of P-adic Integers has Convergent Subsequence/Lemma 1}}{{qed|lemma}}
=== Lemma 2 ===
{{:Sequence of P-adic Integers has Convergent Subsequence/Lemma 2}}{{qed|lemma}}
=== Lemma 3 ===
{{:Sequence of P-adic Integers has Convergent Subsequence/Lemma 3}}{{qed|lemma}}
=== Lemma 4 ===
{{:Sequence of P-adic Integers has Convergent Subsequence/Lemma 4}}{{qed|lemma}}
From P-adic Expansion Converges to P-adic Number:
:$\ds \sum_{n \mathop = 0}^\infty b_n p^n$ converges to some $x \in \Q_p$
By definition of $p$-adic integer:
:$x \in \Z_p$
=== Lemma 5 ===
{{:Sequence of P-adic Integers has Convergent Subsequence/Lemma 5}}{{qed}}
Theorem: Sequence of P-adic Integers has Convergent Subsequence

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $\sequence{x_n}$ be a sequence of $p$-adic integers.
Then:
:there exists a convergent subsequence $\sequence {x_{n_r} }_{r \mathop \in \N}$ of $\sequence{x_n}$

Proof:
From P-adic Integers are Compact Subspace:
:$\Z_p$ is a compact subspace in the metric space induced by $\norm{\,\cdot\,}_p$
From Compact Subspace of Metric Space is Sequentially Compact in Itself:
:$\Z_p$ is sequentially compact in itself
By definition of sequentially compact in itself:
:every sequence in $\Z_p$ has a subsequence which converges in the topology to a point in $\Z_p$
From Equivalence of Definitions of Convergence in Normed Division Rings:
:every sequence in $\Z_p$ has a subsequence which converges in the norm to a point in $\Z_p$
{{qed}}
Theorem: P-adic Integers is Valuation Ring Induced by P-adic Norm/Corollary

{{begin-itemize}}
{{item|(a):|the $p$-adic integers, $\Z_p$, is a local ring}}
{{item|(b):|the principal ideal $p\Z_p$ is the unique maximal ideal of $\Z_p$}}
{{end-itemize}}

Proof:
From $p$-adic Integers is Valuation Ring Induced by $p$-adic Norm:
:$\Z_p$ is the valuation ring induced by the non-Archimedean norm $\norm {\,\cdot\,}_p$
From Valuation Ideal of $p$-adic Numbers:
:$p \Z_p$ is the valuation ideal induced by the non-Archimedean norm $\norm {\,\cdot\,}_p$
From {{Corollary|Valuation Ideal is Maximal Ideal of Induced Valuation Ring|1}}:
{{begin-itemize}}
{{item|(a):|$\Z_p$ is a local ring}}
{{item|(b):|$\Z_p$ is the unique maximal ideal of $\Z_p$}}
{{end-itemize}}
{{qed}}
Theorem: Equations defining Plane Reflection/Cartesian

Let $\LL$ be a straight line through the origin $O$ of a cartesian plane.
Let the angle between $\LL$ and the $x$-axis be $\alpha$.
Let $\phi_\alpha$ denote the reflection in the plane whose axis is $\LL$.
Let $P = \tuple {x, y}$ be an arbitrary point in the plane.
Then:
:$\map {\phi_\alpha} P = \tuple {x \cos 2 \alpha + y \sin 2 \alpha, x \sin 2 \alpha - y \cos 2 \alpha}$

Proof:
:420px
Let $\LL$ reflect $P = \tuple {x, y}$ onto $P' = \tuple {x', y'}$.
Let $OP$ form an angle $\theta$ with the $x$-axis.
We have:
:$OP = OP'$
Thus:
{{begin-eqn}}
{{eqn | l = x
      | r = OP \cos \theta
}}
{{eqn | l = y
      | r = OP \sin \theta
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = x'
      | r = OP \map \cos {\theta + 2 \paren {\alpha - \theta} }
      | c = from the geometry
}}
{{eqn | r = OP \map \cos {2 \alpha - \theta}
      | c = simplifying
}}
{{eqn | r = OP \paren {\cos 2 \alpha \cos \theta + \sin 2 \alpha \sin \theta}
      | c = Cosine of Difference
}}
{{eqn | r = OP \cos \theta \cos 2 \alpha + OP \sin \theta \sin 2 \alpha
      | c = factoring
}}
{{eqn | r = x \cos 2 \alpha + y \sin 2 \alpha
      | c = substituting $x$ and $y$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = y'
      | r = OP \map \sin {\theta + 2 \paren {\alpha - \theta} }
      | c = from the geometry
}}
{{eqn | r = OP \map \sin {2 \alpha - \theta}
      | c = simplifying
}}
{{eqn | r = OP \paren {\sin 2 \alpha \cos \theta - \cos 2 \alpha \sin \theta}
      | c = Sine of Difference
}}
{{eqn | r = OP \cos \theta \sin 2 \alpha - OP \sin \theta \cos 2 \alpha
      | c = factoring
}}
{{eqn | r = x \sin 2 \alpha - y \cos 2 \alpha
      | c = substituting $x$ and $y$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Sequence of P-adic Integers has Convergent Subsequence/Lemma 3

:there exists a sequence $\sequence{b_n}$ of $p$-adic digits:
::for all $j \in \N$, there exists infinitely many $n \in \N$ such that the canonical expansion of $x_n$ begins with the $p$-adic digits $b_j \, \ldots \, b_1 b_0$

Proof:
=== Lemma 1 ===
{{:Sequence of P-adic Integers has Convergent Subsequence/Lemma 1}}{{qed|lemma}}
Theorem: Sequence of P-adic Integers has Convergent Subsequence/Lemma 4

:there exists a subsequence $\sequence{x_{n_j}}_{j \mathop \in \N}$ of $\sequence{x_n}$:
::for all $j \in \N$, the canonical expansion of $x_{n_j}$ begins with the $p$-adic digits $b_j \, \ldots \, b_1 b_0$

Proof:
The proof proceeds using the principle of recursive definition.
For any non-empty subset $S$ of $\N$, let $\min S$ denote the smallest element of $S$.
From the Well-Ordering Principle, for any non-empty subset $S$ of $\N$, $\min S$ always exists.
Let $T = \N \times \N$.
Let $n_0 = \min \set{n \in \N : \text{ the canonical expansion  of } x_n \text{ begins with the } p \text{-adic digits } b_0}$
By hypothesis and Well-Ordering Principle:
:$n_0$ exists
By definition of smallest element:
:the canonical expansion of $x_{n_0}$ begins with the $p$-adic digit $b_0$
Let $a = \tuple{0, n_0} \in T$.
Let $h: T \to \N$ be the mapping defined by:
:$\map h {j, k} = \min \set{n > k : \text{ the canonical expansion  of } x_n \text{ begins with the } p \text{-adic digits } b_{j+1}, b_j, \ldots, b_0}$
By hypothesis and Well-Ordering Principle:
:$h$ is well-defined
By definition of smallest element:
:the canonical expansion of $x_{\map h {j, k} }$ begins with the $p$-adic digit $b_{j+1} b_j \ldots b_1 b_0$
Let $g: T \to T$  be the mapping defined by:
:$\map g {j, k} = \tuple {j+1, \map h {j, k} }$
From principle of recursive definition:
:there exists exactly one mapping $f: \N \to T$ such that:
::$\forall j \in \N: \map f j = \begin{cases}
a & : j = 0 \\
\map g {\map f n} & : j = n + 1
\end{cases}$
That is:
:there exists exactly one mapping $f: \N \to T$ such that:
::$\forall j \in \N: \map f j = \begin{cases}
\tuple{0, n_0} & : j = 0 \\
\tuple {j, \map h {n, \map  f n} } & : j = n + 1
\end{cases}$
{{qed}}
category:Sequence of P-adic Integers has Convergent Subsequence
f0rz07tybmposkagnhprmf77mmy1tgx
Theorem: Sequence of P-adic Integers has Convergent Subsequence/Lemma 5

:the subsequence $\sequence{x_{n_j}}_{j \mathop \in \N}$ converges to $x \in \Z_p$

Proof:
By definition of the canonical expansion $\ldots \, b_n \, \ldots \, b_1 b_0$ converges to $x$:
:the sequence of partial sums $\ds \sum_{n \mathop = 0}^j b_n p^n$ converges to $x$
Let $\sequence{y_j}$ be the sequence of partial sums:
:$y_j = \ds \sum_{n \mathop = m}^j b_n p^n$
From Null Sequence Test for Convergence, it is sufficient to show that:
:$\sequence{x_{n_j} - y_j}$ is a null sequence
For all $j \in \N$, we have:
{{begin-eqn}}
{{eqn | l = x_{n_j} - y_j
      | r = \sum_{n \mathop = 0}^\infty a^{\paren j}_n p^n - \sum_{n \mathop = 0}^j b_n p^n
}}
{{eqn | r = \sum_{n \mathop = 0}^j \paren{a^{\paren j}_n - b_n} p^n + \sum_{n \mathop = j + 1}^\infty a^{\paren j}_n p^n
}}
{{eqn | r = \sum_{n \mathop = 0}^j 0 \cdot p^n + \sum_{n \mathop = j + 1}^\infty a^{\paren j}_n p^n
}}
{{end-eqn}}
From P-adic Norm of P-adic Expansion is determined by First Nonzero Coefficient:
:$\norm{x_{n_j} - y_j}_p \le \dfrac 1 {p^{j + 1} } < \dfrac 1 {p^j}$
From Sequence of Powers of Number less than One
:$\ds \lim_{j \mathop \to \infty} \dfrac 1 {p^j} = 0$
From Squeeze Theorem for Real Sequences:
:$\ds \lim_{j \mathop \to \infty} \norm{x_{n_j} - y_j}_p = 0$
By definition of convergence:
:$\sequence{x_{n_j} - y_j}$ converges to $0$
It follows that $\sequence{x_{n_j} - y_j}$ is a null sequence by definition.
{{qed}}
category:Sequence of P-adic Integers has Convergent Subsequence
gl6temg5zi697qju8p5i280vrfliqgv
Theorem: Sequence of P-adic Integers has Convergent Subsequence/Lemma 2

Let $\sequence{b_0, b_1, \ldots, b_j}$ be a finite sequence of $p$-adic digits such that:
:there exists infinitely many $n \in \N$ such that the canonical expansion of $x_n$ begins with the $p$-adic digits $b_j \, \ldots \, b_1 b_0$
Then there exists a $p$-adic digit $b_{j + 1}$ such that:
:there exists infinitely many $n \in \N$ such that the canonical expansion of $x_n$ begins with the $p$-adic digits $b_{j+1}b_j \, \ldots \, b_1 b_0$

Proof:
=== Lemma ===
{{:Sequence of P-adic Integers has Convergent Subsequence/Lemma 6}}{{qed|lemma}}
Theorem: Absolute Value of Measurable Function is Measurable

Let $\struct {X, \Sigma}$ be a measurable space. 
Let $f : X \to \overline \R$ be a $\Sigma$-measurable function.
Then: 
:$\size f$ is a $\Sigma$-measurable function.

Proof:
From Characterization of Measurable Functions, it suffices to show that for each real number $t \in \R$, we have: 
:$\set {x \in X : \size {\map f x} \le t} \in \Sigma$
If $t < 0$, we have: 
:$\set {x \in X : \size {\map f x} \le t} = \O$
So, from Properties of Algebras of Sets, we have: 
:$\set {x \in X : \size {\map f x} \le t} \in \Sigma$
if $t < 0$. 
If $t \ge 0$, we can write: 
{{begin-eqn}}
{{eqn | l = \set {x \in X : \size {\map f x} \le t}
	  | r = \set {x \in X : -t \le \map f x \le t}
}}
{{eqn | r = \set {x \in X : -t \le \map f x} \cap \set {x \in X : \map f x \le t}
}}
{{end-eqn}}
Since $f$ is $\Sigma$-measurable, we have that both: 
:$\set {x \in X : -t \le \map f x} \in \Sigma$
and:
:$\set {x \in X : \map f x \le t} \in \Sigma$
from Characterization of Measurable Functions.
From Properties of Algebras of Sets, the intersection of any two sets in $\Sigma$ is contained in $\Sigma$. 
So:
:$\set {x \in X : -t \le \map f x} \cap \set {x \in X : \map f x \le t} \in \Sigma$ 
if $t \ge 0$. 
That is: 
:$\set {x \in X : \size {\map f x} \le t} \in \Sigma$
if $t \ge 0$.
So:
:$\set {x \in X : \size {\map f x} \le t} \in \Sigma$
for all $t \in \R$.
{{qed}}
Category:Measurable Functions
dckrwwvw1f72e6b48ctejz6fio0fijz
Theorem: Pointwise Maximum of Simple Functions is Simple

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g : X \to \R$ be simple functions. 
Then the pointwise maximum $\max \set {f, g}: X \to \R$ is also simple function.

Proof:
From Pointwise Sum of Simple Functions is Simple Function:
:$f + g$ is simple.
From Scalar Multiple of Simple Function is Simple Function:
:$-g$ is simple.
Then, from Pointwise Sum of Simple Functions is Simple Function, we have: 
:$f - g$ is simple.
From Absolute Value of Simple Function is Simple Function:
:$\size {f - g}$ is simple.
From Pointwise Sum of Simple Functions is Simple Function, we then have: 
:$\paren {f + g} + \size {f - g}$ is simple. 
Finally, from Scalar Multiple of Simple Function is Simple Function, we have: 
:$\dfrac 1 2 \paren {\paren {f + g} + \size {f - g} }$ is simple.
By Maximum Function in terms of Absolute Value, we have: 
:$\ds \max \set {f, g} = \frac 1 2 \paren {\paren {f + g} + \size {f - g} }$
so:
:$\max \set {f, g}$ is simple.
{{qed}}
Theorem: Pointwise Maximum of Simple Functions is Simple

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g : X \to \R$ be simple functions. 
Then the pointwise maximum $\max \set {f, g}: X \to \R$ is also simple function.

Proof:
From Simple Function is Measurable, we have that: 
:$f$ and $g$ are $\Sigma$-measurable.
For brevity let:
:$h = \max \set {f, g}$
From Pointwise Maximum of Measurable Functions is Measurable, we have that: 
:$h$ is $\Sigma$-measurable.
From Measurable Function is Simple Function iff Finite Image Set, we aim to show that: 
:$\map h X$ is a finite set. 
From Measurable Function is Simple Function iff Finite Image Set, we have: 
:$\map f X$ and $\map g X$ are finite sets.
Let $x \in X$. 
If $\map f x < \map g x$, then: 
:$\map h x = \map g x$
so that: 
:$\map h x \in \map g X$
If $\map g x \le \map f x$, then: 
:$\map h x = \map f x$
so that: 
:$\map h x \in \map f X$
Since for $x \in X$ we have either $\map g x \le \map f x$ or $\map f x < \map g x$, we obtain:
:$\map h X \subseteq \map f X \cup \map g X$
From Union of Finite Sets is Finite, we have that: 
:$\map f X \cup \map g X$ is finite.
Then, from Subset of Finite Set is Finite: 
:$\map h X$ is finite.
So:
:$h$ is simple.
{{qed}}
Theorem: Equations defining Plane Reflection/Examples/X-Axis

Let $\phi_x$ denote the reflection in the plane whose axis is the $x$-axis.
Let $P = \tuple {x, y}$ be an arbitrary point in the plane
Then:
:$\map {\phi_x} P = \tuple {x, -y}$

Proof:
From Equations defining Plane Reflection:
:$\map {\phi_\alpha} P = \tuple {x \cos 2 \alpha + y \sin 2 \alpha, x \sin 2 \alpha - y \cos 2 \alpha}$
where $\alpha$ denotes the angle between the axis and the $x$-axis.
By definition, the $x$-axis, being coincident with itself, is at a zero angle with itself.
Hence $\phi_x$ can be expressed as $\phi_\alpha$ in the above equations such that $\alpha = 0$.
Hence we have:
{{begin-eqn}}
{{eqn | l = \map {\phi_x} P
      | r = \tuple {x \map \cos {2 \times 0} + y \map \sin {2 \times 0}, x \map \sin {2 \times 0} - y \map \cos {2 \times 0} }
      | c = 
}}
{{eqn | r = \tuple {x \cos 0 + y \sin 0, x \sin 0 - y \cos 0}
      | c = 
}}
{{eqn | r = \tuple {x, -y}
      | c = Cosine of Zero is One, Sine of Zero is Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Equations defining Plane Reflection/Examples/Y-Axis

Let $\phi_y$ denote the reflection in the plane whose axis is the $y$-axis.
Let $P = \tuple {x, y}$ be an arbitrary point in the plane
Then:
:$\map {\phi_y} P = \tuple {-x, y}$

Proof:
From Equations defining Plane Reflection:
:$\map {\phi_\alpha} P = \tuple {x \cos 2 \alpha + y \sin 2 \alpha, x \sin 2 \alpha - y \cos 2 \alpha}$
where $\alpha$ denotes the angle between the axis and the $x$-axis.
By definition, the $y$-axis, is perpendicular to the $x$-axis
Hence $\phi_y$ can be expressed as $\phi_\alpha$ in the above equations such that $\alpha = \dfrac \pi 2$ radians.
Hence we have:
{{begin-eqn}}
{{eqn | l = \map {\phi_x} P
      | r = \tuple {x \map \cos {2 \dfrac \pi 2} + y \map \sin {2 \dfrac \pi 2}, x \map \sin {2 \dfrac \pi 2} - y \map \cos {2 \dfrac \pi 2} }
      | c = 
}}
{{eqn | r = \tuple {x \cos \pi + y \sin \pi, x \sin \pi - y \cos \pi}
      | c = 
}}
{{eqn | r = \tuple {-x, y}
      | c = Cosine of Straight Angle, Sine of Straight Angle
}}
{{end-eqn}}
{{qed}}
Theorem: Plane Reflection is Space Rotation

Let $M$ be a straight line in the plane passing through the origin.
Let $s_M$ be the '''reflection''' of $\R^2$ in $M$.
Then $s_M$ is the rotation of the plane in space through one half turn about $M$ as an axis.

Proof:
{{ProofWanted|Needs equations of space rotation}}
Theorem: Plane Reflection is Involution

Let $M$ be a straight line in the plane passing through the origin.
Let $s_M$ be the '''reflection''' of $\R^2$ in $M$.
Then $s_M$ is an involution in the sense that:
:$s_M \circ s_M = I_{\R^2}$
where $I_{\R^2}$ is the identity mapping on $\R_2$.
That is:
:$s_M = {s_M}^{-1}$

Proof:
Let the angle between $M$ and the $x$-axis be $\alpha$.
Let $P = \tuple {x, y}$ be an arbitrary point in the plane.
Then from Equations defining Plane Reflection:
:$\map {s_M} P = \tuple {x \cos 2 \alpha + y \sin 2 \alpha, x \sin 2 \alpha - y \cos 2 \alpha}$
Thus:
{{begin-eqn}}
{{eqn | l = \map {s_M \circ s_M} P
      | r = \map {s_M} {\map {s_M} P}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map {s_M} {\tuple {x \cos 2 \alpha + y \sin 2 \alpha, x \sin 2 \alpha - y \cos 2 \alpha} }
      | c = 
}}
{{eqn | r = {\tuple {\paren {x \cos 2 \alpha + y \sin 2 \alpha} \cos 2 \alpha + \paren {x \sin 2 \alpha - y \cos 2 \alpha} \sin 2 \alpha, \paren {x \cos 2 \alpha + y \sin 2 \alpha} \sin 2 \alpha - \paren {x \sin 2 \alpha - y \cos 2 \alpha}  \cos 2 \alpha} }
      | c = 
}}
{{eqn | r = \tuple {x \cos^2 2 \alpha + y \sin 2 \alpha \cos 2 \alpha + x \sin^2 2 \alpha - y \sin 2 \alpha \cos 2 \alpha, x \sin 2 \alpha \cos 2 \alpha + y \sin^2 2 \alpha - x \sin 2 \alpha \cos 2 \alpha + y \cos^2 2 \alpha}
      | c = 
}}
{{eqn | r = \tuple {x \paren {\cos^2 2 + \sin^2 2 \alpha}, y \paren {\sin^2 2 \alpha + \cos^2 2 \alpha} }
      | c = simplifying
}}
{{eqn | r = \tuple {x, y}
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Equations defining Plane Rotation/Cartesian

Let $r_\alpha$ be the rotation of the plane about the origin through an angle of $\alpha$.
Let $P = \tuple {x, y}$ be an arbitrary point in the plane.
Then:
:$\map {r_\alpha} P = \tuple {x \cos \alpha - y \sin \alpha, x \sin \alpha + y \cos \alpha}$

Proof:
:420px
Let $r_\alpha$ rotate $P = \tuple {x, y}$ onto $P' = \tuple {x', y'}$.
Let $OP$ form an angle $\theta$ with the $x$-axis.
We have:
:$OP = OP'$
Thus:
{{begin-eqn}}
{{eqn | l = x
      | r = OP \cos \theta
}}
{{eqn | l = y
      | r = OP \sin \theta
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = x'
      | r = OP \map \cos {\alpha + \theta}
      | c = from the geometry
}}
{{eqn | r = OP \paren {\cos \alpha \cos \theta - \sin \alpha \sin \theta}
      | c = Cosine of Sum
}}
{{eqn | r = OP \cos \theta \cos \alpha - OP \sin \theta \sin \alpha
      | c = factoring
}}
{{eqn | r = x \cos \alpha - y \sin \alpha
      | c = substituting $x$ and $y$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = y'
      | r = OP \map \sin {\alpha + \theta}
      | c = from the geometry
}}
{{eqn | r = OP \paren {\sin \alpha \cos \theta + \cos \alpha \sin \theta}
      | c = Sine of Difference
}}
{{eqn | r = OP \cos \theta \sin \alpha + OP \sin \theta \cos \alpha
      | c = factoring
}}
{{eqn | r = x \sin \alpha + y \cos \alpha
      | c = substituting $x$ and $y$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Triangle Inequality for Integrals/Corollary

Let $f: X \to \overline \R$ be a $\mu$-integrable function be such that: 
:$\ds \int \size f \rd \mu = 0$
Then: 
:$\ds \int f \rd \mu = 0$

Proof:
From Triangle Inequality for Integrals, we have: 
:$\ds \size {\int f \rd \mu} \le \int \size f \rd \mu$
We have: 
:$\ds \int \size f \rd \mu = 0$
so:
:$\ds \size {\int f \rd \mu} \le 0$
That is: 
:$\ds \size {\int f \rd \mu} = 0$
so:
:$\ds \int f \rd \mu = 0$
{{qed}}
Category:Triangle Inequality for Integrals
97byyxdwv54jd3q085his6g1mo7zalp
Theorem: Integral of Integrable Function over Measurable Set is Well-Defined

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $E \in \Sigma$. 
Let $f: X \to \overline \R$ be a $\mu$-integrable function.
Then the $\mu$-integral of $f$ over $E$:
:$\ds \int_E f \rd \mu = \int f \cdot \chi_E \rd \mu$
is well-defined.

Proof:
We need to show that $f \cdot \chi_E$ is $\mu$-integrable, so that its $\mu$-integral is well-understood.
Since $f$ is $\mu$-integrable, it is certainly $\Sigma$-measurable.
From Characteristic Function Measurable iff Set Measurable, we have that: 
:$\chi_E$ is $\Sigma$-measurable.
Then by Pointwise Product of Measurable Functions is Measurable, we have: 
:$f \cdot \chi_E$ is $\Sigma$-measurable.
We now want to verify that: 
:$\ds \int \paren {f \cdot \chi_E}^+ \rd \mu < \infty$
and:
:$\ds \int \paren {f \cdot \chi_E}^- \rd \mu < \infty$
Note that from the definition of a characteristic function:
:$\map {\chi_E} x \in \set {0, 1}$
so, for $x \in X$:
:$\map {f \cdot \chi_E} x \ge 0$ {{iff}} $\map {\chi_E} x = 0$ or $\map {\chi_E} x = 1$ and $\map f x \ge 0$
and:
:$\map {f \cdot \chi_E} x \le 0$ {{iff}} $\map {\chi_E} x = 0$ or $\map {\chi_E} x = 1$ and $\map f x \le 0$
So, we have: 
:$\paren {f \cdot \chi_E}^+ = f^+ \cdot \chi_E$
and:
:$\paren {f \cdot \chi_E}^- = f^- \cdot \chi_E$
We can see that: 
:$f^+ \cdot \chi_E \le f^+$
and:
:$f^- \cdot \chi_E \le f^-$
Since $f$ is $\mu$-integrable, we have: 
:$\ds \int f^+ \rd \mu < \infty$
and:
:$\ds \int f^- \rd \mu < \infty$
Then, from Integral of Positive Measurable Function is Monotone, we have: 
:$\ds \int f^+ \cdot \chi_E \rd \mu \le \int f^+ \rd \mu < \infty$
and:
:$\ds \int f^- \cdot \chi_E \rd \mu \le \int f^- \rd \mu < \infty$
This gives:
:$\ds \int \paren {f \cdot \chi_E}^+ \rd \mu < \infty$
and:
:$\ds \int \paren {f \cdot \chi_E}^- \rd \mu < \infty$
as required.
{{qed}}
Category:Integrals of Measure-Integrable Functions
bh58chkcvbd4x94nv8b1xrckjc9da7c
Theorem: Integrable Function with Zero Integral on Sub-Sigma-Algebra is A.E. Zero

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\GG$ be a sub-$\sigma$-algebra of $\Sigma$.
Let $f : X \to \overline \R$ be a $\GG$-integrable function.
Suppose that, for all $G \in \GG$:
:$\ds \int_G f \rd \mu = 0$
Then $f = 0$ $\mu$-almost everywhere.

Proof:
In view of Measurable Function Zero A.E. iff Absolute Value has Zero Integral, we shall show:
:$\ds \int \size f \rd \mu = 0$
Since $f$ is $\GG$-measurable:
:$G_+ := \set {x \in X : \map f x > 0} \in \GG$
and:
:$G_- := \set {x \in X : \map f x \le 0} \in \GG$
On the one hand:
{{begin-eqn}}
{{eqn | l = \int f^+ \rd \mu
      | r = \int f \cdot \chi_{G_+} \rd \mu
      | c = $f^+$ is positive part of $f$
}}
{{eqn | r = \int_{G_+} f \rd \mu
}}
{{eqn | r = 0
      | c = {{hypothesis}}
}}
{{end-eqn}}
On the other hand, from $f \cdot \chi_{G_-} \le 0$ follows:
{{begin-eqn}}
{{eqn | l = \paren {f \cdot \chi_{G_-} }^+
      | r = 0
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \paren {f \cdot \chi_{G_-} }^-
      | r = -\paren {f \cdot \chi_{G_-} }
}}
{{eqn | r = \paren {-f} \cdot \chi_{G_-}
}}
{{eqn | r = f^-
      | c = $f^-$ is negative part of $f$
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \int_{G_-} f \rd \mu
      | r = \int f \cdot \chi_{G_-} \rd \mu
}}
{{eqn | r = \int \paren {f \cdot \chi_{G_-} }^+ \rd \mu - \int \paren {f \cdot \chi_{G_-} }^- \rd \mu
      | c = integral of $f \cdot \chi_{G_-}$
}}
{{eqn | r = -\int f^- \rd \mu
}}
{{end-eqn}}
which implies:
{{begin-eqn}}
{{eqn | l = \int f^- \rd \mu
      | r = -\int f \cdot \chi_{G_-} \rd \mu
}}
{{eqn | r = -\int_{G_-} f \rd \mu
}}
{{eqn | r = 0
      | c = {{hypothesis}}
}}
{{end-eqn}}
Therefore:
:$\ds \int \size f \rd \mu = \int f^+ \rd \mu + \int f^- \rd \mu = 0$
{{qed}}