:: A Theory of Matrices of Real Elements
::  by Yatsuka Nakamura , Nobuyuki Tamura and Wenpai Chang
::
:: Received February 20, 2006
:: Copyright (c) 2006-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 NUMBERS, NAT_1, REAL_1, SUBSET_1, VECTSP_1, ARYTM_3, RELAT_1,
      FINSEQ_1, ARYTM_1, EUCLID, FINSEQ_2, CARD_1, XBOOLE_0, ALGSTR_0,
      STRUCT_0, XXREAL_0, FUNCT_1, MATRIX_1, TREES_1, INCSP_1, FVSUM_1, CARD_3,
      RVSUM_1, QC_LANG1, GROUP_1, SUPINF_2, MATRIXR1;
 notations TARSKI, SUBSET_1, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, ORDINAL1,
      FUNCT_1, MATRIX_0, NUMBERS, VECTSP_1, RELSET_1, FINSEQ_1, STRUCT_0,
      ALGSTR_0, RLVECT_1, GROUP_1, MATRIX_1, MATRIX_4, MATRIX_3, RVSUM_1,
      FINSEQ_2, FVSUM_1, EUCLID;
 constructors REAL_1, BINOP_2, FVSUM_1, GOBOARD1, MATRIX_3, MATRIX_4, RVSUM_1,
      RELSET_1;
 registrations RELSET_1, NUMBERS, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2,
      STRUCT_0, VECTSP_1, VALUED_0, ORDINAL1, XREAL_0, RVSUM_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin :: Preliminaries

reserve i,j for Nat;

theorem :: MATRIXR1:1
  for r1,r2 being Real, fr1,fr2 being Element of F_Real
   st r1=fr1 & r2=
  fr2 holds r1+r2=fr1+fr2;

theorem :: MATRIXR1:2
  for r1,r2 being Real, fr1,fr2 being Element of F_Real
  st r1=fr1 & r2=
  fr2 holds r1*r2=fr1*fr2;

theorem :: MATRIXR1:3
  for F being FinSequence of REAL holds F + -F = 0*(len F) & F - F = 0*(len F);

theorem :: MATRIXR1:4
  for F1,F2 being FinSequence of REAL st len F1=len F2 holds F1 - F2 =
  F1 + - F2;

theorem :: MATRIXR1:5
  for F being FinSequence of REAL holds F - 0*(len F) = F;

theorem :: MATRIXR1:6
  for F being FinSequence of REAL holds 0*(len F) -F = -F;

theorem :: MATRIXR1:7
  for F1,F2 being FinSequence of REAL st len F1=len F2 holds F1 - -F2 =
  F1 + F2;

theorem :: MATRIXR1:8
  for F1,F2 being FinSequence of REAL st len F1=len F2 holds -(F1 - F2)
  = F2 - F1;

theorem :: MATRIXR1:9
  for F1,F2 being FinSequence of REAL st len F1=len F2 holds -(F1 - F2)
  = -F1 + F2;

theorem :: MATRIXR1:10
  for F1,F2 being FinSequence of REAL st len F1=len F2 & F1 - F2 = 0*(
  len F1) holds F1=F2;

theorem :: MATRIXR1:11
  for F1,F2,F3 being FinSequence of REAL st len F1=len F2 & len F2=len
  F3 holds F1 - F2 - F3 = F1 - (F2 + F3);

theorem :: MATRIXR1:12
  for F1,F2,F3 being FinSequence of REAL st len F1=len F2 & len F2=len
  F3 holds F1 + (F2 - F3) = F1 + F2 - F3;

theorem :: MATRIXR1:13
  for F1,F2,F3 being FinSequence of REAL st len F1=len F2 & len F2=len
  F3 holds F1 - (F2 - F3) = F1 - F2 + F3;

theorem :: MATRIXR1:14
  for F1,F2 being FinSequence of REAL st len F1=len F2 holds F1 = F1 + F2 - F2;

theorem :: MATRIXR1:15
  for F1,F2 being FinSequence of REAL st len F1=len F2 holds F1 = F1 - F2 + F2;

