let P be non zero_proj2 Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u being non zero Element of (TOP-REAL 3) st u = normalize_proj2 P holds
|{(dir2a P),(dir2b P),(normalize_proj2 P)}| = - ((((u . 1) * (u . 1)) + 1) + ((u . 3) * (u . 3)))
let u be non zero Element of (TOP-REAL 3); :: thesis: ( u = normalize_proj2 P implies |{(dir2a P),(dir2b P),(normalize_proj2 P)}| = - ((((u . 1) * (u . 1)) + 1) + ((u . 3) * (u . 3))) )
assume A1: u = normalize_proj2 P ; :: thesis: |{(dir2a P),(dir2b P),(normalize_proj2 P)}| = - ((((u . 1) * (u . 1)) + 1) + ((u . 3) * (u . 3)))
then A2: u . 2 = 1 by Def4;
reconsider un = u as Element of REAL 3 by EUCLID:22;
thus |{(dir2a P),(dir2b P),(normalize_proj2 P)}| = - |(un,un)| by A1, Th25
.= - ((((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) + ((u . 3) * (u . 3))) by EUCLID_8:63
.= - ((((u . 1) * (u . 1)) + 1) + ((u . 3) * (u . 3))) by A2 ; :: thesis: verum