Proof of Toolkit for AL3

Routine facts about maps, natural numbers, real numbers and predicative formulas are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (vi)). Several results cited below on matrices and points of $\mathbb{R}^{n}$ are stated for earlier versions of the definitions; the sets $\mathbb{R}^{n}$ and $\mathcal{M}_{m\times n}(\mathbb{R})$ and their operations are the same in both versions by The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (i) and The Earlier and the New Versions of the Definitions of Euclidean Space, Real Matrices and Normed Spaces Agree (ii), and the further notions agree by the clauses of The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree named at each use.

Proof of (i). By Basic Properties of the Trace (iii), $\operatorname{tr}(UV)=\operatorname{tr}(VU)$ for the product and the trace of the earlier versions. These are the product and the trace of the current versions by The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (vi) and The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (viii).

Proof of (ii). By Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (i), $(AB)C=A(BC)$ for the product of the earlier version, which is the current product by The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (vi); this applies to each of the four products $AB$, $(AB)C$, $BC$ and $A(BC)$.

Proof of (iii). By Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (iv), applied with $n$ and $p$ in place of $m$ and $n$, $I_{n}A=A$ for the identity matrix and the product of the earlier versions. These are the current ones by The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (v) and The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (vi).

Proof of (iv). By The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite (iii), with $z=x$ and $y$ in place of $x$, $x\cdot(ty)=t\,(x\cdot y)$ for the dot product of the earlier version, which is the current one by The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (i); the scalar multiple $ty$ is the same in both versions.

Proof of (v). For $z\in\mathbb{R}^{n}$, $Az$ and $Bz$ lie in $\mathbb{R}^{n}$ (Matrix-Vector Product (i)), so $z\cdot(Az)$ and $z\cdot(Bz)$ are real numbers (The Dot Product on $\mathbb{R}^n$ (i)). The condition that defines $\preceq$ in The Positive Semidefinite Ordering on Symmetric Matrices (i), read for the arbitrary square matrices $A$ and $B$, is that $z\cdot(Az)\le z\cdot(Bz)$ for every $z\in\mathbb{R}^{n}$, with the order of $\mathbb{R}$; this is the asserted condition.

Proof of (vi). By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii), $\{x\in A:\varphi(x)\}=\{x:x\in A\wedge\varphi(x)\}$ and $\{x\in B:\psi(x)\}=\{x:x\in B\wedge\psi(x)\}$. For every set $x$, the conditions $x\in A\wedge\varphi(x)$ and $x\in B\wedge\psi(x)$ are equivalent: if $x\in A$ and $\varphi(x)$, then $x\in B$, and $\psi(x)$ as $x\in A$; if $x\in B$ and $\psi(x)$, then $x\in A$, and so $\varphi(x)$. The two classes are therefore equal by (vii).

Proof of (vii). By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), $\{x:\psi(x)\}$ is the unique class $Z$ such that, for every set $s$, $s\in Z$ if and only if $\psi(s)$. For every set $s$, $s\in\{x:\varphi(x)\}$ if and only if $\varphi(s)$, by the same clause, that is, if and only if $\psi(s)$. So $\{x:\varphi(x)\}$ has the property that characterizes $\{x:\psi(x)\}$, and the two classes are equal by the uniqueness in Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i).