begin :: Matrices of Real Elements

theorem :: MATRIXR1:16
  for K being non empty multMagma, p being FinSequence of K, a
  being Element of K holds len (a*p)=len p;

theorem :: MATRIXR1:17
  for r being Real, fr being Element of F_Real, p being
FinSequence of REAL, fp being FinSequence of F_Real st r=fr & p=fp holds r*p=fr
  *fp;

theorem :: MATRIXR1:18
  for K being Field, a being Element of K, A being Matrix of K holds
  Indices (a*A) = Indices A;

theorem :: MATRIXR1:19
  for K being Field, a being Element of K, M being Matrix of K st
  1<=i & i<=width M holds Col(a*M,i)=a*Col(M,i);

theorem :: MATRIXR1:20
  for K being Field, a being Element of K, M being (Matrix of K), i
  being Nat st 1<=i & i<=len M holds Line(a*M,i)=a*Line(M,i);

theorem :: MATRIXR1:21
  for K being Field, A,B being Matrix of K st width A=len B holds ex C
  being Matrix of K st len C=len A & width C=width B & for i,j st [i,j] in
  Indices C holds C*(i,j)=Line(A,i) "*" Col(B,j);

theorem :: MATRIXR1:22
  for K being Field,a being Element of K,A,B being Matrix of K st
  width A=len B holds A*(a*B)=a*(A*B);

definition
  let A be Matrix of REAL;
  func MXR2MXF A -> Matrix of F_Real equals
:: MATRIXR1:def 1
  A;
end;

definition
  let A be Matrix of F_Real;
  func MXF2MXR A -> Matrix of REAL equals
:: MATRIXR1:def 2
  A;
end;

theorem :: MATRIXR1:23
  for D1,D2 being set, A being (Matrix of D1), B being Matrix of D2 st A
  =B holds for i,j st [i,j] in Indices A holds A*(i,j)=B*(i,j);

theorem :: MATRIXR1:24
  for K being Field, A,B being Matrix of K holds Indices (A+B)=Indices A;

definition
  let A,B be Matrix of REAL;
  func A+B -> Matrix of REAL equals
:: MATRIXR1:def 3
  MXF2MXR ((MXR2MXF A)+(MXR2MXF B));
end;

theorem :: MATRIXR1:25
  for A,B being Matrix of REAL holds len (A+B) = len A & width (A+
B)=width A & for i,j holds [i,j] in Indices A implies (A+B)*(i,j) = A*(i,j) + B
  *(i,j);

theorem :: MATRIXR1:26
  for A,B,C being Matrix of REAL st len C = len A & width C =
width A & for i,j st [i,j] in Indices A holds C*(i,j) = A*(i,j) + B*(i,j) holds
  C=A+B;

definition
  let A be Matrix of REAL;
  func -A -> Matrix of REAL equals
:: MATRIXR1:def 4
  MXF2MXR (-(MXR2MXF A));
end;

definition
  let A,B be Matrix of REAL;
  func A - B -> Matrix of REAL equals
:: MATRIXR1:def 5
  MXF2MXR ((MXR2MXF A)-(MXR2MXF B));
  func A*B -> Matrix of REAL equals
:: MATRIXR1:def 6
  MXF2MXR ((MXR2MXF A)*(MXR2MXF B));
end;

definition
  let a be Real, A be Matrix of REAL;
  func a * A -> Matrix of REAL means
:: MATRIXR1:def 7

  for ea being Element of F_Real st ea=a holds it=MXF2MXR (ea*(MXR2MXF A));
end;

theorem :: MATRIXR1:27
  for a being Real, A being Matrix of REAL holds len (a*A)=len A &
  width (a*A)=width A;

theorem :: MATRIXR1:28
  for a being Real, A being Matrix of REAL
   holds Indices (a*A) = Indices A;

theorem :: MATRIXR1:29
  for a being Real, A being (Matrix of REAL), i2,j2 being Nat st [
  i2,j2] in Indices A holds (a*A)*(i2,j2)=a*(A*(i2,j2));

