:: 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
::
:: Copyright (c) 2021 Association of Mizar Users

theorem :: ANPROJ11:1
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 end;

theorem Th2: :: ANPROJ11:2
for a, b, c, d, e being Real holds |{|[a,1,0]|,|[b,0,1]|,|[c,d,e]|}| = (c - (a * d)) - (e * b)
proof end;

theorem Th3: :: ANPROJ11:3
for a, b, c, d, e being Real holds |{|[1,a,0]|,|[0,b,1]|,|[c,d,e]|}| = ((b * e) + (a * c)) - d
proof end;

theorem Th4: :: ANPROJ11:4
for a, b, c, d, e being Real holds |{|[1,0,a]|,|[0,1,b]|,|[c,d,e]|}| = (e - (c * a)) - (d * b)
proof end;

theorem Th5: :: ANPROJ11:5
for u being Element of () holds
( u is zero iff |(u,u)| = 0 )
proof end;

theorem :: ANPROJ11:6
for u, v, w being non zero Element of () st |{u,v,w}| = 0 holds
ex p being non zero Element of () st
( |(p,u)| = 0 & |(p,v)| = 0 & |(p,w)| = 0 )
proof end;

theorem Th7: :: ANPROJ11:7
for u, v, w being non zero Element of () st |(u,v)| = 0 & are_Prop w,v holds
|(u,w)| = 0
proof end;

theorem Th8: :: ANPROJ11:8
for a, u, v being non zero Element of () st not are_Prop u,v & |(a,u)| = 0 & |(a,v)| = 0 holds
are_Prop a,u <X> v
proof end;

theorem Th9: :: ANPROJ11:9
for u, v being non zero Element of ()
for r being Real st r <> 0 & are_Prop u,v holds
are_Prop r * u,v
proof end;

definition
let P be Point of ();
attr P is zero_proj1 means :Def1: :: ANPROJ11:def 1
for u being non zero Element of () st P = Dir u holds
u . 1 = 0 ;
end;

:: deftheorem Def1 defines zero_proj1 ANPROJ11:def 1 :
for P being Point of () holds
( P is zero_proj1 iff for u being non zero Element of () st P = Dir u holds
u . 1 = 0 );

registration
cluster zero_proj1 for Element of the U1 of ();
existence
ex b1 being Point of () st b1 is zero_proj1
proof end;
end;

registration
cluster non zero_proj1 for Element of the U1 of ();
existence
not for b1 being Point of () holds b1 is zero_proj1
proof end;
end;

theorem Th10: :: ANPROJ11:10
for P being non zero_proj1 Point of ()
for u being non zero Element of () st P = Dir u holds
u . 1 <> 0
proof end;

definition
let P be non zero_proj1 Point of ();
func normalize_proj1 P -> non zero Element of () means :Def2: :: ANPROJ11:def 2
( Dir it = P & it . 1 = 1 );
existence
ex b1 being non zero Element of () st
( Dir b1 = P & b1 . 1 = 1 )
proof end;
uniqueness
for b1, b2 being non zero Element of () st Dir b1 = P & b1 . 1 = 1 & Dir b2 = P & b2 . 1 = 1 holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines normalize_proj1 ANPROJ11:def 2 :
for P being non zero_proj1 Point of ()
for b2 being non zero Element of () holds
( b2 = normalize_proj1 P iff ( Dir b2 = P & b2 . 1 = 1 ) );

theorem Th11: :: ANPROJ11:11
for P being non zero_proj1 Point of ()
for u being non zero Element of () st P = Dir u holds
normalize_proj1 P = |[1,((u . 2) / (u . 1)),((u . 3) / (u . 1))]|
proof end;

theorem :: ANPROJ11:12
for P being non zero_proj1 Point of ()
for Q being Point of () st Q = Dir () holds
not Q is zero_proj1 by Def2;

definition
let P be Point of ();
attr P is zero_proj2 means :Def3: :: ANPROJ11:def 3
for u being non zero Element of () st P = Dir u holds
u . 2 = 0 ;
end;

