Processing math: 100%

:: Pascal's Theorem in Real Projective Plane
:: by Roland Coghetto
::
:: Received June 27, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

theorem Th01: :: PASCAL:1

for p, q, r being Point of (TOP-REAL 3) holds
( |{p,q,r}| = |{r,p,q}| & |{p,q,r}| = |{q,r,p}| )

proof end;

theorem Th02: :: PASCAL:2

for K being Field
for a, b, c, d, e, f, g, h, i, a1, b1, c1, d1, e1, f1, g1, h1, i1 being Element of K st <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> = <*<*a1,b1,c1*>,<*d1,e1,f1*>,<*g1,h1,i1*>*> holds
( a = a1 & b = b1 & c = c1 & d = d1 & e = e1 & f = f1 & g = g1 & h = h1 & i = i1 )

proof end;

theorem Th03: :: PASCAL:3

for K being Field
for M being Matrix of 3,K ex a, b, c, d, e, f, g, h, i being Element of K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>

proof end;

theorem Th04: :: PASCAL:4

for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
( a = M * (1,1) & b = M * (1,2) & c = M * (1,3) & d = M * (2,1) & e = M * (2,2) & f = M * (2,3) & g = M * (3,1) & h = M * (3,2) & i = M * (3,3) )

proof end;

theorem Th05: :: PASCAL:5

for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
M @ = <*<*a,d,g*>,<*b,e,h*>,<*c,f,i*>*>

proof end;

theorem Th06: :: PASCAL:6

for K being Field
for a, b, c, d, e, f, g, h, i being Element of K
for M being Matrix of 3,K st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & M is symmetric holds
( b = d & c = g & h = f )

proof end;

theorem Th07: :: PASCAL:7

for M, N being Matrix of 3,F_Real st N is symmetric holds
((M @) * N) * M is symmetric

proof end;

theorem Th08: :: PASCAL:8

for M being Matrix of 3,F_Real
for a, b, c, d, e, f, g, h, i, x, y, z being Element of F_Real
for v being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for p being FinSequence of 1 -tuples_on REAL st p = M * uf & v = M2F p & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & uf = <*x,y,z*> holds
( p = <*<*(((a * x) + (b * y)) + (c * z))*>,<*(((d * x) + (e * y)) + (f * z))*>,<*(((g * x) + (h * y)) + (i * z))*>*> & v = <*(((a * x) + (b * y)) + (c * z)),(((d * x) + (e * y)) + (f * z)),(((g * x) + (h * y)) + (i * z))*> )

proof end;

Lm01: for p being FinSequence of REAL
for N1, M, N2 being Matrix of 3,REAL st len p = 3 holds
((N1 * M) * N2) * p = N1 * (M * (N2 * p))

proof end;

Lm02: for p being FinSequence of REAL
for N, M being Matrix of 3,REAL st len p = 3 holds
|((N * p),(M * (N * p)))| = |(p,((((N @) * M) * N) * p))|

proof end;

Lm03: for NR, M being Matrix of 3,REAL holds ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) is Matrix of 3,REAL

proof end;

Lm04: for n being Nat
for A, B, C, D, E being Matrix of n,REAL holds (A * ((B * C) * D)) * E = ((A * B) * C) * (D * E)

proof end;

Lm05: for n being Nat
for A, B being Matrix of n,F_Real holds MXF2MXR (A * B) = (MXF2MXR A) * (MXF2MXR B)

proof end;

Lm06: for A being Matrix of REAL holds MXF2MXR (MXR2MXF A) = A

proof end;

Lm07: for n being Nat
for A, B being Matrix of n,REAL holds MXR2MXF (A * B) = (MXR2MXF A) * (MXR2MXF B)

proof end;

Lm08: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
NR * (MXF2MXR ((MXR2MXF NR) ~)) = 1_Rmatrix 3

proof end;

Lm09: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
(NR @) * (MXF2MXR ((MXR2MXF (NR @)) ~)) = 1_Rmatrix 3

proof end;

Lm10: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
(MXF2MXR ((MXR2MXF NR) ~)) * NR = 1_Rmatrix 3

proof end;

Lm11: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
(MXF2MXR ((MXR2MXF (NR @)) ~)) * (NR @) = 1_Rmatrix 3

proof end;

Lm12: for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL st NR = MXF2MXR N holds
NR @ is invertible

proof end;

Lm13: for N being invertible Matrix of 3,F_Real
for NR, M, M2 being Matrix of 3,REAL st NR = MXF2MXR N & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M) * (MXF2MXR ((MXR2MXF NR) ~)) holds
((NR @) * M2) * NR = M

proof end;

Lm14: for n being Nat
for N being invertible Matrix of n,F_Real
for M being Matrix of n,REAL st M = MXF2MXR N holds
M is invertible

proof end;

Lm15: for n being Nat
for N being Matrix of n,F_Real
for M being Matrix of n,REAL st M is invertible & N = MXR2MXF M holds
N is invertible

proof end;

theorem Th09: :: PASCAL:9

for p being FinSequence of REAL
for M being Matrix of 3,REAL
for a, b, c, d, e, f, g, h, i, p1, p2, p3 being Element of REAL st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & p = <*p1,p2,p3*> holds
M * p = <*(((a * p1) + (b * p2)) + (c * p3)),(((d * p1) + (e * p2)) + (f * p3)),(((g * p1) + (h * p2)) + (i * p3))*>

proof end;

Lm16: for p being FinSequence of REAL
for M being Matrix of 3,REAL st p = 0. (TOP-REAL 3) holds
M * p = p

proof end;

Lm17: <*<*0,0,0*>,<*0,0,0*>,<*0,0,0*>*> = 0. (F_Real,3,3)

