Proof of The Summation Map on Real-Valued Maps over a Finite Set, and the Dot Product, Euclidean Norm and Euclidean Distance as Maps

Each result cited is universally quantified over the data in its own statement. We work in Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces. $\mathbb{R}$ is an ordered field by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals, hence a commutative ring by Ordered Fields §ordered-field and Fields §field; so by Commutative Rings, Fields and Ordered Fields: Standard Notation §rings its addition $+$ is associative and commutative with neutral element $0$.

Predicativity and uniqueness. Every expression to which Maps and Relations Given by Formulas §map or Maps and Relations Given by Formulas §binary is applied below is built from ordered pairs and from values of maps and binary operations, the maps being set variables or parameters. These are defined set symbols by Functions, Values of a Function, and Functions from One Class to Another §value and Binary Operations on a Set §notation, and no quantifier over a class variable arises. So each such expression is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure. At each use we check that the symbols are used properly, that is, that each argument lies in the domain of what is applied to it. In each clause, the value prescribed by the cited scheme is shown to equal the value required by the clause at every argument. So the two conditions on a map coincide, and the uniqueness given by the scheme is the uniqueness claimed.

Clause sum-map. Let $B$ be finite. By The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set §members, the elements of $\mathbb{R}^{B}$ are exactly the maps $a:B\to\mathbb{R}$. For such $a$ and $k\in B$ we have $k\in B=\operatorname{dom}a$, and $a(k)\in\operatorname{ran}a\subseteq\mathbb{R}$ by Functions, Values of a Function, and Functions from One Class to Another §map, Functions, Values of a Function, and Functions from One Class to Another §value and Relations, Domain, Range, Inverse and Composition §range. So $a(k)$ is used properly, and Maps and Relations Given by Formulas §binary gives a map $e:\mathbb{R}^{B}\times B\to\mathbb{R}$ with $e(a,k)=a(k)$. Now apply Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set §finite-operation with the operation $+$ on $X=\mathbb{R}$, which has the neutral element $0$, with $A=\mathbb{R}^{B}$, the finite set $B$ and $f=e$. It gives exactly one map $h:\mathbb{R}^{B}\to\mathbb{R}$ with $h(a)=\sum_{k\in B}e_{a}(k)$ for every $a\in\mathbb{R}^{B}$, where $e_{a}:B\to\mathbb{R}$ is $k\mapsto e(a,k)$. The functions $e_{a}$ and $a$ both have domain $B$, and $e_{a}(k)=a(k)$ for every $k\in B$, so $e_{a}=a$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Hence $h(a)=\sum_{k\in B}a(k)$. Here the sum is the iterated operation of $+$ over $B$ of Sums and Products over a Finite Set and over an Interval §operation and Sums and Products over a Finite Set and over an Interval §empty, which is the sum over $B$ of Commutative Rings, Fields and Ordered Fields: Standard Notation §rings. So $\Sigma_{B}=h$ is the required map, and it is the only one.

Clause dot-product. Let $n\in\mathbb{N}$. By Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §space, $\mathbb{R}^{n}=\mathbb{R}^{[n]}$, and $[n]=\{1,\dots,n\}$ by Intervals of Natural Numbers §segment; this set is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §naturals. Let $\Sigma_{[n]}$ be the map of the clause sum-map for $B=[n]$, and let $\odot$ be the binary operation on $\mathbb{R}^{[n]}$ given by Pointwise Operations on Real-Valued Maps Exist and Are Unique §binary for $\cdot$ and $I=[n]$. By Pointwise Operations on Real-Valued Maps §operations, $x\odot y$ is the pointwise product $xy$, and $(xy)(k)=x_{k}y_{k}$ for $k\in[n]$, with components as in Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership. For $x,y\in\mathbb{R}^{n}$, the pair $(x,y)$ lies in $\mathbb{R}^{n}\times\mathbb{R}^{n}=\operatorname{dom}\odot$ by Binary Operations on a Set §notation. Also $xy\in\mathbb{R}^{[n]}=\operatorname{dom}\Sigma_{[n]}$ by Binary Operations on a Set §notation, and $\Sigma_{[n]}(xy)\in\mathbb{R}$. So Maps and Relations Given by Formulas §binary gives exactly one map $f:\mathbb{R}^{n}\times\mathbb{R}^{n}\to\mathbb{R}$ with $f(x,y)=\Sigma_{[n]}(x\odot y)$. By the clause sum-map, $\Sigma_{[n]}(xy)=\sum_{k\in[n]}(xy)(k)$. By The Dot Product on $\mathbb{R}^n$ §dot-product, $x\cdot y=\sum_{k=1}^{n}x_{k}y_{k}$; by Iterated Operations: Finite Sums and Finite Products §iterated, this is the iterated sum of the map $k\mapsto x_{k}y_{k}$ on $[n]$; that map is $xy$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality; and since $1\le n$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order, Sums and Products over a Finite Set and over an Interval §intervals gives $\sum_{k=1}^{n}(xy)_{k}=\sum_{k\in[n]}(xy)(k)$. Hence $f(x,y)=x\cdot y$.

