:: Pascal's Theorem in Real Projective Plane
:: by Roland Coghetto
::
:: Received June 27, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REAL_1, XCMPLX_0, ANPROJ_1, PENCIL_1, MCART_1, EUCLID_5,
ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, EUCLID, FINSEQ_1, FUNCT_1, MATRIX_1,
MATRIX_3, NAT_1, NUMBERS, PRE_TOPC, QC_LANG1, RELAT_1, RVSUM_1, STRUCT_0,
SUBSET_1, SUPINF_2, TARSKI, TREES_1, VECTSP_1, XXREAL_0, MATRIX_6,
MESFUNC1, MATRIXR1, MATRIXR2, FINSEQ_2, ANPROJ_8, ANPROJ_9, PASCAL,
RELAT_2, MATRIXC1, PRALG_1, COLLSP, ANPROJ_2, INCSP_1;
notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1, FINSEQ_1,
FINSEQ_4, PRE_TOPC, RVSUM_1, EUCLID, DOMAIN_1, ANPROJ_1, TARSKI,
XXREAL_0, FUNCT_2, VECTSP_1, MATRIX_0, MATRIX_1, MATRIX_3, GROUP_1,
RLVECT_1, EUCLID_5, FINSEQ_2, LAPLACE, MATRIXR1, MATRIXR2, MATRIX_6,
ANPROJ_8, MATRPROB, ANPROJ_9, STRUCT_0, COLLSP, ANPROJ_2;
constructors BINOP_2, FINSEQ_4, MONOID_0, EUCLID_5, MATRIX13, REALSET1,
ANPROJ_2, LAPLACE, MATRIXR2, ANPROJ_8, MATRPROB, ANPROJ_9, MATRIX_3;
registrations ANPROJ_1, FUNCT_1, STRUCT_0, VECTSP_1, REVROT_1, MATRIX_0,
RELSET_1, NUMBERS, XREAL_0, MEMBERED, MONOID_0, EUCLID, VALUED_0,
FINSEQ_2, MATRIX_6, SUBSET_1, RLTOPSP1, XCMPLX_0, ANPROJ_2;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions TARSKI, ANPROJ_2;
equalities VECTSP_1, STRUCT_0, ANPROJ_9, MATRIXR2;
expansions STRUCT_0, MATRIXR2;
theorems MATRIX_9, EUCLID_5, ANPROJ_1, ANPROJ_2, XREAL_0, EUCLID, MATRIXR2,
FINSEQ_2, XCMPLX_1, RVSUM_1, MATRIX_0, FINSEQ_1, ENUMSET1, EUCLID_8,
LAPLACE, MATRIX_6, MATRIXR1, MATRIX_3, TARSKI, ANPROJ_8, MATRIX_5,
MATRPROB, ANPROJ_9, ORDINAL1, MATRIX_4, MATRIX14, HESSENBE, COLLSP;
begin :: Preliminaries
reserve n for Nat;
reserve K for Field;
reserve a,b,c,d,e,f,g,h,i,a1,b1,c1,d1,e1,f1,g1,h1,i1 for Element of K;
reserve M,N for Matrix of 3,K;
reserve p for FinSequence of REAL;
theorem Th01:
for p,q,r being Point of TOP-REAL 3 holds
|{p,q,r}| = |{r,p,q}| & |{p,q,r}| = |{q,r,p}|
proof
let p,q,r be Point of TOP-REAL 3;
thus |{p,q,r}| = - |{p,r,q}| by ANPROJ_8:29
.= |{r,p,q}| by ANPROJ_8:30;
thus |{p,q,r}| = - |{q,p,r}| by ANPROJ_8:30
.= |{q,r,p}| by ANPROJ_8:29;
end;
theorem Th02:
<* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *> =
<* <* a1,b1,c1 *>,
<* d1,e1,f1 *>,
<* g1,h1,i1 *> *>
implies
a = a1 & b = b1 & c = c1 &
d = d1 & e = e1 & f = f1 &
g = g1 & h = h1 & i = i1
proof
assume <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *> =
<* <* a1,b1,c1 *>,
<* d1,e1,f1 *>,
<* g1,h1,i1 *> *>;
then <*a,b,c*> = <*a1,b1,c1*> &
<*d,e,f*> = <*d1,e1,f1*> &
<*g,h,i*> = <*g1,h1,i1*> by FINSEQ_1:78;
hence thesis by FINSEQ_1:78;
end;
theorem Th03:
ex a,b,c,d,e,f,g,h,i st
M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *>
proof
reconsider 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) as Element of K;
take a,b,c,d,e,f,g,h,i;
thus thesis by MATRIXR2:37;
end;
theorem Th04:
M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *>
implies
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
assume M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *>;
then
A1: M.1 = <*a,b,c*> & M.2 = <*d,e,f*> &
M.3 = <*g,h,i*> by FINSEQ_1:45;
A2: [1,1] in Indices M & [1,2] in Indices M & [1,3] in Indices M &
[2,1] in Indices M & [2,2] in Indices M &
[2,3] in Indices M &[3,1] in Indices M & [3,2] in Indices M &
[3,3] in Indices M by MATRIX_0:24,ANPROJ_8:1;
then ex s be FinSequence of K st s = M.1 & M*(1,1) = s.1
by MATRIX_0:def 5;
hence M*(1,1) = a by A1,FINSEQ_1:45;
ex s be FinSequence of K st s = M.1 & M*(1,2) = s.2
by A2,MATRIX_0:def 5;
hence M*(1,2) = b by A1,FINSEQ_1:45;
ex s be FinSequence of K st s = M.1 & M*(1,3) = s.3
by A2,MATRIX_0:def 5;
hence M*(1,3) = c by A1,FINSEQ_1:45;
ex s be FinSequence of K st s = M.2 & M*(2,1) = s.1
by A2,MATRIX_0:def 5;
hence M*(2,1) = d by A1,FINSEQ_1:45;
ex s be FinSequence of K st s = M.2 & M*(2,2) = s.2
by A2,MATRIX_0:def 5;
hence M*(2,2) = e by A1,FINSEQ_1:45;
ex s be FinSequence of K st s = M.2 & M*(2,3) = s.3
by A2,MATRIX_0:def 5;
hence M*(2,3) = f by A1,FINSEQ_1:45;
ex s be FinSequence of K st s = M.3 & M*(3,1) = s.1
by A2,MATRIX_0:def 5;
hence M*(3,1) = g by A1,FINSEQ_1:45;
ex s be FinSequence of K st s = M.3 & M*(3,2) = s.2
by A2,MATRIX_0:def 5;
hence M*(3,2) = h by A1,FINSEQ_1:45;
ex s be FinSequence of K st s = M.3 & M*(3,3) = s.3
by A2,MATRIX_0:def 5;
hence M*(3,3) = i by A1,FINSEQ_1:45;
end;
theorem Th05:
M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *>
implies
M@ = <* <* a,d,g *>,
<* b,e,h *>,
<* c,f,i *> *>
proof
assume M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *>;
then
A1: 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) by Th04;
consider ap,bp,cp,dp,ep,fp,gp,hp,ip being Element of K such that
A2: M@ = <* <* ap,bp,cp *>,
<* dp,ep,fp *>,
<* gp,hp,ip *> *> by Th03;
A3: ap = M@*(1,1) & bp = M@*(1,2) & cp = M@*(1,3) & dp = M@*(2,1) &
ep = M@*(2,2) & fp = M@*(2,3) & gp = M@*(3,1) & hp = M@*(3,2) &
ip = M@*(3,3) by A2,Th04;
[1,1] in Indices M & [1,2] in Indices M & [1,3] in Indices M &
[2,1] in Indices M & [2,2] in Indices M & [2,3] in Indices M &
[3,1] in Indices M & [3,2] in Indices M & [3,3] in Indices M
by MATRIX_0:24,ANPROJ_8:1;
then M*(1,1) = (M@)*(1,1) & M*(1,2) = (M@)*(2,1) &
M*(1,3) = (M@)*(3,1) & M*(2,1) = (M@)*(1,2) &
M*(2,2) = (M@)*(2,2) & M*(2,3) = (M@)*(3,2) &
M*(3,1) = (M@)*(1,3) & M*(3,2) = (M@)*(2,3) &
M*(3,3) = (M@)*(3,3) by MATRIX_0:def 6;
hence thesis by A2,A1,A3;
end;
theorem Th06:
M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *> &
M is symmetric implies b = d & c = g & h = f
proof
assume that
A1: M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *> and
A2: M is symmetric;
A3: M = M@ by A2,MATRIX_6:def 5;
M@ = <* <* a, d, g *>,
<* b, e, h *>,
<* c, f, i *> *> by A1,Th05;
hence thesis by A1,A3,Th02;
end;
theorem Th07:
for M,N being Matrix of 3,F_Real st
N is symmetric holds M@ * N * M is symmetric
proof
let M,N be Matrix of 3,F_Real;
assume
A1: N is symmetric;
A2: len N = 3 & width N = 3 & len M = 3 & width M = 3 by MATRIX_0:24;
then
A3: width (M@) = len N & width N = len M by MATRIX_0:29;
width (M@) = len N & width N <> 0 by A2,MATRIX_0:29;
then
A4: (M@ * N)@ = (N@) * (M@@) by MATRIX_3:22
.= (N@) * M by A2,MATRIX_0:57;
width (M@ * N) = len M & width M <> 0 by MATRIX_0:24,A2;
then ((M@ * N) * M)@ = (M@) * (M@ * N)@ by MATRIX_3:22
.= (M@) * (N * M) by A4,A1,MATRIX_6:def 5
.= (M@ * N) * M by A3,MATRIX_3:33;
hence thesis by MATRIX_6:def 5;
end;
theorem Th08:
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
let M be Matrix of 3,F_Real;
let a,b,c,d,e,f,g,h,i,x,y,z being Element of F_Real;
let v being Element of TOP-REAL 3;
let uf being FinSequence of F_Real;
let p being FinSequence of (1-tuples_on REAL);
assume
A1: p = M * uf & v = M2F p &
M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *> &
uf = <* x,y,z *>;
then
A2: len uf = 3 by FINSEQ_1:45;
A3: len <*uf*> = 1 by FINSEQ_1:39;
rng <*uf*> = {uf} by FINSEQ_1:39;
then uf in rng <*uf*> by TARSKI:def 1; then
A4: width <*uf*> = 3 by A2,A3,MATRIX_0:def 3; then
A5: width (<*uf*>@) = len <*uf*> by MATRIX_0:29
.= 1 by FINSEQ_1:39;
len (<*uf*>@) = 3 by MATRIX_0:def 6,A4; then
A6: <*uf*>@ is Matrix of 3,1,F_Real by A5,MATRIX_0:20;
uf.1 = x & uf.2 = y & uf.3 = z by A1,FINSEQ_1:45; then
A8: <*uf*>@ = <* <* x *>,<* y *>, <* z *> *> by A2,ANPROJ_8:77;
thus
A9: p = M * <*uf*>@ by A1,LAPLACE:def 9
.= <* <* a * x + b * y + c * z *>,
<* d * x + e * y + f * z *>,
<* g * x + h * y + i * z *> *>
by A1,A8,A6,ANPROJ_9:7;
now
thus len p = 3 by A9,FINSEQ_1:45;
p.1 = <* a * x + b * y + c * z *> by A9,FINSEQ_1:45;
hence (p.1).1 = a * x + b * y + c * z by FINSEQ_1:40;
p.2 = <* d * x + e * y + f * z *> by A9,FINSEQ_1:45;
hence (p.2).1 = d * x + e * y + f * z by FINSEQ_1:40;
p.3 = <* g * x + h * y + i * z *> by A9,FINSEQ_1:45;
hence (p.3).1 = g * x + h * y + i * z by FINSEQ_1:40;
end;
hence thesis by A1,ANPROJ_8:def 2;
end;
Lm01:
for N1,M,N2 being Matrix of 3,REAL st
len p = 3 holds
(N1 * M * N2) * p = N1 * ( M * ( N2 * p))
proof
let N1,M,N2 being Matrix of 3,REAL;
assume
A1: len p = 3;
A2: width M = 3 & len M = 3 & width N1 = 3 & len N2 = 3 & width N2 = 3
by MATRIX_0:24;
A3: len(N2 * p) = 3 by A1,A2,MATRIXR1:61;
A4: len p = width N2 & width (N1 * M) = len N2 & len p > 0 & len N2 > 0
by MATRIXR2:4,A2,A1;
N1 * (M * (N2 * p)) = (N1 * M) * (N2 * p) by A3,A2,MATRIXR2:59
.= (N1 * M * N2) * p by A4,MATRIXR2:59;
hence thesis;
end;
Lm02:
for N,M being Matrix of 3,REAL holds
len p = 3 implies |( N * p, M * (N * p) )| = |( p, (N@ * M * N) * p )|
proof
let N,M being Matrix of 3,REAL;
assume
A1: len p = 3;
A2: len N = 3 by MATRIX_0:24;
A3: len M = 3 by MATRIX_0:24;
A4: width N = 3 by MATRIX_0:24;
A5: width M = 3 by MATRIX_0:24;
width N = len p & len p > 0 by A1,MATRIX_0:24;
then width M = len (N * p) & len(N * p) > 0 by A2,A4,A5,MATRIXR1:61;
then len (M * (N * p)) = len N by A2,A3,MATRIXR1:61;
then |( N * p, M * (N * p) )| = |( p, N@ * (M * (N * p)) )|
by A2,A4,A1,MATRPROB:48
.= |( p, (N@ * M * N) * p )| by A1,Lm01;
hence thesis;
end;
Lm03:
for NR,M being Matrix of 3,REAL holds
MXF2MXR((MXR2MXF(NR@))~) * M * MXF2MXR((MXR2MXF NR)~) is
Matrix of 3,REAL
proof
let NR,M be Matrix of 3,REAL;
now
reconsider M6 = MXF2MXR((MXR2MXF(NR@))~) as Matrix of 3,REAL
by MATRIXR1:def 2;
M6 * M is Matrix of 3,REAL;
hence MXF2MXR((MXR2MXF(NR@))~) * M is Matrix of 3,REAL;
thus MXF2MXR((MXR2MXF(NR))~) is Matrix of 3,REAL by MATRIXR1:def 2;
end;
then reconsider M3 = MXF2MXR((MXR2MXF(NR@))~) * M,
M4 = MXF2MXR((MXR2MXF(NR))~) as Matrix of 3,REAL;
M3 * M4 is Matrix of 3,REAL;
hence thesis;
end;
Lm04:
for A,B,C,D,E being Matrix of n,REAL holds
A * (B * C * D) * E = (A * B) * C * (D * E)
proof
let A,B,C,D,E being Matrix of n,REAL;
A * (B * C * D) * E = A * (B * (C * D)) * E by MATRIXR2:28
.= A * ((B * (C * D)) * E) by MATRIXR2:28
.= A * ((B * ((C * D) * E))) by MATRIXR2:28
.= A * ((B * (C * (D * E)))) by MATRIXR2:28
.= A * ((B * C) * (D * E)) by MATRIXR2:28
.= (A * (B * C)) * (D * E) by MATRIXR2:28
.= (A * B) * C * (D * E) by MATRIXR2:28;
hence thesis;
end;
Lm05:
for A,B being Matrix of n,F_Real holds
MXF2MXR (A * B) = MXF2MXR A * MXF2MXR B
proof
let A,B being Matrix of n,F_Real;
(MXF2MXR A) * (MXF2MXR B) = MXF2MXR
(MXR2MXF(MXF2MXR A) * MXR2MXF(MXF2MXR B))
by MATRIXR1:def 6
.= MXF2MXR (A * MXR2MXF(MXF2MXR B)) by ANPROJ_8:16
.= MXF2MXR (A * B) by ANPROJ_8:16;
hence thesis;
end;
Lm06:
for A being Matrix of REAL holds MXF2MXR MXR2MXF A = A
proof
let A being Matrix of REAL;
MXF2MXR MXR2MXF A = MXR2MXF A by MATRIXR1:def 2
.= A by MATRIXR1:def 1;
hence thesis;
end;
Lm07:
for A,B being Matrix of n,REAL holds MXR2MXF (A * B) = MXR2MXF A * MXR2MXF B
proof
let A,B being Matrix of n,REAL;
A * B = (MXF2MXR MXR2MXF A) * B by Lm06
.= (MXF2MXR MXR2MXF A) * (MXF2MXR MXR2MXF B) by Lm06
.= MXF2MXR (MXR2MXF A * MXR2MXF B) by Lm05;
hence thesis by ANPROJ_8:16;
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
let N being invertible Matrix of 3,F_Real;
let NR being Matrix of 3,REAL;
assume
A1: NR = MXF2MXR N;
A2: N~ is_reverse_of N by MATRIX_6:def 4;
NR * (MXF2MXR((MXR2MXF NR)~)) = MXF2MXR N * (MXF2MXR (N~))
by A1,ANPROJ_8:16
.= MXF2MXR (N * N~) by Lm05
.= 1_Rmatrix(3) by A2,MATRIX_6:def 2 ;
hence thesis;
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
let N being invertible Matrix of 3,F_Real;
let NR being Matrix of 3,REAL;
assume NR = MXF2MXR N;
then NR@ = N@ by MATRIXR1:def 2; then
NR@ = MXF2MXR N@ by MATRIXR1:def 2;
hence thesis by Lm08;
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
let N being invertible Matrix of 3,F_Real;
let NR being Matrix of 3,REAL;
assume
A1: NR = MXF2MXR N;
A2: N~ is_reverse_of N by MATRIX_6:def 4;
(MXF2MXR((MXR2MXF NR)~)) * NR = (MXF2MXR (N~)) * MXF2MXR N
by A1,ANPROJ_8:16
.= MXF2MXR (N~ * N) by Lm05
.= 1_Rmatrix(3) by A2,MATRIX_6:def 2 ;
hence thesis;
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
let N being invertible Matrix of 3,F_Real;
let NR being Matrix of 3,REAL;
assume NR = MXF2MXR N;
then NR@ = N@ by MATRIXR1:def 2; then
NR@ = MXF2MXR N@ by MATRIXR1:def 2;
hence thesis by Lm10;
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
let N being invertible Matrix of 3,F_Real;
let NR being Matrix of 3,REAL;
assume
A1: NR = MXF2MXR N;
reconsider C = (MXR2MXF (NR@))~ as Matrix of 3,F_Real;
reconsider B = (MXF2MXR((MXR2MXF (NR@))~)) as Matrix of 3,REAL
by MATRIXR1:def 2;
(NR@) * B = 1_Rmatrix(3) & B * (NR@) = 1_Rmatrix(3)
by A1,Lm11,Lm09;
hence thesis;
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
let N being invertible Matrix of 3,F_Real;
let NR,M,M2 being Matrix of 3,REAL;
assume that
A1: NR = MXF2MXR N and
A2: M2 = (MXF2MXR((MXR2MXF(NR@))~)) * M * (MXF2MXR((MXR2MXF NR)~));
reconsider NI = MXF2MXR((MXR2MXF NR)~), NJ = MXF2MXR((MXR2MXF (NR@))~) as
Matrix of 3,REAL by MATRIXR1:def 2;
A3: NI * NR = 1_Rmatrix(3) by A1,Lm10;
(NR@) * M2 * NR = ((NR@) * NJ) * M * (NI * NR) by A2,Lm04
.= 1_Rmatrix(3) * M * 1_Rmatrix(3) by A1,Lm09,A3
.= M * 1_Rmatrix(3) by MATRIXR2:70
.= M by MATRIXR2:71;
hence thesis;
end;
Lm14:
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
let N being invertible Matrix of n,F_Real;
let M being Matrix of n,REAL;
assume
A1: M = MXF2MXR N;
A2: N~ is_reverse_of N by MATRIX_6:def 4;
reconsider M2 = MXF2MXR (N~) as Matrix of n,REAL by MATRIXR1:def 2;
now
thus M * M2 = 1_Rmatrix(n)
proof
M * M2 = MXF2MXR (N * (N~)) by A1,Lm05
.= 1_Rmatrix(n) by A2,MATRIX_6:def 2;
hence thesis;
end;
thus M2 * M = 1_Rmatrix(n)
proof
M2 * M = MXF2MXR (N~ * N) by A1,Lm05
.= 1_Rmatrix(n) by A2,MATRIX_6:def 2;
hence thesis;
end;
end;
hence thesis;
end;
Lm15:
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
let N being Matrix of n,F_Real;
let M being Matrix of n,REAL;
assume that
A1: M is invertible and
A2: N = MXR2MXF M;
consider MI be Matrix of n,REAL such that
A3: MI * M = 1_Rmatrix(n) and
A4: M * MI = 1_Rmatrix(n) by A1;
reconsider NI = MXR2MXF MI as Matrix of n,F_Real;
now
A5: N * NI = MXR2MXF (M * MI) by A2,Lm07
.= 1.(F_Real,n) by A4,ANPROJ_8:16;
A6: NI * N = MXR2MXF (MI * M) by A2,Lm07
.= 1.(F_Real,n) by A3,ANPROJ_8:16;
thus N * NI = NI * N by A5,A6;
thus N * NI = 1.(F_Real,n) by A5;
end;
hence thesis by MATRIX_6:def 2,def 3;
end;
theorem Th09:
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
let M being Matrix of 3,REAL;
let a,b,c,d,e,f,g,h,i,p1,p2,p3 being Element of REAL;
assume that
A1: M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *> and
A2: p = <* p1,p2,p3 *>;
A3: p.1 = p1 & p.2 = p2 & p.3 = p3 by A2,FINSEQ_1:45;
p = |[ p1,p2,p3 ]| by A2;
then reconsider ru = p as Element of REAL 3 by EUCLID:22;
A4: MXR2MXF ColVec2Mx p = <* ru *>@ by ANPROJ_8:72;
reconsider a,b,c,d,e,f,g,h,i as Element of F_Real;
reconsider fu1 = ru.1,fu2 = ru.2,fu3 = ru.3 as Element of F_Real
by XREAL_0:def 1;
A5: <* ru *>@ = <* <* fu1 *>,<* fu2 *>,<* fu3 *> *>
by EUCLID_8:50,ANPROJ_8:77;
A6: len ru = 3 by EUCLID_8:50;
A7: len <*ru*> = 1 by FINSEQ_1:39;
rng <*ru*> = {ru} by FINSEQ_1:39;
then ru in rng <*ru*> by TARSKI:def 1; then
A8: width <*ru*> = 3 by A6,A7,MATRIX_0:def 3; then
A9: width (<*ru*>@) = len <*ru*> by MATRIX_0:29
.= 1 by FINSEQ_1:39;
A10: len (<*ru*>@) = 3 by MATRIX_0:def 6,A8; then
A11: <*ru*>@ is Matrix of 3,1,F_Real by A9,MATRIX_0:20;
reconsider M2 = <*ru*>@ as Matrix of 3,1,F_Real by A10,A9,MATRIX_0:20;
A12: M * ColVec2Mx p = M * (<* ru *>@) by A4,MATRIXR1:def 1
.= MXF2MXR((MXR2MXF M) * (MXR2MXF (<*ru*>@)))
by MATRIXR1:def 6;
A13: MXR2MXF (<*ru*>@) is Matrix of 3,1,F_Real by MATRIXR1:def 1,A11;
A14: MXR2MXF (<*ru*>@) = <* <* fu1 *>,<* fu2 *>,<* fu3 *> *>
by A5,MATRIXR1:def 1;
A15:(MXR2MXF M) * (MXR2MXF (<*ru*>@)) =
<* <* a * fu1 + b * fu2 + c * fu3 *>,
<* d * fu1 + e * fu2 + f * fu3 *>,
<* g * fu1 + h * fu2 + i * fu3 *> *>
by A13,A1,MATRIXR1:def 1,A14,ANPROJ_9:7;
reconsider q = <* a * fu1 + b * fu2 + c * fu3,
d * fu1 + e * fu2 + f * fu3,
g * fu1 + h * fu2 + i * fu3 *> as FinSequence of REAL;
A16: q.1 = a * fu1 + b * fu2 + c * fu3 &
q.2 = d * fu1 + e * fu2 + f * fu3 &
q.3 = g * fu1 + h * fu2 + i * fu3 by FINSEQ_1:45;
q = |[ a * fu1 + b * fu2 + c * fu3,
d * fu1 + e * fu2 + f * fu3,
g * fu1 + h * fu2 + i * fu3 ]|;
then reconsider rq = q as Element of REAL 3 by EUCLID:22;
reconsider qf = q as FinSequence of F_Real;
A17: len q = 3 by FINSEQ_1:45;
A18: ColVec2Mx rq = MXR2MXF ColVec2Mx rq by MATRIXR1:def 1
.= <*qf*>@ by ANPROJ_8:72;
then
A19: ColVec2Mx rq = F2M q by A17,ANPROJ_8:88
.= <* <* a * fu1 + b * fu2 + c * fu3 *>,
<* d * fu1 + e * fu2 + f * fu3 *>,
<* g * fu1 + h * fu2 + i * fu3 *> *>
by A16,A17,ANPROJ_8:def 1
.= M * ColVec2Mx p by A15,A12,MATRIXR1:def 2;
M * p = Col(ColVec2Mx rq,1) by A19,MATRIXR1:def 11
.= <* a * fu1 + b * fu2 + c * fu3,
d * fu1 + e * fu2 + f * fu3,
g * fu1 + h * fu2 + i * fu3 *> by A18,ANPROJ_8:93;
hence thesis by A3;
end;
Lm16:
for M being Matrix of 3,REAL st p = 0.TOP-REAL 3
holds M * p = p
proof
let M being Matrix of 3,REAL;
assume
A1: p = 0.TOP-REAL 3;
consider a,b,c,d,e,f,g,h,i being Element of REAL such that
A2: MXR2MXF M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *> by Th03;
A3: M = <* <* a,b,c *>,
<* d,e,f *>,
<* g,h,i *> *> by A2,MATRIXR1:def 1;
set u = 0.TOP-REAL 3;
A4: p.1 = 0 & p.2 = 0 & p.3 = 0 by A1,EUCLID_5:4,FINSEQ_1:45;
reconsider r1 = p.1, r2 = p.2, r3 = p.3 as Element of REAL
by XREAL_0:def 1;
A5: p = <* r1,r2,r3 *> by A1,EUCLID_5:4,A4;
M * p = <* a * r1 + b * r2 + c * r3,
d * r1 + e * r2 + f * r3,
g * r1 + h * r2 + i * r3 *>
by A3,A5,Th09
.= <* 0,0,0 *> by A4;
hence thesis by A1,EUCLID_5:4;
end;
Lm17:
<* <* 0,0,0 *>,
<* 0,0,0 *>,
<* 0,0,0 *> *> = 0.(F_Real,3,3)
proof
A1: 0.(F_Real,3,3) = 3 |-> (3|-> 0.F_Real) by MATRIX_3:def 1;
3 |-> 0.F_Real = <* 0,0,0 *> by FINSEQ_2:62;
hence thesis by A1,FINSEQ_2:62;
end;
Lm18:
<* <* 0,0,0 *>,
<* 0,0,0 *>,
<* 0,0,0 *> *> = 0_Rmatrix(3)
proof
0_Rmatrix(3) = MXF2MXR (0.(F_Real,3,3)) by MATRIXR1:def 8;
hence thesis by MATRIXR1:def 2,Lm17;
end;
Lm19:
for M being Matrix of n,K holds M * 0.(K,n,n) = 0.(K,n,n)
proof
let M be Matrix of n,K;
A2: len 0.(K,n,n) = len 0.(K,n,n) & width 0.(K,n,n) = width 0.(K,n,n);
A3: len M = n & width M = n & len 0.(K,n,n) = n by MATRIX_0:24;
reconsider M0 = M * (0.(K,n,n)) as Matrix of K;
A4: len M0 = n & width M0 = n by MATRIX_0:24;
M * (0.(K,n,n)) = M * ((0.(K,n,n))+(0.(K,n,n))) by MATRIX_3:4
.= M * (0.(K,n,n)) + M * (0.(K,n,n))
by A2,A3,MATRIX_4:62;
hence thesis by A4,MATRIX_4:6;
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
let M be Matrix of 3,REAL;
A1: width MXR2MXF M = 3 & len MXR2MXF M = 3 by MATRIX_0:24;
0.(F_Real,3,3) = MXR2MXF M * 0.(F_Real,3,3) by Lm19;
hence 0_Rmatrix(3) = MXF2MXR (MXR2MXF M * 0.(F_Real,3,3)) by MATRIXR1:def 8
.= MXF2MXR MXR2MXF M * MXF2MXR (0.(F_Real,3,3))
by Lm05
.= M * MXF2MXR (0.(F_Real,3,3)) by Lm06
.= M * 0_Rmatrix(3) by MATRIXR1:def 8;
0.(F_Real,3,3) = 0.(F_Real,3,3) * MXR2MXF M by A1,MATRIX_5:22;
hence 0_Rmatrix(3) = MXF2MXR (0.(F_Real,3,3) * MXR2MXF M)
by MATRIXR1:def 8
.= MXF2MXR (0.(F_Real,3,3)) * MXF2MXR MXR2MXF M
by Lm05
.= MXF2MXR (0.(F_Real,3,3)) * M by Lm06
.= 0_Rmatrix(3) * M by MATRIXR1:def 8;
end;
begin :: Conic in Real Projective Plane
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
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;
end;
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
{P where P is Point of ProjectiveSpace TOP-REAL 3:
for u being Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a,b,c,d,e,f,u) = 0};
coherence
proof
set C = {P where P is Point of ProjectiveSpace TOP-REAL 3:
for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a,b,c,d,e,f,u) = 0};
C c= the carrier of ProjectiveSpace TOP-REAL 3
proof
let x be object;
assume x in C;
then ex P be Point of ProjectiveSpace TOP-REAL 3 st x = P &
for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a,b,c,d,e,f,u) = 0;
hence thesis;
end;
hence thesis;
end;
end;
reserve a,b,c,d,e,f for Real;
reserve u,u1,u2 for non zero Element of TOP-REAL 3;
reserve P for Element of ProjectiveSpace TOP-REAL 3;
theorem Th10:
Dir u1 = Dir u2 & qfconic(a,b,c,d,e,f,u1) = 0 implies
qfconic(a,b,c,d,e,f,u2) = 0
proof
assume that
A1: Dir u1 = Dir u2 and
A2: qfconic(a,b,c,d,e,f,u1) = 0;
are_Prop u1,u2 by A1,ANPROJ_1:22;
then consider r be Real such that
A3: r <> 0 and
A4: u1 = r * u2 by ANPROJ_1:1;
r is non zero by A3; then
A5: r * r <> 0 by ORDINAL1:def 14;
u1.1 = r * u2.1 & u1.2 = r * u2.2 & u1.3 = r * u2.3 by A4,RVSUM_1:44;
then r * r * (a * u2.1 * u2.1 + b * u2.2 * u2.2 + c * u2.3 * u2.3
+ d * u2.1 * u2.2 + e * u2.1 * u2.3 + f * u2.3 * u2.2) = r * r * 0
by A2;
hence thesis by A5,XCMPLX_1:5;
end;
theorem Th11:
P = Dir u & qfconic(a,b,c,d,e,f,u) = 0 implies
P in conic(a,b,c,d,e,f)
proof
assume that
A2: P = Dir u and
A3: qfconic(a,b,c,d,e,f,u) = 0;
for v be Element of TOP-REAL 3 st v is non zero & P = Dir v holds
qfconic(a,b,c,d,e,f,v) = 0 by A2,A3,Th10;
hence thesis;
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
<* <* a, d, e *>,
<* d, b, f *>,
<* e, f, c *> *>;
coherence
proof
reconsider fr1 = a,fr2 = b,fr3 =c, fr4 = d, fr5 = e, fr6 = f as
Element of F_Real by XREAL_0:def 1;
set S = <* <* fr1,fr4,fr5 *>,
<* fr4,fr2,fr6 *>,
<* fr5,fr6,fr3 *> *>;
S is Matrix of 3,F_Real by MATRIXR2:35;
hence thesis;
end;
end;
theorem Th12:
symmetric_3(a,b,c,d,e,f) is symmetric
proof
reconsider a,b,c,d,e,f as Element of F_Real by XREAL_0:def 1;
(symmetric_3(a,b,c,d,e,f))@ = <* <* a, d, e *>,
<* d, b, f *>,
<* e, f, c *> *> by Th05;
hence thesis by MATRIX_6:def 5;
end;
theorem Th13:
for a,b,c,d,e,f being Real, u being Point of TOP-REAL 3,
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
let a,b,c,d,e,f being Real;
let u being Point of TOP-REAL 3;
let M being Matrix of 3,REAL;
assume that
A1: p = u and
A2: M = symmetric_3(a,b,c,d,e,f);
reconsider ru = u as Element of REAL 3 by EUCLID:22;
A3: MXR2MXF ColVec2Mx p = <* ru *>@ by A1,ANPROJ_8:72;
reconsider a,b,c,d,e,f as Element of F_Real by XREAL_0:def 1;
reconsider fu1 = ru.1,fu2 = ru.2,fu3 = ru.3 as Element of F_Real
by XREAL_0:def 1;
A4: <* ru *>@ = <* <* fu1 *>,<* fu2 *>,<* fu3 *> *>
by EUCLID_8:50,ANPROJ_8:77;
A5: len ru = 3 by EUCLID_8:50;
A6: len <*ru*> = 1 by FINSEQ_1:39;
rng <*ru*> = {ru} by FINSEQ_1:39;
then ru in rng <*ru*> by TARSKI:def 1; then
A7: width <*ru*> = 3 by A5,A6,MATRIX_0:def 3; then
A8: width (<*ru*>@) = len <*ru*> by MATRIX_0:29
.= 1 by FINSEQ_1:39;
A9: len (<*ru*>@) = 3 by MATRIX_0:def 6,A7; then
A10: <*ru*>@ is Matrix of 3,1,F_Real by A8,MATRIX_0:20;
reconsider M2 = <*ru*>@ as Matrix of 3,1,F_Real by A9,A8,MATRIX_0:20;
A11: M * ColVec2Mx p = M * (<* ru *>@) by A3,MATRIXR1:def 1
.= MXF2MXR((MXR2MXF M) * (MXR2MXF (<*ru*>@)))
by MATRIXR1:def 6;
A12: MXR2MXF (<*ru*>@) is Matrix of 3,1,F_Real by MATRIXR1:def 1,A10;
A13: MXR2MXF (<*ru*>@) = <* <* fu1 *>,<* fu2 *>,<* fu3 *> *>
by A4,MATRIXR1:def 1;
A14: (MXR2MXF M) * (MXR2MXF (<*ru*>@)) =
<* <* a * fu1 + d * fu2 + e * fu3 *>,
<* d * fu1 + b * fu2 + f * fu3 *>,
<* e * fu1 + f * fu2 + c * fu3 *> *>
by A12,A2,MATRIXR1:def 1,A13,ANPROJ_9:7;
reconsider q = <* a * fu1 + d * fu2 + e * fu3,
d * fu1 + b * fu2 + f * fu3,
e * fu1 + f * fu2 + c * fu3 *> as FinSequence of REAL;
A15: q.1 = a * fu1 + d * fu2 + e * fu3 &
q.2 = d * fu1 + b * fu2 + f * fu3 &
q.3 = e * fu1 + f * fu2 + c * fu3 by FINSEQ_1:45;
A16: |[ a * u.1 + d * u.2 + e * u.3,
d * u.1 + b * u.2 + f * u.3,
e * u.1 + f * u.2 + c * u.3 ]| in TOP-REAL 3;
then reconsider rq = q as Element of REAL 3 by EUCLID:22;
reconsider qf = q as FinSequence of F_Real;
A17: len q = 3 by FINSEQ_1:45;
A18: ColVec2Mx rq = MXR2MXF ColVec2Mx rq by MATRIXR1:def 1
.= <*qf*>@ by ANPROJ_8:72;
then
A19: ColVec2Mx rq = F2M q by A17,ANPROJ_8:88
.= <* <* a * fu1 + d * fu2 + e * fu3 *>,
<* d * fu1 + b * fu2 + f * fu3 *>,
<* e * fu1 + f * fu2 + c * fu3 *> *>
by A15,A17,ANPROJ_8:def 1
.= M * ColVec2Mx p by A14,A11,MATRIXR1:def 2;
A20: M * p = Col(ColVec2Mx rq,1) by A19,MATRIXR1:def 11
.= <* a * fu1 + d * fu2 + e * fu3,
d * fu1 + b * fu2 + f * fu3,
e * fu1 + f * fu2 + c * fu3 *> by A18,ANPROJ_8:93; then
A21: (M * p).1 = a * fu1 + d * fu2 + e * fu3 &
(M * p).2 = d * fu1 + b * fu2 + f * fu3 &
(M * p).3 = e * fu1 + f * fu2 + c * fu3 by FINSEQ_1:45;
A22: len M = 3 & width M = 3 by MATRIX_0:24;
u in TOP-REAL 3;
then u in REAL 3 by EUCLID:22; then
A23: len p = 3 by A1,EUCLID_8:50;
reconsider Mp = M * p as Element of REAL 3 by A16,A20,EUCLID:22;
|(p,M * p)| = ru.1 * Mp.1 + ru.2 * Mp.2 + ru.3 * Mp.3 by A1,EUCLID_8:63
.= qfconic(a,b,c,2 * d,2 * e,2 * f,u) by A21;
hence thesis by A23,A22,MATRPROB:44;
end;
theorem Th14:
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
let N being invertible Matrix of 3,F_Real;
let NR,M1,M2 being Matrix of 3,REAL;
let a,b,c,d,e,f being Real;
assume
A1: NR = MXF2MXR N & M1 = symmetric_3(a,b,c,d/2,f/2,e/2) &
M2 = MXF2MXR((MXR2MXF(NR@))~) * M1 * MXF2MXR((MXR2MXF NR)~);
reconsider M = symmetric_3(a,b,c,d/2,f/2,e/2) as Matrix of 3,REAL;
A2: MXR2MXF M = symmetric_3(a,b,c,d/2,f/2,e/2) by MATRIXR1:def 1;
reconsider Q = (MXR2MXF (NR@))~ as Matrix of 3,F_Real;
reconsider T = MXF2MXR((MXR2MXF(NR@))~) as Matrix of 3,REAL
by MATRIXR1:def 2;
T * M is Matrix of 3,REAL;
then reconsider M3 = MXF2MXR((MXR2MXF(NR@))~) * M,
M4 = MXF2MXR((MXR2MXF NR)~) as Matrix of 3,REAL
by MATRIXR1:def 2;
reconsider M5 = (MXR2MXF(NR@))~ as Matrix of 3,F_Real;
reconsider M6 = MXF2MXR M5 as Matrix of 3,REAL by MATRIXR1:def 2;
NR@ is invertible by A1,Lm12;
then
A3: MXR2MXF(NR@) is invertible by Lm15;
A4: (MXR2MXF(NR@))@ = MXR2MXF NR
proof
reconsider N1 = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
A5: NR@ = N@ by A1,MATRIXR1:def 2;
reconsider N2 = MXR2MXF(NR@) as Matrix of 3,F_Real;
A6: len N = 3 & width N = 3 by MATRIX_0:24;
(MXR2MXF(NR@))@ = (N@)@ by A5,MATRIXR1:def 1
.= N by A6,MATRIX_0:57;
hence thesis by A1,ANPROJ_8:16;
end;
A7: M5@ = (MXR2MXF NR)~ by A3,MATRIX14:31,A4;
MXR2MXF M2 is symmetric
proof
A8: len M5 = 3 & width M5 = 3 by MATRIX_0:24;
MXR2MXF M2 = MXR2MXF M3 * MXR2MXF M4 by A1,Lm07
.= MXR2MXF (M6 * M) * MXR2MXF (MXF2MXR((MXR2MXF NR)~))
.= ((MXR2MXF (MXF2MXR M5)) * (MXR2MXF M)) *
(MXR2MXF (MXF2MXR((MXR2MXF NR)~))) by Lm07
.= (M5 * MXR2MXF M) * (MXR2MXF (MXF2MXR((MXR2MXF NR)~)))
by ANPROJ_8:16
.= (M5 * MXR2MXF M) * ((MXR2MXF NR)~) by ANPROJ_8:16
.= M5@@ * MXR2MXF M * M5@ by A7,A8,MATRIX_0:57;
hence thesis by A2,Th12,Th07;
end;
hence thesis;
end;
theorem Th15:
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
let a1,a2,a3,a4,a5,a6,b1,b2,b3,b4,b5,b6 being Real;
assume
A1: symmetric_3(a1,a2,a3,a4,a5,a6) = symmetric_3(b1,b2,b3,b4,b5,b6);
reconsider fa1 = a1,fa2 = a2, fa3 = a3,
fa4 = a4,fa5 = a5, fa6 = a6,
fb1 = b1,fb2 = b2, fb3 = b3,
fb4 = b4,fb5 = b5, fb6 = b6 as Element of F_Real
by XREAL_0:def 1;
<* <* fa1, fa4, fa5 *>,
<* fa4, fa2, fa6 *>,
<* fa5, fa6, fa3 *> *> =
<* <* fb1, fb4, fb5 *>,
<* fb4, fb2, fb6 *>,
<* fb5, fb6, fb3 *> *> by A1;
hence thesis by Th02;
end;
theorem Th16:
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 & b = 0 & c = 0 & d = 0 & e = 0 & 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 being Matrix of 3,REAL
for 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 & fe = 0 & fi = 0 & fb = 0 & ff = 0 & fc = 0) &
(homography(N)).P in conic(fa,fe,fi,2 * fb,2 * fc,2 * ff))
proof
let a,b,c,d,e,f be Real;
let P being Point of ProjectiveSpace TOP-REAL 3;
let N being invertible Matrix of 3,F_Real;
assume that
A1: not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & f = 0 ) and
A2: P in conic(a,b,c,d,e,f);
consider Q be Point of ProjectiveSpace TOP-REAL 3 such that
A3: P = Q and
A4: for u be Element of TOP-REAL 3 st u is non zero & Q = Dir u holds
qfconic(a,b,c,d,e,f,u) = 0 by A2;
reconsider M = symmetric_3(a,b,c,d/2,e/2,f/2) as Matrix of 3,REAL;
A5: MXR2MXF M = symmetric_3(a,b,c,d/2,e/2,f/2) by MATRIXR1:def 1;
consider uh,vh being Element of TOP-REAL 3,
ufh being FinSequence of F_Real,
ph being FinSequence of (1-tuples_on REAL)
such that
A6: P = Dir uh & uh is not zero & uh = ufh & ph = N * ufh & vh = M2F ph &
vh is not zero & (homography(N)).P = Dir vh by ANPROJ_8:def 4;
reconsider pR = uh as FinSequence of REAL by EUCLID:24;
A7: SumAll QuadraticForm(pR,M,pR) = qfconic(a,b,c,2 * (d/2),
2 * (e/2),2 * (f/2),uh) by Th13
.= 0 by A3,A4,A6;
reconsider x = uh`1, y = uh`2, z = uh`3 as Element of F_Real
by XREAL_0:def 1;
A8: ufh = <* x,y,z *> by A6,EUCLID_5:27;
consider an, bn, cn, dn, en, fn, gn, hn, iN be Element of F_Real such that
A9: N = <* <* an,bn,cn *>,
<* dn,en,fn *>,
<* gn,hn,iN *> *> by Th03;
reconsider uf=ufh as FinSequence of REAL;
reconsider NR = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
reconsider M2 = MXF2MXR((MXR2MXF(NR@))~) * M * MXF2MXR((MXR2MXF NR)~)
as Matrix of 3,REAL by Lm03;
reconsider T = MXF2MXR((MXR2MXF(NR@))~) as Matrix of 3,REAL
by MATRIXR1:def 2;
T * M is Matrix of 3,REAL;
then reconsider M3 = MXF2MXR((MXR2MXF(NR@))~) * M,
M4 = MXF2MXR((MXR2MXF NR)~) as Matrix of 3,REAL
by MATRIXR1:def 2;
reconsider M5 = (MXR2MXF(NR@))~ as Matrix of 3,F_Real;
reconsider M6 = MXF2MXR M5 as Matrix of 3,REAL by MATRIXR1:def 2;
NR@ is invertible by Lm12;
then
A10: MXR2MXF(NR@) is invertible by Lm15;
(MXR2MXF(NR@))@ = MXR2MXF NR
proof
reconsider N1 = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
A11: NR@ = N@ by MATRIXR1:def 2;
reconsider N2 = MXR2MXF(NR@) as Matrix of 3,F_Real;
A12: len N = 3 & width N = 3 by MATRIX_0:24;
(MXR2MXF(NR@))@ = (N@)@ by A11,MATRIXR1:def 1
.= N by A12,MATRIX_0:57;
hence thesis by ANPROJ_8:16;
end;
then
A13: M5@ = (MXR2MXF NR)~ by A10,MATRIX14:31;
A14: MXR2MXF M2 is symmetric
proof
A15: len M5 = 3 & width M5 = 3 by MATRIX_0:24;
MXR2MXF M2 = MXR2MXF M3 * MXR2MXF M4 by Lm07
.= MXR2MXF (M6 * M) * MXR2MXF (MXF2MXR((MXR2MXF NR)~))
.= ((MXR2MXF (MXF2MXR M5)) * (MXR2MXF M)) *
(MXR2MXF (MXF2MXR((MXR2MXF NR)~))) by Lm07
.= (M5 * MXR2MXF M) * (MXR2MXF (MXF2MXR((MXR2MXF NR)~)))
by ANPROJ_8:16
.= (M5 * MXR2MXF M) * ((MXR2MXF NR)~) by ANPROJ_8:16
.= M5@@ * MXR2MXF M * M5@ by A13,A15,MATRIX_0:57;
hence thesis by A5,Th12,Th07;
end;
consider ma,mb,mc,md,me,mf,mg,mh,mi be Element of F_Real such that
A16: M2 = <* <* ma,mb,mc *>,
<* md,me,mf *>,
<* mg,mh,mi *> *> by Th03;
MXR2MXF M2 = <* <* ma,mb,mc *>,
<* md,me,mf *>,
<* mg,mh,mi *> *> by A16,MATRIXR1:def 1;
then
A17: mb = md & mc = mg & mh = mf by A14,Th06;
uh in TOP-REAL 3;
then uh in REAL 3 by EUCLID:22; then
A18: len uf = 3 by A6,EUCLID_8:50;
A19: len (NR@ * M2 * NR) = 3 & width (NR@ * M2 * NR) = 3 by MATRIX_0:24;
A20: |( NR * uf, M2 * (NR * uf) )| = |( uf , (NR@ * M2 * NR) * uf )|
by A18,Lm02
.= SumAll
QuadraticForm(uf,(NR@ * M2 * NR), uf)
by A18,A19,MATRPROB:44
.= 0 by A6,A7,Lm13;
width NR = 3 by MATRIX_0:24;
then len (NR * uf) = len NR by A18,MATRIXR1:61; then
A21: len (NR * uf) = 3 by MATRIX_0:24;
then len (NR * uf) = len M2 & len (NR * uf) = width M2 & len (NR * uf) > 0
by MATRIX_0:24;
then
A22: SumAll QuadraticForm(NR * uf,M2,NR * uf) = 0 by A20,MATRPROB:44;
reconsider u3 = NR * uf as Element of TOP-REAL 3 by A21,EUCLID:76;
u3 is non zero
proof
assume
A23: u3 is zero;
reconsider p = 0.TOP-REAL 3 as FinSequence of REAL by EUCLID:24;
A24: width NR = 3 & width Inv(NR) = 3 & len NR = 3 by MATRIX_0:24;
A25: NR is invertible by Lm14;
Inv(NR) * p = (Inv(NR) * NR) * uf by A23,A24,A18,MATRIXR2:59
.= 1_Rmatrix(3) * uf by A25,MATRIXR2:def 6
.= uf by A18,MATRIXR2:86;
hence contradiction by Lm16,A6;
end;
then reconsider u2 = NR * uf as non zero Element of TOP-REAL 3;
reconsider fa = ma,fb = mb, fc = mc,
fe = me, ff = mf, fi = mi as Real;
M2 = symmetric_3(fa,fe,fi,fb,fc,ff) by A16,A17; then
A26: qfconic(fa,fe,fi,2 * fb,2 * fc,2* ff,u2) = 0 by A22,Th13;
A27: not (fa = 0 & fe = 0 & fi = 0 & 2 * fb = 0 & 2 * ff = 0 & 2 * fc = 0)
proof
assume
A28: fa = 0 & fe = 0 & fi = 0 & 2 * fb = 0 & 2 * ff = 0 & 2 * fc = 0;
A29: (NR@) * 0_Rmatrix(3) * NR = 0_Rmatrix(3) * NR by Lm20
.= 0_Rmatrix(3) by Lm20;
reconsider z1 = 0, z2 = 0, z3 = 0,
z4 = 0, z5 = 0, z6 = 0,
z7 = 0, z8 = 0, z9 = 0,
a1 = a, b1 = b, c1 = c,
d1 = d/2, e1 = f/2, f1 = e/2 as Element of F_Real
by XREAL_0:def 1;
<* <* a1, d1, f1 *>,
<* d1, b1, e1 *>,
<* f1, e1, c1 *> *> =
<* <* z1,z2,z3 *>,
<* z4,z5,z6 *>,
<* z7,z8,z9 *> *> by A29,Lm13,A28,A17,A16,Lm18;
then a1 = z1 & b1 = z5 & c1 = z9 & d1 = z2 & e1 = z5 & f1 = z3 by Th02;
hence contradiction by A1;
end;
A30: u2 = vh
proof
ph = <* <* an * x + bn * y + cn * z *>,
<* dn * x + en * y + fn * z *>,
<* gn * x + hn * y + iN * z *> *> &
vh = <* an * x + bn * y + cn * z ,
dn * x + en * y + fn * z ,
gn * x + hn * y + iN * z *> by A6,A8,A9,Th08;
hence thesis by A8,Th09,A9,MATRIXR1:def 2;
end;
for ufa,ufb,ufc,ufd,ufe,ufi,uff being Real
for UM1,UM2 being Matrix of 3,REAL
for UNR being Matrix of 3,REAL
st UM1 = symmetric_3(a,b,c,d/2,e/2,f/2) &
UNR = MXF2MXR N &
UM2 = MXF2MXR((MXR2MXF(UNR@))~) * UM1 * MXF2MXR((MXR2MXF UNR)~) &
UM2 = symmetric_3(ufa,ufe,ufi,ufb,ufc,uff) holds
not(ufa = 0 & ufe = 0 & ufi = 0 & ufb = 0 & uff = 0 & ufc = 0) &
(homography(N)).P in conic(ufa,ufe,ufi,2 * ufb,2 * ufc,2 * uff)
proof
let ufa,ufb,ufc,ufd,ufe,ufi,uff being Real;
let UM1,UM2 being Matrix of 3,REAL;
let UNR being Matrix of 3,REAL;
assume that
A31: UM1 = symmetric_3(a,b,c,d/2,e/2,f/2) and
A32: UNR = MXF2MXR N and
A33: UM2 = MXF2MXR((MXR2MXF(UNR@))~) * UM1 * MXF2MXR((MXR2MXF UNR)~) and
A34: UM2 = symmetric_3(ufa,ufe,ufi,ufb,ufc,uff);
symmetric_3(ufa,ufe,ufi,ufb,ufc,uff) = symmetric_3(fa,fe,fi,fb,fc,ff)
by A31,A32,A33,A34,A16,A17;
then fa = ufa & fb = ufb & fc = ufc & fe = ufe & ff = uff & fi = ufi
by Th15;
hence
not (ufa = 0 & ufe = 0 & ufi = 0 & ufb = 0 & uff = 0 & ufc = 0) &
(homography(N)).P in conic(ufa,ufe,ufi,2 * ufb,2 * ufc,2 * uff)
by A27,A30,A26,A6,Th11;
end;
hence thesis;
end;
theorem Th17:
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 & b = 0 & c = 0 & d = 0 & e = 0 & 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 be Real st not (a2 = 0 & b2 = 0 & c2 = 0 & d2 = 0 &
e2 = 0 & 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
let a,b,c,d,e,f being Real;
let P1,P2,P3,P4,P5,P6 being Point of ProjectiveSpace TOP-REAL 3;
let N being invertible Matrix of 3,F_Real;
assume that
A1: not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & f = 0 ) and
A2: 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);
reconsider M1 = symmetric_3(a,b,c,d/2,e/2,f/2) as Matrix of 3,REAL;
reconsider NR = MXF2MXR N as Matrix of 3,REAL by MATRIXR1:def 2;
reconsider M2 = MXF2MXR((MXR2MXF(NR@))~) * M1 *
MXF2MXR((MXR2MXF NR)~) as Matrix of 3,REAL by Lm03;
consider ra,rb,rc,rd,re,rf,rg,rh,ri be Element of F_Real such that
A3: MXR2MXF M2 = <* <* ra, rb, rc *> ,
<* rd, re, rf *>,
<* rg, rh, ri *> *> by Th03;
MXR2MXF M2 is symmetric by Th14; then
A4: rb = rd & rc = rg & rf = rh by A3,Th06;
reconsider fa = ra, fe = re,fi = ri,fb = rb,fc = rc,ff = rf as Real;
A5: M2 = symmetric_3(fa,fe,fi,fb,fc,ff) by A3,A4,MATRIXR1:def 1;
now
reconsider a2 = ra,b2 = re,c2 = ri,d2 = 2 * rb,e2 = 2 * rc,
f2 = 2 * rf as Real;
take a2,b2,c2,d2,e2,f2;
thus not(a2 = 0 & b2 = 0 & c2 = 0 & d2 = 0 & e2 = 0 & 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) by A1,A2,A5,Th16;
end;
hence thesis;
end;
reserve a,b,c,d,e,f,g,h,i for Element of F_Real;
theorem Th18:
(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
hereby
assume
A1: qfconic(a,b,c,d,e,f,|[1,0,0]|) = 0;
|[1,0,0]|.1 = |[1,0,0]|`1 &
|[1,0,0]|.2 = |[1,0,0]|`2 &
|[1,0,0]|.3 = |[1,0,0]|`3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
then |[1,0,0]|.1 = 1 & |[1,0,0]|.2 = 0 & |[1,0,0]|.3 = 0 by EUCLID_5:2;
hence a = 0 by A1;
end;
hereby
assume
A2: qfconic(a,b,c,d,e,f,|[0,1,0]|) = 0;
|[0,1,0]|.1 = |[0,1,0]|`1 &
|[0,1,0]|.2 = |[0,1,0]|`2 &
|[0,1,0]|.3 = |[0,1,0]|`3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
then |[0,1,0]|.1 = 0 & |[0,1,0]|.2 = 1 & |[0,1,0]|.3 = 0 by EUCLID_5:2;
hence b = 0 by A2;
end;
hereby
assume
A3: qfconic(a,b,c,d,e,f,|[0,0,1]|) = 0;
|[0,0,1]|.1 = |[0,0,1]|`1 &
|[0,0,1]|.2 = |[0,0,1]|`2 &
|[0,0,1]|.3 = |[0,0,1]|`3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
then |[0,0,1]|.1 = 0 & |[0,0,1]|.2 = 0 & |[0,0,1]|.3 = 1 by EUCLID_5:2;
hence c = 0 by A3;
end;
hereby
assume
A4: qfconic(0,0,0,d,e,f,|[1,1,1]|) = 0;
|[1,1,1]|.1 = |[1,1,1]|`1 &
|[1,1,1]|.2 = |[1,1,1]|`2 &
|[1,1,1]|.3 = |[1,1,1]|`3
by EUCLID_5:def 1,EUCLID_5:def 2,EUCLID_5:def 3;
then |[1,1,1]|.1 = 1 & |[1,1,1]|.2 = 1 & |[1,1,1]|.3 = 1 by EUCLID_5:2;
hence d + e + f = 0 by A4;
end;
end;
begin :: Pascal's theorem
reserve M for Matrix of 3,F_Real;
reserve e1,e2,e3,f1,f2,f3 for Element of F_Real;
reserve MABC,MAEF,MDBF,MDEC,MDEF,MDBC,MAEC,MABF,
MABE,MACF,MBDF,MCDE,MACE,MBDE,MCDF for Matrix of 3,F_Real;
reserve r1,r2 for Real;
Lm21:
a = 1 & b = 0 & c = 0 & d = 0 & e = 1 & f = 0 &
M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = i
proof
assume that
A1: a = 1 & b = 0 & c = 0 & d = 0 & e = 1 & f = 0
and
A2: M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
Det M = a * e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h
by A2,MATRIX_9:46
.= i by A1;
hence thesis;
end;
Lm22:
for 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
let d,e,f,g,h,i be Real;
assume that
A1: (r1 <> 0 or r2 <> 0) and
A2: r1 * d * e + r2 * d * f = (r1 + r2) * e * f and
A3: r1 * g * h + r2 * g * i = (r1 + r2) * h * i;
per cases by A1;
suppose
A4: r1 <> 0;
A5: i * (h - g) * (e * (d - f) * r1 + f * (d - e) * r2) = i * (h - g) * 0
by A2;
f * (e - d) * (h * (g - i) * r1 + i * (g - h) * r2) = f * (e - d) * 0
by A3;
then i * (g - h) * e * (d - f) * r1 = f * (d - e) * h * (g - i) * r1
by A5;
hence thesis by A4,XCMPLX_1:5;
end;
suppose
A6: r2 <> 0;
h * (g - i) * (e * (d - f) * r1 + f * (d - e) * r2) = h * (g - i) * 0
by A2;
then
A7: h * (g - i) * e * (d - f) * r1 = - h * (g - i) * f * (d - e) * r2;
e * (d - f) * (h * (g - i) * r1 + i * (g - h) * r2) = e * (d - f) * 0
by A3;
then e * (d - f) * h * (g - i) * r1 = - e * (d - f) * i * (g - h) * r2;
hence thesis by A7,A6,XCMPLX_1:5;
end;
end;
Lm23:
a = 1 & b = 0 & c = 0 & d = 0 & e = 0 & f = 1 &
M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = - h
proof
assume that
A1: a = 1 & b = 0 & c = 0 & d = 0 & e = 0 & f = 1
and
A2: M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
Det M = a * e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A2,MATRIX_9:46
.= - h by A1;
hence thesis;
end;
Lm24:
a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1 &
M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = g - i
proof
assume that
A1: a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1
and
A2: M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
Det M = a * e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A2,MATRIX_9:46
.= g - i by A1;
hence thesis;
end;
Lm25:
a = 0 & b = 0 & c = 1 & d = 1 & e = 1 & f = 1 &
M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = h - g
proof
assume that
A1: a = 0 & b = 0 & c = 1 & d = 1 & e = 1 & f = 1
and
A2: M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
Det M = a * e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A2,MATRIX_9:46
.= h - g by A1;
hence thesis;
end;
Lm26:
a = 1 & b = 0 & c = 0 & d = 0 & e = 1 & f = 0 &
M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = i
proof
assume that
A1: a = 1 & b = 0 & c = 0 & d = 0 & e = 1 & f = 0
and
A2: M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
Det M = a * e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A2,MATRIX_9:46
.= i by A1;
hence thesis;
end;
Lm27:
a = 1 & b = 0 & c = 0 & d = 0 & e = 0 & f = 1 &
M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = - h
proof
assume that
A1: a = 1 & b = 0 & c = 0 & d = 0 & e = 0 & f = 1
and
A2: M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
Det M = a * e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A2,MATRIX_9:46
.= - h by A1;
hence thesis;
end;
Lm28:
a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1 &
M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = g - i
proof
assume that
A1: a = 0 & b = 1 & c = 0 & d = 1 & e = 1 & f = 1
and
A2: M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
Det M = a * e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A2,MATRIX_9:46
.= g - i by A1;
hence thesis;
end;
Lm29:
a = 0 & b = 0 & c = 1 & d = 1 & e = 1 & f = 1 &
M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*> implies Det M = h - g
proof
assume that
A1: a = 0 & b = 0 & c = 1 & d = 1 & e = 1 & f = 1
and
A2: M = <*<* a,b,c*>,<*d,e,f*>,<*g,h,i*>*>;
Det M = a * e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A2,MATRIX_9:46
.= h - g by A1;
hence thesis;
end;
Lm30:
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 *> *>
implies
Det MABE * Det MACF * Det MBDF * Det MCDE = e3 * f2 * (f1 - f3) * (e1 - e2)
proof
assume that
A1: MABE = <* <* 1,0,0 *>, <* 0,1,0 *>, <* e1,e2,e3 *> *> and
A2: MACF = <* <* 1,0,0 *>, <* 0,0,1 *>, <* f1,f2,f3 *> *> and
A3: MBDF = <* <* 0,1,0 *>, <* 1,1,1 *>, <* f1,f2,f3 *> *> and
A4: MCDE = <* <* 0,0,1 *>, <* 1,1,1 *>, <* e1,e2,e3 *> *> ;
Det MABE = e3 & Det MACF = - f2 &
Det MBDF = f1 - f3 & Det MCDE = e2 - e1
by A1,A2,A3,A4,Lm21,Lm23,Lm24,Lm25;
hence thesis;
end;
Lm31:
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 *> *>
implies
Det MABF * Det MACE * Det MBDE * Det MCDF = f3 * e2 * (e1 - e3) * (f1 - f2)
proof
assume that
A1: MABF = <* <* 1,0,0 *>, <* 0,1,0 *>, <* f1,f2,f3 *> *> and A2:
MACE = <* <* 1,0,0 *>, <* 0,0,1 *>, <* e1,e2,e3 *> *> and A3:
MBDE = <* <* 0,1,0 *>, <* 1,1,1 *>, <* e1,e2,e3 *> *> and A4:
MCDF = <* <* 0,0,1 *>, <* 1,1,1 *>, <* f1,f2,f3 *> *>;
Det MABF = f3 & Det MACE = - e2 &
Det MBDE = e1 - e3 & Det MCDF = f2 - f1
by A1,A2,A3,A4,Lm26,Lm27,Lm28,Lm29;
hence thesis;
end;
theorem Th19:
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)
implies
Det MABE * Det MACF * Det MBDF * Det MCDE
= Det MABF * Det MACE * Det MBDE * Det MCDF
proof
assume that
A1: MABE = <* <* 1,0,0 *>, <* 0,1,0 *>, <* e1,e2,e3 *> *> and
A2: MACF = <* <* 1,0,0 *>, <* 0,0,1 *>, <* f1,f2,f3 *> *> and
A3: MBDF = <* <* 0,1,0 *>, <* 1,1,1 *>, <* f1,f2,f3 *> *> and
A4: MCDE = <* <* 0,0,1 *>, <* 1,1,1 *>, <* e1,e2,e3 *> *> and
A5: MABF = <* <* 1,0,0 *>, <* 0,1,0 *>, <* f1,f2,f3 *> *> and
A6: MACE = <* <* 1,0,0 *>, <* 0,0,1 *>, <* e1,e2,e3 *> *> and
A7: MBDE = <* <* 0,1,0 *>, <* 1,1,1 *>, <* e1,e2,e3 *> *> and
A8: MCDF = <* <* 0,0,1 *>, <* 1,1,1 *>, <* f1,f2,f3 *> *> and
A9: (r1 <> 0 or r2 <> 0) and
A10: r1 * e1 * e2 + r2 * e1 * e3 = (r1 + r2) * e2 * e3 and
A11: r1 * f1 * f2 + r2 * f1 * f3 = (r1 + r2) * f2 * f3;
reconsider d = e1,e = e2, f = e3,g = f1,h = f2,i = f3 as Real;
A12: Det MABE * Det MACF * Det MBDF * Det MCDE
= e3 * f2 * (f1 - f3) * (e1 - e2)
by A1,A2,A3,A4,Lm30;
e3 * f2 * (f1 - f3) * (e1 - e2) = f3 * e2 * (e1 - e3) * (f1 - f2)
by A9,A10,A11,Lm22;
hence thesis by A12,A5,A6,A7,A8,Lm31;
end;
reserve p1,p2,p3,p4,p5,p6 for Point of TOP-REAL 3;
theorem Th20:
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 *> implies
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
assume that
A1: MABE = <* p1, p2, p5 *> and
A2: MACF = <* p1, p3, p6 *> and
A3: MBDF = <* p2, p4, p6 *> and
A4: MCDE = <* p3, p4, p5 *> and
A5: MABF = <* p1, p2, p6 *> and
A6: MACE = <* p1, p3, p5 *> and
A7: MBDE = <* p2, p4, p5 *> and
A8: MCDF = <* p3, p4, p6 *>;
p1 = <* p1`1,p1`2,p1`3 *> & p2 = <* p2`1,p2`2,p2`3 *> &
p3 = <* p3`1,p3`2,p3`3 *> & p4 = <* p4`1,p4`2,p4`3 *> &
p5 = <* p5`1,p5`2,p5`3 *> & p6 = <* p6`1,p6`2,p6`3 *> by EUCLID_5:3;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,ANPROJ_8:35;
end;
reserve p7,p8,p9 for Point of TOP-REAL 3;
theorem Th21:
|{p1,p5,p9}| = 0 implies
|{p1,p5,p7}| * |{p2,p5,p9}| = - |{p1,p2,p5}| * |{p5,p9,p7}|
proof
assume
A1: |{p1,p5,p9}| = 0;
A2: |{p1,p2,p5}| = |{p5,p1,p2}| & |{p1,p5,p9}| = - |{p5,p1,p9}| &
|{p5,p1,p7}| = - |{p1,p5,p7}| & |{p5,p2,p9}| = - |{p2,p5,p9}| &
|{p5,p9,p7}| = - |{p5,p7,p9}| by ANPROJ_8:29,ANPROJ_8:30,Th01; then
A3: |{p5,p1,p9}| = 0 by A1;
|{p5,p1,p7}| * |{p5,p2,p9}| - |{p5,p1,p2}| * |{p5,p7,p9}| +
|{p5,p1,p9}| * |{p5,p7,p2}| = 0 by ANPROJ_8:28;
hence thesis by A2,A3;
end;
theorem Th22:
|{p1,p6,p8}| = 0 implies
|{p1,p2,p6}| * |{p3,p6,p8}| = |{p1,p3,p6}| * |{p2,p6,p8}|
proof
assume
A1: |{p1,p6,p8}| = 0;
A2: |{p1,p6,p8}| = - |{p6,p1,p8}| & |{p6,p8,p3}| = |{p3,p6,p8}| &
|{p6,p1,p3}| = |{p1,p3,p6}| & |{p6,p8,p2}| = |{p2,p6,p8}| &
|{p1,p2,p6}| = |{p6,p1,p2}| by ANPROJ_8:30,Th01; then
A3: |{p6,p1,p8}| = 0 by A1;
|{p6,p1,p8}| * |{p6,p2,p3}| - |{p6,p1,p2}| * |{p6,p8,p3}| +
|{p6,p1,p3}| * |{p6,p8,p2}| = 0 by ANPROJ_8:28;
hence thesis by A2,A3;
end;
theorem Th23:
|{p2,p4,p9}| = 0 implies
|{p2,p4,p5}| * |{p2,p9,p7}| = - |{p2,p4,p7}| * |{p2,p5,p9}|
proof
assume
A1: |{p2,p4,p9}| = 0;
|{p2,p4,p5}| * |{p2,p9,p7}| - |{p2,p4,p9}| * |{p2,p5,p7}| +
|{p2,p4,p7}| * |{p2,p5,p9}| = 0 by ANPROJ_8:28;
hence thesis by A1;
end;
theorem Th24:
|{p2,p6,p7}| = 0 implies
|{p2,p4,p7}| * |{p2,p6,p8}| = - |{p2,p4,p6}| * |{p2,p8,p7}|
proof
assume
A1: |{p2,p6,p7}| = 0;
A2: |{p2,p7,p6}| = - |{p2,p6,p7}| & |{p2,p7,p8}| = - |{p2,p8,p7}|
by ANPROJ_8:29;
|{p2,p4,p7}| * |{p2,p6,p8}| - |{p2,p4,p6}| * |{p2,p7,p8}| + |{p2,p4,p8}|
* |{p2,p7,p6}| = 0 by ANPROJ_8:28;
hence thesis by A1,A2;
end;
theorem Th25:
|{p3,p4,p8}| = 0 implies
|{p3,p4,p6}| * |{p3,p5,p8}| = |{p3,p4,p5}| * |{p3,p6,p8}|
proof
assume
A1: |{p3,p4,p8}| = 0;
|{p3,p4,p6}| * |{p3,p5,p8}| - |{p3,p4,p5}| * |{p3,p6,p8}| +
|{p3,p4,p8}| * |{p3,p6,p5}| = 0 by ANPROJ_8:28;
hence thesis by A1;
end;
theorem Th26:
|{p3,p5,p7}| = 0 implies
|{p1,p3,p5}| * |{p5,p8,p7}| = - |{p1,p5,p7}| * |{p3,p5,p8}|
proof
assume
A1: |{p3,p5,p7}| = 0;
A2: |{p3,p5,p7}| = - |{p5,p3,p7}| & |{p5,p8,p3}| = |{p3,p5,p8}| &
|{p5,p7,p1}| = |{p1,p5,p7}| & |{p1,p3,p5}| = |{p5,p1,p3}|
by ANPROJ_8:30,Th01; then
A3: |{p5,p3,p7}| = 0 & - |{p1,p3,p5}| = |{p5,p3,p1}| by ANPROJ_8:29,A1;
|{p5,p8,p3}| * |{p5,p7,p1}| - |{p5,p8,p7}| * |{p5,p3,p1}| +
|{p5,p8,p1}| * |{p5,p3,p7}| = 0 by ANPROJ_8:28;
then |{p3,p5,p8}| * |{p1,p5,p7}| = |{p5,p8,p7}| * ( - |{p1,p3,p5}|)
by A2,A3;
hence thesis;
end;
theorem Th27:
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
let r125,r136,r246,r345,r126,r135,r245,r346,r157,
r259,r597,r368,r268,r297,r247,r287,r358,r587 being non zero Real;
assume that
A1: r125 * r136 * r246 * r345 = r126 * r135 * r245 * r346 and
A2: r157 * r259 = - r125 * r597 and
A3: r126 * r368 = r136 * r268 and
A4: r245 * r297 = - r247 * r259 and
A5: r247 * r268 = - r246 * r287 and
A6: r346 * r358 = r345 * r368 and
A7: r135 * r587 = - r157 * r358;
reconsider r1 = r246 * r125 * r247 * r259 * r136 * r268 *
r345 * r368 * r157 * r358 * r126 * r135 * r245 * r346,
r2 = r247 * r268 * r157 * r259 * r245 * r126 * r368 * r346 *
r358 * r135 * r125 * r136 * r246 * r345 as non zero Real;
(((((- r287 * r246) * (- r125 * r597)) *
(- r247 * r259) * (r136 * r268)) * (r345 * r368)) *
(-r157 * r358)) * (r126 * r135 * r245 * r346)
= ((((r247 * r268 * (r157 * r259)) * (r245 * r297) * (r126 * r368)) *
(r346 * r358)) * (r135 * r587)) * (r125 * r136 * r246 * r345)
by A1,A2,A3,A4,A5,A6,A7;
then r1 * (r287 * r597) = r2 * (r297 * r587) & r1 <> 0 & r2 <> 0
by ORDINAL1:def 14;
hence thesis by XCMPLX_1:5;
end;
theorem Th28:
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
implies
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
assume that
A1: p1 = <* 1,0,0 *> and
A2: p2 = <* 0,1,0 *> and
A3: p3 = <* 0,0,1 *> and
A4: p4 = <* 1,1,1 *> and
A5: p5 = <* e1,e2,e3 *> and
A6: p6 = <* f1,f2,f3 *> and
A8: qfconic(0,0,0,r1,r2,-(r1+r2),p5) = 0 and
A9: qfconic(0,0,0,r1,r2,-(r1+r2),p6) = 0;
p1.1 = 1 & p1.2 = 0 & p1.3 = 0 by A1,FINSEQ_1:45;
hence qfconic(0,0,0,r1,r2,-(r1+r2),p1) = 0;
p2.1 = 0 & p2.2 = 1 & p2.3 = 0 by A2,FINSEQ_1:45;
hence qfconic(0,0,0,r1,r2,-(r1+r2),p2) = 0;
p3.1 = 0 & p3.2 = 0 & p3.3 = 1 by A3,FINSEQ_1:45;
hence qfconic(0,0,0,r1,r2,-(r1+r2),p3) = 0;
p4.1 = 1 & p4.2 = 1 & p4.3 = 1 by A4,FINSEQ_1:45;
hence qfconic(0,0,0,r1,r2,-(r1+r2),p4) = 0;
p5.1 = e1 & p5.2 = e2 & p5.3 = e3 by A5,FINSEQ_1:45;
hence r1 * e1 * e2 + r2 * e1 * e3 = (r1 + r2) * e2 * e3 by A8;
p6.1 = f1 & p6.2 = f2 & p6.3 = f3 by A6,FINSEQ_1:45;
hence r1 * f1 * f2 + r2 * f1 * f3 = (r1 + r2) * f2 * f3 by A9;
end;
theorem Th29:
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
implies
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
proof
assume that
A1: p1 = <* 1,0,0 *> and
A2: p2 = <* 0,1,0 *> and
A3: p3 = <* 0,0,1 *> and
A4: p4 = <* 1,1,1 *> and
A5: p5 = <* e1,e2,e3 *> and
A6: p6 = <* f1,f2,f3 *> and
A7: |{p1,p2,p5}| <> 0 and
A8: |{p1,p3,p6}| <> 0 and
A9: |{p2,p4,p6}| <> 0 and
A10: |{p3,p4,p5}| <> 0 and
A11: |{p1,p2,p6}| <> 0 and
A12: |{p1,p3,p5}| <> 0 and
A13: |{p2,p4,p5}| <> 0 and
A14: |{p3,p4,p6}| <> 0 and
A15: |{p1,p5,p7}| <> 0 and
A16: |{p2,p5,p9}| <> 0 and
A17: |{p5,p9,p7}| <> 0 and
A18: |{p3,p6,p8}| <> 0 and
A19: |{p2,p6,p8}| <> 0 and
A20: |{p2,p9,p7}| <> 0 and
A21: |{p2,p4,p7}| <> 0 and
A22: |{p2,p8,p7}| <> 0 and
A23: |{p3,p5,p8}| <> 0 and
A24: |{p5,p8,p7}| <> 0 and
A25: (r1 <> 0 or r2 <> 0) and
A26: qfconic(0,0,0,r1,r2,-(r1+r2),p5) = 0 and
A27: qfconic(0,0,0,r1,r2,-(r1+r2),p6) = 0 and
A28: |{p1,p5,p9}| = 0 and
A29: |{p1,p6,p8}| = 0 and
A30: |{p2,p4,p9}| = 0 and
A31: |{p2,p6,p7}| = 0 and
A32: |{p3,p4,p8}| = 0 and
A33: |{p3,p5,p7}| = 0;
reconsider r125 = |{p1,p2,p5}|, r136 = |{p1,p3,p6}|, r246 = |{p2,p4,p6}|,
r345 = |{p3,p4,p5}|, r126 = |{p1,p2,p6}|,r135 = |{p1,p3,p5}|,
r245 = |{p2,p4,p5}|, r346 = |{p3,p4,p6}|,r157 = |{p1,p5,p7}|,
r259 = |{p2,p5,p9}|, r597 = |{p5,p9,p7}|,r368 = |{p3,p6,p8}|,
r268 = |{p2,p6,p8}|, r297 = |{p2,p9,p7}|, r247 = |{p2,p4,p7}|,
r287 = |{p2,p8,p7}|, r358 = |{p3,p5,p8}|, r587 = |{p5,p8,p7}| as
non zero Real by A7,A8,A9,A10,
A11,A12,A13,A14,A15,A16,A17,A18,A19,A20,A21,A22,A23,A24;
p1 = <* p1`1,p1`2,p1`3 *> &
p2 = <* p2`1,p2`2,p2`3 *> &
p3 = <* p3`1,p3`2,p3`3 *> &
p4 = <* p4`1,p4`2,p4`3 *> &
p5 = <* p5`1,p5`2,p5`3 *> &
p6 = <* p6`1,p6`2,p6`3 *> by EUCLID_5:3;
then reconsider 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 *> as Matrix of 3,F_Real by ANPROJ_8:19;
p1 = <* 1,0,0 *> & p2 = <* 0,1,0 *> & p3 = <* 0,0,1 *> &
p4 = <* 1,1,1 *> & p5 = <* e1,e2,e3 *> & p6 = <* f1,f2,f3 *> &
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 *> by A1,A2,A3,A4,A5,A6;
then
A34: 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 }| by Th20;
now
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)
by A1,A2,A3,A4,A5,A6,A25,A26,A27,Th28;
then Det MABE * Det MACF * Det MBDF * Det MCDE
= Det MABF * Det MACE * Det MBDE * Det MCDF by Th19;
hence r125 * r136 * r246 * r345 = r126 * r135 * r245 * r346 by A34;
thus r157 * r259 = - r125 * r597 & r126 * r368 = r136 * r268 &
r245 * r297 = - r247 * r259 & r247 * r268 = - r246 * r287 &
r346 * r358 = r345 * r368 & r135 * r587 = - r157 * r358
by A28,A29,A30,A31,A32,A33,Th21,Th22,Th23,Th24,Th25,Th26;
end;
hence thesis by Th27;
end;
theorem Th30:
|{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}| implies
|{p7,p2,p5}| * |{p7,p8,p9}| = 0
proof
assume
A1: |{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|;
A2: |{p7,p2,p8}| = |{p2,p8,p7}| & |{p7,p5,p9}| = |{p5,p9,p7}| &
|{p7,p2,p9}| = |{p2,p9,p7}| & |{p7,p5,p8}| = |{p5,p8,p7}| by Th01;
|{p7,p5,p8}| = |{p5,p8,p7}| by Th01
.= - |{p8,p5,p7}| by ANPROJ_8:30;
then
A3: |{p7,p5,p8}| = - |{p7,p8,p5}| by Th01;
|{p7,p2,p8}| * |{p7,p5,p9}| - |{p7,p2,p5}| * |{p7,p8,p9}| +
|{p7,p2,p9}| * |{p7,p8,p5}| = 0 by ANPROJ_8:28;
then |{p7,p2,p8}| * |{p7,p5,p9}| - |{p7,p2,p5}| * |{p7,p8,p9}| -
|{p7,p2,p9}| * |{p7,p5,p8}| = 0 by A3;
hence thesis by A2,A1;
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:
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
let PCPP be CollProjectiveSpace;
let c1,c2,c3,c4,c5,c6,c7,c8,c9 being Element of PCPP;
assume that
A11: not c1,c2,c4 are_collinear and
A12: not c1,c2,c5 are_collinear and
A13: not c1,c6,c4 are_collinear and
A14: not c1,c6,c5 are_collinear and
A15: not c2,c6,c4 are_collinear and
A16: not c3,c4,c2 are_collinear and
A17: not c3,c4,c6 are_collinear and
A18: not c3,c5,c2 are_collinear and
A19: not c3,c5,c6 are_collinear and
A20: not c4,c5,c2 are_collinear and
A21: c1,c4,c7 are_collinear and
A22: c1,c5,c8 are_collinear and
A23: c2,c3,c7 are_collinear and
A24: c2,c5,c9 are_collinear and
A25: c6,c3,c8 are_collinear and
A26: c6,c4,c9 are_collinear and
A27: c9,c2,c4 are_collinear or c1,c4,c9 are_collinear or
c2,c3,c9 are_collinear or c2,c4,c7 are_collinear or c2,c5,c8
are_collinear or c2,c9,c8 are_collinear or c2,c9,c7 are_collinear or
c6,c4,c8 are_collinear or c6,c5,c8 are_collinear or c4,c9,c8
are_collinear or c4,c9,c7 are_collinear;
A34: for v102,v103,v100,v104 being Element of PCPP holds v100=v104
or not v104,v100,v102
are_collinear or not v104,v100,v103 are_collinear or v102,v103,v104
are_collinear
proof let v102,v103,v100,v104 being Element of PCPP;
v104,v100,v104 are_collinear by COLLSP:5;
hence thesis by COLLSP:3;
end;
A38: for v102,v104,v100,v103 being Element of PCPP holds v100=v103 or
not v103,v100,v102
are_collinear or not v103,v100,v104 are_collinear or v102,v103,v104
are_collinear
proof let v102,v104,v100,v103 being Element of PCPP;
v103,v100,v103 are_collinear by COLLSP:5;
hence thesis by COLLSP:3;
end;
A47: not c5=c2 by COLLSP:2,A12;
A49: not c6,c4,c1 are_collinear by HESSENBE:1,A13;
A51: not c4,c1,c6 are_collinear by HESSENBE:1,A13;
A54: not c6=c4 by A13,COLLSP:2;
A61: not c6,c4,c2 are_collinear by HESSENBE:1,A15;
A67: not c6,c3,c4 are_collinear by HESSENBE:1,A17;
A69: not c2,c3,c5 are_collinear by HESSENBE:1,A18;
A75: c4,c7,c1 are_collinear by A21,HESSENBE:1;
A79: c2,c7,c3 are_collinear by A23,COLLSP:4;
A81: c9,c2,c5 are_collinear by A24,HESSENBE:1;
A83: c2,c9,c5 are_collinear by A24,COLLSP:4;
A85: c6,c8,c3 are_collinear by A25,COLLSP:4;
A89: c4,c9,c6 are_collinear by A26,HESSENBE:1;
A98: c1,c4,c9 are_collinear or c2,c3,c9 are_collinear or
c2,c4,c7 are_collinear or c2,c5,c8 are_collinear or
c2,c9,c8 are_collinear or c2,c9,c7 are_collinear or
c6,c4,c8 are_collinear or c6,c5,c8 are_collinear or
c4,c9,c8 are_collinear or c4,c9,c7 are_collinear or
c9,c4,c2 are_collinear by A27,COLLSP:4;
A101: for v102,v103,v104,v101 being Element of PCPP holds v104=v101 or
not v101,v104,v102 are_collinear or
not v101,v104,v103 are_collinear or v102,v103,v104 are_collinear
proof
let v102,v103,v104,v101 being Element of PCPP;
v101,v104,v104 are_collinear by COLLSP:2;
hence thesis by COLLSP:3;
end;
A105: for v103,v104,v102,v101 being Element of PCPP holds v102=v101 or
not v101,v102,v103 are_collinear or not v101,v102,v104 are_collinear
or v102,v103,v104 are_collinear
proof
let v103,v104,v102,v101 being Element of PCPP;
v101,v102,v102 are_collinear by COLLSP:2;
hence thesis by COLLSP:3;
end;
A121: c7,c4,c1 are_collinear by A21,HESSENBE:1;
A124: for v2,v101,v100 being Element of PCPP holds v101=v100 or
not v100,v101,v2 are_collinear or v2,v101,v100 are_collinear
proof
let v2,v101,v100 being Element of PCPP;
v101=v100 or not v100,v101,v2 are_collinear or
not v100,v101,v101 are_collinear or v2,v101,v100 are_collinear
by A34;
hence thesis by COLLSP:2;
end;
A130: c2,c5,c5 are_collinear by COLLSP:2;
A133: not c2,c5,c4 are_collinear by A130,A47,A34,A20;
A144: c8,c5,c1 are_collinear by A22,HESSENBE:1;
A147: for v0 being Element of PCPP holds c7=c4 or
not c4,c7,v0 are_collinear or v0,c4,c1 are_collinear by A75,A38;
A158: for v0 being Element of PCPP holds c7=c2 or
not c2,c7,v0 are_collinear or c2,c3,v0 are_collinear by A79,HESSENBE:2;
A161: for v0 being Element of PCPP holds c9=c2 or
not c2,c9,v0 are_collinear or c2,v0,c5 are_collinear by A83,HESSENBE:2;
A169: c9,c4,c6 are_collinear by A26,HESSENBE:1;
A175: for v0 being Element of PCPP holds c9=c4 or
not c4,c9,v0 are_collinear or c4,v0,c6 are_collinear by A89,HESSENBE:2;
A203: c5=c6 or not c6,c5,c8 are_collinear or c8,c5,c6 are_collinear by A124;
A213: c9=c4 or not c4,c9,c8 are_collinear or c6,c8,c4 are_collinear
by A89,A34;
A234: c5=c2 or not c2,c5,c8 are_collinear or c8,c5,c2 are_collinear by A124;
A241: c4=c2 or not c2,c4,c7 are_collinear or c7,c4,c2 are_collinear by A124;
A247: c9=c4 or c1,c4,c9 are_collinear or c2,c3,c9 are_collinear or
c8=c5 or c8=c6 or c7=c4 or c9=c2 or c7=c2
by A11,A121,A105,COLLSP:2,A12,A69,A158,A49,A175,A67,
A54,A26,A14,A144,A15,A98,A169,A101,A203,A213,A85,
A147,A83,HESSENBE:2,A161,A241,A234;
A248: not c2,c3,c9 are_collinear or c9,c2,c3 are_collinear by HESSENBE:1;
c4=c1 or not c1,c4,c9 are_collinear or c9,c4,c1 are_collinear by A124;
hence contradiction
by A11,A21,A16,HESSENBE:1,A23,A19,A25,A14,A22,A61,A26,
A133,A24,A51,A169,COLLSP:2,A69,A247,A248,A81,A105;
end;
reserve P1,P2,P3,P4,P5,P6,P7,P8,P9 for Point of ProjectiveSpace TOP-REAL 3,
a,b,c,d,e,f for Real;
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
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;
theorem Th32:
P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration
implies
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
assume
A1: P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration;
assume
A2: not(
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);
not P1,P2,P4 are_collinear & not P1,P2,P5 are_collinear &
not P1,P2,P6 are_collinear & not P1,P3,P4 are_collinear &
not P1,P3,P5 are_collinear & not P1,P3,P6 are_collinear &
not P2,P3,P4 are_collinear & not P2,P3,P5 are_collinear &
not P4,P5,P1 are_collinear & not P4,P5,P2 are_collinear &
not P4,P5,P3 are_collinear & not P4,P6,P2 are_collinear &
not P4,P6,P3 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
by A1,ANPROJ_8:57,HESSENBE:1;
hence contradiction by A2,ANPROJ_8:57,Th31;
end;
theorem Th33:
not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & 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
implies P7,P8,P9 are_collinear
proof
assume that
A1: not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & f = 0) and
A2: {P1,P2,P3,P4,P5,P6} c= conic(a,b,c,d,e,f) and
A3: not (P1,P2,P3 are_collinear) and
A4: not (P1,P2,P4 are_collinear) and
A5: not (P1,P3,P4 are_collinear) and
A6: not (P2,P3,P4 are_collinear) and
A7: not P7,P2,P5 are_collinear and
A8: not P1,P2,P5 are_collinear and
A9: not P1,P2,P6 are_collinear and
A10: not P1,P3,P5 are_collinear and
A11: not P1,P3,P6 are_collinear and
A12: not P1,P5,P7 are_collinear and
A13: not P2,P4,P5 are_collinear and
A14: not P2,P4,P6 are_collinear and
A15: not P2,P4,P7 are_collinear and
A16: not P2,P5,P9 are_collinear and
A17: not P2,P6,P8 are_collinear and
A18: not P2,P7,P8 are_collinear and
A19: not P2,P7,P9 are_collinear and
A20: not P3,P4,P5 are_collinear and
A21: not P3,P4,P6 are_collinear and
A22: not P3,P5,P8 are_collinear and
A23: not P3,P6,P8 are_collinear and
A24: not P5,P7,P8 are_collinear and
A25: not P5,P7,P9 are_collinear and
A26: P1,P5,P9 are_collinear and
A27: P1,P6,P8 are_collinear and
A28: P2,P4,P9 are_collinear and
A29: P2,P6,P7 are_collinear and
A30: P3,P4,P8 are_collinear and
A31: P3,P5,P7 are_collinear;
consider N being invertible Matrix of 3,F_Real such that
A32: (homography(N)).P1 = Dir100 and
A33: (homography(N)).P2 = Dir010 and
A34: (homography(N)).P3 = Dir001 and
A35: (homography(N)).P4 = Dir111 by A3,A4,A5,A6,ANPROJ_9:30;
consider u5 being Point of TOP-REAL 3 such that
A36: u5 is non zero and
A37: (homography(N)).P5 = Dir u5 by ANPROJ_1:26;
reconsider p51 = u5.1,p52 = u5.2, p53 = u5.3 as Real;
A38: u5`1 = u5.1 & u5`2 = u5.2 & u5`3 = u5.3 by EUCLID_5:def 1,def 2,def 3;
then
A39: (homography(N)).P5 = Dir |[ p51,p52,p53 ]| by A37,EUCLID_5:3;
consider u6 being Point of TOP-REAL 3 such that
A40: u6 is non zero and
A41: (homography(N)).P6 = Dir u6 by ANPROJ_1:26;
reconsider p61 = u6.1,p62 = u6.2, p63 = u6.3 as Real;
A42: u6`1 = u6.1 & u6`2 = u6.2 & u6`3 = u6.3 by EUCLID_5:def 1,def 2,def 3;
then
A43: (homography(N)).P6 = Dir |[ p61,p62,p63 ]| by A41,EUCLID_5:3;
consider u7 being Point of TOP-REAL 3 such that
A44: u7 is non zero and
A45: (homography(N)).P7 = Dir u7 by ANPROJ_1:26;
reconsider p71 = u7.1,p72 = u7.2, p73 = u7.3 as Real;
A46: u7`1 = u7.1 & u7`2 = u7.2 & u7`3 = u7.3 by EUCLID_5:def 1,def 2,def 3;
then
A47: (homography(N)).P7 = Dir |[ p71,p72,p73 ]| by A45,EUCLID_5:3;
consider u8 being Point of TOP-REAL 3 such that
A48: u8 is non zero and
A49: (homography(N)).P8 = Dir u8 by ANPROJ_1:26;
reconsider p81 = u8.1,p82 = u8.2, p83 = u8.3 as Real;
A50: u8`1 = u8.1 & u8`2 = u8.2 & u8`3 = u8.3 by EUCLID_5:def 1,def 2,def 3;
then
A51: (homography(N)).P8 = Dir |[ p81,p82,p83 ]| by A49,EUCLID_5:3;
consider u9 being Point of TOP-REAL 3 such that
A52: u9 is non zero and
A53: (homography(N)).P9 = Dir u9 by ANPROJ_1:26;
reconsider p91 = u9.1,p92 = u9.2, p93 = u9.3 as Real;
A54: u9`1 = u9.1 & u9`2 = u9.2 & u9`3 = u9.3 by EUCLID_5:def 1,def 2,def 3;
then
A55: (homography(N)).P9 = Dir |[ p91,p92,p93 ]| by A53,EUCLID_5:3;
A56: P1 in {P1,P2,P3,P4,P5,P6} & P2 in {P1,P2,P3,P4,P5,P6} &
P3 in {P1,P2,P3,P4,P5,P6} & P4 in {P1,P2,P3,P4,P5,P6} &
P5 in {P1,P2,P3,P4,P5,P6} & P6 in {P1,P2,P3,P4,P5,P6} by ENUMSET1:def 4;
consider a2,b2,c2,d2,e2,f2 be Real such that
A57: not (a2 = 0 & b2 = 0 & c2 = 0 & d2 = 0 & e2 = 0 & f2 = 0 ) and
A58: (homography(N)).P1 in conic(a2,b2,c2,d2,e2,f2) and
A59: (homography(N)).P2 in conic(a2,b2,c2,d2,e2,f2) and
A60: (homography(N)).P3 in conic(a2,b2,c2,d2,e2,f2) and
A61: (homography(N)).P4 in conic(a2,b2,c2,d2,e2,f2) and
A62: (homography(N)).P5 in conic(a2,b2,c2,d2,e2,f2) and
A63: (homography(N)).P6 in conic(a2,b2,c2,d2,e2,f2) by A56,A2,A1,Th17;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A64: Dir |[1,0,0]| = P and
A65: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A32,A58;
A66: qfconic(a2,b2,c2,d2,e2,f2,|[1,0,0]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[0,1,0]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[p51,p52,p53]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0
proof
thus qfconic(a2,b2,c2,d2,e2,f2,|[1,0,0]|) = 0 by A64,A65,ANPROJ_9:10;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A67: Dir |[0,1,0]| = P and
A68: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A33,A59;
thus qfconic(a2,b2,c2,d2,e2,f2,|[0,1,0]|) = 0 by A67,A68,ANPROJ_9:10;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A69: Dir |[0,0,1]| = P and
A70: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A34,A60;
thus qfconic(a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 by A69,A70,ANPROJ_9:10;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A71: Dir |[1,1,1]| = P and
A72: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A35,A61;
thus qfconic(a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 by A71,A72,ANPROJ_9:10;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A73: Dir |[p51,p52,p53]| = P and
A74: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A39,A62;
|[p51,p52,p53]| is non zero & Dir |[p51,p52,p53]| = P
by A73,A36,A38,EUCLID_5:3;
hence qfconic(a2,b2,c2,d2,e2,f2,|[p51,p52,p53]|) = 0 by A74;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A75: Dir |[p61,p62,p63]| = P and
A76: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A43,A63;
|[p61,p62,p63]| is non zero & Dir |[p61,p62,p63]| = P
by A75,A42,EUCLID_5:3,A40;
hence qfconic(a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 by A76;
end;
reconsider a2f = a2,b2f = b2,c2f = c2,d2f = d2,e2f = e2,f2f = f2 as
Element of F_Real by XREAL_0:def 1;
qfconic(a2f,b2f,c2f,d2f,e2,f2f,|[1,0,0]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[0,1,0]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[0,0,1]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[1,1,1]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[p51,p52,p53]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[p61,p62,p63]|) = 0 by A66;
then a2f = 0 & b2f = 0 & c2f = 0 by Th18;
then
A77: a2f = 0 & b2f = 0 & c2f = 0 & d2f + e2f + f2f = 0 by A66,Th18;
reconsider r1 = d2, r2 = e2 as Real;
reconsider p71,p72,p73,p81,p82,p83,p91,p92,p93 as Element of F_Real
by XREAL_0:def 1;
|[1,0,0]| = <* 1,0,0 *> & <* 0,1,0 *> = |[0,1,0]| &
<* 0,0,1 *> = |[0,0,1]| & <* 1,1,1 *> = |[1,1,1]| &
<* p51,p52,p53 *> = |[p51,p52,p53]| &
<* p61,p62,p63 *> = |[p61,p62,p63]| &
<* p71,p72,p73 *> = |[p71,p72,p73]| &
<* p81,p82,p83 *> = |[p81,p82,p83]| &
<* p91,p92,p93 *> = |[p91,p92,p93]|;
then reconsider p1 = <* 1,0,0 *>, p2 = <* 0,1,0 *>, p3 = <* 0,0,1 *>,
p4 = <* 1,1,1 *>, p5 = <* p51,p52,p53 *>, p6 = <* p61,p62,p63 *>,
p7 = <* p71,p72,p73 *>, p8 = <* p81,p82,p83 *>, p9 = <* p91,p92,p93 *> as
Point of TOP-REAL 3;
A82: u5 = |[p51,p52,p53]| by EUCLID_5:3,A38;
A83: u6 = |[p61,p62,p63]| by A42,EUCLID_5:3;
A84: p7 is non zero by A44,A46,EUCLID_5:3;
A85: p8 is non zero by A48,A50,EUCLID_5:3;
A86: p9 is non zero by A52,A54,EUCLID_5:3;
A87: (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 by A77,A66,A57;
A88: |{p7,p2,p5}| <> 0
proof
A89: not (homography(N)).P7,(homography(N)).P2,
(homography(N)).P5 are_collinear by A7,ANPROJ_8:102;
(homography(N)).P7 = Dir p7 & (homography(N)).P2 = Dir p2 &
(homography(N)).P5 = Dir p5 by A33,A38,A37,EUCLID_5:3,A45,A46;
hence thesis by ANPROJ_8:43,A89,A84,ANPROJ_9:10,A82,A36,ANPROJ_2:23;
end;
A90: p51 is Element of F_Real & p52 is Element of F_Real &
p53 is Element of F_Real & p61 is Element of F_Real &
p62 is Element of F_Real & p63 is Element of F_Real by XREAL_0:def 1;
now
thus |{p1,p2,p5}| <> 0
proof
not (homography(N)).P1,(homography(N)).P2,
(homography(N)).P5 are_collinear by A8,ANPROJ_8:102;
hence thesis
by A32,A33,A37,ANPROJ_8:43,ANPROJ_9:10,A82,A36,ANPROJ_2:23;
end;
thus |{p1,p2,p6}| <> 0
proof
not (homography(N)).P1,(homography(N)).P2,
(homography(N)).P6 are_collinear by A9,ANPROJ_8:102;
hence thesis
by A32,A33,A41,ANPROJ_8:43,A83,A40,ANPROJ_9:10,ANPROJ_2:23;
end;
thus |{p1,p3,p5}| <> 0
proof
not (homography(N)).P1,(homography(N)).P3,
(homography(N)).P5 are_collinear by A10,ANPROJ_8:102;
hence thesis
by A34,A32,A37,ANPROJ_8:43,ANPROJ_9:10,A82,A36,ANPROJ_2:23;
end;
thus |{p1,p3,p6}| <> 0
proof
not (homography(N)).P1,(homography(N)).P3,
(homography(N)).P6 are_collinear by A11,ANPROJ_8:102;
hence thesis
by A32,A41,A34,ANPROJ_8:43,A83,A40,ANPROJ_9:10,ANPROJ_2:23;
end;
thus |{p1,p5,p7}| <> 0
proof
not (homography(N)).P1,(homography(N)).P5,
(homography(N)).P7 are_collinear by A12,ANPROJ_8:102;
hence thesis
by A32,A37,A47,ANPROJ_8:43,ANPROJ_9:10,A82,A36,A84,ANPROJ_2:23;
end;
thus |{p2,p4,p5}| <> 0
proof
not (homography(N)).P2,(homography(N)).P4,
(homography(N)).P5 are_collinear by A13,ANPROJ_8:102;
hence thesis
by A33,A37,A35,ANPROJ_8:43,ANPROJ_9:10,A82,A36,ANPROJ_2:23;
end;
thus |{p2,p4,p6}| <> 0
proof
not (homography(N)).P2,(homography(N)).P4,
(homography(N)).P6 are_collinear by A14,ANPROJ_8:102;
hence thesis
by A33,A41,A35,ANPROJ_8:43,ANPROJ_9:10,A83,A40,ANPROJ_2:23;
end;
thus |{p2,p4,p7}| <> 0
proof
not (homography(N)).P2,(homography(N)).P4,
(homography(N)).P7 are_collinear by A15,ANPROJ_8:102;
hence thesis
by A33,A47,A35,ANPROJ_8:43,ANPROJ_9:10,A84,ANPROJ_2:23;
end;
thus |{p2,p5,p9}| <> 0
proof
not (homography(N)).P2,(homography(N)).P5,
(homography(N)).P9 are_collinear by A16,ANPROJ_8:102;
hence thesis
by A33,A37,A55,ANPROJ_8:43,ANPROJ_9:10,A82,A36,A86,ANPROJ_2:23;
end;
thus |{p2,p6,p8}| <> 0
proof
not (homography(N)).P2,(homography(N)).P6,
(homography(N)).P8 are_collinear by A17,ANPROJ_8:102;
hence thesis
by A33,A41,A51,ANPROJ_8:43,ANPROJ_9:10,A83,A40,A85,ANPROJ_2:23;
end;
thus |{p2,p8,p7}| <> 0
proof
A91: |{p2,p8,p7}| = - |{p2,p7,p8}| by ANPROJ_8:29;
not (homography(N)).P2,(homography(N)).P7,
(homography(N)).P8 are_collinear by A18,ANPROJ_8:102;
hence thesis
by A33,A47,A51,A91,ANPROJ_8:43,ANPROJ_9:10,A84,A85,ANPROJ_2:23;
end;
thus |{p2,p9,p7}| <> 0
proof
A92: |{p2,p9,p7}| = - |{p2,p7,p9}| by ANPROJ_8:29;
not (homography(N)).P2,(homography(N)).P7,
(homography(N)).P9 are_collinear by A19,ANPROJ_8:102;
hence thesis
by A92,ANPROJ_8:43,A33,A47,A55,ANPROJ_9:10,A84,A86,ANPROJ_2:23;
end;
thus |{p3,p4,p5}| <> 0
proof
not (homography(N)).P3,(homography(N)).P4,
(homography(N)).P5 are_collinear by A20,ANPROJ_8:102;
hence thesis
by A34,A35,A37,ANPROJ_8:43,ANPROJ_9:10,A82,A36,ANPROJ_2:23;
end;
thus |{p3,p4,p6}| <> 0
proof
not (homography(N)).P3,(homography(N)).P4,
(homography(N)).P6 are_collinear by A21,ANPROJ_8:102;
hence thesis
by A34,A35,A41,ANPROJ_8:43,ANPROJ_9:10,A83,A40,ANPROJ_2:23;
end;
thus |{p3,p5,p8}| <> 0
proof
not (homography(N)).P3,(homography(N)).P5,
(homography(N)).P8 are_collinear by A22,ANPROJ_8:102;
hence thesis
by A34,A37,A51,ANPROJ_8:43,ANPROJ_9:10,A82,A36,A85,ANPROJ_2:23;
end;
thus |{p3,p6,p8}| <> 0
proof
not (homography(N)).P3,(homography(N)).P6,
(homography(N)).P8 are_collinear by A23,ANPROJ_8:102;
hence thesis
by ANPROJ_8:43,A34,A41,A51,ANPROJ_9:10,A83,A40,A85,ANPROJ_2:23;
end;
A93: |{p5,p8,p7}| = - |{p5,p7,p8}| by ANPROJ_8:29;
thus |{p5,p7,p8}| <> 0
proof
not (homography(N)).P5,(homography(N)).P7,
(homography(N)).P8 are_collinear by A24,ANPROJ_8:102;
hence thesis
by ANPROJ_8:43,A37,A47,A51,A82,A36,A84,A85,ANPROJ_2:23;
end;
hence |{p5,p8,p7}| <> 0 by A93;
A94: |{p5,p9,p7}| = - |{p5,p7,p9}| by ANPROJ_8:29;
|{p5,p7,p9}| <> 0
proof
not (homography(N)).P5,(homography(N)).P7,
(homography(N)).P9 are_collinear by A25,ANPROJ_8:102;
hence thesis
by A37,A47,A55,ANPROJ_8:43,A82,A36,A84,A86,ANPROJ_2:23;
end;
hence |{p5,p9,p7}| <> 0 by A94;
thus |{p1,p5,p9}| = 0 & |{p1,p6,p8}| = 0 &
|{p2,p4,p9}| = 0 & |{p2,p6,p7}| = 0 &
|{p3,p4,p8}| = 0 & |{p3,p5,p7}| = 0
proof
thus |{p1,p5,p9}| = 0
proof
consider u,v,w be Element of TOP-REAL 3 such that
A95: (homography(N)).P1 = Dir u and
A96: (homography(N)).P5 = Dir v and
A97: (homography(N)).P9 = Dir w and
A98: u is non zero and
A99: v is non zero and
A100: w is non zero and
A101: u,v,w are_LinDep by A26,ANPROJ_8:102,ANPROJ_2:23;
[Dir u,Dir v,Dir w] in
the Collinearity of ProjectiveSpace(TOP-REAL 3)
by A98,A99,A100,A101,ANPROJ_1:25;
then p1,p5,p9 are_LinDep
by A32,A37,A55,A95,A96,A97,ANPROJ_9:10,A82,A36,A86,ANPROJ_1:25;
hence thesis by ANPROJ_8:43;
end;
thus |{p1,p6,p8}| = 0
proof
consider u,v,w be Element of TOP-REAL 3 such that
A102: (homography(N)).P1 = Dir u and
A103: (homography(N)).P6 = Dir v and
A104: (homography(N)).P8 = Dir w and
A105: u is non zero and
A106: v is non zero and
A107: w is non zero and
A108: u,v,w are_LinDep by A27,ANPROJ_8:102,ANPROJ_2:23;
A109: [Dir u,Dir v,Dir w] in
the Collinearity of ProjectiveSpace(TOP-REAL 3)
by A105,A106,A107,A108,ANPROJ_1:25;
p1,p6,p8 are_LinDep
by A32,A41,A51,A102,A103,A104,A109,
ANPROJ_9:10,A83,A40,A85,ANPROJ_1:25;
hence thesis by ANPROJ_8:43;
end;
thus |{p2,p4,p9}| = 0
proof
consider u,v,w be Element of TOP-REAL 3 such that
A110: (homography(N)).P2 = Dir u and
A111: (homography(N)).P4 = Dir v and
A112: (homography(N)).P9 = Dir w and
A113: u is non zero and
A114: v is non zero and
A115: w is non zero and
A116: u,v,w are_LinDep by A28,ANPROJ_8:102,ANPROJ_2:23;
[Dir u,Dir v,Dir w] in
the Collinearity of ProjectiveSpace(TOP-REAL 3)
by A113,A114,A115,A116,ANPROJ_1:25;
then p2,p4,p9 are_LinDep
by A33,A35,A55,A110,A111,A112,ANPROJ_9:10,A86,ANPROJ_1:25;
hence thesis by ANPROJ_8:43;
end;
thus |{p2,p6,p7}| = 0
proof
consider u,v,w be Element of TOP-REAL 3 such that
A117: (homography(N)).P2 = Dir u and
A118: (homography(N)).P6 = Dir v and
A119: (homography(N)).P7 = Dir w and
A120: u is non zero and
A121: v is non zero and
A122: w is non zero and
A123: u,v,w are_LinDep by A29,ANPROJ_8:102,ANPROJ_2:23;
A124: [Dir u,Dir v,Dir w] in
the Collinearity of ProjectiveSpace(TOP-REAL 3)
by A120,A121,A122,A123,ANPROJ_1:25;
p2,p6,p7 are_LinDep
by A33,A41,A47,A117,A118,A119,A124,ANPROJ_9:10,
A83,A40,A84,ANPROJ_1:25;
hence thesis by ANPROJ_8:43;
end;
thus |{p3,p4,p8}| = 0
proof
consider u,v,w be Element of TOP-REAL 3 such that
A125: (homography(N)).P3 = Dir u and
A126: (homography(N)).P4 = Dir v and
A127: (homography(N)).P8 = Dir w and
A128: u is non zero and
A129: v is non zero and
A130: w is non zero and
A131: u,v,w are_LinDep by A30,ANPROJ_8:102,ANPROJ_2:23;
[Dir u,Dir v,Dir w] in
the Collinearity of ProjectiveSpace(TOP-REAL 3)
by A128,A129,A130,A131,ANPROJ_1:25;
then p3,p4,p8 are_LinDep
by A34,A35,A51,A125,A126,A127,ANPROJ_9:10,A85,ANPROJ_1:25;
hence thesis by ANPROJ_8:43;
end;
thus |{p3,p5,p7}| = 0
proof
consider u,v,w be Element of TOP-REAL 3 such that
A132: (homography(N)).P3 = Dir u and
A133: (homography(N)).P5 = Dir v and
A134: (homography(N)).P7 = Dir w and
A135: u is non zero and
A136: v is non zero and
A137: w is non zero and
A138: u,v,w are_LinDep by A31,ANPROJ_8:102,ANPROJ_2:23;
[Dir u,Dir v,Dir w] in
the Collinearity of ProjectiveSpace(TOP-REAL 3)
by A135,A136,A137,A138,ANPROJ_1:25;
then p3,p5,p7 are_LinDep
by A34,A37,A47,A132,A133,A134,ANPROJ_9:10,A82,A36,A84,ANPROJ_1:25;
hence thesis by ANPROJ_8:43;
end;
end;
end;
then |{p2,p8,p7}| * |{p5,p9,p7}| = |{p2,p9,p7}| * |{p5,p8,p7}|
by A90,A87,Th29;
then |{p7,p2,p5}| * |{p7,p8,p9}| = 0 by Th30;
then |{p7,p8,p9}| = 0 by A88,XCMPLX_1:6; then
A139: p7,p8,p9 are_LinDep by ANPROJ_8:43;
(homography(N)).P7 = Dir p7 & (homography(N)).P8 = Dir p8 &
(homography(N)).P9 = Dir p9 &
p7 is non zero & p8 is non zero & p9 is non zero
by A52,A54,EUCLID_5:3,A44,A46,A50,A48,A45,A49,A53;
hence thesis by A139,ANPROJ_2:23,ANPROJ_8:102;
end;
theorem Th34:
not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & 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
implies
P7,P8,P9 are_collinear
proof
assume that
A1: not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & f = 0) and
A2: {P1,P2,P3,P4,P5,P6} c= conic(a,b,c,d,e,f) and
A3: not P1,P2,P3 are_collinear &
P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration;
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
by A3,Th32;
hence thesis by A1,A2,Th33;
end;
registration
cluster TOP-REAL 3 -> up-3-dimensional;
coherence
proof
take u = |[1,0,0]|, v = |[0,1,0]|, w = |[0,0,1]|;
let a,b,c be Real such that
A1: a*u + b*v + c*w = 0.TOP-REAL 3;
A2: |[a,b,c]|`1 = a & |[a,b,c]|`2 = b & |[a,b,c]|`3 = c by EUCLID_5:2;
A3: c*w = |[c*0,c*0,c*1]| by EUCLID_5:8;
a*u = |[a*1,a*0,a*0]| & b*v = |[b*0,b*1,b*0]| by EUCLID_5:8;
then a*u + b*v + c*w = |[a+0,0+b,0+0]| + c*w by EUCLID_5:6
.= |[a+0,b+0,0+c]| by A3,EUCLID_5:6;
hence thesis by A1,A2,EUCLID_5:2,4;
end;
end;
theorem Th35:
not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & 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
implies P7,P8,P9 are_collinear
proof
assume that
A1: not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & f = 0) and
A2: {P1,P2,P3,P4,P5,P6} c= conic(a,b,c,d,e,f) and
A3: P1,P2,P3 are_collinear and
A4: P1,P2,P3,P4,P5,P6,P7,P8,P9 are_in_Pascal_configuration;
not P1,P4,P5 are_collinear by A4,COLLSP:8;
then consider N being invertible Matrix of 3,F_Real such that
A5: (homography(N)).P1 = Dir100 and
A6: (homography(N)).P2 = Dir010 and
A7: (homography(N)).P4 = Dir001 and
A8: (homography(N)).P5 = Dir111 by A4,ANPROJ_9:30;
consider u3 being Point of TOP-REAL 3 such that
A9: u3 is non zero and
A10: (homography(N)).P3 = Dir u3 by ANPROJ_1:26;
reconsider p31 = u3.1,p32 = u3.2, p33 = u3.3 as Real;
A11: u3`1 = u3.1 & u3`2 = u3.2 & u3`3 = u3.3 by EUCLID_5:def 1,def 2,def 3;
then
A12: (homography(N)).P3 = Dir |[ p31,p32,p33 ]| by A10,EUCLID_5:3;
consider u6 being Point of TOP-REAL 3 such that
A13: u6 is non zero and
A14: (homography(N)).P6 = Dir u6 by ANPROJ_1:26;
reconsider p61 = u6.1,p62 = u6.2, p63 = u6.3 as Real;
A15: u6`1 = u6.1 & u6`2 = u6.2 & u6`3 = u6.3 by EUCLID_5:def 1,def 2,def 3;
then
A16: (homography(N)).P6 = Dir |[ p61,p62,p63 ]| by A14,EUCLID_5:3;
A17: P1 in {P1,P2,P3,P4,P5,P6} & P2 in {P1,P2,P3,P4,P5,P6} &
P3 in {P1,P2,P3,P4,P5,P6} & P4 in {P1,P2,P3,P4,P5,P6} &
P5 in {P1,P2,P3,P4,P5,P6} & P6 in {P1,P2,P3,P4,P5,P6} by ENUMSET1:def 4;
consider a2,b2,c2,d2,e2,f2 be Real such that
A18: not (a2 = 0 & b2 = 0 & c2 = 0 & d2 = 0 & e2 = 0 & f2 = 0 ) and
A19: (homography(N)).P1 in conic(a2,b2,c2,d2,e2,f2) and
A20: (homography(N)).P2 in conic(a2,b2,c2,d2,e2,f2) and
A21: (homography(N)).P3 in conic(a2,b2,c2,d2,e2,f2) and
A22: (homography(N)).P4 in conic(a2,b2,c2,d2,e2,f2) and
A23: (homography(N)).P5 in conic(a2,b2,c2,d2,e2,f2) and
A24: (homography(N)).P6 in conic(a2,b2,c2,d2,e2,f2) by A17,A2,A1,Th17;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A25: Dir |[1,0,0]| = P and
A26: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A5,A19;
A27: qfconic(a2,b2,c2,d2,e2,f2,|[1,0,0]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[0,1,0]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 &
qfconic(a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0
proof
thus qfconic(a2,b2,c2,d2,e2,f2,|[1,0,0]|) = 0 by A25,A26,ANPROJ_9:10;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A28: Dir |[0,1,0]| = P and
A29: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A6,A20;
thus qfconic(a2,b2,c2,d2,e2,f2,|[0,1,0]|) = 0 by A28,A29,ANPROJ_9:10;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A30: Dir |[0,0,1]| = P and
A31: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A7,A22;
thus qfconic(a2,b2,c2,d2,e2,f2,|[0,0,1]|) = 0 by A30,A31,ANPROJ_9:10;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A32: Dir |[1,1,1]| = P and
A33: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A8,A23;
thus qfconic(a2,b2,c2,d2,e2,f2,|[1,1,1]|) = 0 by A32,A33,ANPROJ_9:10;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A34: Dir |[p31,p32,p33]| = P and
A35: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A12,A21;
|[p31,p32,p33]| is non zero & Dir |[p31,p32,p33]| = P
by A34,A9,A11,EUCLID_5:3;
hence qfconic(a2,b2,c2,d2,e2,f2,|[p31,p32,p33]|) = 0 by A35;
consider P be Point of ProjectiveSpace TOP-REAL 3 such that
A36: Dir |[p61,p62,p63]| = P and
A37: for u be Element of TOP-REAL 3 st u is non zero & P = Dir u holds
qfconic(a2,b2,c2,d2,e2,f2,u) = 0 by A16,A24;
|[p61,p62,p63]| is non zero & Dir |[p61,p62,p63]| = P
by A36,A15,EUCLID_5:3,A13;
hence qfconic(a2,b2,c2,d2,e2,f2,|[p61,p62,p63]|) = 0 by A37;
end;
reconsider a2f = a2,b2f = b2,c2f = c2,d2f = d2,e2f = e2,f2f = f2 as
Element of F_Real by XREAL_0:def 1;
qfconic(a2f,b2f,c2f,d2f,e2,f2f,|[1,0,0]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[0,1,0]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[0,0,1]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[1,1,1]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[p31,p32,p33]|) = 0 &
qfconic(a2f,b2f,c2f,d2f,e2f,f2f,|[p61,p62,p63]|) = 0 by A27;
then
A38: a2f = 0 & b2f = 0 & c2f = 0 by Th18;
then
A39: a2f = 0 & b2f = 0 & c2f = 0 & d2f + e2f + f2f = 0 by A27,Th18;
reconsider r1 = d2, r2 = f2 as Real;
|[1,0,0]| = <* 1,0,0 *> & <* 0,1,0 *> = |[0,1,0]| &
<* 0,0,1 *> = |[0,0,1]| & <* 1,1,1 *> = |[1,1,1]| &
<* p31,p32,p33 *> = |[p31,p32,p33]| &
<* p61,p62,p63 *> = |[p61,p62,p63]|;
then reconsider p1 = <* 1,0,0 *>, p2 = <* 0,1,0 *>,
p4 = <* 0,0,1 *>, p5 = <* 1,1,1 *>,
p3 = <* p31,p32,p33 *>, p6 = <* p61,p62,p63 *>
as Point of TOP-REAL 3;
A42: u3 = |[p31,p32,p33]| by EUCLID_5:3,A11;
A43: u6 = |[p61,p62,p63]| by A15,EUCLID_5:3;
A44: (r1 <> 0 or r2 <> 0) & qfconic(0,0,0,r1,-(r1+r2),r2,p3) = 0 &
qfconic(0,0,0,r1,-(r1+r2),r2,p6) = 0 by A39,A27,A18;
A45: p1`1 = 1 & p1`2 = 0 & p1`3 = 0 & p2`1 = 0 & p2`2 = 1 &
p2`3 = 0 & p3`1 = p31 & p3`2 = p32 & p3`3 = p33 by EUCLID_5:2;
A46: p3`1 = p3.1 & p3`2 = p3.2 & p3`3 = p3.3 by EUCLID_5:def 1,def 2,def 3;
A47: (homography(N)).P1 = Dir p1 & (homography(N)).P2 = Dir p2 &
(homography(N)).P3 = Dir p3 by A5,A6,A11,A10,EUCLID_5:3;
|{p1,p2,p3}| = 0
proof
consider u,v,w be Element of TOP-REAL 3 such that
A48: (homography(N)).P1 = Dir u and
A49: (homography(N)).P2 = Dir v and
A50: (homography(N)).P3 = Dir w and
A51: u is non zero and
A52: v is non zero and
A53: w is non zero and
A54: u,v,w are_LinDep by A3,ANPROJ_8:102,ANPROJ_2:23;
A55: [Dir u,Dir v,Dir w] in
the Collinearity of ProjectiveSpace(TOP-REAL 3)
by A51,A52,A53,A54,ANPROJ_1:25;
p1,p2,p3 are_LinDep
by A5,A6,A10,ANPROJ_9:10,A42,A9,A48,A49,A50,A55,ANPROJ_1:25;
hence thesis by ANPROJ_8:43;
end;
then
A56: 0 = 1 * p2`2 * p3`3 - 0 * p2`2*p3`1 - 1 *p2`3*p3`2 + 0 *p2`3*p3`1 -
0 *p2`1*p3`3 + 0 * p2`1*p3`2 by A45,ANPROJ_8:27
.= p3`3 by A45;
A57: p31 <> 0 & p32 <> 0
proof
assume p31 = 0 or p32 = 0;
then per cases;
suppose p31 = 0;
then
A58: p3 = |[ p32 * 0,p32 * 1,p32 * 0]| by A56,EUCLID_5:2
.= p32 * |[0,1,0]| by EUCLID_5:8;
now
p32 <> 0
proof
assume p32 = 0;
then p3 = |[0 * 0,0 * 1,0 * 0 ]| by A58,EUCLID_5:8
.= 0.TOP-REAL 3 by EUCLID_5:4;
hence thesis by A11,EUCLID_5:3,A9;
end;
hence are_Prop p3,|[0,1,0]| by A58,ANPROJ_1:1;
thus p3 is non zero by A11,EUCLID_5:3,A9;
thus |[0,1,0]| is non zero by ANPROJ_9:11;
end;
then (homography(N)).P3 = (homography(N)).P2 by A47,ANPROJ_1:22;
then P3 = P2 by ANPROJ_9:16;
hence contradiction by A4,ANPROJ_2:def 7;
end;
suppose p32 = 0;
then
A59: p3 = |[ p31 * 1,p31 * 0,p31 * 0]| by A56,EUCLID_5:2
.= p31 * |[1,0,0]| by EUCLID_5:8;
now
p31 <> 0
proof
assume p31 = 0;
then p3 = |[0 * 1,0 * 0,0 * 0 ]| by A59,EUCLID_5:8
.= 0.TOP-REAL 3 by EUCLID_5:4;
hence thesis by EUCLID_5:3,A11,A9;
end;
hence are_Prop p3,|[1,0,0]| by A59,ANPROJ_1:1;
thus p3 is non zero by EUCLID_5:3,A11,A9;
thus |[1,0,0]| is non zero by ANPROJ_9:11;
end;
then Dir p3 = Dir100 by ANPROJ_1:22;
then P3 = P1 by A47,ANPROJ_9:16;
hence contradiction by ANPROJ_2:def 7,A4;
end;
end;
now
A60: r1 = 0
proof
assume r1 <> 0;
then r1 * p31 <> 0 by A57,XCMPLX_1:6;
hence contradiction by A57,XCMPLX_1:6,A38,A27,A46,A56,A45;
end;
hence r2 * p6.3 * (p6.1 - p6.2) = 0 by A44;
thus r2 <> 0
proof
assume
A61: r2 = 0;
A62: a2f = 0 & b2f = 0 & c2f = 0 & d2f + e2f + f2f = 0
by A38,A27,Th18;
thus thesis by A18,A62,A60,A61;
end;
end;
then r2 <> 0 & ((r2 * p6.3) = 0 or p6.1 - p6.2 = 0) by XCMPLX_1:6;
then per cases by XCMPLX_1:6;
suppose p6.3 = 0;
then
A63: p6`3 = 0 by EUCLID_5:def 3;
A64: p6 = |[p61 + 0,0 + p62,0 + 0]| by A63,EUCLID_5:2
.= |[p61 * 1, p61 * 0,p61 * 0]| + |[p62 * 0,p62 * 1,p62 * 0]|
by EUCLID_5:6
.= p61 * |[1,0,0]| + |[p62 * 0,p62 * 1,p62 * 0]| by EUCLID_5:8
.= p61 * |[1,0,0]| + p62 * |[0,1,0]| by EUCLID_5:8;
per cases;
suppose p61 = 0 & p62 = 0;
then p6 = 0.TOP-REAL 3 by A63,EUCLID_5:2,4;
hence thesis by A15,EUCLID_5:3,A13;
end;
suppose
A65: p61 <> 0 & p62 = 0;
now
p6 = |[p61 * 1,p61 * 0,p61 * 0]| by A63,EUCLID_5:2,A65
.= p61 * |[1,0,0]| by EUCLID_5:8;
hence are_Prop p6,|[1,0,0]| by A65,ANPROJ_1:1;
thus p6 is non zero by A15,EUCLID_5:3,A13;
thus |[1,0,0]| is non zero by ANPROJ_9:11;
end;
then Dir p6 = Dir100 by ANPROJ_1:22;
then P1 = P6 by ANPROJ_9:16,A5,A14,A43;
hence thesis by A4,ANPROJ_2:def 7;
end;
suppose
A66: p61 = 0 & p62 <> 0;
now
p6 = |[p62 * 0,p62 * 1,p62 * 0]| by A63,EUCLID_5:2,A66
.= p62 * |[0,1,0]| by EUCLID_5:8;
hence are_Prop p6,|[0,1,0]| by A66,ANPROJ_1:1;
thus p6 is non zero by A15,EUCLID_5:3,A13;
thus |[0,1,0]| is non zero by ANPROJ_9:11;
end;
then Dir p6 = Dir010 by ANPROJ_1:22;
then P2 = P6 by ANPROJ_9:16,A6,A14,A43;
hence thesis by A4,ANPROJ_2:def 7;
end;
suppose p61 <> 0 & p62 <>0;
now
now
thus p6 = p61 * |[1,0,0]| + p62 * |[0,1,0]| by A64;
thus |[1,0,0]| is non zero by ANPROJ_9:11;
thus |[0,1,0]| is non zero by ANPROJ_9:11;
thus not are_Prop |[1,0,0]|,|[0,1,0]|
proof
assume are_Prop |[1,0,0]|,|[0,1,0]|;
then consider a be Real such that
a <> 0 and
A67: |[1,0,0]| = a * |[0,1,0]| by ANPROJ_1:1;
|[1,0,0]| = |[a * 0,a * 1,a * 0]| by A67,EUCLID_5:8
.= |[0,a,0]|;
hence thesis by FINSEQ_1:78;
end;
end;
hence |[1,0,0]|,|[0,1,0]|,p6 are_LinDep by ANPROJ_1:6;
thus |[1,0,0]| is non zero by ANPROJ_9:11;
thus |[0,1,0]| is non zero by ANPROJ_9:11;
thus p6 is non zero by A15,EUCLID_5:3,A13;
end;
then [Dir100,Dir010,Dir p6]
in the Collinearity of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:25;
hence thesis by A4,A5,A6,A14,A43,COLLSP:def 2,ANPROJ_8:102;
end;
end;
suppose
A68: p6.1 = p6.2;
A69: p61 = p6`1 by EUCLID_5:2
.= p6.2 by A68,EUCLID_5:def 1
.= p6`2 by EUCLID_5:def 2
.= p62 by EUCLID_5:2;
now
thus p4 is non zero by ANPROJ_9:11;
thus p5 is non zero by ANPROJ_9:11;
thus p6 is non zero by A13,A15,EUCLID_5:3;
|{p4,p5,p6}| = 0
proof
p6`1 = p61 & p6`2 = p61 & p4`1 = 0 & p4`2 = 0 & p4`3 = 1 &
p5`1 = 1 & p5`2 = 1 & p5`3 = 1 &
|{p4,p5,p6}| = p4`1 * p5`2 * p6`3
- p4`3*p5`2*p6`1- p4`1*p5`3*p6`2
+ p4`2*p5`3*p6`1 - p4`2*p5`1*p6`3
+ p4`3*p5`1*p6`2 by EUCLID_5:2,A69,ANPROJ_8:27;
hence thesis;
end;
hence |[0,0,1]|,|[1,1,1]|,p6 are_LinDep by ANPROJ_8:43;
end;
then
A70: [Dir001,Dir111,Dir p6]
in the Collinearity of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:25;
reconsider p1 = P1,p2 = P2,p3 = P3,q1 = P4,q2 = P5,
q3 = P6,r1 = P7,r2 = P8,r3 = P9 as
Element of ProjectiveSpace TOP-REAL 3;
p2<>p3 & p1<>p3 & q2<>q3 & q1<>q2 & q1<>q3 &
not p1,p2,q1 are_collinear & p1,p2,p3 are_collinear &
q1,q2,q3 are_collinear & p1,q2,r3 are_collinear &
q1,p2,r3 are_collinear & p1,q3,r2 are_collinear &
p3,q1,r2 are_collinear & p2,q3,r1 are_collinear &
p3,q2,r1 are_collinear
by COLLSP:2,A3,A4,A70,A7,A8,A14,A43,
COLLSP:def 2,ANPROJ_2:24,ANPROJ_8:102;
hence thesis by ANPROJ_8:57,HESSENBE:16;
end;
end;
::$N Pascal's theorem
::$L https://en.wikipedia.org/wiki/Pascal's_theorem Pascal's theorem
theorem
not (a = 0 & b = 0 & c = 0 & d = 0 & e = 0 & 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
implies
P7,P8,P9 are_collinear
proof
per cases;
suppose P1,P2,P3 are_collinear;
hence thesis by Th35;
end;
suppose not P1,P2,P3 are_collinear;
hence thesis by Th34;
end;
end;