The Mizar abstract of MATRIX

Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users
The abstract of the Mizar article:: The Product and the Determinant of Matrices with Entries in a Field
by
Katarzyna Zawadzka
Received May 17, 1993
MML identifier: MATRIX_3
[ Mizar article, MML identifier index ]
environ

 vocabulary VECTSP_1, RLVECT_1, MATRIX_1, FINSEQ_2, ARYTM_1, FINSEQ_1, TREES_1,
      FUNCT_1, RELAT_1, BOOLE, INCSP_1, CAT_3, RVSUM_1, GROUP_1, BINOP_1,
      SETWISEO, SQUARE_1, MATRIX_2, QC_LANG1, FINSUB_1, FINSET_1, FUNCOP_1,
      PARTFUN1, FINSEQOP, FUNCT_5, SUBSET_1, FVSUM_1, MATRIX_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, STRUCT_0,
      FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, BINOP_1,
      FUNCT_3, FUNCOP_1, RLVECT_1, VECTSP_1, SETWISEO, SETWOP_2, FINSEQ_2,
      FINSEQOP, MATRIX_1, FINSUB_1, MATRIX_2, NAT_1, SQUARE_1, FVSUM_1,
      TREES_1, FUNCT_5, CAT_2;
 constructors ALGSTR_1, BINOP_1, SETWISEO, SETWOP_2, FINSEQOP, MATRIX_2, NAT_1,
      SQUARE_1, FVSUM_1, CAT_2, FINSOP_1, MEMBERED, PARTFUN1, RELAT_2,
      XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, FINSUB_1, FINSET_1, RELSET_1, STRUCT_0, FVSUM_1,
      MATRIX_2, FUNCOP_1, XREAL_0, ARYTM_3, VECTSP_1, MEMBERED, ZFMISC_1,
      FUNCT_2, PARTFUN1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

 reserve x,y,z,x1,x2,y1,y2,z1,z2 for set,
  i,j,k,l,n,m for Nat,
  D for non empty set,
  K for Field;

::  Auxiliary theorems

theorem :: MATRIX_3:1
 n = n + k implies k=0;

definition let K,n,m;
  func 0.(K,n,m) -> Matrix of n,m,K equals
:: MATRIX_3:def 1
  n |-> (m |-> 0.K);
end;

definition let K;let A be Matrix of K;
  func -A -> Matrix of K means
:: MATRIX_3:def 2
len it= len A & width it =width A &
      for i,j holds [i,j] in Indices A implies it*(i,j)= -(A*(i,j));
  end;

definition let K;let A,B be Matrix of K;
  func A+B -> Matrix of K means
:: MATRIX_3:def 3
 len it =len A & width it=width A &
      for i,j holds [i,j] in Indices A implies
      it*(i,j) = A*(i,j) + B*(i,j);
 end;

canceled;

theorem :: MATRIX_3:3
  for i,j st [i,j] in Indices (0.(K,n,m)) holds
             (0.(K,n,m))*(i,j)= 0.K;

theorem :: MATRIX_3:4
   for A,B being Matrix of K st len A= len B & width A=width B
       holds A + B = B + A;

theorem :: MATRIX_3:5
   for A,B,C being Matrix of K st len A=len B & len A=len C &
        width A=width B & width A=width C holds
        (A + B) + C= A + (B + C);

theorem :: MATRIX_3:6
    for A being Matrix of n,m,K holds A + 0.(K,n,m)= A;

theorem :: MATRIX_3:7
   for A being Matrix of n,m,K holds A + (-A) = 0.(K,n,m);

definition let K;let A,B be Matrix of K;
  assume width A=len B;
  func A*B ->Matrix of K means
:: MATRIX_3:def 4
 len it=len A & width it=width B &
   for i,j st [i,j] in Indices it holds
    it*(i,j)=Line(A,i) "*" Col(B,j);
 end;

definition let n,k,m;let K;let A be Matrix of n,k,K;
  let B be Matrix of width A,m,K;
redefine func A*B -> Matrix of len A,width B,K;
end;

definition let K;let M be Matrix of K;
           let a be Element of K;
  func a*M -> Matrix of K means
:: MATRIX_3:def 5
    len it=len M & width it =width M &
  for i,j st [i,j] in Indices M holds it*(i,j)=a*(M*(i,j));
end;

definition let K;let M be Matrix of K;
           let a be Element of K;
  func M*a -> Matrix of K equals
:: MATRIX_3:def 6
   a*M;
 end;

theorem :: MATRIX_3:8
   for p,q being FinSequence of the carrier of K st len p=len q holds
  len (mlt(p,q))=len p & len (mlt(p,q))=len q;