:: deftheorem Def3 defines zero_proj2 ANPROJ11:def 3 :
for P being Point of () holds
( P is zero_proj2 iff for u being non zero Element of () st P = Dir u holds
u . 2 = 0 );

registration
cluster zero_proj2 for Element of the U1 of ();
existence
ex b1 being Point of () st b1 is zero_proj2
proof end;
end;

registration
cluster non zero_proj2 for Element of the U1 of ();
existence
not for b1 being Point of () holds b1 is zero_proj2
proof end;
end;

theorem Th13: :: ANPROJ11:13
for P being non zero_proj2 Point of ()
for u being non zero Element of () st P = Dir u holds
u . 2 <> 0
proof end;

definition
let P be non zero_proj2 Point of ();
func normalize_proj2 P -> non zero Element of () means :Def4: :: ANPROJ11:def 4
( Dir it = P & it . 2 = 1 );
existence
ex b1 being non zero Element of () st
( Dir b1 = P & b1 . 2 = 1 )
proof end;
uniqueness
for b1, b2 being non zero Element of () st Dir b1 = P & b1 . 2 = 1 & Dir b2 = P & b2 . 2 = 1 holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines normalize_proj2 ANPROJ11:def 4 :
for P being non zero_proj2 Point of ()
for b2 being non zero Element of () holds
( b2 = normalize_proj2 P iff ( Dir b2 = P & b2 . 2 = 1 ) );

theorem Th14: :: ANPROJ11:14
for P being non zero_proj2 Point of ()
for u being non zero Element of () st P = Dir u holds
normalize_proj2 P = |[((u . 1) / (u . 2)),1,((u . 3) / (u . 2))]|
proof end;

theorem :: ANPROJ11:15
for P being non zero_proj2 Point of ()
for Q being Point of () st Q = Dir () holds
not Q is zero_proj2 by Def4;

definition
let P be Point of ();
attr P is zero_proj3 means :Def5: :: ANPROJ11:def 5
for u being non zero Element of () st P = Dir u holds
u . 3 = 0 ;
end;

:: deftheorem Def5 defines zero_proj3 ANPROJ11:def 5 :
for P being Point of () holds
( P is zero_proj3 iff for u being non zero Element of () st P = Dir u holds
u . 3 = 0 );

registration
cluster zero_proj3 for Element of the U1 of ();
existence
ex b1 being Point of () st b1 is zero_proj3
proof end;
end;

registration
cluster non zero_proj3 for Element of the U1 of ();
existence
not for b1 being Point of () holds b1 is zero_proj3
proof end;
end;

theorem Th16: :: ANPROJ11:16
for P being non zero_proj3 Point of ()
for u being non zero Element of () st P = Dir u holds
u . 3 <> 0
proof end;

definition
let P be non zero_proj3 Point of ();
func normalize_proj3 P -> non zero Element of () means :Def6: :: ANPROJ11:def 6
( Dir it = P & it . 3 = 1 );
existence
ex b1 being non zero Element of () st
( Dir b1 = P & b1 . 3 = 1 )
proof end;
uniqueness
for b1, b2 being non zero Element of () st Dir b1 = P & b1 . 3 = 1 & Dir b2 = P & b2 . 3 = 1 holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines normalize_proj3 ANPROJ11:def 6 :
for P being non zero_proj3 Point of ()
for b2 being non zero Element of () holds
( b2 = normalize_proj3 P iff ( Dir b2 = P & b2 . 3 = 1 ) );

theorem Th17: :: ANPROJ11:17
for P being non zero_proj3 Point of ()
for u being non zero Element of () st P = Dir u holds
normalize_proj3 P = |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]|
proof end;

theorem :: ANPROJ11:18
for P being non zero_proj3 Point of ()
for Q being Point of () st Q = Dir () holds
not Q is zero_proj3 by Def6;

registration
cluster non zero_proj1 non zero_proj2 for Element of the U1 of ();
existence
ex b1 being Point of () st
( not b1 is zero_proj1 & not b1 is zero_proj2 )
proof end;
end;