theorem :: MATRIXR1:30
  for a being Real, A being Matrix of REAL st width A>0
   holds (a*A )@=a*(A@);

theorem :: MATRIXR1:31
  for a being Real,i being Nat,A being Matrix of REAL
    st len A>0 & i in
dom A holds (ex p being FinSequence of REAL st p=A.i) & for q being FinSequence
  of REAL st q=A.i holds (a*A).i=a*q;

theorem :: MATRIXR1:32
  for A being Matrix of REAL holds 1*A=A;

theorem :: MATRIXR1:33
  for A being Matrix of REAL holds A+A=2*A;

theorem :: MATRIXR1:34
  for A being Matrix of REAL holds A+A+A=3*A;

definition
  let n,m be Nat;
  func 0_Rmatrix(n,m) -> Matrix of REAL equals
:: MATRIXR1:def 8
  MXF2MXR (0.(F_Real,n,m));
end;

theorem :: MATRIXR1:35
  for A,B being Matrix of REAL holds A--B=A+B;

theorem :: MATRIXR1:36
  for n,m being Nat,A being Matrix of REAL st len A=n & width A=m
  & n>0 holds A+ 0_Rmatrix(n,m)=A & 0_Rmatrix(n,m)+A=A;

theorem :: MATRIXR1:37
  for A,B being Matrix of REAL st len A=len B & width A=width B & A = A
  + B holds B = 0_Rmatrix(len A,width A);

theorem :: MATRIXR1:38
  for A,B being Matrix of REAL st len A=len B & width A=width B & A+B=
  0_Rmatrix(len A,width A) holds B=-A;

theorem :: MATRIXR1:39
  for A,B being Matrix of REAL st len A=len B & width A=width B & B - A
  = B holds A=0_Rmatrix(len A,width A);

theorem :: MATRIXR1:40
  for a being Real,A,B being Matrix of REAL st width A=len B holds
  A*(a*B)=a*(A*B);

theorem :: MATRIXR1:41
  for a being Real,A,B being Matrix of REAL
   st width A=len B & len A>0 &
  len B>0 & width B>0 holds (a*A)*B=a*(A*B);

theorem :: MATRIXR1:42
  for M being Matrix of REAL holds M + 0_Rmatrix(len M,width M) = M;

theorem :: MATRIXR1:43
  for a being Real, A,B being Matrix of REAL st len A=len B &
  width A=width B holds a*(A + B) = a*A + a*B;

theorem :: MATRIXR1:44
  for A being Matrix of REAL st len A>0 holds 0 * A = 0_Rmatrix (len A,
  width A);

definition
  let x be FinSequence of REAL;
  assume
 len x > 0;
  func ColVec2Mx x -> Matrix of REAL means
:: MATRIXR1:def 9

  len it=len x & width it=1 & for j st j in dom x holds it.j = <*x.j*>;
end;

theorem :: MATRIXR1:45
  for x being FinSequence of REAL,M being Matrix of REAL st len x>0
  holds M=ColVec2Mx x iff Col(M,1)=x & width M=1;

theorem :: MATRIXR1:46
  for x1,x2 being FinSequence of REAL st len x1=len x2 & len x1>0
  holds ColVec2Mx (x1+x2)=ColVec2Mx (x1)+ColVec2Mx (x2);

theorem :: MATRIXR1:47
  for a being Real,x being FinSequence of REAL st len x>0 holds
  ColVec2Mx (a*x)=a*ColVec2Mx x;

definition
  let x be FinSequence of REAL;
  func LineVec2Mx x -> Matrix of REAL means
:: MATRIXR1:def 10

  width it=len x & len it=1 & for j st j in dom x holds it*(1,j) =x.j;
end;

theorem :: MATRIXR1:48
  for x being FinSequence of REAL, M being Matrix of REAL holds M=
  LineVec2Mx x iff Line(M,1)=x & len M=1;

