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

proof

let x, y be Vector of V; :: according to HAHNBAN1:def 11 :: thesis: (prodReIm l) . (x + y) = ((prodReIm l) . x) + ((prodReIm l) . y)
thus (prodReIm l) . (x + y) = [**((RtoC l) . (x + y)),(- ((i-shift (RtoC l)) . (x + y)))**] by Def28
.= [**((RtoC l) . (x + y)),(- ((RtoC l) . (i_FC * (x + y))))**] by Def27
.= [**(((RtoC l) . x) + ((RtoC l) . y)),(- ((RtoC l) . (i_FC * (x + y))))**] by Def17
.= [**(((RtoC l) . x) + ((RtoC l) . y)),(- ((RtoC l) . ((i_FC * x) + (i_FC * y))))**] by VECTSP_1:def 26
.= [**(((RtoC l) . x) + ((RtoC l) . y)),(- (((RtoC l) . (i_FC * x)) + ((RtoC l) . (i_FC * y))))**] by Def17
.= [**((RtoC l) . x),(- ((RtoC l) . (i_FC * x)))**] + [**((RtoC l) . y),(- ((RtoC l) . (i_FC * y)))**]
.= [**((RtoC l) . x),(- ((i-shift (RtoC l)) . x))**] + [**((RtoC l) . y),(- ((RtoC l) . (i_FC * y)))**] by Def27
.= [**((RtoC l) . x),(- ((i-shift (RtoC l)) . x))**] + [**((RtoC l) . y),(- ((i-shift (RtoC l)) . y))**] by Def27
.= ((prodReIm l) . x) + [**((RtoC l) . y),(- ((i-shift (RtoC l)) . y))**] by Def28
.= ((prodReIm l) . x) + ((prodReIm l) . y) by Def28 ; :: thesis: verum

end;

prodReIm l is homogeneous

proof

let x be Vector of V; :: according to HAHNBAN1:def 12 :: thesis: for r being Scalar of holds (prodReIm l) . (r * x) = r * ((prodReIm l) . x)
let r be Scalar of ; :: thesis: (prodReIm l) . (r * x) = r * ((prodReIm l) . x)
reconsider r1 = r as Element of COMPLEX by COMPLFLD:def 1;
set a = Re r1;
set b = Im r1;
A2: r1 = (Re r1) + ((Im r1) * <i> ) by COMPLEX1:29;
A3: ((Re r1) * ((RtoC l) . x)) - ((Im r1) * (- ((RtoC l) . (i_FC * x)))) = ((Re r1) * ((RtoC l) . x)) + ((Im r1) * ((RtoC l) . (i_FC * x)))
.= ((RtoC l) . ([**(Re r1),0 **] * x)) + ((Im r1) * ((RtoC l) . (i_FC * x))) by Def18
.= ((RtoC l) . ([**(Re r1),0 **] * x)) + ((RtoC l) . ([**0 ,(Im r1)**] * x)) by Th29
.= (RtoC l) . (([**(Re r1),0 **] * x) + ([**0 ,(Im r1)**] * x)) by Def17
.= (RtoC l) . (([**(Re r1),0 **] + [**0 ,(Im r1)**]) * x) by VECTSP_1:def 26
.= (RtoC l) . (r * x) by COMPLEX1:29 ;
A4: x = (i_FC * (i_FC * (- (1_ F_Complex )))) * x by Th8, Th9, VECTSP_1:def 26
.= i_FC * (((- (1_ F_Complex )) * i_FC ) * x) by VECTSP_1:def 26 ;
A5: - (1_ F_Complex ) = [**(- 1),0 **] by COMPLFLD:4, COMPLFLD:10;
A6: ((Re r1) * (- ((RtoC l) . (i_FC * x)))) + (((RtoC l) . x) * (Im r1)) = (- ((Re r1) * ((RtoC l) . (i_FC * x)))) + ((Im r1) * ((RtoC l) . (i_FC * (((- (1_ F_Complex )) * i_FC ) * x)))) by A4
.= (- ((RtoC l) . ([**(Re r1),0 **] * (i_FC * x)))) + (- ((- (Im r1)) * ((RtoC l) . (i_FC * (((- (1_ F_Complex )) * i_FC ) * x))))) by Def18
.= (- ((RtoC l) . ([**(Re r1),0 **] * (i_FC * x)))) + (- ((RtoC l) . ([**0 ,(- (Im r1))**] * (((- (1_ F_Complex )) * i_FC ) * x)))) by Th29
.= (- ((RtoC l) . ([**(Re r1),0 **] * (i_FC * x)))) + (- ((RtoC l) . ([**0 ,(- (Im r1))**] * ((- (1_ F_Complex )) * (i_FC * x))))) by VECTSP_1:def 26
.= (- ((RtoC l) . ([**(Re r1),0 **] * (i_FC * x)))) + (- ((RtoC l) . (([**0 ,(- (Im r1))**] * (- (1_ F_Complex ))) * (i_FC * x)))) by VECTSP_1:def 26
.= - (((RtoC l) . ([**(Re r1),0 **] * (i_FC * x))) + ((RtoC l) . ([**0 ,(Im r1)**] * (i_FC * x)))) by A5
.= - ((RtoC l) . (([**(Re r1),0 **] * (i_FC * x)) + ([**0 ,(Im r1)**] * (i_FC * x)))) by Def17
.= - ((RtoC l) . (([**(Re r1),0 **] + [**0 ,(Im r1)**]) * (i_FC * x))) by VECTSP_1:def 26
.= - ((RtoC l) . ((i_FC * r) * x)) by A2, VECTSP_1:def 26 ;
thus (prodReIm l) . (r * x) = [**((RtoC l) . (r * x)),(- ((i-shift (RtoC l)) . (r * x)))**] by Def28
.= [**((RtoC l) . (r * x)),(- ((RtoC l) . (i_FC * (r * x))))**] by Def27
.= ((RtoC l) . (r * x)) + ((((Re r1) * (- ((RtoC l) . (i_FC * x)))) + (((RtoC l) . x) * (Im r1))) * <i> ) by A6, VECTSP_1:def 26
.= r * [**((RtoC l) . x),(- ((RtoC l) . (i_FC * x)))**] by A2, A3
.= r * [**((RtoC l) . x),(- ((i-shift (RtoC l)) . x))**] by Def27
.= r * ((prodReIm l) . x) by Def28 ; :: thesis: verum

end;

hence prodReIm l is linear-Functional of V by A1; :: thesis: verum