begin
theorem
theorem
:: deftheorem defines COMPLEX2Field MATRIX_5:def 1 :
for A being Matrix of COMPLEX holds COMPLEX2Field A = A;
:: deftheorem defines Field2COMPLEX MATRIX_5:def 2 :
for A being Matrix of F_Complex holds Field2COMPLEX A = A;
theorem
theorem
theorem
theorem
:: deftheorem defines + MATRIX_5:def 3 :
for A, B being Matrix of COMPLEX holds A + B = Field2COMPLEX ((COMPLEX2Field A) + (COMPLEX2Field B));
:: deftheorem defines - MATRIX_5:def 4 :
for A being Matrix of COMPLEX holds - A = Field2COMPLEX (- (COMPLEX2Field A));
:: deftheorem defines - MATRIX_5:def 5 :
for A, B being Matrix of COMPLEX holds A - B = Field2COMPLEX ((COMPLEX2Field A) - (COMPLEX2Field B));
:: deftheorem defines * MATRIX_5:def 6 :
for A, B being Matrix of COMPLEX holds A * B = Field2COMPLEX ((COMPLEX2Field A) * (COMPLEX2Field B));
:: deftheorem Def7 defines * MATRIX_5:def 7 :
for x being complex number
for A, b3 being Matrix of COMPLEX holds
( b3 = x * A iff for ea being Element of F_Complex st ea = x holds
b3 = Field2COMPLEX (ea * (COMPLEX2Field A)) );
theorem
theorem
theorem
canceled;
theorem Th10:
theorem
theorem
theorem Th13:
theorem
theorem
:: deftheorem defines 0_Cx MATRIX_5:def 8 :
for n, m being Nat holds 0_Cx (n,m) = Field2COMPLEX (0. (F_Complex,n,m));
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th36:
theorem
theorem Th38:
theorem
theorem Th40:
theorem
theorem