The abstract of the Mizar article:

Calculation of Matrices of Field Elements. Part I

by

Yatsuka Nakamura, and

Hiroshi Yamazaki

Received August 8, 2003

MML identifier: MATRIX_4

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, FINSEQ_1, RELAT_1, FUNCT_1, ARYTM_1, VECTSP_1, INCSP_1,
      RLVECT_1, FINSEQ_2, RVSUM_1, MATRIX_1, TREES_1, CAT_3, PARTFUN1;
 notation TARSKI, XBOOLE_0, FINSEQ_2, SUBSET_1, XREAL_0, REAL_1, NAT_1,
      RELAT_1, FUNCT_1, STRUCT_0, FINSEQ_1, BINOP_1, ZFMISC_1, FINSEQOP,
      MATRIX_3, MATRIX_1, VECTSP_1, FVSUM_1, FUNCT_3, RLVECT_1;
 constructors DOMAIN_1, NAT_1, TOPMETR, INT_1, MATRIX_3, FVSUM_1, FUNCT_3,
      SETWOP_2;
 clusters FUNCT_1, STRUCT_0, INT_1, RELSET_1, XBOOLE_0;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

 reserve a,b,r,y1,y2,lambda for Real, i,j,n for Nat;

definition let K be Field, M1, M2 be Matrix of K;
  func M1-M2 -> Matrix of K equals
:: MATRIX_4:def 1
   M1+(-M2);
end;

theorem :: MATRIX_4:1
for K being Field, M being Matrix of K
  st len M>0 holds --M=M;

theorem :: MATRIX_4:2
for K being Field,M being Matrix of K
  st len M>0 holds M+(-M)=0.(K,len M,width M);

theorem :: MATRIX_4:3
for K being Field,M being Matrix of K
  st len M>0 holds M - M=0.(K,len M,width M);

theorem :: MATRIX_4:4
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2=width M3 &
  len M1>0 &
  M1+M3=M2+M3 holds M1=M2;

theorem :: MATRIX_4:5
for K being Field,M1,M2 being Matrix of K
  st len M2>0 holds
  M1--M2=M1+M2;

theorem :: MATRIX_4:6
  for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 &
  M1 = M1 + M2 holds M2 = 0.(K,len M1,width M1);

theorem :: MATRIX_4:7
for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 &
  M1 - M2 = 0.(K,len M1,width M1) holds M1 = M2;

theorem :: MATRIX_4:8
for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 &
  len M1 >0 & M1+M2= 0.(K,len M1,width M1) holds M2=-M1;

theorem :: MATRIX_4:9
for n,m being Nat,K being Field st n>0
  holds -(0.(K,n,m))=0.(K,n,m);

theorem :: MATRIX_4:10
  for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 &
  M2 - M1 = M2 holds M1=0.(K,len M1,width M1);

theorem :: MATRIX_4:11
for K being Field,M1,M2 being Matrix of K
st len M1=len M2 & width M1=width M2 & len M1>0 holds
    M1 = M1 -(M2 - M2);

theorem :: MATRIX_4:12
for K being Field,M1,M2 being Matrix of K
st len M1=len M2 & width M1=width M2 & len M1>0 holds
    - (M1 + M2) = -M1+-M2;

theorem :: MATRIX_4:13
  for K being Field,M1,M2 being Matrix of K
st len M1=len M2 & width M1=width M2 & len M1>0 holds
    M1 - (M1 - M2) = M2;

theorem :: MATRIX_4:14
for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 &
  M1 - M3 = M2 - M3 holds M1 = M2;

theorem :: MATRIX_4:15
for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 &
  M3 - M1 = M3 - M2 holds M1 = M2;

theorem :: MATRIX_4:16
for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  M1 - M2 - M3 = M1 - M3 - M2;

theorem :: MATRIX_4:17
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  M1 - M3 = (M1 - M2) - (M3 - M2);

theorem :: MATRIX_4:18
for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  (M3 - M1) - (M3 - M2) = M2 - M1;

theorem :: MATRIX_4:19
  for K being Field,M1,M2,M3,M4 being Matrix of K
  st len M1=len M2 & len M2=len M3 & len M3=len M4 &
  width M1=width M2 & width M2 = width M3 & width M3=width M4 &
  len M1>0 &  M1 - M2 = M3 - M4 holds M1 - M3 = M2 - M4;

theorem :: MATRIX_4:20
for K being Field,M1,M2 being Matrix of K
st len M1=len M2 & width M1=width M2 & len M1>0 holds
 M1 = M1 + (M2 - M2);

