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