avewright/proofwiki-math huggingface dataset:
Theorem: Rational Number can be Expressed as Simple Finite Continued Fraction

Let $q \in \Q$ be a rational number.
Then $q$ can be expressed as a simple finite continued fraction.

Proof:
Let $q = \dfrac a b$ be a rational number expressed in canonical form.
That is $b > 0$ and $a \perp b = 1$.
By the Euclidean Algorithm, we have:
{{begin-eqn}}
{{eqn | l = a
      | r = q_1 b + r_1,
      | rr= 0 < r_1 < b
      | c = or $\dfrac a b = q_1 + \dfrac {r_1} b$
}}
{{eqn | l = b
      | r = q_2 r_1 + r_2,
      | rr= 0 < r_2 < r_1
      | c = or $\dfrac b {r_1} = q_2 + \dfrac {r_2} {r_1}$
}}
{{eqn | l = r_1
      | r = q_3 r_2 + r_3,
      | rr= 0 < r_3 < r_2
      | c = or $\dfrac {r_2} {r_1} = q_3 + \dfrac {r_3} {r_2}$
}}
{{eqn | o = \vdots
}}
{{eqn | l = r_{n-3}
      | r = q_{n - 1} r_{n - 2} + r_{n - 1},
      | rr= 0 < r_{n - 1} < r_{n - 2}
      | c = or $\dfrac {r_{n - 3} } {r_{n - 2} } = q_{n - 1} + \dfrac {r_{n - 1} } {r_{n - 2} }$
}}
{{eqn | l = r_{n - 2}
      | r = q_n r_{n - 1} + 0,
      | c = or $\dfrac {r_{n - 2} } {r_{n - 1} } = q_n$
}}
{{end-eqn}}
Thus from the system of equations on the {{RHS}}, we get:
{{begin-eqn}}
{{eqn | l = \frac a b
      | r = q_1 + \cfrac 1 {\frac b {r_1} }
      | c =
}}
{{eqn | r = q_1 + \cfrac 1 {q_2 + \cfrac 1 {\frac {r_1} {r_2} } }
      | c =
}}
{{eqn | r = q_1 + \cfrac 1 {q_2 + \cfrac 1 {q_3 + \cfrac 1 {\frac {r_2} {r_3} } } }
      | c =
}}
{{eqn | o = \cdots
      | c =
}}
{{eqn | r = q_1 + \cfrac 1 {q_2 + \cfrac 1 {q_3 + \cfrac 1 {\ddots \cfrac {} {q_{n - 1} + \cfrac 1 {q_n} } } } }
      | c =
}}
{{end-eqn}}
This shows that $q$ has the SFCF $\sqbrk {q_1, q_2, q_3, \ldots, q_n}$.
{{qed}}
Theorem: Principal Right Ideal is Right Ideal

Let $\struct {R, +, \circ}$ be a ring with unity.
Let $a \in R$.
Let $aR$ be the principal right ideal of $R$ generated by $a$.
Then $aR$ is an right ideal of $R$.

Proof:
We establish that $aR$ is an right ideal of $R$, by verifying the conditions of Test for Right Ideal.
$aR \ne \O$, as $a \circ 1_R = a \in aR$.
Let $x, y \in ar$.
Then:
{{begin-eqn}}
{{eqn | q = \exists r, s \in R
      | l = x
      | r = a \circ r, y = a \circ s
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-y}
      | r = a \circ r + \paren {a \circ -s}
      | c = Product with Ring Negative
}}
{{eqn | r = a \circ \paren {r + \paren {-s} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-y}
      | o = \in
      | r = aR
      | c = 
}}
{{end-eqn}}
Let $s \in aR, x \in R$.
{{begin-eqn}}
{{eqn | l = s
      | o = \in
      | r = aR, x \in R
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists r \in R
      | l = s
      | r = a \circ r
      | c = 
}}
{{eqn | ll= \leadsto
      | l = s \circ x
      | r = a \circ r \circ x
      | c = 
}}
{{eqn | o = \in
      | r = aR
      | c = 
}}
{{end-eqn}}
Thus by Test for Right Ideal, $aR$ is a right ideal of $R$.
{{qed}}
Category:Ideal Theory
ttxrbv8jfdv89sfrnygry6fbth0285o
Theorem: Principal Left Ideal is Left Ideal