theorem :: MATRIX_4:21
for K being Field,M1,M2 being Matrix of K
st len M1=len M2 & width M1=width M2 & len M1>0 holds
 M1 = M1 + M2 - M2;

theorem :: MATRIX_4:22
for K being Field,M1,M2 being Matrix of K
st len M1=len M2 & width M1=width M2 & len M1>0 holds
 M1 = M1 - M2 + M2;

theorem :: MATRIX_4:23
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2=width M3 & len M1>0 holds
  M1 + M3 = (M1 + M2) + (M3 - M2);

theorem :: MATRIX_4:24
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  M1 + M2 - M3 = M1 - M3 + M2;

theorem :: MATRIX_4:25
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  M1 - M2 + M3 = M3 - M2 + M1;

theorem :: MATRIX_4:26
for K being Field,M1,M2,M3 being Matrix of K
 st len M1=len M2 & len M2=len M3 &
 width M1=width M2 & width M2 = width M3 & len M1>0 holds
 M1 + M3 = (M1 + M2) - (M2 - M3);

theorem :: MATRIX_4:27
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  M1 - M3 = (M1 + M2) - (M3 + M2);

theorem :: MATRIX_4:28
for K being Field,M1,M2,M3,M4 being Matrix of K
 st len M1=len M2 & len M2=len M3 & len M3=len M4 &
 width M1=width M2 & width M2 = width M3 & width M3=width M4 &
 len M1>0 &  M1 + M2 = M3 + M4 holds M1 - M3 = M4 - M2;

theorem :: MATRIX_4:29
  for K being Field,M1,M2,M3,M4 being Matrix of K
  st len M1=len M2 & len M2=len M3 & len M3=len M4 &
  width M1=width M2 & width M2 = width M3 & width M3=width M4 &
  len M1>0 &  M1 - M3 = M4 - M2 holds M1 + M2 = M3 + M4;

theorem :: MATRIX_4:30
  for K being Field,M1,M2,M3,M4 being Matrix of K
  st len M1=len M2 & len M2=len M3 & len M3=len M4 &
  width M1=width M2 & width M2 = width M3 & width M3=width M4 &
  len M1>0 &  M1 + M2 = M3 - M4 holds M1 + M4 = M3 - M2;

theorem :: MATRIX_4:31
for K being Field,M1,M2,M3 being Matrix of K
 st len M1=len M2 & len M2=len M3 &
 width M1=width M2 & width M2 = width M3 & len M1>0 holds
 M1 - (M2 + M3) = M1 - M2 - M3;

theorem :: MATRIX_4:32
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  M1 - (M2 - M3) = M1 - M2 + M3;

theorem :: MATRIX_4:33
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  M1 - (M2 - M3) = M1 +( M3 - M2);

theorem :: MATRIX_4:34
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  M1 - M3 = (M1-M2)+(M2 - M3);

theorem :: MATRIX_4:35
  for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 &
  -M1=-M2 holds  M1=M2;

theorem :: MATRIX_4:36
  for K being Field,M being Matrix of K
  st len M>0 & -M=0.(K,len M,width M) holds
  M= 0.(K,len M,width M);

theorem :: MATRIX_4:37
  for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 &
  M1 + -M2 = 0.(K,len M1,width M1) holds M1 = M2;

theorem :: MATRIX_4:38
for K being Field,M1,M2 being Matrix of K
st len M1=len M2 & width M1=width M2 & len M1>0 holds
 M1=M1+M2+(-M2);

theorem :: MATRIX_4:39
  for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 holds
  M1=M1+(M2 + -M2);

theorem :: MATRIX_4:40
  for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 holds
  M1=(-M2+M1)+M2;

theorem :: MATRIX_4:41
  for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 holds
  -(-M1+M2)=M1+-M2;

theorem :: MATRIX_4:42
  for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 holds
  M1+M2=-(-M1+-M2);

theorem :: MATRIX_4:43
  for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 holds
  -(M1 - M2) = M2 - M1;

theorem :: MATRIX_4:44
for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 holds
  - M1 - M2 = - M2 - M1;

theorem :: MATRIX_4:45
  for K being Field,M1,M2 being Matrix of K
  st len M1=len M2 & width M1=width M2 & len M1>0 holds
  M1 = - M2 - (- M1 - M2);

theorem :: MATRIX_4:46
for K being Field,M1,M2,M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  - M1 - M2 - M3 = - M1 - M3 - M2;

