let P be non zero_proj1 non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)); dual1 P = dual2 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_proj2 P = |[((u . 1) / (u . 2)),1,((u . 3) / (u . 2))]| )
by A2, Th11, Th14;
now ( Line ((Pdir1a P),(Pdir1b P)) c= Line ((Pdir2a P),(Pdir2b P)) & Line ((Pdir2a P),(Pdir2b P)) c= Line ((Pdir1a P),(Pdir1b P)) )now for x being object st x in Line ((Pdir1a P),(Pdir1b P)) holds
x in Line ((Pdir2a P),(Pdir2b P))let x be
object ;
( x in Line ((Pdir1a P),(Pdir1b P)) implies x in Line ((Pdir2a P),(Pdir2b P)) )assume
x in Line (
(Pdir1a P),
(Pdir1b P))
;
x in Line ((Pdir2a P),(Pdir2b 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_proj2 P) . 1);
set c3 =
- ((normalize_proj2 P) . 3);
A11:
- ((normalize_proj2 P) . 1) =
- ((normalize_proj2 P) `1)
.=
- ((u . 1) / (u . 2))
by A3, EUCLID_5:2
;
A12:
- ((normalize_proj2 P) . 3) =
- ((normalize_proj2 P) `3)
.=
- ((u . 3) / (u . 2))
by A3, EUCLID_5:2
;
|{|[1,(- ((normalize_proj2 P) . 1)),0]|,|[0,(- ((normalize_proj2 P) . 3)),1]|,|[(u9 `1),(u9 `2),(u9 `3)]|}| = (((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) - (u9 `2)
by A11, A12, Th3;
then |{(dir2a P),(dir2b P),u9}| =
(((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- 1) * (u9 `2))
by EUCLID_5:3
.=
(((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2))
by XCMPLX_1:60, A2, Th13
.=
((((u . 1) / (- (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2))
by XCMPLX_1:188
.=
((((u . 1) / (- (u . 2))) * (u9 `1)) + (((u . 3) / (- (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2))
by XCMPLX_1:188
.=
((((u . 1) / (- (u . 2))) * (u9 `1)) + (((u . 3) / (- (u . 2))) * (u9 `3))) + (((u . 2) / (- (u . 2))) * (u9 `2))
by XCMPLX_1:188
.=
(1 / (- (u . 2))) * ((((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3)))
.=
0
by A10
;
then
Pdir2a P,
Pdir2b P,
P9 are_collinear
by A6, A7, BKMODEL1:1;
hence
x in Line (
(Pdir2a P),
(Pdir2b P))
by A4;
verum end; hence
Line (
(Pdir1a P),
(Pdir1b P))
c= Line (
(Pdir2a P),
(Pdir2b P))
;
Line ((Pdir2a P),(Pdir2b P)) c= Line ((Pdir1a P),(Pdir1b P))now for x being object st x in Line ((Pdir2a P),(Pdir2b P)) holds
x in Line ((Pdir1a P),(Pdir1b P))let x be
object ;
( x in Line ((Pdir2a P),(Pdir2b P)) implies x in Line ((Pdir1a P),(Pdir1b P)) )assume
x in Line (
(Pdir2a P),
(Pdir2b 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:
Pdir2a P,
Pdir2b 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_proj2 P) . 1);
set c3 =
- ((normalize_proj2 P) . 3);
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_proj2 P) . 1) =
- ((normalize_proj2 P) `1)
.=
- ((u . 1) / (u . 2))
by A3, EUCLID_5:2
;
A20:
- ((normalize_proj2 P) . 3) =
- ((normalize_proj2 P) `3)
.=
- ((u . 3) / (u . 2))
by A3, EUCLID_5:2
;
A21:
- (u . 2) <> 0
by A2, Th13;
A22:
0 =
|{(dir2a P),(dir2b P),u9}|
by A14, A15, A16, BKMODEL1:1
.=
|{|[1,(- ((normalize_proj2 P) . 1)),0]|,|[0,(- ((normalize_proj2 P) . 3)),1]|,|[(u9 `1),(u9 `2),(u9 `3)]|}|
by EUCLID_5:3
.=
(((- ((normalize_proj2 P) . 3)) * (u9 `3)) + ((- ((normalize_proj2 P) . 1)) * (u9 `1))) - (u9 `2)
by Th3
.=
(((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- 1) * (u9 `2))
by A19, A20
.=
(((- ((u . 1) / (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2))
by XCMPLX_1:60, A2, Th13
.=
((((u . 1) / (- (u . 2))) * (u9 `1)) + ((- ((u . 3) / (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2))
by XCMPLX_1:188
.=
((((u . 1) / (- (u . 2))) * (u9 `1)) + (((u . 3) / (- (u . 2))) * (u9 `3))) + ((- ((u . 2) / (u . 2))) * (u9 `2))
by XCMPLX_1:188
.=
((((u . 1) / (- (u . 2))) * (u9 `1)) + (((u . 3) / (- (u . 2))) * (u9 `3))) + (((u . 2) / (- (u . 2))) * (u9 `2))
by XCMPLX_1:188
.=
(1 / (- (u . 2))) * ((((u . 1) * (u9 `1)) + ((u . 2) * (u9 `2))) + ((u . 3) * (u9 `3)))
;
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 (
(Pdir2a P),
(Pdir2b P))
c= Line (
(Pdir1a P),
(Pdir1b P))
;
verum
hence
dual1 P = dual2 P
; verum