:: Calculation of Matrices of Field Elements. Part {I}
::  by Yatsuka Nakamura and Hiroshi Yamazaki
::
:: Received August 8, 2003
:: Copyright (c) 2003-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 NAT_1, VECTSP_1, MATRIX_1, ARYTM_1, ARYTM_3, FINSEQ_1, CARD_1,
      XXREAL_0, TREES_1, RELAT_1, SUPINF_2, SUBSET_1, NUMBERS, RVSUM_1,
      FINSEQ_2, STRUCT_0, FUNCT_1, TARSKI, ALGSTR_0, ZFMISC_1, XBOOLE_0,
      PARTFUN1, INCSP_1, CARD_3, FVSUM_1;
 notations TARSKI, XBOOLE_0, FINSEQ_2, SUBSET_1, ORDINAL1, NUMBERS, NAT_1,
      ZFMISC_1, RELAT_1, FUNCT_1, FINSEQ_1, MATRIX_0, STRUCT_0, ALGSTR_0,
      BINOP_1, FINSEQOP, MATRIX_3, MATRIX_1, VECTSP_1, FVSUM_1, FUNCT_3,
      XXREAL_0;
 constructors BINOP_1, FUNCT_3, NAT_1, FVSUM_1, MATRIX_3, RELSET_1, MATRIX_1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, XREAL_0, STRUCT_0, ORDINAL1,
      FINSEQ_2, CARD_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve i,j 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 holds --M=M;

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

theorem :: MATRIX_4:3
  for K being Field,M being Matrix of K 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 & M1+M3=M2+M3 holds M1=M2;

theorem :: MATRIX_4:5
  for K being Field,M1,M2 being Matrix of K 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 & 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 & 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 & M1+M2= 0.(K,len M1,width M1) holds M2=-M1;

theorem :: MATRIX_4:9
  for n,m being Nat,K being Field 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 & 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 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 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 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 & 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 & 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 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 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 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 & 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 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 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 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 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 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 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 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 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 & 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 & 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 & 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 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 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 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 & width
  M1=width M2 holds M1 - M3 = (M1-M2)+(M2 - M3);

theorem :: MATRIX_4:35
  for K being Field,M1,M2,M3 being Matrix of K st -M1=-M2 holds M1=M2;

theorem :: MATRIX_4:36
  for K being Field,M being Matrix of K st -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 & 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 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 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 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 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 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 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 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 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 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 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 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 holds (M3 - M1) - (
  M3 - M2) = - (M1 - M2);

theorem :: MATRIX_4:50
  for K being Field, M being Matrix of K 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 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 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 & 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 & M3 - M1 = M3 + -
  M2 holds M1 = M2;

theorem :: MATRIX_4:55
  for K being set, 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 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 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 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 & (ex i st [i,j] in Indices A) holds Col(A+B,j)=Col(A,j)+Col(B,j);

theorem :: MATRIX_4:61
  for V1 being Field,P1,P2 be FinSequence 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;