registration
cluster non zero_proj1 non zero_proj3 for Element of the U1 of ();
existence
ex b1 being Point of () st
( not b1 is zero_proj1 & not b1 is zero_proj3 )
proof end;
end;

registration
cluster non zero_proj2 non zero_proj3 for Element of the U1 of ();
existence
ex b1 being Point of () st
( not b1 is zero_proj2 & not b1 is zero_proj3 )
proof end;
end;

registration
cluster non zero_proj1 non zero_proj2 non zero_proj3 for Element of the U1 of ();
existence
ex b1 being Point of () st
( not b1 is zero_proj1 & not b1 is zero_proj2 & not b1 is zero_proj3 )
proof end;
end;

definition
let P be non zero_proj1 Point of ();
func dir1a P -> non zero Element of () equals :: ANPROJ11:def 7
|[(- (() . 2)),1,0]|;
coherence
|[(- (() . 2)),1,0]| is non zero Element of ()
;
end;

:: deftheorem defines dir1a ANPROJ11:def 7 :
for P being non zero_proj1 Point of () holds dir1a P = |[(- (() . 2)),1,0]|;

definition
let P be non zero_proj1 Point of ();
func Pdir1a P -> Point of () equals :: ANPROJ11:def 8
Dir ();
coherence
Dir () is Point of ()
by ANPROJ_1:26;
end;

:: deftheorem defines Pdir1a ANPROJ11:def 8 :
for P being non zero_proj1 Point of () holds Pdir1a P = Dir ();

definition
let P be non zero_proj1 Point of ();
func dir1b P -> non zero Element of () equals :: ANPROJ11:def 9
|[(- (() . 3)),0,1]|;
coherence
|[(- (() . 3)),0,1]| is non zero Element of ()
;
end;

:: deftheorem defines dir1b ANPROJ11:def 9 :
for P being non zero_proj1 Point of () holds dir1b P = |[(- (() . 3)),0,1]|;

definition
let P be non zero_proj1 Point of ();
func Pdir1b P -> Point of () equals :: ANPROJ11:def 10
Dir ();
coherence
Dir () is Point of ()
by ANPROJ_1:26;
end;

:: deftheorem defines Pdir1b ANPROJ11:def 10 :
for P being non zero_proj1 Point of () holds Pdir1b P = Dir ();

theorem :: ANPROJ11:19
for P being non zero_proj1 Point of () holds dir1a P <> dir1b P by FINSEQ_1:78;

theorem Th20: :: ANPROJ11:20
for P being non zero_proj1 Point of () holds Dir () <> Dir ()
proof end;

theorem Th21: :: ANPROJ11:21
for P being non zero_proj1 Element of ()
for u being non zero Element of ()
for v being Element of () st u = normalize_proj1 P holds
|{(),(),v}| = |(u,v)|
proof end;

theorem :: ANPROJ11:22
for P being non zero_proj1 Element of ()
for u being non zero Element of () st u = normalize_proj1 P holds
|{(),(),()}| = (1 + ((u . 2) * (u . 2))) + ((u . 3) * (u . 3))
proof end;

definition
let P be non zero_proj2 Point of ();
func dir2a P -> non zero Element of () equals :: ANPROJ11:def 11
|[1,(- (() . 1)),0]|;
coherence
|[1,(- (() . 1)),0]| is non zero Element of ()
;
end;

:: deftheorem defines dir2a ANPROJ11:def 11 :
for P being non zero_proj2 Point of () holds dir2a P = |[1,(- (() . 1)),0]|;

definition
let P be non zero_proj2 Point of ();
func Pdir2a P -> Point of () equals :: ANPROJ11:def 12
Dir ();
coherence
Dir () is Point of ()
by ANPROJ_1:26;
end;

:: deftheorem defines Pdir2a ANPROJ11:def 12 :
for P being non zero_proj2 Point of () holds Pdir2a P = Dir ();

definition
let P be non zero_proj2 Point of ();
func dir2b P -> non zero Element of () equals :: ANPROJ11:def 13
|[0,(- (() . 3)),1]|;
coherence
|[0,(- (() . 3)),1]| is non zero Element of ()
;
end;

