let P be non zero_proj1 non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)); dual1 P = dual3 P
consider u being Element of (TOP-REAL 3) such that
A1:
not u is zero
and
A2:
P = Dir u
by ANPROJ_1:26;
reconsider u = u as non zero Element of (TOP-REAL 3) by A1;
A3:
( normalize_proj1 P = |[1,((u . 2) / (u . 1)),((u . 3) / (u . 1))]| & normalize_proj3 P = |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| )
by A2, Th11, Th17;
now ( Line ((Pdir1a P),(Pdir1b P)) c= Line ((Pdir3a P),(Pdir3b P)) & Line ((Pdir3a P),(Pdir3b P)) c= Line ((Pdir1a P),(Pdir1b P)) )now for x being object st x in Line ((Pdir1a P),(Pdir1b P)) holds
x in Line ((Pdir3a P),(Pdir3b P))let x be
object ;
( x in Line ((Pdir1a P),(Pdir1b P)) implies x in Line ((Pdir3a P),(Pdir3b P)) )assume
x in Line (
(Pdir1a P),
(Pdir1b P))
;
x in Line ((Pdir3a P),(Pdir3b P))then consider P9 being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A4:
x = P9
and A5:
Pdir1a P,
Pdir1b P,
P9 are_collinear
;
consider u9 being
Element of
(TOP-REAL 3) such that A6:
not
u9 is
zero
and A7:
P9 = Dir u9
by ANPROJ_1:26;
set a2 =
- ((normalize_proj1 P) . 2);
set a3 =
- ((normalize_proj1 P) . 3);
set b1 =
u9 `1 ;
set b2 =
u9 `2 ;
set b3 =
u9 `3 ;
A8:
- ((normalize_proj1 P) . 2) =
- ((normalize_proj1 P) `2)
.=
- ((u . 2) / (u . 1))
by A3, EUCLID_5:2
;
A9:
- ((normalize_proj1 P) . 3) =
- ((normalize_proj1 P) `3)
.=
- ((u . 3) / (u . 1))
by A3, EUCLID_5:2
;
0 =
|{(dir1a P),(dir1b P),u9}|
by A5, A6, A7, BKMODEL1:1
.=
|{|[(- ((normalize_proj1 P) . 2)),1,0]|,|[(- ((normalize_proj1 P) . 3)),0,1]|,|[(u9 `1),(u9 `2),(u9 `3)]|}|
by EUCLID_5:3
.=
((u9 `1) - ((- ((normalize_proj1 P) . 2)) * (u9 `2))) - ((- ((normalize_proj1 P) . 3)) * (u9 `3))
by Th2
.=
((u9 `1) + (((u . 2) / (u . 1)) * (u9 `2))) + (((u . 3) / (u . 1)) * (u9 `3))
by A8, A9
;
then A10:
0 =
(u . 1) * (((u9 `1) + (((u . 2) / (u . 1)) * (u9 `2))) + (((u . 3) / (u . 1)) * (u9 `3)))
.=
(((u . 1) * (u9 `1)) + (((u . 1) * ((u . 2) / (u . 1))) * (u9 `2))) + (((u . 1) * ((u . 3) / (u . 1))) * (u9 `3))
.=
(((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + (((u . 1) * ((u . 3) / (u . 1))) * (u9 `3))
by A2, Th10, XCMPLX_1:87
.=
(((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3))
by A2, Th10, XCMPLX_1:87
;
set c2 =
- ((normalize_proj3 P) . 1);
set c3 =
- ((normalize_proj3 P) . 2);
A11:
- ((normalize_proj3 P) . 1) =
- ((normalize_proj3 P) `1)
.=
- ((u . 1) / (u . 3))
by A3, EUCLID_5:2
;
A12:
- ((normalize_proj3 P) . 2) =
- ((normalize_proj3 P) `2)
.=
- ((u . 2) / (u . 3))
by A3, EUCLID_5:2
;
|{|[1,0,(- ((normalize_proj3 P) . 1))]|,|[0,1,(- ((normalize_proj3 P) . 2))]|,|[(u9 `1),(u9 `2),(u9 `3)]|}| = ((u9 `3) - ((- ((normalize_proj3 P) . 1)) * (u9 `1))) - ((- ((normalize_proj3 P) . 2)) * (u9 `2))
by Th4;
then |{(dir3a P),(dir3b P),u9}| =
((((u . 1) / (u . 3)) * (u9 `1)) + (((u . 2) / (u . 3)) * (u9 `2))) + (1 * (u9 `3))
by A11, A12, EUCLID_5:3
.=
((((u . 1) / (u . 3)) * (u9 `1)) + (((u . 2) / (u . 3)) * (u9 `2))) + (((u . 3) / (u . 3)) * (u9 `3))
by XCMPLX_1:60, A2, Th16
.=
(1 / (u . 3)) * ((((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3)))
.=
0
by A10
;
then
Pdir3a P,
Pdir3b P,
P9 are_collinear
by A6, A7, BKMODEL1:1;
hence
x in Line (
(Pdir3a P),
(Pdir3b P))
by A4;
verum end; hence
Line (
(Pdir1a P),
(Pdir1b P))
c= Line (
(Pdir3a P),
(Pdir3b P))
;
Line ((Pdir3a P),(Pdir3b P)) c= Line ((Pdir1a P),(Pdir1b P))now for x being object st x in Line ((Pdir3a P),(Pdir3b P)) holds
x in Line ((Pdir1a P),(Pdir1b P))let x be
object ;
( x in Line ((Pdir3a P),(Pdir3b P)) implies x in Line ((Pdir1a P),(Pdir1b P)) )assume
x in Line (
(Pdir3a P),
(Pdir3b P))
;
x in Line ((Pdir1a P),(Pdir1b P))then consider P9 being
Point of
(ProjectiveSpace (TOP-REAL 3)) such that A13:
x = P9
and A14:
Pdir3a P,
Pdir3b P,
P9 are_collinear
;
consider u9 being
Element of
(TOP-REAL 3) such that A15:
not
u9 is
zero
and A16:
P9 = Dir u9
by ANPROJ_1:26;
set a2 =
- ((normalize_proj1 P) . 2);
set a3 =
- ((normalize_proj1 P) . 3);
set b1 =
u9 `1 ;
set b2 =
u9 `2 ;
set b3 =
u9 `3 ;
set c2 =
- ((normalize_proj3 P) . 1);
set c3 =
- ((normalize_proj3 P) . 2);
A17:
- ((normalize_proj1 P) . 2) =
- ((normalize_proj1 P) `2)
.=
- ((u . 2) / (u . 1))
by A3, EUCLID_5:2
;
A18:
- ((normalize_proj1 P) . 3) =
- ((normalize_proj1 P) `3)
.=
- ((u . 3) / (u . 1))
by A3, EUCLID_5:2
;
A19:
- ((normalize_proj3 P) . 1) =
- ((normalize_proj3 P) `1)
.=
- ((u . 1) / (u . 3))
by A3, EUCLID_5:2
;
A20:
- ((normalize_proj3 P) . 2) =
- ((normalize_proj3 P) `2)
.=
- ((u . 2) / (u . 3))
by A3, EUCLID_5:2
;
A21:
0 =
|{(dir3a P),(dir3b P),u9}|
by A14, A15, A16, BKMODEL1:1
.=
|{|[1,0,(- ((normalize_proj3 P) . 1))]|,|[0,1,(- ((normalize_proj3 P) . 2))]|,|[(u9 `1),(u9 `2),(u9 `3)]|}|
by EUCLID_5:3
.=
((u9 `3) - ((- ((normalize_proj3 P) . 1)) * (u9 `1))) - ((- ((normalize_proj3 P) . 2)) * (u9 `2))
by Th4
.=
((((u . 1) / (u . 3)) * (u9 `1)) + (((u . 2) / (u . 3)) * (u9 `2))) + (1 * (u9 `3))
by A19, A20
.=
((((u . 1) / (u . 3)) * (u9 `1)) + (((u . 2) / (u . 3)) * (u9 `2))) + (((u . 3) / (u . 3)) * (u9 `3))
by XCMPLX_1:60, A2, Th16
.=
(1 / (u . 3)) * ((((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3)))
;
A22:
u . 3
<> 0
by A2, Th16;
A23:
(u . 1) / (u . 1) = 1
by XCMPLX_1:60, A2, Th10;
|{(dir1a P),(dir1b P),u9}| =
|{|[(- ((normalize_proj1 P) . 2)),1,0]|,|[(- ((normalize_proj1 P) . 3)),0,1]|,|[(u9 `1),(u9 `2),(u9 `3)]|}|
by EUCLID_5:3
.=
((u9 `1) - ((- ((normalize_proj1 P) . 2)) * (u9 `2))) - ((- ((normalize_proj1 P) . 3)) * (u9 `3))
by Th2
.=
((((u . 1) / (u . 1)) * (u9 `1)) + (((u . 2) / (u . 1)) * (u9 `2))) + (((u . 3) / (u . 1)) * (u9 `3))
by A17, A18, A23
.=
(1 / (u . 1)) * ((((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3)))
.=
(1 / (u . 1)) * 0
by A22, A21, XCMPLX_1:6
.=
0
;
then
Pdir1a P,
Pdir1b P,
P9 are_collinear
by A15, A16, BKMODEL1:1;
hence
x in Line (
(Pdir1a P),
(Pdir1b P))
by A13;
verum end; hence
Line (
(Pdir3a P),
(Pdir3b P))
c= Line (
(Pdir1a P),
(Pdir1b P))
;
verum
hence
dual1 P = dual3 P
; verum