Let $\struct {R, +, \circ}$ be a ring with unity.
Let $a \in R$.
Let $Ra$ be the principal left ideal of $R$ generated by $a$.
Then $Ra$ is an left ideal of $R$.

Proof:
We establish that $Ra$ is an left ideal of $R$, by verifying the conditions of Test for Left Ideal.
$Ra \ne \O$, as $1_R \circ a = a \in Ra$.
Let $x, y \in Ra$.
Then:
{{begin-eqn}}
{{eqn | q = \exists r, s \in R
      | l = x
      | r = r \circ a, y = s \circ a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-y}
      | r = r \circ a + \paren {-s \circ a}
      | c = Product with Ring Negative
}}
{{eqn | r = \paren {r + \paren {-s} } \circ a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-y}
      | o = \in
      | r = Ra
      | c = 
}}
{{end-eqn}}
Let $s \in Ra, x \in R$.
{{begin-eqn}}
{{eqn | l = s
      | o = \in
      | r = Ra, x \in R
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists r \in R
      | l = s
      | r = r \circ a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \circ s
      | r = x \circ r \circ a
      | c = 
}}
{{eqn | o = \in
      | r = Ra
      | c = 
}}
{{end-eqn}}
Thus by Test for Left Ideal, $Ra$ is a left ideal of $R$.
{{qed}}
Theorem: Principal Ideal of Commutative Ring

Let $\struct {R, +, \circ}$ be a commutative ring with unity.
Let $a \in R$.
Let $Ra$ be the principal left ideal of $R$ generated by $a$.
Let $aR$ be the principal right ideal of $R$ generated by $a$.
Let $\ideal a$ be the principal ideal of $R$ generated by $a$.
Then $Ra = \ideal a = aR$.

Proof:
By definition of principal left ideal:
:$Ra = \set{r \circ a: r \in R}$
By definition of commutative ring with unity and center of ring:
:$a$ is in the center of $R$
From Principal Ideal from Element in Center of Ring:
:$\ideal a = R \circ a = \set{r \circ a: r \in R}$
Hence:
:$Ra = \ideal a$
We have:
{{begin-eqn}}
{{eqn | l = Ra 
      | r = \set{r \circ a : r \in R}
      | c = {{Defof|Principal Left Ideal of Ring}}
}}
{{eqn | r = \set{a \circ r : r \in R}
      | c = commutativity of ring product $\circ$
}}
{{eqn | r = aR
      | c = {{Defof|Principal Right Ideal of Ring}}
}}
{{end-eqn}}
{{qed}}
Category:Ideal Theory
ladeilhl0herl1pgelp5u31a3emuk46
Theorem: Linear Transformations between Finite-Dimensional Normed Vector Spaces are Continuous

Linear transformations between finite-dimensional normed vector spaces are continuous.

Proof:
We have that Norms on Finite-Dimensional Real Vector Space are Equivalent.
Choose the Euclidean norm.
Let $X = \struct {\R^n, \norm {\, \cdot \,}_2}$ and $Y = \struct {\R^m, \norm {\, \cdot \,}_2}$ be normed vector spaces.
Let the matrix $A \in \R^{m \times n}$ be given by:
:$A = \begin {bmatrix}
a_{1 1} & \cdots & a_{1 n} \\
 \vdots & \ddots & \vdots \\
