let V be VectSp of F_Complex ; for l being linear-Functional of (RealVS V) holds prodReIm l is linear-Functional of V
let l be linear-Functional of (RealVS V); prodReIm l is linear-Functional of V
A1:
prodReIm l is homogeneous
proof
let x be
Vector of
V;
HAHNBAN1:def 8 for r being Scalar of holds (prodReIm l) . (r * x) = r * ((prodReIm l) . x)let r be
Scalar of ;
(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, VECTSP_1:def 17
.=
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
;
verum
end;
prodReIm l is additive
proof
let x,
y be
Vector of
V;
VECTSP_1:def 19 (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
;
verum
end;
hence
prodReIm l is linear-Functional of V
by A1; verum