let P be non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u being non zero Element of (TOP-REAL 3)
for v being Element of (TOP-REAL 3) st u = normalize_proj3 P holds
|{(dir3a P),(dir3b P),v}| = |(u,v)|
let u be non zero Element of (TOP-REAL 3); :: thesis: for v being Element of (TOP-REAL 3) st u = normalize_proj3 P holds
|{(dir3a P),(dir3b P),v}| = |(u,v)|
let v be Element of (TOP-REAL 3); :: thesis: ( u = normalize_proj3 P implies |{(dir3a P),(dir3b P),v}| = |(u,v)| )
assume u = normalize_proj3 P ; :: thesis: |{(dir3a P),(dir3b P),v}| = |(u,v)|
then A1: ( u . 3 = 1 & P = Dir u ) by Def6;
then normalize_proj3 P = |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]| by Th17;
then ( (normalize_proj3 P) `1 = (u . 1) / (u . 3) & (normalize_proj3 P) `2 = (u . 2) / (u . 3) ) ;
then |{(dir3a P),(dir3b P),v}| = |{|[1,0,(- ((u . 1) / (u . 3)))]|,|[0,1,(- ((u . 2) / (u . 3)))]|,|[(v `1),(v `2),(v `3)]|}|
.= ((v `3) - ((v `1) * (- ((u . 1) / (u . 3))))) - ((v `2) * (- ((u . 2) / (u . 3)))) by Th4
.= (((u `1) * (v `1)) + ((u `2) * (v `2))) + ((u `3) * (v `3)) by A1
.= |(u,v)| by EUCLID_5:29 ;
hence |{(dir3a P),(dir3b P),v}| = |(u,v)| ; :: thesis: verum