let V be 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 homogeneous

proof

let x be Vector of V; :: according to HAHNBAN1:def 8 :: 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:13;
A3: - (1_ F_Complex) = [**(- 1),0**] by COMPLFLD:2, COMPLFLD:8;
x = (i_FC * (i_FC * (- (1_ F_Complex)))) * x by Th3, Th4
.= i_FC * (((- (1_ F_Complex)) * i_FC) * x) by VECTSP_1:def 16 ;
then A4: ((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))))
.= (- ((RtoC l) . ([**(Re r1),0**] * (i_FC * x)))) + (- ((- (Im r1)) * ((RtoC l) . (i_FC * (((- (1_ F_Complex)) * i_FC) * x))))) by Def13
.= (- ((RtoC l) . ([**(Re r1),0**] * (i_FC * x)))) + (- ((RtoC l) . ([**0,(- (Im r1))**] * (((- (1_ F_Complex)) * i_FC) * x)))) by Th19
.= (- ((RtoC l) . ([**(Re r1),0**] * (i_FC * x)))) + (- ((RtoC l) . ([**0,(- (Im r1))**] * ((- (1_ F_Complex)) * (i_FC * x))))) by VECTSP_1:def 16
.= (- ((RtoC l) . ([**(Re r1),0**] * (i_FC * x)))) + (- ((RtoC l) . (([**0,(- (Im r1))**] * (- (1_ F_Complex))) * (i_FC * x)))) by VECTSP_1:def 16
.= - (((RtoC l) . ([**(Re r1),0**] * (i_FC * x))) + ((RtoC l) . ([**0,(Im r1)**] * (i_FC * x)))) by A3
.= - ((RtoC l) . (([**(Re r1),0**] * (i_FC * x)) + ([**0,(Im r1)**] * (i_FC * x)))) by Def12
.= - ((RtoC l) . (([**(Re r1),0**] + [**0,(Im r1)**]) * (i_FC * x))) by VECTSP_1:def 15
.= - ((RtoC l) . ((i_FC * r) * x)) by A2, VECTSP_1:def 16 ;
A5: ((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 Def13
.= ((RtoC l) . ([**(Re r1),0**] * x)) + ((RtoC l) . ([**0,(Im r1)**] * x)) by Th19
.= (RtoC l) . (([**(Re r1),0**] * x) + ([**0,(Im r1)**] * x)) by Def12
.= (RtoC l) . (([**(Re r1),0**] + [**0,(Im r1)**]) * x) by VECTSP_1:def 15
.= (RtoC l) . (r * x) by COMPLEX1:13 ;
thus (prodReIm l) . (r * x) = [**((RtoC l) . (r * x)),(- ((i-shift (RtoC l)) . (r * x)))**] by Def23
.= [**((RtoC l) . (r * x)),(- ((RtoC l) . (i_FC * (r * x))))**] by Def22
.= ((RtoC l) . (r * x)) + ((((Re r1) * (- ((RtoC l) . (i_FC * x)))) + (((RtoC l) . x) * (Im r1))) * <i>) by A4, VECTSP_1:def 16
.= r * [**((RtoC l) . x),(- ((RtoC l) . (i_FC * x)))**] by A2, A5
.= r * [**((RtoC l) . x),(- ((i-shift (RtoC l)) . x))**] by Def22
.= r * ((prodReIm l) . x) by Def23 ; :: thesis: verum

end;

prodReIm l is additive

proof

let x, y be Vector of V; :: according to VECTSP_1:def 19 :: 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 Def23
.= [**((RtoC l) . (x + y)),(- ((RtoC l) . (i_FC * (x + y))))**] by Def22
.= [**(((RtoC l) . x) + ((RtoC l) . y)),(- ((RtoC l) . (i_FC * (x + y))))**] by Def12
.= [**(((RtoC l) . x) + ((RtoC l) . y)),(- ((RtoC l) . ((i_FC * x) + (i_FC * y))))**] by VECTSP_1:def 14
.= [**(((RtoC l) . x) + ((RtoC l) . y)),(- (((RtoC l) . (i_FC * x)) + ((RtoC l) . (i_FC * y))))**] by Def12
.= [**((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 Def22
.= [**((RtoC l) . x),(- ((i-shift (RtoC l)) . x))**] + [**((RtoC l) . y),(- ((i-shift (RtoC l)) . y))**] by Def22
.= ((prodReIm l) . x) + [**((RtoC l) . y),(- ((i-shift (RtoC l)) . y))**] by Def23
.= ((prodReIm l) . x) + ((prodReIm l) . y) by Def23 ; :: thesis: verum

end;

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