:: A Theory of Matrices of Complex Elements
::  by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received December 10, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies GROUP_1, COMPLFLD, SUPINF_2, CARD_1, MATRIX_1, NUMBERS, ARYTM_3,
      ARYTM_1, RELAT_1, XCMPLX_0, SUBSET_1, FINSEQ_1, TREES_1, VECTSP_1, NAT_1,
      ALGSTR_0, FUNCT_1, BINOP_2, COMPLEX1, XXREAL_0, VALUED_0, TARSKI,
      ORDINAL4, MATRIX_5;
 notations TARSKI, SUBSET_1, ORDINAL1, NAT_D, RELAT_1, FUNCT_1, VALUED_0,
      MATRIX_0, STRUCT_0, ALGSTR_0, FINSEQ_1, BINOP_1, MATRIX_3, MATRIX_1,
      NUMBERS, MATRIX_4, COMPLEX1, COMPLFLD, XCMPLX_0, GROUP_1, BINOP_2,
      XXREAL_0, VECTSP_1, RLVECT_1;
 constructors BINOP_1, COMPLFLD, FVSUM_1, MATRIX_3, MATRIX_4, BINOP_2, NAT_D,
      RVSUM_1, RELSET_1, MATRIX_1;
 registrations RELSET_1, XCMPLX_0, XREAL_0, STRUCT_0, VECTSP_1, COMPLFLD,
      RVSUM_1, FINSEQ_1, NAT_1, MEMBERED;
 requirements NUMERALS, SUBSET, ARITHM;


begin

theorem :: MATRIX_5:1
  1 = 1_F_Complex;

theorem :: MATRIX_5:2
  0.F_Complex = 0;

definition
  let A be Matrix of COMPLEX;
  func COMPLEX2Field A -> Matrix of F_Complex equals
:: MATRIX_5:def 1
  A;
end;

definition
  let A be Matrix of F_Complex;
  func Field2COMPLEX A -> Matrix of COMPLEX equals
:: MATRIX_5:def 2
  A;
end;

theorem :: MATRIX_5:3
  for A,B being Matrix of COMPLEX st COMPLEX2Field A = COMPLEX2Field B
  holds A=B;

theorem :: MATRIX_5:4
  for A,B being Matrix of F_Complex st Field2COMPLEX A = Field2COMPLEX B
  holds A=B;

theorem :: MATRIX_5:5
  for A being Matrix of COMPLEX holds A = Field2COMPLEX COMPLEX2Field A;

theorem :: MATRIX_5:6
  for A being Matrix of F_Complex holds A = COMPLEX2Field Field2COMPLEX A;

definition
  let A,B be Matrix of COMPLEX;
  func A+B -> Matrix of COMPLEX equals
:: MATRIX_5:def 3
  Field2COMPLEX ((COMPLEX2Field A)+(
  COMPLEX2Field B));
end;

definition
  let A be Matrix of COMPLEX;
  func -A -> Matrix of COMPLEX equals
:: MATRIX_5:def 4
  Field2COMPLEX (-COMPLEX2Field A);
end;

definition
  let A,B be Matrix of COMPLEX;
  func A - B -> Matrix of COMPLEX equals
:: MATRIX_5:def 5
  Field2COMPLEX ((COMPLEX2Field A)-(
  COMPLEX2Field B));
  func A*B -> Matrix of COMPLEX equals
:: MATRIX_5:def 6
  Field2COMPLEX ((COMPLEX2Field A)*(
  COMPLEX2Field B));
end;

definition
  let x be Complex, A be Matrix of COMPLEX;
  func x * A -> Matrix of COMPLEX means
:: MATRIX_5:def 7

  for ea being Element of
  F_Complex st ea=x holds it=Field2COMPLEX (ea*(COMPLEX2Field A));
end;

theorem :: MATRIX_5:7
  for A being Matrix of COMPLEX holds len A = len COMPLEX2Field A &
  width A=width COMPLEX2Field A;

theorem :: MATRIX_5:8
  for A being Matrix of F_Complex holds len A =len Field2COMPLEX A &
  width A=width Field2COMPLEX A;

theorem :: MATRIX_5:9
  for K being Field, M being Matrix of K holds (1_K)*M=M;

theorem :: MATRIX_5:10
  for M being Matrix of COMPLEX holds 1*M=M;

theorem :: MATRIX_5:11
  for K being Field, a,b being Element of K, M being Matrix of K holds a
  *(b*M)=(a*b)*M;

theorem :: MATRIX_5:12
  for K being Field, a,b being Element of K, M being Matrix of K
  holds (a+b)*M=a*M + b*M;

theorem :: MATRIX_5:13
  for M being Matrix of COMPLEX holds M+M = 2*M;

theorem :: MATRIX_5:14
  for M being Matrix of COMPLEX holds M+M+M = 3*M;

definition
  let n,m be Nat;
  func 0_Cx(n,m) -> Matrix of COMPLEX equals
:: MATRIX_5:def 8
  Field2COMPLEX (0.(F_Complex,n,m));
end;

theorem :: MATRIX_5:15
  for n,m being Nat holds COMPLEX2Field 0_Cx(n,m)=0.(
  F_Complex,n,m);

theorem :: MATRIX_5:16 :: MATRIX_4:6
  for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
  & M1 = M1 + M2 holds M2 = 0_Cx(len M1,width M1);

theorem :: MATRIX_5:17 :: MATRIX_4:8
  for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
  & M1+M2= 0_Cx(len M1,width M1) holds M2=-M1;

theorem :: MATRIX_5:18 :: MATRIX_4:10
  for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
  & M2 - M1 = M2 holds M1=0_Cx(len M1,width M1);

theorem :: MATRIX_5:19
  for M being Matrix of COMPLEX holds M + 0_Cx(len M,width M) = M;

theorem :: MATRIX_5:20
  for K being Field, b being Element of K,M1,M2 being Matrix of K
  st len M1 = len M2 & width M1 = width M2 holds b*(M1+M2)=b*M1 + b*M2;

theorem :: MATRIX_5:21
  for M1,M2 being Matrix of COMPLEX for a being Complex st len M1
  =len M2 & width M1=width M2 holds a*(M1 + M2) = a*M1 + a*M2;

theorem :: MATRIX_5:22
  for K being Field,M1,M2 being Matrix of K st width M1=len M2 &
  len M1>0& len M2>0 holds 0.(K,len M1,width M1)*M2=0.(K,len M1,width M2);

theorem :: MATRIX_5:23
  for M1,M2 being Matrix of COMPLEX st width M1=len M2 &len M1>0&len M2>
  0 holds 0_Cx(len M1,width M1)*M2=0_Cx(len M1,width M2);

theorem :: MATRIX_5:24
  for K being Field,M1 being Matrix of K st len M1>0 holds 0.K*M1=
  0.(K,len M1,width M1);

theorem :: MATRIX_5:25
  for M1 being Matrix of COMPLEX st len M1>0 holds 0*M1 = 0_Cx(len M1,
  width M1);

definition
  let s be complex-valued Function, k be set;
  redefine func s.k -> Element of COMPLEX;
end;

theorem :: MATRIX_5:26
  for i,j being Nat,M1,M2 being Matrix of COMPLEX st len M2>0
holds ex s being FinSequence of COMPLEX st len s = len M2 & s.1=(M1*(i,1))*(M2*
(1,j)) & for k be Nat st 1<=k & k < len M2 holds s.(k+1)=s.k + (M1*(
  i,k+1))*(M2*(k+1,j));