let C be non empty strict CLSStruct ; :: thesis: ( C = ComplexVectSpace A implies ( C is Abelian & C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital ) )
assume A1: C = ComplexVectSpace A ; :: thesis: ( C is Abelian & C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
thus for u, v being Element of C holds u + v = v + u by Th5, A1; :: according to RLVECT_1:def 2 :: thesis: ( C is add-associative & C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
thus for u, v, w being Element of C holds (u + v) + w = u + (v + w) by Th6, A1; :: according to RLVECT_1:def 3 :: thesis: ( C is right_zeroed & C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
thus for u being Element of C holds u + (0. C) = u :: according to RLVECT_1:def 4 :: thesis: ( C is right_complementable & C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
proof
let u be Element of C; :: thesis: u + (0. C) = u
reconsider v = u as Element of Funcs (A,COMPLEX) by A1;
thus u + (0. C) = (ComplexFuncAdd A) . ((ComplexFuncZero A),v) by Th5, A1
.= u by Th10 ; :: thesis: verum
end;
thus for u being Element of C holds u is right_complementable :: according to ALGSTR_0:def 16 :: thesis: ( C is vector-distributive & C is scalar-distributive & C is scalar-associative & C is scalar-unital )
proof
let u be Element of C; :: thesis: u is right_complementable
reconsider v = u as Element of Funcs (A,COMPLEX) by A1;
reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;
reconsider w = (ComplexFuncExtMult A) . [mj,v] as VECTOR of C by A1;
take w ; :: according to ALGSTR_0:def 11 :: thesis: u + w = 0. C
thus u + w = 0. C by Th11, A1; :: thesis: verum
end;
thus for a being Complex
for u, v being VECTOR of C holds a * (u + v) = (a * u) + (a * v) by Lm2, A1; :: according to CLVECT_1:def 2 :: thesis: ( C is scalar-distributive & C is scalar-associative & C is scalar-unital )
thus for a, b being Complex
for v being VECTOR of C holds (a + b) * v = (a * v) + (b * v) by Th14, A1; :: according to CLVECT_1:def 3 :: thesis: ( C is scalar-associative & C is scalar-unital )
thus for a, b being Complex
for v being VECTOR of C holds (a * b) * v = a * (b * v) by Th13, A1; :: according to CLVECT_1:def 4 :: thesis: C is scalar-unital
thus for v being Element of C holds 1r * v = v by Th12, A1; :: according to CLVECT_1:def 5 :: thesis: verum