:: Principle of Duality in Real Projective Plane: a Proof of the Converse
:: of {D}esargues' Theorem and a Proof of the Converse of {P}appus'
:: Theorem by Transport
:: by Roland Coghetto
::
:: Received September 30, 2021
:: Copyright (c) 2021-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies INCSP_1, ANPROJ11, REAL_1, XCMPLX_0, ANPROJ_1, ANPROJ_2,
PENCIL_1, MCART_1, EUCLID_5, ARYTM_1, ARYTM_3, CARD_1, EUCLID, FUNCT_1,
NUMBERS, PRE_TOPC, RELAT_1, SUBSET_1, SUPINF_2, ANPROJ_9, TARSKI,
INCPROJ, RVSUM_1, BKMODEL1, CARD_FIL, PROJRED2, PBOOLE, RELAT_2, AFF_2,
VECTSP_1, ANALOAF;
notations TARSKI, SUBSET_1, XCMPLX_0, PRE_TOPC, RVSUM_1, COLLSP, INCPROJ,
ANPROJ_9, XREAL_0, NUMBERS, FUNCT_1, FINSEQ_2, EUCLID, ANPROJ_1,
BKMODEL1, STRUCT_0, RLVECT_1, EUCLID_5, INCSP_1, PROJRED2, ANPROJ_2;
constructors MONOID_0, EUCLID_5, ANPROJ_9, BKMODEL1, EUCLID_8, PROJRED2;
registrations BKMODEL3, ORDINAL1, ANPROJ_1, STRUCT_0, XREAL_0, MONOID_0,
EUCLID, VALUED_0, ANPROJ_2, FUNCT_1, FINSEQ_1, XCMPLX_0, INCPROJ, PASCAL;
requirements SUBSET, NUMERALS, ARITHM, BOOLE;
equalities BKMODEL1, XCMPLX_0, COLLSP, INCPROJ, ANPROJ_9, EUCLID_5;
expansions TARSKI, XBOOLE_0, STRUCT_0, PROJRED2;
theorems EUCLID_8, EUCLID_5, ANPROJ_1, ANPROJ_2, EUCLID, XCMPLX_1, RVSUM_1,
FINSEQ_1, ANPROJ_8, INCPROJ, ANPROJ_9, XBOOLE_0, COLLSP, BKMODEL1,
EUCLID_4;
begin ::Preliminaries
theorem
for a,b,c,d,e,f,g,h,i being Real holds
|{ |[a,b,c]|,
|[d,e,f]|,
|[g,h,i]| }| = a * e * i + b * f * g + c * d * h
- g * e * c - h * f * a - i * d * b
proof
let a,b,c,d,e,f,g,h,i be Real;
reconsider p = |[a,b,c]|, q = |[d,e,f]|, r = |[g,h,i]| as
Element of TOP-REAL 3;
|{ |[a,b,c]|,
|[d,e,f]|,
|[g,h,i]| }| = p`1 * q`2 * r`3 - p`3*q`2*r`1 - p`1*q`3*r`2
+ p`2*q`3*r`1 - p`2*q`1*r`3 + p`3*q`1*r`2 by ANPROJ_8:27;
hence thesis;
end;
theorem Th2:
for a,b,c,d,e being Real holds
|{ |[a,1,0]|,
|[b,0,1]|,
|[c,d,e]| }| = c - a * d - e * b
proof
let a,b,c,d,e be Real;
reconsider p = |[a,1,0]|, q = |[b,0,1]|, r = |[c,d,e]| as
Element of TOP-REAL 3;
|{ |[a,1,0]|,
|[b,0,1]|,
|[c,d,e]| }| = p`1 * q`2 * r`3 - p`3*q`2*r`1 - p`1*q`3*r`2
+ p`2*q`3*r`1 - p`2*q`1*r`3 + p`3*q`1*r`2 by ANPROJ_8:27;
hence thesis;
end;
theorem Th3:
for a,b,c,d,e being Real holds
|{ |[1,a,0]|,
|[0,b,1]|,
|[c,d,e]| }| = b * e + a * c - d
proof
let a,b,c,d,e be Real;
reconsider p = |[1,a,0]|, q = |[0,b,1]|, r = |[c,d,e]| as
Element of TOP-REAL 3;
|{ |[1,a,0]|,
|[0,b,1]|,
|[c,d,e]| }| = p`1 * q`2 * r`3 - p`3*q`2*r`1 - p`1*q`3*r`2
+ p`2*q`3*r`1 - p`2*q`1*r`3 + p`3*q`1*r`2 by ANPROJ_8:27;
hence thesis;
end;
theorem Th4:
for a,b,c,d,e being Real holds
|{ |[1,0,a]|,
|[0,1,b]|,
|[c,d,e]| }| = e - c * a - d * b
proof
let a,b,c,d,e be Real;
reconsider p = |[1,0,a]|, q = |[0,1,b]|, r = |[c,d,e]| as
Element of TOP-REAL 3;
|{ |[1,0,a]|,
|[0,1,b]|,
|[c,d,e]| }| = p`1 * q`2 * r`3 - p`3*q`2*r`1 - p`1*q`3*r`2
+ p`2*q`3*r`1 - p`2*q`1*r`3 + p`3*q`1*r`2 by ANPROJ_8:27;
hence thesis;
end;
theorem Th5:
for u being Element of TOP-REAL 3 holds u is zero iff |( u, u )| = 0
proof
let u be Element of TOP-REAL 3;
reconsider un = u as Element of REAL 3 by EUCLID:22;
hereby
assume u is zero;
then 0.REAL 3 = u by EUCLID:66;
then |( un,un )| = 0 by EUCLID_4:17;
hence |( u, u )| = 0;
end;
assume |( u, u )| = 0;
then un = 0.REAL 3 by EUCLID_4:17;
hence thesis by EUCLID:66;
end;
theorem
for u,v,w being non zero Element of TOP-REAL 3 st |{u,v,w}| = 0
holds ex p being non zero Element of TOP-REAL 3 st
|(p,u)| = 0 & |(p,v)| = 0 & |(p,w)| = 0
proof
let u,v,w be non zero Element of TOP-REAL 3;
assume
A1: |{u,v,w}| = 0;
reconsider p = |[u`1,v`1,w`1]|,
q = |[u`2,v`2,w`2]|,
r = |[u`3,v`3,w`3]| as Element of TOP-REAL 3;
A3: |{ p,q,r }| = p`1 * q`2 * r`3 - p`3*q`2*r`1 - p`1*q`3*r`2 + p`2*q`3*r`1 -
p`2*q`1*r`3 + p`3*q`1*r`2 by ANPROJ_8:27;
|{u,v,w}| = u`1 * v`2 * w`3 - u`3*v`2*w`1 - u`1*v`3*w`2 + u`2*v`3*w`1 -
u`2*v`1*w`3 + u`3*v`1*w`2 by ANPROJ_8:27;
then consider a,b,c be Real such that
A4: a * p + b * q + c * r = 0.TOP-REAL 3 and
A5: a <> 0 or b <> 0 or c <> 0 by A1,A3,ANPROJ_8:42;
A6: |[0,0,0]|
= |[a * p`1,a * p`2,a * p`3]| + b * q + c * r by A4,EUCLID_5:4,7
.= |[a * p`1,a * p`2,a * p`3]| + |[b * q`1,b * q`2,b * q`3]| + c * r
by EUCLID_5:7
.= |[a * p`1,a * p`2,a * p`3]| + |[b * q`1,b * q`2,b * q`3]|
+ |[c * r`1,c * r`2,c * r`3]| by EUCLID_5:7
.= |[a * p`1+b*q`1,a * p`2+b*q`2,a * p`3+b*q`3]|
+ |[c * r`1,c * r`2,c * r`3]| by EUCLID_5:6
.= |[a * p`1+b*q`1+c*r`1,a * p`2+b*q`2+c*r`2,a * p`3+b*q`3+c*r`3]|
by EUCLID_5:6;
reconsider p = |[a,b,c]| as non zero Element of TOP-REAL 3 by A5;
take p;
thus |(p,u)| = p`1 * u`1 + p`2 * u`2 + p`3 * u`3 by EUCLID_5:29
.= a * u`1+p`2*u`2+p`3*u`3
.= a * u`1+b*u`2+p`3*u`3
.= a * u`1+b*u`2+c*u`3
.= 0 by A6,FINSEQ_1:78;
thus |(p,v)| = p`1 * v`1 + p`2 * v`2 + p`3 * v`3 by EUCLID_5:29
.= a * v`1+p`2*v`2+p`3*v`3
.= a * v`1+b*v`2+p`3*v`3
.= a * v`1+b*v`2+c*v`3
.= 0 by A6,FINSEQ_1:78;
thus |(p,w)| = p`1 * w`1 + p`2 * w`2 + p`3 * w`3 by EUCLID_5:29
.= a * w`1+p`2*w`2+p`3*w`3
.= a * w`1+b*w`2+p`3*w`3
.= a * w`1+b*w`2+c*w`3
.= 0 by A6,FINSEQ_1:78;
end;
theorem Th7:
for u,v,w being non zero Element of TOP-REAL 3 st
|(u,v)| = 0 & are_Prop w,v holds |(u,w)| = 0
proof
let u,v,w be non zero Element of TOP-REAL 3;
assume that
A1: |(u,v)| = 0 and
A2: are_Prop w,v;
consider a be Real such that
a <> 0 and
A3: w = a * v by A2,ANPROJ_1:1;
reconsider un = u,vn = v as Element of REAL 3 by EUCLID:22;
thus |(u,w)| = |(a * vn,un)| by A3
.= a * |(v,u)| by EUCLID_8:68
.= 0 by A1;
end;
theorem Th8:
for a,u,v being non zero Element of TOP-REAL 3 st not are_Prop u,v &
|(a,u)| = 0 & |(a,v)| = 0 holds are_Prop a,u <X> v
proof
let a,u,v be non zero Element of TOP-REAL 3;
assume that
A1: not are_Prop u,v and
A2: |(a,u)| = 0 and
A3: |(a,v)| = 0;
u <X> v is non zero by A1,ANPROJ_8:51;
then reconsider uv = u <X> v as non zero Element of TOP-REAL 3;
A4: a`1 * u`1 + a`2 * u`2 + a`3 * u`3 = 0 &
a`1 * v`1 + a`2 * v`2 + a`3 * v`3 = 0 by A2,A3,EUCLID_5:29;
per cases by EUCLID_5:3,4;
suppose
A5: a`1 <> 0;
then
A6: u`1 = -a`2/a`1 * u`2 - a`3/a`1 * u`3 &
v`1 = -a`2/a`1 * v`2 - a`3/a`1 * v`3 by A4,ANPROJ_8:13;
set p1 = u,p2 = v;
now
reconsider r = a`1 as Real;
thus
A7: u <X> v = |[ 1 *( p1`2 * p2`3 - p1`3 * p2`2),
a`2/a`1 *( p1`2 * p2`3 - p1`3 * p2`2),
(a`3/a`1) * (- p1`3*p2`2 + p1`2*p2`3) ]| by A6
.= ( p1`2 * p2`3 - p1`3 * p2`2) * |[ 1 ,a`2/a`1, a`3/a`1 ]|
by EUCLID_5:8
.= ( p1`2 * p2`3 - p1`3 * p2`2) * |[ a`1 / r, a`2 / r, a`3 / r ]|
by A5,XCMPLX_1:60
.= ( p1`2 * p2`3 - p1`3 * p2`2) * ((1/a`1) * a) by EUCLID_5:7
.= (( p1`2 * p2`3 - p1`3 * p2`2) * (1/a`1)) * a by RVSUM_1:49;
p1`2 * p2`3 - p1`3 * p2`2 <> 0
proof
assume p1`2 * p2`3 - p1`3 * p2`2 = 0;
then u <X> v = |[0 * a`1,0 * a`2,0 * a`3]| by A7,EUCLID_5:7
.= 0.TOP-REAL 3 by EUCLID_5:4;
hence thesis by A1,ANPROJ_8:51;
end;
hence (p1`2 * p2`3 - p1`3 * p2`2) * (1/a`1) <> 0 by A5;
end;
hence thesis by ANPROJ_1:1;
end;
suppose
A8: a`2 <> 0;
then
A9: u`2 = -a`1/a`2 * u`1 - a`3/a`2 * u`3 &
v`2 = -a`1/a`2 * v`1 - a`3/a`2 * v`3 by A4,ANPROJ_8:13;
set p1 = u, p2 = v;
now
reconsider r = a`2 as Real;
thus
A10: u <X> v = |[ (a`1/a`2) *( p1`3 * p2`1 - p1`1 * p2`3),
1 *( p1`3 * p2`1 - p1`1 * p2`3),
(a`3/a`2) * ( p1`3*p2`1 - p1`1*p2`3) ]| by A9
.= (p1`3*p2`1-p1`1*p2`3) * |[a`1/a`2,1,a`3/a`2]| by EUCLID_5:8
.= (p1`3*p2`1-p1`1*p2`3) * |[a`1/r,r/r,a`3/r]| by A8,XCMPLX_1:60
.= (p1`3*p2`1-p1`1*p2`3) * ((1/a`2) * a) by EUCLID_5:7
.= ((p1`3*p2`1-p1`1*p2`3) * (1/a`2)) * a by RVSUM_1:49;
p1`3*p2`1-p1`1*p2`3 <> 0
proof
assume p1`3*p2`1-p1`1*p2`3 = 0;
then u <X> v = |[0 * a`1,0 * a`2,0 * a`3]| by A10,EUCLID_5:7
.= 0.TOP-REAL 3 by EUCLID_5:4;
hence thesis by A1,ANPROJ_8:51;
end;
hence (p1`3*p2`1-p1`1*p2`3) * (1/a`2) <> 0 by A8;
end;
hence thesis by ANPROJ_1:1;
end;
suppose
A11: a`3 <> 0;
a`3 * u`3 + a`1 * u`1 + a`2 * u`2 = 0 &
a`3 * v`3 + a`1 * v`1 + a`2 * v`2 = 0 by A4;
then
A12: u`3 = -a`1/a`3 * u`1 - a`2/a`3 * u`2 &
v`3 = -a`1/a`3 * v`1 - a`2/a`3 * v`2 by A11,ANPROJ_8:13;
set p1 = u, p2 = v;
now
reconsider r = a`3 as Real;
thus
A13: u <X> v = |[ (a`1/a`3) * (p1`1 * p2`2 - p1`2 * p2`1),
a`2/a`3 * (p1`1 * p2`2 - p1`2 * p2`1),
1 * (p1`1 * p2`2 - p1`2 * p2`1) ]| by A12
.= (p1`1*p2`2-p1`2*p2`1) * |[a`1/a`3,a`2/a`3,1]| by EUCLID_5:8
.= (p1`1*p2`2-p1`2*p2`1) * |[a`1/r,a`2/r,r/r]|
by A11,XCMPLX_1:60
.= (p1`1*p2`2-p1`2*p2`1) * ((1/a`3) * a) by EUCLID_5:7
.= ((p1`1*p2`2-p1`2*p2`1) * (1/a`3)) * a by RVSUM_1:49;
p1`1*p2`2-p1`2*p2`1 <> 0
proof
assume p1`1*p2`2-p1`2*p2`1 = 0;
then u <X> v = |[0 * a`1,0 * a`2,0 * a`3]| by A13,EUCLID_5:7
.= 0.TOP-REAL 3 by EUCLID_5:4;
hence thesis by A1,ANPROJ_8:51;
end;
hence (p1`1*p2`2-p1`2*p2`1) * (1/a`3) <> 0 by A11;
end;
hence thesis by ANPROJ_1:1;
end;
end;
theorem Th9:
for u,v being non zero Element of TOP-REAL 3
for r being Real st r <> 0 & are_Prop u,v holds are_Prop r * u,v
proof
let u,v be non zero Element of TOP-REAL 3;
let r be Real;
assume that
A1: r <> 0 and
A2: are_Prop u,v;
consider a be Real such that
A3: a <> 0 and
A4: u = a * v by ANPROJ_1:1,A2;
r * u = (r * a) * v by A4,RVSUM_1:49;
hence thesis by A1,A3,ANPROJ_1:1;
end;
begin :: Alignment of definitions
definition
let P being Point of ProjectiveSpace TOP-REAL 3;
attr P is zero_proj1 means
:Def1:
for u being non zero Element of TOP-REAL 3 st P = Dir u holds u.1 = 0;
end;
registration
cluster zero_proj1 for Point of ProjectiveSpace TOP-REAL 3;
existence
proof
take Dir001;
reconsider p = |[0,0,1]| as non zero Element of TOP-REAL 3;
now
let u be non zero Element of TOP-REAL 3;
assume Dir001 = Dir u;
then are_Prop u, p by ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A1: u = a * p by ANPROJ_1:1;
thus u.1 = a * p.1 by A1,RVSUM_1:44
.= a * 0
.= 0;
end;
hence thesis;
end;
end;
registration
cluster non zero_proj1 for Point of ProjectiveSpace TOP-REAL 3;
existence
proof
set P = Dir100;
take P;
reconsider u = |[1,0,0]| as non zero Element of TOP-REAL 3;
now
thus P = Dir u;
thus u.1 <> 0;
end;
hence thesis;
end;
end;
theorem Th10:
for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st P = Dir u holds
u.1 <> 0
proof
let P be non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
assume
A1: P = Dir u;
consider u9 be non zero Element of TOP-REAL 3 such that
A2: P = Dir u9 and
A3: u9.1 <> 0 by Def1;
are_Prop u,u9 by A1,A2,ANPROJ_1:22;
then consider a be Real such that
A4: a <> 0 and
A5: u = a * u9 by ANPROJ_1:1;
assume u.1 = 0;
then a * u9.1 = 0 by A5,RVSUM_1:44;
hence thesis by A3,A4;
end;
definition
let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
func normalize_proj1(P) -> non zero Element of TOP-REAL 3 means
:Def2:
Dir it = P & it.1 = 1;
existence
proof
consider u be non zero Element of TOP-REAL 3 such that
A1: P = Dir u and
A2: u.1 <> 0 by Def1;
reconsider v = |[1, u`2/u.1,u`3/u.1]| as non zero Element of TOP-REAL 3;
take v;
u.1 * v = |[u.1 * 1, u.1 * (u`2/u.1),u.1*(u`3/u.1)]| by EUCLID_5:8
.= |[u.1, u`2, u.1*(u`3/u.1)]| by XCMPLX_1:87,A2
.= |[u`1, u`2, u`3]| by A2,XCMPLX_1:87
.= u by EUCLID_5:3;
then are_Prop u,v by A2,ANPROJ_1:1;
hence thesis by A1,ANPROJ_1:22;
end;
uniqueness
proof
let u,v be non zero Element of TOP-REAL 3 such that
A4: P = Dir u & u.1 = 1 and
A5: P = Dir v & v.1 = 1;
are_Prop u,v by A4,A5,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A6: u = a * v by ANPROJ_1:1;
A7: 1 = a * v.1 by A4,A6,RVSUM_1:44
.= a by A5;
a * v = |[a * v`1, a * v`2, a * v`3]| by EUCLID_5:7
.= v by A7,EUCLID_5:3;
hence thesis by A6;
end;
end;
theorem Th11:
for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st P = Dir u holds
normalize_proj1 P = |[1, u.2/u.1,u.3/u.1]|
proof
let P be non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
let u9 be non zero Element of TOP-REAL 3;
assume P = Dir u9;
then Dir u9 = Dir normalize_proj1 P by Def2;
then are_Prop u9,normalize_proj1 P by ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A1: normalize_proj1 P = a * u9 by ANPROJ_1:1;
A2: normalize_proj1 P = |[a * u9`1,a * u9`2,a * u9`3 ]| by A1,EUCLID_5:7;
A3: 1 = (normalize_proj1 P)`1 by Def2
.= a * u9`1 by A2;
then
A4: u9`1 = 1 / a & a = 1 / u9`1 by XCMPLX_1:73;
normalize_proj1 P = |[ 1,u9`2 / u9`1,(1 / u9`1) * u9`3]|
by A1,A3,A4,EUCLID_5:7
.= |[ 1,u9.2 / u9.1,u9.3/u9.1]|;
hence thesis;
end;
theorem
for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
for Q being Point of ProjectiveSpace TOP-REAL 3 st
Q = Dir normalize_proj1(P) holds Q is non zero_proj1 by Def2;
definition
let P being Point of ProjectiveSpace TOP-REAL 3;
attr P is zero_proj2 means
:Def3:
for u being non zero Element of TOP-REAL 3 st P = Dir u holds u.2 = 0;
end;
registration
cluster zero_proj2 for Point of ProjectiveSpace TOP-REAL 3;
existence
proof
take Dir001;
reconsider p = |[0,0,1]| as non zero Element of TOP-REAL 3;
now
let u be non zero Element of TOP-REAL 3;
assume Dir001 = Dir u;
then are_Prop u, p by ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A1: u = a * p by ANPROJ_1:1;
thus u.2 = a * p.2 by A1,RVSUM_1:44
.= a * 0
.= 0;
end;
hence thesis;
end;
end;
registration
cluster non zero_proj2 for Point of ProjectiveSpace TOP-REAL 3;
existence
proof
set P = Dir010;
take P;
reconsider u = |[0,1,0]| as non zero Element of TOP-REAL 3;
now
thus P = Dir u;
thus u.2 <> 0;
end;
hence thesis;
end;
end;
theorem Th13:
for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st P = Dir u holds
u.2 <> 0
proof
let P be non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
assume
A1: P = Dir u;
consider u9 be non zero Element of TOP-REAL 3 such that
A2: P = Dir u9 and
A3: u9.2 <> 0 by Def3;
are_Prop u,u9 by A1,A2,ANPROJ_1:22;
then consider a be Real such that
A4: a <> 0 and
A5: u = a * u9 by ANPROJ_1:1;
assume u.2 = 0;
then a * u9.2 = 0 by A5,RVSUM_1:44;
hence thesis by A3,A4;
end;
definition
let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
func normalize_proj2(P) -> non zero Element of TOP-REAL 3 means
:Def4:
Dir it = P & it.2 = 1;
existence
proof
consider u be non zero Element of TOP-REAL 3 such that
A1: P = Dir u and
A2: u.2 <> 0 by Def3;
reconsider v = |[u`1/u.2, 1,u`3/u.2]| as non zero Element of TOP-REAL 3;
take v;
u.2 * v = |[u.2 * (u`1/u.2), u.2 * 1,u.2*(u`3/u.2)]| by EUCLID_5:8
.= |[u`1, u.2, u.2*(u`3/u.2)]| by XCMPLX_1:87,A2
.= |[u`1, u`2, u`3]| by A2,XCMPLX_1:87
.= u by EUCLID_5:3;
then are_Prop u,v by A2,ANPROJ_1:1;
hence thesis by A1,ANPROJ_1:22;
end;
uniqueness
proof
let u,v being non zero Element of TOP-REAL 3 such that
A4: P = Dir u & u.2 = 1 and
A5: P = Dir v & v.2 = 1;
are_Prop u,v by A4,A5,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A6: u = a * v by ANPROJ_1:1;
A7: 1 = a * v.2 by A4,A6,RVSUM_1:44
.= a by A5;
a * v = |[a * v`1, a * v`2, a * v`3]| by EUCLID_5:7
.= v by A7,EUCLID_5:3;
hence thesis by A6;
end;
end;
theorem Th14:
for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st P = Dir u holds
normalize_proj2 P = |[u.1/u.2,1,u.3/u.2]|
proof
let P be non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
let u9 be non zero Element of TOP-REAL 3;
assume P = Dir u9;
then Dir u9 = Dir normalize_proj2 P by Def4;
then are_Prop u9,normalize_proj2 P by ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A1: normalize_proj2 P = a * u9 by ANPROJ_1:1;
A2: normalize_proj2 P = |[a * u9`1,a * u9`2,a * u9`3 ]| by A1,EUCLID_5:7;
A3: 1 = (normalize_proj2 P)`2 by Def4
.= a * u9`2 by A2;
then
A4: u9`2 = 1 / a & a = 1 / u9`2 by XCMPLX_1:73;
normalize_proj2 P = |[ u9`1 / u9`2,1,(1 / u9`2) * u9`3]|
by A1,A3,A4,EUCLID_5:7
.= |[ u9.1 / u9.2,1,u9.3/u9.2]|;
hence thesis;
end;
theorem
for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
for Q being Point of ProjectiveSpace TOP-REAL 3 st
Q = Dir normalize_proj2(P) holds Q is non zero_proj2 by Def4;
definition
let P being Point of ProjectiveSpace TOP-REAL 3;
attr P is zero_proj3 means
:Def5:
for u being non zero Element of TOP-REAL 3 st P = Dir u holds u.3 = 0;
end;
registration
cluster zero_proj3 for Point of ProjectiveSpace TOP-REAL 3;
existence
proof
take Dir100;
reconsider p = |[1,0,0]| as non zero Element of TOP-REAL 3;
now
let u be non zero Element of TOP-REAL 3;
assume Dir100 = Dir u;
then are_Prop u, p by ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A1: u = a * p by ANPROJ_1:1;
thus u.3 = a * p.3 by A1,RVSUM_1:44
.= a * 0
.= 0;
end;
hence thesis;
end;
end;
registration
cluster non zero_proj3 for Point of ProjectiveSpace TOP-REAL 3;
existence
proof
set P = Dir001;
take P;
reconsider u = |[0,0,1]| as non zero Element of TOP-REAL 3;
now
thus P = Dir u;
thus u.3 <> 0;
end;
hence thesis;
end;
end;
theorem Th16:
for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st P = Dir u holds
u.3 <> 0
proof
let P be non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
assume
A1: P = Dir u;
consider u9 be non zero Element of TOP-REAL 3 such that
A2: P = Dir u9 and
A3: u9.3 <> 0 by Def5;
are_Prop u,u9 by A1,A2,ANPROJ_1:22;
then consider a be Real such that
A4: a <> 0 and
A5: u = a * u9 by ANPROJ_1:1;
assume u.3 = 0;
then a * u9.3 = 0 by A5,RVSUM_1:44;
hence thesis by A3,A4;
end;
definition
let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
func normalize_proj3(P) -> non zero Element of TOP-REAL 3 means
:Def6:
Dir it = P & it.3 = 1;
existence
proof
consider u be non zero Element of TOP-REAL 3 such that
A1: P = Dir u and
A2: u.3 <> 0 by Def5;
reconsider v = |[u`1/u.3, u`2/u.3,1]| as non zero Element of TOP-REAL 3;
take v;
u.3 * v = |[u.3 * (u`1/u.3), u.3 * (u`2/u.3),u.3*1]| by EUCLID_5:8
.= |[u`1, u.3 * (u`2/u.3), u.3 ]| by XCMPLX_1:87,A2
.= |[u`1, u`2, u`3]| by A2,XCMPLX_1:87
.= u by EUCLID_5:3;
then are_Prop u,v by A2,ANPROJ_1:1;
hence thesis by A1,ANPROJ_1:22;
end;
uniqueness
proof
let u,v be non zero Element of TOP-REAL 3 such that
A4: P = Dir u & u.3 = 1 and
A5: P = Dir v & v.3 = 1;
are_Prop u,v by A4,A5,ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A6: u = a * v by ANPROJ_1:1;
A7: 1 = a * v.3 by A4,A6,RVSUM_1:44
.= a by A5;
a * v = |[a * v`1, a * v`2, a * v`3]| by EUCLID_5:7
.= v by A7,EUCLID_5:3;
hence thesis by A6;
end;
end;
theorem Th17:
for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st P = Dir u holds
normalize_proj3 P = |[u.1/u.3,u.2/u.3,1]|
proof
let P be non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
let u9 be non zero Element of TOP-REAL 3;
assume P = Dir u9;
then Dir u9 = Dir normalize_proj3 P by Def6;
then are_Prop u9,normalize_proj3 P by ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A1: normalize_proj3 P = a * u9 by ANPROJ_1:1;
A2: normalize_proj3 P = |[a * u9`1,a * u9`2,a * u9`3 ]| by A1,EUCLID_5:7;
A3: 1 = (normalize_proj3 P)`3 by Def6
.= a * u9`3 by A2;
then
A4: u9`3 = 1 / a & a = 1 / u9`3 by XCMPLX_1:73;
normalize_proj3 P = |[ u9`1 / u9`3,(1 / u9`3) * u9`2,1]|
by A1,A3,A4,EUCLID_5:7
.= |[ u9.1 / u9.3,u9.2/u9.3,1]|;
hence thesis;
end;
theorem
for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
for Q being Point of ProjectiveSpace TOP-REAL 3 st
Q = Dir normalize_proj3(P) holds Q is non zero_proj3 by Def6;
registration
cluster non zero_proj1 non zero_proj2 for Point of
ProjectiveSpace TOP-REAL 3;
existence
proof
reconsider u = |[1,1,0]| as non zero Element of TOP-REAL 3;
reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
take P;
reconsider un = u as Element of REAL 3 by EUCLID:22;
u.1 <> 0 & u.2 <> 0;
hence thesis;
end;
end;
registration
cluster non zero_proj1 non zero_proj3 for Point of
ProjectiveSpace TOP-REAL 3;
existence
proof
reconsider u = |[1,0,1]| as non zero Element of TOP-REAL 3;
reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
take P;
reconsider un = u as Element of REAL 3 by EUCLID:22;
u.1 <> 0 & u.3 <> 0;
hence thesis;
end;
end;
registration
cluster non zero_proj2 non zero_proj3 for Point of
ProjectiveSpace TOP-REAL 3;
existence
proof
reconsider u = |[0,1,1]| as non zero Element of TOP-REAL 3;
reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
take P;
reconsider un = u as Element of REAL 3 by EUCLID:22;
u.2 <> 0 & u.3 <> 0;
hence thesis;
end;
end;
registration
cluster non zero_proj1 non zero_proj2 non zero_proj3 for Point of
ProjectiveSpace TOP-REAL 3;
existence
proof
reconsider u = |[1,1,1]| as non zero Element of TOP-REAL 3;
reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
take P;
reconsider un = u as Element of REAL 3 by EUCLID:22;
u.1 <> 0 & u.2 <> 0 & u.3 <> 0;
hence thesis;
end;
end;
definition
let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
func dir1a(P) -> non zero Element of TOP-REAL 3 equals
|[- (normalize_proj1(P)).2,1,0]|;
coherence;
end;
definition
let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
func Pdir1a P -> Point of ProjectiveSpace TOP-REAL 3 equals
Dir (dir1a P);
coherence by ANPROJ_1:26;
end;
definition
let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
func dir1b(P) -> non zero Element of TOP-REAL 3 equals
|[- (normalize_proj1(P)).3,0,1]|;
coherence;
end;
definition
let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
func Pdir1b P -> Point of ProjectiveSpace TOP-REAL 3 equals
Dir (dir1b P);
coherence by ANPROJ_1:26;
end;
theorem
for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3 holds
dir1a(P) <> dir1b(P) by FINSEQ_1:78;
theorem Th20:
for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3 holds
Dir dir1a(P) <> Dir dir1b(P)
proof
let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
assume Dir dir1a(P) = Dir dir1b(P);
then are_Prop dir1a(P),dir1b(P) by ANPROJ_1:22;
then consider a be Real such that
A1: a <> 0 and
A2: dir1a(P) = a * dir1b(P) by ANPROJ_1:1;
0 = (dir1a(P))`3
.= a * (dir1b(P))`3 by A2,RVSUM_1:44
.= a * 1;
hence contradiction by A1;
end;
theorem Th21:
for P being non zero_proj1 Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3
for v being Element of TOP-REAL 3 st u = normalize_proj1 P holds
|{ dir1a P,dir1b P,v }| = |(u,v)|
proof
let P be non zero_proj1 Element of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
let v be Element of TOP-REAL 3;
assume u = normalize_proj1 P;
then
A1: u.1 = 1 & P = Dir u by Def2;
then normalize_proj1 P = |[1, u.2/u.1,u.3/u.1]| by Th11;
then (normalize_proj1(P))`2 = u.2/u.1 & (normalize_proj1(P))`3 = u.3/u.1;
then |{ dir1a P,dir1b P,v }| = |{ |[ -u.2/u.1, 1 , 0 ]|,
|[ -u.3/u.1, 0 , 1 ]|,
|[ v`1 , v`2, v`3 ]| }|
.= v`1 - (-u.2/u.1) * v`2 - v`3 * (-u.3/u.1) by Th2
.= (1/u.1) * (u`1 * v`1 + u`2 * v`2 + v`3 * u`3) by A1
.= (1/u.1) * |(u,v)| by EUCLID_5:29;
hence thesis by A1;
end;
theorem
for P being non zero_proj1 Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st u = normalize_proj1 P holds
|{ dir1a P,dir1b P,normalize_proj1 P }| = 1 + u.2 * u.2 + u.3 * u.3
proof
let P be non zero_proj1 Element of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
assume
A1: u = normalize_proj1 P;
then
A2: u.1 = 1 by Def2;
reconsider un = u as Element of REAL 3 by EUCLID:22;
thus |{ dir1a P,dir1b P,normalize_proj1 P }| = |(un,un)| by A1,Th21
.= u.1 * u.1 + u.2 * u.2 + u.3 * u.3 by EUCLID_8:63
.= 1 + u.2 * u.2 + u.3 * u.3 by A2;
end;
definition
let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
func dir2a(P) -> non zero Element of TOP-REAL 3 equals
|[1, - (normalize_proj2(P)).1,0]|;
coherence;
end;
definition
let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
func Pdir2a P -> Point of ProjectiveSpace TOP-REAL 3 equals
Dir (dir2a P);
coherence by ANPROJ_1:26;
end;
definition
let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
func dir2b(P) -> non zero Element of TOP-REAL 3 equals
|[0, - (normalize_proj2(P)).3,1]|;
coherence;
end;
definition
let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
func Pdir2b P -> Point of ProjectiveSpace TOP-REAL 3 equals
Dir (dir2b P);
coherence by ANPROJ_1:26;
end;
theorem
for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3 holds
dir2a(P) <> dir2b(P) by FINSEQ_1:78;
theorem Th24:
for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3 holds
Dir dir2a(P) <> Dir dir2b(P)
proof
let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
assume Dir dir2a(P) = Dir dir2b(P);
then are_Prop dir2a(P),dir2b(P) by ANPROJ_1:22;
then consider a be Real such that
A1: a <> 0 and
A2: dir2a(P) = a * dir2b(P) by ANPROJ_1:1;
0 = (dir2a(P))`3
.= a * (dir2b(P))`3 by A2,RVSUM_1:44
.= a * 1;
hence contradiction by A1;
end;
theorem Th25:
for P being non zero_proj2 Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3
for v being Element of TOP-REAL 3 st u = normalize_proj2 P holds
|{ dir2a P,dir2b P,v }| = - |(u,v)|
proof
let P be non zero_proj2 Element of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
let v be Element of TOP-REAL 3;
assume u = normalize_proj2 P;
then
A1: u.2 = 1 & P = Dir u by Def4;
then normalize_proj2 P = |[u.1/u.2,1,u.3/u.2]| by Th14;
then (normalize_proj2(P))`1 = u.1/u.2 & (normalize_proj2(P))`3 = u.3/u.2;
then |{ dir2a P,dir2b P,v }| = |{ |[ 1, -u.1/u.2, 0 ]|,
|[ 0, -u.3/u.2, 1 ]|,
|[ v`1, v`2, v`3 ]| }|
.= (-u.3/u.2) * v`3 + (-u.1/u.2) * v`1 - v`2 by Th3
.= -(1/u.2) * (u`1 * v`1 + u`2 * v`2 + u`3 * v`3) by A1
.= -(1/u.2) * |(u,v)| by EUCLID_5:29;
hence thesis by A1;
end;
theorem
for P being non zero_proj2 Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st u = normalize_proj2 P holds
|{ dir2a P,dir2b P,normalize_proj2 P }| = - (u.1 * u.1 + 1 + u.3 * u.3)
proof
let P be non zero_proj2 Element of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
assume
A1: u = normalize_proj2 P;
then
A2: u.2 = 1 by Def4;
reconsider un = u as Element of REAL 3 by EUCLID:22;
thus |{ dir2a P,dir2b P,normalize_proj2 P }| = - |(un,un)| by A1,Th25
.= - (u.1 * u.1 + u.2 * u.2 + u.3 * u.3) by EUCLID_8:63
.= - (u.1 * u.1 + 1 + u.3 * u.3) by A2;
end;
definition
let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
func dir3a(P) -> non zero Element of TOP-REAL 3 equals
|[1,0,- (normalize_proj3(P)).1]|;
coherence;
end;
definition
let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
func Pdir3a P -> Point of ProjectiveSpace TOP-REAL 3 equals
Dir (dir3a P);
coherence by ANPROJ_1:26;
end;
definition
let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
func dir3b(P) -> non zero Element of TOP-REAL 3 equals
|[0,1,- (normalize_proj3(P)).2]|;
coherence;
end;
definition
let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
func Pdir3b P -> Point of ProjectiveSpace TOP-REAL 3 equals
Dir (dir3b P);
coherence by ANPROJ_1:26;
end;
theorem
for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3 holds
dir3a(P) <> dir3b(P) by FINSEQ_1:78;
theorem Th28:
for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3 holds
Dir dir3a(P) <> Dir dir3b(P)
proof
let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
assume Dir dir3a(P) = Dir dir3b(P);
then are_Prop dir3a(P),dir3b(P) by ANPROJ_1:22;
then consider a be Real such that
A1: a <> 0 and
A2: dir3a(P) = a * dir3b(P) by ANPROJ_1:1;
0 = (dir3a(P))`2
.= a * (dir3b(P))`2 by A2,RVSUM_1:44
.= a * 1;
hence contradiction by A1;
end;
theorem Th29:
for P being non zero_proj3 Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3
for v being Element of TOP-REAL 3 st u = normalize_proj3 P holds
|{ dir3a P,dir3b P,v }| = |(u,v)|
proof
let P be non zero_proj3 Element of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
let v be Element of TOP-REAL 3;
assume u = normalize_proj3 P;
then
A1: u.3 = 1 & P = Dir u by Def6;
then normalize_proj3 P = |[u.1/u.3, u.2/u.3, 1]| by Th17;
then (normalize_proj3(P))`1 = u.1/u.3 & (normalize_proj3(P))`2 = u.2/u.3;
then |{ dir3a P,dir3b P,v }| = |{ |[ 1, 0, -u.1/u.3 ]|,
|[ 0, 1, -u.2/u.3 ]|,
|[ v`1, v`2, v`3 ]| }|
.= v`3 - v`1 * (-u.1/u.3) - v`2 * (-u.2/u.3) by Th4
.= u`1 * v`1 + u`2 * v`2 + u`3 * v`3 by A1
.= |(u,v)| by EUCLID_5:29;
hence thesis;
end;
theorem
for P being non zero_proj3 Element of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st u = normalize_proj3 P holds
|{ dir3a P,dir3b P,normalize_proj3 P }| = u.1 * u.1 + u.2 * u.2 + 1
proof
let P be non zero_proj3 Element of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
assume
A1: u = normalize_proj3 P;
then
A2: u.3 = 1 by Def6;
reconsider un = u as Element of REAL 3 by EUCLID:22;
thus |{ dir3a P,dir3b P,normalize_proj3 P }| = |(un,un)| by A1,Th29
.= u.1 * u.1 + u.2 * u.2 + u.3 * u.3 by EUCLID_8:63
.= u.1 * u.1 + u.2 * u.2 + 1 by A2;
end;
definition
let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
func dual1 P -> Element of ProjectiveLines real_projective_plane equals
Line(Pdir1a P,Pdir1b P);
correctness
proof
reconsider P1 = Pdir1a P, P2 = Pdir1b P as Point of real_projective_plane;
reconsider L = Line(P1,P2) as LINE of real_projective_plane
by Th20,COLLSP:def 7;
L in {B where B is Subset of real_projective_plane:
B is LINE of real_projective_plane};
hence thesis;
end;
end;
definition
let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
func dual2 P -> Element of ProjectiveLines real_projective_plane equals
Line(Pdir2a P,Pdir2b P);
correctness
proof
reconsider P1 = Pdir2a P, P2 = Pdir2b P as Point of real_projective_plane;
reconsider L = Line(P1,P2) as LINE of real_projective_plane
by Th24,COLLSP:def 7;
L in {B where B is Subset of real_projective_plane:
B is LINE of real_projective_plane};
hence thesis;
end;
end;
definition
let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
func dual3 P -> Element of ProjectiveLines real_projective_plane equals
Line(Pdir3a P,Pdir3b P);
correctness
proof
reconsider P1 = Pdir3a P, P2 = Pdir3b P as Point of real_projective_plane;
reconsider L = Line(P1,P2) as LINE of real_projective_plane
by Th28,COLLSP:def 7;
L in {B where B is Subset of real_projective_plane:
B is LINE of real_projective_plane};
hence thesis;
end;
end;
theorem
for P being non zero_proj1 non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st P = Dir u holds
normalize_proj1 P = |[1, u.2/u.1, u.3/u.1]| &
normalize_proj2 P = |[u.1/u.2, 1, u.3/u.2]| by Th11,Th14;
theorem
for P being non zero_proj1 non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
for u being non zero Element of TOP-REAL 3 st P = Dir u holds
normalize_proj1 P = u.2/u.1 * normalize_proj2 P &
normalize_proj2 P = u.1/u.2 * normalize_proj1 P
proof
let P be non zero_proj1 non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
let u be non zero Element of TOP-REAL 3;
assume
A1: P = Dir u;
set r = u.1 / u.2;
A2: u.1 <> 0 & u.2 <> 0 by A1,Th10,Th13;
A3: (u.1/u.2) * (u.2/u.1) = r * (1 / r) by XCMPLX_1:57
.= 1 by A2,XCMPLX_1:106;
Dir normalize_proj1 P = P & Dir normalize_proj2 P = P by Def2,Def4;
then are_Prop normalize_proj1 P,normalize_proj2 P by ANPROJ_1:22;
then consider a be Real such that
a <> 0 and
A4: normalize_proj1 P = a * normalize_proj2 P by ANPROJ_1:1;
normalize_proj1 P = |[1, u.2/u.1, u.3/u.1]| &
normalize_proj2 P = |[u.1/u.2, 1, u.3/u.2]| by A1,Th11,Th14;
then
A5: |[1, u.2/u.1, u.3/u.1]| = |[ a * (u.1 / u.2),a*1,a * (u.3/u.2)]|
by A4,EUCLID_5:8;
hence normalize_proj1 P = (u.2/u.1) * normalize_proj2 P by A4,FINSEQ_1:78;
(u.1/u.2) * normalize_proj1 P
= (u.1/u.2) * ((u.2/u.1) * normalize_proj2 P) by A4,A5,FINSEQ_1:78
.= ((u.1/u.2) * (u.2/u.1)) * normalize_proj2 P by RVSUM_1:49
.= normalize_proj2 P by A3,RVSUM_1:52;
hence normalize_proj2 P = (u.1/u.2) * normalize_proj1 P;
end;
theorem Th33:
for P being non zero_proj1 non zero_proj2 Point of ProjectiveSpace
TOP-REAL 3 holds dual1 P = dual2 P
proof
let P be non zero_proj1 non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
consider u be Element of TOP-REAL 3 such that
A1: u is not zero and
A2: P = Dir u by ANPROJ_1:26;
reconsider u as non zero Element of TOP-REAL 3 by A1;
A3: normalize_proj1 P = |[1, u.2/u.1,u.3/u.1]| &
normalize_proj2 P = |[u.1/u.2,1,u.3/u.2]| by A2,Th11,Th14;
now
now
let x be object;
assume x in Line(Pdir1a P,Pdir1b P);
then consider P9 be Point of ProjectiveSpace TOP-REAL 3 such that
A4: x = P9 and
A5: Pdir1a P,Pdir1b P,P9 are_collinear;
consider u9 be Element of TOP-REAL 3 such that
A6: u9 is non zero and
A7: P9 = Dir u9 by ANPROJ_1:26;
set a2 = - (normalize_proj1(P)).2,
a3 = - (normalize_proj1(P)).3,
b1 = u9`1, b2 = u9`2, b3 = u9`3;
A8: a2 = - (normalize_proj1(P))`2
.= - u.2/u.1 by A3;
A9: a3 = - (normalize_proj1(P))`3
.= - u.3/u.1 by A3;
0 = |{ dir1a P,dir1b P,u9 }| by A5,A6,A7,BKMODEL1:1
.= |{ |[a2, 1 , 0]| ,
|[a3, 0 , 1]|,
|[b1, b2, b3]| }|
.= b1 - a2 * b2 - a3 * b3 by Th2
.= b1 + u.2/u.1 * b2 + u.3/u.1 * b3 by A8,A9;
then
A10: 0 = u.1 * (b1 + u.2/u.1 * b2 + u.3/u.1 * b3)
.= u.1 * b1 + u.1 * (u.2 / u.1) * b2 + u.1 * (u.3/u.1) * b3
.= u.1 * b1 + u.2 * b2 + u.1 * (u.3/u.1) * b3
by A2,Th10,XCMPLX_1:87
.= u.1 * b1 + u.2 * b2 + u.3 * b3 by A2,Th10,XCMPLX_1:87;
set c2 = - (normalize_proj2(P)).1,
c3 = - (normalize_proj2(P)).3;
A11: c2 = - (normalize_proj2(P))`1
.= - u.1/u.2 by A3;
A12: c3 = - (normalize_proj2(P))`3
.= - u.3/u.2 by A3;
|{ |[1, c2, 0]|,
|[0, c3, 1]|,
|[u9`1,u9`2,u9`3]| }| = (- u.1/u.2) * b1 + (-u.3/u.2) * b3 - b2
by A11,A12,Th3;
then |{dir2a P,dir2b P,u9}|
= (- u.1/u.2) * b1 + (-u.3/u.2) * b3 + (-1) * b2
.= (- u.1/u.2) * b1 + (-u.3/u.2) * b3 + (-u.2/u.2) * b2
by XCMPLX_1:60,A2,Th13
.= (u.1/(-u.2)) * b1 + (-u.3/u.2) * b3 + (-u.2/u.2) * b2
by XCMPLX_1:188
.= (u.1/(-u.2)) * b1 + (u.3/(-u.2)) * b3 + (-u.2/u.2) * b2
by XCMPLX_1:188
.= (u.1/(-u.2)) * b1 + (u.3/(-u.2)) * b3 + (u.2/(-u.2)) * b2
by XCMPLX_1:188
.= (1 / -u.2) * (u.1 * b1 + u.2 * b2 + u.3 * b3)
.= 0 by A10;
then Pdir2a P,Pdir2b P,P9 are_collinear by A6,A7,BKMODEL1:1;
hence x in Line(Pdir2a P,Pdir2b P) by A4;
end;
hence Line(Pdir1a P,Pdir1b P) c= Line(Pdir2a P,Pdir2b P);
now
let x be object;
assume x in Line(Pdir2a P,Pdir2b P);
then consider P9 be Point of ProjectiveSpace TOP-REAL 3 such that
A13: x = P9 and
A14: Pdir2a P,Pdir2b P,P9 are_collinear;
consider u9 be Element of TOP-REAL 3 such that
A15: u9 is non zero and
A16: P9 = Dir u9 by ANPROJ_1:26;
set a2 = - (normalize_proj1(P)).2,
a3 = - (normalize_proj1(P)).3,
b1 = u9`1, b2 = u9`2, b3 = u9`3;
set c2 = - (normalize_proj2(P)).1,
c3 = - (normalize_proj2(P)).3;
A17: a2 = - (normalize_proj1(P))`2
.= - u.2/u.1 by A3;
A18: a3 = - (normalize_proj1(P))`3
.= - u.3/u.1 by A3;
A19: c2 = - (normalize_proj2(P))`1
.= - u.1/u.2 by A3;
A20: c3 = - (normalize_proj2(P))`3
.= - u.3/u.2 by A3;
A21: - u.2 <> 0 by A2,Th13;
A22: 0 = |{ dir2a P,dir2b P,u9 }| by A14,A15,A16,BKMODEL1:1
.= |{ |[1, c2 , 0]| ,
|[0, c3 , 1]|,
|[b1, b2, b3]| }|
.= c3 * b3 + c2 * b1 - b2 by Th3
.= (- u.1/u.2) * b1 + (-u.3/u.2) * b3 + (-1) * b2 by A19,A20
.= (- u.1/u.2) * b1 + (-u.3/u.2) * b3 + (-u.2/u.2) * b2
by XCMPLX_1:60,A2,Th13
.= (u.1/(-u.2)) * b1 + (-u.3/u.2) * b3 + (-u.2/u.2) * b2
by XCMPLX_1:188
.= (u.1/(-u.2)) * b1 + (u.3/(-u.2)) * b3 + (-u.2/u.2) * b2
by XCMPLX_1:188
.= (u.1/(-u.2)) * b1 + (u.3/(-u.2)) * b3 + (u.2/(-u.2)) * b2
by XCMPLX_1:188
.= (1 / -u.2) * (u.1 * b1 + u.2 * b2 + u.3 * b3);
A23: u.1/u.1 = 1 by XCMPLX_1:60,A2,Th10;
|{dir1a P,dir1b P,u9}| = |{ |[a2, 1 , 0]| ,
|[a3, 0 , 1]|,
|[b1, b2, b3]| }|
.= b1 - a2 * b2 - a3 * b3 by Th2
.= (u.1/u.1) * b1 + u.2/u.1 * b2 + u.3/u.1 * b3 by A17,A18,A23
.= (1/u.1) * (u.1 * b1 + u.2 * b2 + u.3 * b3)
.= (1 / u.1) * 0 by A22,A21,XCMPLX_1:6
.= 0;
then Pdir1a P,Pdir1b P,P9 are_collinear by A15,A16,BKMODEL1:1;
hence x in Line(Pdir1a P,Pdir1b P) by A13;
end;
hence Line(Pdir2a P,Pdir2b P) c= Line(Pdir1a P,Pdir1b P);
end;
hence thesis;
end;
theorem Th34:
for P being non zero_proj2 non zero_proj3 Point of ProjectiveSpace
TOP-REAL 3 holds dual2 P = dual3 P
proof
let P be non zero_proj2 non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
consider u be Element of TOP-REAL 3 such that
A1: u is not zero and
A2: P = Dir u by ANPROJ_1:26;
reconsider u as non zero Element of TOP-REAL 3 by A1;
A3: normalize_proj3 P = |[u.1/u.3,u.2/u.3,1]| &
normalize_proj2 P = |[u.1/u.2,1,u.3/u.2]| by A2,Th17,Th14;
now
now
let x be object;
assume x in Line(Pdir2a P,Pdir2b P);
then consider P9 be Point of ProjectiveSpace TOP-REAL 3 such that
A4: x = P9 and
A5: Pdir2a P,Pdir2b P,P9 are_collinear;
consider u9 be Element of TOP-REAL 3 such that
A6: u9 is non zero and
A7: P9 = Dir u9 by ANPROJ_1:26;
set a2 = - (normalize_proj2(P)).1,
a3 = - (normalize_proj2(P)).3,
b1 = u9`1, b2 = u9`2, b3 = u9`3;
A8: a2 = - (normalize_proj2(P))`1
.= - u.1/u.2 by A3;
A9: a3 = - (normalize_proj2(P))`3
.= - u.3/u.2 by A3;
0 = |{ dir2a P,dir2b P,u9 }| by A5,A6,A7,BKMODEL1:1
.= |{ |[1, a2, 0]| ,
|[0, a3, 1]|,
|[b1, b2, b3]| }|
.= a2 * b1 + a3 * b3 - b2 by Th3
.= -(u.1/u.2 * b1 + b2 + u.3/u.2 * b3) by A8,A9;
then
A10: 0 = u.2 * (u.1/u.2 *b1 + b2 + u.3/u.2 * b3)
.= u.2 * b2 + u.2 * (u.1 / u.2) * b1 + u.2 * (u.3/u.2) * b3
.= u.2 * b2 + u.1 * b1 + u.2 * (u.3/u.2) * b3
by A2,Th13,XCMPLX_1:87
.= u.2 * b2 + u.1 * b1 + u.3 * b3 by A2,Th13,XCMPLX_1:87;
set c2 = - (normalize_proj3(P)).1,
c3 = - (normalize_proj3(P)).2;
A11: c2 = - (normalize_proj3(P))`1
.= - u.1/u.3 by A3;
A12: c3 = - (normalize_proj3(P))`2
.= - u.2/u.3 by A3;
A13: u.3 / u.3 = 1 by A2,Th16,XCMPLX_1:60;
|{ |[1, 0,c2]|,
|[0, 1,c3]|,
|[u9`1,u9`2,u9`3]| }| = b3 - b1 * (-u.1/u.3) - b2 * (-u.2/u.3)
by A11,A12,Th4
.= (u.1/u.3) * b1 + (u.2/u.3) * b2 + b3;
then |{dir3a P,dir3b P,u9}|
= (u.1 * (1/u.3)) * b1 + (u.2/(u.3)) * b2 + (u.3/u.3) * b3
by A13
.= (1 /u.3) * (u.1 * b1 + u.2 * b2 + u.3 * b3)
.= 0 by A10;
then Pdir3a P,Pdir3b P,P9 are_collinear by A6,A7,BKMODEL1:1;
hence x in Line(Pdir3a P,Pdir3b P) by A4;
end;
hence Line(Pdir2a P,Pdir2b P) c= Line(Pdir3a P,Pdir3b P);
now
let x be object;
assume x in Line(Pdir3a P,Pdir3b P);
then consider P9 be Point of ProjectiveSpace TOP-REAL 3 such that
A14: x = P9 and
A15: Pdir3a P,Pdir3b P,P9 are_collinear;
consider u9 be Element of TOP-REAL 3 such that
A16: u9 is non zero and
A17: P9 = Dir u9 by ANPROJ_1:26;
set a2 = - (normalize_proj3(P)).1,
a3 = - (normalize_proj3(P)).2,
b1 = u9`1, b2 = u9`2, b3 = u9`3;
set c2 = - (normalize_proj2(P)).1,
c3 = - (normalize_proj2(P)).3;
A18: a2 = - (normalize_proj3(P))`1
.= - u.1/u.3 by A3;
A19: a3 = - (normalize_proj3(P))`2
.= - u.2/u.3 by A3;
A20: c2 = - (normalize_proj2(P))`1
.= - u.1/u.2 by A3;
A21: c3 = - (normalize_proj2(P))`3
.= - u.3/u.2 by A3;
A22: 0 = |{ dir3a P,dir3b P,u9 }| by A15,A16,A17,BKMODEL1:1
.= |{ |[1, 0, a2]| ,
|[0, 1, a3]|,
|[b1, b2, b3]| }|
.= b3 - a2 * b1 - a3 * b2 by Th4
.= (u.1/u.3) * b1 + (u.2/u.3) * b2 + 1 * b3 by A18,A19
.= (u.1/u.3) * b1 + (u.2/u.3) * b2 + (u.3/u.3) * b3
by XCMPLX_1:60,A2,Th16
.= (1 /u.3) * (u.1 * b1 + u.2 * b2 + u.3 * b3);
A23: u.3 <> 0 by A2,Th16;
|{dir2a P,dir2b P,u9}| = |{ |[1 ,c2, 0]| ,
|[0 ,c3, 1]|,
|[b1, b2, b3]| }|
.= c3 * b3 + c2 * b1 - b2 by Th3
.= (-u.1/u.2) * b1 + (-1) * b2 + (-u.3/u.2) * b3 by A20,A21
.= (-u.1/u.2) * b1 + (-u.2/u.2) * b2 + (-u.3/u.2) * b3
by XCMPLX_1:60,A2,Th13
.= (u.1/-u.2) * b1 + (-u.2/u.2) * b2 + (-u.3/u.2) * b3
by XCMPLX_1:188
.= (u.1/-u.2) * b1 + (u.2/-u.2) * b2 + (-u.3/u.2) * b3
by XCMPLX_1:188
.= (u.1/-u.2) * b1 + (u.2/-u.2) * b2 + (u.3/-u.2) * b3
by XCMPLX_1:188
.= (1/-u.2) * (u.1 * b1 + u.2 * b2 + u.3 * b3)
.= (1/-u.2) * 0 by A23,XCMPLX_1:6,A22
.= 0;
then Pdir2a P,Pdir2b P,P9 are_collinear by A16,A17,BKMODEL1:1;
hence x in Line(Pdir2a P,Pdir2b P) by A14;
end;
hence Line(Pdir3a P,Pdir3b P) c= Line(Pdir2a P,Pdir2b P);
end;
hence thesis;
end;
theorem Th35:
for P being non zero_proj1 non zero_proj3 Point of ProjectiveSpace
TOP-REAL 3 holds dual1 P = dual3 P
proof
let P be non zero_proj1 non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
consider u be Element of TOP-REAL 3 such that
A1: u is not zero and
A2: P = Dir u by ANPROJ_1:26;
reconsider u as non zero Element of TOP-REAL 3 by A1;
A3: normalize_proj1 P = |[1, u.2/u.1,u.3/u.1]| &
normalize_proj3 P = |[u.1/u.3,u.2/u.3,1]| by A2,Th11,Th17;
now
now
let x be object;
assume x in Line(Pdir1a P,Pdir1b P);
then consider P9 be Point of ProjectiveSpace TOP-REAL 3 such that
A4: x = P9 and
A5: Pdir1a P,Pdir1b P,P9 are_collinear;
consider u9 be Element of TOP-REAL 3 such that
A6: u9 is non zero and
A7: P9 = Dir u9 by ANPROJ_1:26;
set a2 = - (normalize_proj1(P)).2,
a3 = - (normalize_proj1(P)).3,
b1 = u9`1, b2 = u9`2, b3 = u9`3;
A8: a2 = - (normalize_proj1(P))`2
.= - u.2/u.1 by A3;
A9: a3 = - (normalize_proj1(P))`3
.= - u.3/u.1 by A3;
0 = |{ dir1a P,dir1b P,u9 }| by A5,A6,A7,BKMODEL1:1
.= |{ |[a2, 1 , 0]| ,
|[a3, 0 , 1]|,
|[b1, b2, b3]| }|
.= b1 - a2 * b2 - a3 * b3 by Th2
.= b1 + u.2/u.1 * b2 + u.3/u.1 * b3 by A8,A9;
then
A10: 0 = u.1 * (b1 + u.2/u.1 * b2 + u.3/u.1 * b3)
.= u.1 * b1 + u.1 * (u.2 / u.1) * b2 + u.1 * (u.3/u.1) * b3
.= u.1 * b1 + u.2 * b2 + u.1 * (u.3/u.1) * b3
by A2,Th10,XCMPLX_1:87
.= u.1 * b1 + u.2 * b2 + u.3 * b3 by A2,Th10,XCMPLX_1:87;
set c2 = - (normalize_proj3(P)).1,
c3 = - (normalize_proj3(P)).2;
A11: c2 = - (normalize_proj3(P))`1
.= - u.1/u.3 by A3;
A12: c3 = - (normalize_proj3(P))`2
.= - u.2/u.3 by A3;
|{ |[1, 0, c2 ]|,
|[0, 1, c3]|,
|[u9`1,u9`2,u9`3]| }| = b3 - c2 * b1 - c3 * b2 by Th4;
then |{dir3a P,dir3b P,u9}|
= (u.1/u.3) * b1 + (u.2/u.3) * b2 + 1 * b3 by A11,A12
.= (u.1/u.3) * b1 + (u.2/u.3) * b2 + (u.3/u.3) * b3
by XCMPLX_1:60,A2,Th16
.= (1 / u.3) * (u.1 * b1 + u.2 * b2 + u.3 * b3)
.= 0 by A10;
then Pdir3a P,Pdir3b P,P9 are_collinear by A6,A7,BKMODEL1:1;
hence x in Line(Pdir3a P,Pdir3b P) by A4;
end;
hence Line(Pdir1a P,Pdir1b P) c= Line(Pdir3a P,Pdir3b P);
now
let x be object;
assume x in Line(Pdir3a P,Pdir3b P);
then consider P9 be Point of ProjectiveSpace TOP-REAL 3 such that
A13: x = P9 and
A14: Pdir3a P,Pdir3b P,P9 are_collinear;
consider u9 be Element of TOP-REAL 3 such that
A15: u9 is non zero and
A16: P9 = Dir u9 by ANPROJ_1:26;
set a2 = - (normalize_proj1(P)).2,
a3 = - (normalize_proj1(P)).3,
b1 = u9`1, b2 = u9`2, b3 = u9`3;
set c2 = - (normalize_proj3(P)).1,
c3 = - (normalize_proj3(P)).2;
A17: a2 = - (normalize_proj1(P))`2
.= - u.2/u.1 by A3;
A18: a3 = - (normalize_proj1(P))`3
.= - u.3/u.1 by A3;
A19: c2 = - (normalize_proj3(P))`1
.= - u.1/u.3 by A3;
A20: c3 = - (normalize_proj3(P))`2
.= - u.2/u.3 by A3;
A21: 0 = |{ dir3a P,dir3b P,u9 }| by A14,A15,A16,BKMODEL1:1
.= |{ |[1, 0,c2]| ,
|[0, 1,c3]|,
|[b1, b2, b3]| }|
.= b3 - c2 * b1 - c3 * b2 by Th4
.= (u.1/u.3) * b1 + (u.2/u.3) * b2 + 1 * b3 by A19,A20
.= (u.1/u.3) * b1 + (u.2/u.3) * b2 + (u.3/u.3) * b3
by XCMPLX_1:60,A2,Th16
.= (1 / u.3) * (u.1 * b1 + u.2 * b2 + u.3 * b3);
A22: u.3 <> 0 by A2,Th16;
A23: u.1/u.1 = 1 by XCMPLX_1:60,A2,Th10;
|{dir1a P,dir1b P,u9}| = |{ |[a2, 1 , 0]| ,
|[a3, 0 , 1]|,
|[b1, b2, b3]| }|
.= b1 - a2 * b2 - a3 * b3 by Th2
.= (u.1/u.1) * b1 + u.2/u.1 * b2 + u.3/u.1 * b3 by A17,A18,A23
.= (1/u.1) * (u.1 * b1 + u.2 * b2 + u.3 * b3)
.= (1 / u.1) * 0 by A22,A21,XCMPLX_1:6
.= 0;
then Pdir1a P,Pdir1b P,P9 are_collinear by A15,A16,BKMODEL1:1;
hence x in Line(Pdir1a P,Pdir1b P) by A13;
end;
hence Line(Pdir3a P,Pdir3b P) c= Line(Pdir1a P,Pdir1b P);
end;
hence thesis;
end;
theorem
for P being non zero_proj1 non zero_proj2 non zero_proj3 Point of
ProjectiveSpace TOP-REAL 3 holds dual1 P = dual2 P & dual1 P = dual3 P &
dual2 P = dual3 P by Th33,Th34,Th35;
theorem Th37:
for P being Element of ProjectiveSpace TOP-REAL 3 holds
P is non zero_proj1 or P is non zero_proj2 or P is non zero_proj3
proof
let P be Element of ProjectiveSpace TOP-REAL 3;
assume that
A1: P is zero_proj1 and
A2: P is zero_proj2 and
A3: P is zero_proj3;
consider u be Element of TOP-REAL 3 such that
A4: u is not zero and
A5: Dir u = P by ANPROJ_1:26;
reconsider u as non zero Element of TOP-REAL 3 by A4;
u`1 = 0 & u`2 = 0 & u`3 = 0 by A1,A2,A3,A5;
hence thesis by EUCLID_5:3,4;
end;
definition
let P being Point of ProjectiveSpace TOP-REAL 3;
func dual P -> Element of ProjectiveLines real_projective_plane means
:Def22:
ex P9 being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3 st P9 = P &
it = dual1 P9
if P is non zero_proj1,
ex P9 being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3 st P9 = P &
it = dual2 P9
if (P is zero_proj1 & P is non zero_proj2),
ex P9 being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3 st P9 = P &
it = dual3 P9
if (P is zero_proj1 & P is zero_proj2 & P is non zero_proj3);
correctness
proof
per cases by Th37;
suppose P is non zero_proj1;
then reconsider P9 = P as
non zero_proj1 Element of ProjectiveSpace TOP-REAL 3;
dual1 P9 is Element of ProjectiveLines real_projective_plane;
hence thesis;
end;
suppose
A1: P is zero_proj1 & P is non zero_proj2;
then reconsider P9 = P as
non zero_proj2 Element of ProjectiveSpace TOP-REAL 3;
dual2 P9 is Element of ProjectiveLines real_projective_plane;
hence thesis by A1;
end;
suppose
A3: P is zero_proj1 & P is zero_proj2 & P is non zero_proj3;
then reconsider P9 = P as
non zero_proj3 Element of ProjectiveSpace TOP-REAL 3;
dual3 P9 is Element of ProjectiveLines real_projective_plane;
hence thesis by A3;
end;
end;
end;
definition
let P being Point of real_projective_plane;
func # P -> Element of ProjectiveSpace TOP-REAL 3 equals P;
coherence;
end;
definition
let P being Point of real_projective_plane;
func dual P -> Element of ProjectiveLines real_projective_plane equals
dual #P;
coherence;
end;
theorem Th38:
for P being Element of real_projective_plane st #P is non zero_proj1 holds
ex P9 being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3 st
P = P9 & dual P = dual1 P9
proof
let P be Element of real_projective_plane;
assume
A1: #P is non zero_proj1;
reconsider P1 = #P as non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
by A1;
per cases;
suppose P1 is non zero_proj2 & P1 is zero_proj3;
hence thesis by Def22;
end;
suppose P1 is zero_proj2 & P1 is non zero_proj3;
hence thesis by Def22;
end;
suppose P1 is zero_proj2 & P1 is zero_proj3;
hence thesis by Def22;
end;
suppose P1 is non zero_proj2 & P1 is non zero_proj3;
hence thesis by Def22;
end;
end;
theorem Th39:
for P being Element of real_projective_plane st #P is non zero_proj2 holds
ex P9 being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3 st
P = P9 & dual P = dual2 P9
proof
let P be Element of real_projective_plane;
assume
A1: #P is non zero_proj2;
reconsider P1 = #P as non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
by A1;
per cases;
suppose
P1 is non zero_proj1 & P1 is zero_proj3;
then reconsider P9 = P1 as
non zero_proj1 non zero_proj2 Element of ProjectiveSpace TOP-REAL 3;
dual P1 = dual1 P9 & dual1 P9 = dual2 P9 by Def22,Th33;
hence thesis;
end;
suppose P1 is zero_proj1 & P1 is non zero_proj3;
hence thesis by Def22;
end;
suppose P1 is zero_proj1 & P1 is zero_proj3;
hence thesis by Def22;
end;
suppose P1 is non zero_proj1 & P1 is non zero_proj3;
then reconsider P9 = P as non zero_proj1 non zero_proj2
non zero_proj3 Element of ProjectiveSpace TOP-REAL 3;
dual P1 = dual1 P9 & dual1 P9 = dual2 P9 by Def22,Th33;
hence thesis;
end;
end;
theorem Th40:
for P being Element of real_projective_plane st #P is non zero_proj3 holds
ex P9 being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3 st
P = P9 & dual P = dual3 P9
proof
let P be Element of real_projective_plane;
assume
A1: #P is non zero_proj3;
reconsider P1 = #P as non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
by A1;
per cases;
suppose
A2: P1 is non zero_proj2 & P1 is zero_proj1;
then reconsider P9 = P as non zero_proj2 non zero_proj3
Element of ProjectiveSpace TOP-REAL 3;
dual P1 = dual2 P9 & dual3 P9 = dual2 P9 by A2,Def22,Th34;
hence thesis;
end;
suppose
P1 is zero_proj2 & P1 is non zero_proj1;
then reconsider P9 = P as non zero_proj1 non zero_proj3
Element of ProjectiveSpace TOP-REAL 3;
dual P1 = dual1 P9 & dual1 P9 = dual3 P9 by Def22,Th35;
hence thesis;
end;
suppose P1 is zero_proj2 & P1 is zero_proj1;
hence thesis by Def22;
end;
suppose P1 is non zero_proj2 & P1 is non zero_proj1;
then reconsider P9 = P as non zero_proj1 non zero_proj2
non zero_proj3 Element of ProjectiveSpace TOP-REAL 3;
dual P1 = dual1 P9 & dual1 P9 = dual3 P9 by Th35,Def22;
hence thesis;
end;
end;
theorem Th41:
for P being non zero_proj1 Element of ProjectiveSpace TOP-REAL 3 holds
not P in Line(Pdir1a P,Pdir1b P)
proof
let P be non zero_proj1 Element of ProjectiveSpace TOP-REAL 3;
assume P in Line(Pdir1a P,Pdir1b P); then
A1: Pdir1a P,Pdir1b P,P are_collinear by COLLSP:11;
reconsider u = normalize_proj1 P as non zero Element of TOP-REAL 3;
A2: P = Dir u by Def2;
|{ dir1a P,dir1b P,u }| = |( u, u )| by Th21;
then |(u, u)| = 0 by A2,A1,BKMODEL1:1;
hence thesis by Th5;
end;
theorem Th42:
for P being non zero_proj2 Element of ProjectiveSpace TOP-REAL 3 holds
not P in Line(Pdir2a P,Pdir2b P)
proof
let P be non zero_proj2 Element of ProjectiveSpace TOP-REAL 3;
assume P in Line(Pdir2a P,Pdir2b P); then
A1: Pdir2a P,Pdir2b P, P are_collinear by COLLSP:11;
reconsider u = normalize_proj2 P as non zero Element of TOP-REAL 3;
A2: P = Dir u by Def4;
|{ dir2a P,dir2b P,u }| = - |( u, u )| by Th25;
then |(u, u)| = 0 by A2,A1,BKMODEL1:1;
hence thesis by Th5;
end;
theorem Th43:
for P being non zero_proj3 Element of ProjectiveSpace TOP-REAL 3 holds
not P in Line(Pdir3a P,Pdir3b P)
proof
let P be non zero_proj3 Element of ProjectiveSpace TOP-REAL 3;
assume P in Line(Pdir3a P,Pdir3b P); then
A1: Pdir3a P,Pdir3b P, P are_collinear by COLLSP:11;
reconsider u = normalize_proj3 P as non zero Element of TOP-REAL 3;
A2: P = Dir u by Def6;
|{ dir3a P,dir3b P,u }| = |( u, u )| by Th29;
then |(u, u)| = 0 by A2,A1,BKMODEL1:1;
hence thesis by Th5;
end;
theorem
for P being Point of real_projective_plane holds not P in dual P
proof
let P be Point of real_projective_plane;
reconsider P9 = P as Element of ProjectiveSpace TOP-REAL 3;
per cases by Th37;
suppose P9 is non zero_proj1;
then reconsider P9 = P as
non zero_proj1 Element of ProjectiveSpace TOP-REAL 3;
#P = P9;
then consider P99 be non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
such that
A1: P = P99 and
A2: dual P = dual1 P99 by Th38;
assume P in dual P;
hence contradiction by A1,A2,Th41;
end;
suppose P9 is non zero_proj2;
then reconsider P9 = P as
non zero_proj2 Element of ProjectiveSpace TOP-REAL 3;
#P = P9;
then consider P99 be non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
such that
A3: P = P99 and
A4: dual P = dual2 P99 by Th39;
assume P in dual P;
hence contradiction by Th42,A3,A4;
end;
suppose P9 is non zero_proj3;
then reconsider P9 = P as
non zero_proj3 Element of ProjectiveSpace TOP-REAL 3;
#P = P9;
then consider P99 be non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
such that
A5: P = P99 and
A6: dual P = dual3 P99 by Th40;
assume P in dual P;
hence contradiction by Th43,A5,A6;
end;
end;
definition
let l being Element of ProjectiveLines real_projective_plane;
func dual l -> Point of real_projective_plane means
:Def25:
ex P,Q being Point of real_projective_plane st P <> Q &
l = Line(P,Q) & it = L2P(P,Q);
existence
proof
consider P,Q be Point of real_projective_plane such that
A1: P <> Q and
A2: l = Line(P,Q) by BKMODEL1:72;
L2P(P,Q) is Point of real_projective_plane;
hence thesis by A1,A2;
end;
uniqueness
proof
let P1,P2 be Point of real_projective_plane such that
A3: ex P,Q be Point of real_projective_plane st P <> Q &
l = Line(P,Q) & P1 = L2P(P,Q) and
A4: ex P,Q being Point of real_projective_plane st P <> Q &
l = Line(P,Q) & P2 = L2P(P,Q);
consider P,Q be Point of real_projective_plane such that
A5: P <> Q and
A6: l = Line(P,Q) and
A7: P1 = L2P(P,Q) by A3;
consider u,v be non zero Element of TOP-REAL 3 such that
A8: P = Dir u and
A9: Q = Dir v and
A10: L2P(P,Q) = Dir(u <X> v) by A5,BKMODEL1:def 5;
consider P9,Q9 be Point of real_projective_plane such that
A11: P9 <> Q9 and
A12: l = Line(P9,Q9) and
A13: P2 = L2P(P9,Q9) by A4;
consider u9,v9 be non zero Element of TOP-REAL 3 such that
A14: P9 = Dir u9 and
A15: Q9 = Dir v9 and
A16: L2P(P9,Q9) = Dir(u9 <X> v9) by A11,BKMODEL1:def 5;
P,Q,P9 are_collinear & P,Q,Q9 are_collinear by A6,A12,COLLSP:10,11;
then |{u,v,u9}| = 0 & |{u,v,v9}| = 0 by A8,A9,A14,A15,BKMODEL1:1;
then
A17: |{u9,u,v}| = 0 & |{v9,u,v}| = 0 by EUCLID_5:33;
A18: now
now
assume u <X> v = 0.TOP-REAL 3;
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A8,A9,A5,ANPROJ_1:22;
end;
hence u <X> v is non zero;
now
assume u9 <X> v9 = 0.TOP-REAL 3;
then are_Prop u9,v9 by ANPROJ_8:51;
hence contradiction by A14,A15,A11,ANPROJ_1:22;
end;
hence u9 <X> v9 is non zero;
end;
then reconsider uv = u <X> v,
u9v9 = u9 <X> v9 as non zero Element of TOP-REAL 3;
not are_Prop u9,v9 by A11,A14,A15,ANPROJ_1:22;
then are_Prop uv,u9 <X> v9 by A17,Th8;
hence thesis by A18,ANPROJ_1:22,A7,A13,A10,A16;
end;
end;
theorem Th45:
for P being Point of real_projective_plane holds dual dual P = P
proof
let P be Point of real_projective_plane;
reconsider P9 = P as Point of ProjectiveSpace TOP-REAL 3;
per cases by Th37;
suppose P9 is non zero_proj1;
then reconsider P9 = P as
non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
reconsider P = P9 as Point of real_projective_plane;
consider P99 be non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
such that
A1: P = P99 & dual P= dual1 P99 by Th38;
reconsider l = Line(Pdir1a P9,Pdir1b P9) as
Element of ProjectiveLines real_projective_plane by A1;
consider P1,P2 be Point of real_projective_plane such that
A2: P1 <> P2 and
A3: l = Line(P1,P2) and
A4: dual l = L2P(P1,P2) by Def25;
A5: Line(P1,P2) = Line(Pdir1a P9,Pdir1b P9) & P1 in Line(P1,P2) &
P2 in Line(P1,P2) by A3,COLLSP:10;
then consider Q1 be Point of ProjectiveSpace TOP-REAL 3 such that
A6: P1 = Q1 and
A7: Pdir1a P9,Pdir1b P9,Q1 are_collinear;
consider Q2 be Point of ProjectiveSpace TOP-REAL 3 such that
A8: P2 = Q2 and
A9: Pdir1a P9,Pdir1b P9,Q2 are_collinear by A5;
consider u,v be non zero Element of TOP-REAL 3 such that
A10: P1 = Dir u and
A11: P2 = Dir v and
A12: L2P(P1,P2) = Dir(u <X> v) by A2,BKMODEL1:def 5;
consider w be Element of TOP-REAL 3 such that
A13: w is not zero and
A14: P9 = Dir w by ANPROJ_1:26;
reconsider w as non zero Element of TOP-REAL 3 by A13;
normalize_proj1 P9 = |[1, w.2/w.1,w.3/w.1]| by A14,Th11;
then (normalize_proj1(P9))`2 = w.2/w.1 &
(normalize_proj1(P9))`3 = w.3/w.1;
then
A15: dir1a P9 <X> dir1b P9
= |[ (1 * 1) - (0 * 0),
(0 * (-w.3/w.1)) - ((-w.2/w.1) * 1),
((-w.2/w.1) * 0) - ((-w.3/w.1) * 1) ]|
.= |[ w`1/w.1, w`2/w.1,w`3/w.1 ]| by A14,Th10,XCMPLX_1:60
.= 1/w.1 * w by EUCLID_5:7;
w.1 <> 0 by A14,Th10;
then reconsider a = 1/w.1 * w as non zero Element of TOP-REAL 3
by ANPROJ_9:3;
now
assume u <X> v = 0.TOP-REAL 3;
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A2,A10,A11,ANPROJ_1:22;
end;
then
A16: u <X> v is non zero;
now
now
thus not are_Prop u,v by A2,A10,A11,ANPROJ_1:22;
thus 0 = |{ dir1a P9,dir1b P9,u }| by A10,A6,A7,BKMODEL1:1
.= |{ u, dir1a P9,dir1b P9 }| by EUCLID_5:34
.= |( a, u )| by A15;
thus 0 = |{ dir1a P9,dir1b P9,v }| by A11,A8,A9,BKMODEL1:1
.= |{ v, dir1a P9,dir1b P9 }| by EUCLID_5:34
.= |( a, v )| by A15;
end;
then are_Prop 1/w.1 * w, u <X> v by Th8;
hence are_Prop w.1 * a,u <X> v by A14,Th10,A16,Th9;
thus w.1 * a = (w.1 * (1/w.1)) * w by RVSUM_1:49
.= 1 * w by A14,Th10,XCMPLX_1:106
.= w by RVSUM_1:52;
end;
hence thesis by A14,A1,A4,A12,A16,ANPROJ_1:22;
end;
suppose P9 is non zero_proj2;
then reconsider P9 = P as
non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
reconsider P = P9 as Point of real_projective_plane;
consider P99 be non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
such that
A17: P = P99 & dual P= dual2 P99 by Th39;
reconsider l = Line(Pdir2a P9,Pdir2b P9) as
Element of ProjectiveLines real_projective_plane by A17;
consider P1,P2 be Point of real_projective_plane such that
A18: P1 <> P2 and
A19: l = Line(P1,P2) and
A20: dual l = L2P(P1,P2) by Def25;
A21: Line(P1,P2) = Line(Pdir2a P9,Pdir2b P9) & P1 in Line(P1,P2) &
P2 in Line(P1,P2) by A19,COLLSP:10;
then consider Q1 be Point of ProjectiveSpace TOP-REAL 3 such that
A22: P1 = Q1 and
A23: Pdir2a P9,Pdir2b P9,Q1 are_collinear;
consider Q2 be Point of ProjectiveSpace TOP-REAL 3 such that
A24: P2 = Q2 and
A25: Pdir2a P9,Pdir2b P9,Q2 are_collinear by A21;
consider u,v be non zero Element of TOP-REAL 3 such that
A26: P1 = Dir u and
A27: P2 = Dir v and
A28: L2P(P1,P2) = Dir(u <X> v) by A18,BKMODEL1:def 5;
consider w be Element of TOP-REAL 3 such that
A29: w is not zero and
A30: P9 = Dir w by ANPROJ_1:26;
reconsider w as non zero Element of TOP-REAL 3 by A29;
normalize_proj2 P9 = |[w.1/w.2, 1, w.3/w.2]| by A30,Th14;
then (normalize_proj2(P9))`1 = w.1/w.2 &
(normalize_proj2(P9))`3 = w.3/w.2;
then
A31: dir2a P9 <X> dir2b P9
= |[ ((-w.1/w.2) * 1) - (0 * (-w.3/w.2)),
(0 * 0) - (1 * 1),
(1 * (-w.3/w.2)) - (0 * (-w.1/w.2)) ]|
.= |[ -w.1/w.2, -w.2/w.2,-w.3/w.2 ]| by A30,Th13,XCMPLX_1:60
.= |[ w.1/(-w.2), -w.2/w.2,-w.3/w.2 ]| by XCMPLX_1:188
.= |[ w.1/(-w.2), w.2/(-w.2),-w.3/w.2 ]| by XCMPLX_1:188
.= |[ w`1/(-w.2), w`2/(-w.2),w`3/(-w.2) ]| by XCMPLX_1:188
.= 1/(-w.2) * w by EUCLID_5:7;
A32: w.2 <> 0 by A30,Th13;
then reconsider a = 1/(-w.2) * w as non zero Element of TOP-REAL 3
by ANPROJ_9:3;
now
assume u <X> v = 0.TOP-REAL 3;
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A18,A26,A27,ANPROJ_1:22;
end;
then
A33: u <X> v is non zero;
now
now
thus not are_Prop u,v by A18,A26,A27,ANPROJ_1:22;
thus 0 = |{ dir2a P9,dir2b P9,u }| by A26,A22,A23,BKMODEL1:1
.= |{ u, dir2a P9,dir2b P9 }| by EUCLID_5:34
.= |( a, u )| by A31;
thus 0 = |{ dir2a P9,dir2b P9,v }| by A27,A24,A25,BKMODEL1:1
.= |{ v, dir2a P9,dir2b P9 }| by EUCLID_5:34
.= |( a, v )| by A31;
end;
then are_Prop 1/(-w.2) * w, u <X> v by Th8;
hence are_Prop (-w.2) * a,u <X> v by A32,A33,Th9;
thus (-w.2) * a = ((-w.2) * (1/(-w.2))) * w by RVSUM_1:49
.= 1 * w by A32,XCMPLX_1:106
.= w by RVSUM_1:52;
end;
hence thesis by A30,A17,A20,A28,A33,ANPROJ_1:22;
end;
suppose P9 is non zero_proj3;
then reconsider P9 = P as
non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
reconsider P = P9 as Point of real_projective_plane;
consider P99 be non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
such that
A34: P = P99 & dual P= dual3 P99 by Th40;
reconsider l = Line(Pdir3a P9,Pdir3b P9) as
Element of ProjectiveLines real_projective_plane by A34;
consider P1,P2 be Point of real_projective_plane such that
A35: P1 <> P2 and
A36: l = Line(P1,P2) and
A37: dual l = L2P(P1,P2) by Def25;
A38: Line(P1,P2) = Line(Pdir3a P9,Pdir3b P9) & P1 in Line(P1,P2) &
P2 in Line(P1,P2) by A36,COLLSP:10;
then consider Q1 be Point of ProjectiveSpace TOP-REAL 3 such that
A39: P1 = Q1 and
A40: Pdir3a P9,Pdir3b P9,Q1 are_collinear;
consider Q2 be Point of ProjectiveSpace TOP-REAL 3 such that
A41: P2 = Q2 and
A42: Pdir3a P9,Pdir3b P9,Q2 are_collinear by A38;
consider u,v be non zero Element of TOP-REAL 3 such that
A43: P1 = Dir u and
A44: P2 = Dir v and
A45: L2P(P1,P2) = Dir(u <X> v) by A35,BKMODEL1:def 5;
consider w be Element of TOP-REAL 3 such that
A46: w is not zero and
A47: P9 = Dir w by ANPROJ_1:26;
reconsider w as non zero Element of TOP-REAL 3 by A46;
normalize_proj3 P9 = |[w.1/w.3, w.2/w.3, 1]| by A47,Th17;
then (normalize_proj3(P9))`1 = w.1/w.3 &
(normalize_proj3(P9))`2 = w.2/w.3;
then
A48: dir3a P9 <X> dir3b P9
= |[ (0 * (-w.2/w.3)) - ((-w.1/w.3) * 1),
((-w.1/w.3) * 0) - (1 * (-w.2/w.3)),
(1 * 1) - (0 * 0) ]|
.= |[ w`1/w.3, w`2/w.3,w`3/w.3 ]| by A47,Th16,XCMPLX_1:60
.= 1/(w.3) * w by EUCLID_5:7;
w.3 <> 0 by A47,Th16;
then reconsider a = 1/(w.3) * w as non zero Element of TOP-REAL 3
by ANPROJ_9:3;
now
assume u <X> v = 0.TOP-REAL 3;
then are_Prop u,v by ANPROJ_8:51;
hence contradiction by A35,A43,A44,ANPROJ_1:22;
end;
then
A49: u <X> v is non zero;
now
now
thus not are_Prop u,v by A35,A43,A44,ANPROJ_1:22;
thus 0 = |{ dir3a P9,dir3b P9,u }| by A43,A39,A40,BKMODEL1:1
.= |{ u, dir3a P9,dir3b P9 }| by EUCLID_5:34
.= |( a, u )| by A48;
thus 0 = |{ dir3a P9,dir3b P9,v }| by A44,A41,A42,BKMODEL1:1
.= |{ v, dir3a P9,dir3b P9 }| by EUCLID_5:34
.= |( a, v )| by A48;
end;
then are_Prop 1/(w.3) * w, u <X> v by Th8;
hence are_Prop (w.3) * a,u <X> v by A47,Th16,A49,Th9;
thus w.3 * a = (w.3 * (1/w.3)) * w by RVSUM_1:49
.= 1 * w by A47,Th16,XCMPLX_1:106
.= w by RVSUM_1:52;
end;
hence thesis by A47,A34,A37,A45,A49,ANPROJ_1:22;
end;
end;
theorem Th46:
for l being Element of ProjectiveLines real_projective_plane holds
dual dual l = l
proof
let l be Element of ProjectiveLines real_projective_plane;
consider P,Q be Point of real_projective_plane such that
A1: P <> Q and
A2: l = Line(P,Q) and
A3: dual l = L2P(P,Q) by Def25;
reconsider P9 = P,Q9 = Q as Point of ProjectiveSpace TOP-REAL 3;
consider u,v be non zero Element of TOP-REAL 3 such that
A4: P = Dir u and
A5: Q = Dir v and
A6: L2P(P,Q) = Dir(u <X> v) by A1,BKMODEL1:def 5;
reconsider l2 = Line(P,Q) as LINE of real_projective_plane
by A1,COLLSP:def 7;
not are_Prop u,v by A1,A4,A5,ANPROJ_1:22;
then u <X> v is non zero by ANPROJ_8:51;
then reconsider uv = u <X> v as non zero Element of TOP-REAL 3;
reconsider R = Dir uv as Point of ProjectiveSpace TOP-REAL 3
by ANPROJ_1:26;
reconsider R9 = R as Element of real_projective_plane;
per cases by Th37;
suppose
A9: R is non zero_proj1;
then reconsider R as non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
#R9 = R;
then consider P99 be non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
such that
A10: R9 = P99 and
A11: dual R9 = dual1 P99 by Th38;
A12: uv.1 / uv.1 = 1 by A9,Th10,XCMPLX_1:60;
normalize_proj1 P99 = |[1, uv.2/uv.1,uv.3/uv.1]| by A10,Th11;
then
A13: (normalize_proj1 P99)`2 = uv.2/uv.1 &
(normalize_proj1 P99)`3 = uv.3/uv.1;
reconsider l1 = Line(Pdir1a P99,Pdir1b P99) as
LINE of real_projective_plane by Th20,COLLSP:def 7;
now
|{ |[- uv.2/uv.1, 1, 0]|,
|[- uv.3/uv.1, 0, 1]|,
|[u`1, u`2,u`3]| }|
= u`1 - (-uv.2/uv.1) * u`2 - u`3 * (-uv.3/uv.1) by Th2
.= (uv.1 / uv.1) * u`1 + (uv.2/uv.1) * u`2 + u`3 * (uv.3/uv.1)
by A12
.= (1/uv.1) * (uv.1 * u`1 + uv.2 * u`2 + uv.3 * u`3)
.= 0;
then|{ dir1a P99,dir1b P99,u }| = 0 by A13;
then Pdir1a P99,Pdir1b P99, P9 are_collinear by A4,BKMODEL1:1;
hence P in l1;
|{ |[- uv.2/uv.1, 1, 0]|,
|[- uv.3/uv.1, 0, 1]|,
|[v`1, v`2,v`3]| }|
= (uv.1 / uv.1) * v`1 - (-uv.2/uv.1) * v`2 - v`3 * (-uv.3/uv.1)
by A12,Th2
.= (1/uv.1) * (uv.1 * v`1 + uv.2 * v`2 + uv.3 * v`3)
.= 0;
then|{ dir1a P99,dir1b P99,v }| = 0 by A13;
then Pdir1a P99,Pdir1b P99, Q9 are_collinear by A5,BKMODEL1:1;
hence Q in l1;
thus P in l2 & Q in l2 by COLLSP:10;
end;
hence thesis by A1,A3,A6,A11,A2,COLLSP:20;
end;
suppose
A14: R is non zero_proj2;
then reconsider R as non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
#R9 = R;
then consider P99 be non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
such that
A15: R9 = P99 and
A16: dual R9 = dual2 P99 by Th39;
A17: uv.2 / uv.2 = 1 by A14,Th13,XCMPLX_1:60;
normalize_proj2 P99 = |[uv.1/uv.2,1,uv.3/uv.2]| by A15,Th14;
then
A18: (normalize_proj2 P99)`1 = uv.1/uv.2 &
(normalize_proj2 P99)`3 = uv.3/uv.2;
reconsider l1 = Line(Pdir2a P99,Pdir2b P99) as
LINE of real_projective_plane by Th24,COLLSP:def 7;
now
|{ |[1 , - uv.1/uv.2, 0]|,
|[0 , - uv.3/uv.2, 1]|,
|[u`1, u`2, u`3]| }|
= (-uv.3/uv.2) * u`3 + (-uv.1/uv.2) * u`1 - u`2 by Th3
.= -((uv.3/uv.2) * u`3 + (uv.1/uv.2) * u`1 + (uv.2/uv.2) * u`2) by A17
.= - ((1 / uv.2) * (uv.1 * u`1 + uv.2 * u`2 + uv.3 * u`3))
.= 0;
then|{ dir2a P99,dir2b P99,u }| = 0 by A18;
then Pdir2a P99,Pdir2b P99, P9 are_collinear by A4,BKMODEL1:1;
hence P in l1;
|{ |[ 1 , - uv.1/uv.2, 0 ]|,
|[ 0 , - uv.3/uv.2, 1 ]|,
|[v`1, v`2, v`3]| }|
= (-uv.3/uv.2) * v`3 + (-uv.1/uv.2) * v`1 - v`2 by Th3
.= -((uv.3/uv.2) * v`3 + (uv.1/uv.2) * v`1 + (uv.2/uv.2) * v`2) by A17
.= - ((1 / uv.2) * (uv.1 * v`1 + uv.2 * v`2 + uv.3 * v`3))
.= 0;
then|{ dir2a P99,dir2b P99,v }| = 0 by A18;
then Pdir2a P99,Pdir2b P99, Q9 are_collinear by A5,BKMODEL1:1;
hence Q in l1;
thus P in l2 & Q in l2 by COLLSP:10;
end;
hence thesis by A3,A6,A16,A2,A1,COLLSP:20;
end;
suppose
A19: R is non zero_proj3;
then reconsider R as non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
#R9 = R;
then consider P99 be non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
such that
A20: R9 = P99 and
A21: dual R9 = dual3 P99 by Th40;
A22: uv.3 / uv.3 = 1 by A19,Th16,XCMPLX_1:60;
normalize_proj3 P99 = |[uv.1/uv.3,uv.2/uv.3,1]| by A20,Th17;
then
A23: (normalize_proj3 P99)`1 = uv.1/uv.3 &
(normalize_proj3 P99)`2 = uv.2/uv.3;
reconsider l1 = Line(Pdir3a P99,Pdir3b P99) as
LINE of real_projective_plane by Th28,COLLSP:def 7;
now
|{ |[1 ,0 , - uv.1/uv.3]|,
|[0 ,1 , - uv.2/uv.3]|,
|[u`1,u`2, u`3 ]| }|
= u`3 - u`1 * (-uv.1/uv.3) - u`2 * (-uv.2/uv.3) by Th4
.= u`1 * (uv.1/uv.3) + u`2 * (uv.2/uv.3) + u`3 * (uv.3 / uv.3) by A22
.= (1 / uv.3) * (uv.1 * u`1 + uv.2 * u`2 + uv.3 * u`3)
.= 0;
then|{ dir3a P99,dir3b P99,u }| = 0 by A23;
then Pdir3a P99,Pdir3b P99, P9 are_collinear by A4,BKMODEL1:1;
hence P in l1;
|{ |[1 ,0 ,- uv.1/uv.3]|,
|[0 ,1 ,- uv.2/uv.3]|,
|[v`1,v`2,v`3]| }|
= v`3 - v`1 * (-uv.1/uv.3) - v`2 * (-uv.2/uv.3) by Th4
.= v`1 * (uv.1/uv.3) + v`2 * (uv.2/uv.3) + v`3 * (uv.3 / uv.3) by A22
.= (1 / uv.3) * (uv.1 * v`1 + uv.2 * v`2 + uv.3 * v`3)
.= 0;
then|{ dir3a P99,dir3b P99,v }| = 0 by A23;
then Pdir3a P99,Pdir3b P99, Q9 are_collinear by A5,BKMODEL1:1;
hence Q in l1;
thus P in l2 & Q in l2 by COLLSP:10;
end;
hence thesis by A3,A6,A21,A2,A1,COLLSP:20;
end;
end;
theorem
for P,Q being Point of real_projective_plane holds
(P <> Q iff dual P <> dual Q)
proof
let P,Q be Point of real_projective_plane;
now
assume
A1: P <> Q;
assume dual P = dual Q;
then P = dual dual Q by Th45;
hence contradiction by A1,Th45;
end;
hence thesis;
end;
theorem Th48:
for l,m being Element of ProjectiveLines real_projective_plane holds
(l <> m iff dual l <> dual m)
proof
let l,m be Element of ProjectiveLines real_projective_plane;
now
assume
A1: l <> m;
assume dual l = dual m;
then l = dual dual m by Th46;
hence contradiction by A1,Th46;
end;
hence thesis;
end;
begin
definition
let l1,l2,l3 being Element of ProjectiveLines real_projective_plane;
pred l1,l2,l3 are_concurrent means
ex P being Point of real_projective_plane st P in l1 & P in l2 & P in l3;
end;
definition
let l being Element of ProjectiveLines real_projective_plane;
func #l -> LINE of IncProjSp_of real_projective_plane equals l;
coherence;
end;
definition
let l being LINE of IncProjSp_of real_projective_plane;
func #l -> Element of ProjectiveLines real_projective_plane equals l;
coherence;
end;
theorem Th49:
for l1,l2,l3 being Element of ProjectiveLines real_projective_plane holds
l1,l2,l3 are_concurrent iff #l1,#l2,#l3 are_concurrent
proof
let l1,l2,l3 be Element of ProjectiveLines real_projective_plane;
now
l1 in {B where B is Subset of real_projective_plane:
B is LINE of real_projective_plane};
hence ex B be Subset of real_projective_plane st l1 = B &
B is LINE of real_projective_plane;
l2 in {B where B is Subset of real_projective_plane:
B is LINE of real_projective_plane};
hence ex B be Subset of real_projective_plane st l2 = B &
B is LINE of real_projective_plane;
l3 in {B where B is Subset of real_projective_plane:
B is LINE of real_projective_plane};
hence ex B be Subset of real_projective_plane st l3 = B &
B is LINE of real_projective_plane;
end;
then reconsider m1 = l1,m2 = l2,m3 = l3 as LINE of real_projective_plane;
reconsider l91 = #l1, l92 = #l2, l93 = #l3 as
LINE of IncProjSp_of real_projective_plane;
hereby
assume l1,l2,l3 are_concurrent;
then consider P be Point of real_projective_plane such that
A1: P in l1 and
A2: P in l2 and
A3: P in l3;
reconsider P as Element of the Points of IncProjSp_of
real_projective_plane;
reconsider P9 = P as POINT of IncProjSp_of real_projective_plane;
P in m1 & P in m2 & P in m3 by A1,A2,A3;
then P9 on l91 & P9 on l92 & P9 on l93 by INCPROJ:5;
hence #l1,#l2,#l3 are_concurrent;
end;
assume #l1,#l2,#l3 are_concurrent;
then consider o be Element of the Points of IncProjSp_of
real_projective_plane
such that
A4: o on #l1 and
A5: o on #l2 and
A6: o on #l3;
reconsider o9 = o as Point of real_projective_plane;
o9 in m1 & o9 in m2 & o9 in m3 by A4,A5,A6,INCPROJ:5;
hence l1,l2,l3 are_concurrent;
end;
theorem
for l1,l2,l3 being LINE of IncProjSp_of real_projective_plane holds
l1,l2,l3 are_concurrent iff #l1,#l2,#l3 are_concurrent
proof
let l1,l2,l3 be LINE of IncProjSp_of real_projective_plane;
reconsider l91 = #l1, l92 = #l2, l93 = #l3 as
Element of ProjectiveLines real_projective_plane;
hereby
assume l1,l2,l3 are_concurrent;
then #l91,#l92,#l93 are_concurrent;
hence #l1,#l2,#l3 are_concurrent by Th49;
end;
assume #l1,#l2,#l3 are_concurrent;
then ##l1,##l2,##l3 are_concurrent by Th49;
hence l1,l2,l3 are_concurrent;
end;
theorem
for P,Q,R being Element of real_projective_plane st P,Q,R are_collinear holds
Q,R,P are_collinear & R,P,Q are_collinear &
P,R,Q are_collinear & R,Q,P are_collinear &
Q,P,R are_collinear by ANPROJ_2:24;
theorem
for l1,l2,l3 being Element of ProjectiveLines real_projective_plane st
l1,l2,l3 are_concurrent holds l2,l1,l3 are_concurrent &
l1,l3,l2 are_concurrent & l3,l2,l1 are_concurrent &
l3,l2,l1 are_concurrent & l2,l3,l1 are_concurrent;
theorem
for P,Q being Point of real_projective_plane
for P9,Q9 being Element of ProjectiveSpace TOP-REAL 3 st
P = P9 & Q = Q9 holds Line(P,Q) = Line(P9,Q9);
theorem Th54:
for P being Point of real_projective_plane
for l being Element of ProjectiveLines real_projective_plane st P in l holds
dual l in dual P
proof
let P be Point of real_projective_plane;
let l be Element of ProjectiveLines real_projective_plane;
assume
A1: P in l;
consider u be Element of TOP-REAL 3 such that
A2: u is not zero and
A3: P = Dir u by ANPROJ_1:26;
reconsider u as non zero Element of TOP-REAL 3 by A2;
reconsider P9 = P as Element of ProjectiveSpace TOP-REAL 3;
reconsider dl = dual l as Point of ProjectiveSpace TOP-REAL 3;
consider Pl,Ql be Point of real_projective_plane such that
A4: Pl <> Ql and
A5: l = Line(Pl,Ql) and
A6: dual l = L2P(Pl,Ql) by Def25;
consider ul,vl be non zero Element of TOP-REAL 3 such that
A7: Pl = Dir ul and
A8: Ql = Dir vl and
A9: L2P(Pl,Ql) = Dir(ul <X> vl) by A4,BKMODEL1:def 5;
reconsider ulvl = ul <X> vl as non zero Element of TOP-REAL 3
by A4,A7,A8,BKMODEL1:78;
consider S be Point of real_projective_plane such that
A10: P = S and
A11: Pl,Ql,S are_collinear by A1,A5;
P,Pl,Ql are_collinear by A10,A11,ANPROJ_2:24;
then
A12: |{u,ul,vl}| = 0 by A3,A7,A8,BKMODEL1:1;
per cases by Th37;
suppose P9 is non zero_proj1;
then reconsider P9 as non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
consider P99 be non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
such that
A13: P9 = P99 and
A14: dual P = dual1 P99 by Th38;
consider S be Point of real_projective_plane such that
A15: P = S and
A16: Pl,Ql,S are_collinear by A1,A5;
P,Pl,Ql are_collinear by A15,A16,ANPROJ_2:24;
then
A17: |{u,ul,vl}| = 0 by A3,A7,A8,BKMODEL1:1;
Dir normalize_proj1 P9 = Dir u by A3,Def2;
then
A18: are_Prop normalize_proj1 P9,u by ANPROJ_1:22;
|{dir1a P9,dir1b P9, ulvl }| = |(normalize_proj1 P9, ulvl)| by Th21
.= 0 by A17,A18,Th7;
then Pdir1a P9,Pdir1b P9, dl are_collinear by A6,A9,BKMODEL1:1;
hence thesis by A13,A14;
end;
suppose P9 is non zero_proj2;
then reconsider P9 as non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
consider P99 be non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
such that
A19: P9 = P99 and
A20: dual P = dual2 P99 by Th39;
Dir normalize_proj2 P9 = Dir u by A3,Def4;
then
A21: are_Prop normalize_proj2 P9,u by ANPROJ_1:22;
|{dir2a P9,dir2b P9, ulvl }| = - |(normalize_proj2 P9, ulvl)| by Th25
.= - 0 by A12,A21,Th7;
then Pdir2a P9,Pdir2b P9, dl are_collinear by A6,A9,BKMODEL1:1;
hence thesis by A19,A20;
end;
suppose P9 is non zero_proj3;
then reconsider P9 as non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
consider P99 be non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
such that
A22: P9 = P99 and
A23: dual P = dual3 P99 by Th40;
Dir normalize_proj3 P9 = Dir u by A3,Def6;
then
A24: are_Prop normalize_proj3 P9,u by ANPROJ_1:22;
|{dir3a P9,dir3b P9, ulvl }| = |(normalize_proj3 P9, ulvl)| by Th29
.= 0 by A12,A24,Th7;
then Pdir3a P9,Pdir3b P9, dl are_collinear by A6,A9,BKMODEL1:1;
hence thesis by A22,A23;
end;
end;
theorem
for P being Point of real_projective_plane
for l being Element of ProjectiveLines real_projective_plane st
dual l in dual P holds P in l
proof
let P be Point of real_projective_plane;
let l be Element of ProjectiveLines real_projective_plane;
assume dual l in dual P;
then dual dual P in dual dual l by Th54;
then P in dual dual l by Th45;
hence thesis by Th46;
end;
theorem Th56:
for P,Q,R being Point of real_projective_plane st P,Q,R are_collinear holds
dual P,dual Q, dual R are_concurrent
proof
let P,Q,R be Point of real_projective_plane;
assume
A1: P,Q,R are_collinear;
per cases;
suppose
A2: Q = R;
reconsider lP = dual P,lQ = dual Q as LINE of real_projective_plane
by INCPROJ:1;
ex x be object st x in lP & x in lQ by BKMODEL1:76,XBOOLE_0:3;
hence thesis by A2;
end;
suppose
A3: Q <> R;
A4: Q,R,P are_collinear by A1,ANPROJ_2:24;
reconsider l = Line(Q,R) as LINE of real_projective_plane
by A3,COLLSP:def 7;
l in {B where B is Subset of real_projective_plane:
B is LINE of real_projective_plane};
then reconsider l = Line(Q,R) as Element of ProjectiveLines
real_projective_plane;
dual l in dual P & dual l in dual Q & dual l in dual R
by A4,COLLSP:11,Th54,COLLSP:10;
hence thesis;
end;
end;
theorem Th57:
for l being Element of ProjectiveLines real_projective_plane
for P,Q,R being Point of real_projective_plane st
P in l & Q in l & R in l holds P,Q,R are_collinear
proof
let l be Element of ProjectiveLines real_projective_plane;
let P,Q,R be Point of real_projective_plane;
assume
A1: P in l & Q in l & R in l;
l is LINE of real_projective_plane by INCPROJ:1;
hence thesis by A1,COLLSP:16;
end;
theorem Th58:
for l1,l2,l3 being Element of ProjectiveLines real_projective_plane st
l1,l2,l3 are_concurrent holds dual l1,dual l2,dual l3 are_collinear
proof
let l1,l2,l3 be Element of ProjectiveLines real_projective_plane;
assume l1,l2,l3 are_concurrent;
then consider P be Point of real_projective_plane such that
A1: P in l1 & P in l2 & P in l3;
reconsider lP = dual P as Element of ProjectiveLines real_projective_plane;
dual l1 in lP & dual l2 in lP & dual l3 in lP by A1,Th54;
hence thesis by Th57;
end;
theorem Th59:
for P,Q,R being Point of real_projective_plane holds
P,Q,R are_collinear iff dual P,dual Q,dual R are_concurrent
proof
let P,Q,R be Point of real_projective_plane;
thus P,Q,R are_collinear implies dual P, dual Q, dual R are_concurrent
by Th56;
assume dual P, dual Q, dual R are_concurrent;
then dual dual P, dual dual Q, dual dual R are_collinear
by Th58;
then P, dual dual Q, dual dual R are_collinear by Th45;
then P, Q, dual dual R are_collinear by Th45;
hence thesis by Th45;
end;
theorem Th60:
for l1,l2,l3 being Element of ProjectiveLines real_projective_plane holds
l1,l2,l3 are_concurrent iff dual l1, dual l2, dual l3 are_collinear
proof
let l1,l2,l3 be Element of ProjectiveLines real_projective_plane;
hereby
assume l1,l2,l3 are_concurrent;
then dual dual l1,l2,l3 are_concurrent by Th46;
then dual dual l1,dual dual l2,l3 are_concurrent by Th46;
then dual dual l1,dual dual l2,dual dual l3 are_concurrent by Th46;
hence dual l1, dual l2, dual l3 are_collinear by Th59;
end;
assume dual l1, dual l2, dual l3 are_collinear;
then dual dual l1, dual dual l2, dual dual l3 are_concurrent by Th59;
then l1, dual dual l2, dual dual l3 are_concurrent by Th46;
then l1, l2, dual dual l3 are_concurrent by Th46;
hence thesis by Th46;
end;
begin :: Some converse theorems
theorem
real_projective_plane is reflexive &
real_projective_plane is transitive &
real_projective_plane is Vebleian &
real_projective_plane is at_least_3rank &
real_projective_plane is Fanoian &
real_projective_plane is Desarguesian &
real_projective_plane is Pappian &
real_projective_plane is 2-dimensional;
::$N Converse reflexive
theorem
for l,m,n being Element of ProjectiveLines real_projective_plane holds
l,m,l are_concurrent & l,l,m are_concurrent & l,m,m are_concurrent
proof
let l1,l2,l3 be Element of ProjectiveLines real_projective_plane;
dual l1,dual l2,dual l1 are_collinear &
dual l1,dual l1,dual l2 are_collinear &
dual l1,dual l2,dual l2 are_collinear by ANPROJ_2:def 7;
then dual dual l1,dual dual l2,dual dual l1 are_concurrent &
dual dual l1,dual dual l1,dual dual l2 are_concurrent &
dual dual l1,dual dual l2,dual dual l2 are_concurrent by Th59;
then l1,dual dual l2,dual dual l1 are_concurrent &
l1,dual dual l1,dual dual l2 are_concurrent &
l1,dual dual l2,dual dual l2 are_concurrent by Th46;
then l1,l2,dual dual l1 are_concurrent &
l1,l1,dual dual l2 are_concurrent &
l1,l2,dual dual l2 are_concurrent by Th46;
hence thesis;
end;
::$N Converse transitive
theorem
for l,m,n,n1,n2 being Element of ProjectiveLines real_projective_plane st
l <> m & l,m,n are_concurrent & l,m,n1 are_concurrent &
l,m,n2 are_concurrent holds n,n1,n2 are_concurrent
proof
let l,m,n,n1,n2 be Element of ProjectiveLines real_projective_plane;
assume that
A1: l <> m and
A2: l,m,n are_concurrent and
A3: l,m,n1 are_concurrent and
A4: l,m,n2 are_concurrent;
dual l <> dual m & dual l,dual m, dual n are_collinear &
dual l,dual m, dual n1 are_collinear &
dual l,dual m, dual n2 are_collinear by A1,A2,A3,A4,Th60,Th48;
then dual dual n, dual dual n1, dual dual n2 are_concurrent
by ANPROJ_2:def 8,Th59;
then n, dual dual n1, dual dual n2 are_concurrent by Th46;
then n, n1, dual dual n2 are_concurrent by Th46;
hence thesis by Th46;
end;
::$N Converse Vebliean
theorem
for l,l1,l2,n,n1 being Element of ProjectiveLines real_projective_plane st
l,l1,n are_concurrent & l1,l2,n1 are_concurrent
ex n2 being Element of ProjectiveLines real_projective_plane st
l,l2,n2 are_concurrent & n,n1,n2 are_concurrent
proof
let l,l1,l2,n,n1 be Element of ProjectiveLines real_projective_plane;
assume that
A1: l,l1,n are_concurrent and
A2: l1,l2,n1 are_concurrent;
dual l, dual l1, dual n are_collinear &
dual l1,dual l2, dual n1 are_collinear by A1,A2,Th60;
then consider P be Point of real_projective_plane such that
A3: dual l, dual l2, P are_collinear and
A4: dual n, dual n1, P are_collinear by ANPROJ_2:def 9;
take dual P;
dual dual l, dual dual l2, dual P are_concurrent &
dual dual n, dual dual n1, dual P are_concurrent
by A3,A4,Th59;
then l, dual dual l2, dual P are_concurrent &
n, dual dual n1, dual P are_concurrent by Th46;
hence thesis by Th46;
end;
::$N Converse at_least_3rank
theorem
for l,m being Element of ProjectiveLines real_projective_plane holds
ex n being Element of ProjectiveLines real_projective_plane st
l <> n & m <> n & l,m,n are_concurrent
proof
let l,m be Element of ProjectiveLines real_projective_plane;
consider r be Point of real_projective_plane such that
A1: dual l <> r and
A2: dual m <> r and
A3: dual l, dual m, r are_collinear by ANPROJ_2:def 10;
now
thus l <> dual r & m <> dual r by Th45,A1,A2;
dual dual l, dual dual m, dual r are_concurrent by A3,Th59;
then l, dual dual m, dual r are_concurrent by Th46;
hence l, m, dual r are_concurrent by Th46;
end;
hence thesis;
end;
::$N Converse Fanoian
theorem
for l1,n2,m,n1,m1,l,n being Element of ProjectiveLines
real_projective_plane holds
(l1,n2,m are_concurrent & n1,m1,m are_concurrent & l1,n1,l are_concurrent &
n2,m1,l are_concurrent & l1,m1,n are_concurrent & n2,n1,n are_concurrent &
l,m,n are_concurrent implies
(l1,n2,m1 are_concurrent or l1,n2,n1 are_concurrent or
l1,n1,m1 are_concurrent or n2,n1,m1 are_concurrent))
proof
let l1,n2,m,n1,m1,l,n be Element of ProjectiveLines real_projective_plane;
assume that
A1: l1,n2,m are_concurrent and
A2: n1,m1,m are_concurrent and
A3: l1,n1,l are_concurrent and
A4: n2,m1,l are_concurrent and
A5: l1,m1,n are_concurrent and
A6: n2,n1,n are_concurrent and
A7: l,m,n are_concurrent;
dual l1,dual n2,dual m are_collinear &
dual n1,dual m1,dual m are_collinear &
dual l1,dual n1,dual l are_collinear &
dual n2,dual m1,dual l are_collinear &
dual l1,dual m1,dual n are_collinear &
dual n2,dual n1,dual n are_collinear &
dual l,dual m,dual n are_collinear by A1,A2,A3,A4,A5,A6,A7,Th60;
then dual l1,dual n2,dual m1 are_collinear or
dual l1,dual n2,dual n1 are_collinear or
dual l1,dual n1,dual m1 are_collinear or
dual n2,dual n1,dual m1 are_collinear by ANPROJ_2:def 11;
hence thesis by Th60;
end;
::$N Converse Desarguesian
theorem
for k,l1,l2,l3,m1,m2,m3,n1,n2,n3 being Element of ProjectiveLines
real_projective_plane st
k <> m1 & l1 <> m1 & k <> m2 & l2 <> m2 & k <> m3 & l3 <> m3 &
not k,l1,l2 are_concurrent & not k,l1,l3 are_concurrent &
not k,l2,l3 are_concurrent &
l1,l2,n3 are_concurrent & m1,m2,n3 are_concurrent &
l2,l3,n1 are_concurrent & m2,m3,n1 are_concurrent &
l1,l3,n2 are_concurrent & m1,m3,n2 are_concurrent &
k,l1,m1 are_concurrent & k,l2,m2 are_concurrent &
k,l3,m3 are_concurrent holds n1,n2,n3 are_concurrent
proof
let k,l1,l2,l3,m1,m2,m3,n1,n2,n3 be Element of ProjectiveLines
real_projective_plane;
assume that
A1: k <> m1 and
A2: l1 <> m1 and
A3: k <> m2 and
A4: l2 <> m2 and
A5: k <> m3 and
A6: l3 <> m3 and
A7: not k,l1,l2 are_concurrent and
A8: not k,l1,l3 are_concurrent and
A9: not k,l2,l3 are_concurrent and
A10: l1,l2,n3 are_concurrent and
A11: m1,m2,n3 are_concurrent and
A12: l2,l3,n1 are_concurrent and
A13: m2,m3,n1 are_concurrent and
A14: l1,l3,n2 are_concurrent and
A15: m1,m3,n2 are_concurrent and
A16: k,l1,m1 are_concurrent and
A17: k,l2,m2 are_concurrent and
A18: k,l3,m3 are_concurrent;
dual k <> dual m1 & dual l1 <> dual m1 & dual k <> dual m2 &
dual l2 <> dual m2 & dual k <> dual m3 & dual l3 <> dual m3 &
not dual k,dual l1,dual l2 are_collinear &
not dual k,dual l1,dual l3 are_collinear &
not dual k,dual l2,dual l3 are_collinear &
dual l1,dual l2,dual n3 are_collinear &
dual m1,dual m2,dual n3 are_collinear &
dual l2,dual l3,dual n1 are_collinear &
dual m2,dual m3,dual n1 are_collinear &
dual l1,dual l3,dual n2 are_collinear &
dual m1,dual m3,dual n2 are_collinear &
dual k,dual l1,dual m1 are_collinear &
dual k,dual l2,dual m2 are_collinear &
dual k,dual l3,dual m3 are_collinear
by A1,A2,A3,A4,A5,A6,Th48,
A7,A8,A9,A10,A11,A12,A13,A14,A15,A16,A17,A18,Th60;
then dual n1,dual n2, dual n3 are_collinear by ANPROJ_2:def 12;
hence thesis by Th60;
end;
::$N Converse Pappian
theorem
for k,l1,l2,l3,m1,m2,m3,n1,n2,n3 being Element of ProjectiveLines
real_projective_plane st
k <> l2 & k <> l3 & l2 <> l3 & l1 <> l2 & l1 <> l3 & k <> m2 &
k <> m3 & m2 <> m3 & m1 <> m2 & m1 <> m3 &
not k,l1,m1 are_concurrent & k,l1,l2 are_concurrent &
k,l1,l3 are_concurrent & k,m1,m2 are_concurrent &
k,m1,m3 are_concurrent & l1,m2,n3 are_concurrent &
m1,l2,n3 are_concurrent & l1,m3,n2 are_concurrent &
l3,m1,n2 are_concurrent & l2,m3,n1 are_concurrent &
l3,m2,n1 are_concurrent holds n1,n2,n3 are_concurrent
proof
let k,l1,l2,l3,m1,m2,m3,n1,n2,n3 be Element of ProjectiveLines
real_projective_plane;
assume that
A1: k <> l2 and
A2: k <> l3 and
A3: l2 <> l3 and
A4: l1 <> l2 and
A5: l1 <> l3 and
A6: k <> m2 and
A7: k <> m3 and
A8: m2 <> m3 and
A9: m1 <> m2 and
A10: m1 <> m3 and
A11: not k,l1,m1 are_concurrent and
A12: k,l1,l2 are_concurrent and
A13: k,l1,l3 are_concurrent and
A14: k,m1,m2 are_concurrent and
A15: k,m1,m3 are_concurrent and
A16: l1,m2,n3 are_concurrent and
A17: m1,l2,n3 are_concurrent and
A18: l1,m3,n2 are_concurrent and
A19: l3,m1,n2 are_concurrent and
A20: l2,m3,n1 are_concurrent and
A21: l3,m2,n1 are_concurrent;
now
thus dual k <> dual l2 & dual k <> dual l3 & dual l2 <> dual l3
by A1,A2,A3,Th48;
thus dual l1 <> dual l2 & dual l1 <> dual l3 & dual k <> dual m2
by A4,A5,A6,Th48;
thus dual k <> dual m3 & dual m2 <> dual m3 & dual m1 <> dual m2 &
dual m1 <> dual m3 by A7,A8,A9,A10,Th48;
thus not dual k,dual l1,dual m1 are_collinear &
dual k,dual l1,dual l2 are_collinear &
dual k,dual l1,dual l3 are_collinear &
dual k,dual m1,dual m2 are_collinear &
dual k,dual m1,dual m3 are_collinear &
dual l1,dual m2,dual n3 are_collinear &
dual m1,dual l2,dual n3 are_collinear &
dual l1,dual m3,dual n2 are_collinear &
dual l3,dual m1,dual n2 are_collinear &
dual l2,dual m3,dual n1 are_collinear &
dual l3,dual m2,dual n1 are_collinear
by A11,A12,A13,A14,A15,A16,A17,A18,A19,A20,A21,Th60;
end;
then dual n1,dual n2, dual n3 are_collinear by ANPROJ_2:def 13;
hence thesis by Th60;
end;
::$N Converse 2_dimensional
theorem
for l,l1,m,m1 being Element of ProjectiveLines
real_projective_plane holds ex n being Element of ProjectiveLines
real_projective_plane st l,l1,n are_concurrent &
m,m1,n are_concurrent
proof
let l,l1,m,m1 be Element of ProjectiveLines
real_projective_plane;
consider R be Point of real_projective_plane such that
A1: dual l, dual l1, R are_collinear and
A2: dual m, dual m1, R are_collinear by ANPROJ_2:def 14;
dual dual l, dual dual l1, dual R are_concurrent &
dual dual m, dual dual m1, dual R are_concurrent by A1,A2,Th59;
then l, dual dual l1, dual R are_concurrent &
m, dual dual m1, dual R are_concurrent by Th46;
then l, l1, dual R are_concurrent &
m, m1, dual R are_concurrent by Th46;
hence thesis;
end;