Proof of The Dot Product on $\mathbb{R}^n$ Is Symmetric, Bilinear and Positive Definite

Each result cited is universally quantified over the data in its own statement.

Throughout, $n\in\mathbb{N}$, so $1\le n$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order. By The Dot Product on $\mathbb{R}^n$ §dot-product, $u\cdot v=\sum_{k=1}^{n}u_{k}v_{k}$ for $u,v\in\mathbb{R}^{n}$; this is the sum, as in Sums and Products over a Finite Set and over an Interval §intervals and Sums and Products over a Finite Set and over an Interval §sums, of the map $k\mapsto u_{k}v_{k}$ from $[n]=\{1,\dots,n\}$ (Intervals of Natural Numbers §segment) to $\mathbb{R}$, which exists by Sets and Maps: Ordinary Notation §maps, the condition $z=u_{k}v_{k}$ being predicative 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, the components $u_{k}=u(k)$ being real numbers by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §membership. Two maps from $[n]$ to $\mathbb{R}$ with the same value at every $k\in[n]$ are equal by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, and then have the same sum; we use this tacitly when we rewrite a sum termwise. The components of $x+y$, $x-y$ and $tx$ are $x_{k}+y_{k}$, $x_{k}-y_{k}$ and $t\,x_{k}$, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §operations. $\mathbb{R}$ is an ordered field, hence a commutative ring, by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals, Ordered Fields §ordered-field and Fields §field. In particular $u\cdot v\in\mathbb{R}$ for $u,v\in\mathbb{R}^{n}$, by Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set §segment-sums, the sum over $\{1,\dots,n\}$ being the iterated operation of Iterated Operations: Finite Sums and Finite Products §iterated by Sums and Products over a Finite Set and over an Interval §intervals.

Clause symmetric. For $k\in[n]$, $x_{k}y_{k}=y_{k}x_{k}$ by commutativity of the product of $\mathbb{R}$, so $x\cdot y=\sum_{k=1}^{n}x_{k}y_{k}=\sum_{k=1}^{n}y_{k}x_{k}=y\cdot x$.

Clause first. For $k\in[n]$, distributivity in $\mathbb{R}$ gives $(x+y)_{k}z_{k}=(x_{k}+y_{k})z_{k}=x_{k}z_{k}+y_{k}z_{k}$. The sum of $\mathbb{R}$ is associative and commutative by Commutative Rings §ring, and for $n\ge1$ the sum over $\{1,\dots,n\}$ is the iterated operation of Iterated Operations: Finite Sums and Finite Products §iterated, by Sums and Products over a Finite Set and over an Interval §intervals; so Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §termwise gives

$$(x+y)\cdot z=\sum_{k=1}^{n}(x_{k}z_{k}+y_{k}z_{k})=\sum_{k=1}^{n}x_{k}z_{k}+\sum_{k=1}^{n}y_{k}z_{k}=x\cdot z+y\cdot z.$$

Next, $(x-y)_{k}z_{k}=(x_{k}-y_{k})z_{k}=x_{k}z_{k}+(-y_{k})z_{k}=x_{k}z_{k}-y_{k}z_{k}$, by distributivity, Negatives, Differences, Reciprocals and Quotients §negative (with $-y_{k}\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima §negative) and Rules of Arithmetic and Order in an Ordered Field §signs; so by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §difference,

$$(x-y)\cdot z=\sum_{k=1}^{n}(x_{k}z_{k}-y_{k}z_{k})=\sum_{k=1}^{n}x_{k}z_{k}-\sum_{k=1}^{n}y_{k}z_{k}=x\cdot z-y\cdot z.$$

Finally, $(tx)_{k}z_{k}=(t\,x_{k})z_{k}=t\,(x_{k}z_{k})$ by associativity, so by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §distributive,

$$(tx)\cdot z=\sum_{k=1}^{n}t\,(x_{k}z_{k})=t\sum_{k=1}^{n}x_{k}z_{k}=t\,(x\cdot z).$$

Clause second. By the clause symmetric, the clause first, and the clause symmetric again: $z\cdot(x+y)=(x+y)\cdot z=x\cdot z+y\cdot z=z\cdot x+z\cdot y$; $z\cdot(x-y)=(x-y)\cdot z=x\cdot z-y\cdot z=z\cdot x-z\cdot y$; and $z\cdot(tx)=(tx)\cdot z=t\,(x\cdot z)=t\,(z\cdot x)$.

Clause nonnegative. For $u\in\mathbb{R}$, $u^{2}=u^{1+1}=u^{1}u^{1}=u\,u$, by $2=1+1$ (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 $x\cdot x=\sum_{k=1}^{n}x_{k}x_{k}=\sum_{k=1}^{n}x_{k}^{2}$. Each term satisfies $x_{k}^{2}=x_{k}x_{k}\ge0$ by Rules of Arithmetic and Order in an Ordered Field §squares, so $x\cdot x\ge0$ by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §nonnegative.

Clause coordinate-square. As the terms $x_{k}^{2}$ are nonnegative, Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §nonnegative gives $x_{j}^{2}\le\sum_{k=1}^{n}x_{k}^{2}=x\cdot x$ for every $j\in[n]$.

Clause definite. The origin $0$ is the constant map with value $0$, by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §origin and Pointwise Operations on Real-Valued Maps §constants, so its components are all $0$. If $x=0$, then $x_{k}x_{k}=0\cdot0=0$ for every $k\in[n]$, by Rules of Arithmetic and Order in an Ordered Field §zero, so $x\cdot x=\sum_{k=1}^{n}0=n\cdot0=0$, by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §constant and, with commutativity, Rules of Arithmetic and Order in an Ordered Field §zero. Conversely, let $x\cdot x=0$ and $k\in[n]$. By the clauses nonnegative and coordinate-square, $0\le x_{k}x_{k}=x_{k}^{2}\le x\cdot x=0$, so $x_{k}x_{k}=0$ by antisymmetry of the order, and $x_{k}=0$ by Rules of Arithmetic and Order in an Ordered Field §zero. Thus $x_{k}=0_{k}$ for every $k\in[n]$, and $x=0$ by Euclidean Space $\mathbb{R}^n$: n-Tuples of Real Numbers with Their Componentwise Operations §equality.