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

ex p being non zero Element of (TOP-REAL 3) st

( |(p,u)| = 0 & |(p,v)| = 0 & |(p,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

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

for r being Real st r <> 0 & are_Prop u,v holds

are_Prop r * u,v

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

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

registration

existence

not for b_{1} being Point of (ProjectiveSpace (TOP-REAL 3)) holds b_{1} is zero_proj1

end;
not for b

proof 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

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

ex b_{1} being non zero Element of (TOP-REAL 3) st

( Dir b_{1} = P & b_{1} . 1 = 1 )

for b_{1}, b_{2} being non zero Element of (TOP-REAL 3) st Dir b_{1} = P & b_{1} . 1 = 1 & Dir b_{2} = P & b_{2} . 1 = 1 holds

b_{1} = b_{2}

end;
func normalize_proj1 P -> non zero Element of (TOP-REAL 3) means :Def2: :: ANPROJ11:def 2

( Dir it = P & it . 1 = 1 );

existence ( Dir it = P & it . 1 = 1 );

ex b

( Dir b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines normalize_proj1 ANPROJ11:def 2 :

for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3))

for b_{2} being non zero Element of (TOP-REAL 3) holds

( b_{2} = normalize_proj1 P iff ( Dir b_{2} = P & b_{2} . 1 = 1 ) );

for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3))

for b

( b

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))]|

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;

for Q being Point of (ProjectiveSpace (TOP-REAL 3)) st Q = Dir (normalize_proj1 P) holds

not Q is zero_proj1 by Def2;

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

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

registration

existence

not for b_{1} being Point of (ProjectiveSpace (TOP-REAL 3)) holds b_{1} is zero_proj2

end;
not for b

proof 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

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

ex b_{1} being non zero Element of (TOP-REAL 3) st

( Dir b_{1} = P & b_{1} . 2 = 1 )

for b_{1}, b_{2} being non zero Element of (TOP-REAL 3) st Dir b_{1} = P & b_{1} . 2 = 1 & Dir b_{2} = P & b_{2} . 2 = 1 holds

b_{1} = b_{2}

end;
func normalize_proj2 P -> non zero Element of (TOP-REAL 3) means :Def4: :: ANPROJ11:def 4

( Dir it = P & it . 2 = 1 );

existence ( Dir it = P & it . 2 = 1 );

ex b

( Dir b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines normalize_proj2 ANPROJ11:def 4 :

for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3))

for b_{2} being non zero Element of (TOP-REAL 3) holds

( b_{2} = normalize_proj2 P iff ( Dir b_{2} = P & b_{2} . 2 = 1 ) );

for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3))

for b

( b

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))]|

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;

for Q being Point of (ProjectiveSpace (TOP-REAL 3)) st Q = Dir (normalize_proj2 P) holds

not Q is zero_proj2 by Def4;

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

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

registration

existence

not for b_{1} being Point of (ProjectiveSpace (TOP-REAL 3)) holds b_{1} is zero_proj3

end;
not for b

proof 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

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

ex b_{1} being non zero Element of (TOP-REAL 3) st

( Dir b_{1} = P & b_{1} . 3 = 1 )

for b_{1}, b_{2} being non zero Element of (TOP-REAL 3) st Dir b_{1} = P & b_{1} . 3 = 1 & Dir b_{2} = P & b_{2} . 3 = 1 holds

b_{1} = b_{2}

end;
func normalize_proj3 P -> non zero Element of (TOP-REAL 3) means :Def6: :: ANPROJ11:def 6

( Dir it = P & it . 3 = 1 );

existence ( Dir it = P & it . 3 = 1 );

ex b

( Dir b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines normalize_proj3 ANPROJ11:def 6 :

for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3))

for b_{2} being non zero Element of (TOP-REAL 3) holds

( b_{2} = normalize_proj3 P iff ( Dir b_{2} = P & b_{2} . 3 = 1 ) );

for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3))

for b

( b

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]|

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;

for Q being Point of (ProjectiveSpace (TOP-REAL 3)) st Q = Dir (normalize_proj3 P) holds

not Q is zero_proj3 by Def6;

registration

existence

ex b_{1} being Point of (ProjectiveSpace (TOP-REAL 3)) st

( not b_{1} is zero_proj1 & not b_{1} is zero_proj2 )

