let P be non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u being non zero Element of (TOP-REAL 3) st u = normalize_proj3 P holds
|{(dir3a P),(dir3b P),(normalize_proj3 P)}| = (((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) + 1
let u be non zero Element of (TOP-REAL 3); :: thesis: ( u = normalize_proj3 P implies |{(dir3a P),(dir3b P),(normalize_proj3 P)}| = (((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) + 1 )
assume A1: u = normalize_proj3 P ; :: thesis: |{(dir3a P),(dir3b P),(normalize_proj3 P)}| = (((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) + 1
then A2: u . 3 = 1 by Def6;
reconsider un = u as Element of REAL 3 by EUCLID:22;
thus |{(dir3a P),(dir3b P),(normalize_proj3 P)}| = |(un,un)| by A1, Th29
.= (((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) + ((u . 3) * (u . 3)) by EUCLID_8:63
.= (((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) + 1 by A2 ; :: thesis: verum