Esta es una prueba algebraica que utiliza cálculos polinómicos. Lo que me gusta considerar como el enfoque "no me hagas pensar". Como tal se aleja bastante de lo que ya tienes. Pero viendo que no ha habido ninguna otra respuesta en los últimos dos días, considero que esta prueba es mejor que ninguna, y que el bumping de la pregunta puede hacer más bien que tenerla marcada como respondida hará mal.
Elección de coordenadas
Estoy usando coordenadas homogéneas . Sin pérdida de generalidad se pueden elegir los puntos definitorios de la configuración así:
$$ A=\begin{pmatrix}1-a^2\\2a\\1+a^2\end{pmatrix}\quad B=\begin{pmatrix}1-b^2\\2b\\1+b^2\end{pmatrix}\quad C=\begin{pmatrix}1-c^2\\2c\\1+c^2\end{pmatrix}\qquad P=\begin{pmatrix}p\\0\\1\end{pmatrix}\quad Q=\begin{pmatrix}1\\0\\p\end{pmatrix} $$
Esto no supone una pérdida de generalidad, ya que siempre se puede elegir el sistema de coordenadas de forma que la circunferencia sea el círculo unitario. (El caso especial en el que $A,B,C$ son colineales ya es demasiado degenerado ya que hará que grandes partes de la construcción sean indefinidas). Además, se puede girar el sistema de coordenadas de forma que $P$ y $Q$ se encuentran en el $y=0$ eje. Estoy usando el sustitución de medio ángulo tangente para $A,B,C$ que puede describir cualquier punto del círculo unitario excepto $(-1,0)$ (que corresponde a un parámetro infinito). Si uno de estos tres puntos es $(-1,0)$ entonces se puede girar todo el montaje por $180°$ . Si esto todavía deja un punto en $(-1,0)$ entonces esto significa que $P,Q$ y dos de $A,B,C$ son colineales, lo que de nuevo hace que gran parte de la construcción sea indefinida. Así que, sin pérdida de generalidad, las coordenadas anteriores pueden representar cualquier situación suficientemente no degenerada (así como varias que siguen siendo demasiado degeneradas para esta construcción).
Formulación del cómputo
A continuación necesitamos círculos a través de $P$ y $Q$ . Dos de estos círculos están definidos por
$$ R_1=\begin{pmatrix} -2p & 0 & 1+p^2 \\ 0 & -2p & 0 \\ 1+p^2 & 0 & -2p \end{pmatrix} \qquad R_2=\begin{pmatrix} 0 & 0 & 0 \\ 0 & 0 & 1 \\ 0 & 1 & 0 \end{pmatrix} $$
$R_1$ es el círculo con diámetro $PQ$ , mientras que $R_2$ es el círculo degenerado formado por la línea $y=0$ y la línea en el infinito (es decir $z=0$ ). Cualquier otro círculo a través de $P$ y $Q$ es una combinación lineal de estos dos. Así que se obtiene
$$\bigcirc APQ=(A^T\cdot R_1\cdot A)R_2 - (A^T\cdot R_2\cdot A)R_1$$
También para $\bigcirc BPQ$ y $\bigcirc CPQ$ . Cualquier punto de la línea $b$ puede describirse como una combinación lineal de $A$ y $C$ . El punto $A_b$ en particular, puede describirse como
$$ A_b = (C^T\cdot\bigcirc APQ\cdot C)A - 2(A^T\cdot\bigcirc APQ\cdot C)C $$
También para $A_c,B_a,B_c,C_a,C_b$ . Tanto los puntos de unión como las líneas de intersección pueden calcularse mediante el producto cruzado, por lo que se tiene
$$A_1 = (B_c\times B_a)\times(C_a\times C_b)$$
También para $B_1$ y $C_1$ . A continuación, necesitamos una fórmula más genérica para "círculo para un diámetro dado". Para puntos con coordenadas homogéneas $(x_1,y_1,z_1)^T$ y $(x_2,y_2,z_2)^T$ este círculo es
$$\begin{pmatrix} 2z_1z_2 & 0 & -x_1z_2-z_1x_2 \\ 0 & 2z_1z_2 & -y_1z_2-z_1y_2 \\ -x_1z_2+z_1x_2 & -y_1z_2+z_1y_2 & 2x_1x_2+2y_1y_2 \end{pmatrix}$$
El eje radical de este círculo con el círculo unitario $\bigcirc ABC$ es
$$\begin{pmatrix} z_1x_2 + x_1z_2 \\ z_1y_2 + y_1z_2 \\ -x_1x_2-y_1y_2-z_1z_2 \end{pmatrix}$$
Enchufando $A$ y $A_1$ en esta fórmula, se obtiene un vector que describe la línea $AX$ , donde $X$ se define en este punto como la intersección de $\bigcirc AA_1$ y $\bigcirc ABC$ . Lo mismo ocurre con las otras dos líneas. Para demostrar que las tres rectas coinciden, verifique que su determinante es cero. Para demostrar que el punto común se encuentra en la circunferencia unitaria, por ejemplo, interceptar dos de ellas (utilizando el producto cruzado) e introducir el resultado en la ecuación de la circunferencia unitaria.
Ejecución del cálculo
Los resultados del cálculo serán bastante grandes. Pero pueden mantenerse en un tamaño manejable cancelando los factores comunes después de cada operación. Esto es válido porque los múltiplos escalares se identifican para coordenadas homogéneas. Si la combinación de parámetros puede hacer que ese factor común sea igual a cero, entonces cancelarlo correspondería a eliminar una singularidad removible. Sólo estoy imprimiendo un ejemplo para cada grupo de objetos, donde los demás se pueden obtener simplemente sustituyendo variables.
\begin{align*} \bigcirc APQ&=\begin{pmatrix} 4ap & 0 & -2ap^2-2a \\ 0 & 4ap & -a^2p^2-2a^2p-a^2+p^2-2p+1 \\ -2ap^2-2a & -a^2p^2-2a^2p-a^2+p^2-2p+1 & 4ap \end{pmatrix} \\ A_b&= \begin{pmatrix} a^2cp^2+ac^2p^2+2a^2cp+a^2c+ac^2+ap^2+cp^2-2cp+a+c \\ a^2c^2p^2+2a^2c^2p+a^2c^2-p^2+2p-1 \\ 2ac^2p+2ap \end{pmatrix} \\ A_1&= \begin{pmatrix} a^2b^2c^2p^2+2a^2b^2c^2p+a^2b^2c^2+a^2bcp^2+a^2bc+bcp^2+bc+p^2-2p+1 \\ -ab^2c^2p^2-2ab^2c^2p-ab^2c^2+ap^2-2ap+a \\ 2a^2bcp+2bcp \end{pmatrix} \\ AX&= \begin{pmatrix} a^2bc + 1 \\ -abc + a \\ a^2bc - 1 \end{pmatrix} \\ X&= \begin{pmatrix} 1-(abc)^2 \\ -2abc \\ 1+(abc)^2 \end{pmatrix} \end{align*}
Observaciones
Puede ser interesante observar que $X$ el punto de intersección de los círculos, no depende de $p$ . Lo que significa que la posición del eje $PQ$ es relevante para la ubicación de $X$ pero la posición de $P$ y $Q$ en ese eje no lo es. Las coordenadas de $X$ vuelven a seguir la forma de una sustitución de medio ángulo tangente, esta vez con el parámetro $-abc$ . No estoy seguro de si esto puede ser de utilidad para un enfoque diferente en la prueba de esto.
Código Sage
Hice todo lo anterior utilizando Sage.
def simpl(x):
if x.is_zero(): return x
return x.parent()(x / gcd(x.list()))
PR1.<a,b,c,p> = ZZ[]
A = vector([1-a^2, 2*a, 1+a^2])
B = A(a=b)
C = A(a=c)
P = vector([p, 0, 1])
Q = vector([1, 0, p])
R1 = matrix(PR1, [[-2*p, 0, p^2+1], [0, -2*p, 0], [p^2+1, 0, -2*p]])
R2 = matrix(PR1, [[0, 0, 0], [0, 0, 1], [0, 1, 0]])
APQ = simpl(A*R1*A*R2 - A*R2*A*R1)
BPQ = APQ(a=b)
CPQ = APQ(a=c)
Ab = simpl(C*APQ*C*A - 2*A*APQ*C*C)
Ac = Ab(a=a, b=c, c=b)
Ba = Ab(a=b, b=a, c=c)
Bc = Ab(a=b, b=c, c=a)
Ca = Ab(a=c, b=a, c=b)
Cb = Ab(a=c, b=b, c=a)
AA = simpl(Ab.cross_product(Ac))
BB = simpl(Bc.cross_product(Ba))
CC = simpl(Ca.cross_product(Cb))
A1 = simpl(BB.cross_product(CC))
B1 = simpl(CC.cross_product(AA))
C1 = simpl(AA.cross_product(BB))
def Radl(P1, P2):
x1, y1, z1 = P1
x2, y2, z2 = P2
v = (z1*x2 + x1*z2, z1*y2 + y1*z2, -x1*x2 - y1*y2 - z1*z2)
return simpl(P1.parent()(v))
AX = Radl(A, A1)
BX = Radl(B, B1)
CX = Radl(C, C1)
assert matrix((AX, BX, CX)).det().is_zero()
X = simpl(AX.cross_product(BX))
assert (X*diagonal_matrix((1, 1, -1))*X).is_zero()
