let P be non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
normalize_proj3 P = |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]|
let u9 be non zero Element of (TOP-REAL 3); :: thesis: ( P = Dir u9 implies normalize_proj3 P = |[((u9 . 1) / (u9 . 3)),((u9 . 2) / (u9 . 3)),1]| )
assume P = Dir u9 ; :: thesis: normalize_proj3 P = |[((u9 . 1) / (u9 . 3)),((u9 . 2) / (u9 . 3)),1]|
then Dir u9 = Dir (normalize_proj3 P) by Def6;
then are_Prop u9, normalize_proj3 P by ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A1: normalize_proj3 P = a * u9 by ANPROJ_1:1;
A2: normalize_proj3 P = |[(a * (u9 `1)),(a * (u9 `2)),(a * (u9 `3))]| by A1, EUCLID_5:7;
A3: 1 = (normalize_proj3 P) `3 by Def6
.= a * (u9 `3) by A2 ;
then A4: ( u9 `3 = 1 / a & a = 1 / (u9 `3) ) by XCMPLX_1:73;
normalize_proj3 P = |[((u9 `1) / (u9 `3)),((1 / (u9 `3)) * (u9 `2)),1]| by A1, A3, A4, EUCLID_5:7
.= |[((u9 . 1) / (u9 . 3)),((u9 . 2) / (u9 . 3)),1]| ;
hence normalize_proj3 P = |[((u9 . 1) / (u9 . 3)),((u9 . 2) / (u9 . 3)),1]| ; :: thesis: verum