:: deftheorem defines dir2b ANPROJ11:def 13 :
for P being non zero_proj2 Point of () holds dir2b P = |[0,(- (() . 3)),1]|;

definition
let P be non zero_proj2 Point of ();
func Pdir2b P -> Point of () equals :: ANPROJ11:def 14
Dir ();
coherence
Dir () is Point of ()
by ANPROJ_1:26;
end;

:: deftheorem defines Pdir2b ANPROJ11:def 14 :
for P being non zero_proj2 Point of () holds Pdir2b P = Dir ();

theorem :: ANPROJ11:23
for P being non zero_proj2 Point of () holds dir2a P <> dir2b P by FINSEQ_1:78;

theorem Th24: :: ANPROJ11:24
for P being non zero_proj2 Point of () holds Dir () <> Dir ()
proof end;

theorem Th25: :: ANPROJ11:25
for P being non zero_proj2 Element of ()
for u being non zero Element of ()
for v being Element of () st u = normalize_proj2 P holds
|{(),(),v}| = - |(u,v)|
proof end;

theorem :: ANPROJ11:26
for P being non zero_proj2 Element of ()
for u being non zero Element of () st u = normalize_proj2 P holds
|{(),(),()}| = - ((((u . 1) * (u . 1)) + 1) + ((u . 3) * (u . 3)))
proof end;

definition
let P be non zero_proj3 Point of ();
func dir3a P -> non zero Element of () equals :: ANPROJ11:def 15
|[1,0,(- (() . 1))]|;
coherence
|[1,0,(- (() . 1))]| is non zero Element of ()
;
end;

:: deftheorem defines dir3a ANPROJ11:def 15 :
for P being non zero_proj3 Point of () holds dir3a P = |[1,0,(- (() . 1))]|;

definition
let P be non zero_proj3 Point of ();
func Pdir3a P -> Point of () equals :: ANPROJ11:def 16
Dir ();
coherence
Dir () is Point of ()
by ANPROJ_1:26;
end;

:: deftheorem defines Pdir3a ANPROJ11:def 16 :
for P being non zero_proj3 Point of () holds Pdir3a P = Dir ();

definition
let P be non zero_proj3 Point of ();
func dir3b P -> non zero Element of () equals :: ANPROJ11:def 17
|[0,1,(- (() . 2))]|;
coherence
|[0,1,(- (() . 2))]| is non zero Element of ()
;
end;

:: deftheorem defines dir3b ANPROJ11:def 17 :
for P being non zero_proj3 Point of () holds dir3b P = |[0,1,(- (() . 2))]|;

definition
let P be non zero_proj3 Point of ();
func Pdir3b P -> Point of () equals :: ANPROJ11:def 18
Dir ();
coherence
Dir () is Point of ()
by ANPROJ_1:26;
end;

:: deftheorem defines Pdir3b ANPROJ11:def 18 :
for P being non zero_proj3 Point of () holds Pdir3b P = Dir ();

theorem :: ANPROJ11:27
for P being non zero_proj3 Point of () holds dir3a P <> dir3b P by FINSEQ_1:78;

theorem Th28: :: ANPROJ11:28
for P being non zero_proj3 Point of () holds Dir () <> Dir ()
proof end;

theorem Th29: :: ANPROJ11:29
for P being non zero_proj3 Element of ()
for u being non zero Element of ()
for v being Element of () st u = normalize_proj3 P holds
|{(),(),v}| = |(u,v)|
proof end;