Clause norm. The square-root map. Let $S=\{s\in\mathbb{R}:0\le s\}$. This is a set by Sets and Maps: Ordinary Notation §set-builder: the formula $0\le s$ is $(0,s)\in{\le}$ by Relations, Domain, Range, Inverse and Composition §relation, with $0$ and $\le$ as parameters, and it 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 §pair-membership. Let $\varphi(u,v)$ be the formula $0\le u\wedge0\le v\wedge v\cdot v=u$, with parameters $0$, $\le$, $\cdot$ and $\mathbb{R}$. Its first two conjuncts are predicative as just said, and $v\cdot v$ in its third conjunct is a defined set symbol by Binary Operations on a Set §notation, used properly for $u,v\in\mathbb{R}$; so, as in the paragraph on predicativity, $\varphi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure, and Maps and Relations Given by Formulas §relation gives a relation $R$ on $\mathbb{R}$ such that, for $u,v\in\mathbb{R}$, $(u,v)\in R$ if and only if $\varphi(u,v)$.

For $v\in\mathbb{R}$, $v^{2}=v^{1+1}=v^{1}v^{1}=v\cdot v$ by Arithmetic and Order of the Natural Numbers §digits, Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §exponents and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product. Hence, by Existence and Uniqueness of Nonnegative k-th Roots of Nonnegative Real Numbers §root with $k=2$, for each $u\in S$ there is exactly one $v\in\mathbb{R}$ with $0\le v$ and $v\cdot v=u$, namely $\sqrt{u}$ by The k-th Root and the Square Root of a Nonnegative Real Number §root and The k-th Root and the Square Root of a Nonnegative Real Number §square-root. By Relations, Domain, Range, Inverse and Composition §on and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, every element of $R$ is a pair $(u,v)$ with $u,v\in\mathbb{R}$ and $\varphi(u,v)$, so $u\in S$. Therefore $R$ is a function by Functions, Values of a Function, and Functions from One Class to Another §function. It has $\operatorname{dom}R=S$ and $\operatorname{ran}R\subseteq\mathbb{R}$ by Relations, Domain, Range, Inverse and Composition §domain and Relations, Domain, Range, Inverse and Composition §range. So $R:S\to\mathbb{R}$ is a map by Functions, Values of a Function, and Functions from One Class to Another §map, with $R(u)=\sqrt{u}$ for $u\in S$ by Functions, Values of a Function, and Functions from One Class to Another §value.

The norm map. Let $f$ be the map of the clause dot-product. For $x\in\mathbb{R}^{n}$, $(x,x)\in\operatorname{dom}f$, and $f(x,x)=x\cdot x\in S$ by The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite §nonnegative. So $R(f(x,x))$ is used properly, and it lies in $\mathbb{R}$. Then Maps and Relations Given by Formulas §map gives exactly one map $g:\mathbb{R}^{n}\to\mathbb{R}$ with $g(x)=R(f(x,x))$, and $R(f(x,x))=\sqrt{x\cdot x}=\lVert x\rVert$ by The Euclidean Norm on $\mathbb{R}^n$ §norm.

Clause distance. Let $\oplus$ be the binary operation on $\mathbb{R}^{[n]}=\mathbb{R}^{n}$ given by Pointwise Operations on Real-Valued Maps Exist and Are Unique §binary for $+$, and let $\nu:\mathbb{R}^{n}\to\mathbb{R}^{n}$ be the map of Pointwise Operations on Real-Valued Maps Exist and Are Unique §negative, both with $I=[n]$. By Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations and Pointwise Operations on Real-Valued Maps §operations, for $x,y\in\mathbb{R}^{n}$ we have $-y=\nu(y)$ and $x-y=x+(-y)=x\oplus\nu(y)$. Here $y\in\operatorname{dom}\nu$, and $\nu(y)\in\mathbb{R}^{n}$. The pair $(x,\nu(y))$ lies in $\mathbb{R}^{n}\times\mathbb{R}^{n}=\operatorname{dom}\oplus$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. Also $x-y\in\mathbb{R}^{n}=\operatorname{dom}g$ by Binary Operations on a Set §notation, with $g$ the map of the clause norm. So Maps and Relations Given by Formulas §binary gives exactly one map $h:\mathbb{R}^{n}\times\mathbb{R}^{n}\to\mathbb{R}$ with $h(x,y)=g(x\oplus\nu(y))$. By the clause norm, $g(x\oplus\nu(y))=g(x-y)=\lVert x-y\rVert$.