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