a_{m 1} & \cdots & a_{m n} \\
\end{bmatrix}$
We have that Set of Linear Transformations is Isomorphic to Matrix Space.
Let $T_A : \R^n \to \R^m$ be the linear transformation such that:
:$\forall \mathbf x \in \R^n : T_A \mathbf x := A \mathbf x$
Then:
{{begin-eqn}}
{{eqn | l = \norm {T_A \mathbf x}^2_2
      | r = \norm {A \mathbf x}^2_2
}}
{{eqn | r = \sum_{i \mathop = 1}^m \paren {\sum_{j \mathop = 1}^n a_{ij} x_j}^2
      | c = {{Defof|Euclidean Norm}}
}}
{{eqn | o = \le
      | r = \sum_{i \mathop = 1}^m \paren {\sum_{j \mathop = 1}^n a_{ij}^2} \paren{\sum_{j \mathop = 1}^n x_j^2}
      | c = Cauchy's Inequality
}}
{{eqn | r = \norm {\mathbf x}_2^2 \paren {\sum_{i \mathop = 1}^m \sum_{j \mathop = 1}^n a_{ij}^2}
      | c = {{Defof|Euclidean Norm}}
}}
{{end-eqn}}
Hence:
:$\ds \norm{T_A \mathbf x}_2 \le \norm{\mathbf x}_2 \sqrt {\sum_{i \mathop = 1}^m \sum_{j \mathop = 1}^n a_{ij}^2 }$
By Continuity of Linear Transformation between Normed Vector Spaces $T_A$ is continuous.
Hence, all linear transformations between finite-dimensional normed vector spaces are continuous. 
{{qed}}
Theorem: Equivalence of Formulations of Axiom of Unions

In the context of class theory, the following formulations of the '''{{axiom-link|Unions}}''' are equivalent:
=== Formulation 1 ===
{{:Axiom:Axiom of Unions (Set Theory)}}
=== Formulation 2 ===
{{:Axiom:Axiom of Unions (Class Theory)}}

Proof:
It is assumed throughout that the {{axiom-link|Extensionality}} and the {{axiom-link|Specification}} both hold.
=== Formulation $1$ implies Formulation $2$ ===
Let formulation $1$ be axiomatic:
{{:Axiom:Axiom of Unions (Set Theory)}}
Thus it is posited that for a given set of sets $A$ the union of $A$ exists:
:$x := \bigcup A := \set {y: \exists z \in A: y \in z}$
and that this is a set.
Formulation $2$ asserts that given the existence of $\bigcup A$, it is axiomatic that $\bigcup A$ is itself a set.
Hence it follows that the truth of formulation $2$ follows from acceptance of the truth of formulation $1$.
From Class Union Exists and is Unique, which depends on:
:the {{axiom-link|Extensionality}}
:the {{axiom-link|Specification}}
$\bigcup A$ is unique for a given $A$.
{{qed|lemma}}
=== Formulation $2$ implies Formulation $1$ ===
Let formulation $2$ be axiomatic:
{{:Axiom:Axiom of Unions (Class Theory)}}
Let $A$ be a set of sets.
Let us create the class:
:$x := \bigcup A := \set {y: \exists z \in A: y \in z}$
From Class Union Exists and is Unique, which depends on:
:the {{axiom-link|Extensionality}}
:the {{axiom-link|Specification}}
$\bigcup A$ exists and is unique for a given $A$.
We have asserted the truth of formulation $2$.
That is, $\bigcup A$ is a set.
As $A$ is arbitrary, it follows that $\bigcup A$ exists and is unique for all sets of sets $A$.
That is, the truth of formulation $1$ follows from acceptance of the truth of formulation $2$.
{{qed}}
Theorem: Intersection of Non-Empty Class is Set/Corollary

Let $x$ be a non-empty set.
Let $\bigcap x$ denote the intersection of $x$.
Then $\bigcap x$ is a set.

Proof:
It is assumed that $x$ is an element of a basic universe.
Hence from the {{axiom-link|Transitivity}}, every set is a class.
Hence Intersection of Non-Empty Class is Set applies directly.
{{qed}}
Theorem: Class Union Distributes over Class Intersection

