Toolkit for AL3

In the setting of Euclidean Space and Real Matrices: Standing Notation (Algebra) and Linear Algebra: Standing Notation: for classes $F$, $D$, $A$ and $B$, $F|_{D}$ is the restriction of $F$ to $D$, $A\times B$ the Cartesian product and $A\subseteq B$ the subclass relation. For predicative formulas $\varphi(x)$ and a class $A$, $\{x:\varphi(x)\}$ and $\{x\in A:\varphi(x)\}$ are formed by class abstraction and restricted class abstraction. For a set $X$ and $n\in\mathbb{N}_{0}$, $X^{n}$ is the set of $n$-tuples in $X$, with components $x_{k}$, and $[n]$ is the segment $\{1,\dots,n\}$. For a vector space $E$ over a field $K$, $\alpha_{E}:E\times E\to E$ and $\sigma_{E}:K\times E\to E$ denote its addition and its scalar multiplication as maps (Vector Space over a Field (ix)).

(i) Cyclicity of the trace. Let $p,q\in\mathbb{N}$, $U\in\mathcal{M}_{p\times q}(\mathbb{R})$ and $V\in\mathcal{M}_{q\times p}(\mathbb{R})$. Then $\operatorname{tr}(UV)=\operatorname{tr}(VU)$.

(ii) Associativity of the matrix product. Let $m,n,p,q\in\mathbb{N}$, $A\in\mathcal{M}_{m\times n}(\mathbb{R})$, $B\in\mathcal{M}_{n\times p}(\mathbb{R})$ and $C\in\mathcal{M}_{p\times q}(\mathbb{R})$. Then $(AB)C=A(BC)$.

(iii) The identity matrix on the left. Let $n,p\in\mathbb{N}$ and $A\in\mathcal{M}_{n\times p}(\mathbb{R})$. Then $I_{n}A=A$.

(iv) Scalars in the second argument of the dot product. Let $n\in\mathbb{N}$, $x,y\in\mathbb{R}^{n}$ and $t\in\mathbb{R}$. Then $x\cdot(ty)=t\,(x\cdot y)$.

(v) The semidefinite ordering through the quadratic form. Let $n\in\mathbb{N}$ and let $A,B\in\mathcal{M}_{n}(\mathbb{R})$. Then $A$ and $B$ satisfy the condition that defines $A\preceq B$ in The Positive Semidefinite Ordering on Symmetric Matrices (i) if and only if

$$z\cdot(Az)\le z\cdot(Bz)\qquad\text{for every }z\in\mathbb{R}^{n}.$$

(vi) Equal restricted abstractions. Let $A$ and $B$ be classes and let $\varphi(x)$ and $\psi(x)$ be predicative formulas such that, for every set $x$, $x\in A$ if and only if $x\in B$, and, if $x\in A$, $\varphi(x)$ if and only if $\psi(x)$. Then $\{x\in A:\varphi(x)\}=\{x\in B:\psi(x)\}$.

(vii) Equal abstractions. Let $\varphi(x)$ and $\psi(x)$ be predicative formulas such that $\varphi(s)$ if and only if $\psi(s)$, for every set $s$. Then $\{x:\varphi(x)\}=\{x:\psi(x)\}$.

(viii) Equality of vector spaces. Let $K$ be a field, and let $E$ and $E'$ be vector spaces over $K$ with the same set of vectors, such that $u+w$ formed in $E$ equals $u+w$ formed in $E'$ for all $u,w\in E$, and $\lambda w$ formed in $E$ equals $\lambda w$ formed in $E'$ for all $\lambda\in K$ and $w\in E$. Then $E$ and $E'$ are the same vector space.

(ix) A vector space formed from its own data. Let $K$ be a field, and let $U$ be a vector space over $K$ with set of vectors $W$, addition $a$ and scalar multiplication $s$. Then $W$, with the addition $a$ and the scalar multiplication $s$, satisfies the conditions of Vector Space over a Field (ix), and the vector space over $K$ it forms is $U$.

(x) Values of a map restricted on a product. Let $R$, $M$ and $S$ be classes with $S\subseteq M$, let $s:R\times M\to M$ be a map, and let $t\in R$ and $w\in S$. Then

$$(s|_{R\times S})((t,w))=s((t,w)).$$