theorem :: MATRIX_3:9
   for i,l st [i,l] in Indices (1.(K,n)) & l=i holds (Line(1.(K,n),i)).l=1_ K;

theorem :: MATRIX_3:10
   for i,l st [i,l] in Indices (1.(K,n)) &
  l<>i holds (Line(1.(K,n),i)).l=0.K;

theorem :: MATRIX_3:11
   for l,j st [l,j] in Indices (1.(K,n))
  & l=j holds (Col(1.(K,n),j)).l=1_ K;

theorem :: MATRIX_3:12
   for l,j st [l,j] in Indices (1.(K,n))
  & l<>j holds (Col(1.(K,n),j)).l=0.K;

theorem :: MATRIX_3:13
  for K being add-associative right_zeroed right_complementable
      (non empty LoopStr) holds
  Sum (n |-> 0.K) = 0.K;

theorem :: MATRIX_3:14
  for K being add-associative right_zeroed right_complementable
      (non empty LoopStr)
  for p being FinSequence of the carrier of K
     for i st i in dom p & for k st k in dom p & k<>i holds p.k=0.K
     holds Sum p=p.i;

theorem :: MATRIX_3:15
for p,q being FinSequence of the carrier of K
  holds len (mlt(p,q))=min(len p,len q);

theorem :: MATRIX_3:16
 for p,q being FinSequence of the carrier of K
  for i st i in dom p & p.i=1_ K &
  for k st k in dom p & k<>i holds p.k=0.K
  for j st j in dom (mlt(p,q)) holds
   (i=j implies mlt(p,q).j=(q.i)) & (i<>j implies mlt(p,q).j=0.K);

theorem :: MATRIX_3:17
 for i,j st [i,j] in Indices (1.(K,n)) holds
  (i=j implies (Line((1.(K,n)),i)).j=1_ K) &
  (i<>j implies (Line((1.(K,n)),i)).j=0.K);

theorem :: MATRIX_3:18
for i,j st [i,j] in Indices (1.(K,n)) holds
  (i=j implies (Col((1.(K,n)),j)).i=1_ K) &
  (i<>j implies (Col((1.(K,n)),j)).i=0.K);

theorem :: MATRIX_3:19
 for p,q being FinSequence of the carrier of K
  for i st i in dom p & i in dom q & p.i=1_ K &
  for k st k in dom p & k<>i holds p.k=0.K
    holds Sum(mlt(p,q))=q.i;

theorem :: MATRIX_3:20
   for A being Matrix of n,K holds 1.(K,n)*A=A;

theorem :: MATRIX_3:21
   for A being Matrix of n,K holds A*(1.(K,n))=A;

theorem :: MATRIX_3:22
    for a,b being Element of K holds
    <*<*a*>*> * <*<*b*>*> =<*<*a*b*>*>;

