avewright/proofwiki-math huggingface dataset:
Theorem: Determinant of Elementary Row Matrix/Scale Row and Add

Let $e_2$ be the elementary row operation $\text {ERO} 2$:
{{begin-axiom}}
{{axiom | n = \text {ERO} 2
        | t = For some $\lambda$, add $\lambda$ times row $j$ to row $i$, where $i \neq j$
        | m = r_i \to r_i + \lambda r_j
}}
{{end-axiom}}
which is to operate on some arbitrary matrix space.
Let $\mathbf E_2$ be the elementary row matrix corresponding to $e_2$.
The determinant of $\mathbf E_2$ is:
:$\map \det {\mathbf E_2} = 1$

Proof:
By Elementary Matrix corresponding to Elementary Row Operation: Scale Row and Add, $\mathbf E_2$ is of the form:
:$E_{a b} = \delta_{a b} + \lambda \cdot \delta_{a i} \cdot \delta_{j b}$
where:
:$E_{a b}$ denotes the element of $\mathbf E$ whose indices are $\tuple {a, b}$
:$\delta_{a b}$ is the Kronecker delta:
::$\delta_{a b} = \begin {cases} 1 & : \text {if $a = b$} \\ 0 & : \text {if $a \ne b$} \end {cases}$
Because $i \ne j$ it follows that:
:if $a = i$ and $b = j$ then $a \ne b$
Hence when $a = b$ we have that:
:$\delta_{a i} \cdot \delta_{j b} = 0$
Hence the diagonal elements of $\mathbf E_2$ are all equal to $1$.
We also have that $\delta_{a i} \cdot \delta_{j b} = 1$ {{iff}} $a = i$ and $b = j$.
Hence, all elements of $\mathbf E_2$ apart from the diagonal elements and $a_{i j}$ are equal to $0$.
Thus $\mathbf E_2$ is a triangular matrix (either upper or lower).
From Determinant of Triangular Matrix, $\map \det {\mathbf E_2}$ is equal to the product of all the diagonal elements of $\mathbf E_2$.
But as we have seen, these are all equal to $1$.
Hence the result.
{{qed}}
Theorem: Determinant of Elementary Row Matrix/Exchange Rows

Let $e_3$ be the elementary row operation $\text {ERO} 3$:
{{begin-axiom}}
{{axiom | n = \text {ERO} 3
        | t = Exchange rows $i$ and $j$
        | m = r_i \leftrightarrow r_j
}}
{{end-axiom}}
which is to operate on some arbitrary matrix space.
Let $\mathbf E_3$ be the elementary row matrix corresponding to $e_3$.
The determinant of $\mathbf E_3$ is:
:$\map \det {\mathbf E_3} = -1$