theorem :: MATRIX_4:47
  for K being Field, M1, M2, M3 being Matrix of K
  st len M1 = len M2 & len M2 = len M3 &
  width M1 = width M2 & width M2 = width M3 & len M1>0 holds
  - M1 - M2 - M3 = - M2 - M3 - M1;

theorem :: MATRIX_4:48
  for K being Field, M1, M2, M3 being Matrix of K
  st len M1=len M2 & len M2=len M3 &
  width M1=width M2 & width M2 = width M3 & len M1>0 holds
  - M1 - M2 - M3 = - M3 - M2 - M1;

theorem :: MATRIX_4:49
  for K being Field, M1, M2, M3 being Matrix of K
  st len M1 = len M2 & len M2 = len M3 &
  width M1 = width M2 & width M2 = width M3 & len M1>0 holds
  (M3 - M1) - (M3 - M2) = - (M1 - M2);

theorem :: MATRIX_4:50
  for K being Field, M being Matrix of K
  st len M>0 holds
  0.(K, len M, width M) - M = - M;

theorem :: MATRIX_4:51
  for K being Field, M1, M2 being Matrix of K
  st len M1 = len M2 & width M1 = width M2 & len M1>0 holds
  M1 + M2 = M1 - - M2;

theorem :: MATRIX_4:52
  for K being Field, M1, M2 being Matrix of K
  st len M1 = len M2 & width M1 = width M2 & len M1>0 holds
  M1 = M1 - (M2 + -M2);

theorem :: MATRIX_4:53
  for K being Field, M1, M2, M3 being Matrix of K
  st len M1 = len M2 & len M2 = len M3 &
  width M1 = width M2 & width M2 = width M3 & len M1>0 &
  M1 - M3 = M2 + - M3 holds M1 = M2;

theorem :: MATRIX_4:54
  for K being Field, M1, M2, M3 being Matrix of K
  st len M1 = len M2 & len M2 = len M3 &
  width M1 = width M2 & width M2 = width M3 & len M1>0 &
  M3 - M1 = M3 + - M2 holds M1 = M2;

theorem :: MATRIX_4:55
for K being Field,A,B being Matrix of K st
  len A=len B & width A=width B holds Indices A=Indices B;

theorem :: MATRIX_4:56    :: EUCLID_2:9
  for K being Field,x,y,z being FinSequence of (the carrier of K) st
  len x=len y & len y=len z holds
  mlt(x+y,z) = mlt(x,z)+mlt(y,z);

theorem :: MATRIX_4:57    :: EUCLID_2:9
  for K being Field,x,y,z being FinSequence of (the carrier of K) st
  len x=len y & len y=len z holds
  mlt(z,x+y) = mlt(z,x)+mlt(z,y);

theorem :: MATRIX_4:58
  for D being non empty set,M being Matrix of D holds
  len M >0 implies for n being Nat holds
  (M is Matrix of n,width M, D) iff n = len M;

theorem :: MATRIX_4:59
for K being Field,j being Nat,A,B being Matrix of K
  st len A=len B & width A=width B & (ex j being Nat st [i,j] in Indices A)
  holds Line(A+B,i)=Line(A,i)+Line(B,i);

theorem :: MATRIX_4:60
for K being Field,j being Nat,A,B being Matrix of K
  st len A=len B & width A=width B & (ex i being Nat st [i,j] in Indices A)
  holds Col(A+B,j)=Col(A,j)+Col(B,j);

theorem :: MATRIX_4:61    ::MATRLIN:34
  for V1 being Field,P1,P2 be FinSequence of the carrier of V1
  st len P1 = len P2
  holds
  Sum(P1+P2) = (Sum P1) + (Sum P2);

theorem :: MATRIX_4:62
  for K being Field,A,B,C being Matrix of K
  st len B=len C & width B=width C & width A=len B & len A>0 & len B>0
  holds A*(B+C)=A*B + A*C;

theorem :: MATRIX_4:63
  for K being Field,A,B,C being Matrix of K
  st len B=len C & width B=width C & len A=width B & len B>0 & len A>0
  holds (B+C)*A=B*A + C*A;

theorem :: MATRIX_4:64
  for K being Field,n,m,k being Nat,
  M1 being Matrix of n,m,K,
  M2 being Matrix of m,k,K st width M1=len M2 & 0< len M1 & 0<len M2 holds
  M1*M2 is Matrix of n,k,K;