theorem :: MATRIX_3:23
    for a1,a2,b1,b2,c1,c2,d1,d2 being Element of K holds
    (a1,b1)][(c1,d1)*(a2,b2)][(c2,d2) =
    (a1*a2+b1*c2,a1*b2+b1*d2)][(c1*a2+d1*c2,c1*b2+ d1*d2);

theorem :: MATRIX_3:24
   for A,B being Matrix of K st width A=len B & width B<>0 holds
   (A*B) @=(B @)*(A @);

begin :: The product of Matrices

definition let I,J be non empty set;
  let X be Element of Fin I;
  let Y be Element of Fin J;
 redefine func [:X,Y:]-> Element of Fin [:I,J:];
end;

definition let I,J,D be non empty set;
  let G be BinOp of D;
  let f be Function of I,D;
  let g be Function of J,D;
 redefine func G*(f,g)-> Function of [:I,J:],D;
end;

theorem :: MATRIX_3:25
 for I, J,D be non empty set for F,G be BinOp of D
 for f be Function of I,D for g being Function of J,D
 for X being Element of Fin I for Y being Element of Fin J st
 F is commutative & F is associative & ( [:Y,X:]<>{} or F has_a_unity )&
 G is commutative holds
  F $$ ([:X,Y:],G*(f,g))=F$$([:Y,X:],G*(g,f));

theorem :: MATRIX_3:26
 for I, J be non empty set for F,G be BinOp of D
 for f be Function of I,D for g being Function of J,D st
 F is commutative & F is associative & F has_a_unity holds
  for x being Element of I for y being Element of J holds
   F $$([:{x},{y}:],G*(f,g))=F$$({x},G[:](f,F$$({y},g)));

theorem :: MATRIX_3:27
 for I, J be non empty set for F,G be BinOp of D
 for f be Function of I,D for g being Function of J,D
 for X being Element of Fin I for Y being Element of Fin J st
 F is commutative & F is associative & F has_a_unity &
 F has_an_inverseOp & G is_distributive_wrt F holds
  for x being Element of I holds
   F $$([:{x},Y:],G*(f,g))=F$$({x},G[:](f,F$$(Y,g)));

theorem :: MATRIX_3:28
 for I, J being non empty set
 for F,G being BinOp of D
 for f being Function of I,D for g being Function of J,D
 for X being Element of Fin I for Y being Element of Fin J st
   F has_a_unity & F is commutative & F is associative &
   F has_an_inverseOp & G is_distributive_wrt F holds
  F$$([:X,Y:],G*(f,g))=F$$(X,G[:](f,F$$(Y,g)));

theorem :: MATRIX_3:29
   for I, J be non empty set for F,G be BinOp of D
 for f be Function of I,D for g being Function of J,D st
 F is commutative associative & F has_a_unity & G is commutative holds
  for x being Element of I for y being Element of J holds
   F $$([:{x},{y}:],G*(f,g))=F$$({y},G[;](F$$({x},f),g));

theorem :: MATRIX_3:30
   for I, J being non empty set
 for F,G being BinOp of D
 for f being Function of I,D for g being Function of J,D
 for X being Element of Fin I for Y being Element of Fin J st
   F has_a_unity & F is commutative associative &
 F has_an_inverseOp & G is_distributive_wrt F & G is commutative holds
  F$$([:X,Y:],G*(f,g))=F$$(Y,G[;](F$$(X,f),g));

theorem :: MATRIX_3:31
 for I, J being non empty set
 for F being BinOp of D
 for f being Function of [:I,J:],D
 for g being Function of I,D
 for Y being Element of Fin J st
 F has_a_unity & F is commutative associative &
 F has_an_inverseOp holds
 for x being Element of I holds
 (for i being Element of I holds g.i=F$$(Y,(curry f).i)) implies
   F$$([:{x},Y:],f)=F$$({x},g);

theorem :: MATRIX_3:32

 for I, J being non empty set
 for F being BinOp of D
 for f being Function of [:I,J:],D
 for g being Function of I,D
 for X being Element of Fin I for Y being Element of Fin J st
 (for i being Element of I holds g.i=F$$(Y,(curry f).i))&
 F has_a_unity & F is commutative & F is associative &
 F has_an_inverseOp holds
   F$$([:X,Y:],f)=F$$(X,g);

theorem :: MATRIX_3:33
 for I, J being non empty set
 for F being BinOp of D
 for f being Function of [:I,J:],D
 for g being Function of J,D
 for X being Element of Fin I st
 F has_a_unity & F is commutative & F is associative &
 F has_an_inverseOp holds
 for y being Element of J holds
 (for j being Element of J holds g.j=F$$(X,(curry' f).j)) implies
   F$$([:X,{y}:],f)=F$$({y},g);

theorem :: MATRIX_3:34

 for I, J being non empty set
 for F being BinOp of D
 for f being Function of [:I,J:],D
 for g being Function of J,D
 for X being Element of Fin I for Y being Element of Fin J st
 (for j being Element of J holds g.j=F$$ (X , (curry' f).j) )&
 F has_a_unity & F is commutative & F is associative &
 F has_an_inverseOp holds
   F$$([:X,Y:],f)=F$$(Y,g);

theorem :: MATRIX_3:35
   for A,B,C being Matrix of K st
  width A=len B & width B=len C
    holds (A*B)*C=A*(B*C);

begin  ::  Determinant

definition let n,K;let M be Matrix of n,K;
 let p be Element of Permutations(n);
func Path_matrix(p,M) -> FinSequence of the carrier of K means
:: MATRIX_3:def 7
 len it=n & for i,j st i in dom it & j=p.i holds it.i=M*(i,j);
end;

definition let n,K;let M be Matrix of n,K;
 func Path_product(M) -> Function of Permutations(n),
    the carrier of K means
:: MATRIX_3:def 8
 for p being Element of Permutations(n) holds
    it.p = -((the mult of K) $$ Path_matrix(p,M),p);
end;

definition let n;let K;let M be Matrix of n,K;
 func Det M -> Element of (the carrier of K) equals
:: MATRIX_3:def 9
(the add of K) $$ (FinOmega(Permutations(n)),Path_product(M));
end;

reserve a for Element of K;

theorem :: MATRIX_3:36
   Det <*<*a*>*> =a;

definition let n;let K; let M be Matrix of n,K;
 func diagonal_of_Matrix(M) -> FinSequence of the carrier of K means
:: MATRIX_3:def 10
    len it = n & for i st i in Seg n holds it.i=M*(i,i);
end;
The abstract of the Mizar article:

The Product and the Determinant of Matrices with Entries in a Field
