let V be ComplexLinearSpace; :: thesis: for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX ,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX ,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let V1 be Subset of V; :: thesis: for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX ,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX ,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let D be non empty set ; :: thesis: for d1 being Element of D
for A being BinOp of D
for M being Function of [:COMPLEX ,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX ,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let d1 be Element of D; :: thesis: for A being BinOp of D
for M being Function of [:COMPLEX ,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX ,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let A be BinOp of D; :: thesis: for M being Function of [:COMPLEX ,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX ,V1:] holds
CLSStruct(# D,d1,A,M #) is Subspace of V
let M be Function of [:COMPLEX ,D:],D; :: thesis: ( V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX ,V1:] implies CLSStruct(# D,d1,A,M #) is Subspace of V )
assume that
A1:
V1 = D
and
A2:
d1 = 0. V
and
A3:
A = the addF of V || V1
and
A4:
M = the Mult of V | [:COMPLEX ,V1:]
; :: thesis: CLSStruct(# D,d1,A,M #) is Subspace of V
set W = CLSStruct(# D,d1,A,M #);
A5:
0. CLSStruct(# D,d1,A,M #) = 0. V
by A2;
A6:
for x, y being VECTOR of CLSStruct(# D,d1,A,M #) holds x + y = the addF of V . [x,y]
by A1, A3, FUNCT_1:72;
( CLSStruct(# D,d1,A,M #) is Abelian & CLSStruct(# D,d1,A,M #) is add-associative & CLSStruct(# D,d1,A,M #) is right_zeroed & CLSStruct(# D,d1,A,M #) is right_complementable & CLSStruct(# D,d1,A,M #) is ComplexLinearSpace-like )
proof
set AV = the
addF of
V;
set MV = the
Mult of
V;
thus
for
x,
y being
VECTOR of
CLSStruct(#
D,
d1,
A,
M #) holds
x + y = y + x
:: according to RLVECT_1:def 5 :: thesis: ( CLSStruct(# D,d1,A,M #) is add-associative & CLSStruct(# D,d1,A,M #) is right_zeroed & CLSStruct(# D,d1,A,M #) is right_complementable & CLSStruct(# D,d1,A,M #) is ComplexLinearSpace-like )
thus
for
x,
y,
z being
VECTOR of
CLSStruct(#
D,
d1,
A,
M #) holds
(x + y) + z = x + (y + z)
:: according to RLVECT_1:def 6 :: thesis: ( CLSStruct(# D,d1,A,M #) is right_zeroed & CLSStruct(# D,d1,A,M #) is right_complementable & CLSStruct(# D,d1,A,M #) is ComplexLinearSpace-like )proof
let x,
y,
z be
VECTOR of
CLSStruct(#
D,
d1,
A,
M #);
:: thesis: (x + y) + z = x + (y + z)
reconsider x1 =
x,
y1 =
y,
z1 =
z as
VECTOR of
V by A1, TARSKI:def 3;
thus (x + y) + z =
the
addF of
V . [(x + y),z1]
by A6
.=
(x1 + y1) + z1
by A6
.=
x1 + (y1 + z1)
by RLVECT_1:def 6
.=
the
addF of
V . [x1,(y + z)]
by A6
.=
x + (y + z)
by A6
;
:: thesis: verum
end;
thus
for
x being
VECTOR of
CLSStruct(#
D,
d1,
A,
M #) holds
x + (0. CLSStruct(# D,d1,A,M #)) = x
:: according to RLVECT_1:def 7 :: thesis: ( CLSStruct(# D,d1,A,M #) is right_complementable & CLSStruct(# D,d1,A,M #) is ComplexLinearSpace-like )proof
let x be
VECTOR of
CLSStruct(#
D,
d1,
A,
M #);
:: thesis: x + (0. CLSStruct(# D,d1,A,M #)) = x
reconsider y =
x as
VECTOR of
V by A1, TARSKI:def 3;
thus x + (0. CLSStruct(# D,d1,A,M #)) =
y + (0. V)
by A2, A6
.=
x
by RLVECT_1:10
;
:: thesis: verum
end;
thus
CLSStruct(#
D,
d1,
A,
M #) is
right_complementable
:: thesis: CLSStruct(# D,d1,A,M #) is ComplexLinearSpace-like proof
let x be
VECTOR of
CLSStruct(#
D,
d1,
A,
M #);
:: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x1 =
x as
VECTOR of
V by A1, TARSKI:def 3;
consider v being
VECTOR of
V such that A7:
x1 + v = 0. V
by ALGSTR_0:def 11;
v =
- x1
by A7, RLVECT_1:def 11
.=
(- 1r ) * x1
by Th4
.=
(- 1r ) * x
by A1, A4, FUNCT_1:72
;
then reconsider y =
v as
VECTOR of
CLSStruct(#
D,
d1,
A,
M #) ;
take
y
;
:: according to ALGSTR_0:def 11 :: thesis: x + y = 0. CLSStruct(# D,d1,A,M #)
thus
x + y = 0. CLSStruct(#
D,
d1,
A,
M #)
by A2, A6, A7;
:: thesis: verum
end;
thus
for
z being
Complex for
x,
y being
VECTOR of
CLSStruct(#
D,
d1,
A,
M #) holds
z * (x + y) = (z * x) + (z * y)
:: according to CLVECT_1:def 2 :: thesis: ( ( for z1, z2 being Complex
for v being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 + z2) * v = (z1 * v) + (z2 * v) ) & ( for z1, z2 being Complex
for v being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of CLSStruct(# D,d1,A,M #) holds 1r * v = v ) )proof
let z be
Complex;
:: thesis: for x, y being VECTOR of CLSStruct(# D,d1,A,M #) holds z * (x + y) = (z * x) + (z * y)let x,
y be
VECTOR of
CLSStruct(#
D,
d1,
A,
M #);
:: thesis: z * (x + y) = (z * x) + (z * y)
reconsider x1 =
x,
y1 =
y as
VECTOR of
V by A1, TARSKI:def 3;
thus z * (x + y) =
the
Mult of
V . [z,(x + y)]
by A1, A4, FUNCT_1:72
.=
z * (x1 + y1)
by A6
.=
(z * x1) + (z * y1)
by Def2
.=
the
addF of
V . [(the Mult of V . [z,x1]),(z * y)]
by A1, A4, FUNCT_1:72
.=
the
addF of
V . [(z * x),(z * y)]
by A1, A4, FUNCT_1:72
.=
(z * x) + (z * y)
by A1, A3, FUNCT_1:72
;
:: thesis: verum
end;
thus
for
z1,
z2 being
Complex for
x being
VECTOR of
CLSStruct(#
D,
d1,
A,
M #) holds
(z1 + z2) * x = (z1 * x) + (z2 * x)
:: thesis: ( ( for z1, z2 being Complex
for v being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of CLSStruct(# D,d1,A,M #) holds 1r * v = v ) )proof
let z1,
z2 be
Complex;
:: thesis: for x being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 + z2) * x = (z1 * x) + (z2 * x)let x be
VECTOR of
CLSStruct(#
D,
d1,
A,
M #);
:: thesis: (z1 + z2) * x = (z1 * x) + (z2 * x)
reconsider y =
x as
VECTOR of
V by A1, TARSKI:def 3;
thus (z1 + z2) * x =
(z1 + z2) * y
by A1, A4, FUNCT_1:72
.=
(z1 * y) + (z2 * y)
by Def2
.=
the
addF of
V . [(the Mult of V . [z1,y]),(z2 * x)]
by A1, A4, FUNCT_1:72
.=
the
addF of
V . [(z1 * x),(z2 * x)]
by A1, A4, FUNCT_1:72
.=
(z1 * x) + (z2 * x)
by A1, A3, FUNCT_1:72
;
:: thesis: verum
end;
thus
for
z1,
z2 being
Complex for
x being
VECTOR of
CLSStruct(#
D,
d1,
A,
M #) holds
(z1 * z2) * x = z1 * (z2 * x)
:: thesis: for v being VECTOR of CLSStruct(# D,d1,A,M #) holds 1r * v = vproof
let z1,
z2 be
Complex;
:: thesis: for x being VECTOR of CLSStruct(# D,d1,A,M #) holds (z1 * z2) * x = z1 * (z2 * x)let x be
VECTOR of
CLSStruct(#
D,
d1,
A,
M #);
:: thesis: (z1 * z2) * x = z1 * (z2 * x)
reconsider y =
x as
VECTOR of
V by A1, TARSKI:def 3;
thus (z1 * z2) * x =
(z1 * z2) * y
by A1, A4, FUNCT_1:72
.=
z1 * (z2 * y)
by Def2
.=
the
Mult of
V . [z1,(z2 * x)]
by A1, A4, FUNCT_1:72
.=
z1 * (z2 * x)
by A1, A4, FUNCT_1:72
;
:: thesis: verum
end;
let x be
VECTOR of
CLSStruct(#
D,
d1,
A,
M #);
:: thesis: 1r * x = x
reconsider y =
x as
VECTOR of
V by A1, TARSKI:def 3;
thus 1r * x =
1r * y
by A1, A4, FUNCT_1:72
.=
x
by Def2
;
:: thesis: verum
end;
hence
CLSStruct(# D,d1,A,M #) is Subspace of V
by A1, A3, A4, A5, Def5; :: thesis: verum