avewright/proofwiki-math huggingface dataset:
Theorem: Linear Operator on the Plane

Let $\phi$ be a linear operator on the real vector space of two dimensions $\R^2$.
Then $\phi$ is completely determined by an ordered tuple of $4$ real numbers.

Proof:
Let $\phi$ be a linear operator on $\R^2$.
Let $\alpha_{11}, \alpha_{12}, \alpha_{21}, \alpha_{22} \in \R$ be the real numbers which satisfy the equations:
{{begin-eqn}}
{{eqn | l = \map \phi {e_1}
      | r = \alpha_{11} e_1 + \alpha_{21} e_2
      | c = 
}}
{{eqn | l = \map \phi {e_2}
      | r = \alpha_{12} e_1 + \alpha_{22} e_2
      | c = 
}}
{{end-eqn}}
where $\tuple {e_1, e_2}$ is the standard ordered basis of $\R^2$.
Then, by linearity:
{{begin-eqn}}
{{eqn | l = \map \phi {\lambda_1, \lambda_2}
      | r = \map \phi {\lambda_1 e_1 + \lambda_2 e_2}
      | c = 
}}
{{eqn | r = \lambda_1 \map \phi {e_1} + \lambda_2 \map \phi {e_2}
      | c = 
}}
{{eqn | r = \paren {\lambda_1 \alpha_{11} + \lambda_2 \alpha_{12} } e_1 + \paren {\lambda_1 \alpha_{21} + \lambda_2 \alpha_{22} } e_2
      | c = 
}}
{{eqn | r = \paren {\lambda_1 \alpha_{11} + \lambda_2 \alpha_{12}, \lambda_1 \alpha_{21} + \lambda_2 \alpha_{22} }
      | c = 
}}
{{end-eqn}}
Conversely, if $\alpha_{11}, \alpha_{12}, \alpha_{21}, \alpha_{22} \in \R$ are ''any'' real numbers, then we can define the mapping $\phi$ as:
:$\map \phi {\lambda_1, \lambda_2} = \tuple {\lambda_1 \alpha_{11} + \lambda_2 \alpha_{12}, \lambda_1 \alpha_{21} + \lambda_2 \alpha_{22} }$
which is easily verified as being a linear operator on $\R^2$:
{{begin-eqn}}
{{eqn | l = b \cdot \map \phi {\lambda_1, \lambda_2} + c \cdot \map \phi {\lambda_3, \lambda_4}
      | r = b \tuple {\lambda_1 \alpha_{11} + \lambda_2 \alpha_{12}, \lambda_1 \alpha_{21} + \lambda_2 \alpha_{22} } + c \tuple {\lambda_3 \alpha_{11} + \lambda_4 \alpha_{12}, \lambda_3 \alpha_{21} + \lambda_4 \alpha_{22} }
      | c = 
}}
{{eqn | r = \tuple {b \lambda_1 \alpha_{11} + b \lambda_2 \alpha_{12}, b \lambda_1 \alpha_{21} + b \lambda_2 \alpha_{22} } + \tuple {c \lambda_3 \alpha_{11} + c \lambda_4 \alpha_{12}, c \lambda_3 \alpha_{21} + c \lambda_4 \alpha_{22} }
      | c = 
}}
{{eqn | r = \tuple {b \lambda_1 \alpha_{11} + b \lambda_2 \alpha_{12} + c \lambda_3 \alpha_{11} + c \lambda_4 \alpha_{12}, b \lambda_1 \alpha_{21} + b \lambda_2 \alpha_{22} + c \lambda_3 \alpha_{21} + c \lambda_4 \alpha_{22} }
      | c = 
}}
{{eqn | r = \tuple {\paren {b \lambda_1 + c \lambda_3} \alpha_{11} + \tuple {b \lambda_2 + c \lambda_4} \alpha_{12}, \paren {b \lambda_1 + c \lambda_3} \alpha_{21} + \paren {c \lambda_2 + c \lambda_4} \alpha_{22} }
      | c = 
}}
{{eqn | r = \tuple {b \lambda_1 + c \lambda_3, b \lambda_2 + c \lambda_4}
      | c = 
}}
{{end-eqn}}
Thus, by Condition for Linear Transformation, $\phi$ is a linear operator on $\R^2$.
Thus each linear operator on $\R^2$ is completely determined by the ordered tuple:
:$\tuple {\alpha_{11}, \alpha_{12}, \alpha_{21}, \alpha_{22} }$
of real numbers.
{{Qed}}
Theorem: Similarity Mapping is Linear Operator

