# Second intersection of a sphere and a line #

This file defines and proves basic results about the second intersection of a sphere with a line through a point on that sphere.

## Main definitions #

`EuclideanGeometry.Sphere.secondInter`

is the second intersection of a sphere with a line through a point on that sphere.

The second intersection of a sphere with a line through a point on that sphere; that point
if it is the only point of intersection of the line with the sphere. The intended use of this
definition is when `p ∈ s`

; the definition does not use `s.radius`

, so in general it returns
the second intersection with the sphere through `p`

and with center `s.center`

.

## Instances For

The distance between `secondInter`

and the center equals the distance between the original
point and the center.

The point given by `secondInter`

lies on the sphere.

If the vector is zero, `secondInter`

gives the original point.

The point given by `secondInter`

equals the original point if and only if the line is
orthogonal to the radius vector.

A point on a line through a point on a sphere equals that point or `secondInter`

.

`secondInter`

is unchanged by multiplying the vector by a nonzero real.

`secondInter`

is unchanged by negating the vector.

Applying `secondInter`

twice returns the original point.

If the vector passed to `secondInter`

is given by a subtraction involving the point in
`secondInter`

, the result of `secondInter`

may be expressed using `lineMap`

.

If the vector passed to `secondInter`

is given by a subtraction involving the point in
`secondInter`

, the result lies in the span of the two points.

If the vector passed to `secondInter`

is given by a subtraction involving the point in
`secondInter`

, the three points are collinear.

If the vector passed to `secondInter`

is given by a subtraction involving the point in
`secondInter`

, and the second point is not outside the sphere, the second point is weakly
between the first point and the result of `secondInter`

.

If the vector passed to `secondInter`

is given by a subtraction involving the point in
`secondInter`

, and the second point is inside the sphere, the second point is strictly between
the first point and the result of `secondInter`

.