set C = CAlgebra A;
thus CAlgebra A is strict ; :: thesis:
thus CAlgebra A is Abelian by Th5; :: thesis:
thus CAlgebra A is add-associative by Th6; :: thesis:
thus CAlgebra A is right_zeroed :: thesis:
proof
let x be Element of (); :: according to RLVECT_1:def 4 :: thesis: x + (0. ()) = x
reconsider f = x as Element of Funcs (A,COMPLEX) ;
thus x + (0. ()) = () . ((),f) by Th5
.= x by Th10 ; :: thesis: verum
end;
thus CAlgebra A is right_complementable :: thesis:
proof
let x be Element of (); :: according to ALGSTR_0:def 16 :: thesis:
reconsider mj = - 1r as Element of COMPLEX by XCMPLX_0:def 2;
reconsider f = x as Element of Funcs (A,COMPLEX) ;
reconsider t = . [mj,f] as Element of () ;
take t ; :: according to ALGSTR_0:def 11 :: thesis: x + t = 0. ()
thus x + t = 0. () by Th11; :: thesis: verum
end;
thus CAlgebra A is commutative by Th7; :: thesis:
thus CAlgebra A is associative by Th8; :: thesis:
thus CAlgebra A is right_unital :: thesis:
proof
let x be Element of (); :: according to VECTSP_1:def 4 :: thesis: x * (1. ()) = x
reconsider f = x as Element of Funcs (A,COMPLEX) ;
thus x * (1. ()) = () . ((),f) by Th7
.= x by Th9 ; :: thesis: verum
end;
thus CAlgebra A is right-distributive by Th15; :: thesis:
thus CAlgebra A is vector-distributive by Lm2; :: thesis:
thus CAlgebra A is scalar-distributive by Th14; :: thesis:
thus CAlgebra A is scalar-associative by Th13; :: thesis:
let x, y be Element of (); :: according to CFUNCDOM:def 9 :: thesis: for a being Complex holds a * (x * y) = (a * x) * y
let a be Complex; :: thesis: a * (x * y) = (a * x) * y
thus a * (x * y) = (a * x) * y by Th16; :: thesis: verum