Let $G$ be a vector space over a field $\struct {K, +, \times}$.
Let $\beta \in K$.
Then the similarity $s_\beta: G \to G$ defined as:
:$\forall \mathbf x \in G: \map {s_\beta} {\mathbf x} = \beta \mathbf x$
is a linear operator on $G$.

Proof:
To prove that $s_\beta$ is a linear operator it is sufficient to demonstrate that:
:$(1): \quad \forall \mathbf x, \mathbf y \in G: \map {s_\beta} {\mathbf x + \mathbf y} = \map {s_\beta} {\mathbf x} + \map {s_\beta} {\mathbf y}$
:$(2): \quad \forall \mathbf x \in G: \forall \lambda \in K: \map {s_\beta} {\lambda \mathbf x} = \lambda \map {s_\beta} {\mathbf x}$
Indeed:
{{begin-eqn}}
{{eqn | q = \forall \mathbf x, \mathbf y \in G
      | l = \map {s_\beta} {\mathbf x + \mathbf y}
      | r = \beta \paren {\mathbf x + \mathbf y}
      | c = Definition of $s_\beta$
}}
{{eqn | r = \beta \, \mathbf x + \beta \, \mathbf y
      | c = {{Vector-space-axiom|1}}
}}
{{eqn | r = \map {s_\beta} {\mathbf x} + \map {s_\beta} {\mathbf y}
      | c = Definition of $s_\beta$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | q = \forall \mathbf x \in G: \forall \lambda \in K
      | l = \map {s_\beta} {\lambda \mathbf x}
      | r = \beta \paren {\lambda \mathbf x}
      | c = Definition of $s_\beta$
}}
{{eqn | r = \beta \lambda \paren {\mathbf x}
      | c = {{Vector-space-axiom|3}}
}}
{{eqn | r = \lambda \beta \paren {\mathbf x}
      | c = {{Field-axiom|M2}}
}}
{{eqn | r = \lambda \map {s_\beta} {\mathbf x}
      | c = Definition of $s_\beta$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Cantor-Dedekind Hypothesis

The points on an infinite straight line are in one-to-one correspondence with the set $\R$ of real numbers.
Hence the set of all points on an infinite straight line and $\R$ are equinumerous.

Proof:
=== Step 1 ===
We will show that there exists a mapping from the infinite straight line $L$ to the set of real numbers $\R$.
Let us establish a relation $h$ between points on $L$ and elements of $\R$.
We allow the Axiom of Choice to set up a choice function to allow the points of $L$ to be selected systematically.
Pick any point on $L$, and label it $z$. This point can be referred to informally as the origin.
Map $z$ to zero, that is, by allowing $\tuple {z, 0} \in h$. 
Using the choice function pick any other point on $L$.
From Euclid's first postulate, we can draw a line segment between the two points.
If the second point is to the right of the origin, let its length be positive.
If the second point is to the left of the origin, let its length be negative.
The existence of the choice function allows that this process can be done for any point on $L$
Hence:
:$\forall p \in L: \exists x \in \R: \tuple {p, x} \in h$
That is, $h$ is left-total.
The method of construction of $h$ is such that every point on $L$ is assigned to exactly one element of $\R$.
Thus it is seen that $h$ is many-to-one.
Hence, by definition, $h$ is a mapping.
Since every point mapped to is associated to exactly one element of $L$, $h$ is injective.
{{qed|lemma}}
Theorem: Rotation of Plane about Origin is Linear Operator

Let $r_\alpha$ be the rotation of the plane about the origin through an angle of $\alpha$.
That is, let $r_\alpha: \R^2 \to \R^2$ be the mapping defined as:
:$\forall x \in \R^2: \map {r_\alpha} x = \text { the point into which a rotation of $\alpha$ carries $x$}$
Then $r_\alpha$ is a linear operator.

Proof:
Let $P = \tuple {\lambda_1, \lambda_2}$ be an arbitrary point in $\R^2$.
From Equations defining Plane Rotation:
:$\map {r_\alpha} P = \tuple {\lambda_1 \cos \alpha - \lambda_2 \sin \alpha, \lambda_1 \sin \alpha + \lambda_2 \cos \alpha}$
This demonstrates that $r_\alpha$ can be expressed as an ordered tuple of $4$ real numbers.
The result follows from Linear Operator on the Plane.
{{qed}}
Theorem: Reflection of Plane in Line through Origin is Linear Operator

Let $M$ be a straight line in the plane $\R^2$ passing through the origin.
Let $s_M$ be the '''reflection''' of $\R^2$ in $M$.
Then $s_M$ is a linear operator for every straight line $M$ through the origin.

Proof:
Let the angle between $M$ and the $x$-axis be $\alpha$.
To prove that $s_M$ is a '''linear operator''' it is sufficient to demonstrate that:
:$(1): \quad \forall P_1, P_2 \in \R^2: \map {s_M} {P_1 + P_2} = \map {s_M} {P_1} + \map {s_M} {P_2}$
:$(2): \quad \forall \lambda \in \R: \map {s_M} {\lambda P_1} = \lambda \map {s_M} {P_1}$
So, let $P_1 = \tuple {x_1, y_1}$ and $P_2 = \tuple {x_2, y_2}$ be arbitrary points in the plane.
{{begin-eqn}}
{{eqn | l = \map {s_M} {P_1 + P_2}
      | r = \tuple {\paren {x_1 + x_2} \cos 2 \alpha + \paren {y_1 + y_2} \sin 2 \alpha, \paren {x_1 + x_2} \sin 2 \alpha - \paren {y_1 + y_2} \cos 2 \alpha}
      | c = Equations defining Plane Reflection: Cartesian
}}
{{eqn | r = \tuple {x_1 \cos 2 \alpha + y_1 \sin 2 \alpha, x_1 \sin 2 \alpha - y_1 \cos 2 \alpha} + \tuple {x_2 \cos 2 \alpha + y_2 \sin 2 \alpha, x_2 \sin 2 \alpha - y_2 \cos 2 \alpha}
      | c = 
}}
{{eqn | r = \map {s_M} {P_1} + \map {s_M} {P_2}
      | c = Equations defining Plane Reflection: Cartesian
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | q = \forall \lambda \in \R
      | l = \map {s_M} {\lambda P_1}
      | r = \map {s_M} {\lambda \tuple {x_1, y_1} }
      | c = Definition of $P_1$
}}
{{eqn | r = \tuple {\lambda x_1 \cos 2 \alpha + \lambda y_1 \sin 2 \alpha, \lambda x_1 \sin 2 \alpha - \lambda y_1 \cos 2 \alpha}
      | c = Equations defining Plane Reflection: Cartesian
}}
{{eqn | r = \lambda \tuple {x_1 \cos 2 \alpha + y_1 \sin 2 \alpha, x_1 \sin 2 \alpha - y_1 \cos 2 \alpha}
      | c = 
}}
{{eqn | r = \lambda \map {s_M} {P_1}
      | c = Equations defining Plane Reflection: Cartesian
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Projection in Plane between Lines passing through Origin is Linear Operator

Let $M$ and $N$ be distinct straight lines through the plane through the origin.
Let $\pr_{M, N}$ be the projection on $M$ along $N$.
Then $\pr_{M, N}$ is a linear operator.

Proof:
Let the angle between $M$ and the $x$-axis be $\theta$.
Let the angle between $N$ and the $x$-axis be $\phi$.
Let $P = \tuple {x, y}$ be an arbitrary point in the plane.
Then from Equations defining Projection in Plane:
:$\map {\pr_{M, N} } P = \begin {cases} 
\tuple {0, y - x \tan \phi} & : \theta = \dfrac \pi 2 \\
\tuple {x, x \tan \theta} & : \phi = \dfrac \pi 2 \\
\tuple {\dfrac {x \tan \phi} {\tan \phi - \tan \theta} - \dfrac y {\tan \phi - \tan \theta}, \dfrac {y \tan \theta} {\tan \theta - \tan \phi} - \dfrac {x \tan \theta \tan \phi} {\tan \theta - \tan \phi} } & : \text {otherwise} 
\end {cases}$
This demonstrates that $\map {\pr_{M, N} } P$ can be expressed as an ordered tuple of $4$ real numbers.
The result follows from Linear Operator on the Plane.
{{qed}}
Theorem: Condition for Straight Lines in Plane to be Parallel/General Equation

Let $L: \alpha_1 x + \alpha_2 y = \beta$ be a straight line in $\R^2$.
Then the straight line $L'$ is parallel to $L$ {{iff}} there is a $\beta' \in \R^2$ such that:
:$L' = \set {\tuple {x, y} \in \R^2: \alpha_1 x + \alpha_2 y = \beta'}$

Proof:
=== Necessary Condition ===
When $L' = L$, the claim is trivial.
Let $L' \ne L$ be described by the equation:
:$\alpha'_1 x + \alpha'_2 y = \beta'$
{{WLOG}}, let $\alpha'_1 \ne 0$ (the case $\alpha'_2 \ne 0$ is similar).
Then for $\tuple {x, y} \in L'$ to hold, one needs:
{{begin-eqn}}
{{eqn | l = \alpha'_1 x + \alpha'_2 y
      | r = \beta'
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \frac {-\alpha'_2} {\alpha'_1} y + \frac {\beta'} {\alpha'_1}
}}
{{end-eqn}}
For $L'$ to be parallel to $L$, it is required that then $\tuple {x, y} \notin L$, that is:
{{begin-eqn}}
{{eqn | l = \alpha_1 x + \alpha_2 y
      | o = \ne
      | r = \beta
}}
{{eqn | ll= \leadstoandfrom
      | l = \alpha_1 \paren {\frac {-\alpha'_2} {\alpha'_1} y + \frac {\beta'} {\alpha'_1} } + \alpha_2 y
      | o = \ne
      | r = \beta
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {\alpha_2 - \alpha_1 \frac {\alpha'_2} {\alpha'_1} } y + \alpha_1 \frac {\beta'} {\alpha'_1}
      | o = \ne
      | r = \beta
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {\alpha_2 - \alpha_1 \frac {\alpha'_2} {\alpha'_1} } y
      | o = \ne
      | r = \beta - \alpha_1 \frac {\beta'} {\alpha'_1}
}}
{{end-eqn}}
It follows that necessarily $\beta - \alpha_1 \frac {\beta'} {\alpha'_1} \ne 0$, or taking $y = 0$ would yield equality.
The only remaining way to obtain the desired inequality for all $y$ is that:
:$\alpha_2 - \alpha_1 \dfrac {\alpha'_2} {\alpha'_1} = 0$
One observes that now $\alpha_1 = 0 \implies \alpha_2 = 0$.
However, as $L: \alpha_1 x + \alpha_2 y = \beta$ is a straight line in $\R^2$, it cannot be that $\alpha_1 = \alpha_2 = 0$.
So $\alpha_1 \ne 0$, and one finds:
:$\alpha'_2 = \dfrac {\alpha'_1} {\alpha_1} \alpha_2$
Hence obtain:
{{begin-eqn}}
{{eqn | l = \alpha'_1 x + \alpha'_2 y
      | r = \beta'
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac {\alpha'_1} {\alpha_1} \paren {\alpha_1 x + \alpha_2 y}
      | r = \beta'
}}
{{eqn | ll= \leadstoandfrom
      | l = \alpha_1 x + \alpha_2 y
      | r = \beta' \frac {\alpha_1} {\alpha'_1}
}}
{{end-eqn}}
That is, $L'$ is described by an equation of the required form.
{{qed|lemma}}
Theorem: Condition for Planes to be Parallel

Let $P: \alpha_1 x_1 + \alpha_2 x_2 + \alpha_3 x_3 = \gamma$ be a plane in $\R^3$.
Then the plane $P'$ is parallel to $P$ {{iff}} there is a $\gamma' \in \R$ such that:
:$P' = \set {\tuple {x_1, x_2, x_3} \in \R^3 : \alpha_1 x_1 + \alpha_2 x_2 + \alpha_3 x_3 = \gamma'}$