(xi) Operations of a space with restricted operations. Let $K$ be a field, let $E$ and $U$ be vector spaces over $K$, and let $W\subseteq E$ be a class such that $U$ has set of vectors $W$, addition $\alpha_{E}|_{W\times W}$ and scalar multiplication $\sigma_{E}|_{K\times W}$. Then $u+w$ formed in $U$ equals $u+w$ formed in $E$ for all $u,w\in U$, and $\lambda w$ formed in $U$ equals $\lambda w$ formed in $E$ for all $\lambda\in K$ and $w\in U$.

(xii) Uniqueness of a space with restricted operations. Let $K$ be a field, let $E$, $U$ and $N$ be vector spaces over $K$, and let $W\subseteq E$ be a class such that $U$ has set of vectors $W$, addition $\alpha_{E}|_{W\times W}$ and scalar multiplication $\sigma_{E}|_{K\times W}$. Suppose that $N$ has set of vectors $W$, that $u+w$ formed in $N$ equals $u+w$ formed in $E$ for all $u,w\in N$, and that $\lambda w$ formed in $N$ equals $\lambda w$ formed in $E$ for all $\lambda\in K$ and $w\in N$. Then $N=U$.

(xiii) Uniqueness of $\mathbb{R}^{k}$ as a real vector space. Let $k\in\mathbb{N}$, and let $E$ and $E'$ be real vector spaces whose set of vectors is $\mathbb{R}^{k}$, whose sum of $x$ and $y$ is the sum $x+y$ of $\mathbb{R}^{k}$, and whose scalar multiple of $x$ by $t$ is the scalar multiple $tx$ of $\mathbb{R}^{k}$, for all $x,y\in\mathbb{R}^{k}$ and $t\in\mathbb{R}$. Then $E=E'$.

(xiv) A larger number is not at most a smaller one. Let $m,n\in\mathbb{N}_{0}$ with $m<n$. Then $n\le m$ does not hold.

(xv) Splitting the segment $[m+p]$. Let $m,p\in\mathbb{N}_{0}$ and $i\in[m+p]$. Then $i\in[m]$, or $i=m+j$ for some $j\in[p]$.

(xvi) Concatenation of tuples. Let $X$ be a set, let $m,p\in\mathbb{N}_{0}$, and let $u\in X^{m}$ and $w\in X^{p}$. Then there is $c\in X^{m+p}$ with

$$c_{i}=u_{i}\quad(i\in[m]),\qquad c_{m+j}=w_{j}\quad(j\in[p]).$$

(xvii) Linear combinations of a concatenation. Let $K$ be a field, let $E$ be a vector space over $K$, let $m,p\in\mathbb{N}_{0}$, let $u\in E^{m}$, $w\in E^{p}$ and $c\in E^{m+p}$ with $c_{i}=u_{i}$ for $i\in[m]$ and $c_{m+j}=w_{j}$ for $j\in[p]$, and let $\lambda\in K^{m+p}$. Then there are $a\in K^{m}$ and $b\in K^{p}$ with $a_{i}=\lambda_{i}$ for $i\in[m]$ and $b_{j}=\lambda_{m+j}$ for $j\in[p]$, and

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

(xviii) Negatives of linear combinations. Let $K$ be a field, let $E$ be a vector space over $K$, let $n\in\mathbb{N}_{0}$, $w\in E^{n}$ and $b\in K^{n}$. Then there is $b'\in K^{n}$ with

$$\sum_{i=1}^{n}b'_{i}w_{i}=-\sum_{i=1}^{n}b_{i}w_{i}.$$

(xix) A summand of zero is a negative. Let $K$ be a field, let $E$ be a vector space over $K$, and let $x,y\in E$ with $x+y=0_{E}$. Then $x=-y$.

(xx) The zero vector on the left. Let $K$ be a field, let $E$ be a vector space over $K$, and let $y\in E$. Then $0_{E}+y=y$.

(xxi) Quadratic forms in orthogonal coordinates. Let $n\in\mathbb{N}$, let $Q\in\mathrm{O}(n)$, let $c,\xi\in\mathbb{R}^{n}$, and let $\eta=Q^{\top}\xi$. Then

$$\xi\cdot\bigl(((Q\operatorname{diag}(c))Q^{\top})\xi\bigr)=\sum_{k=1}^{n}c_{k}\eta_{k}^{2}.$$

(xxii) Norms in orthogonal coordinates. Let $n\in\mathbb{N}$, let $Q\in\mathrm{O}(n)$, let $\xi\in\mathbb{R}^{n}$, and let $\eta=Q^{\top}\xi$. Then

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