:: 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 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 (TOP-REAL 3) holds
( u is zero iff |(u,u)| = 0 )

proof end;

theorem :: ANPROJ11:6

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 end;

theorem Th7: :: ANPROJ11:7

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 end;

theorem Th8: :: ANPROJ11:8

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 end;

theorem Th9: :: ANPROJ11:9

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 end;

definition

let P be Point of (ProjectiveSpace (TOP-REAL 3));

attr P is zero_proj1 means :Def1: :: ANPROJ11:def 1
for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
u . 1 = 0 ;

end;

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

registration

cluster zero_proj1 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
ex b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) st b₁ is zero_proj1

proof end;

end;

registration

cluster non zero_proj1 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
not for b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) holds b₁ is zero_proj1

proof end;

end;

theorem Th10: :: ANPROJ11:10

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 end;

definition

let P be non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3));

func normalize_proj1 P -> non zero Element of (TOP-REAL 3) means :Def2: :: ANPROJ11:def 2
( Dir it = P & it . 1 = 1 );

existence
ex b₁ being non zero Element of (TOP-REAL 3) st
( Dir b₁ = P & b₁ . 1 = 1 )

proof end;

uniqueness
for b₁, b₂ being non zero Element of (TOP-REAL 3) st Dir b₁ = P & b₁ . 1 = 1 & Dir b₂ = P & b₂ . 1 = 1 holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines normalize_proj1 ANPROJ11:def 2 :
for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3))
for b₂ being non zero Element of (TOP-REAL 3) holds
( b₂ = normalize_proj1 P iff ( Dir b₂ = P & b₂ . 1 = 1 ) );

theorem Th11: :: ANPROJ11:11

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 end;

theorem :: ANPROJ11:12

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
not Q is zero_proj1 by Def2;

definition

let P be Point of (ProjectiveSpace (TOP-REAL 3));

attr P is zero_proj2 means :Def3: :: ANPROJ11:def 3
for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
u . 2 = 0 ;

end;

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

registration

cluster zero_proj2 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
ex b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) st b₁ is zero_proj2

proof end;

end;

registration

cluster non zero_proj2 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
not for b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) holds b₁ is zero_proj2

proof end;

end;

theorem Th13: :: ANPROJ11:13

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 end;

definition

let P be non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3));

func normalize_proj2 P -> non zero Element of (TOP-REAL 3) means :Def4: :: ANPROJ11:def 4
( Dir it = P & it . 2 = 1 );

existence
ex b₁ being non zero Element of (TOP-REAL 3) st
( Dir b₁ = P & b₁ . 2 = 1 )

proof end;

uniqueness
for b₁, b₂ being non zero Element of (TOP-REAL 3) st Dir b₁ = P & b₁ . 2 = 1 & Dir b₂ = P & b₂ . 2 = 1 holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines normalize_proj2 ANPROJ11:def 4 :
for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3))
for b₂ being non zero Element of (TOP-REAL 3) holds
( b₂ = normalize_proj2 P iff ( Dir b₂ = P & b₂ . 2 = 1 ) );

theorem Th14: :: ANPROJ11:14

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 end;

theorem :: ANPROJ11:15

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
not Q is zero_proj2 by Def4;

definition

let P be Point of (ProjectiveSpace (TOP-REAL 3));

attr P is zero_proj3 means :Def5: :: ANPROJ11:def 5
for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
u . 3 = 0 ;

end;

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

registration

cluster zero_proj3 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
ex b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) st b₁ is zero_proj3

proof end;

end;

registration

cluster non zero_proj3 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
not for b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) holds b₁ is zero_proj3

proof end;

end;

theorem Th16: :: ANPROJ11:16

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 end;

definition

let P be non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3));

func normalize_proj3 P -> non zero Element of (TOP-REAL 3) means :Def6: :: ANPROJ11:def 6
( Dir it = P & it . 3 = 1 );

existence
ex b₁ being non zero Element of (TOP-REAL 3) st
( Dir b₁ = P & b₁ . 3 = 1 )

proof end;

uniqueness
for b₁, b₂ being non zero Element of (TOP-REAL 3) st Dir b₁ = P & b₁ . 3 = 1 & Dir b₂ = P & b₂ . 3 = 1 holds
b₁ = b₂

proof end;

end;

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

theorem Th17: :: ANPROJ11:17

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 end;

theorem :: ANPROJ11:18

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
not Q is zero_proj3 by Def6;

registration

cluster non zero_proj1 non zero_proj2 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
ex b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) st
( not b₁ is zero_proj1 & not b₁ is zero_proj2 )

proof end;

end;

registration

cluster non zero_proj1 non zero_proj3 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
ex b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) st
( not b₁ is zero_proj1 & not b₁ is zero_proj3 )

proof end;

end;

registration

cluster non zero_proj2 non zero_proj3 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
ex b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) st
( not b₁ is zero_proj2 & not b₁ is zero_proj3 )

proof end;

end;

registration

cluster non zero_proj1 non zero_proj2 non zero_proj3 for Element of the U1 of (ProjectiveSpace (TOP-REAL 3));