Proof:
=== Necessary Condition ===
We have that $P$ and $P'$ are parallel.
If $P = P'$, then $\gamma' = \gamma$ and we are done.
Let $P \neq P'$.
Let $\mathbf x$ be a point in $P$.
Construct a line $L$ through $\mathbf x$ perpendicular to $P'$.
Let $L_{P'}$ be a line in $P'$ that intersects $L$.
Let $L_P$ be a line in $P'$ that intersects $L$ and is parallel to $L_{P'}$.
The line $L_P$ exists since $P$ and $P'$ are parallel.
Since $L$ is perpendicular to $P'$, $L$ is perpendicular to $L_{P'}$.
From Parallelism implies Equal Corresponding Angles, $L$ is perpendicular to $L_P$.
Therefore, $L$ is perpendicular to $P$.
We have:
:$P: \alpha_1 x_1 + \alpha_2 x_2 + \alpha_3 x_3 = \gamma$
Let $\mathbf v$ be the vector:
:$\mathbf v = \alpha_1 \mathbf i + \alpha_2 \mathbf j + \alpha_3 \mathbf k$
From Coefficients of Coordinates in General Equation of Plane Form Vector Perpendicular to Plane, $\mathbf v$ is perpendicular to $P$.
From Two Lines Perpendicular to Same Plane are Parallel, $\mathbf v$ is parallel to $L$.
Let $P'$ be given by:
:$P' = \set {\tuple {x_1, x_2, x_3} \in \R^3 : \beta_1 x_1 + \beta_2 x_2 + \beta_3 x_3 = \delta}$
Let $\mathbf w$ be the vector:
:$\mathbf w = \beta_1 \mathbf i + \beta_2 \mathbf j + \beta_3 \mathbf k$
From Coefficients of Coordinates in General Equation of Plane Form Vector Perpendicular to Plane,  is perpendicular to $P'$.
From Two Lines Perpendicular to Same Plane are Parallel, $\mathbf w$ is parallel to $L$.
Thus, by Lines Parallel to Same Line not in Same Plane are Parallel to each other, $\mathbf v$ is parallel to $\mathbf w$.
Therefore, $\mathbf w = k \mathbf v$ for some $k \neq 0$.
Therefore:
:$\forall i \in \closedint 1 3 : \beta_i = k \alpha_i$
Thus, an equivalent equation for $P'$ is:
:$P' = \set {\tuple {x_1, x_2, x_3} \in \R^3 : k \alpha_1 x_1 + k \alpha_2 x_2 + k \alpha_3 x_3 = \delta}$
or
:$P' = \set {\tuple {x_1, x_2, x_3} \in \R^3 : \alpha_1 x_1 + \alpha_2 x_2 + \alpha_3 x_3 = \delta/k}$
Let $\gamma' = \delta/k$.
Thus, we have:
:$P' = \set {\tuple {x_1, x_2, x_3} \in \R^3 : \alpha_1 x_1 + \alpha_2 x_2 + \alpha_3 x_3 = \gamma'}$
{{qed|lemma}}
Theorem: Lines are Subspaces of Plane

