pascal.miz
begin
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 ::
PASCAL:1
Th01: for p,q,r be
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 ::
PASCAL:2
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 ::
PASCAL:3
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 ::
PASCAL:4
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 ::
PASCAL:5
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 be
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 ::
PASCAL:6
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 ::
PASCAL:7
Th07: for M,N be
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 ::
PASCAL:8
Th08: for M be
Matrix of 3,
F_Real holds for a,b,c,d,e,f,g,h,i,x,y,z be
Element of
F_Real holds for v be
Element of (
TOP-REAL 3) holds for uf be
FinSequence of
F_Real holds for p be
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 be
Element of
F_Real ;
let v be
Element of (
TOP-REAL 3);
let uf be
FinSequence of
F_Real ;
let p be
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 be
Matrix of 3,
REAL st (
len p)
= 3 holds (((N1
* M)
* N2)
* p)
= (N1
* (M
* (N2
* p)))
proof
let N1,M,N2 be
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 be
Matrix of 3,
REAL holds (
len p)
= 3 implies
|((N
* p), (M
* (N
* p)))|
=
|(p, ((((N
@ )
* M)
* N)
* p))|
proof
let N,M be
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 be
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 be
Matrix of n,
REAL holds ((A
* ((B
* C)
* D))
* E)
= (((A
* B)
* C)
* (D
* E))
proof
let A,B,C,D,E be
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 be
Matrix of n,
F_Real holds (
MXF2MXR (A
* B))
= ((
MXF2MXR A)
* (
MXF2MXR B))
proof
let A,B be
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 be
Matrix of
REAL holds (
MXF2MXR (
MXR2MXF A))
= A
proof
let A be
Matrix of
REAL ;
(
MXF2MXR (
MXR2MXF A))
= (
MXR2MXF A) by
MATRIXR1:def 2
.= A by
MATRIXR1:def 1;
hence thesis;
end;
Lm07: for A,B be
Matrix of n,
REAL holds (
MXR2MXF (A
* B))
= ((
MXR2MXF A)
* (
MXR2MXF B))
proof
let A,B be
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 be
invertible
Matrix of 3,
F_Real holds for NR be
Matrix of 3,
REAL st NR
= (
MXF2MXR N) holds (NR
* (
MXF2MXR ((
MXR2MXF NR)
~ )))
= (
1_Rmatrix 3)
proof
let N be
invertible
Matrix of 3,
F_Real ;
let NR be
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 be
invertible
Matrix of 3,
F_Real holds for NR be
Matrix of 3,
REAL st NR
= (
MXF2MXR N) holds ((NR
@ )
* (
MXF2MXR ((
MXR2MXF (NR
@ ))
~ )))
= (
1_Rmatrix 3)
proof
let N be
invertible
Matrix of 3,
F_Real ;
let NR be
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 be
invertible
Matrix of 3,
F_Real holds for NR be
Matrix of 3,
REAL st NR
= (
MXF2MXR N) holds ((
MXF2MXR ((
MXR2MXF NR)
~ ))
* NR)
= (
1_Rmatrix 3)
proof
let N be
invertible
Matrix of 3,
F_Real ;
let NR be
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 be
invertible
Matrix of 3,
F_Real holds for NR be
Matrix of 3,
REAL st NR
= (
MXF2MXR N) holds ((
MXF2MXR ((
MXR2MXF (NR
@ ))
~ ))
* (NR
@ ))
= (
1_Rmatrix 3)
proof
let N be
invertible
Matrix of 3,
F_Real ;
let NR be
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 be
invertible
Matrix of 3,
F_Real holds for NR be
Matrix of 3,
REAL st NR
= (
MXF2MXR N) holds (NR
@ ) is
invertible
proof
let N be
invertible
Matrix of 3,
F_Real ;
let NR be
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 be
invertible
Matrix of 3,
F_Real holds for NR,M,M2 be
Matrix of 3,
REAL st NR
= (
MXF2MXR N) & M2
= (((
MXF2MXR ((
MXR2MXF (NR
@ ))
~ ))
* M)
* (
MXF2MXR ((
MXR2MXF NR)
~ ))) holds (((NR
@ )
* M2)
* NR)
= M
proof
let N be
invertible
Matrix of 3,
F_Real ;
let NR,M,M2 be
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 be
invertible
Matrix of n,
F_Real holds for M be
Matrix of n,
REAL st M
= (
MXF2MXR N) holds M is
invertible
proof
let N be
invertible
Matrix of n,
F_Real ;
let M be
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 be
Matrix of n,
F_Real holds for M be
Matrix of n,
REAL st M is
invertible & N
= (
MXR2MXF M) holds N is
invertible
proof
let N be
Matrix of n,
F_Real ;
let M be
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,
MATRIX_6:def 3;
end;
theorem ::
PASCAL:9
Th09: for M be
Matrix of 3,
REAL holds for a,b,c,d,e,f,g,h,i,p1,p2,p3 be
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 be
Matrix of 3,
REAL ;
let a,b,c,d,e,f,g,h,i,p1,p2,p3 be
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 be
Matrix of 3,
REAL st p
= (
0. (
TOP-REAL 3)) holds (M
* p)
= p
proof
let M be
Matrix of 3,
REAL ;
assume
A1: p
= (
0. (
TOP-REAL 3));
consider a,b,c,d,e,f,g,h,i be
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 be
Matrix of n, K st n
>
0 holds (M
* (
0. (K,n,n)))
= (
0. (K,n,n))
proof
let M be
Matrix of n, K;
assume
A1: n
>
0 ;
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,
A1,
MATRIX_4: 62;
hence thesis by
A4,
MATRIX_4: 6;
end;
Lm20: for M be
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
definition
let a,b,c,d,e,f be
Real;
let u be
Element of (
TOP-REAL 3);
::
PASCAL:def1
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;
::
PASCAL:def2
func
conic (a,b,c,d,e,f) ->
Subset of (
ProjectiveSpace (
TOP-REAL 3)) equals { P where P be
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 };
coherence
proof
set C = { P where P be
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 ::
PASCAL:10
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 ::
PASCAL:11
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;
::
PASCAL:def3
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 ::
PASCAL:12
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 ::
PASCAL:13
Th13: for a,b,c,d,e,f be
Real, u be
Point of (
TOP-REAL 3), M be
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 be
Real;
let u be
Point of (
TOP-REAL 3);
let M be
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 ::
PASCAL:14
Th14: for N be
invertible
Matrix of 3,
F_Real holds for NR,M1,M2 be
Matrix of 3,
REAL holds for a,b,c,d,e,f be
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 be
invertible
Matrix of 3,
F_Real ;
let NR,M1,M2 be
Matrix of 3,
REAL ;
let a,b,c,d,e,f be
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 ::
PASCAL:15
Th15: for a1,a2,a3,a4,a5,a6,b1,b2,b3,b4,b5,b6 be
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 be
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 ::
PASCAL:16
Th16: for a,b,c,d,e,f be
Real holds for P be
Point of (
ProjectiveSpace (
TOP-REAL 3)) holds for N be
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 be
Real holds for M1,M2 be
Matrix of 3,
REAL holds for NR be
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 be
Point of (
ProjectiveSpace (
TOP-REAL 3));
let N be
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 be
Element of (
TOP-REAL 3), ufh be
FinSequence of
F_Real , ph be
FinSequence of (1
-tuples_on
REAL ) such that
A6: P
= (
Dir uh) & not uh is
zero & uh
= ufh & ph
= (N
* ufh) & vh
= (
M2F ph) & not vh is
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 be
Real holds for UM1,UM2 be
Matrix of 3,
REAL holds for UNR be
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 be
Real;
let UM1,UM2 be
Matrix of 3,
REAL ;
let UNR be
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 ::
PASCAL:17
Th17: for a,b,c,d,e,f be
Real holds for P1,P2,P3,P4,P5,P6 be
Point of (
ProjectiveSpace (
TOP-REAL 3)) holds for N be
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 be
Real;
let P1,P2,P3,P4,P5,P6 be
Point of (
ProjectiveSpace (
TOP-REAL 3));
let N be
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 ::
PASCAL:18
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
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 be
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 ::
PASCAL:19
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 ::
PASCAL:20
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 ::
PASCAL:21
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 ::
PASCAL:22
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 ::
PASCAL:23
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 ::
PASCAL:24
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 ::
PASCAL:25
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 ::
PASCAL:26
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 ::
PASCAL:27
Th27: for r125,r136,r246,r345,r126,r135,r245,r346,r157,r259,r597,r368,r268,r297,r247,r287,r358,r587 be 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 be 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 ::
PASCAL:28
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 ::
PASCAL:29
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 ::
PASCAL:30
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;
theorem ::
PASCAL:31
Th31: for PCPP be
CollProjectiveSpace holds for c1,c2,c3,c4,c5,c6,c7,c8,c9 be
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 be
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 be
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 be
Element of PCPP;
(v104,v100,v104)
are_collinear by
COLLSP: 5;
hence thesis by
COLLSP: 3;
end;
A38: for v102,v104,v100,v103 be
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 be
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 be
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 be
Element of PCPP;
(v101,v104,v104)
are_collinear by
COLLSP: 2;
hence thesis by
COLLSP: 3;
end;
A105: for v103,v104,v102,v101 be
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 be
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 be
Element of PCPP holds v101
= v100 or not (v100,v101,v2)
are_collinear or (v2,v101,v100)
are_collinear
proof
let v2,v101,v100 be
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 be
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 be
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 be
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 be
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));
::
PASCAL:def4
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 ::
PASCAL:32
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 ::
PASCAL:33
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 be
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 be
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,
EUCLID_5:def 2,
EUCLID_5:def 3;
then
A39: ((
homography N)
. P5)
= (
Dir
|[p51, p52, p53]|) by
A37,
EUCLID_5: 3;
consider u6 be
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,
EUCLID_5:def 2,
EUCLID_5:def 3;
then
A43: ((
homography N)
. P6)
= (
Dir
|[p61, p62, p63]|) by
A41,
EUCLID_5: 3;
consider u7 be
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,
EUCLID_5:def 2,
EUCLID_5:def 3;
then
A47: ((
homography N)
. P7)
= (
Dir
|[p71, p72, p73]|) by
A45,
EUCLID_5: 3;
consider u8 be
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,
EUCLID_5:def 2,
EUCLID_5:def 3;
then
A51: ((
homography N)
. P8)
= (
Dir
|[p81, p82, p83]|) by
A49,
EUCLID_5: 3;
consider u9 be
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,
EUCLID_5:def 2,
EUCLID_5: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 ::
PASCAL:34
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,
EUCLID_5: 4;
end;
end
theorem ::
PASCAL:35
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 be
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 be
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,
EUCLID_5:def 2,
EUCLID_5:def 3;
then
A12: ((
homography N)
. P3)
= (
Dir
|[p31, p32, p33]|) by
A10,
EUCLID_5: 3;
consider u6 be
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,
EUCLID_5:def 2,
EUCLID_5: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,
EUCLID_5:def 2,
EUCLID_5: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 ;
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;
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,
EUCLID_5: 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;
::$Notion-Name
theorem ::
PASCAL:36
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;