let P be non zero_proj1 Element of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for u being non zero Element of (TOP-REAL 3) st u = normalize_proj1 P holds
|{(dir1a P),(dir1b P),(normalize_proj1 P)}| = (1 + ((u . 2) * (u . 2))) + ((u . 3) * (u . 3))
let u be non zero Element of (TOP-REAL 3); :: thesis: ( u = normalize_proj1 P implies |{(dir1a P),(dir1b P),(normalize_proj1 P)}| = (1 + ((u . 2) * (u . 2))) + ((u . 3) * (u . 3)) )
assume A1: u = normalize_proj1 P ; :: thesis: |{(dir1a P),(dir1b P),(normalize_proj1 P)}| = (1 + ((u . 2) * (u . 2))) + ((u . 3) * (u . 3))
then A2: u . 1 = 1 by Def2;
reconsider un = u as Element of REAL 3 by EUCLID:22;
thus |{(dir1a P),(dir1b P),(normalize_proj1 P)}| = |(un,un)| by A1, Th21
.= (((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) + ((u . 3) * (u . 3)) by EUCLID_8:63
.= (1 + ((u . 2) * (u . 2))) + ((u . 3) * (u . 3)) by A2 ; :: thesis: verum