proof end;

Lm18: <*<*0,0,0*>,<*0,0,0*>,<*0,0,0*>*> = 0_Rmatrix 3

proof end;

Lm19: for n being Nat
for K being Field
for M being Matrix of n,K st n > 0 holds
M * (0. (K,n,n)) = 0. (K,n,n)

proof end;

Lm20: for M being Matrix of 3,REAL holds
( M * (0_Rmatrix 3) = 0_Rmatrix 3 & (0_Rmatrix 3) * M = 0_Rmatrix 3 )

proof end;

definition

let a, b, c, d, e, f be Real;
let u be Element of (TOP-REAL 3);

func qfconic (a,b,c,d,e,f,u) -> Real equals :: PASCAL:def 1
((((((a * (u . 1)) * (u . 1)) + ((b * (u . 2)) * (u . 2))) + ((c * (u . 3)) * (u . 3))) + ((d * (u . 1)) * (u . 2))) + ((e * (u . 1)) * (u . 3))) + ((f * (u . 2)) * (u . 3));

coherence
((((((a * (u . 1)) * (u . 1)) + ((b * (u . 2)) * (u . 2))) + ((c * (u . 3)) * (u . 3))) + ((d * (u . 1)) * (u . 2))) + ((e * (u . 1)) * (u . 3))) + ((f * (u . 2)) * (u . 3)) is Real ;

end;

:: deftheorem defines qfconic PASCAL:def 1 :
for a, b, c, d, e, f being Real
for u being Element of (TOP-REAL 3) holds qfconic (a,b,c,d,e,f,u) = ((((((a * (u . 1)) * (u . 1)) + ((b * (u . 2)) * (u . 2))) + ((c * (u . 3)) * (u . 3))) + ((d * (u . 1)) * (u . 2))) + ((e * (u . 1)) * (u . 3))) + ((f * (u . 2)) * (u . 3));

definition

let a, b, c, d, e, f be Real;

func conic (a,b,c,d,e,f) -> Subset of (ProjectiveSpace (TOP-REAL 3)) equals :: PASCAL:def 2
{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } ;

coherence
{ P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } is Subset of (ProjectiveSpace (TOP-REAL 3))

proof end;

end;

:: deftheorem defines conic PASCAL:def 2 :
for a, b, c, d, e, f being Real holds conic (a,b,c,d,e,f) = { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (a,b,c,d,e,f,u) = 0 } ;

theorem Th10: :: PASCAL:10

for a, b, c, d, e, f being Real
for u1, u2 being non zero Element of (TOP-REAL 3) st Dir u1 = Dir u2 & qfconic (a,b,c,d,e,f,u1) = 0 holds
qfconic (a,b,c,d,e,f,u2) = 0

proof end;

theorem Th11: :: PASCAL:11

for a, b, c, d, e, f being Real
for u being non zero Element of (TOP-REAL 3)
for P being Element of (ProjectiveSpace (TOP-REAL 3)) st P = Dir u & qfconic (a,b,c,d,e,f,u) = 0 holds
P in conic (a,b,c,d,e,f)

proof end;

definition

let a, b, c, d, e, f be Real;

func symmetric_3 (a,b,c,d,e,f) -> Matrix of 3,F_Real equals :: PASCAL:def 3
<*<*a,d,e*>,<*d,b,f*>,<*e,f,c*>*>;

coherence
<*<*a,d,e*>,<*d,b,f*>,<*e,f,c*>*> is Matrix of 3,F_Real

proof end;

end;

:: deftheorem defines symmetric_3 PASCAL:def 3 :
for a, b, c, d, e, f being Real holds symmetric_3 (a,b,c,d,e,f) = <*<*a,d,e*>,<*d,b,f*>,<*e,f,c*>*>;

theorem Th12: :: PASCAL:12

for a, b, c, d, e, f being Real holds symmetric_3 (a,b,c,d,e,f) is symmetric

proof end;

theorem Th13: :: PASCAL:13

for p being FinSequence of REAL
for a, b, c, d, e, f being Real
for u being Point of (TOP-REAL 3)
for M being Matrix of 3,REAL st p = u & M = symmetric_3 (a,b,c,d,e,f) holds
SumAll (QuadraticForm (p,M,p)) = qfconic (a,b,c,(2 * d),(2 * e),(2 * f),u)

proof end;

theorem Th14: :: PASCAL:14

for N being invertible Matrix of 3,F_Real
for NR, M1, M2 being Matrix of 3,REAL
for a, b, c, d, e, f being Real st NR = MXF2MXR N & M1 = symmetric_3 (a,b,c,(d / 2),(f / 2),(e / 2)) & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) holds
MXR2MXF M2 is symmetric

proof end;

theorem Th15: :: PASCAL:15

for a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 being Real st symmetric_3 (a1,a2,a3,a4,a5,a6) = symmetric_3 (b1,b2,b3,b4,b5,b6) holds
( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 & a6 = b6 )

proof end;

theorem Th16: :: PASCAL:16

for a, b, c, d, e, f being Real
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for N being invertible Matrix of 3,F_Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & P in conic (a,b,c,d,e,f) holds
for fa, fb, fc, fd, fe, fi, ff being Real
for M1, M2, NR being Matrix of 3,REAL st M1 = symmetric_3 (a,b,c,(d / 2),(e / 2),(f / 2)) & NR = MXF2MXR N & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) & M2 = symmetric_3 (fa,fe,fi,fb,fc,ff) holds
( ( not fa = 0 or not fe = 0 or not fi = 0 or not fb = 0 or not ff = 0 or not fc = 0 ) & (homography N) . P in conic (fa,fe,fi,(2 * fb),(2 * fc),(2 * ff)) )