end;
ex b

( not b

proof end;

registration

existence

ex b_{1} being Point of (ProjectiveSpace (TOP-REAL 3)) st

( not b_{1} is zero_proj1 & not b_{1} is zero_proj3 )

end;
ex b

( not b

proof end;

registration

existence

ex b_{1} being Point of (ProjectiveSpace (TOP-REAL 3)) st

( not b_{1} is zero_proj2 & not b_{1} is zero_proj3 )

end;
ex b

( not b

proof end;

registration

ex b_{1} being Point of (ProjectiveSpace (TOP-REAL 3)) st

( not b_{1} is zero_proj1 & not b_{1} is zero_proj2 & not b_{1} is zero_proj3 )
end;

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

existence ex b

( not b

proof end;

definition

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

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

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

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

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

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

coherence

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

end;
coherence

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

:: deftheorem defines Pdir1a ANPROJ11:def 8 :

for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir1a P = Dir (dir1a P);

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

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

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

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

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

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

coherence

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

end;
coherence

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

:: deftheorem defines Pdir1b ANPROJ11:def 10 :

for P being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir1b P = Dir (dir1b P);

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

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

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

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

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

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

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

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

coherence

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

end;
coherence

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

:: deftheorem defines Pdir2a ANPROJ11:def 12 :

for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir2a P = Dir (dir2a P);

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

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

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

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

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

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

coherence

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

end;
coherence

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

:: deftheorem defines Pdir2b ANPROJ11:def 14 :

for P being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir2b P = Dir (dir2b P);

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

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

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

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

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

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

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

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

coherence

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

end;
coherence

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

:: deftheorem defines Pdir3a ANPROJ11:def 16 :

for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir3a P = Dir (dir3a P);

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

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

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

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

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

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

coherence

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

end;
coherence

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

:: deftheorem defines Pdir3b ANPROJ11:def 18 :

for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds Pdir3b P = Dir (dir3b P);

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

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

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

coherence

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

end;
func dual1 P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 19

Line ((Pdir1a P),(Pdir1b P));

correctness Line ((Pdir1a P),(Pdir1b P));

coherence

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

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

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

coherence

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

end;
func dual2 P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 20

Line ((Pdir2a P),(Pdir2b P));

correctness Line ((Pdir2a P),(Pdir2b P));

coherence

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

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

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

coherence

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

end;
func dual3 P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 21

Line ((Pdir3a P),(Pdir3b P));

correctness Line ((Pdir3a P),(Pdir3b P));

coherence

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

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

for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) holds dual3 P = Line ((Pdir3a P),(Pdir3b P));

theorem :: ANPROJ11:31

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

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;

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

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

consistency

for b_{1} 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_{1} = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{1} = 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_{1} = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{1} = 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_{1} = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{1} = dual3 P9 ) ) ) );

existence

( ( for b_{1} 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_{1} = dual1 P9 ) iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{1} = 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_{1} = dual1 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{1} = 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_{1} = dual2 P9 ) iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{1} = dual3 P9 ) ) ) ) ) & ( not P is zero_proj1 implies ex b_{1} being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{1} = dual1 P9 ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ex b_{1} being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{1} = dual2 P9 ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ex b_{1} being Element of ProjectiveLines real_projective_plane ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{1} = dual3 P9 ) ) );

uniqueness

for b_{1}, b_{2} 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_{1} = dual1 P9 ) & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{2} = dual1 P9 ) implies b_{1} = b_{2} ) & ( 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_{1} = dual2 P9 ) & ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{2} = dual2 P9 ) implies b_{1} = b_{2} ) & ( 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_{1} = dual3 P9 ) & ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{2} = dual3 P9 ) implies b_{1} = b_{2} ) );

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

;

consistency

for b

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

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

existence

