Proof of A Homogeneous Linear System with More Unknowns than Equations Has a Nonzero Solution

Each result cited is universally quantified over the data in its own statement. $\mathbb{R}$ is the ordered field of the setting of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces, sums are as in Sums and Products over a Finite Set and over an Interval §sums, and negatives and differences in $\mathbb{R}$ as in Negatives, Differences, Reciprocals and Quotients §negative. For $p\in\mathbb{N}$ and $u\in\mathbb{R}^{p}$, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §equality and Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §origin, $u=0$ if and only if $u_{j}=0$ for every $j\in[p]$; so $u\neq0$ if and only if $u_{j}\neq0$ for some $j\in[p]$.

Step 1 (a zero first column). Let $m,n\in\mathbb{N}$ and $A\in\mathcal{M}_{m\times n}(\mathbb{R})$ with $A_{i1}=0$ for every $i\in[m]$; here $1\in[n]$ by Arithmetic and Order of the Natural Numbers §least. For the standard basis vector $e_{1}\in\mathbb{R}^{n}$ of Identity Matrix and Standard Basis Vectors §basis, Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes §column gives $(Ae_{1})_{i}=A_{i1}=0$ for every $i\in[m]$, so $Ae_{1}=0$; and $(e_{1})_{1}=\delta_{11}=1\neq0$ by Identity Matrix and Standard Basis Vectors §identity, so $e_{1}\neq0$.

Step 2 (eliminating the first unknown). Let $m,n'\in\mathbb{N}$, $n=n'+1$, $A\in\mathcal{M}_{m\times n}(\mathbb{R})$ and $r\in[m]$ with $A_{r1}\neq0$, and let $c$ be the reciprocal $A_{r1}^{-1}$ of $A_{r1}\neq0$ in the field $\mathbb{R}$, by Negatives, Differences, Reciprocals and Quotients §reciprocal, so $A_{r1}c=1$. By Bijections between Intervals: the Gap Map and the Reversal §gap (with $n'$ for $n$ and $j=1$), $g_{1}$ is a bijection from $[n']$ onto $[n]\setminus\{1\}$; by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse its inverse is a map $h:[n]\setminus\{1\}\to[n']$, and $h(g_{1}(k))=k$ for $k\in[n']$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §injective-inverse, $g_{1}$ being injective. Let $y\in\mathbb{R}^{n'}$, for $i\in[m]$ put $S_{i}=\sum_{k=1}^{n'}A_{i,g_{1}(k)}y_{k}$, and let $t=-(c\,S_{r})$. By Maps Defined by Cases §cases, on the set $[n]$ with the predicative property $j=1$ and the expressions $t$ and $y(h(j))$ (the latter used properly for $j\neq1$, since then $j\in[n]\setminus\{1\}$), there is exactly one map $x:[n]\to\mathbb{R}$ with $x_{1}=t$ and $x_{j}=y_{h(j)}$ for $j\in[n]$, $j\neq1$. Thus $x\in\mathbb{R}^{n}$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership, and $x_{g_{1}(k)}=y_{k}$ for $k\in[n']$, as $g_{1}(k)\neq1$. By Matrix-Vector Product §product and Iterated Operations over an Interval: Extracting One Term and Reversing the Order §extraction (with $n'$ for $n$, $j=1$, and the terms $A_{ij}x_{j}$), for every $i\in[m]$,

$$(\ast)\qquad (Ax)_{i}=S_{i}+A_{i1}t=S_{i}-(A_{i1}c)S_{r},$$

the last step by Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs and the difference of Negatives, Differences, Reciprocals and Quotients §negative. (i) For $i=r$, $(\ast)$ and $A_{r1}c=1$ give $(Ax)_{r}=S_{r}-S_{r}=0$.