Proof of (viii). Let $S$ be the common set of vectors. The additions $\alpha_{E}$ and $\alpha_{E'}$ are maps $S\times S\to S$, and every element of $S\times S$ is a pair $(u,w)$ with $u,w\in S$ (The Cartesian Product of Two Classes (i)), at which

$$\alpha_{E}((u,w))=u+w\ \text{(formed in }E)=u+w\ \text{(formed in }E')=\alpha_{E'}((u,w)).$$

So $\alpha_{E}=\alpha_{E'}$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii). Likewise $\sigma_{E}$ and $\sigma_{E'}$ are maps $K\times S\to S$ which agree at every pair $(\lambda,w)$ with $\lambda\in K$ and $w\in S$, so $\sigma_{E}=\sigma_{E'}$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii). A vector space over $K$ consists of its set with its addition and its scalar multiplication (Vector Space over a Field (ix)), and these coincide for $E$ and $E'$; hence $E$ and $E'$ are the same vector space.

Proof of (ix). As $U$ is a vector space over $K$, its set of vectors with its addition and its scalar multiplication satisfies the conditions of Vector Space over a Field (ix); by hypothesis these are $W$, $a$ and $s$. The vector space formed by $W$, $a$ and $s$ therefore has the same set of vectors, addition and scalar multiplication as $U$, and so it is $U$ (Vector Space over a Field (ix)).

Proof of (x). Since $t\in R$ and $w\in S\subseteq M$, the pair $(t,w)$ lies in $R\times S$ and in $R\times M$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (viii)). As $s:R\times M\to M$ is a map, Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (vi), applied to the class $R\times S$ and its element $(t,w)\in R\times M$, gives $(s|_{R\times S})((t,w))=s((t,w))$.

Proof of (xi). Let $u,w\in U$, that is, $u,w\in W$. The addition $\alpha_{E}$ is a binary operation on the set $E$ and $W\subseteq E$, so by Toolkit for AL1 (v)

$$u+w\ \text{(formed in }U)=(\alpha_{E}|_{W\times W})((u,w))=u+w\ \text{(formed in }E).$$

Let $\lambda\in K$ and $w\in W$. The scalar multiplication $\sigma_{E}:K\times E\to E$ is a map and $W\subseteq E$, so by (x), with $R=K$, $M=E$ and $S=W$,

$$\lambda w\ \text{(formed in }U)=(\sigma_{E}|_{K\times W})((\lambda,w))=\sigma_{E}((\lambda,w))=\lambda w\ \text{(formed in }E).$$

Proof of (xii). $N$ and $U$ both have the set of vectors $W$. For $u,w\in W$, $u+w$ formed in $N$ equals $u+w$ formed in $E$ by hypothesis, which equals $u+w$ formed in $U$ by (xi); likewise, for $\lambda\in K$ and $w\in W$, $\lambda w$ formed in $N$ equals $\lambda w$ formed in $E$, which equals $\lambda w$ formed in $U$ by (xi). Hence $N=U$ by (viii).

Proof of (xiii). $E$ and $E'$ are vector spaces over $\mathbb{R}$ (Vector Space over a Field (x)) with the same set of vectors $\mathbb{R}^{k}$. For $x,y\in\mathbb{R}^{k}$ the sums of $x$ and $y$ in $E$ and in $E'$ both equal $x+y$ in $\mathbb{R}^{k}$, and for $t\in\mathbb{R}$ the scalar multiples of $x$ by $t$ in $E$ and in $E'$ both equal $tx$ in $\mathbb{R}^{k}$. Hence $E=E'$ by (viii).

Proof of (xiv). By The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (ii), $m<n$ gives $m\le n$ and $m\neq n$. If also $n\le m$, then $m=n$ by antisymmetry (Order and Arithmetic of ℕ₀ in Flat Form (i)), a contradiction. So $n\le m$ does not hold.

Proof of (xv). If $m=0$, then $m+p=p$ (Order and Arithmetic of ℕ₀ in Flat Form (iii)), so $i\in[p]$ and $i=0+i$: the second alternative holds with $j=i$. If $p=0$, then $m+p=m$ (Order and Arithmetic of ℕ₀ in Flat Form (iii)), so $i\in[m]$. Otherwise $m$ and $p$ are nonzero elements of $\mathbb{N}_{0}$, hence natural numbers (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii)), and Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] (iii) shows that $i\in[m]$ or $i=m+j$ for some $j\in[p]$.

Proof of (xvi). First, two facts on segments, for $m,p\in\mathbb{N}_{0}$. Since $m\le m+p$ (Order and Arithmetic of ℕ₀ in Flat Form (i)), $[m]\subseteq[m+p]$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (v). Since $1\le m+1$, Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (iii) gives

$$\{1,\dots,m+p\}=\{1,\dots,m\}\cup\{m+1,\dots,m+p\},$$

the two intervals being disjoint, and by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (iv) the map $j\mapsto j+m$ sends $\{1,\dots,p\}$ into $\{1+m,\dots,p+m\}=\{m+1,\dots,m+p\}$. Hence, for every $j\in[p]$,

$$m+j\in[m+p]\qquad\text{and}\qquad m+j\notin[m].\tag{$\ast$}$$

Moreover $m+j=m+j'$ implies $j=j'$ (Order and Arithmetic of ℕ₀ in Flat Form (iv)).