proof end;

theorem Th17: :: PASCAL:17

for a, b, c, d, e, f being Real
for P1, P2, P3, P4, P5, P6 being Point of (ProjectiveSpace (TOP-REAL 3))
for N being invertible Matrix of 3,F_Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & P1 in conic (a,b,c,d,e,f) & P2 in conic (a,b,c,d,e,f) & P3 in conic (a,b,c,d,e,f) & P4 in conic (a,b,c,d,e,f) & P5 in conic (a,b,c,d,e,f) & P6 in conic (a,b,c,d,e,f) holds
ex a2, b2, c2, d2, e2, f2 being Real st
( ( not a2 = 0 or not b2 = 0 or not c2 = 0 or not d2 = 0 or not e2 = 0 or not f2 = 0 ) & (homography N) . P1 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P2 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P3 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P4 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P5 in conic (a2,b2,c2,d2,e2,f2) & (homography N) . P6 in conic (a2,b2,c2,d2,e2,f2) )

proof end;

theorem Th18: :: PASCAL:18

for a, b, c, d, e, f being Element of F_Real holds
( ( qfconic (a,b,c,d,e,f,|[1,0,0]|) = 0 implies a = 0 ) & ( qfconic (a,b,c,d,e,f,|[0,1,0]|) = 0 implies b = 0 ) & ( qfconic (a,b,c,d,e,f,|[0,0,1]|) = 0 implies c = 0 ) & ( qfconic (0,0,0,d,e,f,|[1,1,1]|) = 0 implies (d + e) + f = 0 ) )

proof end;

Lm21: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 1 & b = 0 & c = 0 & d = 0 & e = 1 & f = 0 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = i

proof end;

Lm22: for r1, r2, d, e, f, g, h, i being Real st ( r1 <> 0 or r2 <> 0 ) & ((r1 * d) * e) + ((r2 * d) * f) = ((r1 + r2) * e) * f & ((r1 * g) * h) + ((r2 * g) * i) = ((r1 + r2) * h) * i holds
((f * h) * (g - i)) * (d - e) = ((i * e) * (d - f)) * (g - h)

proof end;

Lm23: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 1 & b = 0 & c = 0 & d = 0 & e = 0 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = - h

proof end;

Lm24: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = g - i

proof end;

Lm25: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 0 & b = 0 & c = 1 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = h - g

proof end;

Lm26: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 1 & b = 0 & c = 0 & d = 0 & e = 1 & f = 0 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = i

proof end;

Lm27: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 1 & b = 0 & c = 0 & d = 0 & e = 0 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = - h

proof end;

Lm28: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = g - i

proof end;

Lm29: for a, b, c, d, e, f, g, h, i being Element of F_Real
for M being Matrix of 3,F_Real st a = 0 & b = 0 & c = 1 & d = 1 & e = 1 & f = 1 & M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> holds
Det M = h - g

proof end;

Lm30: for e1, e2, e3, f1, f2, f3 being Element of F_Real
for MABE, MACF, MBDF, MCDE being Matrix of 3,F_Real st MABE = <*<*1,0,0*>,<*0,1,0*>,<*e1,e2,e3*>*> & MACF = <*<*1,0,0*>,<*0,0,1*>,<*f1,f2,f3*>*> & MBDF = <*<*0,1,0*>,<*1,1,1*>,<*f1,f2,f3*>*> & MCDE = <*<*0,0,1*>,<*1,1,1*>,<*e1,e2,e3*>*> holds
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = ((e3 * f2) * (f1 - f3)) * (e1 - e2)

proof end;

