set S = CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #);
A1:
now for a, b being Complex
for v, u, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds
( v + w = w + v & (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )let a,
b be
Complex;
for v, u, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds
( v + w = w + v & (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )let v,
u,
w be
VECTOR of
CLSStruct(#
(C_LinComb V),
(@ (ZeroCLC V)),
(C_LCAdd V),
(C_LCMult V) #);
( v + w = w + v & (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )reconsider a1 =
a,
b1 =
b as
Element of
COMPLEX by XCMPLX_0:def 2;
reconsider x =
v,
y =
u,
z =
w,
yx =
u + v,
xz =
v + w,
ax =
a1 * v,
az =
a1 * w,
bx =
b1 * v as
Element of
C_LinComb V ;
A2:
(
@ z = w &
@ yx = u + v )
;
A3:
(
@ xz = v + w &
@ ax = a * v )
;
A4:
(
@ az = a * w &
@ bx = b * v )
;
(
@ x = v &
@ y = u )
;
then reconsider K =
v,
L =
u,
M =
w,
LK =
u + v,
KM =
v + w,
aK =
a * v,
aM =
a * w,
bK =
b * v as
C_Linear_Combination of
V by A2, A3, A4;
hence v + w =
K + M
.=
w + v
by A5
;
( (u + v) + w = u + (v + w) & v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )thus (u + v) + w =
LK + M
by A5
.=
(L + K) + M
by A5
.=
L + (K + M)
by Th22
.=
L + KM
by A5
.=
u + (v + w)
by A5
;
( v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) = v & ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )thus v + (0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #)) =
K + (ZeroCLC V)
by A5
.=
v
by Th23
;
( ex w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) st v + w = 0. CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) & a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )
- K in the
carrier of
CLSStruct(#
(C_LinComb V),
(@ (ZeroCLC V)),
(C_LCAdd V),
(C_LCMult V) #)
by Def12;
then
- K in CLSStruct(#
(C_LinComb V),
(@ (ZeroCLC V)),
(C_LCAdd V),
(C_LCMult V) #)
;
then
- K = vector (
CLSStruct(#
(C_LinComb V),
(@ (ZeroCLC V)),
(C_LCAdd V),
(C_LCMult V) #),
(- K))
by RLVECT_2:def 1;
then v + (vector (CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #),(- K))) =
K - K
by A5
.=
0. CLSStruct(#
(C_LinComb V),
(@ (ZeroCLC V)),
(C_LCAdd V),
(C_LCMult V) #)
by Th37
;
hence
ex
w being
VECTOR of
CLSStruct(#
(C_LinComb V),
(@ (ZeroCLC V)),
(C_LCAdd V),
(C_LCMult V) #) st
v + w = 0. CLSStruct(#
(C_LinComb V),
(@ (ZeroCLC V)),
(C_LCAdd V),
(C_LCMult V) #)
;
( a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )hence a * (v + w) =
a1 * KM
.=
a1 * (K + M)
by A5
.=
(a1 * K) + (a1 * M)
by Th28
.=
aK + (a1 * M)
by A7
.=
aK + aM
by A7
.=
(a * v) + (a * w)
by A5
;
( (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & 1r * v = v )thus (a + b) * v =
(a1 + b1) * K
by A7
.=
(a1 * K) + (b1 * K)
by Th27
.=
aK + (b * K)
by A7
.=
aK + bK
by A7
.=
(a * v) + (b * v)
by A5
;
( (a * b) * v = a * (b * v) & 1r * v = v )thus (a * b) * v =
(a * b) * K
by A7
.=
a1 * (b1 * K)
by Th29
.=
a * bK
by A7
.=
a * (b * v)
by A7
;
1r * v = vthus 1r * v =
1r * K
by A7
.=
v
by Th30
;
verum end;
A8:
for v being Element of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds v is right_complementable
by A1;
for u, v, w being VECTOR of CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) holds (u + v) + w = u + (v + w)
by A1;
hence
CLSStruct(# (C_LinComb V),(@ (ZeroCLC V)),(C_LCAdd V),(C_LCMult V) #) is ComplexLinearSpace
by A1, A8, ALGSTR_0:def 16, CLVECT_1:def 2, CLVECT_1:def 3, CLVECT_1:def 4, CLVECT_1:def 5, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4; verum