Let $\psi(i,y)$ be the condition: $i\in[m]$ and $y=u_{i}$, or there is $j\in[p]$ with $i=m+j$ and $y=w_{j}$. By (xv), every $i\in[m+p]$ has some $y\in X$ with $\psi(i,y)$, as $u_{i},w_{j}\in X$ (Tuples in a Set: the Set of n-Tuples and Their Components (ii)). If $\psi(i,y)$ and $\psi(i,y')$, then $y=y'$: the first alternative for one and the second for the other would put some $m+j$ into $[m]$, contrary to $(\ast)$; two instances of the first give $y=u_{i}=y'$; and two instances $i=m+j$, $i=m+j'$ of the second give $j=j'$ by cancellation, so $y=w_{j}=y'$. The condition is predicative, so Maps from Functional Predicative Relations, and Families of Sections (ii) gives a map $c:[m+p]\to X$ with $\psi(i,c(i))$ for every $i\in[m+p]$, and $c\in X^{m+p}$ by Tuples in a Set: the Set of n-Tuples and Their Components (ii). For $i\in[m]$, the second alternative of $\psi(i,c_{i})$ is excluded by $(\ast)$, so $c_{i}=u_{i}$. For $j\in[p]$, $m+j\notin[m]$ by $(\ast)$, so $\psi(m+j,c_{m+j})$ holds by the second alternative, with some $j'\in[p]$ such that $m+j=m+j'$ and $c_{m+j}=w_{j'}$; then $j'=j$ and $c_{m+j}=w_{j}$.

Proof of (xvii). By Tuples in a Set: the Set of n-Tuples and Their Components (ii), $\lambda:[m+p]\to K$ is a map. Moreover $[m]\subseteq[m+p]$, and $m+j\in[m+p]$ for every $j\in[p]$. If $m$ and $p$ are nonzero, they are natural numbers (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii)), and this is Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] (i) and Splitting the Segment [m+n] into [m] and a Shifted Copy of [n] (ii). If $m=0$, then $[m]=\emptyset$ (Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i)), $m+j=j$ and $m+p=p$; if $p=0$, then $m+p=m$ and $[p]=\emptyset$ (Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i)); the sums with $0$ are evaluated by Order and Arithmetic of ℕ₀ in Flat Form (iii). Hence $a=\lambda|_{[m]}:[m]\to K$ is a map with $a_{i}=\lambda_{i}$ for $i\in[m]$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (vi)), so $a\in K^{m}$, and Maps from Functional Predicative Relations, and Families of Sections (ii) gives a map $b:[p]\to K$ with $b_{j}=\lambda_{m+j}$, so $b\in K^{p}$. Then $\lambda_{i}c_{i}=a_{i}u_{i}$ for $i\in[m]$ and $\lambda_{m+j}c_{m+j}=b_{j}w_{j}$ for $j\in[p]$. Sums of vectors are taken for the addition of $E$, which is associative and commutative with neutral element $0_{E}$ (Vector Space over a Field (i), Vector Space over a Field (ii), The Zero Vector, Negatives and Differences in a Vector Space (i)).

If $m,p\in\mathbb{N}$, Splitting an Operation over the Segment [m+n] into [m] and a Shifted Copy of [n] (ii), applied to the addition of $E$ and the map $k\mapsto\lambda_{k}c_{k}$ on $[m+p]$, gives

$$\sum_{k=1}^{m+p}\lambda_{k}c_{k}=\sum_{k=1}^{m}\lambda_{k}c_{k}+\sum_{j=1}^{p}\lambda_{m+j}c_{m+j}=\sum_{i=1}^{m}a_{i}u_{i}+\sum_{j=1}^{p}b_{j}w_{j},$$

the last step because the tuples of terms agree termwise and hence are equal (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii)). If $m=0$, then $m+p=p$, $\sum_{i=1}^{0}a_{i}u_{i}=0_{E}$ as an empty sum (Span of a Finite Family; Spanning Families (i)), and $\lambda_{k}c_{k}=\lambda_{0+k}c_{0+k}=b_{k}w_{k}$ for $k\in[p]$; so the left side is $\sum_{j=1}^{p}b_{j}w_{j}=0_{E}+\sum_{j=1}^{p}b_{j}w_{j}$ by (xx). If $p=0$, then $m+p=m$, $\sum_{j=1}^{0}b_{j}w_{j}=0_{E}$ (Span of a Finite Family; Spanning Families (i)), and $\lambda_{k}c_{k}=a_{k}u_{k}$ for $k\in[m]$; so the left side is $\sum_{i=1}^{m}a_{i}u_{i}=\sum_{i=1}^{m}a_{i}u_{i}+0_{E}$ by The Zero Vector, Negatives and Differences in a Vector Space (i).

