[proofplan]
We use the defining [chord-and-tangent group law](/page/Elliptic%20Curve%20Group%20Law), whose use is valid in this page context because the short Weierstrass cubic is nonsingular. In the secant case, the line through $P$ and $Q$ meets the [projective closure](/page/Projective%20Closure) of the cubic in a third point $R=(x_R,y_R)$; comparing the $x^2$ coefficient after substitution gives $x_R=\lambda^2-x_1-x_2$, and reflecting $R$ across the $x$-axis gives $P+Q$. In the tangent case, the same coefficient comparison applies, with $x_1$ counted twice because the line is tangent at $P$.
[/proofplan]
[step:Verify that the displayed slopes are defined]
Assume first that $P \ne Q$. If $x_1=x_2$, then the curve equation gives
\begin{align*}
y_1^2=x_1^3+ax_1+b=y_2^2.
\end{align*}
Thus $(y_2-y_1)(y_2+y_1)=0$. Since $P \ne Q$, we have $y_2 \ne y_1$, hence $y_2=-y_1$, so $Q=(x_1,-y_1)=-P$, contradicting the hypothesis $Q \ne -P$. Therefore $x_2-x_1 \ne 0$, and the secant slope defined by
\begin{align*}
\lambda=\frac{y_2-y_1}{x_2-x_1}
\end{align*}
is defined.
Assume now that $P=Q$. Since $Q \ne -P$, we have $P \ne -P$. Under the [chord-and-tangent group law](/page/Elliptic%20Curve%20Group%20Law), the inverse of an affine point on a short Weierstrass curve is obtained by reflection in the $x$-axis, so $-P=(x_1,-y_1)$. If $2y_1=0$, then $\operatorname{char}(k)\ne 2$ implies $y_1=0$, hence $P=-P$, a contradiction. Therefore $2y_1\ne 0$, and the tangent slope defined by
\begin{align*}
\lambda=\frac{3x_1^2+a}{2y_1}
\end{align*}
is defined.
[/step]
[step:Compute the third intersection point in the secant case]
Assume $P \ne Q$. Define $\mu \in k$ by
\begin{align*}
\mu:=y_1-\lambda x_1.
\end{align*}
Let $L \subset k^2$ be the set of $k$-points on the affine line defined by
\begin{align*}
L=\{(x,y)\in k^2:y=\lambda x+\mu\}.
\end{align*}
Since $\lambda=(y_2-y_1)/(x_2-x_1)$ and $\mu=y_1-\lambda x_1$, both $P$ and $Q$ lie on $L$. Let $\mathbb{P}^2_k$ denote the projective plane over $k$, and let $[X:Y:Z]$ denote its homogeneous coordinates. The projective closure of $E$ in $\mathbb{P}^2_k$ is defined by
\begin{align*}
Y^2Z=X^3+aXZ^2+bZ^3,
\end{align*}
and the point at infinity is $O=[0:1:0]$. The projective closure of the nonvertical line $L$ is defined by
\begin{align*}
Y=\lambda X+\mu Z.
\end{align*}
It does not contain $O$: setting $Z=0$ in the two projective equations forces $X=0$ from $X^3=0$, and then $Y=0$ from $Y=\lambda X$. The triple $[0:0:0]$ is excluded from homogeneous coordinates, so this is not a projective point. Hence all intersections of this line with $E$ are affine and are detected by the following substitution.
Substituting $y=\lambda x+\mu$ into the equation of $E$ gives the cubic polynomial map $F:k\to k$ defined by
\begin{align*}
F(x)=x^3+ax+b-(\lambda x+\mu)^2.
\end{align*}
Expanding,
\begin{align*}
F(x)=x^3-\lambda^2x^2+(a-2\lambda\mu)x+(b-\mu^2).
\end{align*}
The $x$-coordinates of the intersection points of $L$ with $E$ are precisely the roots of $F$. Since $P$ and $Q$ lie on both $L$ and $E$, the elements $x_1$ and $x_2$ are roots of $F$. Since $P\ne Q$ and the first step proved $x_1\ne x_2$, the linear factors $x-x_1$ and $x-x_2$ are distinct. Polynomial division in $k[x]$ gives a monic linear polynomial $G\in k[x]$ such that
\begin{align*}
F(x)=(x-x_1)(x-x_2)G(x).
\end{align*}
Since $G$ is monic and linear, there is a unique element $x_R\in k$ such that
\begin{align*}
G(x)=x-x_R.
\end{align*}
Define $y_R\in k$ by
\begin{align*}
y_R:=\lambda x_R+\mu.
\end{align*}
Then $R:=(x_R,y_R)$ is the remaining affine intersection point, counted with multiplicity. Thus
\begin{align*}
F(x)=(x-x_1)(x-x_2)(x-x_R).
\end{align*}
Comparing the coefficient of $x^2$ 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*}
Since $R$ lies on $L$, its $y$-coordinate satisfies
\begin{align*}
y_R=\lambda x_R+\mu=\lambda x_R+y_1-\lambda x_1=y_1+\lambda(x_R-x_1).
\end{align*}
[guided]
We now compute the third intersection of the secant line with the cubic. The line through $P$ and $Q$ has slope
\begin{align*}
\lambda=\frac{y_2-y_1}{x_2-x_1},
\end{align*}
and we define its intercept $\mu\in k$ by
\begin{align*}
\mu:=y_1-\lambda x_1.
\end{align*}
Thus the set of $k$-points on the affine line is
\begin{align*}
L=\{(x,y)\in k^2:y=\lambda x+\mu\}.
\end{align*}
By construction $P=(x_1,y_1)$ lies on $L$. Also,
\begin{align*}
\lambda x_2+\mu=\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*}
so $Q=(x_2,y_2)$ lies on $L$ as well.
Why does this substitution find all three intersections relevant to the group law? Let $\mathbb{P}^2_k$ denote the projective plane over $k$, and let $[X:Y:Z]$ denote its homogeneous coordinates. The [projective closure](/page/Projective%20Closure) of $E$ in $\mathbb{P}^2_k$ is defined by the homogeneous equation
\begin{align*}
Y^2Z=X^3+aXZ^2+bZ^3,
\end{align*}
and the point at infinity is $O=[0:1:0]$. The projective closure of the line has equation
\begin{align*}
Y=\lambda X+\mu Z.
\end{align*}
At $Z=0$, the projective Weierstrass equation gives $X^3=0$, so $X=0$; the line equation then gives $Y=0$. Since the triple $[0:0:0]$ is excluded from homogeneous coordinates, this is not a projective point, and the line does not pass through $O$. Therefore every intersection of this nonvertical line with $E$ is affine, and its $x$-coordinate is found by substituting $y=\lambda x+\mu$ into the affine equation of $E$. Define the polynomial map $F:k\to k$ by
\begin{align*}
F(x)=x^3+ax+b-(\lambda x+\mu)^2.
\end{align*}
Then a point $(x,\lambda x+\mu)$ lies on $E$ exactly when $F(x)=0$. Expanding the square gives
\begin{align*}
F(x)=x^3+ax+b-\lambda^2x^2-2\lambda\mu x-\mu^2=x^3-\lambda^2x^2+(a-2\lambda\mu)x+(b-\mu^2).
\end{align*}
Thus the coefficient of $x^2$ is $-\lambda^2$.
Because $P$ and $Q$ are intersection points, $F(x_1)=0$ and $F(x_2)=0$. Since $P\ne Q$ and the first step proved $x_1\ne x_2$, the factors $x-x_1$ and $x-x_2$ are distinct. Polynomial division in $k[x]$ gives a monic linear polynomial $G\in k[x]$ such that
\begin{align*}
F(x)=(x-x_1)(x-x_2)G(x).
\end{align*}
A monic linear polynomial over $k$ has the form $x-x_R$ for a unique element $x_R\in k$. Define $y_R\in k$ by
\begin{align*}
y_R:=\lambda x_R+\mu.
\end{align*}
Then $R:=(x_R,y_R)$ is the remaining affine intersection point, counted with multiplicity. Hence
\begin{align*}
F(x)=(x-x_1)(x-x_2)(x-x_R).
\end{align*}
Expanding 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+(x_1x_2+x_1x_R+x_2x_R)x-x_1x_2x_R.
\end{align*}
Comparing the $x^2$ coefficient with the earlier expression for $F$ gives
\begin{align*}
-(x_1+x_2+x_R)=-\lambda^2.
\end{align*}
Therefore
\begin{align*}
x_R=\lambda^2-x_1-x_2.
\end{align*}
Finally, because $R$ lies on the line $L$, its $y$-coordinate is obtained by substituting $x_R$ into the line equation:
\begin{align*}
y_R=\lambda x_R+\mu=\lambda x_R+y_1-\lambda x_1=y_1+\lambda(x_R-x_1).
\end{align*}
[/guided]
[/step]
[step:Reflect the third secant intersection to obtain the group sum]
By the defining [chord-and-tangent group law](/page/Elliptic%20Curve%20Group%20Law), when $P\ne Q$ the sum $P+Q$ is the reflection of the third intersection point $R=(x_R,y_R)$ across the $x$-axis. Hence
\begin{align*}
P+Q=(x_R,-y_R).
\end{align*}
Define $(x_3,y_3):=(x_R,-y_R)$. From the previous step,
\begin{align*}
x_3=x_R=\lambda^2-x_1-x_2,
\end{align*}
and
\begin{align*}
y_3=-y_R
= -\bigl(y_1+\lambda(x_R-x_1)\bigr)
=\lambda(x_1-x_R)-y_1
=\lambda(x_1-x_3)-y_1.
\end{align*}
This proves the formula in the case $P\ne Q$.
[/step]
[step:Compute the tangent slope and repeat the coefficient comparison]
Assume $P=Q$. The tangent line at $P=(x_1,y_1)$ has equation
\begin{align*}
y=\lambda x+\mu,
\end{align*}
where
\begin{align*}
\lambda=\frac{3x_1^2+a}{2y_1}.
\end{align*}
Define $\mu\in k$ by
\begin{align*}
\mu:=y_1-\lambda x_1.
\end{align*}
Indeed, differentiating the affine equation $y^2=x^3+ax+b$ formally along a tangent direction gives
\begin{align*}
2y_1\lambda=3x_1^2+a,
\end{align*}
and $2y_1\ne 0$ by the first step. Since $E$ is nonsingular, this tangent line is the line used in the [chord-and-tangent group law](/page/Elliptic%20Curve%20Group%20Law). The tangent line is also nonvertical, so its [projective closure](/page/Projective%20Closure) does not contain $O=[0:1:0]$ by the same calculation used for a line of the form $Y=\lambda X+\mu Z$ in the secant case.
Define the polynomial map $F:k\to k$ by
\begin{align*}
F(x)=x^3+ax+b-(\lambda x+\mu)^2.
\end{align*}
As before,
\begin{align*}
F(x)=x^3-\lambda^2x^2+(a-2\lambda\mu)x+(b-\mu^2).
\end{align*}
The polynomial derivative $F':k\to k$ is
\begin{align*}
F'(x)=3x^2+a-2\lambda(\lambda x+\mu).
\end{align*}
Because $P$ lies on the tangent line, $\lambda x_1+\mu=y_1$. Therefore
\begin{align*}
F'(x_1)=3x_1^2+a-2\lambda y_1=0,
\end{align*}
where the final equality is the defining relation $2y_1\lambda=3x_1^2+a$. Also $F(x_1)=0$ because $P\in E$ and $P$ lies on the tangent line. Thus $x_1$ is a root of $F$ with multiplicity at least two, so polynomial division in $k[x]$ gives a monic linear polynomial $G\in k[x]$ such that
\begin{align*}
F(x)=(x-x_1)^2G(x).
\end{align*}
Since $G$ is monic and linear, there is a unique element $x_R\in k$ such that
\begin{align*}
G(x)=x-x_R.
\end{align*}
Define $y_R\in k$ by
\begin{align*}
y_R:=\lambda x_R+\mu.
\end{align*}
Then $R:=(x_R,y_R)$ is the remaining affine intersection point, counted with multiplicity, and
\begin{align*}
F(x)=(x-x_1)^2(x-x_R).
\end{align*}
Comparing the coefficient of $x^2$ gives
\begin{align*}
-(2x_1+x_R)=-\lambda^2,
\end{align*}
so
\begin{align*}
x_R=\lambda^2-2x_1=\lambda^2-x_1-x_2,
\end{align*}
because $x_2=x_1$ when $P=Q$. Also,
\begin{align*}
y_R=\lambda x_R+\mu=y_1+\lambda(x_R-x_1).
\end{align*}
[/step]
[step:Reflect the tangent intersection to obtain the doubling formula]
By the tangent case in the defining [chord-and-tangent group law](/page/Elliptic%20Curve%20Group%20Law), $2P=P+P$ is the reflection of the third tangent intersection point $R=(x_R,y_R)$ across the $x$-axis. Thus, defining $(x_3,y_3):=(x_R,-y_R)$, we obtain
\begin{align*}
x_3=x_R=\lambda^2-x_1-x_2,
\end{align*}
and
\begin{align*}
y_3=-y_R
= -\bigl(y_1+\lambda(x_R-x_1)\bigr)
=\lambda(x_1-x_R)-y_1
=\lambda(x_1-x_3)-y_1.
\end{align*}
This is the asserted formula in the case $P=Q$. Combining the secant and tangent cases proves the theorem.
[/step]