theorem :: ANPROJ11:30
for P being non zero_proj3 Element of ()
for u being non zero Element of () st u = normalize_proj3 P holds
|{(),(),()}| = (((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) + 1
proof end;

definition
let P be non zero_proj1 Point of ();
func dual1 P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 19
Line ((),());
correctness
coherence
Line ((),()) is Element of ProjectiveLines real_projective_plane
;
proof end;
end;

:: deftheorem defines dual1 ANPROJ11:def 19 :
for P being non zero_proj1 Point of () holds dual1 P = Line ((),());

definition
let P be non zero_proj2 Point of ();
func dual2 P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 20
Line ((),());
correctness
coherence
Line ((),()) is Element of ProjectiveLines real_projective_plane
;
proof end;
end;

:: deftheorem defines dual2 ANPROJ11:def 20 :
for P being non zero_proj2 Point of () holds dual2 P = Line ((),());

definition
let P be non zero_proj3 Point of ();
func dual3 P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 21
Line ((),());
correctness
coherence
Line ((),()) is Element of ProjectiveLines real_projective_plane
;
proof end;
end;

:: deftheorem defines dual3 ANPROJ11:def 21 :
for P being non zero_proj3 Point of () holds dual3 P = Line ((),());

theorem :: ANPROJ11:31
for P being non zero_proj1 non zero_proj2 Point of ()
for u being non zero Element of () 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 ;

theorem :: ANPROJ11:32
for P being non zero_proj1 non zero_proj2 Point of ()
for u being non zero Element of () st P = Dir u holds
( normalize_proj1 P = ((u . 2) / (u . 1)) * () & normalize_proj2 P = ((u . 1) / (u . 2)) * () )
proof end;

theorem Th33: :: ANPROJ11:33
for P being non zero_proj1 non zero_proj2 Point of () holds dual1 P = dual2 P
proof end;

theorem Th34: :: ANPROJ11:34
for P being non zero_proj2 non zero_proj3 Point of () holds dual2 P = dual3 P
proof end;

theorem Th35: :: ANPROJ11:35
for P being non zero_proj1 non zero_proj3 Point of () holds dual1 P = dual3 P
proof end;

theorem :: ANPROJ11:36
for P being non zero_proj1 non zero_proj2 non zero_proj3 Point of () holds
( dual1 P = dual2 P & dual1 P = dual3 P & dual2 P = dual3 P ) by ;

theorem Th37: :: ANPROJ11:37
for P being Element of () holds
( not P is zero_proj1 or not P is zero_proj2 or not P is zero_proj3 )
proof end;

definition
let P be Point of ();
func dual P -> Element of ProjectiveLines real_projective_plane means :Def22: :: ANPROJ11:def 22
ex P9 being non zero_proj1 Point of () st
( P9 = P & it = dual1 P9 ) if not P is zero_proj1
ex P9 being non zero_proj2 Point of () st
( P9 = P & it = dual2 P9 ) if ( P is zero_proj1 & not P is zero_proj2 )
ex P9 being non zero_proj3 Point of () st
( P9 = P & it = dual3 P9 ) if ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 )
;
correctness
consistency
for b1 being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & P is zero_proj1 & not P is zero_proj2 implies ( ex P9 being non zero_proj1 Point of () st
( P9 = P & b1 = dual1 P9 ) iff ex P9 being non zero_proj2 Point of () st
( P9 = P & b1 = dual2 P9 ) ) ) & ( not P is zero_proj1 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj1 Point of () st
( P9 = P & b1 = dual1 P9 ) iff ex P9 being non zero_proj3 Point of () st
( P9 = P & b1 = dual3 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj2 Point of () st
( P9 = P & b1 = dual2 P9 ) iff ex P9 being non zero_proj3 Point of () st
( P9 = P & b1 = dual3 P9 ) ) ) )
;
existence
( ( for b1 being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & P is zero_proj1 & not P is zero_proj2 implies ( ex P9 being non zero_proj1 Point of () st
( P9 = P & b1 = dual1 P9 ) iff ex P9 being non zero_proj2 Point of () st
( P9 = P & b1 = dual2 P9 ) ) ) & ( not P is zero_proj1 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj1 Point of () st
( P9 = P & b1 = dual1 P9 ) iff ex P9 being non zero_proj3 Point of () st
( P9 = P & b1 = dual3 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 & P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( ex P9 being non zero_proj2 Point of () st
( P9 = P & b1 = dual2 P9 ) iff ex P9 being non zero_proj3 Point of () st
( P9 = P & b1 = dual3 P9 ) ) ) ) ) & ( not P is zero_proj1 implies ex b1 being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj1 Point of () st
( P9 = P & b1 = dual1 P9 ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ex b1 being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj2 Point of () st
( P9 = P & b1 = dual2 P9 ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ex b1 being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj3 Point of () st
( P9 = P & b1 = dual3 P9 ) ) )
;
uniqueness
for b1, b2 being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & ex P9 being non zero_proj1 Point of () st
( P9 = P & b1 = dual1 P9 ) & ex P9 being non zero_proj1 Point of () st
( P9 = P & b2 = dual1 P9 ) implies b1 = b2 ) & ( P is zero_proj1 & not P is zero_proj2 & ex P9 being non zero_proj2 Point of () st
( P9 = P & b1 = dual2 P9 ) & ex P9 being non zero_proj2 Point of () st
( P9 = P & b2 = dual2 P9 ) implies b1 = b2 ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 & ex P9 being non zero_proj3 Point of () st
( P9 = P & b1 = dual3 P9 ) & ex P9 being non zero_proj3 Point of () st
( P9 = P & b2 = dual3 P9 ) implies b1 = b2 ) )
;
proof end;
end;