Let $A$, $B$ and $C$ be classes.
Then:
:$A \cup \paren {B \cap C} = \paren {A \cup B} \cap \paren {A \cup C}$
where:
:$A \cup B$ denotes class union
:$B \cap C$ denotes class intersection.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in A \cup \paren {B \cap C}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in A \lor \paren {x \in B \land x \in C}
      | c = {{Defof|Class Union}} and {{Defof|Class Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in A \lor x \in B} \land \paren {x \in A \lor x \in C}
      | c = Disjunction is Left Distributive over Conjunction
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \paren {A \cup B} \cap \paren {A \cup C}
      | c = {{Defof|Class Union}} and {{Defof|Class Intersection}}
}}
{{end-eqn}}
{{qed}}
Theorem: Class Intersection Distributes over Class Union

Let $A$, $B$ and $C$ be classes.
Then:
:$A \cap \paren {B \cup C} = \paren {A \cap B} \cup \paren {A \cap C}$
where:
:$A \cap B$ denotes class intersection
:$B \cup C$ denotes class union.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in A \cap \paren {B \cup C}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in A \land \paren {x \in B \lor x \in C}
      | c = {{Defof|Class Union}} and {{Defof|Class Intersection}}
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in A \land x \in B} \lor \paren {x \in A \land x \in C}
      | c = Conjunction is Left Distributive over Disjunction
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \paren {A \cap B} \cup \paren {A \cap C}
      | c = {{Defof|Class Union}} and {{Defof|Class Intersection}}
}}
{{end-eqn}}
{{qed}}
Theorem: Theory of Structure is Complete

Let $\AA$ be a structure for a signature for predicate logic $\LL$.
Let $\map {\operatorname{Th}} \AA$ be the theory of $\AA$.
Then $\map {\operatorname{Th}} \AA$ is complete.

Proof:
By definition of $\map {\operatorname{Th}} \AA$ be the theory of $\AA$:
:$\AA \models \map {\operatorname{Th}} \AA$
so that $\map {\operatorname{Th}} \AA$ is consistent.
Now let $\mathbf A$ be an $\LL$-sentence.
Let $\map {\operatorname{val}_\AA} {\mathbf A}$ be the value of $\mathbf A$ in $\AA$.
Then either $\map {\operatorname{val}_\AA} {\mathbf A} = T$ or $\map {\operatorname{val}_\AA} {\mathbf A} = F$.
By definition of value, the latter implies:
:$\map {\operatorname{val}_\AA} {\neg \mathbf A} = T$
Therefore, by definition of the models relation $\models$:
:$\AA \models \mathbf A$ or $\AA \models \mathbf A$
That is, by definition of the theory $\map {\operatorname{Th}} \AA$:
:$\mathbf A \in \map {\operatorname{Th}} \AA$ or $\neg \mathbf A \in \map {\operatorname{Th}} \AA$
By Element is Semantic Consequence of Set, it follows that:
:$\map {\operatorname{Th}} \AA \models \mathbf A$ or $\map {\operatorname{Th}} \AA \models \neg \mathbf A$
Since $\mathbf A$ was arbitrary, it follows that $\map {\operatorname{Th}} \AA$ is complete.
{{qed}}
Theorem: Class Difference with Class Difference