Proof:
Let $\mathbf I$ denote the unit matrix of arbitrary order $n$.
By Determinant of Unit Matrix:
:$\map \det {\mathbf I} = 1$
Let $\rho$ be the permutation on $\tuple {1, 2, \ldots, n}$ which transposes $i$ and $j$.
From Parity of K-Cycle, $\map \sgn \rho = -1$.
By definition we have that $\mathbf E_3$ is $\mathbf I$ with rows $i$ and $j$ transposed.
By the definition of a determinant:
:$\ds \map \det {\mathbf I} = \sum_{\lambda} \paren {\map \sgn \lambda \prod_{k \mathop = 1}^n a_{k \map \lambda k} }$
By Permutation of Determinant Indices:
:$\ds \map \det {\mathbf E_3} = \sum_\lambda \paren {\map \sgn \rho \map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \rho k \map \lambda k} }$
We can take $\map \sgn \rho = -1$ outside the summation because it is constant, and so we get:
{{begin-eqn}}
{{eqn | l = \map \det {\mathbf E_3}
      | r = \map \sgn \rho \sum_\lambda \paren {\map \sgn \lambda \prod_{k \mathop = 1}^n a_{\map \rho k \map \lambda k} }
      | c = 
}}
{{eqn | r = -\sum_\lambda \paren {\map \sgn \lambda \prod_{k \mathop = 1}^n a_{k \map \lambda k} }
      | c = 
}}
{{eqn | r = -\map \det {\mathbf I}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Elementary Matrix corresponding to Elementary Column Operation/Scale Column

Let $e$ be the elementary column operation acting on $\mathbf I$ as:
{{begin-axiom}}
{{axiom | n = \text {ECO} 1
        | t = For some $\lambda \in K_{\ne 0}$, multiply column $k$ of $\mathbf I$ by $\lambda$
        | m = \kappa_k \to \lambda \kappa_k
}}
{{end-axiom}}

Proof:
By definition of the unit matrix:
:$I_{a b} = \delta_{a b}$
where:
:$I_{a b}$ denotes the element of $\mathbf I$ whose indices are $\tuple {a, b}$.
By definition, $\mathbf E$ is the square matrix of order $m$ formed by applying $e$ to the unit matrix $\mathbf I$.
That is, all elements of column $k$ of $\mathbf I$ are to be multiplied by $\lambda$.
By definition of unit matrix, all elements of column $k$ are $0$ except for element $I_{k k}$, which is $1$.
Thus in $\mathbf E$:
:$E_{k k} = \lambda \cdot 1 = \lambda$
The elements in all the other columns of $\mathbf E$ are the same as the corresponding elements of $\mathbf I$.
Hence the result.
{{qed}}
Category:Elementary Matrix corresponding to Elementary Column Operation
jb6yvslnfj0bla5ztd3536s3d31e4o2
Theorem: Elementary Matrix corresponding to Elementary Column Operation/Scale Column and Add

Let $e$ be the elementary column operation acting on $\mathbf I$ as:
{{begin-axiom}}
{{axiom | n = \text {ECO} 2
        | t = For some $\lambda \in K$, add $\lambda$ times column $j$ to row $i$
        | m = \kappa_i \to \kappa_i + \lambda r_j
}}
{{end-axiom}}

Proof:
By definition of the unit matrix:
:$I_{a b} = \delta_{a b}$
where:
:$I_{a b}$ denotes the element of $\mathbf I$ whose indices are $\tuple {a, b}$.
By definition, $\mathbf E$ is the square matrix of order $m$ formed by applying $e$ to the unit matrix $\mathbf I$.
That is, all elements of column $i$ of $\mathbf I$ are to have the corresponding elements of column $j$ added to them after the latter have been multiplied by $\lambda$.
By definition of unit matrix:
:all elements of column $i$ are $0$ except for element $I_{i i}$, which is $1$.
:all elements of column $j$ are $0$ except for element $I_{j j}$, which is $1$.
Thus in $\mathbf E$:
:where $b \ne i$, $E_{a b} = \delta_{a b}$
:where $b = i$:
::$E_{a b} = \delta_{a b}$ where $a \ne j$
::$E_{a b} = \delta_{a b} + \lambda \cdot 1$ where $a = j$
That is:
:$E_{a b} = \delta_{a b}$ for all elements of $\mathbf E$
except where $b = i$ and $a = j$, at which element:
:$E_{a b} = \delta_{a b} + \lambda$
That is:
:$E_{a b} = \delta_{a b} + \lambda \cdot \delta_{b i} \cdot \delta_{j a}$
Hence the result.
{{qed}}
Theorem: Elementary Matrix corresponding to Elementary Column Operation/Exchange Columns

Let $e$ be the elementary column operation acting on $\mathbf I$ as:
{{begin-axiom}}
{{axiom | n = \text {ECO} 3
        | t = Interchange columns $i$ and $j$
        | m = \kappa_i \leftrightarrow \kappa_j
}}
{{end-axiom}}

Proof:
By definition of the unit matrix:
:$I_{a b} = \delta_{a b}$
where:
:$I_{a b}$ denotes the element of $\mathbf I$ whose indices are $\tuple {a, b}$.
By definition, $\mathbf E$ is the square matrix of order $n$ formed by applying $e$ to the unit matrix $\mathbf I$.
That is, all elements of column $i$ of $\mathbf I$ are to be exchanged with the corresponding elements of column $j$.
By definition of unit matrix:
:all elements of column $i$ are $0$ except for element $I_{i i}$, which is $1$.
:all elements of column $j$ are $0$ except for element $I_{j j}$, which is $1$.
Thus in $\mathbf E$:
:where $a \ne i$ and $a \ne j$, $E_{a b} = \delta_{a b}$ (all columns except $i$ and $j$ are unchanged)
:where $a = i$, $E_{a b} = \delta_{a j}$ (the contents of column $j$)
:where $a = j$, $E_{a b} = \delta_{a i}$ (the contents of column $i$)
That is:
:$E_{a b} = \begin {cases} \delta_{a b} & : \text {if $b \ne i$ and $b \ne j$} \\ \delta_{a j} & : \text {if $b = i$} \\ \delta_{a i} & : \text {if $b = j$} \end {cases}$
Hence the result.
{{qed}}
Category:Elementary Matrix corresponding to Elementary Column Operation
3d6p4m50lbveddqbkwxoje3483kcrsf
Theorem: Column Equivalence is Equivalence Relation

Column equivalence is an equivalence relation.

Proof:
In the following, $\mathbf A$, $\mathbf B$ and $\mathbf C$ denote arbitrary matrices in a given matrix space $\map \MM {m, n}$ for $m, n \in \Z_{>0}$.
We check in turn each of the conditions for equivalence:
Theorem: Row Operation has Inverse

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\Gamma$ be a row operation which transforms $\mathbf A$ to a new matrix $\mathbf B \in \map \MM {m, n}$.
Then there exists another row operation $\Gamma'$ which transforms $\mathbf B$ back to $\mathbf A$.

Proof:
Let $\sequence {e_i}_{1 \mathop \le i \mathop \le k}$ be the finite sequence of elementary row operations that compose $\Gamma$.
Let $\sequence {\mathbf E_i}_{1 \mathop \le i \mathop \le k}$ be the corresponding finite sequence of the elementary row matrices.
From Row Operation is Equivalent to Pre-Multiplication by Product of Elementary Matrices, we have:
:$\mathbf R \mathbf A = \mathbf B$
where $\mathbf R$ is the product of $\sequence {\mathbf E_i}_{1 \mathop \le i \mathop \le k}$:
:$\mathbf R = \mathbf E_k \mathbf E_{k - 1} \dotsb \mathbf E_2 \mathbf E_1$
By Elementary Row Matrix is Nonsingular, each of $\mathbf E_i$ is nonsingular.
By Product of Matrices is Nonsingular iff Matrices are Nonsingular, it follows that $\mathbf R$ is likewise nonsingular.
Thus $\mathbf R$ has an inverse $\mathbf R^{-1}$.
Hence:
{{begin-eqn}}
{{eqn | l = \mathbf R \mathbf A
      | r = \mathbf B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf R^{-1} \mathbf R \mathbf A
      | r = \mathbf R^{-1} \mathbf B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf A
      | r = \mathbf R^{-1} \mathbf B
      | c = 
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | l = \mathbf R^{-1}
      | r = \paren {\mathbf E_k \mathbf E_{k - 1} \dotsb \mathbf E_2 \mathbf E_1}^{-1}
      | c = 
}}
{{eqn | r = {\mathbf E_1}^{-1} {\mathbf E_2}^{-1} \dotsb {\mathbf E_{k - 1} }^{-1} {\mathbf E_k}^{-1}
      | c = Inverse of Matrix Product
}}
{{end-eqn}}
From Elementary Row Matrix for Inverse of Elementary Row Operation is Inverse, each of ${\mathbf E_i}^{-1}$ is the elementary row matrix corresponding to the inverse $e'_i$ of the corresponding elementary row operation $e_i$.
Let $\Gamma'$ be the row operation composed of the finite sequence of elementary row operations $\tuple {e'_k, e'_{k - 1}, \ldots, e'_2, e'_1}$.
Thus $\Gamma'$ is a row operation which transforms $\mathbf B$ into $\mathbf A$.
Hence the result.
{{qed}}
Theorem: Real Numbers with Absolute Value form Normed Vector Space

Let $\R$ be the set of real numbers.
Let $\size {\, \cdot \,}$ be the absolute value.
Then $\struct {\R, \size {\, \cdot \,}}$ is a normed vector space.

Proof:
We have that:
:Real Numbers form Vector Space
:Absolute Value is Norm
By definition, $\struct {\R, \size {\, \cdot \,}}$ is a normed vector space.
{{qed}}
Theorem: Finite Dimensional Real Vector Space with Euclidean Norm form Normed Vector Space

Let $\R^n$ be an $n$-dimensional real vector space.
Let $\norm {\, \cdot \,}_2$ be the Euclidean norm.
Then $\struct {\R^n, \norm {\, \cdot \,}_2}$ is a normed vector space.

Proof:
We have that:
:Real Vector Space is Vector Space
:By Euclidean Space is Normed Vector Space, $\norm {\, \cdot \,}_2$ is a norm on $\R^n$
By definition, $\struct {\R^n, \norm {\, \cdot \,}_2}$ is a normed vector space.
{{qed}}
Theorem: Row Operation is Equivalent to Pre-Multiplication by Product of Elementary Matrices

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\Gamma$ be a row operation which transforms $\mathbf A$ to a new matrix $\mathbf B \in \map \MM {m, n}$.
Then there exists a unique nonsingular square matrix $\mathbf R$ of order $m$ such that:
:$\mathbf R \mathbf A = \mathbf B$
where $\mathbf R$ is the product of a finite sequence of elementary row matrices.

Proof:
The proof proceeds by induction.
By definition, $\Gamma$ is a finite sequence of elementary row operations on $\mathbf A$.
Let $\sequence e_k$ denote a finite sequence of elementary row operations $\tuple {e_1, e_2, \ldots, e_k}$ applied on $\mathbf A$ in order: first $e_1$, then $e_2$, then $\ldots$, then $e_k$.
Let $\Gamma_k$ be the row operation which consists of $\sequence e_k$.
Let $\mathbf E_k$ denote the elementary row matrix of order $m$ formed by applying $e_k$ to the unit matrix $I_m$.
For all $r \in \Z_{>0}$, let $\map P r$ be the proposition:
:For all $\Gamma_r$, there exists a unique nonsingular square matrix $\mathbf R_r$ of order $m$ such that:
::$\mathbf R_r \mathbf A = \mathbf B_r$
:where:
::$\Gamma_r$ is a row operation which transforms $\mathbf A$ to a new matrix $\mathbf B_r \in \map \MM {m, n}$.
::$\mathbf R_r$ is the product of the finite sequence of elementary row matrices:
:::$\mathbf R_r = \mathbf E_r \mathbf E_{r - 1} \dotsb \mathbf E_2 \mathbf E_1$
Theorem: Product of Matrices is Nonsingular iff Matrices are Nonsingular

Let $\mathbf A$ and $\mathbf B$ be square matrices of order $n$.
Let $\mathbf A \mathbf B$ denote the matrix product of $\mathbf A$ and $\mathbf B$.
Then:
:$\mathbf A \mathbf B$ is nonsingular
{{iff}}
:both $\mathbf A$ and $\mathbf B$ are nonsingular.

Proof:
=== Necessary Condition ===
Let both $\mathbf A$ and $\mathbf B$ be nonsingular.
By Matrix is Nonsingular iff Determinant has Multiplicative Inverse:
:$\map \det {\mathbf A} \ne 0$ and $\map \det {\mathbf B} \ne 0$
where $\map \det {\mathbf A}$ denotes the determinant of $\mathbf A$.
By Determinant of Matrix Product:
:$\map \det {\mathbf A} \map \det {\mathbf B} = \map \det {\mathbf A \mathbf B}$
Thus as both $\map \det {\mathbf A} \ne 0$ and $\map \det {\mathbf B} \ne 0$, it follows that:
:$\map \det {\mathbf A \mathbf B} \ne 0$
Hence by Matrix is Nonsingular iff Determinant has Multiplicative Inverse, $\mathbf A \mathbf B$ is nonsingular.
Theorem: Elementary Row Matrix is Nonsingular

Let $\mathbf E$ be an elementary row matrix.
Then $\mathbf E$ is nonsingular.

Proof:
From Elementary Row Matrix for Inverse of Elementary Row Operation is Inverse it is demonstrated that:
:if $\mathbf E$ is the elementary row matrix corresponding to an elementary row operation $e$
then:
:the inverse of $e$ corresponds to an elementary row matrix which is the inverse of $\mathbf E$.
So as $\mathbf E$ has an inverse, {{afortiori}} it is nonsingular.
{{qed}}
Theorem: Existence of Inverse Elementary Column Operation

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\map e {\mathbf A}$ be an elementary column operation which transforms $\mathbf A$ to a new matrix $\mathbf A' \in \map \MM {m, n}$.
Let $\map {e'} {\mathbf A'}$ be the inverse of $e$.
Then $e'$ is an elementary column operation which always exists and is unique.

Proof:
Let us take each type of elementary column operation in turn.
For each $\map e {\mathbf A}$, we will construct $\map {e'} {\mathbf A'}$ which will transform $\mathbf A'$ into a new matrix $\mathbf A' ' \in \map \MM {m, n}$, which will then be demonstrated to equal $\mathbf A$.
In the below, let:
:$\kappa_k$ denote column $k$ of $\mathbf A$
:$\kappa'_k$ denote column $k$ of $\mathbf A'$
:$\kappa' '_k$ denote column $k$ of $\mathbf A' '$
for arbitrary $k$ such that $1 \le k \le m$.
By definition of elementary column operation:
:only the column or columns directly operated on by $e$ is or are different between $\mathbf A$ and $\mathbf A'$
and similarly:
:only the column or columns directly operated on by $e'$ is or are different between $\mathbf A'$ and $\mathbf A' '$.
Hence it is understood that in the following, only those columns directly affected will be under consideration when showing that $\mathbf A = \mathbf A' '$.
Theorem: Column Operation has Inverse

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\Gamma$ be a column operation which transforms $\mathbf A$ to a new matrix $\mathbf B \in \map \MM {m, n}$.
Then there exists another column operation $\Gamma'$ which transforms $\mathbf B$ back to $\mathbf A$.

Proof:
Let $\sequence {e_i}_{1 \mathop \le i \mathop \le k}$ be the finite sequence of elementary column operations that compose $\Gamma$.
Let $\sequence {\mathbf E_i}_{1 \mathop \le i \mathop \le k}$ be the corresponding finite sequence of the elementary column matrices.
From Column Operation is Equivalent to Post-Multiplication by Product of Elementary Matrices, we have:
:$\mathbf A \mathbf K = \mathbf B$
where $\mathbf K$ is the product of $\sequence {\mathbf E_i}_{1 \mathop \le i \mathop \le k}$:
:$\mathbf K = \mathbf E_1 \mathbf E_2 \dotsb \mathbf E_{k - 1} \mathbf E_k$
By Elementary Column Matrix is Nonsingular, each of $\mathbf E_i$ is nonsingular.
By Product of Matrices is Nonsingular iff Matrices are Nonsingular, it follows that $\mathbf K$ is likewise nonsingular.
Thus $\mathbf K$ has an inverse $\mathbf K^{-1}$.
Hence:
{{begin-eqn}}
{{eqn | l = \mathbf A \mathbf K
      | r = \mathbf B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf A \mathbf K \mathbf K^{-1}
      | r = \mathbf B \mathbf K^{-1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf A
      | r = \mathbf B \mathbf K^{-1}
      | c = 
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | l = \mathbf K^{-1}
      | r = \paren {\mathbf E_1 \mathbf E_2 \dotsb \mathbf E_{k - 1} \mathbf E_k}^{-1}
      | c = 
}}
{{eqn | r = {\mathbf E_k}^{-1} {\mathbf E_{k - 1} }^{-1} \dotsb {\mathbf E_2}^{-1} {\mathbf E_1}^{-1}
      | c = Inverse of Matrix Product
}}
{{end-eqn}}
From Elementary Column Matrix for Inverse of Elementary Column Operation is Inverse, each of ${\mathbf E_i}^{-1}$ is the elementary column matrix corresponding to the inverse $e'_i$ of the corresponding elementary column operation $e_i$.
Let $\Gamma'$ be the column operation composed of the finite sequence of elementary column operations $\tuple {e'_k, e'_{k - 1}, \ldots, e'_2, e'_1}$.
Thus $\Gamma'$ is a column operation which transforms $\mathbf B$ into $\mathbf A$.
Hence the result.
{{qed}}
Theorem: Elementary Column Matrix is Nonsingular

Let $\mathbf E$ be an elementary column matrix.
Then $\mathbf E$ is nonsingular.

Proof:
From Elementary Column Matrix for Inverse of Elementary Column Operation is Inverse it is demonstrated that:
:if $\mathbf E$ is the elementary column matrix corresponding to an elementary column operation $e$
then:
:the inverse of $e$ corresponds to an elementary column matrix which is the inverse of $\mathbf E$.
So as $\mathbf E$ has an inverse, {{afortiori}} it is nonsingular.
{{qed}}
Theorem: Column Operation is Equivalent to Post-Multiplication by Product of Elementary Matrices

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\Gamma$ be a column operation which transforms $\mathbf A$ to a new matrix $\mathbf B \in \map \MM {m, n}$.
Then there exists a unique nonsingular square matrix $\mathbf K$ of order $n$ such that:
:$\mathbf A \mathbf K = \mathbf B$
where $\mathbf K$ is the product of a finite sequence of elementary column matrices.

Proof:
The proof proceeds by induction.
By definition, $\Gamma$ is a finite sequence of elementary column operations on $\mathbf A$.
Let $\sequence e_k$ denote a finite sequence of elementary column operations $\tuple {e_1, e_2, \ldots, e_k}$ applied on $\mathbf A$ in order: first $e_1$, then $e_2$, then $\ldots$, then $e_k$.
Let $\Gamma_k$ be the column operation which consists of $\sequence e_k$.
Let $\mathbf E_k$ denote the elementary column matrix of order $n$ formed by applying $e_k$ to the unit matrix $I_n$.
For all $r \in \Z_{>0}$, let $\map P r$ be the proposition:
:For all $\Gamma_r$, there exists a unique nonsingular square matrix $\mathbf K_r$ of order $n$ such that:
::$\mathbf A \mathbf K_r = \mathbf B_r$
:where:
::$\Gamma_r$ is a column operation which transforms $\mathbf A$ to a new matrix $\mathbf B_r \in \map \MM {m, n}$.
::$\mathbf K_r$ is the product of the finite sequence of elementary column matrices:
:::$\mathbf K_r = \mathbf E_1 \mathbf E_2 \dotsb \mathbf E_{r - 1} \mathbf E_r$
Theorem: Existence of Inverse Elementary Row Operation/Scalar Product of Row

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\map e {\mathbf A}$ be the elementary row operation which transforms $\mathbf A$ to a new matrix $\mathbf A' \in \map \MM {m, n}$.
{{begin-axiom}}
{{axiom | n = \text {ERO} 1
        | t = For some $\lambda \in K_{\ne 0}$, multiply row $i$ by $\lambda$
        | m = r_i \to \lambda r_i
}}
{{end-axiom}}
Let $\map {e'} {\mathbf A'}$ be the inverse of $e$.
Then $e'$ is the elementary row operation:
:$e' := r_i \to \dfrac 1 \lambda r_i$

Proof:
Let $\map e {\mathbf A}$ be the elementary row operation:
:$e := r_k \to \lambda r_k$
where $\lambda \ne 0$.
Then $r'_k$ is such that:
:$\forall a'_{k i} \in r'_k: a'_{k i} = \lambda a_{k i}$
Now let $\map {e'} {\mathbf A'}$ be the elementary row operation which transforms $\mathbf A'$ to $\mathbf A' '$:
:$e' := r_k \to \dfrac 1 \lambda r_k$
Because it is stipulated in the definition of an elementary row operation that $\lambda \ne 0$, it follows by definition of a field that $\dfrac 1 \lambda$ exists.
Hence $e'$ is defined.
So applying $e'$ to $\mathbf A'$ we get:
{{begin-eqn}}
{{eqn | q = \forall a' '_{k i} \in r' '_k
      | l = a' '_{k i}
      | r = \dfrac 1 \lambda a'_{k i}
      | c = 
}}
{{eqn | r = \dfrac 1 \lambda \paren {\lambda a_{k i} }
      | c = 
}}
{{eqn | r = a_{k i}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall a' '_{k i} \in r' '_k
      | l = a' '_{k i}
      | r = a_{k i}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r' '_k
      | r = r_k
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf A' '
      | r = \mathbf A
      | c = 
}}
{{end-eqn}}
It is noted that for $e'$ to be an elementary row operation, the only possibility is for it to be as defined.
Theorem: Existence of Inverse Elementary Row Operation/Add Scalar Product of Row to Another

Let $\map \MM {m, n}$ be a metric space of order $m \times n$ over a field $K$.
Let $\mathbf A \in \map \MM {m, n}$ be a matrix. 
Let $\map e {\mathbf A}$ be the elementary row operation which transforms $\mathbf A$ to a new matrix $\mathbf A' \in \map \MM {m, n}$.
{{begin-axiom}}
{{axiom | n = \text {ERO} 2
        | t = For some $\lambda \in K$, add $\lambda$ times row $k$ to row $l$
        | m = r_k \to r_k + \lambda r_l
}}
{{end-axiom}}
Let $\map {e'} {\mathbf A'}$ be the inverse of $e$.
Then $e'$ is the elementary row operation:
:$e' := r'_k \to r'_k - \lambda r'_l$

Proof:
Let $\map e {\mathbf A}$ be the elementary row operation:
:$e := r_k \to r_k + \lambda r_l$
Then $r'_k$ is such that:
:$\forall a'_{k i} \in r'_k: a'_{k i} = a_{k i} + \lambda a_{l i}$
Now let $\map {e'} {\mathbf A'}$ be the elementary row operation which transforms $\mathbf A'$ to $\mathbf A' '$:
:$e' := r'_k \to r'_k - \lambda r'_l$
Applying $e'$ to $\mathbf A'$ we get:
{{begin-eqn}}
{{eqn | q = \forall a' '_{k i} \in r' '_k
      | l = a' '_{k i}
      | r = a'_{k i} - \lambda a'_{l i}
      | c = 
}}
{{eqn | r = \paren {a_{k i} + \lambda a_{l i} } - \lambda a'_{l i}
      | c = 
}}
{{eqn | r = \paren {a_{k i} + \lambda a_{l i} } - \lambda a_{l i}
      | c = as $\lambda a'_{l i} = \lambda a_{l i}$: row $l$ was not changed by $e$
}}
{{eqn | r = a_{k i}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall a' '_{k i} \in r' '_k
      | l = a' '_{k i}
      | r = a_{k i}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r' '_{k i}
      | r = r_{k i}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf A' '
      | r = \mathbf A
      | c = 
}}
{{end-eqn}}
It is noted that for $e'$ to be an elementary row operation, the only possibility is for it to be as defined.