Lm31: for e1, e2, e3, f1, f2, f3 being Element of F_Real
for MABF, MACE, MBDE, MCDF being Matrix of 3,F_Real st MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> & MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> & MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> & MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> holds
(((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF) = ((f3 * e2) * (e1 - e3)) * (f1 - f2)

proof end;

theorem Th19: :: PASCAL:19

for e1, e2, e3, f1, f2, f3 being Element of F_Real
for MABF, MABE, MACF, MBDF, MCDE, MACE, MBDE, MCDF being Matrix of 3,F_Real
for r1, r2 being Real st MABE = <*<*1,0,0*>,<*0,1,0*>,<*e1,e2,e3*>*> & MACF = <*<*1,0,0*>,<*0,0,1*>,<*f1,f2,f3*>*> & MBDF = <*<*0,1,0*>,<*1,1,1*>,<*f1,f2,f3*>*> & MCDE = <*<*0,0,1*>,<*1,1,1*>,<*e1,e2,e3*>*> & MABF = <*<*1,0,0*>,<*0,1,0*>,<*f1,f2,f3*>*> & MACE = <*<*1,0,0*>,<*0,0,1*>,<*e1,e2,e3*>*> & MBDE = <*<*0,1,0*>,<*1,1,1*>,<*e1,e2,e3*>*> & MCDF = <*<*0,0,1*>,<*1,1,1*>,<*f1,f2,f3*>*> & ( r1 <> 0 or r2 <> 0 ) & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 holds
(((Det MABE) * (Det MACF)) * (Det MBDF)) * (Det MCDE) = (((Det MABF) * (Det MACE)) * (Det MBDE)) * (Det MCDF)

proof end;

theorem Th20: :: PASCAL:20

for MABF, MABE, MACF, MBDF, MCDE, MACE, MBDE, MCDF being Matrix of 3,F_Real
for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 3) st MABE = <*p1,p2,p5*> & MACF = <*p1,p3,p6*> & MBDF = <*p2,p4,p6*> & MCDE = <*p3,p4,p5*> & MABF = <*p1,p2,p6*> & MACE = <*p1,p3,p5*> & MBDE = <*p2,p4,p5*> & MCDF = <*p3,p4,p6*> holds
( Det MABE = |{p1,p2,p5}| & Det MACF = |{p1,p3,p6}| & Det MBDF = |{p2,p4,p6}| & Det MCDE = |{p3,p4,p5}| & Det MABF = |{p1,p2,p6}| & Det MACE = |{p1,p3,p5}| & Det MBDE = |{p2,p4,p5}| & Det MCDF = |{p3,p4,p6}| )

proof end;

theorem Th21: :: PASCAL:21

for p1, p2, p5, p7, p9 being Point of (TOP-REAL 3) st |{p1,p5,p9}| = 0 holds
|{p1,p5,p7}| * |{p2,p5,p9}| = - (|{p1,p2,p5}| * |{p5,p9,p7}|)

proof end;

theorem Th22: :: PASCAL:22

for p1, p2, p3, p6, p8 being Point of (TOP-REAL 3) st |{p1,p6,p8}| = 0 holds
|{p1,p2,p6}| * |{p3,p6,p8}| = |{p1,p3,p6}| * |{p2,p6,p8}|

proof end;

theorem Th23: :: PASCAL:23

for p2, p4, p5, p7, p9 being Point of (TOP-REAL 3) st |{p2,p4,p9}| = 0 holds
|{p2,p4,p5}| * |{p2,p9,p7}| = - (|{p2,p4,p7}| * |{p2,p5,p9}|)

proof end;

theorem Th24: :: PASCAL:24

for p2, p4, p6, p7, p8 being Point of (TOP-REAL 3) st |{p2,p6,p7}| = 0 holds
|{p2,p4,p7}| * |{p2,p6,p8}| = - (|{p2,p4,p6}| * |{p2,p8,p7}|)

proof end;

theorem Th25: :: PASCAL:25

for p3, p4, p5, p6, p8 being Point of (TOP-REAL 3) st |{p3,p4,p8}| = 0 holds
|{p3,p4,p6}| * |{p3,p5,p8}| = |{p3,p4,p5}| * |{p3,p6,p8}|

proof end;

theorem Th26: :: PASCAL:26

for p1, p3, p5, p7, p8 being Point of (TOP-REAL 3) st |{p3,p5,p7}| = 0 holds
|{p1,p3,p5}| * |{p5,p8,p7}| = - (|{p1,p5,p7}| * |{p3,p5,p8}|)

proof end;

theorem Th27: :: PASCAL:27

for r125, r136, r246, r345, r126, r135, r245, r346, r157, r259, r597, r368, r268, r297, r247, r287, r358, r587 being non zero Real st ((r125 * r136) * r246) * r345 = ((r126 * r135) * r245) * r346 & r157 * r259 = - (r125 * r597) & r126 * r368 = r136 * r268 & r245 * r297 = - (r247 * r259) & r247 * r268 = - (r246 * r287) & r346 * r358 = r345 * r368 & r135 * r587 = - (r157 * r358) holds
r287 * r597 = r297 * r587

proof end;

theorem Th28: :: PASCAL:28

for e1, e2, e3, f1, f2, f3 being Element of F_Real
for r1, r2 being Real
for p1, p2, p3, p4, p5, p6 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 holds
( qfconic (0,0,0,r1,r2,(- (r1 + r2)),p1) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p2) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p3) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p4) = 0 & ((r1 * e1) * e2) + ((r2 * e1) * e3) = ((r1 + r2) * e2) * e3 & ((r1 * f1) * f2) + ((r2 * f1) * f3) = ((r1 + r2) * f2) * f3 )

proof end;

theorem Th29: :: PASCAL:29

