[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*}[/step]

[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: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]