let P be Point of real_projective_plane; for l being Element of ProjectiveLines real_projective_plane st P in l holds
dual l in dual P
let l be Element of ProjectiveLines real_projective_plane; ( P in l implies dual l in dual P )
assume A1:
P in l
; dual l in dual P
consider u being Element of (TOP-REAL 3) such that
A2:
not u is zero
and
A3:
P = Dir u
by ANPROJ_1:26;
reconsider u = u as non zero Element of (TOP-REAL 3) by A2;
reconsider P9 = P as Element of (ProjectiveSpace (TOP-REAL 3)) ;
reconsider dl = dual l as Point of (ProjectiveSpace (TOP-REAL 3)) ;
consider Pl, Ql being Point of real_projective_plane such that
A4:
Pl <> Ql
and
A5:
l = Line (Pl,Ql)
and
A6:
dual l = L2P (Pl,Ql)
by Def25;
consider ul, vl being non zero Element of (TOP-REAL 3) such that
A7:
Pl = Dir ul
and
A8:
Ql = Dir vl
and
A9:
L2P (Pl,Ql) = Dir (ul <X> vl)
by A4, BKMODEL1:def 5;
reconsider ulvl = ul <X> vl as non zero Element of (TOP-REAL 3) by A4, A7, A8, BKMODEL1:78;
consider S being Point of real_projective_plane such that
A10:
P = S
and
A11:
Pl,Ql,S are_collinear
by A1, A5;
P,Pl,Ql are_collinear
by A10, A11, ANPROJ_2:24;
then A12:
|{u,ul,vl}| = 0
by A3, A7, A8, BKMODEL1:1;
per cases
( not P9 is zero_proj1 or not P9 is zero_proj2 or not P9 is zero_proj3 )
by Th37;
suppose
not
P9 is
zero_proj1
;
dual l in dual Pthen reconsider P9 =
P9 as non
zero_proj1 Point of
(ProjectiveSpace (TOP-REAL 3)) ;
consider P99 being non
zero_proj1 Point of
(ProjectiveSpace (TOP-REAL 3)) such that A13:
P9 = P99
and A14:
dual P = dual1 P99
by Th38;
consider S being
Point of
real_projective_plane such that A15:
P = S
and A16:
Pl,
Ql,
S are_collinear
by A1, A5;
P,
Pl,
Ql are_collinear
by A15, A16, ANPROJ_2:24;
then A17:
|{u,ul,vl}| = 0
by A3, A7, A8, BKMODEL1:1;
Dir (normalize_proj1 P9) = Dir u
by A3, Def2;
then A18:
are_Prop normalize_proj1 P9,
u
by ANPROJ_1:22;
|{(dir1a P9),(dir1b P9),ulvl}| =
|((normalize_proj1 P9),ulvl)|
by Th21
.=
0
by A17, A18, Th7
;
then
Pdir1a P9,
Pdir1b P9,
dl are_collinear
by A6, A9, BKMODEL1:1;
hence
dual l in dual P
by A13, A14;
verum end; suppose
not
P9 is
zero_proj2
;
dual l in dual Pthen reconsider P9 =
P9 as non
zero_proj2 Point of
(ProjectiveSpace (TOP-REAL 3)) ;
consider P99 being non
zero_proj2 Point of
(ProjectiveSpace (TOP-REAL 3)) such that A19:
P9 = P99
and A20:
dual P = dual2 P99
by Th39;
Dir (normalize_proj2 P9) = Dir u
by A3, Def4;
then A21:
are_Prop normalize_proj2 P9,
u
by ANPROJ_1:22;
|{(dir2a P9),(dir2b P9),ulvl}| =
- |((normalize_proj2 P9),ulvl)|
by Th25
.=
- 0
by A12, A21, Th7
;
then
Pdir2a P9,
Pdir2b P9,
dl are_collinear
by A6, A9, BKMODEL1:1;
hence
dual l in dual P
by A19, A20;
verum end; suppose
not
P9 is
zero_proj3
;
dual l in dual Pthen reconsider P9 =
P9 as non
zero_proj3 Point of
(ProjectiveSpace (TOP-REAL 3)) ;
consider P99 being non
zero_proj3 Point of
(ProjectiveSpace (TOP-REAL 3)) such that A22:
P9 = P99
and A23:
dual P = dual3 P99
by Th40;
Dir (normalize_proj3 P9) = Dir u
by A3, Def6;
then A24:
are_Prop normalize_proj3 P9,
u
by ANPROJ_1:22;
|{(dir3a P9),(dir3b P9),ulvl}| =
|((normalize_proj3 P9),ulvl)|
by Th29
.=
0
by A12, A24, Th7
;
then
Pdir3a P9,
Pdir3b P9,
dl are_collinear
by A6, A9, BKMODEL1:1;
hence
dual l in dual P
by A22, A23;
verum end;