Proof of Kit for def:normed-space

Throughout, formulas are written with abbreviations and quantify over set variables only, so they are predicative. The parameters $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$ are variables other than $x_{0},x_{1},\dots$ and other than the bound variables below; $0$ and $1$ are sets, being elements of $\mathbb{R}$, and $+$, $\cdot$ and $\le$ are sets, as maps from $\mathbb{R}\times\mathbb{R}$ to $\mathbb{R}$ and a subclass of $\mathbb{R}\times\mathbb{R}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)). We first build formulas in the four set variables $x_{0},x_{1},x_{2},x_{3}$, written $V$, $a$, $s$ and $\nu$, and move them to the positions $i,j,k,l$ at the end. The letters $u,v,w,y,z,b,d,e,f,p,c,q,r,t,\lambda,\kappa$ denote further set variables.

The standing hypothesis. For variables $A$ and $B$ let $\pi(c,A,B)$ be the formula $\forall p\,\bigl(p\in c\Leftrightarrow\exists u\,\exists v\,(u\in A\wedge v\in B\wedge p=(u,v))\bigr)$. For sets $A$ and $B$, the only set $c$ with $\pi(c,A,B)$ is the Cartesian product $A\times B$, which is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii). Let $\mu(F,A,B)$ be the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), which holds exactly when $F$ is a map $F:A\to B$, and let

$$\tau=\exists c\,\bigl(\pi(c,V,V)\wedge\mu(a,c,V)\bigr)\wedge\exists c\,\bigl(\pi(c,\mathbb{R},V)\wedge\mu(s,c,V)\bigr)\wedge\mu(\nu,V,\mathbb{R}).$$

It holds exactly when $a$ is a binary operation on $V$, $s$ is a map $\mathbb{R}\times V\to V$, and $\nu$ is a map $V\to\mathbb{R}$. Assume $\tau$. For $u,v\in V$, $((u,v),w)\in a$ holds exactly for $w=u+v$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi); for $\lambda\in\mathbb{R}$ and $v\in V$, $((\lambda,v),w)\in s$ holds exactly for $w=\lambda v$, and for $v\in V$, $(v,y)\in\nu$ holds exactly for $y=\lVert v\rVert$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x), since $(\lambda,v)\in\mathbb{R}\times V$ (Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (i)) and the domains are $\mathbb{R}\times V$ and $V$ (Functions, Values of a Function, and Functions from One Class to Another (iii)); and for $r,t\in\mathbb{R}$, $((r,t),q)\in{+}$ and $((r,t),q)\in{\cdot}$ hold exactly for $q=r+t$ and $q=r\cdot t$, as $+$ and $\cdot$ are binary operations on $\mathbb{R}$. These values lie in $V$, $V$, $\mathbb{R}$ and $\mathbb{R}$. So in each formula below, every premise of these forms singles out exactly one set, which exists, and a universally quantified implication whose premises name values in this way states the property of the named values given in its conclusion.

Let $\zeta(z)$ be $z\in V\wedge\forall w\,\bigl(w\in V\Rightarrow((w,z),w)\in a\bigr)$; under $\tau$ it says that $z\in V$ and $w+z=w$ for every $w\in V$. Let $\varepsilon_{1},\dots,\varepsilon_{8}$ be the formulas

