Demostración del teorema de Pappus a través pseudo-divisiones
De Software Libre para la Enseñanza y el Aprendizaje de las Matemáticas (2010-11)
Sean A,B,C y A',B',C' colineales. Si las rectas AB',BC' y CA' cortan a las rectas BA',CB' y AC' entonces los puntos de intersección P,Q,R están alineados.
Por lo tanto, si les damos coordenadas cartesianas a cada uno de nuestros puntos, podremos escribir las hipótesis y la tesis del teorema mediante ecuaciones algebraicas. Esto es:
<math>A=(0,0)</math>, <math>B=(u_1,0)</math>, <math>C=(u_6,0)</math>, <math>A'=(u_2,u_3)</math>, <math>B'=(u_4,u_5)</math>, <math>C'=(x_1,u_7)</math>, <math>P=(x_2,x_3)</math>, <math>Q=(x_4,x_5)</math> y <math>R=(x_6,x_7)</math>.
Por lo tanto, nuestras hipótesis serán:
1) Ya que los puntos son colineales, las pendientes entre cualesquiera 2 puntos, tendrán que ser iguales, luego:
<math>\frac{u_7-u_3}{x_1-u_2}=\frac{u_5-u_3}{u_4-u_2}</math> lo que implica que <math>(u_7-u_3)(u_4-u_2)-(u_5-u_3)(x_1-u_2)=0</math>
2)De nuevo, por la misma razón:
<math>\frac{u_3-0}{u_2-u_1}=\frac{x_3-0}{x_2-u_1} \rightarrow u_3(x_2-u_1)-x_3(u_2-u_1)=0</math>
3) Y la tercera hipótesis es:
<math>\frac{u_5-0}{u_4-0}=\frac{x_3-0}{x_2-0} \rightarrow (x_2u_5)-(x_3u_4)=0</math>
4) <math>\frac{u_7-0}{x_1-0}=\frac{x_5-0}{x_4-0} \rightarrow (u_7x_4)-(x_5x_1)=0</math>
5) <math>\frac{u_3-0}{u_2-u_6}=\frac{x_5-0}{x_4-u_6} \rightarrow u_3(x_4-u_6)-x_5(u_2-u_6)=0</math>
6) <math>\frac{u_7-0}{x_1-u_1}=\frac{x_7-0}{x_6-u_1} \rightarrow u_7(x_6-u_1)-x_7(x_1-u_1)=0</math>
7) <math>\frac{u_5-0}{u_4-u_6}\frac{x_7-0}{x_6-u_6} \rightarrow u_5(x_6-u_6)-x_7(u_4-u_6)=0</math>
Y la ecuación de la tesis, será:
<math>\frac{x_7-x_3}{x_6-x_2}=\frac{x_5-x_3}{x_4-x_2} \rightarrow (x_7-x_3)(x_4-x_2)-(x_5-x_3)(x_6-x_2)=0</math>
Nuestro objetivo es demostrar que cualquier solución del sistema formado por las ecuaciones 1),2),3),4),5),6) y 7), es, a su vez, solución la ecuación que describe la tesis. Con ello, estamos diciendo que la ecuación de la tesis es equivalente al sistema de ecuaciones y por tanto, se verificaría nuestro teorema.
Para ello, usamos la pseudo-división y más concretamente el pseudo-resto, ya que las soluciones del sistema de ecuaciones anterior junto con la tesis, serán también soluciones de la ecuación de la tesis y los sucesivos restos de las divisiones entre cada una de las ecuaciones de las hipótesis y los restos obtenido de las ecuaciones anteriores. Este método se denomina método de wu.
Un teorema nos dice que si el ultimo resto en el última pseudo-división es cero entonces tendremos que las soluciones del sistema de ecuaciones serán las soluciones de la ecuación de la tesis.
Programado y resuelto en maxima con el teorema de Pappus, obtenemos el resultado previsto, como veremos.
Primero, instalamos descargamos el paquete que maxima necesita para darnos los pseudo-restos:
(%i1) load(grobner);
En segundo lugar, damos nombre a las ecuaciones:
(%i2) h1:(u7-u3)*(u4-u2)-(u5-u3)*(x1-u2); (%o2) (u4-u2)*(u7-u3)-(u5-u3)*(x1-u2)
(%i3) h2:u3*(x2-u1)-x3*(u2-u1); (%o3) u3*(x2-u1)-(u2-u1)*x3
(%i4) h3:x2*u5-x3*u4; (%o4) u5*x2-u4*x3
(%i5) h4:u7*x4-x5*x1; (%o5) u7*x4-x1*x5
(%i6) h5:u3*(x4-u6)-x5*(u2-u6); (%o6) u3*(x4-u6)-(u2-u6)*x5
(%i7) h6:u7*(x6-u1)-x7*(x1-u1); (%o7) u7*(x6-u1)-(x1-u1)*x7
(%i8) h7:u5*(x6-u6)-x7*(u4-u6); (%o8) u5*(x6-u6)-(u4-u6)*x7
Y la ecuación de la tesis:
(%i9) g:(x7-x3)*(x4-x2)-(x5-x3)*(x6-x2); (%o9) (x4-x2)*(x7-x3)-(x5-x3)*(x6-x2)
Ahora, triangulamos el sistema. Nos quedaría así:
(%i10) f7:h7; (%o10) u5*(x6-u6)-(u4-u6)*x7
(%i11) f6:second(poly_pseudo_divide(h6,[f7],[x7])); (%o11) u6*(u7*x6-u5*x1+u1*(u5-u7))+u4*(u1*u7-u7*x6)+u5*x1*x6-u1*u5*x6
(%i12) f5:h5; (%o12) u3*(x4-u6)-(u2-u6)*x5
(%i13) f4:second(poly_pseudo_divide(h4,[f5],[x5])); (%o13) u6*(u7*x4-u3*x1)+u3*x1*x4-u2*u7*x4
(%i14) f3:h3; (%o14) u5*x2-u4*x3
(%i15) f2:second(poly_pseudo_divide(h2,[f3],[x3])); (%o15) u4*(u1*u3-u3*x2)+u2*u5*x2-u1*u5*x2
(%i16) f1:h1; (%o16) (u4-u2)*(u7-u3)-(u5-u3)*(x1-u2)
Realizamos las pseudo-divisiones:
(%i17) R7:g; (%o17) (x4-x2)*(x7-x3)-(x5-x3)*(x6-x2)
(%i18) R6:second(poly_pseudo_divide(R7,[f7],[x7])); (%o18) u4*((x5-x3)*x6-x2*x5+x3*x4)+u6*((x3-x5)*x6+x2*(x5-u5)+(u5-x3)*x4)-u5*x4*x6+u5*x2*x6
(%i19) R5:second(poly_pseudo_divide(R6,[f6],[x6])); (%o19) u7*(u6*(u4*(u1*(2*x5-2*x3)-2*x2*x5+2*x3*x4)+u5*(u4*(x2-x4)+u1*(x2-x4)))+u6^2* (x2*x5+u1*(x3-x5)+u5*(x4-x2)-x3*x4)+u4^2*(x2*x5+u1*(x3-x5)-x3*x4)+u1*u4*u5*(x4-x2))+x1* (u5*u6*(u4*(x5-x3)+x2*x5-x3*x4)+u4*u5*(x3*x4-x2*x5)+u5*u6^2*(x3-x5))+u5*u6* (u1*(x3*x4-x2*x5)+u1*u4*(x3-x5))+u1*u4*u5*(x2*x5-x3*x4)+u1*u5*u6^2*(x5-x3)
(%i20) R4:second(poly_pseudo_divide(R5,[f5],[x5])); (%o20) u6*(u2*(u7*(u4*(2*u1*x3-2*x3*x4)+u5*(u4*x4+u1*x4))+u5*(-u1*x3*x4-u1*u4*x3)+u5*x1* (x3*x4+u4*x3)+(-u4-u1)*u5*u7*x2)+u7*(u4^2*(u1*(x3-u3)-x3*x4)+u1*u4*u5*x4-2*u1*u3*u4*x4)+x2* (u7*(2*u3*u4*x4-u1*u4*u5+u3*u4^2)+u5*(u1*u3*x4+u1*u3*u4)+u5*x1*(-u3*x4-u3*u4))+u4*u5*x1*(x3-u3)*x4 +u1*u4*u5*(u3-x3)*x4)+u6^2*(u7*(u4*(2*x3*x4+u1*(2*u3-2*x3))+u5*(-u4*x4-u1*x4)+u1*u3*x4)+u2* (u7*(x3*x4-u5*x4-u1*x3)-u5*x1*x3+u1*u5*x3+u5*u7*x2)+x2* (u7*(-u3*x4+(u4+u1)*u5-2*u3*u4)+u3*u5*x1-u1*u3*u5)+u5*(u1*(x3-u3)*x4+u1*u4*(x3-u3))+u5*x1* ((u3-x3)*x4+u4*(u3-x3)))+u2* (u7*(u4^2*(x3*x4-u1*x3)-u1*u4*u5*x4)-u4*u5*x1*x3*x4+u1*u4*u5*x3*x4+u1*u4*u5*u7*x2)+u6^3* (u7*(-x3*x4+u5*x4+u1*(x3-u3))+u5*x1*(x3-u3)+u1*u5*(u3-x3)+(u3-u5)*u7*x2)+x2* (u3*u4*u5*x1*x4-u3*u4^2*u7*x4-u1*u3*u4*u5*x4)+u1*u3*u4^2*u7*x4
(%i21) R3:second(poly_pseudo_divide(R4,[f4],[x4])); (%o21) u7*x1*(u6* (u3*(u2*((u4^2+2*u1*u4)*x3-u1*u5*x2-u1*u4*u5)+u1*u4^2*x3-u1*u4*u5*x2)-u2^2*u4*u5*x3)+u6^2* (u3*(u2*((-2*u4-u1)*x3+u1*u5)+(-u4^2-2*u1*u4)*x3+u1*u5*x2+u1*u4*u5)+2*u2*u4*u5*x3+u2^2*u5*x3)+u6^3* (u3*((2*u4+u1)*x3+u2*x3-u1*u5)-u4*u5*x3-2*u2*u5*x3)+u6^4*(u5*x3-u3*x3)+u2*u3* (u1*u4*u5*x2-u1*u4^2*x3))+u7^2*(u6* (u2*(2*u1*u4*u5*x2-2*u1*u4^2*x3)+u2^2*((u4+u1)*u5*x2-2*u1*u4*x3)+u2*u3*(u1*u4^2-u4^2*x2))+u6^2*(u2* (4*u1*u4*x3+(-2*u4-2*u1)*u5*x2)+u2^2*(u1*x3-u5*x2)+u1*u4^2*x3+u3* (u2*(2*u4*x2-2*u1*u4)+u4^2*x2-u1*u4^2)-u1*u4*u5*x2)+u6^3* (u2*(2*u5*x2-2*u1*x3)-2*u1*u4*x3+u3*(-2*u4*x2+u2*(u1-x2)+2*u1*u4)+(u4+u1)*u5*x2)+u2^2* (u1*u4^2*x3-u1*u4*u5*x2)+u6^4*(u1*x3+u3*(x2-u1)-u5*x2))+u7*(u6*(u1*u2^2*u4*u5*x3-u1*u2*u3*u4*u5*x2) +u6^2*(-2*u1*u2*u4*u5*x3-u1*u2^2*u5*x3+u3*(u2*(u1*u5*x2+u1*u4*u5)+u1*u4*u5*x2))+u6^3* (u1*u4*u5*x3+2*u1*u2*u5*x3+u3*(-u1*u5*x2-u1*u4*u5-u1*u2*u5))+u6^4*(u1*u3*u5-u1*u5*x3))
(%i22) R2:second(poly_pseudo_divide(R3,[f3],[x3])); (%o22) u4*(u7*x1*(u6^2*(u3*u5*(u2*(2*x2-u1)+u1*x2)-2*u2*u5^2*x2)+u6*(u2^2*u5^2*x2-u1*u2*u3*u5*x2)+ u6^3*(u5^2*x2+u3*u5*(u1-2*x2)))+u7^2*(u6^3*(u5*(u1*x2-2*u2*x2)+u2*u3*(x2-u1))+u6^4*(u5*x2+u3*(u1-x2)) +u5*u6^2*(u2^2*x2-2*u1*u2*x2)+u1*u2^2*u5*u6*x2)+u7*(u6^3*(u3*u5*(u1*x2+u1*u2)-u1*u5^2*x2)+u6^2* (2*u1*u2*u5^2*x2-u1*u2*u3*u5*x2)-u1*u2^2*u5^2*u6*x2-u1*u3*u5*u6^4))+u4^2*(u7^2* (u6^3*(u3*(2*x2-2*u1)-u5*x2)+u6^2*(2*u2*u5*x2+u2*u3*(2*u1-2*x2))-u2^2*u5*u6*x2)+u7* (u3*u5*u6^2*(-u1*x2-u1*u2)+u1*u2*u3*u5*u6*x2+u1*u3*u5*u6^3)+u7*x1* (u3*u5*u6^2*(x2-u1)+u2*u3*u5*u6*(u1-x2)))+u7*x1* (u6^3*(u3*u5*(-u2*x2-u1*x2)+2*u2*u5^2*x2)+u6^2*(u1*u2*u3*u5*x2-u2^2*u5^2*x2)+u6^4*(u3*u5*x2-u5^2*x2))+ u4^3*u7^2*(u2*u3*u6*(x2-u1)+u3*u6^2*(u1-x2))+u7*(u1*u5^2*u6^4*x2-2*u1*u2*u5^2*u6^3*x2+u1*u2^2*u5^2*u6^2*x2) +u7^2*(-u1*u5*u6^4*x2+2*u1*u2*u5*u6^3*x2-u1*u2^2*u5*u6^2*x2)
(%i23) R1:second(poly_pseudo_divide(R2,[f2],[x2])); (%o23) u5*(u4^2*(u3^2* (u2*(u1*(-u6^2*u7*x1-u6^3*u7)+u1^2*(u6*u7*x1+u6^2*u7))+u1*(u6^3*u7*x1+u6^4*u7)+u1^2*(-u6^2*u7*x1-u6^3*u7)) +u3*(u2^2*(u1*u6^2*u7^2-u1^2*u6*u7^2)-u1*u6^4*u7^2+u1^2*u6^3*u7^2))+u4*(u3^2* (u2*(u1*u6^3*u7*x1-u1^2*u6^2*u7*x1)-u1*u6^4*u7*x1+u1^2*u6^3*u7*x1)+u3* (u2*(u1*u6^4*u7^2-u1^2*u6^3*u7^2)+u2^2*(u1^2*u6^2*u7^2-u1*u6^3*u7^2)))+u4^3*(u3* (u2*(u1^2*u6*u7^2-u1*u6^2*u7^2)+u1*u6^3*u7^2-u1^2*u6^2*u7^2)+u3^2* (u2*(u1*u6^2*u7-u1^2*u6*u7)-u1*u6^3*u7+u1^2*u6^2*u7)))+u5^2*(u3*u4*(u2* (u1*(-u6^3*u7*x1-u6^4*u7)+u1^2*(u6^2*u7*x1+u6^3*u7))+u1*u6^4*u7*x1-u1^2*u6^3*u7*x1+u2^2* (u1*u6^3*u7-u1^2*u6^2*u7))+u3*u4^2*(u2*(u1*(u6^2*u7*x1+u6^3*u7)+u1^2*(-u6*u7*x1-u6^2*u7))-u1*u6^3*u7*x1+ u1^2*u6^2*u7*x1+u2^2*(u1^2*u6*u7-u1*u6^2*u7)))
(%i24) R0:second(poly_pseudo_divide(R1,[f1],[x1])); (%o24) 0