( ( for b

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

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

uniqueness

for b

( ( not P is zero_proj1 & ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

( P9 = P & b

proof end;

:: deftheorem Def22 defines dual ANPROJ11:def 22 :

for P being Point of (ProjectiveSpace (TOP-REAL 3))

for b_{2} being Element of ProjectiveLines real_projective_plane holds

( ( not P is zero_proj1 implies ( b_{2} = dual P iff ex P9 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{2} = dual1 P9 ) ) ) & ( P is zero_proj1 & not P is zero_proj2 implies ( b_{2} = dual P iff ex P9 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{2} = dual2 P9 ) ) ) & ( P is zero_proj1 & P is zero_proj2 & not P is zero_proj3 implies ( b_{2} = dual P iff ex P9 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) st

( P9 = P & b_{2} = dual3 P9 ) ) ) );

for P being Point of (ProjectiveSpace (TOP-REAL 3))

for b

( ( not P is zero_proj1 implies ( b

( P9 = P & b

( P9 = P & b

( P9 = P & b

definition
end;

definition

let P be Point of real_projective_plane;

dual (# P) is Element of ProjectiveLines real_projective_plane ;

end;
func dual P -> Element of ProjectiveLines real_projective_plane equals :: ANPROJ11:def 24

dual (# P);

coherence dual (# P);

dual (# P) is Element of ProjectiveLines real_projective_plane ;

:: deftheorem defines dual ANPROJ11:def 24 :

for P being Point of real_projective_plane holds dual P = dual (# P);

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 )

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 )

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 )

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;

definition

let l be Element of ProjectiveLines real_projective_plane;

ex b_{1}, P, Q being Point of real_projective_plane st

( P <> Q & l = Line (P,Q) & b_{1} = L2P (P,Q) )

for b_{1}, b_{2} being Point of real_projective_plane st ex P, Q being Point of real_projective_plane st

( P <> Q & l = Line (P,Q) & b_{1} = L2P (P,Q) ) & ex P, Q being Point of real_projective_plane st

( P <> Q & l = Line (P,Q) & b_{2} = L2P (P,Q) ) holds

b_{1} = b_{2}

end;
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 P, Q being Point of real_projective_plane st

( P <> Q & l = Line (P,Q) & it = L2P (P,Q) );

ex b

( P <> Q & l = Line (P,Q) & b

proof end;

uniqueness for b

( P <> Q & l = Line (P,Q) & b

( P <> Q & l = Line (P,Q) & b

b

proof end;

:: deftheorem Def25 defines dual ANPROJ11:def 25 :

for l being Element of ProjectiveLines real_projective_plane

for b_{2} being Point of real_projective_plane holds

( b_{2} = dual l iff ex P, Q being Point of real_projective_plane st

( P <> Q & l = Line (P,Q) & b_{2} = L2P (P,Q) ) );

for l being Element of ProjectiveLines real_projective_plane

for b

( b

( P <> Q & l = Line (P,Q) & b

theorem Th48: :: ANPROJ11:48

for l, m being Element of ProjectiveLines real_projective_plane holds

( l <> m iff dual l <> dual m )

( l <> m iff dual l <> dual m )

proof end;

definition

let l1, l2, l3 be Element of ProjectiveLines real_projective_plane;

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

ex P being Point of real_projective_plane st

( P in l1 & P in l2 & P in l3 );

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

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;

coherence

l is LINE of (IncProjSp_of real_projective_plane) ;

end;
coherence

l is LINE of (IncProjSp_of real_projective_plane) ;

:: deftheorem defines # ANPROJ11:def 27 :

for l being Element of ProjectiveLines real_projective_plane holds # l = l;

for l being Element of ProjectiveLines real_projective_plane holds # l = l;

definition

let l be LINE of (IncProjSp_of real_projective_plane);

coherence

l is Element of ProjectiveLines real_projective_plane ;

end;
coherence

l is Element of ProjectiveLines real_projective_plane ;

:: deftheorem defines # ANPROJ11:def 28 :

for l being LINE of (IncProjSp_of real_projective_plane) holds # l = l;

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 )

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

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

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

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

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

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

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

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

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

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 )

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

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

( l,m,l are_concurrent & l,l,m are_concurrent & l,m,m are_concurrent )

proof end;

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

n,n1,n2 are_concurrent

proof end;

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 )

ex n2 being Element of ProjectiveLines real_projective_plane st

( l,l2,n2 are_concurrent & n,n1,n2 are_concurrent )

proof end;

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 )

( l <> n & m <> n & l,m,n are_concurrent )

proof end;

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

n2,n1,m1 are_concurrent

proof end;

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

n1,n2,n3 are_concurrent

proof end;

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

n1,n2,n3 are_concurrent

proof end;

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 )

( l,l1,n are_concurrent & m,m1,n are_concurrent )

proof end;