let P be non zero_proj1 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_proj1 P holds
|{(dir1a P),(dir1b 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_proj1 P holds
|{(dir1a P),(dir1b P),v}| = |(u,v)|
let v be Element of (TOP-REAL 3); :: thesis: ( u = normalize_proj1 P implies |{(dir1a P),(dir1b P),v}| = |(u,v)| )
assume u = normalize_proj1 P ; :: thesis: |{(dir1a P),(dir1b P),v}| = |(u,v)|
then A1: ( u . 1 = 1 & P = Dir u ) by Def2;
then normalize_proj1 P = |[1,((u . 2) / (u . 1)),((u . 3) / (u . 1))]| by Th11;
then ( (normalize_proj1 P) `2 = (u . 2) / (u . 1) & (normalize_proj1 P) `3 = (u . 3) / (u . 1) ) ;
then |{(dir1a P),(dir1b P),v}| = |{|[(- ((u . 2) / (u . 1))),1,0]|,|[(- ((u . 3) / (u . 1))),0,1]|,|[(v `1),(v `2),(v `3)]|}|
.= ((v `1) - ((- ((u . 2) / (u . 1))) * (v `2))) - ((v `3) * (- ((u . 3) / (u . 1)))) by Th2
.= (1 / (u . 1)) * ((((u `1) * (v `1)) + ((u `2) * (v `2))) + ((v `3) * (u `3))) by A1
.= (1 / (u . 1)) * |(u,v)| by EUCLID_5:29 ;
hence |{(dir1a P),(dir1b P),v}| = |(u,v)| by A1; :: thesis: verum