Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### 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;
```