let V be non empty VectSp of F_Complex ; :: thesis: for l being linear-Functional of V holds projRe l is linear-Functional of (RealVS V)
let l be linear-Functional of V; :: thesis: projRe l is linear-Functional of (RealVS V)
A1: projRe l is additive

proof

let x, y be VECTOR of (RealVS V); :: according to HAHNBAN:def 4 :: thesis: (projRe l) . (x + y) = ((projRe l) . x) + ((projRe l) . y)
A2: addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #) by Def22;
then reconsider x1 = x, y1 = y as Vector of V ;
thus (projRe l) . (x + y) = Re (l . (x1 + y1)) by A2, Def23
.= Re ((l . x1) + (l . y1)) by Def11
.= (Re (l . x1)) + (Re (l . y1)) by COMPLEX1:19
.= (Re (l . x1)) + ((projRe l) . y) by Def23
.= ((projRe l) . x) + ((projRe l) . y) by Def23 ; :: thesis: verum

end;

projRe l is homogeneous

proof

let x be VECTOR of (RealVS V); :: according to HAHNBAN:def 5 :: thesis: for b₁ being Element of REAL holds (projRe l) . (b₁ * x) = b₁ * ((projRe l) . x)
let r be Real; :: thesis: (projRe l) . (r * x) = r * ((projRe l) . x)
addLoopStr(# the carrier of V,the addF of V,the U2 of V #) = addLoopStr(# the carrier of (RealVS V),the addF of (RealVS V),the U2 of (RealVS V) #) by Def22;
then reconsider x1 = x as Vector of V ;
r * x = [**r,0 **] * x1 by Def22;
hence (projRe l) . (r * x) = Re (l . ([**r,0 **] * x1)) by Def23
.= Re ([**r,0 **] * (l . x1)) by Def12
.= ((Re [**r,0 **]) * (Re (l . x1))) - ((Im [**r,0 **]) * (Im (l . x1))) by COMPLEX1:24
.= ((Re [**r,0 **]) * (Re (l . x1))) - (0 * (Im (l . x1))) by COMPLEX1:28
.= r * (Re (l . x1)) by COMPLEX1:28
.= r * ((projRe l) . x) by Def23 ;
:: thesis: verum

end;

hence projRe l is linear-Functional of (RealVS V) by A1; :: thesis: verum