for e1, e2, e3, f1, f2, f3 being Element of F_Real
for r1, r2 being Real
for p1, p2, p3, p4, p5, p6, p7, p8, p9 being Point of (TOP-REAL 3) st p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> & p4 = <*1,1,1*> & p5 = <*e1,e2,e3*> & p6 = <*f1,f2,f3*> & |{p1,p2,p5}| <> 0 & |{p1,p3,p6}| <> 0 & |{p2,p4,p6}| <> 0 & |{p3,p4,p5}| <> 0 & |{p1,p2,p6}| <> 0 & |{p1,p3,p5}| <> 0 & |{p2,p4,p5}| <> 0 & |{p3,p4,p6}| <> 0 & |{p1,p5,p7}| <> 0 & |{p2,p5,p9}| <> 0 & |{p5,p9,p7}| <> 0 & |{p3,p6,p8}| <> 0 & |{p2,p6,p8}| <> 0 & |{p2,p9,p7}| <> 0 & |{p2,p4,p7}| <> 0 & |{p2,p8,p7}| <> 0 & |{p3,p5,p8}| <> 0 & |{p5,p8,p7}| <> 0 & ( r1 <> 0 or r2 <> 0 ) & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p5) = 0 & qfconic (0,0,0,r1,r2,(- (r1 + r2)),p6) = 0 & |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 & |{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 & |{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0 holds
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|

proof end;

theorem Th30: :: PASCAL:30

for p2, p5, p7, p8, p9 being Point of (TOP-REAL 3) st |{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}| holds
|{p7,p2,p5}| * |{p7,p8,p9}| = 0

proof end;

::PROVER9
:: set$ignore_option_dependencies$. % GUI handles dependencies
:: if$Prover9$. % Options for Prover9
:: assign$max_seconds, 60$.
:: end_if.
:: if$Mace4$. % Options for Mace4
:: assign$max_seconds, 60$.
:: end_if.
:: formulas$assumptions$.
:: $(x = y$ | $x = z$ | $y = z$) -> f$x,y,z$ #label$COLLSP2$.
:: $(x != y$ & f$x,y,z$ & f$x,y,u$ & f$x,y,v$) -> f$z,u,v$ #label$COLLSP3$.
:: f$x,y,x$ #label$COLLSP5$.
:: f$x,y,z$ -> $f(y,z,x$ & f$z,x,y$ & f$y,x,z$ & f$x,z,y$ & f$z,x,y$) #label$HESSENBE1$.
:: end_of_list.
:: formulas$goals$.
:: -f$x1,x2,x4$ & -f$x1,x2,x5$ &
:: -f$x1,x6,x4$ & -f$x1,x6,x5$ &
:: -f$x2,x6,x4$ & -f$x3,x4,x2$ &
:: -f$x3,x4,x6$ & -f$x3,x5,x2$ &
:: -f$x3,x5,x6$ & -f$x4,x5,x2$ &
:: f$x1,x4,x7$ & f$x1,x5,x8$ &
:: f$x2,x3,x7$ & f$x2,x5,x9$ &
:: f$x6,x3,x8$ & f$x6,x4,x9$
:: -> $-f(x9,x2,x4$ & -f$x1,x4,x9$ &
:: -f$x2,x3,x9$ & -f$x2,x4,x7$ &
:: -f$x2,x5,x8$ & -f$x2,x9,x8$ &
:: -f$x2,x9,x7$ & -f$x6,x4,x8$ &
:: -f$x6,x5,x8$ & -f$x4,x9,x8$ &
:: -f$x4,x9,x7$).
:: end_of_list.
:: ============================== prooftrans ============================
:: Prover9 $32$ version Dec-2007, Dec 2007.
:: Process 10620 was started by RC on ,
:: Wed
:: The command was "/cygdrive/c/Program Files $x86$/Prover9-Mace4/bin-win32/prover9".
:: ============================== end of head ===========================
:: ============================== end of input ==========================
:: ============================== PROOF =================================
:: % -------- Comments from original proof --------
:: % Proof 1 at 0.36 $+ 0.09$ seconds.
:: % Length of proof is 104.
:: % Level of proof is 29.
:: % Maximum clause weight is 44.
:: % Given clauses 786.
:: 1 x = y | x = z | y = z -> f$x,y,z$ # label$COLLSP2$ # label$non_clause$. $$assumption$$ .
:: 2 x != y & f$x,y,z$ & f$x,y,u$ & f$x,y,w$ -> f$z,u,w$ # label$COLLSP3$ # label$non_clause$. $$assumption$$ .
:: 3 f$x,y,z$ -> f$y,z,x$ & f$z,x,y$ & f$y,x,z$ & f$x,z,y$ & f$z,x,y$ # label$HESSENBE1$ # label$non_clause$. $$assumption$$ .
:: 4 -f$x,y,z$ & -f$x,y,u$ & -f$x,w,z$ & -f$x,w,u$ & -f$y,w,z$ & -f$v5,z,y$ & -f$v5,z,w$ & -f$v5,u,y$ & -f$v5,u,w$ & -f$z,u,y$ & f$x,z,v6$ & f$x,u,v7$ & f$y,v5,v6$ & f$y,u,v8$ & f$w,v5,v7$ & f$w,z,v8$ -> -f$v8,y,z$ & -f$x,z,v8$ & -f$y,v5,v8$ & -f$y,z,v6$ & -f$y,u,v7$ & -f$y,v8,v7$ & -f$y,v8,v6$ & -f$w,z,v7$ & -f$w,u,v7$ & -f$z,v8,v7$ & -f$z,v8,v6$ # label$non_clause$ # label$goal$. $$goal$$ .
:: 6 x != y | f$y,z,x$ # label$COLLSP2$. $$clausify(1)$$ .
:: 7 x != y | f$z,y,x$ # label$COLLSP2$. $$clausify(1)$$ .
:: 8 x = y | -f$y,x,z$ | -f$y,x,u$ | -f$y,x,w$ | f$z,u,w$ # label$COLLSP3$. $$clausify(2)$$ .
:: 9 f$x,y,x$ # label$COLLSP5$. $$assumption$$ .
:: 10 -f$x,y,z$ | f$y,z,x$ # label$HESSENBE1$. $$clausify(3)$$ .
:: 11 -f$x,y,z$ | f$z,x,y$ # label$HESSENBE1$. $$clausify(3)$$ .
:: 12 -f$x,y,z$ | f$y,x,z$ # label$HESSENBE1$. $$clausify(3)$$ .
:: 13 -f$x,y,z$ | f$x,z,y$ # label$HESSENBE1$. $$clausify(3)$$ .
:: 14 -f$c1,c2,c3$. $$deny(4)$$ .
:: 15 -f$c1,c2,c4$. $$deny(4)$$ .
:: 16 -f$c1,c5,c3$. $$deny(4)$$ .
:: 17 -f$c1,c5,c4$. $$deny(4)$$ .
:: 18 -f$c2,c5,c3$. $$deny(4)$$ .
:: 19 -f$c6,c3,c2$. $$deny(4)$$ .
:: 20 -f$c6,c3,c5$. $$deny(4)$$ .
:: 21 -f$c6,c4,c2$. $$deny(4)$$ .
:: 22 -f$c6,c4,c5$. $$deny(4)$$ .
:: 23 -f$c3,c4,c2$. $$deny(4)$$ .
:: 24 f$c1,c3,c7$. $$deny(4)$$ .
:: 25 f$c1,c4,c8$. $$deny(4)$$ .
:: 26 f$c2,c6,c7$. $$deny(4)$$ .
:: 27 f$c2,c4,c9$. $$deny(4)$$ .
:: 28 f$c5,c6,c8$. $$deny(4)$$ .
:: 29 f$c5,c3,c9$. $$deny(4)$$ .
:: 30 f$c9,c2,c3$ | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | f$c5,c3,c8$ | f$c5,c4,c8$ | f$c3,c9,c8$ | f$c3,c9,c7$. $$deny(4)$$ .
:: 34 f$x,y,y$. $$xx_res(7,a)$$ .
:: 35 x = y | -f$y,x,z$ | -f$y,x,u$ | f$z,u,y$. $$resolve(9,a,8,d)$$ .
:: 36 x = y | -f$y,x,z$ | -f$y,x,u$ | f$z,y,u$. $$resolve(9,a,8,c)$$ .
:: 37 x = y | -f$y,x,z$ | -f$y,x,u$ | f$y,z,u$. $$resolve(9,a,8,b)$$ .
:: 40 -f$c2,c3,c1$. $$ur(11,b,14,a)$$ .
:: 42 c3 != c2. $$ur(7,b,14,a)$$ .
:: 43 c3 != c1. $$ur(6,b,14,a)$$ .
:: 49 c4 != c2. $$ur(7,b,15,a)$$ .
:: 54 -f$c3,c1,c5$. $$ur(10,b,16,a)$$ .
:: 55 c5 != c3. $$ur(7,b,16,a),flip(a)$$ .
:: 57 -f$c1,c4,c5$. $$ur(13,b,17,a)$$ .
:: 61 c5 != c4. $$ur(7,b,17,a),flip(a)$$ .
:: 63 -f$c5,c2,c3$. $$ur(12,b,18,a)$$ .
:: 64 -f$c5,c3,c2$. $$ur(11,b,18,a)$$ .
:: 70 -f$c2,c6,c3$. $$ur(10,b,19,a)$$ .
:: 79 -f$c4,c6,c2$. $$ur(12,b,21,a)$$ .
:: 86 -f$c5,c6,c4$. $$ur(10,b,22,a)$$ .
:: 92 f$c1,c7,c3$. $$resolve(24,a,13,a)$$ .
:: 99 f$c1,c8,c4$. $$resolve(25,a,13,a)$$ .
:: 108 f$c7,c2,c6$. $$resolve(26,a,11,a)$$ .
:: 113 f$c2,c9,c4$. $$resolve(27,a,13,a)$$ .
:: 120 f$c5,c8,c6$. $$resolve(28,a,13,a)$$ .
:: 127 f$c5,c9,c3$. $$resolve(29,a,13,a)$$ .
:: 130 f$c3,c9,c5$. $$resolve(29,a,10,a)$$ .
:: 132 -f$c5,c3,x$ | -f$c5,c3,y$ | f$x,c9,y$. $$resolve(29,a,8,c),flip(a),unit_del(a,55)$$ .
:: 134 f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | f$c5,c3,c8$ | f$c5,c4,c8$ | f$c3,c9,c8$ | f$c3,c9,c7$ | f$c9,c3,c2$. $$resolve(30,a,13,a)$$ .
:: 142 x = y | -f$y,x,z$ | -f$y,x,u$ | f$z,u,x$. $$resolve(34,a,8,d)$$ .
:: 144 x = y | -f$y,x,z$ | -f$y,x,u$ | f$x,z,u$. $$resolve(34,a,8,b)$$ .
:: 145 -f$c2,c4,c3$. $$ur(8,a,49,a,c,34,a,d,9,a,e,23,a)$$ .
:: 146 -f$c2,c4,c6$. $$ur(8,a,49,a,c,34,a,d,9,a,e,21,a)$$ .
:: 148 -f$c4,c2,c1$. $$ur(8,a,49,a(flip),c,34,a,d,9,a,e,15,a)$$ .
:: 149 -f$c3,c2,c1$. $$ur(8,a,42,a(flip),c,34,a,d,9,a,e,14,a)$$ .
:: 150 f$c7,c3,c1$. $$resolve(92,a,10,a)$$ .
:: 173 x = y | -f$y,x,z$ | f$z,x,y$. $$resolve(35,c,34,a)$$ .
:: 182 -f$c3,c5,c1$. $$ur(35,a,55,a,c,34,a,d,16,a)$$ .
:: 184 -f$c4,c5,c1$. $$ur(35,a,61,a,c,34,a,d,17,a)$$ .
:: 193 f$c8,c4,c1$. $$resolve(99,a,10,a)$$ .
:: 310 c9 = c2 | -f$c2,c9,x$ | f$c2,c4,x$. $$resolve(113,a,37,b)$$ .
:: 311 c9 = c2 | -f$c2,c9,x$ | f$x,c2,c4$. $$resolve(113,a,36,c)$$ .
:: 314 c9 = c2 | -f$c2,c9,x$ | f$c4,x,c2$. $$resolve(113,a,35,b)$$ .
:: 351 c8 = c5 | -f$c5,c8,x$ | f$c6,x,c5$. $$resolve(120,a,35,b)$$ .
:: 389 f$c9,c3,c5$. $$resolve(127,a,10,a)$$ .
:: 413 c9 = c3 | -f$c3,c9,x$ | f$x,c3,c5$. $$resolve(130,a,36,c)$$ .
:: 416 c9 = c3 | -f$c3,c9,x$ | f$c5,x,c3$. $$resolve(130,a,35,b)$$ .
:: 506 -f$c5,c3,x$ | f$c3,c9,x$. $$resolve(132,a,34,a)$$ .
:: 581 c9 = c3 | -f$c9,c3,x$ | f$c5,x,c3$. $$resolve(142,b,389,a),flip(a)$$ .
:: 751 c9 = c3 | -f$c9,c3,x$ | f$c3,x,c5$. $$resolve(144,c,389,a),flip(a)$$ .
:: 755 c8 = c4 | -f$c8,c4,x$ | f$c4,x,c1$. $$resolve(144,c,193,a),flip(a)$$ .
:: 756 c7 = c3 | -f$c7,c3,x$ | f$c3,x,c1$. $$resolve(144,c,150,a),flip(a)$$ .
:: 774 c7 = c2 | -f$c7,c2,x$ | f$c2,x,c6$. $$resolve(144,c,108,a),flip(a)$$ .
:: 797 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | f$c5,c3,c8$ | f$c5,c4,c8$ | f$c3,c9,c8$ | f$c3,c9,c7$. $$resolve(581,b,134,k),unit_del(b,63)$$ .
:: 799 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | f$c5,c3,c8$ | f$c3,c9,c8$ | f$c3,c9,c7$ | f$c8,c4,c5$. $$resolve(797,i,173,b),flip(k),unit_del(k,61)$$ .
:: 843 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | f$c5,c3,c8$ | f$c3,c9,c8$ | f$c3,c9,c7$ | c8 = c4. $$resolve(799,k,755,b),unit_del(l,184)$$ .
:: 847 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | f$c3,c9,c8$ | f$c3,c9,c7$ | c8 = c4. $$resolve(843,h,506,a),merge(k)$$ .
:: 882 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | f$c3,c9,c7$ | c8 = c4 | f$c5,c8,c3$. $$resolve(847,h,416,b),merge(j)$$ .
:: 1055 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | f$c3,c9,c7$ | c8 = c4 | c8 = c5. $$resolve(882,j,351,b),unit_del(k,20)$$ .
:: 1071 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | c8 = c4 | c8 = c5 | f$c7,c3,c5$. $$resolve(1055,h,413,b),merge(j)$$ .
:: 1256 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c8$ | f$c2,c9,c7$ | c8 = c4 | c8 = c5 | c7 = c3. $$resolve(1071,j,756,b),unit_del(k,182)$$ .
:: 1273 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | f$c2,c9,c7$ | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2. $$resolve(1256,f,310,b),merge(k)$$ .
:: 1293 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | f$c7,c2,c4$. $$resolve(1273,f,311,b),merge(j)$$ .
:: 1497 c9 = c3 | f$c1,c3,c9$ | f$c2,c6,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. $$resolve(1293,j,774,b),unit_del(k,146)$$ .
:: 1529 c9 = c3 | f$c1,c3,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2 | f$c2,c9,c6$. $$resolve(1497,c,13,a)$$ .
:: 1809 c9 = c3 | f$c1,c3,c9$ | f$c2,c3,c7$ | f$c2,c4,c8$ | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. $$resolve(1529,j,314,b),merge(j),unit_del(j,79)$$ .
:: 1821 c9 = c3 | f$c1,c3,c9$ | f$c2,c3,c7$ | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2 | f$c8,c4,c2$. $$resolve(1809,d,173,b),unit_del(i,49)$$ .
:: 2066 c9 = c3 | f$c1,c3,c9$ | f$c2,c3,c7$ | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. $$resolve(1821,i,755,b),merge(i),unit_del(i,148)$$ .
:: 2067 c9 = c3 | f$c1,c3,c9$ | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2 | f$c7,c3,c2$. $$resolve(2066,c,173,b),unit_del(h,42)$$ .
:: 2087 c9 = c3 | f$c1,c3,c9$ | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. $$resolve(2067,h,756,b),merge(h),unit_del(h,149)$$ .
:: 2099 c9 = c3 | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2 | f$c9,c3,c1$. $$resolve(2087,b,173,b),unit_del(g,43)$$ .
:: 2339 c9 = c3 | c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. $$resolve(2099,g,751,b),merge(g),unit_del(g,54)$$ .
:: 2346 c8 = c4 | c8 = c5 | c7 = c3 | c9 = c2 | c7 = c2. $$para(2339(a,1),27(a,3)),unit_del(f,145)$$ .
:: 2353 c8 = c4 | c8 = c5 | c7 = c3 | c7 = c2. $$para(2346(d,1),29(a,3)),unit_del(e,64)$$ .
:: 2360 c8 = c4 | c7 = c3 | c7 = c2. $$para(2353(b,1),25(a,3)),unit_del(d,57)$$ .
:: 2367 c7 = c3 | c7 = c2. $$para(2360(a,1),28(a,3)),unit_del(c,86)$$ .
:: 2374 c7 = c2. $$para(2367(a,1),26(a,3)),unit_del(b,70)$$ .
:: 2470 $F. [back_rewrite(150),rewrite([2374(1)]),unit_del(a,40)].
:: ============================== end of proof ==========================
:: OTT2MIZ (J. URBAN)

theorem Th31: :: PASCAL:31

for PCPP being CollProjectiveSpace
for c1, c2, c3, c4, c5, c6, c7, c8, c9 being Element of PCPP st not c1,c2,c4 are_collinear & not c1,c2,c5 are_collinear & not c1,c6,c4 are_collinear & not c1,c6,c5 are_collinear & not c2,c6,c4 are_collinear & not c3,c4,c2 are_collinear & not c3,c4,c6 are_collinear & not c3,c5,c2 are_collinear & not c3,c5,c6 are_collinear & not c4,c5,c2 are_collinear & c1,c4,c7 are_collinear & c1,c5,c8 are_collinear & c2,c3,c7 are_collinear & c2,c5,c9 are_collinear & c6,c3,c8 are_collinear & c6,c4,c9 are_collinear holds
( not c9,c2,c4 are_collinear & not c1,c4,c9 are_collinear & not c2,c3,c9 are_collinear & not c2,c4,c7 are_collinear & not c2,c5,c8 are_collinear & not c2,c9,c8 are_collinear & not c2,c9,c7 are_collinear & not c6,c4,c8 are_collinear & not c6,c5,c8 are_collinear & not c4,c9,c8 are_collinear & not c4,c9,c7 are_collinear )

proof end;

definition

let P1, P2, P3, P4, P5, P6, P7, P8, P9 be Point of (ProjectiveSpace (TOP-REAL 3));

pred P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration means :: PASCAL:def 4
( not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not P1,P2,P5 are_collinear & not P1,P2,P6 are_collinear & not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear & not P2,P4,P5 are_collinear & not P2,P4,P6 are_collinear & not P3,P4,P5 are_collinear & not P3,P4,P6 are_collinear & not P2,P3,P5 are_collinear & not P2,P3,P6 are_collinear & not P4,P5,P1 are_collinear & not P4,P6,P1 are_collinear & not P5,P6,P1 are_collinear & not P5,P6,P2 are_collinear & P1,P5,P9 are_collinear & P1,P6,P8 are_collinear & P2,P4,P9 are_collinear & P2,P6,P7 are_collinear & P3,P4,P8 are_collinear & P3,P5,P7 are_collinear );

end;

:: deftheorem defines are_in_Pascal_configuration PASCAL:def 4 :
for P1, P2, P3, P4, P5, P6, P7, P8, P9 being Point of (ProjectiveSpace (TOP-REAL 3)) holds
( P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration iff ( not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not P1,P2,P5 are_collinear & not P1,P2,P6 are_collinear & not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear & not P2,P4,P5 are_collinear & not P2,P4,P6 are_collinear & not P3,P4,P5 are_collinear & not P3,P4,P6 are_collinear & not P2,P3,P5 are_collinear & not P2,P3,P6 are_collinear & not P4,P5,P1 are_collinear & not P4,P6,P1 are_collinear & not P5,P6,P1 are_collinear & not P5,P6,P2 are_collinear & P1,P5,P9 are_collinear & P1,P6,P8 are_collinear & P2,P4,P9 are_collinear & P2,P6,P7 are_collinear & P3,P4,P8 are_collinear & P3,P5,P7 are_collinear ) );

theorem Th32: :: PASCAL:32

for P1, P2, P3, P4, P5, P6, P7, P8, P9 being Point of (ProjectiveSpace (TOP-REAL 3)) st P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration holds
( not P7,P2,P5 are_collinear & not P1,P5,P7 are_collinear & not P2,P4,P7 are_collinear & not P2,P5,P9 are_collinear & not P2,P6,P8 are_collinear & not P2,P7,P8 are_collinear & not P2,P7,P9 are_collinear & not P3,P5,P8 are_collinear & not P3,P6,P8 are_collinear & not P5,P7,P8 are_collinear & not P5,P7,P9 are_collinear )

proof end;

theorem Th33: :: PASCAL:33

for P1, P2, P3, P4, P5, P6, P7, P8, P9 being Point of (ProjectiveSpace (TOP-REAL 3))
for a, b, c, d, e, f being Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & {P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear & not P7,P2,P5 are_collinear & not P1,P2,P5 are_collinear & not P1,P2,P6 are_collinear & not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear & not P1,P5,P7 are_collinear & not P2,P4,P5 are_collinear & not P2,P4,P6 are_collinear & not P2,P4,P7 are_collinear & not P2,P5,P9 are_collinear & not P2,P6,P8 are_collinear & not P2,P7,P8 are_collinear & not P2,P7,P9 are_collinear & not P3,P4,P5 are_collinear & not P3,P4,P6 are_collinear & not P3,P5,P8 are_collinear & not P3,P6,P8 are_collinear & not P5,P7,P8 are_collinear & not P5,P7,P9 are_collinear & P1,P5,P9 are_collinear & P1,P6,P8 are_collinear & P2,P4,P9 are_collinear & P2,P6,P7 are_collinear & P3,P4,P8 are_collinear & P3,P5,P7 are_collinear holds
P7,P8,P9 are_collinear

proof end;

theorem Th34: :: PASCAL:34

for P1, P2, P3, P4, P5, P6, P7, P8, P9 being Point of (ProjectiveSpace (TOP-REAL 3))
for a, b, c, d, e, f being Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & {P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & not P1,P2,P3 are_collinear & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration holds
P7,P8,P9 are_collinear

proof end;

registration

cluster TOP-REAL 3 -> up-3-dimensional ;

coherence
TOP-REAL 3 is up-3-dimensional

proof end;

end;

theorem Th35: :: PASCAL:35

for P1, P2, P3, P4, P5, P6, P7, P8, P9 being Point of (ProjectiveSpace (TOP-REAL 3))
for a, b, c, d, e, f being Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & {P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & P1,P2,P3 are_collinear & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration holds
P7,P8,P9 are_collinear

proof end;

:: Pascal's theorem

theorem :: PASCAL:36

for P1, P2, P3, P4, P5, P6, P7, P8, P9 being Point of (ProjectiveSpace (TOP-REAL 3))
for a, b, c, d, e, f being Real st ( not a = 0 or not b = 0 or not c = 0 or not d = 0 or not e = 0 or not f = 0 ) & {P1,P2,P3,P4,P5,P6} c= conic (a,b,c,d,e,f) & P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration holds
P7,P8,P9 are_collinear

proof end;