let P be non zero_proj2 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_proj2 P holds
|{(dir2a P),(dir2b 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_proj2 P holds
|{(dir2a P),(dir2b P),v}| = - |(u,v)|
let v be Element of (TOP-REAL 3); :: thesis: ( u = normalize_proj2 P implies |{(dir2a P),(dir2b P),v}| = - |(u,v)| )
assume u = normalize_proj2 P ; :: thesis: |{(dir2a P),(dir2b P),v}| = - |(u,v)|
then A1: ( u . 2 = 1 & P = Dir u ) by Def4;
then normalize_proj2 P = |[((u . 1) / (u . 2)),1,((u . 3) / (u . 2))]| by Th14;
then ( (normalize_proj2 P) `1 = (u . 1) / (u . 2) & (normalize_proj2 P) `3 = (u . 3) / (u . 2) ) by EUCLID_5:2;
then |{(dir2a P),(dir2b P),v}| = |{|[1,(- ((u . 1) / (u . 2))),0]|,|[0,(- ((u . 3) / (u . 2))),1]|,|[(v `1),(v `2),(v `3)]|}| by EUCLID_5:3
.= (((- ((u . 3) / (u . 2))) * (v `3)) + ((- ((u . 1) / (u . 2))) * (v `1))) - (v `2) by Th3
.= - ((1 / (u . 2)) * ((((u `1) * (v `1)) + ((u `2) * (v `2))) + ((u `3) * (v `3)))) by A1
.= - ((1 / (u . 2)) * |(u,v)|) by EUCLID_5:29 ;
hence |{(dir2a P),(dir2b P),v}| = - |(u,v)| by A1; :: thesis: verum