:$A \setminus \paren {A \setminus B} = A \cap B$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in A \setminus \paren {A \setminus B}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in A \land x \notin \paren {A \setminus B}
      | c = {{Defof|Class Difference}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in A \land \lnot \paren {x \in A \land x \notin B}
      | c = {{Defof|Class Difference}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in A \land \paren {x \notin A \lor x \in B}
      | c = De Morgan's Laws
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in A \land x \notin A} \lor \paren {x \in A \land x \in B}
      | c = Conjunction is Left Distributive over Disjunction
}}
{{eqn | o = \leadstoandfrom
      | r = \bot \lor \paren {x \in A \land x \in B}
      | c = {{Defof|Contradiction}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in A \land x \in B
      | c = Disjunction with Contradiction
}}
{{eqn | o = \leadstoandfrom
      | r = x \in \paren {A \cap B}
      | c = {{Defof|Class Intersection}}
}}
{{eqn | o = \leadsto
      | r = A \setminus \paren {A \setminus B} = \paren {A \cap B}
      | c = {{Defof|Class Equality}}
}}
{{end-eqn}}
{{qed}}
Theorem: Class Difference of B with Class Difference of A with B

:$B \setminus \paren {A \setminus B} = B$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in B \setminus \paren {A \setminus B}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in B \land x \notin \paren {A \setminus B}
      | c = {{Defof|Class Difference}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in B \land \paren {x \notin A \lor x \in B}
      | c = De Morgan's Laws
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in B \land x \notin A} \lor \paren {x \in B \land x \in B}
      | c = Conjunction is Left Distributive over Disjunction
}}
{{eqn | o = \leadstoandfrom
      | r = \paren {x \in B \land x \notin A} \lor x \in B
      | c = Rule of Idempotence: Conjunction
}}
{{eqn | o = \leadstoandfrom
      | r = x \in B
      | c = Disjunction Absorbs Conjunction
}}
{{eqn | o = \leadsto
      | r = B \setminus \paren {A \setminus B} = B
      | c = {{Defof|Class Equality}}
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection with Subclass is Subclass

:$A \subseteq B \iff A \cap B = A$

Proof:
Let $A \cap B = A$.
Then by the definition of class equality:
:$A \subseteq A \cap B$
Thus:
{{begin-eqn}}     
{{eqn | l = x
      | o = \in
      | r = A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A \cap B
      | c = {{Defof|Subclass}}: $A \subseteq A \cap B$
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A
      | c = {{Defof|Class Intersection}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = B
      | c = {{Defof|Conjunction}}
}}
{{eqn | ll= \leadsto
      | l = A
      | o = \subseteq
      | r = B
      | c = {{Defof|Subclass}}
}}
{{end-eqn}}
{{qed|lemma}}
Now let $A \subseteq B$.
{{begin-eqn}}     
{{eqn | l = x
      | o = \in
      | r = A \cap B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A
      | c = {{Defof|Class Intersection}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A
      | c = {{Defof|Conjunction}}
}}
{{eqn | ll= \leadsto
      | l = A \cap B
      | o = \subseteq
      | r = A
      | c = {{Defof|Subclass}}
}}
{{end-eqn}}
We also have:
{{begin-eqn}}     
{{eqn | l = x
      | o = \in
      | r = A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A
      | c = 
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = B
      | c = {{Defof|Subclass}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A \cap B
      | c = {{Defof|Class Intersection}}
}}
{{end-eqn}}
So as we have:
{{begin-eqn}}     
{{eqn | l = A \cap B
      | o = \subseteq
      | r = A
}}
{{eqn | l = A
      | o = \subseteq
      | r = A \cap B
}}
{{end-eqn}}
it follows from the definition of class equality that:
:$A \cap B = A$
{{Qed}}
Theorem: Union with Superclass is Superclass

:$A \subseteq B \iff A \cup B = B$

Proof:
Let $A \cup B = B$.
Then by definition of class equality:
:$A \cup B \subseteq B$
Thus:
{{begin-eqn}}     
{{eqn | l = x
      | o = \in
      | r = A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A
      | c = Rule of Addition
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A \cup B
      | c = {{Defof|Class Union}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = B
      | c = {{Defof|Subclass}}: $A \cup B \subseteq B$
}}
{{eqn | ll= \leadsto
      | l = A
      | o = \subseteq
      | r = B
      | c = {{Defof|Subclass}}
}}
{{end-eqn}}
{{qed|lemma}}
Now let $A \subseteq B$.
We have:
{{begin-eqn}}     
{{eqn | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A
      | c = Rule of Addition
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A \cup B
      | c = {{Defof|Class Union}}
}}
{{eqn | ll= \leadsto
      | l = B
      | o = \subseteq
      | r = A \cup B
      | c = {{Defof|Subclass}}
}}
{{end-eqn}}
From Subset of Union, we have $S \cup T \supseteq T$.
We also have:
{{begin-eqn}}     
{{eqn | l = x
      | o = \in
      | r = A \cup B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = A
      | c = Rule of Addition
}}
{{eqn | lo= \lor
      | l = x
      | o = \in
      | r = B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = B
      | c = as $x \in A \implies x \in B$
}}
{{eqn | ll= \leadsto
      | l = A \cup B
      | o = \subseteq
      | r = B
      | c = {{Defof|Subclass}}
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = A \cup B
      | o = \subseteq
      | r = B
      | c = 
}}
{{eqn | l = B
      | o = \subseteq
      | r = A \cup B
      | c = 
}}
{{end-eqn}}
By definition of class equality:
:$A \cup B = B$
{{Qed}}
Theorem: Class Difference with Class Difference with Subclass

Let $A$ and $B$ be classes.
Let $B \subseteq A$.
Then:
:$A \setminus \paren {A \setminus B} = B$

Proof:
From Class Difference with Class Difference:
:$A \setminus \paren {A \setminus B} = A \cap B$
for all classes $A$ and $B$.
From Intersection with Subclass is Subclass:
:$A \subseteq B \iff A \cap B = A$
The result follows.
{{qed}}
Theorem: Equivalence of Formulations of Axiom of Powers

In the context of class theory, the following formulations of the '''{{axiom-link|Powers}}''' are equivalent:
=== Formulation 1 ===
{{:Axiom:Axiom of Powers (Set Theory)}}
=== Formulation 2 ===
{{:Axiom:Axiom of Powers (Class Theory)}}

Proof:
It is assumed throughout that the {{axiom-link|Extensionality}} and the {{axiom-link|Specification}} both hold.
Theorem: Linear Integral Bounded Operator is Continuous

Let $I = \closedint 0 1$ be a closed real interval.
Let $A : I \times I \to \R$ be a real function such that:
:$\ds \int_0^1 \int_0^1 \paren {\map A {t, \tau} }^2 \rd t \rd \tau < \infty$
{{Research|For now "bounded" means above. Need to check if this meaning is standard}}
where $\times$ denotes the cartesian product.
Let $T_A : \map {L^2} I \to \map {L^2} I$ be an integral operator such that:
:$\ds \map {\paren {T_A \mathbf x} } t := \int_0^1 \map A {t, \tau} \map {\mathbf x} \tau \rd \tau$
where $\mathbf x \in \map {L^2} I$, and $\map {L^2} I$ is the Lebesgue $2$-space.
Then $T_A$ is a continuous transformation.

Proof:
We have that Riemann Integral Operator is Linear Mapping.
{{Research|Probably this should be replaced with Lebesgue integral. The source does not say anything about compatibility of Riemann integral and Lebesgue space}}
Hence, $T_A$ is a linear transformation.
Furthermore:
{{begin-eqn}}
{{eqn | l = \norm {T_A \mathbf x}_2^2
      | r = \int_0^1 \paren {\int_0^1 \map A {t, \tau} \map {\mathbf x} \tau \rd \tau}^2 \rd t
      | c = {{Defof|P-Seminorm}}
}}
{{eqn | o = \le
      | r = \int_0^1 \paren{\int_0^1 \paren{\map A {t, \tau} }^2 \rd \tau} \paren {\int_0^1 \paren{\map {\mathbf x} \tau}^2 \rd \tau }\rd t
      | c = Cauchy-Bunyakovsky-Schwarz Inequality for Definite Integrals
}}
{{eqn | o = \le
      | r = \paren {\int_0^1 \int_0^1 \paren{\map A {t, \tau} }^2 \rd \tau \rd t} \paren {\int_0^1 \paren{\map {\mathbf x} \tau}^2 \rd \tau }
}}
{{eqn | r = \paren {\int_0^1 \int_0^1 \paren{\map A {t, \tau} }^2 \rd \tau \rd t} \norm {\mathbf x}_2^2
      | c = {{Defof|P-Seminorm}}
}}
{{eqn | o = <
      | r = \infty
}}
{{end-eqn}}
Hence:
:$T_A \mathbf x \in \map {L^2} I$
By Continuity of Linear Transformation between Normed Vector Spaces:
:$T_A \in \map {CL} {\map {L^2} I}$
{{qed}}
Theorem: Subset is Element of Power Set

:$y \in \powerset x \iff y \subseteq x$

Proof:
By definition of power set, $\powerset x$ is the set of subsets of $x$.
Hence the result, by definition of subset and power set.
{{qed}}
Theorem: Class Union Exists and is Unique

Let $V$ be a basic universe.
Let $A \subseteq V$ be a class.
Let $\bigcup A$ denote the union of $A$.
Then $\bigcup A$ is guaranteed to exist and is unique.

Proof:
By the Axiom of Specification the union of $A$ can be created:
:$\bigcup A := \set {x: \exists y: x \in y \land y \in A}$
Hence $\bigcup A$ exists.
Let $B$ and $C$ both be unions of $A$.
From the definition of union:
:$\forall A$:
::$x \in B \iff \exists y \in A: x \in y$
::$x \in C \iff \exists y \in A: x \in y$
From Biconditional is Commutative and Biconditional is Transitive:
:$x \in B \iff x \in C$
By the Axiom of Extension:
:$B = C$
Hence the union of $A$ is unique.
{{qed}}
Theorem: Trace of Product of Matrices

Let $\struct {R, +, \circ}$ be a commutative ring.
Let $\mathbf A = \sqbrk a_{m n}$ be an $m \times n$ matrix over $R$.
Let $\mathbf B = \sqbrk b_{n m}$ be an $n \times m$ matrix over $R$.
Then:
:$\map \tr {\mathbf A \mathbf B} = \map \tr {\mathbf B \mathbf A}$
where $\map \tr {\mathbf A}$ denotes the trace of $\mathbf A$.

Proof:
Let $\mathbf A \mathbf B = \mathbf C = \sqbrk c_m$.
Let $\mathbf B \mathbf A = \mathbf D = \sqbrk d_n$.
Then by definition of matrix products:
{{begin-eqn}}
{{eqn | q = \forall i, j \in \closedint 1 m
      | l = c_{i j}
      | r = \sum_{k \mathop = 1}^n a_{i k} \circ b_{k j}
}}
{{eqn | q = \forall i, j \in \closedint 1 n
      | l = d_{i j}
      | r = \sum_{k \mathop = 1}^m b_{i k} \circ a_{k j}
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \map \tr {\mathbf A \mathbf B}
      | r = \sum_{j \mathop = 1}^m c_{jj}
      | c = {{Defof|Trace of Matrix}}
}}
{{eqn | r = \sum_{j \mathop = 1}^m \sum_{k \mathop = 1}^n a_{j k} \circ b_{k j}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \sum_{j \mathop = 1}^m a_{j k} \circ b_{k j}
      | c = Exchange of Order of Indexed Summations
}}
{{eqn | r = \sum_{k \mathop = 1}^n \sum_{j \mathop = 1}^m b_{k j} \circ a_{j k}
      | c = $\circ$ is commutative
}}
{{eqn | r = \sum_{k \mathop = 1}^n d_{kk}
      | c =
}}
{{eqn | r = \map \tr {\mathbf B \mathbf A}
      | c = {{Defof|Trace of Matrix}}
}}
{{end-eqn}}
{{qed}}
Category:Traces of Matrices
Category:Conventional Matrix Multiplication
sj1xvs5lzeios04xuvxy2nbcnyztzis