$$\begin{aligned} &\forall u\,\forall v\,\forall w\,\forall b\,\forall d\,\forall e\,\forall f\,\bigl((u\in V\wedge v\in V\wedge w\in V\wedge((u,v),b)\in a\wedge((b,w),d)\in a\wedge((v,w),e)\in a\wedge((u,e),f)\in a)\Rightarrow d=f\bigr),\\ &\forall u\,\forall v\,\forall b\,\forall d\,\bigl((u\in V\wedge v\in V\wedge((u,v),b)\in a\wedge((v,u),d)\in a)\Rightarrow b=d\bigr),\\ &\exists z\,\zeta(z),\\ &\forall v\,\forall z\,\bigl((v\in V\wedge\zeta(z))\Rightarrow\exists y\,(y\in V\wedge((v,y),z)\in a)\bigr),\\ &\forall\lambda\,\forall\kappa\,\forall v\,\forall b\,\forall d\,\forall e\,\bigl((\lambda\in\mathbb{R}\wedge\kappa\in\mathbb{R}\wedge v\in V\wedge((\kappa,v),b)\in s\wedge((\lambda,b),d)\in s\wedge((\lambda,\kappa),e)\in{\cdot})\Rightarrow((e,v),d)\in s\bigr),\\ &\forall v\,\bigl(v\in V\Rightarrow((1,v),v)\in s\bigr),\\ &\forall\lambda\,\forall u\,\forall v\,\forall b\,\forall d\,\forall e\,\forall f\,\bigl((\lambda\in\mathbb{R}\wedge u\in V\wedge v\in V\wedge((u,v),b)\in a\wedge((\lambda,b),d)\in s\wedge((\lambda,u),e)\in s\wedge((\lambda,v),f)\in s)\Rightarrow((e,f),d)\in a\bigr),\\ &\forall\lambda\,\forall\kappa\,\forall v\,\forall b\,\forall d\,\forall e\,\forall f\,\bigl((\lambda\in\mathbb{R}\wedge\kappa\in\mathbb{R}\wedge v\in V\wedge((\lambda,\kappa),b)\in{+}\wedge((b,v),d)\in s\wedge((\lambda,v),e)\in s\wedge((\kappa,v),f)\in s)\Rightarrow((e,f),d)\in a\bigr). \end{aligned}$$

Under $\tau$ their premises name $b=u+v$, $d=(u+v)+w$, $e=v+w$, $f=u+(v+w)$ in the first; $b=u+v$, $d=v+u$ in the second; $b=\kappa v$, $d=\lambda(\kappa v)$, $e=\lambda\cdot\kappa$ in the fifth; $b=u+v$, $d=\lambda(u+v)$, $e=\lambda u$, $f=\lambda v$ in the seventh; and $b=\lambda+\kappa$, $d=(\lambda+\kappa)v$, $e=\lambda v$, $f=\kappa v$ in the eighth; and the conclusions $((e,v),d)\in s$, $((1,v),v)\in s$ and $((e,f),d)\in a$ say $d=(\lambda\cdot\kappa)v$, $1v=v$, $d=\lambda u+\lambda v$ and $d=\lambda v+\kappa v$. So, under $\tau$, $\varepsilon_{1},\dots,\varepsilon_{8}$ state, in this order, Vector Space over a Field (i), Vector Space over a Field (ii), Vector Space over a Field (iii), Vector Space over a Field (iv), Vector Space over a Field (v), Vector Space over a Field (vi), Vector Space over a Field (vii) and Vector Space over a Field (viii) for $K=\mathbb{R}$. As $V$, a set variable, stands for a set, Vector Space over a Field (ix) and Vector Space over a Field (x) show that

$$\gamma=\tau\wedge\varepsilon_{1}\wedge\dots\wedge\varepsilon_{8}$$

expresses $\Gamma$. Under $\gamma$, $\zeta(z)$ holds exactly for $z=0_{V}$, by The Zero Vector, Negatives and Differences in a Vector Space (i).

The four conditions. By Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (iii) with $n=2$, $i=0$ and $k=1$, the condition "$x_{0}\in\mathbb{R}$ and $x_{1}=|x_{0}|$" is expressed by a predicative formula in $x_{0},x_{1}$ with parameters among $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$; renaming $x_{0}$ and $x_{1}$ to $\lambda$ and $t$ (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i)) gives a predicative formula $\alpha(\lambda,t)$ that holds exactly when $\lambda\in\mathbb{R}$ and $t=|\lambda|$. Then $|\lambda|\in\mathbb{R}$, being $\lambda$ or $-\lambda$. Let $\eta_{1},\dots,\eta_{4}$ be the formulas

