set W = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);
A1: for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + w = w + v
proof
let v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: v + w = w + v
reconsider v9 = v, w9 = w as VECTOR of V ;
v + w = v9 + w9 ;
hence v + w = w9 + v9
.= w + v ;
:: thesis: verum
end;
A2: for u, v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (u + v) + w = u + (v + w)
proof
let u, v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: (u + v) + w = u + (v + w)
reconsider u9 = u, v9 = v, w9 = w as VECTOR of V ;
(u9 + v9) + w9 = u9 + (v9 + w9) by RLVECT_1:def 3;
hence (u + v) + w = u + (v + w) ; :: thesis: verum
end;
A3: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v is right_complementable
proof
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: v is right_complementable
reconsider v9 = v as VECTOR of V ;
v9 is right_complementable by ALGSTR_0:def 16;
then consider w9 being VECTOR of V such that
A4: v9 + w9 = 0. V ;
reconsider w = w9 as VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
thus v + w = 0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by A4; :: thesis: verum
end;
A5: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v
proof
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v
reconsider v9 = v as VECTOR of V ;
thus v + (0. CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v9 + (0. V)
.= v ; :: thesis: verum
end;
A6: for a, b being Complex
for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a * b) * v = a * (b * v)
proof
let a, b be Complex; :: thesis: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a * b) * v = a * (b * v)
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: (a * b) * v = a * (b * v)
reconsider v9 = v as VECTOR of V ;
(a * b) * v9 = a * (b * v9) by CLVECT_1:def 4;
hence (a * b) * v = a * (b * v) ; :: thesis: verum
end;
A7: for a, b being Complex
for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a + b) * v = (a * v) + (b * v)
proof
let a, b be Complex; :: thesis: for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v9 = v as VECTOR of V ;
(a + b) * v9 = (a * v9) + (b * v9) by CLVECT_1:def 3;
hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum
end;
A8: for a being Complex
for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds a * (v + w) = (a * v) + (a * w)
proof
let a be Complex; :: thesis: for v, w being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v9 = v, w9 = w as VECTOR of V ;
a * (v9 + w9) = (a * v9) + (a * w9) by CLVECT_1:def 2;
hence a * (v + w) = (a * v) + (a * w) ; :: thesis: verum
end;
for v being VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds 1r * v = v
proof
let v be VECTOR of CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: 1r * v = v
reconsider v9 = v as VECTOR of V ;
thus 1r * v = 1r * v9
.= v by CLVECT_1:def 5 ; :: thesis: verum
end;
then reconsider W = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) as ComplexLinearSpace by A1, A2, A5, A3, A8, A7, A6, 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;
A9: the Mult of W = the Mult of V | [:COMPLEX, the carrier of W:] by RELSET_1:19;
( 0. W = 0. V & the addF of W = the addF of V || the carrier of W ) by RELSET_1:19;
hence CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V by A9, CLVECT_1:def 8; :: thesis: verum