Proof of (xviii). By Maps from Functional Predicative Relations, and Families of Sections (ii) there is $b'\in K^{n}$ with $b'_{i}=0-b_{i}$, the difference in $K$, for $i\in[n]$, and the constant $n$-tuple $o=[n]\times\{0\}$ lies in $K^{n}$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (vii)). By The Span of a Finite Family is the Smallest Subspace Containing It (i), applied to $w$ with the coefficients $o$ and $b$,

$$\sum_{i=1}^{n}b'_{i}w_{i}=\sum_{i=1}^{n}(0-b_{i})w_{i}=\sum_{i=1}^{n}0\,w_{i}-\sum_{i=1}^{n}b_{i}w_{i}=0_{E}-\sum_{i=1}^{n}b_{i}w_{i}.$$

By The Zero Vector, Negatives and Differences in a Vector Space (iii) the right side is $0_{E}+\bigl(-\sum_{i=1}^{n}b_{i}w_{i}\bigr)$, which is $-\sum_{i=1}^{n}b_{i}w_{i}$ by (xx).

Proof of (xix). By Vector Space over a Field (ii), $y+x=x+y=0_{E}$. By The Zero Vector, Negatives and Differences in a Vector Space (ii), $-y$ is the unique $w\in E$ with $y+w=0_{E}$; as $x$ is such a $w$, $x=-y$.

Proof of (xx). By Vector Space over a Field (ii) and The Zero Vector, Negatives and Differences in a Vector Space (i), $0_{E}+y=y+0_{E}=y$.

Proof of (xxi). Write $D=\operatorname{diag}(c)$, the same matrix in both versions by The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (xiii); the product, transpose, matrix-vector product and dot product also agree by The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (vi), The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (vii), The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (iv) and The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (i). By the rule $(AB)z=A(Bz)$ of Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (v), used twice,

$$((QD)Q^{\top})\xi=(QD)(Q^{\top}\xi)=(QD)\eta=Q(D\eta).$$

By The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite (i) and Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (viii), with $A=Q$, $x=D\eta$ and $w=\xi$,

$$\xi\cdot\bigl(Q(D\eta)\bigr)=\bigl(Q(D\eta)\bigr)\cdot\xi=(D\eta)\cdot(Q^{\top}\xi)=(D\eta)\cdot\eta=\eta\cdot(D\eta).$$

Finally $\eta\cdot(D\eta)=\sum_{k=1}^{n}c_{k}\eta_{k}^{2}$ by Eigenvalues: the Determinant Criterion, Diagonal Matrices, Orthogonal Similarity and Orthogonality of Eigenvectors of Symmetric Matrices (ii).

Proof of (xxii). The set $\mathrm{O}(n)$, the identity matrix, the product, the transpose, the matrix-vector product and the Euclidean norm agree in both versions by The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (xiv), The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (v), The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (vi), The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (vii), The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (iv) and The Earlier and the New Versions of the Definitions of the Dot Product, the Euclidean Norm and Distance, and the Matrix Operations Agree (ii). By Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion (i), $QQ^{\top}=I_{n}$, so by Algebraic Rules for Matrix Products, Matrix-Vector Products and Transposes (v)

$$Q\eta=Q(Q^{\top}\xi)=(QQ^{\top})\xi=I_{n}\xi=\xi.$$

By Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion (iii), $\lVert\xi\rVert=\lVert Q\eta\rVert=\lVert\eta\rVert$, and by Properties of the Euclidean Norm on $\mathbb{R}^n$: Square, Distance, Vanishing, Coordinate Bounds, Homogeneity, Triangle Inequalities and Expansion of a Square (i)

$$\lVert\xi\rVert^{2}=\lVert\eta\rVert^{2}=\sum_{k=1}^{n}\eta_{k}^{2}.$$