existence
ex b₁ being Point of (ProjectiveSpace (TOP-REAL 3)) st
( not b₁ is zero_proj1 & not b₁ is zero_proj2 & not b₁ is zero_proj3 )

proof end;

end;

definition

let P be non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3));

func dir1a P -> non zero Element of (TOP-REAL 3) equals :: ANPROJ11:def 7
|[(- ((normalize_proj1 P) . 2)),1,0]|;

coherence
|[(- ((normalize_proj1 P) . 2)),1,0]| is non zero Element of (TOP-REAL 3) ;

end;

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

definition

let P be non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3));

func Pdir1a P -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ11:def 8
Dir (dir1a P);

coherence
Dir (dir1a P) is Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

end;

:: deftheorem defines Pdir1a ANPROJ11:def 8 :
for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir1a P = Dir (dir1a P);

definition

let P be non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3));

func dir1b P -> non zero Element of (TOP-REAL 3) equals :: ANPROJ11:def 9
|[(- ((normalize_proj1 P) . 3)),0,1]|;

coherence
|[(- ((normalize_proj1 P) . 3)),0,1]| is non zero Element of (TOP-REAL 3) ;

end;

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

definition

let P be non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3));

func Pdir1b P -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ11:def 10
Dir (dir1b P);

coherence
Dir (dir1b P) is Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

end;

:: deftheorem defines Pdir1b ANPROJ11:def 10 :
for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir1b P = Dir (dir1b P);

theorem :: ANPROJ11:19

for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds dir1a P <> dir1b P by FINSEQ_1:78;

theorem Th20: :: ANPROJ11:20

for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds Dir (dir1a P) <> Dir (dir1b P)

proof end;

theorem Th21: :: ANPROJ11:21

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 end;

theorem :: ANPROJ11:22

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 end;

definition

let P be non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3));

func dir2a P -> non zero Element of (TOP-REAL 3) equals :: ANPROJ11:def 11
|[1,(- ((normalize_proj2 P) . 1)),0]|;

coherence
|[1,(- ((normalize_proj2 P) . 1)),0]| is non zero Element of (TOP-REAL 3) ;

end;

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

definition

let P be non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3));

func Pdir2a P -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ11:def 12
Dir (dir2a P);

coherence
Dir (dir2a P) is Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

end;

:: deftheorem defines Pdir2a ANPROJ11:def 12 :
for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir2a P = Dir (dir2a P);

definition

let P be non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3));

func dir2b P -> non zero Element of (TOP-REAL 3) equals :: ANPROJ11:def 13
|[0,(- ((normalize_proj2 P) . 3)),1]|;

coherence
|[0,(- ((normalize_proj2 P) . 3)),1]| is non zero Element of (TOP-REAL 3) ;

end;

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

definition

let P be non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3));

func Pdir2b P -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ11:def 14
Dir (dir2b P);

coherence
Dir (dir2b P) is Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

end;

:: deftheorem defines Pdir2b ANPROJ11:def 14 :
for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir2b P = Dir (dir2b P);

theorem :: ANPROJ11:23

for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds dir2a P <> dir2b P by FINSEQ_1:78;

theorem Th24: :: ANPROJ11:24

for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds Dir (dir2a P) <> Dir (dir2b P)

proof end;

theorem Th25: :: ANPROJ11:25

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 end;

theorem :: ANPROJ11:26

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 end;

definition

let P be non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3));

func dir3a P -> non zero Element of (TOP-REAL 3) equals :: ANPROJ11:def 15
|[1,0,(- ((normalize_proj3 P) . 1))]|;

coherence
|[1,0,(- ((normalize_proj3 P) . 1))]| is non zero Element of (TOP-REAL 3) ;

end;

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

definition

let P be non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3));

func Pdir3a P -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ11:def 16
Dir (dir3a P);

coherence
Dir (dir3a P) is Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

end;

:: deftheorem defines Pdir3a ANPROJ11:def 16 :
for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir3a P = Dir (dir3a P);

definition

let P be non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3));

func dir3b P -> non zero Element of (TOP-REAL 3) equals :: ANPROJ11:def 17
|[0,1,(- ((normalize_proj3 P) . 2))]|;

coherence
|[0,1,(- ((normalize_proj3 P) . 2))]| is non zero Element of (TOP-REAL 3) ;

end;

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

definition

let P be non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3));

func Pdir3b P -> Point of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ11:def 18
Dir (dir3b P);

coherence
Dir (dir3b P) is Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;

end;

:: deftheorem defines Pdir3b ANPROJ11:def 18 :
for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir3b P = Dir (dir3b P);

theorem :: ANPROJ11:27

for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds dir3a P <> dir3b P by FINSEQ_1:78;

theorem Th28: :: ANPROJ11:28

for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds Dir (dir3a P) <> Dir (dir3b P)

proof end;

theorem Th29: :: ANPROJ11:29

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 end;

theorem :: ANPROJ11:30

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 end;

definition

let P be non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3));

func dual1 P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 19
Line ((Pdir1a P),(Pdir1b P));

