Proof of Bilinearity and Symmetry of the Dot Product on $\mathbb{R}^n$

Throughout, coordinates of points of $\mathbb{R}^n$ are those of Euclidean Space $\mathbb{R}^n$, and $z\cdot w=\sum_{i=1}^{n}z_iw_i$ by Difference, Dot Product, and Orthogonality in $\mathbb{R}^n$. Claims 2 and 3 of Properties of Finite Sums are used as additivity and homogeneity of finite sums, and the field axioms of the field $\mathbb{R}$ (associativity and commutativity of addition and multiplication, distributivity, the additive identity and additive inverses) are used for the coordinatewise computations.

Claim 1. For each $i$ the field multiplication is commutative, so $z_iw_i=w_iz_i$; the two families of summands are therefore the same family, and the sums defining $z\cdot w$ and $w\cdot z$ coincide.

Claim 2. By Sum of Points of $\mathbb{R}^n$ the $i$th coordinate of $z+z'$ is $z_i+z'_i$, so by distributivity the $i$th summand of $(z+z')\cdot w$ is

The family of summands of $(z+z')\cdot w$ is thus the pointwise sum of the families $i\mapsto z_iw_i$ and $i\mapsto z'_iw_i$, and additivity of finite sums gives $(z+z')\cdot w=z\cdot w+z'\cdot w$.

Claim 3. By Difference, Dot Product, and Orthogonality in $\mathbb{R}^n$ the $i$th coordinate of $z-z'$ is $z_i-z'_i$, and by associativity of addition, the additive-inverse axiom and the additive-identity axiom, $(z_i-z'_i)+z'_i=z_i$ for each $i$; hence $(z-z')+z'=z$, the two points having the same coordinates. Claim 2 applied to the points $z-z'$ and $z'$ therefore gives

Adding $-(z'\cdot w)$ to both sides and using the same three field axioms gives $(z-z')\cdot w=z\cdot w-z'\cdot w$.

Claim 4. By Scalar Multiple of a Point of $\mathbb{R}^n$ the $i$th coordinate of $\mu z$ is $\mu z_i$, so by associativity of multiplication the $i$th summand of $(\mu z)\cdot w$ is $(\mu z_i)w_i=\mu\,(z_iw_i)$. Homogeneity of finite sums now gives

Claim 5. Each identity follows from claim 1 together with the corresponding identity in the first argument: for instance $w\cdot(z+z')=(z+z')\cdot w=z\cdot w+z'\cdot w=w\cdot z+w\cdot z'$, and likewise for the difference using claim 3 and for the scalar multiple using claim 4.