[proofplan]
We take the unique nonvertical affine line through $P$ and $Q$, substitute its equation into the Weierstrass equation, and obtain a monic cubic polynomial whose roots are the three intersection $x$-coordinates. Since $x_1$ and $x_2$ are two roots, coefficient comparison gives the $x$-coordinate of the remaining intersection. The nonsingularity assumption $4a^3+27b^2\neq 0$ ensures that this short Weierstrass equation defines an elliptic curve, so the chord-and-tangent group law is available. That group law defines $P+Q$ as the reflection of the remaining intersection across the $x$-axis, which gives the stated formulas for $x_3$ and $y_3$. The characteristic assumption $\operatorname{char}(k)\neq 2,3$ is used to work in short Weierstrass form and to identify nonsingularity with $4a^3+27b^2\neq 0$; the coordinate computation itself only uses that this model is already given and that $x_2-x_1\neq 0$.
[/proofplan]
[step:Construct the secant line through $P$ and $Q$]
Since $x_1 \neq x_2$, the element $x_2-x_1 \in k$ is nonzero, so the element $\lambda \in k$ defined by
\begin{align*}
\lambda=\frac{y_2-y_1}{x_2-x_1}
\end{align*}
is well-defined. Define the intercept
\begin{align*}
c := y_1-\lambda x_1 \in k.
\end{align*}
Then $y_1=\lambda x_1+c$ by definition of $c$. Also,
\begin{align*}
\lambda x_2+c = \lambda x_2+y_1-\lambda x_1 = y_1+\lambda(x_2-x_1) = y_1+(y_2-y_1) = y_2.
\end{align*}
Let $L \subset k^2$ denote the affine line consisting of all pairs $(x,y) \in k^2$ satisfying $y=\lambda x+c$. The preceding computations show that both $P$ and $Q$ belong to $L$.
[/step]
[step:Substitute the secant line into the cubic equation]
Define the polynomial map $F:k\to k$ as follows: for each $x\in k$, set
\begin{align*}
F(x) := x^3-\lambda^2x^2+(a-2\lambda c)x+(b-c^2).
\end{align*}
A point $(x,\lambda x+c)\in L$ lies on $E$ exactly when
\begin{align*}
(\lambda x+c)^2=x^3+ax+b.
\end{align*}
Expanding and moving all terms to the right-hand side gives
\begin{align*}
0 = x^3+ax+b-(\lambda x+c)^2 = x^3-\lambda^2x^2+(a-2\lambda c)x+(b-c^2) = F(x).
\end{align*}
Since $P,Q\in E(k)$ and both lie on $L$, we have $F(x_1)=0$ and $F(x_2)=0$.
[guided]
The reason for introducing the line equation $y=\lambda x+c$ is that the third intersection point of this line with the cubic is determined by a one-variable polynomial. Define the polynomial map $F:k\to k$ as follows: for each $x\in k$, set
\begin{align*}
F(x) := x^3-\lambda^2x^2+(a-2\lambda c)x+(b-c^2).
\end{align*}
For a point on the line, the $y$-coordinate is forced to be $y=\lambda x+c$. Therefore such a point lies on $E$ exactly when its coordinates satisfy the Weierstrass equation:
\begin{align*}
(\lambda x+c)^2=x^3+ax+b.
\end{align*}
Expanding the square and collecting all terms on the right gives
\begin{align*}
0 = x^3+ax+b-(\lambda x+c)^2 = x^3+ax+b-(\lambda^2x^2+2\lambda cx+c^2) = x^3-\lambda^2x^2+(a-2\lambda c)x+(b-c^2) = F(x).
\end{align*}
Thus the roots of $F$ are precisely the $x$-coordinates of the intersections of $L$ with $E$, counted algebraically. Because $P=(x_1,y_1)$ and $Q=(x_2,y_2)$ are both points of $E(k)$ and the preceding step showed that both lie on $L$, their $x$-coordinates satisfy $F(x_1)=0$ and $F(x_2)=0$.
This is the algebraic form of the geometric statement that the secant line already accounts for two of the three intersections with the cubic.
[/guided]
[/step]
[step:Compare coefficients to find the third intersection coordinate]
Since $F\in k[x]$ is monic of degree $3$ and $F(x_1)=0$, polynomial division by the monic linear polynomial $x-x_1$ gives a quotient $G\in k[x]$ and a remainder $r_1\in k$ such that $F(x)=(x-x_1)G(x)+r_1$; evaluating at $x=x_1$ gives $r_1=F(x_1)=0$. Thus $F(x)=(x-x_1)G(x)$. Because $x_2\neq x_1$ and $F(x_2)=0$, evaluating this factorisation at $x=x_2$ gives $(x_2-x_1)G(x_2)=0$, and since $x_2-x_1\neq 0$ in the field $k$, we get $G(x_2)=0$. Polynomial division by $x-x_2$ gives a quotient $H\in k[x]$ and a remainder $r_2\in k$ such that $G(x)=(x-x_2)H(x)+r_2$; evaluating at $x=x_2$ gives $r_2=G(x_2)=0$. The polynomial $H$ is monic of degree $1$, so there is a unique element $x_R\in k$ such that $H(x)=x-x_R$. Therefore
\begin{align*}
F(x)=(x-x_1)(x-x_2)(x-x_R).
\end{align*}
Expanding the coefficient of $x^2$ in the right-hand side gives
\begin{align*}
(x-x_1)(x-x_2)(x-x_R)
=
x^3-(x_1+x_2+x_R)x^2+\text{terms of degree at most }1.
\end{align*}
Comparing with
\begin{align*}
F(x)=x^3-\lambda^2x^2+(a-2\lambda c)x+(b-c^2)
\end{align*}
yields
\begin{align*}
x_1+x_2+x_R=\lambda^2.
\end{align*}
Hence
\begin{align*}
x_R=\lambda^2-x_1-x_2.
\end{align*}
[guided]
We now turn the two known intersections into the third one. Since $F\in k[x]$ is a monic cubic polynomial and $F(x_1)=0$, divide $F$ by the monic linear polynomial $x-x_1$ in $k[x]$. Polynomial division gives a quotient $G\in k[x]$ and a remainder $r_1\in k$ with
\begin{align*}
F(x)=(x-x_1)G(x)+r_1.
\end{align*}
Evaluating this identity at $x=x_1$ gives $r_1=F(x_1)=0$, so
\begin{align*}
F(x)=(x-x_1)G(x).
\end{align*}
Because $x_2\neq x_1$ and $F(x_2)=0$, evaluating the last identity at $x=x_2$ gives $(x_2-x_1)G(x_2)=0$. Since $x_2-x_1\neq 0$ in the field $k$, it follows that $G(x_2)=0$. Dividing $G$ by $x-x_2$ gives a quotient $H\in k[x]$ and a remainder $r_2\in k$ with
\begin{align*}
G(x)=(x-x_2)H(x)+r_2.
\end{align*}
Evaluating at $x=x_2$ gives $r_2=G(x_2)=0$, hence
\begin{align*}
G(x)=(x-x_2)H(x).
\end{align*}
The original polynomial $F$ is monic of degree $3$, so after removing the two monic linear factors $x-x_1$ and $x-x_2$, the remaining polynomial $H$ is monic of degree $1$. Hence there is a unique element $x_R\in k$ with $H(x)=x-x_R$, and therefore
\begin{align*}
F(x)=(x-x_1)(x-x_2)(x-x_R).
\end{align*}
Now compare the coefficient of $x^2$. Expanding only the degree-$3$ and degree-$2$ terms gives
\begin{align*}
(x-x_1)(x-x_2)(x-x_R)
=
x^3-(x_1+x_2+x_R)x^2+\text{terms of degree at most }1.
\end{align*}
On the other hand, the definition of $F$ gives
\begin{align*}
F(x)=x^3-\lambda^2x^2+(a-2\lambda c)x+(b-c^2).
\end{align*}
Since these are the same polynomial in $k[x]$, their $x^2$ coefficients are equal. Thus
\begin{align*}
x_1+x_2+x_R=\lambda^2,
\end{align*}
and solving for $x_R$ yields
\begin{align*}
x_R=\lambda^2-x_1-x_2.
\end{align*}
This is the algebraic content of the geometric fact that the third intersection coordinate is forced once the first two intersection coordinates and the slope of the line are known.
[/guided]
[/step]
[step:Reflect the third intersection point to obtain the group sum]
Define the third intersection point $R\in k^2$ by
\begin{align*}
R := (x_R,y_R).
\end{align*}
Define its $y$-coordinate $y_R\in k$ by
\begin{align*}
y_R := \lambda x_R+c.
\end{align*}
By construction, $R\in L\cap E(k)$. Since $4a^3+27b^2\neq 0$ and $\operatorname{char}(k)\neq 2,3$, the equation $E:y^2=x^3+ax+b$ defines a nonsingular short Weierstrass elliptic curve. By the definition of the [chord-and-tangent group law](/page/Elliptic%20Curve%20Group%20Law), for a nonvertical line through two distinct affine points $P$ and $Q$, the sum $P+Q$ is the reflection of the third intersection point $R$ across the $x$-axis. Therefore
\begin{align*}
P+Q=(x_R,-y_R).
\end{align*}
Therefore $x_3=x_R$, and the previous step gives
\begin{align*}
x_3=\lambda^2-x_1-x_2.
\end{align*}
For the $y$-coordinate, using $c=y_1-\lambda x_1$ gives
\begin{align*}
y_3 = -y_R = -(\lambda x_R+c) = -(\lambda x_R+y_1-\lambda x_1) = \lambda(x_1-x_R)-y_1 = \lambda(x_1-x_3)-y_1.
\end{align*}
Thus
\begin{align*}
P+Q=(x_3,y_3)
\end{align*}
with the stated formulas.
[guided]
The preceding guided computation produced the third intersection $x$-coordinate $x_R=\lambda^2-x_1-x_2$, but the group law uses the whole third point. Define $R\in k^2$ by
\begin{align*}
R := (x_R,y_R).
\end{align*}
Because $R$ lies on the secant line $L$, its $y$-coordinate is defined by the line equation:
\begin{align*}
y_R := \lambda x_R+c.
\end{align*}
The previous step showed that $F(x_R)=0$, and the substitution step proved that $F(x)=0$ is exactly the condition for $(x,\lambda x+c)$ to lie on $E$. Hence $R\in L\cap E(k)$.
Before using the group law, we verify that it is available for this curve. The theorem statement assumes $4a^3+27b^2\neq 0$ and $\operatorname{char}(k)\neq 2,3$, so the equation $E:y^2=x^3+ax+b$ defines a nonsingular short Weierstrass elliptic curve. The definition of the [chord-and-tangent group law](/page/Elliptic%20Curve%20Group%20Law) says that when a nonvertical line through two distinct affine points $P$ and $Q$ meets the curve again at $R$, the sum $P+Q$ is the reflection of $R$ across the $x$-axis. In affine coordinates this reflection sends $(x_R,y_R)$ to $(x_R,-y_R)$, so
\begin{align*}
P+Q=(x_R,-y_R).
\end{align*}
Therefore $x_3=x_R$. To make the coordinate computation explicit inside this guided step, recall that the secant substitution gave
\begin{align*}
F(x)=x^3-\lambda^2x^2+(a-2\lambda c)x+(b-c^2)
\end{align*}
and that the two known roots $x_1,x_2$ give the factorisation
\begin{align*}
F(x)=(x-x_1)(x-x_2)(x-x_R).
\end{align*}
Comparing the coefficient of $x^2$ in these two expressions gives
\begin{align*}
x_1+x_2+x_R=\lambda^2,
\end{align*}
so
\begin{align*}
x_3=x_R=\lambda^2-x_1-x_2.
\end{align*}
For the second coordinate, substitute the definition of $y_R$ and then the definition of $c$:
\begin{align*}
y_3 = -y_R = -(\lambda x_R+c) = -(\lambda x_R+y_1-\lambda x_1) = \lambda(x_1-x_R)-y_1.
\end{align*}
Since $x_3=x_R$, this becomes
\begin{align*}
y_3=\lambda(x_1-x_3)-y_1.
\end{align*}
Thus $P+Q=(x_3,y_3)$ with exactly the two displayed formulas.
[/guided]
[/step]