:: deftheorem Def22 defines dual ANPROJ11:def 22 :
for P being Point of ()
for b2 being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 implies ( b2 = dual P iff ex P9 being non zero_proj1 Point of () st
( P9 = P & b2 = dual1 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ( b2 = dual P iff ex P9 being non zero_proj2 Point of () st
( P9 = P & b2 = dual2 P9 ) ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( b2 = dual P iff ex P9 being non zero_proj3 Point of () st
( P9 = P & b2 = dual3 P9 ) ) ) );

definition
let P be Point of real_projective_plane;
func # P -> Element of () equals :: ANPROJ11:def 23
P;
coherence
P is Element of ()
;
end;

:: deftheorem defines # ANPROJ11:def 23 :
for P being Point of real_projective_plane holds # P = P;

definition
let P be Point of real_projective_plane;
coherence ;
end;

:: deftheorem defines dual ANPROJ11:def 24 :
for P being Point of real_projective_plane holds dual P = dual (# P);

theorem Th38: :: ANPROJ11:38
for P being Element of real_projective_plane st not # P is zero_proj1 holds
ex P9 being non zero_proj1 Point of () st
( P = P9 & dual P = dual1 P9 )
proof end;

theorem Th39: :: ANPROJ11:39
for P being Element of real_projective_plane st not # P is zero_proj2 holds
ex P9 being non zero_proj2 Point of () st
( P = P9 & dual P = dual2 P9 )
proof end;

theorem Th40: :: ANPROJ11:40
for P being Element of real_projective_plane st not # P is zero_proj3 holds
ex P9 being non zero_proj3 Point of () st
( P = P9 & dual P = dual3 P9 )
proof end;

theorem Th41: :: ANPROJ11:41
for P being non zero_proj1 Element of () holds not P in Line ((),())
proof end;

theorem Th42: :: ANPROJ11:42
for P being non zero_proj2 Element of () holds not P in Line ((),())
proof end;

theorem Th43: :: ANPROJ11:43
for P being non zero_proj3 Element of () holds not P in Line ((),())
proof end;

theorem :: ANPROJ11:44
for P being Point of real_projective_plane holds not P in dual P
proof end;

definition
let l be Element of ProjectiveLines real_projective_plane;
func dual l -> Point of real_projective_plane means :Def25: :: ANPROJ11:def 25
ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & it = L2P (P,Q) );
existence
ex b1, P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b1 = L2P (P,Q) )
proof end;
uniqueness
for b1, b2 being Point of real_projective_plane st ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b1 = L2P (P,Q) ) & ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b2 = L2P (P,Q) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines dual ANPROJ11:def 25 :
for l being Element of ProjectiveLines real_projective_plane
for b2 being Point of real_projective_plane holds
( b2 = dual l iff ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b2 = L2P (P,Q) ) );

theorem Th45: :: ANPROJ11:45
for P being Point of real_projective_plane holds dual (dual P) = P
proof end;

theorem Th46: :: ANPROJ11:46
for l being Element of ProjectiveLines real_projective_plane holds dual (dual l) = l
proof end;