theorem :: MATRIXR1:49
  for x being FinSequence of REAL st len x>0 holds (LineVec2Mx x)@
  = ColVec2Mx x & (ColVec2Mx x)@=LineVec2Mx x;

theorem :: MATRIXR1:50
  for x1,x2 being FinSequence of REAL st len x1=len x2 holds
  LineVec2Mx (x1+x2)=LineVec2Mx (x1)+LineVec2Mx (x2);

theorem :: MATRIXR1:51
  for a being Real, x being FinSequence of REAL
    holds LineVec2Mx (a*x)=a*LineVec2Mx x;

definition
  let M be Matrix of REAL;
  let x be FinSequence of REAL;
  func M*x -> FinSequence of REAL equals
:: MATRIXR1:def 11
  Col(M*(ColVec2Mx x),1);
  func x*M -> FinSequence of REAL equals
:: MATRIXR1:def 12
  Line((LineVec2Mx x)*M,1);
end;

theorem :: MATRIXR1:52
  for x being FinSequence of REAL, A being Matrix of REAL st len A
  >0 & width A>0 & (len A=len x or width (A@)=len x) holds (A@)*x = x*A;

theorem :: MATRIXR1:53
  for x being FinSequence of REAL,A being Matrix of REAL st len A>
  0 & width A>0 & (width A=len x or len (A@)=len x) holds A*x = x*(A@);

theorem :: MATRIXR1:54
  for A,B being Matrix of REAL st len A=len B holds for i being
  Nat st 1<=i & i<=width A holds Col(A+B,i)=Col(A,i)+Col(B,i);

theorem :: MATRIXR1:55
  for A,B being Matrix of REAL st width A=width B holds for i
  being Nat st 1<=i & i<=len A holds Line(A+B,i)=Line(A,i)+Line(B,i);

theorem :: MATRIXR1:56
  for a being Real, M being (Matrix of REAL), i being Nat st 1<=i
  & i<=width M holds Col(a*M,i)=a*Col(M,i);

theorem :: MATRIXR1:57
  for x1,x2 being FinSequence of REAL, A being Matrix of REAL st len x1=
  len x2 & width A=len x1 & len x1>0 & len A>0 holds A*(x1+x2)=A*x1 + A*x2;

theorem :: MATRIXR1:58
  for x1,x2 being FinSequence of REAL, A being Matrix of REAL st len x1=
  len x2 & len A=len x1 & len x1>0 holds (x1+x2)*A=x1*A + x2*A;

theorem :: MATRIXR1:59
  for a being Real,x being FinSequence of REAL, A being Matrix of
  REAL st width A=len x & len x>0 holds A*(a*x)=a*(A*x);

theorem :: MATRIXR1:60
  for a being Real, x being FinSequence of REAL,
      A being Matrix of REAL
  st len A=len x & len x>0 & width A>0 holds (a*x)*A=a*(x*A);

theorem :: MATRIXR1:61
  for x being FinSequence of REAL, A being Matrix of REAL st width
  A=len x & len x>0 holds len (A*x) = len A;

theorem :: MATRIXR1:62
  for x being FinSequence of REAL, A being Matrix of REAL st len A
  =len x holds len (x*A) = width A;

theorem :: MATRIXR1:63
  for x being FinSequence of REAL, A,B being Matrix of REAL st len
A=len B & width A=width B & width A=len x & len A>0 & len x>0 holds (A+B)*x=A*x
  + B*x;

theorem :: MATRIXR1:64
  for x being FinSequence of REAL, A,B being Matrix of REAL st len
  A=len B & width A=width B & len A=len x & len x>0 holds x*(A+B)=x*A + x*B;

theorem :: MATRIXR1:65
  for n,m being Nat, x being FinSequence of REAL st len x=m &
  n>0 & m>0 holds (0_Rmatrix(n,m))*x=0*n;

theorem :: MATRIXR1:66
  for n,m being Nat, x being FinSequence of REAL st len x=n &
  n>0 holds x*(0_Rmatrix(n,m))=0*m;