:: 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;