let V be VectSp of F_Complex ; :: thesis: for l being linear-Functional of V holds projIm l is linear-Functional of (RealVS V)
let l be linear-Functional of V; :: thesis: projIm l is linear-Functional of (RealVS V)
A1: projIm l is homogeneous

proof

let x be VECTOR of (RealVS V); :: according to HAHNBAN:def 3 :: thesis: for b₁ being object holds (projIm l) . (b₁ * x) = b₁ * ((projIm l) . x)
let r be Real; :: thesis: (projIm l) . (r * x) = r * ((projIm l) . x)
addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x as Vector of V ;
r * x = [**r,0**] * x1 by Def17;
hence (projIm l) . (r * x) = Im (l . ([**r,0**] * x1)) by Def19
.= Im ([**r,0**] * (l . x1)) by Def8
.= ((Re [**r,0**]) * (Im (l . x1))) + ((Re (l . x1)) * (Im [**r,0**])) by COMPLEX1:9
.= ((Re [**r,0**]) * (Im (l . x1))) + ((Re (l . x1)) * 0) by COMPLEX1:12
.= r * (Im (l . x1)) by COMPLEX1:12
.= r * ((projIm l) . x) by Def19 ;
:: thesis: verum

end;

projIm l is additive

proof

let x, y be VECTOR of (RealVS V); :: according to HAHNBAN:def 2 :: thesis: (projIm l) . (x + y) = ((projIm l) . x) + ((projIm l) . y)
A2: addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) = addLoopStr(# the carrier of (RealVS V), the addF of (RealVS V), the ZeroF of (RealVS V) #) by Def17;
then reconsider x1 = x, y1 = y as Vector of V ;
thus (projIm l) . (x + y) = Im (l . (x1 + y1)) by A2, Def19
.= Im ((l . x1) + (l . y1)) by VECTSP_1:def 20
.= (Im (l . x1)) + (Im (l . y1)) by COMPLEX1:8
.= (Im (l . x1)) + ((projIm l) . y) by Def19
.= ((projIm l) . x) + ((projIm l) . y) by Def19 ; :: thesis: verum

end;

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