correctness
coherence
Line ((Pdir1a P),(Pdir1b P)) is Element of ProjectiveLines real_projective_plane;

proof end;

end;

:: deftheorem defines dual1 ANPROJ11:def 19 :
for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual1 P = Line ((Pdir1a P),(Pdir1b P));

definition

let P be non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3));

func dual2 P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 20
Line ((Pdir2a P),(Pdir2b P));

correctness
coherence
Line ((Pdir2a P),(Pdir2b P)) is Element of ProjectiveLines real_projective_plane;

proof end;

end;

:: deftheorem defines dual2 ANPROJ11:def 20 :
for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual2 P = Line ((Pdir2a P),(Pdir2b P));

definition

let P be non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3));

func dual3 P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 21
Line ((Pdir3a P),(Pdir3b P));

correctness
coherence
Line ((Pdir3a P),(Pdir3b P)) is Element of ProjectiveLines real_projective_plane;

proof end;

end;

:: deftheorem defines dual3 ANPROJ11:def 21 :
for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual3 P = Line ((Pdir3a P),(Pdir3b P));

theorem :: ANPROJ11:31

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 :: ANPROJ11:32

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 end;

theorem Th33: :: ANPROJ11:33

for P being non zero_proj1 non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual1 P = dual2 P

proof end;

theorem Th34: :: ANPROJ11:34

for P being non zero_proj2 non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual2 P = dual3 P

proof end;

theorem Th35: :: ANPROJ11:35

for P being non zero_proj1 non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual1 P = dual3 P

proof end;

theorem :: ANPROJ11:36

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: :: ANPROJ11:37

for P being Element of (ProjectiveSpace (TOP-REAL 3)) 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 (ProjectiveSpace (TOP-REAL 3));

func dual P -> Element of ProjectiveLines real_projective_plane means :Def22: :: ANPROJ11:def 22
ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & it = dual1 P9 ) if not P is 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 & not P is 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 & not P is zero_proj3 )
;

correctness
consistency
for b₁ 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 (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = 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 (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = 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 (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) );
existence
( ( for b₁ 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 (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = 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 (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = 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 (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) ) ) ) & ( not P is zero_proj1 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ex b₁ being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) ) );
uniqueness
for b₁, b₂ being Element of ProjectiveLines real_projective_plane holds
( ( not P is zero_proj1 & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual1 P9 ) & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual1 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & not P is zero_proj2 & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual2 P9 ) & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual2 P9 ) implies b₁ = b₂ ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₁ = dual3 P9 ) & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st
( P9 = P & b₂ = dual3 P9 ) implies b₁ = b₂ ) );

proof end;

end;

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

definition

let P be Point of real_projective_plane;

func # P -> Element of (ProjectiveSpace (TOP-REAL 3)) equals :: ANPROJ11:def 23
P;

coherence
P is Element of (ProjectiveSpace (TOP-REAL 3)) ;

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;

func dual P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 24
dual (# P);

coherence
dual (# P) is Element of ProjectiveLines real_projective_plane ;

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 (ProjectiveSpace (TOP-REAL 3)) 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 (ProjectiveSpace (TOP-REAL 3)) 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 (ProjectiveSpace (TOP-REAL 3)) st
( P = P9 & dual P = dual3 P9 )

proof end;

theorem Th41: :: ANPROJ11:41

for P being non zero_proj1 Element of (ProjectiveSpace (TOP-REAL 3)) holds not P in Line ((Pdir1a P),(Pdir1b P))

proof end;

theorem Th42: :: ANPROJ11:42

for P being non zero_proj2 Element of (ProjectiveSpace (TOP-REAL 3)) holds not P in Line ((Pdir2a P),(Pdir2b P))

proof end;

theorem Th43: :: ANPROJ11:43

for P being non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)) holds not P in Line ((Pdir3a P),(Pdir3b P))

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 b₁, P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b₁ = L2P (P,Q) )

proof end;

uniqueness
for b₁, b₂ being Point of real_projective_plane st ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b₁ = L2P (P,Q) ) & ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b₂ = L2P (P,Q) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def25 defines dual ANPROJ11:def 25 :
for l being Element of ProjectiveLines real_projective_plane
for b₂ being Point of real_projective_plane holds
( b₂ = dual l iff ex P, Q being Point of real_projective_plane st
( P <> Q & l = Line (P,Q) & b₂ = 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 (IncProjSp_of real_projective_plane) equals :: ANPROJ11:def 27
l;

coherence
l is LINE of (IncProjSp_of real_projective_plane) ;

end;

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

definition

let l be LINE of (IncProjSp_of real_projective_plane);

func # l -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 28
l;

coherence
l is Element of ProjectiveLines real_projective_plane ;

end;

:: deftheorem defines # ANPROJ11:def 28 :
for l being LINE of (IncProjSp_of real_projective_plane) 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 (IncProjSp_of real_projective_plane) 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 (ProjectiveSpace (TOP-REAL 3)) 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

( 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 ) ;

:: 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;