The one-dimensional subspaces of $\R^2$ are precisely the homogeneous lines of plane analytic geometry.

Proof:
Follows directly from Equivalent Statements for Vector Subspace Dimension One Less.
{{qed}}
{{explain|Explain how}}
Theorem: Planes are Subspaces of Space

The two-dimensional subspaces of $\R^3$ are precisely the homogeneous planes of solid analytic geometry.

Proof:
Follows directly from Equivalent Statements for Vector Subspace Dimension One Less.
{{qed}}
{{explain|How?}}
Theorem: Matrix Space Semigroup under Hadamard Product

Let $\map {\MM_S} {m, n}$ be the matrix space over a semigroup $\struct {S, \cdot}$.
Then the algebraic structure $\struct {\map {\MM_S} {m, n}, \circ}$, where $\circ$ is the Hadamard product, is also a semigroup.
If $\struct {S, \cdot}$ is a commutative semigroup then so is $\struct {\map {\MM_S} {m, n}, \circ}$.
If $\struct {S, \cdot}$ is a monoid then so is $\struct {\map {\MM_S} {m, n}, \circ}$.

Proof:
$\struct {S, \cdot}$ is a semigroup and is therefore closed and associative.
As $\struct {S, \cdot}$ is closed, then so is $\struct {\map {\MM_S} {m, n}, \circ}$ from Closure of Hadamard Product.
As $\struct {S, \cdot}$ is associative, then so is $\struct {\map {\MM_S} {m, n}, \circ}$ from Associativity of Hadamard Product.
Thus if $\struct {S, \cdot}$ is a semigroup then so is $\struct {\map {\MM_S} {m, n}, \circ}$.
If $\struct {S, \cdot}$ is commutative, then so is $\struct {\map {\MM_S} {m, n}, \circ}$ from Commutativity of Hadamard Product.
Thus if $\struct {S, \cdot}$ is a commutative semigroup then so is $\struct {\map {\MM_S} {m, n}, \circ}$.
Let $\struct {S, \cdot}$ be a monoid, with identity $e$.
Then from Zero Matrix is Identity for Hadamard Product, $\struct {\map {\MM_S} {m, n}, \circ}$ also has an identity and is therefore also a monoid.
{{Qed}}
Category:Hadamard Product
mghfcbo5xnx98nct7q34ig8cc1t7uoo
Theorem: Hadamard Product over Group forms Group