(ii) If $y\neq0$, say $y_{k}\neq0$ with $k\in[n']$, then $x_{g_{1}(k)}=y_{k}\neq0$, so $x\neq0$.

(iii) Let moreover $m=m'+1$ with $m'\in\mathbb{N}$. By Bijections between Intervals: the Gap Map and the Reversal §gap, $g_{r}$ is a bijection from $[m']$ onto $[m]\setminus\{r\}$. By Maps and Relations Given by Formulas §binary, there is exactly one map $A':[m']\times[n']\to\mathbb{R}$, that is, $A'\in\mathcal{M}_{m'\times n'}(\mathbb{R})$, with

$$A'_{i'k}=A_{g_{r}(i'),g_{1}(k)}-A_{g_{r}(i'),1}\,c\,A_{r,g_{1}(k)}\qquad(i'\in[m'],\ k\in[n'])$$

($g_{r}(i')\in[m]$ and $g_{1}(k)\in[n]$ by Bijections between Intervals: the Gap Map and the Reversal §gap, so these entries exist; $A'_{i'k}=A'((i',k))$ by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §entries). For $i'\in[m']$ and $i=g_{r}(i')$, $(\ast)$, Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §distributive (for the commutative ring $\mathbb{R}$) and Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §difference give $(Ax)_{i}=\sum_{k=1}^{n'}\bigl(A_{i,g_{1}(k)}y_{k}-A_{i1}cA_{r,g_{1}(k)}y_{k}\bigr)=\sum_{k=1}^{n'}A'_{i'k}y_{k}=(A'y)_{i'}$, the second equality termwise by the rule $(x-y)z=xz-yz$ of Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §signs, the last by Matrix-Vector Product §product.

Step 3 (the class for the induction). For $m\in\mathbb{N}$ let $P(m)$ be the statement: for every $n\in\mathbb{N}$ with $m<n$ and every $A\in\mathbb{R}^{[m]\times[n]}$ there is $x\in\mathbb{R}^{[n]}$ with $x(j)\neq0$ for some $j\in[n]$ such that, for every $i\in[m]$ and every map $a:[n]\to\mathbb{R}$ with $a(j)=A((i,j))\cdot x(j)$ for all $j\in[n]$, $\sum_{k=1}^{n}a_{k}=0$. For given $A$, $x$ and $i$ exactly one such map $a$ exists, by Maps and Relations Given by Formulas §map; hence, by Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §matrices, Real Matrices: the Set of Real m x n Matrices with Their Entrywise Operations §entries, Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §space, Matrix-Vector Product §product and the description of $u\neq0$ above, $P(m)$ says exactly that the lemma holds for this $m$ and all $n$ and $A$. Written out, $P(m)$ quantifies over the sets $n$, $A$, $x$, $i$, $j$ and $a$ only: the condition that $a$ is a map $[n]\to\mathbb{R}$ is predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §map; the values $A((i,j))$, $x(j)$, $a(j)$ and the product in $\mathbb{R}$ enter predicatively by Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field §value-substitution and Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field §operation-substitution, applied successively for the nested term $A((i,j))\cdot x(j)$, first to the product and then to its operands (equivalently, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination); and $\sum_{k=1}^{n}a_{k}=0$ is $\exists w\,(\mathrm{it}(w,n,a)\wedge w=0)$ with the predicative formula $\mathrm{it}$ of Iterated Operations Are Given by a Predicative Formula §predicative for the addition of $\mathbb{R}$ (the sum over $\{1,\dots,n\}$ agreeing with the iterated operation by Sums and Products over a Finite Set and over an Interval §intervals), its parameters being $\mathbb{R}$, the addition of $\mathbb{R}$, $\mathbb{N}$ and the order and addition of $\mathbb{N}_{0}$. The remaining symbols ($[m]$, $[n]$, $[m]\times[n]$, $\mathbb{R}^{[m]\times[n]}$, $\mathbb{R}^{[n]}$, $0$, $<$) are defined set symbols or class terms used properly. So $P(m)$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, and The Class Comprehension Theorem for Predicative Formulas §comprehension gives a class $Z$ such that, for every set $m$, $m\in Z$ if and only if $m\in\mathbb{N}$ and $P(m)$. Then $Z\subseteq\mathbb{N}$.

In Steps 4 and 5, $n\in\mathbb{N}$ is given with $\ell<n$, where $\ell=1$ in Step 4 and $\ell=m+1$ in Step 5. As $1\le\ell$ by Arithmetic and Order of the Natural Numbers §least, Arithmetic and Order of the Natural Numbers §partial-order gives $1<n$, so $n\neq1$ by Arithmetic and Order of the Natural Numbers §trichotomy, and $n=n'+1$ for some $n'\in\mathbb{N}$ by Arithmetic and Order of the Natural Numbers §predecessor.

Step 4 ($1\in Z$). Let $m=1$ and $A\in\mathcal{M}_{1\times n}(\mathbb{R})$. Here $[1]=\{1\}$, by Arithmetic and Order of the Natural Numbers §partial-order. If $A_{11}=0$, Step 1 gives $x=e_{1}$. Otherwise take $r=1$ and, in Step 2, $y=e_{1}\in\mathbb{R}^{n'}$, which is nonzero as in Step 1 ($1\in[n']$ by Arithmetic and Order of the Natural Numbers §least); the resulting $x\in\mathbb{R}^{n}$ satisfies $x\neq0$ by (ii) and $(Ax)_{1}=0$ by (i), so $Ax=0$ as $[1]=\{1\}$. Hence $P(1)$, and $1\in Z$.

Step 5 ($m\in Z$ implies $m+1\in Z$). Let $m\in Z$, now with $m+1<n$, and let $A\in\mathcal{M}_{(m+1)\times n}(\mathbb{R})$. From $m+1<n'+1$, Arithmetic and Order of the Natural Numbers §order gives $m<n'$. If $A_{i1}=0$ for every $i\in[m+1]$, Step 1 gives $x=e_{1}$. Otherwise choose $r\in[m+1]$ with $A_{r1}\neq0$ and form $A'\in\mathcal{M}_{m\times n'}(\mathbb{R})$ as in (iii), with $m'=m$. Since $m\in Z$ and $m<n'$, $P(m)$ gives $y\in\mathbb{R}^{n'}$ with $y\neq0$ and $A'y=0$. Let $x$ be the point of Step 2 for this $y$. Then $x\neq0$ by (ii); $(Ax)_{r}=0$ by (i); and $(Ax)_{g_{r}(i')}=(A'y)_{i'}=0$ for every $i'\in[m]$ by (iii), where $g_{r}(i')\in[m+1]$ by Bijections between Intervals: the Gap Map and the Reversal §gap. As $g_{r}$ maps $[m]$ onto $[m+1]\setminus\{r\}$, every $i\in[m+1]$ is $r$ or $g_{r}(i')$ for some $i'\in[m]$, so $(Ax)_{i}=0$ for every $i\in[m+1]$ and $Ax=0$. Hence $P(m+1)$, and $m+1\in Z$.

By Steps 4 and 5, Arithmetic and Order of the Natural Numbers §induction gives $Z=\mathbb{N}$. For the given $m<n$ and $A$, $P(m)$ yields $x\in\mathbb{R}^{n}$ with $x\neq0$ and $Ax=0$, as claimed.