:: Calculation of Matrices of Field Elements. Part {I}
:: by Yatsuka Nakamura and Hiroshi Yamazaki
::
:: Received August 8, 2003
:: Copyright (c) 2003-2018 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