let P be non zero_proj1 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_proj1 P = ((u . 2) / (u . 1)) * (normalize_proj2 P) & normalize_proj2 P = ((u . 1) / (u . 2)) * (normalize_proj1 P) )
let u be non zero Element of (TOP-REAL 3); :: thesis: ( P = Dir u implies ( normalize_proj1 P = ((u . 2) / (u . 1)) * (normalize_proj2 P) & normalize_proj2 P = ((u . 1) / (u . 2)) * (normalize_proj1 P) ) )
assume A1: P = Dir u ; :: thesis: ( normalize_proj1 P = ((u . 2) / (u . 1)) * (normalize_proj2 P) & normalize_proj2 P = ((u . 1) / (u . 2)) * (normalize_proj1 P) )
set r = (u . 1) / (u . 2);
A2: ( u . 1 <> 0 & u . 2 <> 0 ) by A1, Th10, Th13;
A3: ((u . 1) / (u . 2)) * ((u . 2) / (u . 1)) = ((u . 1) / (u . 2)) * (1 / ((u . 1) / (u . 2))) by XCMPLX_1:57
.= 1 by A2, XCMPLX_1:106 ;
( Dir (normalize_proj1 P) = P & Dir (normalize_proj2 P) = P ) by Def2, Def4;
then are_Prop normalize_proj1 P, normalize_proj2 P by ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A4: normalize_proj1 P = a * (normalize_proj2 P) by ANPROJ_1:1;
( normalize_proj1 P = |[1,((u . 2) / (u . 1)),((u . 3) / (u . 1))]| & normalize_proj2 P = |[((u . 1) / (u . 2)),1,((u . 3) / (u . 2))]| ) by A1, Th11, Th14;
then A5: |[1,((u . 2) / (u . 1)),((u . 3) / (u . 1))]| = |[(a * ((u . 1) / (u . 2))),(a * 1),(a * ((u . 3) / (u . 2)))]| by A4, EUCLID_5:8;
hence normalize_proj1 P = ((u . 2) / (u . 1)) * (normalize_proj2 P) by A4, FINSEQ_1:78; :: thesis: normalize_proj2 P = ((u . 1) / (u . 2)) * (normalize_proj1 P)
((u . 1) / (u . 2)) * (normalize_proj1 P) = ((u . 1) / (u . 2)) * (((u . 2) / (u . 1)) * (normalize_proj2 P)) by A4, A5, FINSEQ_1:78
.= (((u . 1) / (u . 2)) * ((u . 2) / (u . 1))) * (normalize_proj2 P) by RVSUM_1:49
.= normalize_proj2 P by A3, RVSUM_1:52 ;
hence normalize_proj2 P = ((u . 1) / (u . 2)) * (normalize_proj1 P) ; :: thesis: verum