let P, Q be non point_at_infty Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( P in absolute & Q in absolute implies RP3_to_T2 Dir001, RP3_to_T2 P equiv RP3_to_T2 Dir001, RP3_to_T2 Q )
assume that
A1: P in absolute and
A2: Q in absolute ; :: thesis: RP3_to_T2 Dir001, RP3_to_T2 P equiv RP3_to_T2 Dir001, RP3_to_T2 Q
reconsider p = RP3_to_T2 P, q = RP3_to_T2 Q, r = RP3_to_T2 Dir001 as Element of TarskiEuclid2Space ;
consider u being non zero Element of (TOP-REAL 3) such that
A3: ( P = Dir u & u `3 = 1 & RP3_to_REAL2 P = |[(u `1),(u `2)]| ) by Def05;
consider v being non zero Element of (TOP-REAL 3) such that
A4: ( Q = Dir v & v `3 = 1 & RP3_to_REAL2 Q = |[(v `1),(v `2)]| ) by Def05;
consider w being non zero Element of (TOP-REAL 3) such that
A5: ( Dir001 = Dir w & w `3 = 1 & RP3_to_REAL2 Dir001 = |[(w `1),(w `2)]| ) by Def05;
are_Prop |[0,0,1]|,w by A5, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A6: w = a * |[0,0,1]| by ANPROJ_1:1;
w = |[(a * 0),(a * 0),(a * 1)]| by A6, EUCLID_5:8;
then A8: ( w `1 = 0 & w `2 = 0 ) by EUCLID_5:2;
reconsider u1 = u `1 , u2 = u `2 , v1 = v `1 , v2 = v `2 , w1 = w `1 , w2 = w `2 as Real ;

now :: thesis: ( dist ((RP3_to_T2 Dir001),(RP3_to_T2 P)) = dist ((RP3_to_T2 Dir001),(RP3_to_T2 Q)) & dist ((RP3_to_T2 Dir001),(RP3_to_T2 P)) = |.((Tn2TR (RP3_to_T2 Dir001)) - (Tn2TR (RP3_to_T2 P))).| & dist ((RP3_to_T2 Dir001),(RP3_to_T2 Q)) = |.((Tn2TR (RP3_to_T2 Dir001)) - (Tn2TR (RP3_to_T2 Q))).| )

A9: ( (Tn2TR (RP3_to_T2 P)) `1 = u `1 & (Tn2TR (RP3_to_T2 P)) `2 = u `2 & (Tn2TR (RP3_to_T2 Q)) `1 = v `1 & (Tn2TR (RP3_to_T2 Q)) `2 = v `2 & (Tn2TR (RP3_to_T2 Dir001)) `1 = w `1 & (Tn2TR (RP3_to_T2 Dir001)) `2 = w `2 ) by A3, A4, A5, EUCLID:52;
reconsider uP = |[(u `1),(u `2),1]| as non zero Element of (TOP-REAL 3) ;

now :: thesis: ( P in absolute & P = Dir uP & uP . 3 = 1 )

thus P in absolute by A1; :: thesis: ( P = Dir uP & uP . 3 = 1 )
thus P = Dir uP by A3, EUCLID_5:3; :: thesis: uP . 3 = 1
uP `3 = 1 by EUCLID_5:2;
hence uP . 3 = 1 by EUCLID_5:def 3; :: thesis: verum

end;

then |[(uP . 1),(uP . 2)]| in circle (0,0,1) by BKMODEL1:84;
then ((uP . 1) ^2) + ((uP . 2) ^2) = 1 by BKMODEL1:13;
then ((uP `1) ^2) + ((uP . 2) ^2) = 1 by EUCLID_5:def 1;
then ((uP `1) ^2) + ((uP `2) ^2) = 1 by EUCLID_5:def 2;
then ((u `1) ^2) + ((uP `2) ^2) = 1 by EUCLID_5:2;
then A10: ((u `1) ^2) + ((u `2) ^2) = 1 by EUCLID_5:2;
reconsider vQ = |[(v `1),(v `2),1]| as non zero Element of (TOP-REAL 3) ;

now :: thesis: ( Q in absolute & Q = Dir vQ & vQ . 3 = 1 )

thus Q in absolute by A2; :: thesis: ( Q = Dir vQ & vQ . 3 = 1 )
thus Q = Dir vQ by A4, EUCLID_5:3; :: thesis: vQ . 3 = 1
vQ `3 = 1 by EUCLID_5:2;
hence vQ . 3 = 1 by EUCLID_5:def 3; :: thesis: verum

end;

then |[(vQ . 1),(vQ . 2)]| in circle (0,0,1) by BKMODEL1:84;
then ((vQ . 1) ^2) + ((vQ . 2) ^2) = 1 by BKMODEL1:13;
then ((vQ `1) ^2) + ((vQ . 2) ^2) = 1 by EUCLID_5:def 1;
then ((vQ `1) ^2) + ((vQ `2) ^2) = 1 by EUCLID_5:def 2;
then ((v `1) ^2) + ((vQ `2) ^2) = 1 by EUCLID_5:2;
then A11: ((v `1) ^2) + ((v `2) ^2) = 1 by EUCLID_5:2;

now :: thesis: ( dist ((RP3_to_T2 Dir001),(RP3_to_T2 P)) = 1 & dist ((RP3_to_T2 Dir001),(RP3_to_T2 Q)) = 1 )

thus dist ((RP3_to_T2 Dir001),(RP3_to_T2 P)) = sqrt (((0 - (u `1)) ^2) + ((0 - (u `2)) ^2)) by A9, A8, GTARSKI2:16
.= sqrt (((u `1) ^2) + ((- (u `2)) ^2)) by SQUARE_1:3
.= 1 by A10, SQUARE_1:3, SQUARE_1:18 ; :: thesis: dist ((RP3_to_T2 Dir001),(RP3_to_T2 Q)) = 1
thus dist ((RP3_to_T2 Dir001),(RP3_to_T2 Q)) = sqrt ((((w `1) - (v `1)) ^2) + (((w `2) - (v `2)) ^2)) by A9, GTARSKI2:16
.= sqrt (((v `1) ^2) + ((- (v `2)) ^2)) by A8, SQUARE_1:3
.= 1 by A11, SQUARE_1:3, SQUARE_1:18 ; :: thesis: verum

end;

hence dist ((RP3_to_T2 Dir001),(RP3_to_T2 P)) = dist ((RP3_to_T2 Dir001),(RP3_to_T2 Q)) ; :: thesis: ( dist ((RP3_to_T2 Dir001),(RP3_to_T2 P)) = |.((Tn2TR (RP3_to_T2 Dir001)) - (Tn2TR (RP3_to_T2 P))).| & dist ((RP3_to_T2 Dir001),(RP3_to_T2 Q)) = |.((Tn2TR (RP3_to_T2 Dir001)) - (Tn2TR (RP3_to_T2 Q))).| )
thus dist ((RP3_to_T2 Dir001),(RP3_to_T2 P)) = |.((Tn2TR (RP3_to_T2 Dir001)) - (Tn2TR (RP3_to_T2 P))).| by GTARSKI2:17; :: thesis: dist ((RP3_to_T2 Dir001),(RP3_to_T2 Q)) = |.((Tn2TR (RP3_to_T2 Dir001)) - (Tn2TR (RP3_to_T2 Q))).|
thus dist ((RP3_to_T2 Dir001),(RP3_to_T2 Q)) = |.((Tn2TR (RP3_to_T2 Dir001)) - (Tn2TR (RP3_to_T2 Q))).| by GTARSKI2:17; :: thesis: verum

end;

hence RP3_to_T2 Dir001, RP3_to_T2 P equiv RP3_to_T2 Dir001, RP3_to_T2 Q by GTARSKI2:18; :: thesis: verum