theorem :: ANPROJ11:47
for P, Q being Point of real_projective_plane holds
( P <> Q iff dual P <> dual Q )
proof end;

theorem Th48: :: ANPROJ11:48
for l, m being Element of ProjectiveLines real_projective_plane holds
( l <> m iff dual l <> dual m )
proof end;

definition
let l1, l2, l3 be Element of ProjectiveLines real_projective_plane;
pred l1,l2,l3 are_concurrent means :: ANPROJ11:def 26
ex P being Point of real_projective_plane st
( P in l1 & P in l2 & P in l3 );
end;

:: deftheorem defines are_concurrent ANPROJ11:def 26 :
for l1, l2, l3 being Element of ProjectiveLines real_projective_plane holds
( l1,l2,l3 are_concurrent iff ex P being Point of real_projective_plane st
( P in l1 & P in l2 & P in l3 ) );

definition
let l be Element of ProjectiveLines real_projective_plane;
func # l -> LINE of equals :: ANPROJ11:def 27
l;
coherence ;
end;

:: deftheorem defines # ANPROJ11:def 27 :
for l being Element of ProjectiveLines real_projective_plane holds # l = l;

definition
let l be LINE of ;
coherence ;
end;

:: deftheorem defines # ANPROJ11:def 28 :
for l being LINE of holds # l = l;

theorem Th49: :: ANPROJ11:49
for l1, l2, l3 being Element of ProjectiveLines real_projective_plane holds
( l1,l2,l3 are_concurrent iff # l1, # l2, # l3 are_concurrent )
proof end;

theorem :: ANPROJ11:50
for l1, l2, l3 being LINE of holds
( l1,l2,l3 are_concurrent iff # l1, # l2, # l3 are_concurrent )
proof end;

theorem :: ANPROJ11:51
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 :: ANPROJ11:52
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 :: ANPROJ11:53
for P, Q being Point of real_projective_plane
for P9, Q9 being Element of () st P = P9 & Q = Q9 holds
Line (P,Q) = Line (P9,Q9) ;

theorem Th54: :: ANPROJ11:54
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 end;

theorem :: ANPROJ11:55
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 end;

theorem Th56: :: ANPROJ11:56
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 end;

theorem Th57: :: ANPROJ11:57
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 end;

theorem Th58: :: ANPROJ11:58
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 end;

theorem Th59: :: ANPROJ11:59
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 end;

theorem Th60: :: ANPROJ11:60
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 end;

theorem :: ANPROJ11:61

:: Converse reflexive
theorem :: ANPROJ11:62
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 end;

:: Converse transitive
theorem :: ANPROJ11:63
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 end;

:: Converse Vebliean
theorem :: ANPROJ11:64
for l, l1, l2, n, n1 being Element of ProjectiveLines real_projective_plane st l,l1,n are_concurrent & l1,l2,n1 are_concurrent holds
ex n2 being Element of ProjectiveLines real_projective_plane st
( l,l2,n2 are_concurrent & n,n1,n2 are_concurrent )
proof end;

:: Converse at_least_3rank
theorem :: ANPROJ11:65
for l, m being Element of ProjectiveLines real_projective_plane ex n being Element of ProjectiveLines real_projective_plane st
( l <> n & m <> n & l,m,n are_concurrent )
proof end;

:: Converse Fanoian
theorem :: ANPROJ11:66
for l1, n2, m, n1, m1, l, n being Element of ProjectiveLines real_projective_plane st 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 & not l1,n2,m1 are_concurrent & not l1,n2,n1 are_concurrent & not l1,n1,m1 are_concurrent holds
n2,n1,m1 are_concurrent
proof end;

:: Converse Desarguesian
theorem :: ANPROJ11:67
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 end;

:: Converse Pappian
theorem :: ANPROJ11:68
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 end;

:: Converse 2_dimensional
theorem :: ANPROJ11:69
for l, l1, m, m1 being Element of ProjectiveLines real_projective_plane ex n being Element of ProjectiveLines real_projective_plane st
( l,l1,n are_concurrent & m,m1,n are_concurrent )
proof end;