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 ; :: 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 ; :: according to RLVECT_1:def 3 :: thesis:
thus for u being Element of C holds u + (0. C) = u :: according to RLVECT_1:def 4 :: thesis:
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) = () . ((),v) by
.= 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:
proof
let u be Element of C; :: thesis:
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 = . [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 ; :: thesis: verum
end;
thus for a being Complex
for u, v being VECTOR of C holds a * (u + v) = (a * u) + (a * v) by ; :: 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 ; :: 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 ; :: according to CLVECT_1:def 4 :: thesis:
thus for v being Element of C holds 1r * v = v by ; :: according to CLVECT_1:def 5 :: thesis: verum