$$\begin{aligned} &\forall v\,\forall y\,\bigl((v\in V\wedge(v,y)\in\nu)\Rightarrow(0,y)\in{\le}\bigr),\\ &\forall v\,\forall y\,\forall z\,\bigl((v\in V\wedge(v,y)\in\nu\wedge y=0\wedge\zeta(z))\Rightarrow v=z\bigr),\\ &\forall\lambda\,\forall v\,\forall w\,\forall y\,\forall t\,\forall r\,\forall q\,\bigl((v\in V\wedge((\lambda,v),w)\in s\wedge(w,y)\in\nu\wedge\alpha(\lambda,t)\wedge(v,r)\in\nu\wedge((t,r),q)\in{\cdot})\Rightarrow y=q\bigr),\\ &\forall u\,\forall v\,\forall w\,\forall y\,\forall r\,\forall t\,\forall q\,\bigl((u\in V\wedge v\in V\wedge((u,v),w)\in a\wedge(w,y)\in\nu\wedge(u,r)\in\nu\wedge(v,t)\in\nu\wedge((r,t),q)\in{+})\Rightarrow(y,q)\in{\le}\bigr). \end{aligned}$$

Under $\gamma$ their premises name $y=\lVert v\rVert$ in the first; $y=\lVert v\rVert$ and $z=0_{V}$ in the second; $w=\lambda v$, $y=\lVert\lambda v\rVert$, $t=|\lambda|$, $r=\lVert v\rVert$ and $q=|\lambda|\,\lVert v\rVert$ in the third; and $w=u+v$, $y=\lVert u+v\rVert$, $r=\lVert u\rVert$, $t=\lVert v\rVert$ and $q=\lVert u\rVert+\lVert v\rVert$ in the fourth. So $\gamma\wedge\eta_{1}$, $\gamma\wedge\eta_{2}$, $\gamma\wedge\eta_{3}$ and $\gamma\wedge\eta_{4}$ express the conditions of (i), (ii), (iii) and (iv) with $V=x_{0}$, addition $x_{1}$, scalar multiplication $x_{2}$ and $\lVert\cdot\rVert=x_{3}$.

Norms and normed spaces. By Norms and Real Normed Spaces (v), under $\Gamma$ the function $\lVert\cdot\rVert$ is a norm on $V$ exactly when it satisfies the four conditions, so the conjunction $\gamma\wedge\eta_{1}\wedge\eta_{2}\wedge\eta_{3}\wedge\eta_{4}$ expresses the condition of (v). By Norms and Real Normed Spaces (vi), under $\Gamma$ the pair $(V,\lVert\cdot\rVert)$ is a real normed space exactly when $\lVert\cdot\rVert$ is a norm on the real vector space $V$, so the same formula expresses the condition of (vi).

Any positions. Each formula $\varphi$ obtained above is thus a predicative formula in $x_{0},x_{1},x_{2},x_{3}$ in the sense of Renaming and Substituting Variables in Predicative Formulas, with parameters among $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$. By Renaming and Substituting Variables in Predicative Formulas (i) with $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$ and $\sigma(3)=l$ (the given $x_{0},\dots,x_{n-1}$ being the first of the distinct set variables $x_{0},x_{1},\dots$ there, so that $x_{1},x_{2},x_{3}$ above are distinct from $x_{0}$ whatever $n$ is), the formula $\varphi(x_{i},x_{j},x_{k},x_{l})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $\varphi$ holds with $x_{0},x_{1},x_{2},x_{3}$ assigned the sets assigned to $x_{i},x_{j},x_{k},x_{l}$, that is, exactly when the condition of the corresponding clause holds with $V=x_{i}$, addition $x_{j}$, scalar multiplication $x_{k}$ and $\lVert\cdot\rVert=x_{l}$. This proves every clause.