Let $\struct {G, \cdot}$ be a group whose identity is $e$.
Let $\map {\MM_G} {m, n}$ be a $m \times n$ matrix space over $\struct {G, \cdot}$.
Then $\struct {\map {\MM_G} {m, n}, \circ}$, where $\circ$ is Hadamard product, is also a group.

Proof:
As $\struct {G, \cdot}$, being a group, is a monoid, it follows from Matrix Space Semigroup under Hadamard Product that $\struct {\map {\MM_G} {m, n}, \circ}$ is also a monoid.
As $\struct {G, \cdot}$ is a group, it follows from Negative Matrix is Inverse for Hadamard Product that all elements of $\struct {\map {\MM_G} {m, n}, \circ}$ have an inverse.
The result follows.
{{Qed}}
Theorem: Matrix Multiplication is Associative

Matrix multiplication (conventional) is associative.

Proof:
Let $\mathbf A = \sqbrk a_{m n}, \mathbf B = \sqbrk b_{n p}, \mathbf C = \sqbrk c_{p q}$ be matrices.
From inspection of the subscripts, we can see that both $\paren {\mathbf A \mathbf B} \mathbf C$ and $\mathbf A \paren {\mathbf B \mathbf C}$ are defined:
$\mathbf A$ has $n$ columns and $\mathbf B$ has $n$ rows, while $\mathbf B$ has $p$ columns and $\mathbf C$ has $p$ rows.
Consider $\paren {\mathbf A \mathbf B} \mathbf C$.
Let $\mathbf R = \sqbrk r_{m p} = \mathbf A \mathbf B, \mathbf S = \sqbrk s_{m q} = \paren {\mathbf A \mathbf B} \mathbf C$.
Then:
{{begin-eqn}}     
{{eqn | l = s_{i j}
      | r = \sum_{k \mathop = 1}^p r_{i k} \circ c_{k j}
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{eqn | l = r_{i k}
      | r = \sum_{l \mathop = 1}^n a_{i l} \circ b_{l k}
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{eqn | ll= \leadsto
      | l = s_{i j}
      | r = \sum_{k \mathop = 1}^p \paren {\sum_{l \mathop = 1}^n a_{i l} \circ b_{l k} } \circ c_{k j}
}}
{{eqn | r = \sum_{k \mathop = 1}^p \sum_{l \mathop = 1}^n \paren {a_{i l} \circ b_{l k} } \circ c_{k j}
      | c = {{Ring-axiom|D}}
}}
{{end-eqn}}
Now consider $\mathbf A \paren {\mathbf B \mathbf C}$.
Let $\mathbf R = \sqbrk r_{n q} = \mathbf B \mathbf C, \mathbf S = \sqbrk s_{m q} = \mathbf A \paren {\mathbf B \mathbf C}$.
Then:
{{begin-eqn}}
{{eqn | l = s_{i j}
      | r = \sum_{l \mathop = 1}^n a_{i l} \circ r_{l j}
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{eqn | l = r_{l j}
      | r = \sum_{k \mathop = 1}^p b_{l k} \circ c_{k j}
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{eqn | ll= \leadsto
      | l = s_{i j}
      | r = \sum_{l \mathop = 1}^n a_{i l} \circ \paren {\sum_{k \mathop = 1}^p b_{l k} \circ c_{k j} }
}}
{{eqn | r = \sum_{l \mathop = 1}^n \sum_{k \mathop = 1}^p a_{i l} \circ \paren {b_{l k} \circ c_{k j} }
      | c = {{Ring-axiom|D}}
}}
{{end-eqn}}
Using {{Ring-axiom|M1}}:
:$\ds s_{i j} = \sum_{k \mathop = 1}^p \sum_{l \mathop = 1}^n \paren {a_{i l} \circ b_{l k} } \circ c_{k j} = \sum_{l \mathop = 1}^n \sum_{k \mathop = 1}^p a_{i l} \circ \paren {b_{l k} \circ c_{k j} } = s'_{i j}$
It is concluded that:
:$\paren {\mathbf A \mathbf B} \mathbf C = \mathbf A \paren {\mathbf B \mathbf C}$
{{qed}}
Theorem: Set of Linear Transformations is Isomorphic to Matrix Space

Let $R$ be a ring with unity.
Let $F$, $G$ and $H$ be free $R$-modules of finite dimension $p, n, m > 0$ respectively.
Let $\sequence {a_p}$, $\sequence {b_n}$ and $\sequence {c_m}$ be ordered bases 
Let $\map {\LL_R} {G, H}$ denote the set of all linear transformations from $G$ to $H$.
Let $\map {\MM_R} {m, n}$ be the $m \times n$ matrix space over $R$.
Let $\sqbrk {u; \sequence {c_m}, \sequence {b_n} }$ be the matrix of $u$ relative to $\sequence {b_n}$ and $\sequence {c_m}$.
Let $M: \map {\LL_R} {G, H} \to \map {\MM_R} {m, n}$ be defined as:
:$\forall u \in \map {\LL_R} {G, H}: \map M u = \sqbrk {u; \sequence {c_m}, \sequence {b_n} }$
Then $M$ is a module isomorphism.

Proof:
Let $u, v \in \map {\LL_R} {G, H}$ such that:
:$\map M u = \map M v$
We have that the matrix of $u$ relative to $\sequence {b_n}$ and $\sequence {c_m}$ is defined as the $m \times n$ matrix $\sqbrk \alpha_{m n}$ where:
:$\ds \forall \tuple {i, j} \in \closedint 1 m \times \closedint 1 n: \map u {b_j} = \sum_{i \mathop = 1}^m \alpha_{i j} \circ c_i$
and it is seen that $\map M u$ and $\map M v$ are the same object.
That is:
:$\map M u = \map M v \implies u = v$
and $M$ is seen to be injective.
{{finish|Surjectivity needs proving, so does homomorphism}}
Theorem: Matrix Multiplication Distributes over Matrix Addition

Matrix multiplication (conventional) is distributive over matrix entrywise addition.

Proof:
Let $\mathbf A = \sqbrk a_{m n}, \mathbf B = \sqbrk b_{n p}, \mathbf C = \sqbrk c_{n p}$ be matrices over a ring $\struct {R, +, \circ}$.
Consider $\mathbf A \paren {\mathbf B + \mathbf C}$.
Let $\mathbf R = \sqbrk r_{n p} = \mathbf B + \mathbf C, \mathbf S = \sqbrk s_{m p} = \mathbf A \paren {\mathbf B + \mathbf C}$.
Let $\mathbf G = \sqbrk g_{m p} = \mathbf A \mathbf B, \mathbf H = \sqbrk h_{m p} = \mathbf A \mathbf C$.
Then:
{{begin-eqn}}
{{eqn | l = s_{i j}
      | r = \sum_{k \mathop = 1}^n a_{i k} \circ r_{k j}
      | c = 
}}
{{eqn | l = r_{k j}
      | r = b_{k j} + c_{k j}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = s_{i j}
      | r = \sum_{k \mathop = 1}^n a_{i k} \circ \paren {b_{k j} + c_{k j} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n a_{i k} \circ b_{k j} + \sum_{k \mathop = 1}^n a_{i k} \circ c_{k j}
      | c = 
}}
{{eqn | r = g_{i j} + h_{i j}
      | c = 
}}
{{end-eqn}}
Thus:
:$\mathbf A \paren {\mathbf B + \mathbf C} = \paren {\mathbf A \mathbf B} + \paren {\mathbf A \mathbf C}$
A similar construction shows that:
:$\paren {\mathbf B + \mathbf C} \mathbf A = \paren {\mathbf B \mathbf A} + \paren {\mathbf C \mathbf A}$
{{Qed}}
Theorem: Unit Matrix is Unity of Ring of Square Matrices

Let $R$ be a ring with unity whose zero is $0_R$ and whose unity is $1_R$.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $\struct {\map {\MM_R} n, +, \times}$ denote the ring of square matrices of order $n$ over $R$.
The unit matrix over $R$:
:$\mathbf I_n = \begin {pmatrix} 1_R & 0_R & 0_R & \cdots & 0_R \\ 0_R & 1_R & 0_R & \cdots & 0_R \\ 0_R & 0_R & 1_R & \cdots & 0_R \\ \vdots & \vdots & \vdots & \ddots & \vdots \\ 0_R & 0_R & 0_R & \cdots & 1_R \end {pmatrix}$
is the identity element of $\struct {\map {\MM_R} n, +, \times}$.

Proof:
In Unit Matrix is Identity for Matrix Multiplication, it is demonstrated that:
:$\forall \mathbf A \in \map {\MM_R} n: \mathbf A \mathbf I_n = \mathbf A = \mathbf I_n \mathbf A$ 
Hence the result, by definition of identity element
{{qed}}
Theorem: Matrix Multiplication over Order n Square Matrices is Closed

Let $\struct {R, +, \circ}$ be a ring.
Let $\map {\MM_R} n$ be a $n \times n$ matrix space over $R$.
Then matrix multiplication (conventional) over $\map {\MM_R} n$ is closed.

Proof:
From the definition of matrix multiplication, the product of two matrices is another matrix.
The order of an $m \times n$ multiplied by an $n \times p$ matrix is $m \times p$.
The entries of that product matrix are elements of the ring over which the matrix is formed.
Thus an $n \times n$ matrix over $R$ multiplied by an $n \times n$ matrix over $R$ gives another $n \times n$ matrix over $R$.
Hence the result.
{{qed}}
Theorem: Square Matrices over Real Numbers under Multiplication form Monoid

Let $\map {\MM_\R} n$ be a $n \times n$ matrix space over the set of real numbers $\R$.
Then the set of all $n \times n$ real matrices $\map {\MM_\R} n$ under matrix multiplication (conventional) forms a monoid.

Proof:
:Matrix Multiplication over Order n Square Matrices is Closed.
:Matrix Multiplication is Associative.
:The Unit Matrix is Unity of Ring of Square Matrices.
{{qed}}