let l be Element of ProjectiveLines real_projective_plane; :: thesis: dual (dual l) = l
consider P, Q being Point of real_projective_plane such that
A1: P <> Q and
A2: l = Line (P,Q) and
A3: dual l = L2P (P,Q) by Def25;
reconsider P9 = P, Q9 = Q as Point of (ProjectiveSpace (TOP-REAL 3)) ;
consider u, v being non zero Element of (TOP-REAL 3) such that
A4: P = Dir u and
A5: Q = Dir v and
A6: L2P (P,Q) = Dir (u <X> v) by A1, BKMODEL1:def 5;
reconsider l2 = Line (P,Q) as LINE of real_projective_plane by A1, COLLSP:def 7;
not are_Prop u,v by A1, A4, A5, ANPROJ_1:22;
then not u <X> v is zero by ANPROJ_8:51;
then reconsider uv = u <X> v as non zero Element of (TOP-REAL 3) ;
reconsider R = Dir uv as Point of (ProjectiveSpace (TOP-REAL 3)) by ANPROJ_1:26;
reconsider R9 = R as Element of real_projective_plane ;
A7: 0 = |((u <X> v),u)| by ANPROJ_8:44
.= (((uv `1) * (u `1)) + ((uv `2) * (u `2))) + ((uv `3) * (u `3)) by EUCLID_5:29
.= (((uv . 1) * (u `1)) + ((uv . 2) * (u `2))) + ((uv . 3) * (u `3)) ;
A8: 0 = |((u <X> v),v)| by ANPROJ_8:45
.= (((uv `1) * (v `1)) + ((uv `2) * (v `2))) + ((uv `3) * (v `3)) by EUCLID_5:29
.= (((uv . 1) * (v `1)) + ((uv . 2) * (v `2))) + ((uv . 3) * (v `3)) ;
per cases ( not R is zero_proj1 or not R is zero_proj2 or not R is zero_proj3 ) by Th37;
suppose A9: not R is zero_proj1 ; :: thesis: dual (dual l) = l
then reconsider R = R as non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) ;
# R9 = R ;
then consider P99 being non zero_proj1 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A10: R9 = P99 and
A11: dual R9 = dual1 P99 by Th38;
A12: (uv . 1) / (uv . 1) = 1 by A9, Th10, XCMPLX_1:60;
normalize_proj1 P99 = |[1,((uv . 2) / (uv . 1)),((uv . 3) / (uv . 1))]| by A10, Th11;
then A13: ( (normalize_proj1 P99) `2 = (uv . 2) / (uv . 1) & (normalize_proj1 P99) `3 = (uv . 3) / (uv . 1) ) by EUCLID_5:2;
reconsider l1 = Line ((Pdir1a P99),(Pdir1b P99)) as LINE of real_projective_plane by Th20, COLLSP:def 7;
now :: thesis: ( P in l1 & Q in l1 & P in l2 & Q in l2 )
|{|[(- ((uv . 2) / (uv . 1))),1,0]|,|[(- ((uv . 3) / (uv . 1))),0,1]|,|[(u `1),(u `2),(u `3)]|}| = ((u `1) - ((- ((uv . 2) / (uv . 1))) * (u `2))) - ((u `3) * (- ((uv . 3) / (uv . 1)))) by Th2
.= ((((uv . 1) / (uv . 1)) * (u `1)) + (((uv . 2) / (uv . 1)) * (u `2))) + ((u `3) * ((uv . 3) / (uv . 1))) by A12
.= (1 / (uv . 1)) * ((((uv . 1) * (u `1)) + ((uv . 2) * (u `2))) + ((uv . 3) * (u `3)))
.= 0 by A7 ;
then |{(dir1a P99),(dir1b P99),u}| = 0 by A13, EUCLID_5:3;
then Pdir1a P99, Pdir1b P99,P9 are_collinear by A4, BKMODEL1:1;
hence P in l1 ; :: thesis: ( Q in l1 & P in l2 & Q in l2 )
|{|[(- ((uv . 2) / (uv . 1))),1,0]|,|[(- ((uv . 3) / (uv . 1))),0,1]|,|[(v `1),(v `2),(v `3)]|}| = ((((uv . 1) / (uv . 1)) * (v `1)) - ((- ((uv . 2) / (uv . 1))) * (v `2))) - ((v `3) * (- ((uv . 3) / (uv . 1)))) by A12, Th2
.= (1 / (uv . 1)) * ((((uv . 1) * (v `1)) + ((uv . 2) * (v `2))) + ((uv . 3) * (v `3)))
.= 0 by A8 ;
then |{(dir1a P99),(dir1b P99),v}| = 0 by A13, EUCLID_5:3;
then Pdir1a P99, Pdir1b P99,Q9 are_collinear by A5, BKMODEL1:1;
hence Q in l1 ; :: thesis: ( P in l2 & Q in l2 )
thus ( P in l2 & Q in l2 ) by COLLSP:10; :: thesis: verum
end;
hence dual (dual l) = l by A1, A3, A6, A11, A2, COLLSP:20; :: thesis: verum
end;
suppose A14: not R is zero_proj2 ; :: thesis: dual (dual l) = l
then reconsider R = R as non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) ;
# R9 = R ;
then consider P99 being non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A15: R9 = P99 and
A16: dual R9 = dual2 P99 by Th39;
A17: (uv . 2) / (uv . 2) = 1 by A14, Th13, XCMPLX_1:60;
normalize_proj2 P99 = |[((uv . 1) / (uv . 2)),1,((uv . 3) / (uv . 2))]| by A15, Th14;
then A18: ( (normalize_proj2 P99) `1 = (uv . 1) / (uv . 2) & (normalize_proj2 P99) `3 = (uv . 3) / (uv . 2) ) by EUCLID_5:2;
reconsider l1 = Line ((Pdir2a P99),(Pdir2b P99)) as LINE of real_projective_plane by Th24, COLLSP:def 7;
now :: thesis: ( P in l1 & Q in l1 & P in l2 & Q in l2 )
|{|[1,(- ((uv . 1) / (uv . 2))),0]|,|[0,(- ((uv . 3) / (uv . 2))),1]|,|[(u `1),(u `2),(u `3)]|}| = (((- ((uv . 3) / (uv . 2))) * (u `3)) + ((- ((uv . 1) / (uv . 2))) * (u `1))) - (u `2) by Th3
.= - (((((uv . 3) / (uv . 2)) * (u `3)) + (((uv . 1) / (uv . 2)) * (u `1))) + (((uv . 2) / (uv . 2)) * (u `2))) by A17
.= - ((1 / (uv . 2)) * ((((uv . 1) * (u `1)) + ((uv . 2) * (u `2))) + ((uv . 3) * (u `3))))
.= 0 by A7 ;
then |{(dir2a P99),(dir2b P99),u}| = 0 by A18, EUCLID_5:3;
then Pdir2a P99, Pdir2b P99,P9 are_collinear by A4, BKMODEL1:1;
hence P in l1 ; :: thesis: ( Q in l1 & P in l2 & Q in l2 )
|{|[1,(- ((uv . 1) / (uv . 2))),0]|,|[0,(- ((uv . 3) / (uv . 2))),1]|,|[(v `1),(v `2),(v `3)]|}| = (((- ((uv . 3) / (uv . 2))) * (v `3)) + ((- ((uv . 1) / (uv . 2))) * (v `1))) - (v `2) by Th3
.= - (((((uv . 3) / (uv . 2)) * (v `3)) + (((uv . 1) / (uv . 2)) * (v `1))) + (((uv . 2) / (uv . 2)) * (v `2))) by A17
.= - ((1 / (uv . 2)) * ((((uv . 1) * (v `1)) + ((uv . 2) * (v `2))) + ((uv . 3) * (v `3))))
.= 0 by A8 ;
then |{(dir2a P99),(dir2b P99),v}| = 0 by A18, EUCLID_5:3;
then Pdir2a P99, Pdir2b P99,Q9 are_collinear by A5, BKMODEL1:1;
hence Q in l1 ; :: thesis: ( P in l2 & Q in l2 )
thus ( P in l2 & Q in l2 ) by COLLSP:10; :: thesis: verum
end;
hence dual (dual l) = l by A3, A6, A16, A2, A1, COLLSP:20; :: thesis: verum
end;
suppose A19: not R is zero_proj3 ; :: thesis: dual (dual l) = l
then reconsider R = R as non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) ;
# R9 = R ;
then consider P99 being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)) such that
A20: R9 = P99 and
A21: dual R9 = dual3 P99 by Th40;
A22: (uv . 3) / (uv . 3) = 1 by A19, Th16, XCMPLX_1:60;
normalize_proj3 P99 = |[((uv . 1) / (uv . 3)),((uv . 2) / (uv . 3)),1]| by A20, Th17;
then A23: ( (normalize_proj3 P99) `1 = (uv . 1) / (uv . 3) & (normalize_proj3 P99) `2 = (uv . 2) / (uv . 3) ) by EUCLID_5:2;
reconsider l1 = Line ((Pdir3a P99),(Pdir3b P99)) as LINE of real_projective_plane by Th28, COLLSP:def 7;
now :: thesis: ( P in l1 & Q in l1 & P in l2 & Q in l2 )
|{|[1,0,(- ((uv . 1) / (uv . 3)))]|,|[0,1,(- ((uv . 2) / (uv . 3)))]|,|[(u `1),(u `2),(u `3)]|}| = ((u `3) - ((u `1) * (- ((uv . 1) / (uv . 3))))) - ((u `2) * (- ((uv . 2) / (uv . 3)))) by Th4
.= (((u `1) * ((uv . 1) / (uv . 3))) + ((u `2) * ((uv . 2) / (uv . 3)))) + ((u `3) * ((uv . 3) / (uv . 3))) by A22
.= (1 / (uv . 3)) * ((((uv . 1) * (u `1)) + ((uv . 2) * (u `2))) + ((uv . 3) * (u `3)))
.= 0 by A7 ;
then |{(dir3a P99),(dir3b P99),u}| = 0 by A23, EUCLID_5:3;
then Pdir3a P99, Pdir3b P99,P9 are_collinear by A4, BKMODEL1:1;
hence P in l1 ; :: thesis: ( Q in l1 & P in l2 & Q in l2 )
|{|[1,0,(- ((uv . 1) / (uv . 3)))]|,|[0,1,(- ((uv . 2) / (uv . 3)))]|,|[(v `1),(v `2),(v `3)]|}| = ((v `3) - ((v `1) * (- ((uv . 1) / (uv . 3))))) - ((v `2) * (- ((uv . 2) / (uv . 3)))) by Th4
.= (((v `1) * ((uv . 1) / (uv . 3))) + ((v `2) * ((uv . 2) / (uv . 3)))) + ((v `3) * ((uv . 3) / (uv . 3))) by A22
.= (1 / (uv . 3)) * ((((uv . 1) * (v `1)) + ((uv . 2) * (v `2))) + ((uv . 3) * (v `3)))
.= 0 by A8 ;
then |{(dir3a P99),(dir3b P99),v}| = 0 by A23, EUCLID_5:3;
then Pdir3a P99, Pdir3b P99,Q9 are_collinear by A5, BKMODEL1:1;
hence Q in l1 ; :: thesis: ( P in l2 & Q in l2 )
thus ( P in l2 & Q in l2 ) by COLLSP:10; :: thesis: verum
end;
hence dual (dual l) = l by A3, A6, A21, A2, A1, COLLSP:20; :: thesis: verum
end;
end;