:: Calculation of Matrices of Field Elements. Part {I}
:: by Yatsuka Nakamura and Hiroshi Yamazaki
::
:: Received August 8, 2003
:: Copyright (c) 2003-2026 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, FUNCSDOM;
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;
equalities BINOP_1, MATRIX_0, MATRIX_3, ALGSTR_0, MATRIX_1;
theorems FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, NAT_1, ZFMISC_1, XBOOLE_0,
RLVECT_1, MATRIX_1, MATRIX_3, VECTSP_1, FVSUM_1, FINSEQ_2, FUNCOP_1,
FINSEQOP, FUNCT_3, CARD_2, CARD_1, MATRIX_0, ORDINAL1;
begin
reserve i,j for Nat;
definition
::$CD
end;
theorem Th1:
for K being Ring, M being Matrix of K holds --M=M
proof
let K be Ring, M be Matrix of K;
per cases by NAT_1:3;
suppose
A1: len M = 0;
then len -M = 0 by MATRIX_1:def 4;
then len --M = 0 by MATRIX_1:def 4;
hence thesis by A1,CARD_2:64;
end;
suppose
A2: len M>0;
len (-M) = len M & width (-M) = width M by MATRIX_1:def 4;
then
A3: -M is Matrix of len M,width M,K by A2,MATRIX_0:20;
M is Matrix of len M,width M,K by A2,MATRIX_0:20;
then
A4: Indices (-M)=Indices M by A3,MATRIX_0:26;
A5: for i,j st [i,j] in Indices M holds M*(i,j) = (--M)*(i,j)
proof
let i,j;
assume
A6: [i,j] in Indices M;
then (-M)*(i,j)= -(M*(i,j)) by MATRIX_1:def 4;
then (-(-M))*(i,j) = --(M*(i,j)) by A4,A6,MATRIX_1:def 4;
hence thesis by RLVECT_1:17;
end;
width (--M) = width (-M) by MATRIX_1:def 4;
then
A7: width (--M)= width M by MATRIX_1:def 4;
len (--M) = len (-M) by MATRIX_1:def 4;
then len (--M) =len M by MATRIX_1:def 4;
hence thesis by A7,A5,MATRIX_0:21;
end;
end;
theorem Th2:
for K being Ring,M being Matrix of K holds M+(-M)=0.(K,len M, width M)
proof
let K be Ring,M be Matrix of K;
per cases by NAT_1:3;
suppose
len M>0;
then M is Matrix of len M,width M,K by MATRIX_0:20;
hence thesis by MATRIX_3:5;
end;
suppose
A1: len M = 0;
A2: len (M+(-M)) = len M by MATRIX_1:def 6;
len (0.(K,len M,width M)) = 0 by A1;
hence thesis by A1,A2,CARD_2:64;
end;
end;
theorem
for K being Ring,M being Matrix of K holds M - M=0.(K,len M,width M) by Th2;
theorem
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2=width M3 and
A5: M1+M3=M2+M3;
A6: M3+-M3=0.(K,len M1,width M1) by A1,A2,A3,A4,Th2;
M1+(M3+(-M3))=M2+M3+(-M3) by A1,A2,A3,A4,A5,MATRIX_3:3;
then
A7: M1+(M3+-M3)=M2+(M3+(-M3)) by A2,A4,MATRIX_3:3;
per cases by NAT_1:3;
suppose
A8: len M1 > 0;
then M2 is Matrix of len M1,width M1,K by A1,A3,MATRIX_0:20;
then
A9: M2+0.(K,len M1,width M1)=M2 by MATRIX_3:4;
M1 is Matrix of len M1,width M1,K by A8,MATRIX_0:20;
hence thesis by A7,A6,A9,MATRIX_3:4;
end;
suppose
len M1 = 0;
hence thesis by A1,CARD_2:64;
end;
end;
theorem
for K being Ring,M1,M2 being Matrix of K holds M1--M2=M1+M2 by Th1;
theorem :: Th6:
for K being Ring,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)
proof
let K be Ring,M1,M2 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: width M1=width M2 and
A3: M1 = M1 + M2;
0.(K,len M1,width M1)=M1+M2+(-M1) by A3,Th2;
then 0.(K,len M1,width M1)=M2+M1+(-M1) by A1,A2,MATRIX_3:2;
then 0.(K,len M1,width M1)=M2+(M1+(-M1)) by A1,A2,MATRIX_3:3;
then
A4: 0.(K,len M1,width M1)=M2+(0.(K,len M1,width M1)) by Th2;
per cases by NAT_1:3;
suppose
len M1 > 0;
then M2 is Matrix of len M1,width M1,K by A1,A2,MATRIX_0:20;
hence thesis by A4,MATRIX_3:4;
end;
suppose
A5: len M1 = 0;
then len (0.(K,len M1,width M1)) = 0;
hence thesis by A1,A5,CARD_2:64;
end;
end;
theorem Th7:
for K being Ring,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
proof
let K be Ring,M1,M2 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: width M1=width M2 and
A3: M1 - M2 = 0.(K,len M1,width M1);
per cases by NAT_1:3;
suppose
A4: len M1 > 0;
then
A5: M2 is Matrix of len M1,width M1,K by A1,A2,MATRIX_0:20;
A6: len (-M2)=len M2 & width (-M2)=width (M2) by MATRIX_1:def 4;
A7: len (0.(K,len M1,width M1))=len M1 by MATRIX_0:def 2;
then width (0.(K,len M1,width M1))=width M1 by A4,MATRIX_0:20;
then M1+(-M2)+M2 = M2+0.(K,len M1,width M1) by A1,A2,A3,A7,MATRIX_3:2
.=M2 by A5,MATRIX_3:4;
then M1+((-M2)+M2)=M2 by A1,A2,A6,MATRIX_3:3;
then M1+(M2+(-M2))=M2 by A6,MATRIX_3:2;
then
A8: M1+(0.(K,len M1,width M1))=M2 by A5,MATRIX_3:5;
M1 is Matrix of len M1,width M1,K by A4,MATRIX_0:20;
hence thesis by A8,MATRIX_3:4;
end;
suppose
len M1 = 0;
hence thesis by A1,CARD_2:64;
end;
end;
theorem Th8:
for K being Ring,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
proof
let K be Ring,M1,M2 be Matrix of K;
assume that
A1: len M1=len M2 & width M1=width M2 and
A2: M1+M2= 0.(K,len M1,width M1);
A3: len (-M2)=len M2 & width (-M2)=width M2 by MATRIX_1:def 4;
M1-(-M2)= 0.(K,len M1,width M1) by A2,Th1;
then M1=-M2 by A1,A3,Th7;
hence thesis by Th1;
end;
theorem Th9:
for n,m being Nat,K being Ring holds -(0.(K,n,m))=0.( K,n,m)
proof
let n,m be Nat,K be Ring;
per cases by NAT_1:3;
suppose
A1: n>0;
A2: 0.(K,n,m) + 0.(K,n,m) = 0.(K,n,m) by MATRIX_3:4;
A3: len (0.(K,n,m))=n by MATRIX_0:def 2;
then width (0.(K,n,m))=m by A1,MATRIX_0:20;
hence thesis by A3,A2,Th8;
end;
suppose
n = 0;
then
A4: len (0.(K,n,m)) = 0;
then len (-(0.(K,n,m))) = 0 by MATRIX_1:def 4;
hence thesis by A4,CARD_2:64;
end;
end;
theorem
for K being Ring,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)
proof
let K be Ring,M1,M2 be Matrix of K;
assume that
A1: len M1=len M2 & width M1=width M2 and
A2: M2 - M1 = M2;
per cases by NAT_1:3;
suppose
A3: len M1 > 0;
A4: len (-M1)=len M1 & width (-M1)=width (M1) by MATRIX_1:def 4;
A5: M2 is Matrix of len M1, width M1, K by A1,A3,MATRIX_0:20;
then M2+(-M1)+(-M2) = 0.(K,len M1,width M1) by A2,MATRIX_3:5;
then (-M1)+M2+(-M2) = 0.(K,len M1,width M1) by A1,A4,MATRIX_3:2;
then (-M1)+(M2+(-M2)) = 0.(K,len M1,width M1) by A1,A4,MATRIX_3:3;
then
A6: -M1+ (0.(K,len M1,width M1))=0.(K,len M1,width M1) by A5,MATRIX_3:5;
-M1 is Matrix of len M1,width M1,K by A3,A4,MATRIX_0:20;
then -M1= 0.(K,len M1,width M1) by A6,MATRIX_3:4;
then M1=- 0.(K,len M1,width M1) by Th1;
hence thesis by Th9;
end;
suppose
A7: len M1 = 0;
then len (0.(K,len M1,width M1)) = 0;
hence thesis by A7,CARD_2:64;
end;
end;
theorem Th11:
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 &
width M1=width M2 holds M1 = M1 -(M2 - M2)
proof
let K be Ring,M1,M2 be Matrix of K;
assume len M1=len M2 & width M1=width M2;
then
A1: M1 -(M2 - M2)=M1-0.(K,len M1,width M1) by Th2
.=M1+0.(K,len M1,width M1) by Th9;
per cases by NAT_1:3;
suppose
len M1 > 0;
then M1 is Matrix of len M1,width M1,K by MATRIX_0:20;
hence thesis by A1,MATRIX_3:4;
end;
suppose
A2: len M1 = 0;
then len (M1 - (M2 - M2)) = 0 by MATRIX_1:def 6;
hence thesis by A2,CARD_2:64;
end;
end;
theorem Th12:
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 &
width M1=width M2 holds -(M1 + M2) = -M1+-M2
proof
let K be Ring,M1,M2 be Matrix of K;
assume
A1: len M1=len M2 & width M1=width M2;
A2: width (-M1)=width M1 by MATRIX_1:def 4;
then
A3: width (-M1+-M2)=width M1 by MATRIX_1:def 6;
A4: len (M1+M2)=len M1 & width (M1+M2)=width M1 by MATRIX_1:def 6;
A5: len (-M1)=len M1 by MATRIX_1:def 4;
then
A6: len (-M1+-M2)=len M1 by MATRIX_1:def 6;
A7: len (-M2)=len M2 & width (-M2)=width M2 by MATRIX_1:def 4;
per cases by NAT_1:3;
suppose
A8: len M1 > 0;
then
A9: M2 is Matrix of len M1,width M1,K by A1,MATRIX_0:20;
A10: M1 is Matrix of len M1,width M1,K by A8,MATRIX_0:20;
M1+M2 +(-M1+-M2) =M1+M2+(-M2+-M1) by A1,A5,A2,A7,MATRIX_3:2
.=M1+M2+-M2+-M1 by A1,A7,A4,MATRIX_3:3
.=M1+(M2+-M2)+-M1 by A1,MATRIX_3:3
.=M1+0.(K,len M1,width M1)+-M1 by A9,MATRIX_3:5
.=M1+-M1 by A10,MATRIX_3:4
.=0.(K,len M1,width M1) by A10,MATRIX_3:5;
hence thesis by A4,A6,A3,Th8;
end;
suppose
A11: len M1 = 0;
then len (-M1) = 0 by MATRIX_1:def 4;
then
A12: len (-M1+-M2) = 0 by MATRIX_1:def 6;
len (M1+M2) = 0 by A11,MATRIX_1:def 6;
then len -(M1+M2) = 0 by MATRIX_1:def 4;
hence thesis by A12,CARD_2:64;
end;
end;
theorem
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 & width M1=
width M2 holds M1 - (M1 - M2) = M2
proof
let K be Ring,M1,M2 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: width M1=width M2;
A3: len (-M1)=len M1 & width (-M1)=width M1 by MATRIX_1:def 4;
A4: len (-M2)=len M2 & width (-M2)=width M2 by MATRIX_1:def 4;
per cases by NAT_1:3;
suppose
A5: len M1 > 0;
A6: len (0.(K,len M1,width M1))=len M1 by MATRIX_0:def 2;
then
A7: width (0.(K,len M1,width M1))=width M1 by A5,MATRIX_0:20;
A8: M2 is Matrix of len M1,width M1,K by A1,A2,A5,MATRIX_0:20;
A9: M1 is Matrix of len M1,width M1,K by A5,MATRIX_0:20;
M1 - (M1 - M2)=M1+(-M1+--M2) by A1,A2,A4,Th12
.=M1+(-M1+M2) by Th1
.=M1+-M1+M2 by A3,MATRIX_3:3
.=0.(K,len M1,width M1)+M2 by A9,MATRIX_3:5
.=M2+0.(K,len M1,width M1) by A1,A2,A6,A7,MATRIX_3:2
.=M2 by A8,MATRIX_3:4;
hence thesis;
end;
suppose
A10: len M1 = 0;
then len (M1 - (M1 - M2)) = 0 by MATRIX_1:def 6;
hence thesis by A1,A10,CARD_2:64;
end;
end;
theorem Th14:
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3 and
A5: M1 - M3 = M2 - M3;
A6: len (-M3)=len M3 & width (-M3)=width M3 by MATRIX_1:def 4;
per cases by NAT_1:3;
suppose
A7: len M1 > 0;
then
A8: M2 is Matrix of len M1,width M1,K by A1,A3,MATRIX_0:20;
A9: M3 is Matrix of len M1,width M1,K by A1,A2,A3,A4,A7,MATRIX_0:20;
M1+-M3+M3=M2+(-M3+M3) by A2,A4,A5,A6,MATRIX_3:3;
then M1+-M3+M3=M2+(M3+-M3) by A6,MATRIX_3:2;
then M1+-M3+M3=M2+0.(K,len M1,width M1) by A9,MATRIX_3:5;
then M1+-M3+M3=M2 by A8,MATRIX_3:4;
then M1+(-M3+M3)=M2 by A1,A2,A3,A4,A6,MATRIX_3:3;
then M1+(M3+-M3)=M2 by A6,MATRIX_3:2;
then
A10: M1+0.(K,len M1,width M1)=M2 by A9,MATRIX_3:5;
M1 is Matrix of len M1,width M1,K by A7,MATRIX_0:20;
hence thesis by A10,MATRIX_3:4;
end;
suppose
len M1 = 0;
hence thesis by A1,CARD_2:64;
end;
end;
theorem Th15:
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3 and
A5: M3 - M1 = M3 - M2;
per cases by NAT_1:3;
suppose
A6: len M1>0;
then
A7: M3 is Matrix of len M1,width M1,K by A1,A2,A3,A4,MATRIX_0:20;
A8: len (-M2)=len M2 & width (-M2)=width M2 by MATRIX_1:def 4;
then
A9: -M2 is Matrix of len M1,width M1,K by A1,A3,A6,MATRIX_0:20;
A10: len (-M1)=len M1 & width (-M1)=width M1 by MATRIX_1:def 4;
then -M1+M3=M3+-M2 by A1,A2,A3,A4,A5,MATRIX_3:2;
then -M1+M3=-M2+M3 by A2,A4,A8,MATRIX_3:2;
then -M1+M3+-M3=-M2+(M3+-M3) by A2,A4,A8,MATRIX_3:3;
then -M1+M3+-M3=-M2+0.(K,len M1,width M1) by A7,MATRIX_3:5;
then -M1+M3+-M3=-M2 by A9,MATRIX_3:4;
then -M1+(M3+-M3)=-M2 by A1,A2,A3,A4,A10,MATRIX_3:3;
then
A11: -M1+0.(K,len M1,width M1)=-M2 by A7,MATRIX_3:5;
-M1 is Matrix of len M1,width M1,K by A6,A10,MATRIX_0:20;
then -M1=-M2 by A11,MATRIX_3:4;
then --M1=M2 by Th1;
hence thesis by Th1;
end;
suppose
len M1=0;
hence thesis by A1,CARD_2:64;
end;
end;
theorem Th16:
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
A5: len (-M3)=len M3 & width (-M3)=width M3 by MATRIX_1:def 4;
A6: len (-M2)=len M2 & width (-M2)=width M2 by MATRIX_1:def 4;
hence M1 - M2 - M3 =M1+(-M2+-M3) by A1,A3,MATRIX_3:3
.=M1+(-M3+-M2) by A2,A4,A6,A5,MATRIX_3:2
.= M1 - M3 - M2 by A1,A2,A3,A4,A5,MATRIX_3:3;
end;
theorem
for K being Ring,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)
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
A5: len (-M2)=len M2 & width (-M2)=width M2 by MATRIX_1:def 4;
A6: len (-M3)=len M3 & width (-M3)=width M3 by MATRIX_1:def 4;
per cases by NAT_1:3;
suppose
A7: len M1>0;
then
A8: M2 is Matrix of len M1,width M1,K by A1,A3,MATRIX_0:20;
A9: len (M1+-M2)=len M1 & width (M1+-M2)=width M1 by MATRIX_1:def 6;
A10: M1 is Matrix of len M1,width M1,K by A7,MATRIX_0:20;
(M1 - M2) - (M3 - M2)=M1+-M2+(-M3+--M2) by A2,A4,A5,Th12
.=M1+-M2+(-M3+M2) by Th1
.=M1+-M2+(M2+-M3) by A2,A4,A6,MATRIX_3:2
.=M1+-M2+M2+-M3 by A1,A3,A9,MATRIX_3:3
.=M1+(-M2+M2)+-M3 by A1,A3,A5,MATRIX_3:3
.=M1+(M2+-M2)+-M3 by A5,MATRIX_3:2
.=M1+0.(K,len M1,width M1)+-M3 by A8,MATRIX_3:5
.=M1+-M3 by A10,MATRIX_3:4;
hence thesis;
end;
suppose
A11: len M1 = 0;
then len (M1-M2) = 0 by MATRIX_1:def 6;
then
A12: len ((M1 - M2) - (M3 - M2)) = 0 by MATRIX_1:def 6;
len (M1-M3) = 0 by A11,MATRIX_1:def 6;
hence thesis by A12,CARD_2:64;
end;
end;
theorem Th18:
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
per cases by NAT_1:3;
suppose
A5: len M1>0;
then
A6: M3 is Matrix of len M1,width M1,K by A1,A2,A3,A4,MATRIX_0:20;
A7: len (-M2)=len M2 & width (-M2)=width M2 by MATRIX_1:def 4;
A8: width (-M1)=width M1 by MATRIX_1:def 4;
then
A9: width (-M1+M3)=width M1 by MATRIX_1:def 6;
A10: len (-M3)=len M3 & width (-M3)=width M3 by MATRIX_1:def 4;
A11: len (-M1)=len M1 by MATRIX_1:def 4;
then
A12: len (-M1+M3)=len M1 by MATRIX_1:def 6;
A13: -M1 is Matrix of len M1,width M1,K by A5,A11,A8,MATRIX_0:20;
(M3 - M1) - (M3 - M2)=(-M1+M3)-(M3+-M2) by A1,A2,A3,A4,A11,A8,MATRIX_3:2
.=(-M1+M3)+(-M3+--M2) by A2,A4,A7,Th12
.=(-M1+M3)+(-M3+M2) by Th1
.=(-M1+M3)+-M3+M2 by A1,A2,A3,A4,A10,A12,A9,MATRIX_3:3
.=-M1+(M3+-M3)+M2 by A1,A2,A3,A4,A11,A8,MATRIX_3:3
.=-M1+(0.(K,len M1,width M1))+M2 by A6,MATRIX_3:5
.=-M1+M2 by A13,MATRIX_3:4
.=M2+-M1 by A1,A3,A11,A8,MATRIX_3:2;
hence thesis;
end;
suppose
A14: len M1=0;
A15: len (M2 - M1) = len M2 by MATRIX_1:def 6;
len ((M3 - M1) - (M3 - M2)) = len (M3 - M1) by MATRIX_1:def 6
.= len M3 by MATRIX_1:def 6;
hence thesis by A1,A2,A14,A15,CARD_2:64;
end;
end;
theorem
for K being Ring,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
proof
let K be Ring,M1,M2,M3,M4 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: len M3=len M4 and
A4: width M1=width M2 and
A5: width M2 = width M3 and
A6: width M3=width M4 and
A7: M1 - M2 = M3 - M4;
A8: len (-M4)=len M1 & width (-M4)=width M1 by A1,A2,A3,A4,A5,A6,MATRIX_1:def 4
;
A9: len (M3+-M4)=len M1 & width (M3+-M4)=width M1 by A1,A2,A4,A5,MATRIX_1:def 6
;
A10: len (-M2)=len M2 & width (-M2)=width M2 by MATRIX_1:def 4;
A11: len (M1+-M3)=len M1 & width (M1+-M3)=width M1 by MATRIX_1:def 6;
A12: len (M1+-M2)=len M1 & width (M1+-M2)=width M1 by MATRIX_1:def 6;
A13: len (M1+-M3)=len M1 & width (M1+-M3)=width M1 by MATRIX_1:def 6;
A14: len (M2+-M4)=len M1 & width (M2+-M4)=width M1 by A1,A4,MATRIX_1:def 6;
A15: len (-M3)=len M3 & width (-M3)=width M3 by MATRIX_1:def 4;
per cases by NAT_1:3;
suppose
len M1 > 0;
then M3+-M4 is Matrix of len M1,width M1,K by A9,MATRIX_0:20;
then M1+-M2+-(M3 +- M4)=0.(K,len M1,width M1) by A7,MATRIX_3:5;
then M1+-M2+(-M3 +-- M4)=0.(K,len M1,width M1) by A1,A2,A4,A5,A8,Th12;
then M1+-M2+(-M3 + M4)=0.(K,len M1,width M1) by Th1;
then M1+-M2+-M3 + M4=0.(K,len M1,width M1) by A1,A2,A4,A5,A15,A12,
MATRIX_3:3;
then M1+(-M2+-M3) + M4=0.(K,len M1,width M1) by A1,A4,A10,MATRIX_3:3;
then M1+(-M3+-M2) + M4=0.(K,len M1,width M1) by A2,A5,A10,A15,MATRIX_3:2;
then M1+-M3+-M2 + M4=0.(K,len M1,width M1) by A1,A2,A4,A5,A15,MATRIX_3:3;
then M1+-M3+(-M2 + M4)=0.(K,len M1,width M1) by A1,A4,A10,A11,MATRIX_3:3;
then M1+-M3+(-M2 + --M4)=0.(K,len M1,width M1) by Th1;
then M1+-M3-(M2 + -M4)=0.(K,len M1,width M1) by A1,A4,A8,Th12;
hence thesis by A13,A14,Th7;
end;
suppose
len M1 = 0;
then len (M1 - M3) = 0 & len (M2 - M4) = 0 by A1,MATRIX_1:def 6;
hence thesis by CARD_2:64;
end;
end;
theorem Th20:
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 &
width M1=width M2 holds M1 = M1 + (M2 - M2)
proof
let K be Ring,M1,M2 be Matrix of K;
assume
A1: len M1=len M2 & width M1=width M2;
per cases by NAT_1:3;
suppose
A2: len M1>0;
then
A3: M1 is Matrix of len M1,width M1,K by MATRIX_0:20;
M2 is Matrix of len M1,width M1,K by A1,A2,MATRIX_0:20;
hence M1+(M2-M2)=M1+0.(K,len M1,width M1) by MATRIX_3:5
.=M1 by A3,MATRIX_3:4;
end;
suppose
A4: len M1 = 0;
len (M1 + (M2 - M2)) = len M1 by MATRIX_1:def 6;
hence thesis by A4,CARD_2:64;
end;
end;
theorem Th21:
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 &
width M1=width M2 holds M1 = M1 + M2 - M2
proof
let K be Ring,M1,M2 be Matrix of K;
assume
A1: len M1=len M2 & width M1=width M2;
hence M1+M2-M2= M1+(M2-M2) by MATRIX_3:3
.=M1 by A1,Th20;
end;
theorem Th22:
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 &
width M1=width M2 holds M1 = M1 - M2 + M2
proof
let K be Ring,M1,M2 be Matrix of K;
assume
A1: len M1=len M2 & width M1=width M2;
then
A2: len (-M2)=len M1 & width (-M2)=width M1 by MATRIX_1:def 4;
hence M1 - M2 + M2=M1+(-M2+M2) by MATRIX_3:3
.=M1+(M2-M2) by A1,A2,MATRIX_3:2
.=M1 by A1,Th20;
end;
theorem
for K being Ring,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)
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2=width M3;
A5: len (M1+M2)=len M1 & width (M1+M2)=width M1 by MATRIX_1:def 6;
A6: len (-M2)=len M1 & width (-M2)=width M1 by A1,A3,MATRIX_1:def 4;
hence (M1 + M2) + (M3 - M2)=M1+M2+(-M2+M3) by A1,A2,A3,A4,MATRIX_3:2
.=M1+M2+-M2+M3 by A6,A5,MATRIX_3:3
.=M1+(M2-M2)+M3 by A1,A3,MATRIX_3:3
.=M1+M3 by A1,A3,Th20;
end;
theorem
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
A5: len (-M3)=len M1 & width (-M3)=width M1 by A1,A2,A3,A4,MATRIX_1:def 4;
thus M1 + M2 - M3 =M1+(M2+-M3) by A1,A3,MATRIX_3:3
.=M1+(-M3+M2) by A1,A3,A5,MATRIX_3:2
.= M1 - M3 + M2 by A5,MATRIX_3:3;
end;
theorem
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
A5: len (-M2)=len M1 & width (-M2)=width M1 by A1,A3,MATRIX_1:def 4;
hence M1 - M2 + M3 =-M2+M1+M3 by MATRIX_3:2
.=-M2+(M1+M3) by A5,MATRIX_3:3
.=-M2+(M3+M1) by A1,A2,A3,A4,MATRIX_3:2
.=-M2+M3+M1 by A1,A2,A3,A4,A5,MATRIX_3:3
.=M3 - M2 + M1 by A1,A2,A3,A4,A5,MATRIX_3:2;
end;
theorem Th26:
for K being Ring,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)
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
per cases by NAT_1:3;
suppose
A5: len M1 > 0;
then
A6: M2 is Matrix of len M1,width M1,K by A1,A3,MATRIX_0:20;
A7: len (-M2)=len M1 & width (-M2)=width M1 by A1,A3,MATRIX_1:def 4;
A8: len (-M3)=len M1 & width (-M3)=width M1 by A1,A2,A3,A4,MATRIX_1:def 4;
A9: len (M1+M2)=len M1 & width (M1+M2)=width M1 by MATRIX_1:def 6;
M1 is Matrix of len M1,width M1,K by A5,MATRIX_0:20;
hence M1 + M3 = M1+0.(K,len M1,width M1)+M3 by MATRIX_3:4
.=M1+(M2+-M2)+M3 by A6,MATRIX_3:5
.=M1+M2+-M2+M3 by A1,A3,MATRIX_3:3
.=M1+M2+(-M2+M3) by A7,A9,MATRIX_3:3
.=M1+M2+(-M2+--M3) by Th1
.=(M1 + M2) - (M2 - M3) by A1,A3,A8,Th12;
end;
suppose
A10: len M1 = 0;
A11: len ((M1 + M2) - (M2 - M3)) = len (M1 + M2) by MATRIX_1:def 6
.= len M1 by MATRIX_1:def 6;
len (M1 + M3) = len M1 by MATRIX_1:def 6;
hence thesis by A10,A11,CARD_2:64;
end;
end;
theorem
for K being Ring,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)
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
len (-M3)=len M1 & width (-M3)=width M1 by A1,A2,A3,A4,MATRIX_1:def 4;
hence M1 - M3 = (M1+M2)-(M2-(-M3)) by A1,A3,Th26
.=(M1+M2)-(M2+M3) by Th1
.=(M1 + M2) - (M3 + M2) by A2,A4,MATRIX_3:2;
end;
theorem Th28:
for K being Ring,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
proof
let K be Ring,M1,M2,M3,M4 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: len M3=len M4 and
A4: width M1=width M2 and
A5: width M2 = width M3 and
A6: width M3=width M4 and
A7: M1 + M2 = M3 + M4;
A8: len (-M2)=len M1 & width (-M2)=width M1 by A1,A4,MATRIX_1:def 4;
M1+M2=M4+M3 by A3,A6,A7,MATRIX_3:2;
then M1+M2+-M2=M4+(M3+-M2) by A3,A6,MATRIX_3:3;
then M1+M2+-M2=M4+(-M2+M3) by A1,A2,A4,A5,A8,MATRIX_3:2;
then M1+(M2-M2)=M4+(-M2+M3) by A1,A4,MATRIX_3:3;
then M1=M4+(-M2+M3) by A1,A4,Th20;
then
A9: M1=M4+-M2+M3 by A1,A2,A3,A4,A5,A6,A8,MATRIX_3:3;
len (M4+-M2)=len M1 & width (M4+-M2)=width M1 by A1,A2,A3,A4,A5,A6,
MATRIX_1:def 6;
hence thesis by A1,A2,A4,A5,A9,Th21;
end;
theorem
for K being Ring,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
proof
let K be Ring,M1,M2,M3,M4 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: len M3=len M4 and
A4: width M1=width M2 and
A5: width M2 = width M3 and
A6: width M3=width M4 and
A7: M1 - M3 = M4 - M2;
A8: len (-M3)=len M1 & width (-M3)=width M1 by A1,A2,A4,A5,MATRIX_1:def 4;
A9: len (-M2)=len M1 & width (-M2)=width M1 by A1,A4,MATRIX_1:def 4;
then M1+-M3=-M2+M4 by A1,A2,A3,A4,A5,A6,A7,MATRIX_3:2;
then M1--M2=M4--M3 by A1,A2,A3,A4,A5,A6,A9,A8,Th28;
then M1+M2=M4--M3 by Th1;
then M1+M2=M4+M3 by Th1;
hence thesis by A3,A6,MATRIX_3:2;
end;
theorem
for K being Ring,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
proof
let K be Ring,M1,M2,M3,M4 be Matrix of K;
assume that
A1: len M1=len M2 & len M2=len M3 and
A2: len M3=len M4 and
A3: width M1=width M2 & width M2 = width M3 and
A4: width M3=width M4 and
A5: M1 + M2 = M3 - M4;
A6: len (-M4)=len M1 & width (-M4)=width M1 by A1,A2,A3,A4,MATRIX_1:def 4;
then M1+M2=-M4+M3 by A1,A3,A5,MATRIX_3:2;
then M1--M4=M3-M2 by A1,A3,A6,Th28;
hence thesis by Th1;
end;
theorem Th31:
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
A5: len (-M2)=len M1 & width (-M2)=width M1 by A1,A3,MATRIX_1:def 4;
M1-(M2+M3)=M1+(-M2+-M3) by A2,A4,Th12
.=M1-M2+-M3 by A5,MATRIX_3:3;
hence thesis;
end;
theorem
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
len (-M3)=len M1 & width (-M3)=width M1 by A1,A2,A3,A4,MATRIX_1:def 4;
then M1-(M2-M3)= M1-M2--M3 by A1,A3,Th31
.=M1+-M2+M3 by Th1;
hence thesis;
end;
theorem
for K being Ring,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)
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume that
A1: len M1=len M2 and
A2: len M2=len M3 and
A3: width M1=width M2 and
A4: width M2 = width M3;
A5: len (-M3)=len M1 & width (-M3)=width M1 by A1,A2,A3,A4,MATRIX_1:def 4;
then M1-(M2-M3)=M1+-(-M3+M2) by A1,A3,MATRIX_3:2
.=M1+(--M3+-M2) by A1,A3,A5,Th12
.=M1+(M3+-M2) by Th1;
hence thesis;
end;
theorem
for K being Ring,M1,M2,M3 being Matrix of K st len M1=len M2 & width
M1=width M2 holds M1 - M3 = (M1-M2)+(M2 - M3)
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume
A1: len M1=len M2 & width M1=width M2;
then
A2: len (-M2)=len M1 & width (-M2)=width M1 by MATRIX_1:def 4;
len (M1+-M2)=len M1 & width (M1+-M2)=width M1 by MATRIX_1:def 6;
then (M1-M2)+(M2 - M3)=M1+-M2+M2+-M3 by A1,MATRIX_3:3
.=M1+(-M2+M2)+-M3 by A2,MATRIX_3:3
.=M1+(M2-M2)+-M3 by A1,A2,MATRIX_3:2
.=M1+-M3 by A1,Th20;
hence thesis;
end;
theorem
for K being Ring,M1,M2,M3 being Matrix of K st -M1=-M2 holds M1=M2
proof
let K be Ring,M1,M2,M3 be Matrix of K;
assume -M1=-M2;
then --M1=M2 by Th1;
hence thesis by Th1;
end;
theorem
for K being Ring,M being Matrix of K st -M=0.(K,len M,width M) holds
M = 0.(K,len M,width M)
proof
let K be Ring,M be Matrix of K;
assume -M=0.(K,len M,width M);
then --M = 0.(K,len M,width M) by Th9;
hence thesis by Th1;
end;
theorem
for K being Ring,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
proof
let K be Ring,M1,M2 be Matrix of K;
assume that
A1: len M1=len M2 & width M1=width M2 and
A2: M1 + -M2 = 0.(K,len M1,width M1);
M1-M2=0.(K,len M1,width M1) by A2;
hence thesis by A1,Th7;
end;
theorem Th38:
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 &
width M1=width M2 holds M1=M1+M2+(-M2)
proof
let K be Ring,M1,M2 be Matrix of K;
A1: M1+M2+(-M2)=M1+M2-M2;
assume len M1=len M2 & width M1=width M2;
hence thesis by A1,Th21;
end;
theorem
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 & width M1=
width M2 holds M1=M1+(M2 + -M2)
proof
let K be Ring,M1,M2 be Matrix of K;
A1: M1+(M2 + -M2)=M1+(M2-M2);
assume len M1=len M2 & width M1=width M2;
hence thesis by A1,Th20;
end;
theorem
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 & width M1=
width M2 holds M1=(-M2+M1)+M2
proof
let K be Ring,M1,M2 be Matrix of K;
assume
A1: len M1=len M2 & width M1=width M2;
then len (-M2)=len M1 & width (-M2)=width M1 by MATRIX_1:def 4;
then (-M2+M1)+M2=M1-M2+M2 by MATRIX_3:2;
hence thesis by A1,Th22;
end;
theorem
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 & width M1=
width M2 holds -(-M1+M2)=M1+-M2
proof
let K be Ring,M1,M2 be Matrix of K;
A1: len (-M1)=len M1 & width (-M1)=width M1 by MATRIX_1:def 4;
assume len M1=len M2 & width M1=width M2;
then -(-M1+M2)=--M1+-M2 by A1,Th12;
hence thesis by Th1;
end;
theorem
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 & width M1=
width M2 holds M1+M2=-(-M1+-M2)
proof
let K be Ring,M1,M2 be Matrix of K;
assume len M1=len M2 & width M1=width M2;
then
A1: len (-M2)=len M1 & width (-M2)=width M1 by MATRIX_1:def 4;
len (-M1)=len M1 & width (-M1)=width M1 by MATRIX_1:def 4;
then -(-M1+-M2)=--M1+--M2 by A1,Th12
.=M1+--M2 by Th1;
hence thesis by Th1;
end;
theorem
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 & width M1=
width M2 holds -(M1 - M2) = M2 - M1
proof
let K be Ring,M1,M2 be Matrix of K;
A1: len (-M1)=len M1 & width (-M1)=width M1 by MATRIX_1:def 4;
assume
A2: len M1=len M2 & width M1=width M2;
then len (-M2)=len M1 & width (-M2)=width M1 by MATRIX_1:def 4;
then -(M1-M2)=-M1+--M2 by Th12
.=-M1+M2 by Th1
.=M2+-M1 by A2,A1,MATRIX_3:2;
hence thesis;
end;
theorem Th44:
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 &
width M1=width M2 holds - M1 - M2 = - M2 - M1
proof
let K be Ring,M1,M2 be Matrix of K;
assume len M1=len M2 & width M1=width M2;
then
A1: len (-M2)=len M1 & width (-M2)=width M1 by MATRIX_1:def 4;
len (-M1)=len M1 & width (-M1)=width M1 by MATRIX_1:def 4;
hence thesis by A1,MATRIX_3:2;
end;
theorem
for K being Ring,M1,M2 being Matrix of K st len M1=len M2 & width M1=
width M2 holds M1 = - M2 - (- M1 - M2)
proof
let K be Ring,M1,M2 be Matrix of K;
A1: len (M1+M2)=len M1 & width (M1+M2)=width M1 by MATRIX_1:def 6;
assume
A2: len M1=len M2 & width M1=width M2;
then
A3: len (-M2)=len M1 & width (-M2)=width M1 by MATRIX_1:def 4;
len (-M1)=len M1 & width (-M1)=width M1 by MATRIX_1:def 4;
then -M2-(-M1-M2)=-M2+(--M1+--M2) by A3,Th12
.=-M2+(M1+--M2) by Th1
.=-M2+(M1+M2) by Th1
.=M1+M2+-M2 by A3,A1,MATRIX_3:2;
hence thesis by A2,Th38;
end;
theorem Th46:
for K being Ring,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
proof
let K be Ring,M1,M2,M3 be Matrix of K;
A1: len (-M1)=len M1 & width (-M1)=width M1 by MATRIX_1:def 4;
assume
len M1=len M2 & len M2=len M3 & width M1=width M2 & width M2 = width M3;
hence thesis by A1,Th16;
end;
theorem Th47:
for K being Ring, 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
proof
let K be Ring, M1, M2, M3 be Matrix of K such that
A1: len M1 = len M2 and
A2: len M2 = len M3 and
A3: width M1 = width M2 and
A4: width M2 = width M3;
- M1 - M2 - M3 = - M2 - M1 - M3 by A1,A3,Th44;
hence thesis by A1,A2,A3,A4,Th46;
end;
theorem
for K being Ring, 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
proof
let K be Ring, M1, M2, M3 be Matrix of K;
assume
A1: len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 =
width M3;
then - M1 - M2 - M3 = - M1 - M3 - M2 by Th46;
hence thesis by A1,Th47;
end;
theorem
for K being Ring, 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)
proof
let K be Ring, M1, M2, M3 be Matrix of K;
assume that
A1: len M1 = len M2 and
A2: len M2 = len M3 and
A3: width M1 = width M2 and
A4: width M2 = width M3;
A5: len (-M1) = len M1 & width (-M1) = width M1 by MATRIX_1:def 4;
A6: len (-M2) = len M2 & width (-M2) = width M2 by MATRIX_1:def 4;
(M3 - M1) - (M3 - M2) = M2 - M1 by A1,A2,A3,A4,Th18
.= (- M1) + M2 by A1,A3,A5,MATRIX_3:2
.= (- M1) +--M2 by Th1
.= - (M1 + -M2) by A1,A3,A6,Th12;
hence thesis;
end;
theorem
for K being Ring, M being Matrix of K holds 0.(K, len M, width M) - M = - M
proof
let K be Ring, M be Matrix of K;
A1: len (-M) = len M by MATRIX_1:def 4;
A2: width (-M) = width M by MATRIX_1:def 4;
A3: len (0.(K, len M, width M)) = len M by MATRIX_0:def 2;
per cases by NAT_1:3;
suppose
A4: len M>0;
then width (0.(K, len M, width M)) = width M by A3,MATRIX_0:20;
then
A5: 0.(K, len M, width M) - M = (-M) + 0.(K, len M, width M) by A1,A2,A3,
MATRIX_3:2;
-M is Matrix of len M, width M, K by A1,A2,A4,MATRIX_0:20;
hence thesis by A5,MATRIX_3:4;
end;
suppose
A6: len M = 0;
len (0.(K, len M, width M) - M) = len (0.(K, len M, width M)) by
MATRIX_1:def 6;
hence thesis by A1,A3,A6,CARD_2:64;
end;
end;
theorem
for K being Ring, M1, M2 being Matrix of K st len M1 = len M2 & width
M1 = width M2 holds M1 + M2 = M1 - - M2 by Th1;
theorem
for K being Ring, M1, M2 being Matrix of K st len M1 = len M2 & width
M1 = width M2 holds M1 = M1 - (M2 + -M2)
proof
let K be Ring, M1, M2 be Matrix of K;
assume len M1 = len M2 & width M1 = width M2;
then M1 = M1 - (M2 - M2) by Th11;
hence thesis;
end;
theorem
for K being Ring, 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
proof
let K be Ring, M1, M2, M3 be Matrix of K;
assume that
A1: len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 =
width M3 and
A2: M1 - M3 = M2 + - M3;
M1 - M3 = M2 - M3 by A2;
hence thesis by A1,Th14;
end;
theorem
for K being Ring, 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
proof
let K be Ring, M1, M2, M3 be Matrix of K such that
A1: len M1 = len M2 & len M2 = len M3 & width M1 = width M2 & width M2 =
width M3 and
A2: M3 - M1 = M3 + - M2;
M3 - M1 = M3 - M2 by A2;
hence thesis by A1,Th15;
end;
theorem Th55:
for K being set, A,B being Matrix of K st len A=len B & width A=
width B holds Indices A=Indices B
proof
let K be set,A,B be Matrix of K;
A1: dom A = Seg len A by FINSEQ_1:def 3;
assume len A=len B & width A=width B;
hence thesis by A1,FINSEQ_1:def 3;
end;
theorem Th56: :: EUCLID_2:9
for K being Ring,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)
proof
let K be Ring,x,y,z be FinSequence of K;
assume that
A1: len x=len y and
A2: len y=len z;
A3: dom z=Seg len x by A1,A2,FINSEQ_1:def 3;
reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on the carrier of K
by A1,A2,FINSEQ_2:92;
A4: dom (x+y) = Seg len (x2+y2) by FINSEQ_1:def 3
.=dom z by A1,A2,CARD_1:def 7,FINSEQ_1:def 3;
A5: dom (mlt(y,z))=Seg len(mlt(y2,z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7;
then
A6: dom (mlt(y,z))=Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
A7: dom x =Seg len x by FINSEQ_1:def 3;
A8: dom y=Seg len x by A1,FINSEQ_1:def 3;
A9: dom (mlt(x,z))=Seg len(mlt(x2,z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7;
then
A10: dom (mlt(x,z)) =Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
A11: for i being Nat st i in dom (mlt(x+y,z)) holds mlt(x+y,z).i = (mlt(x,z)
+mlt(y,z)).i
proof
let i be Nat;
A12: rng x c= the carrier of K & rng y c= the carrier of K by FINSEQ_1:def 4;
A13: rng z c= the carrier of K & rng (x+y) c= the carrier of K by
FINSEQ_1:def 4;
dom (the multF of K) = [:the carrier of K,the carrier of K:] by
FUNCT_2:def 1;
then mlt(x+y,z)=(the multF of K).:(x+y,z) & [:rng (x+y),rng z:] c= dom (
the multF of K) by A13,FVSUM_1:def 7,ZFMISC_1:96;
then
A14: dom (mlt(x+y,z)) = dom(x+y) /\ dom z by FUNCOP_1:69;
assume
A15: i in dom mlt(x+y,z);
then i in dom z by A14,XBOOLE_0:def 4;
then
A16: z.i in rng z by FUNCT_1:def 3;
len (x2+y2)=len x by CARD_1:def 7;
then
A17: dom (x2+y2)=Seg len x by FINSEQ_1:def 3;
then
A18: i in Seg len x by A15,A14,XBOOLE_0:def 4;
then
A19: (x+y).i in rng (x+y) by A17,FUNCT_1:def 3;
i in dom y by A1,A18,FINSEQ_1:def 3;
then
A20: y.i in rng y by FUNCT_1:def 3;
A21: i in dom x by A18,FINSEQ_1:def 3;
then x.i in rng x by FUNCT_1:def 3;
then reconsider a=x.i, b=y.i, d=(x+y).i, e=z.i as Element of K by A12,A13
,A20,A16,A19;
dom (<:y,z:>) =(dom x) /\ (dom x) by A8,A3,A7,FUNCT_3:def 7
.= dom x;
then
A22: i in dom (<:y,z:>) by A18,FINSEQ_1:def 3;
dom [:y,z:]=[:dom y,dom z:] by FUNCT_3:def 8;
then
A23: [i,i] in dom [:y,z:] by A8,A3,A15,A17,A14,ZFMISC_1:87;
dom [:y,z:]=[:dom y,dom z:] by FUNCT_3:def 8;
then
A24: [i,i] in dom [:y,z:] by A8,A3,A15,A17,A14,ZFMISC_1:87;
dom (the multF of K)= [:the carrier of K,the carrier of K:] by
FUNCT_2:def 1;
then [b,e] in dom (the multF of K) by ZFMISC_1:87;
then
dom ((the multF of K)*(y,z)) = dom ((the multF of K)*[:y,z:]) & [:y,z
:].(i,i ) in dom (the multF of K) by A8,A3,A15,A17,A14,FINSEQOP:def 4
,FUNCT_3:def 8;
then [i,i] in dom ((the multF of K)*(y,z)) by A24,FUNCT_1:11;
then
A25: b*e=((the multF of K)*(y,z)).(i,i) by FINSEQOP:77
.=((the multF of K)*[:y,z:]).(i,i) by FINSEQOP:def 4
.=(the multF of K).([:y,z:].(i,i)) by A23,FUNCT_1:13
.=(the multF of K).(y.i,z.i) by A8,A3,A15,A17,A14,FUNCT_3:def 8
.=(the multF of K).((<:y,z:>).i) by A8,A3,A15,A17,A14,FUNCT_3:49
.= ((the multF of K)*(<:y,z:>)).i by A22,FUNCT_1:13
.= ((the multF of K).:(y,z)).i by FUNCOP_1:def 3
.= mlt(y,z).i by FVSUM_1:def 7;
dom (<:x+y,z:>) = dom (x+y) /\ dom (z) by FUNCT_3:def 7
.= dom x by A3,A4,FINSEQ_1:def 3;
then
A26: i in dom (<:x+y,z:>) by A18,FINSEQ_1:def 3;
A27: mlt(x+y,z).i = ((the multF of K).:(x+y,z)).i by FVSUM_1:def 7
.= ((the multF of K)*<:x+y,z:>).i by FUNCOP_1:def 3
.= (the multF of K).((<:x+y,z:>).i) by A26,FUNCT_1:13
.= d*e by A4,A15,A14,FUNCT_3:49;
A28: dom (<:mlt(x,z),mlt(y,z):>) = dom (mlt(x,z)) /\ dom (mlt(y,z)) by
FUNCT_3:def 7
.= dom x by A9,A5,FINSEQ_1:def 3;
A29: dom (<:x,y:>)= dom (x) /\ dom (y) by FUNCT_3:def 7
.= dom x by A8,A7;
A30: ((the addF of K).:(mlt(x,z),mlt(y,z))) =(mlt(x,z)+mlt(y,z)) by
FVSUM_1:def 3;
dom [:x,z:]=[:dom x,dom z:] by FUNCT_3:def 8;
then
A31: [i,i] in dom [:x,z:] by A3,A7,A15,A17,A14,ZFMISC_1:87;
dom [:x,z:]=[:dom x,dom z:] by FUNCT_3:def 8;
then
A32: [i,i] in dom [:x,z:] by A3,A7,A15,A17,A14,ZFMISC_1:87;
dom (<:x,z:>) = (dom x) /\ (dom x) by A3,A7,FUNCT_3:def 7
.= dom x;
then
A33: i in dom (<:x,z:>) by A18,FINSEQ_1:def 3;
A34: (x+y).i = ((the addF of K).:(x,y)).i by FVSUM_1:def 3
.= ((the addF of K)*(<:x,y:>)).i by FUNCOP_1:def 3
.= (the addF of K).((<:x,y:>).i) by A21,A29,FUNCT_1:13
.= a+b by A8,A7,A18,FUNCT_3:49;
dom (the multF of K)= [:the carrier of K,the carrier of K:] by
FUNCT_2:def 1;
then [a,e] in dom (the multF of K) by ZFMISC_1:87;
then
dom ((the multF of K)*(x,z)) = dom ((the multF of K)*[:x,z:]) & [:x,z
:].(i,i ) in dom (the multF of K) by A3,A7,A15,A17,A14,FINSEQOP:def 4
,FUNCT_3:def 8;
then [i,i] in dom ((the multF of K)*(x,z)) by A32,FUNCT_1:11;
then a*e=((the multF of K)*(x,z)).(i,i) by FINSEQOP:77
.=((the multF of K)*[:x,z:]).(i,i) by FINSEQOP:def 4
.=(the multF of K).([:x,z:].(i,i)) by A31,FUNCT_1:13
.=(the multF of K).(x.i,z.i) by A3,A7,A15,A17,A14,FUNCT_3:def 8
.=(the multF of K).((<:x,z:>).i) by A3,A7,A15,A17,A14,FUNCT_3:49
.=((the multF of K)*(<:x,z:>)).i by A33,FUNCT_1:13
.=((the multF of K).:(x,z)).i by FUNCOP_1:def 3
.=mlt(x,z).i by FVSUM_1:def 7;
then
a*e+b*e =(the addF of K).((<:mlt(x,z),mlt(y,z):>).i) by A9,A10,A6,A18,A25,
FUNCT_3:49
.= ((the addF of K)*<:mlt(x,z),mlt(y,z):>).i by A21,A28,FUNCT_1:13
.=(mlt(x,z)+mlt(y,z)).i by A30,FUNCOP_1:def 3;
hence thesis by A34,A27,VECTSP_1:def 7;
end;
dom (mlt(x+y,z))=Seg len(mlt(x2+y2,z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.= dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
hence thesis by A11,FINSEQ_1:13;
end;
theorem Th57: :: EUCLID_2:9
for K being Ring,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)
proof
let K be Ring,x,y,z be FinSequence of K;
assume that
A1: len x=len y and
A2: len y=len z;
A3: dom z=Seg len x by A1,A2,FINSEQ_1:def 3;
reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on the carrier of K
by A1,A2,FINSEQ_2:92;
A4: dom (x+y) = Seg len (x2+y2) by FINSEQ_1:def 3
.=dom z by A1,A2,CARD_1:def 7,FINSEQ_1:def 3;
A5: dom (mlt(z,y))=Seg len(mlt(z2,y2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7;
then
A6: dom (mlt(z,y))=Seg len (mlt(z2,x2)+mlt(z2,y2)) by CARD_1:def 7
.= dom (mlt(z2,x2)+mlt(z2,y2)) by FINSEQ_1:def 3;
A7: dom x =Seg len x by FINSEQ_1:def 3;
A8: dom y=Seg len x by A1,FINSEQ_1:def 3;
A9: dom (mlt(z,x))=Seg len(mlt(z2,x2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7;
then
A10: dom (mlt(z,x)) =Seg len (mlt(z2,x2)+mlt(z2,y2)) by CARD_1:def 7
.= dom (mlt(z2,x2)+mlt(z2,y2)) by FINSEQ_1:def 3;
A11: for i being Nat st i in dom (mlt(z,x+y)) holds mlt(z,x+y).i = (mlt(z,x)
+mlt(z,y)).i
proof
let i be Nat;
A12: rng x c= the carrier of K & rng y c= the carrier of K by FINSEQ_1:def 4;
A13: rng z c= the carrier of K & rng (x+y) c= the carrier of K by
FINSEQ_1:def 4;
dom (the multF of K) = [:the carrier of K,the carrier of K:] by
FUNCT_2:def 1;
then mlt(z,x+y)=(the multF of K).:(z,x+y) & [:rng z,rng (x+y):] c= dom (
the multF of K) by A13,FVSUM_1:def 7,ZFMISC_1:96;
then
A14: dom (mlt(z,x+y)) = dom z /\ dom(x+y) by FUNCOP_1:69;
assume
A15: i in dom mlt(z,x+y);
then i in dom z by A14,XBOOLE_0:def 4;
then
A16: z.i in rng z by FUNCT_1:def 3;
len (x2+y2)=len x by CARD_1:def 7;
then
A17: dom (x2+y2)=Seg len x by FINSEQ_1:def 3;
then
A18: i in Seg len x by A15,A14,XBOOLE_0:def 4;
then
A19: (x+y).i in rng (x+y) by A17,FUNCT_1:def 3;
i in dom y by A1,A18,FINSEQ_1:def 3;
then
A20: y.i in rng y by FUNCT_1:def 3;
A21: i in dom x by A18,FINSEQ_1:def 3;
then x.i in rng x by FUNCT_1:def 3;
then reconsider a=x.i, b=y.i, d=(x+y).i, e=z.i as Element of K by A12,A13
,A20,A16,A19;
dom (<:z,y:>) =(dom x) /\ (dom x) by A8,A3,A7,FUNCT_3:def 7
.= dom x;
then
A22: i in dom (<:z,y:>) by A18,FINSEQ_1:def 3;
dom [:z,y:]=[:dom z,dom y:] by FUNCT_3:def 8;
then
A23: [i,i] in dom [:z,y:] by A8,A3,A15,A17,A14,ZFMISC_1:87;
dom [:z,y:]=[:dom z,dom y:] by FUNCT_3:def 8;
then
A24: [i,i] in dom [:z,y:] by A8,A3,A15,A17,A14,ZFMISC_1:87;
dom (the multF of K)= [:the carrier of K,the carrier of K:] by
FUNCT_2:def 1;
then [e,b] in dom (the multF of K) by ZFMISC_1:87;
then
dom ((the multF of K)*(z,y)) = dom ((the multF of K)*[:z,y:]) & [:z,y
:].(i,i ) in dom (the multF of K) by A8,A3,A15,A17,A14,FINSEQOP:def 4
,FUNCT_3:def 8;
then [i,i] in dom ((the multF of K)*(z,y)) by A24,FUNCT_1:11;
then
A25: e*b=((the multF of K)*(z,y)).(i,i) by FINSEQOP:77
.=((the multF of K)*[:z,y:]).(i,i) by FINSEQOP:def 4
.=(the multF of K).([:z,y:].(i,i)) by A23,FUNCT_1:13
.=(the multF of K).(z.i,y.i) by A8,A3,A15,A17,A14,FUNCT_3:def 8
.=(the multF of K).((<:z,y:>).i) by A8,A3,A15,A17,A14,FUNCT_3:49
.= ((the multF of K)*(<:z,y:>)).i by A22,FUNCT_1:13
.= ((the multF of K).:(z,y)).i by FUNCOP_1:def 3
.= mlt(z,y).i by FVSUM_1:def 7;
dom (<:z,x+y:>) = dom (z) /\ dom (x+y) by FUNCT_3:def 7
.= dom x by A3,A4,FINSEQ_1:def 3;
then
A26: i in dom (<:z,x+y:>) by A18,FINSEQ_1:def 3;
A27: mlt(z,x+y).i = ((the multF of K).:(z,x+y)).i by FVSUM_1:def 7
.= ((the multF of K)*<:z,x+y:>).i by FUNCOP_1:def 3
.= (the multF of K).((<:z,x+y:>).i) by A26,FUNCT_1:13
.= e*d by A4,A15,A14,FUNCT_3:49;
A28: dom (<:mlt(z,x),mlt(z,y):>) = dom (mlt(z,x)) /\ dom (mlt(z,y)) by
FUNCT_3:def 7
.= dom x by A9,A5,FINSEQ_1:def 3;
A29: dom (<:x,y:>)= dom (x) /\ dom (y) by FUNCT_3:def 7
.= dom x by A8,A7;
A30: ((the addF of K).:(mlt(z,x),mlt(z,y))) =(mlt(z,x)+mlt(z,y)) by
FVSUM_1:def 3;
dom [:z,x:]=[:dom z,dom x:] by FUNCT_3:def 8;
then
A31: [i,i] in dom [:z,x:] by A3,A7,A15,A17,A14,ZFMISC_1:87;
dom [:z,x:]=[:dom z,dom x:] by FUNCT_3:def 8;
then
A32: [i,i] in dom [:z,x:] by A3,A7,A15,A17,A14,ZFMISC_1:87;
dom (<:z,x:>) = (dom x) /\ (dom x) by A3,A7,FUNCT_3:def 7
.= dom x;
then
A33: i in dom (<:z,x:>) by A18,FINSEQ_1:def 3;
A34: (x+y).i = ((the addF of K).:(x,y)).i by FVSUM_1:def 3
.= ((the addF of K)*(<:x,y:>)).i by FUNCOP_1:def 3
.= (the addF of K).((<:x,y:>).i) by A21,A29,FUNCT_1:13
.= a+b by A8,A7,A18,FUNCT_3:49;
dom (the multF of K)= [:the carrier of K,the carrier of K:] by
FUNCT_2:def 1;
then [e,a] in dom (the multF of K) by ZFMISC_1:87;
then
dom ((the multF of K)*(z,x)) = dom ((the multF of K)*[:z,x:]) & [:z,x
:].(i,i ) in dom (the multF of K) by A3,A7,A15,A17,A14,FINSEQOP:def 4
,FUNCT_3:def 8;
then [i,i] in dom ((the multF of K)*(z,x)) by A32,FUNCT_1:11;
then e*a=((the multF of K)*(z,x)).(i,i) by FINSEQOP:77
.=((the multF of K)*[:z,x:]).(i,i) by FINSEQOP:def 4
.=(the multF of K).([:z,x:].(i,i)) by A31,FUNCT_1:13
.=(the multF of K).(z.i,x.i) by A3,A7,A15,A17,A14,FUNCT_3:def 8
.=(the multF of K).((<:z,x:>).i) by A3,A7,A15,A17,A14,FUNCT_3:49
.=((the multF of K)*(<:z,x:>)).i by A33,FUNCT_1:13
.=((the multF of K).:(z,x)).i by FUNCOP_1:def 3
.=mlt(z,x).i by FVSUM_1:def 7;
then
e*a+e*b =(the addF of K).((<:mlt(z,x),mlt(z,y):>).i) by A9,A10,A6,A18,A25,
FUNCT_3:49
.= ((the addF of K)*<:mlt(z,x),mlt(z,y):>).i by A21,A28,FUNCT_1:13
.=(mlt(z,x)+mlt(z,y)).i by A30,FUNCOP_1:def 3;
hence thesis by A34,A27,VECTSP_1:def 7;
end;
dom (mlt(z,x+y))=Seg len(mlt(z2,x2+y2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(z2,x2)+mlt(z2,y2)) by CARD_1:def 7
.= dom (mlt(z2,x2)+mlt(z2,y2)) by FINSEQ_1:def 3;
hence thesis by A11,FINSEQ_1:13;
end;
theorem
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
by MATRIX_0:20,def 2;
theorem Th59:
for K being Ring,j being Nat,A,B being Matrix of K
st width A=width B & (i in dom A) holds
Line(A+B,i)=Line(A,i)+Line(B,i)
proof
let K be Ring,j be Nat,A,B be Matrix of K;
assume that
A1: width A=width B and
A2: i in dom A;
reconsider wA=width A as Element of NAT by ORDINAL1:def 12;
reconsider a= Line(A,i),b=Line(B,i) as Element of wA-tuples_on (the
carrier of K) by A1;
A3: width (A+B)=width A by MATRIX_1:def 6;
A4: i in Seg len A by A2,FINSEQ_1:def 3;
A5: len (A+B)=len A by MATRIX_1:def 6;
then
A6: Indices (A+B)=Indices A by A3,Th55;
A7: for k being Nat st 1<=k & k<=len (Line(A+B,i)) holds (Line(A+B,i)).k=(
Line(A,i)+Line(B,i)).k
proof
let k be Nat;
assume
A8: 1<=k & k<=len Line(A+B,i);
A9: len Line(A+B,i) = width A by A3,MATRIX_0:def 7;
then
A10: k in Seg width (A+B) by A3,A8,FINSEQ_1:1;
len Line(B,i)=width(B) by MATRIX_0:def 7;
then k in Seg len (Line(B,i)) by A1,A8,A9,FINSEQ_1:1;
then k in dom Line(B,i) by FINSEQ_1:def 3;
then reconsider e=Line(B,i).k as Element of K by FINSEQ_2:11;
i in dom (A+B) by A5,A4,FINSEQ_1:def 3;
then
A11: [i,k] in Indices (A+B) by A10,ZFMISC_1:87;
A12: (Line(A+B,i)).k= (A+B)*(i,k) by A10,MATRIX_0:def 7
.= A*(i,k)+B*(i,k) by A6,A11,MATRIX_1:def 6;
A13: len Line(A,i)=width(A) by MATRIX_0:def 7;
then
A14: k in Seg len (Line(A,i)) by A8,A9,FINSEQ_1:1;
then k in dom Line(A,i) by FINSEQ_1:def 3;
then reconsider d=Line(A,i).k as Element of K by FINSEQ_2:11;
len (Line(A,i)+Line(B,i))= len (a+b) .= width A by CARD_1:def 7
.= len (Line(A,i)) by CARD_1:def 7;
then k in dom (Line(A,i)+Line(B,i)) by A14,FINSEQ_1:def 3;
then
A15: (Line(A,i)+Line(B,i)).k=d+e by FVSUM_1:17;
Line(A,i).k=A*(i,k) by A13,A14,MATRIX_0:def 7;
hence thesis by A1,A13,A12,A14,A15,MATRIX_0:def 7;
end;
A16: len (Line(A,i)+Line(B,i))=len (a+b) .= width A by CARD_1:def 7;
len (Line(A+B,i)) = width A by A3,MATRIX_0:def 7;
hence thesis by A16,A7,FINSEQ_1:14;
end;
theorem Th60:
for K being Ring,j being Nat,A,B being Matrix of K st len A=len
B & j in Seg(width A) holds Col(A+B,j)=Col(A,j)+Col(B,j)
proof
let K be Ring,j be Nat, A,B be Matrix of K;
A1: len (A+B)=len A by MATRIX_1:def 6;
assume that
A2: len A=len B and
A3: j in Seg width A;
reconsider a = Col(A,j),b=Col(B,j) as Element of (len A)-tuples_on (the
carrier of K) by A2;
A4: width (A+B)=width A by MATRIX_1:def 6;
then
A5: Indices (A+B)=Indices A by A1,Th55;
A6: for k being Nat st 1<=k & k<=len (Col(A+B,j)) holds (Col(A+B,j)).k=(Col(
A,j)+Col(B,j)).k
proof
let k be Nat;
assume
A7: 1<=k & k<=len (Col(A+B,j));
A8: len (Col(A+B,j)) = len A by A1,MATRIX_0:def 8;
then k in Seg len A by A7,FINSEQ_1:1;
then
A9: k in dom (A+B) by A1,FINSEQ_1:def 3;
len (Col(B,j))=len(B) by MATRIX_0:def 8;
then k in Seg len (Col(B,j)) by A2,A7,A8,FINSEQ_1:1;
then k in dom Col(B,j) by FINSEQ_1:def 3;
then reconsider e=Col(B,j).k as Element of K by FINSEQ_2:11;
A10: dom A=Seg len A by FINSEQ_1:def 3
.=dom B by A2,FINSEQ_1:def 3;
A11: len (Col(A,j))=len(A) by MATRIX_0:def 8;
then
A12: k in Seg len (Col(A,j)) by A7,A8,FINSEQ_1:1;
then k in dom Col(A,j) by FINSEQ_1:def 3;
then reconsider d = Col(A,j).k as Element of K by FINSEQ_2:11;
len (Col(A,j)+Col(B,j)) = len (a+b) .= len A by CARD_1:def 7
.= len (Col(A,j)) by CARD_1:def 7;
then k in dom (Col(A,j)+Col(B,j)) by A12,FINSEQ_1:def 3;
then
A13: (Col(A,j)+Col(B,j)).k=d+e by FVSUM_1:17;
A14: [k,j] in Indices (A+B) by A3,A4,A9,ZFMISC_1:87;
A15: (Col(A+B,j)).k= (A+B)*(k,j) by A9,MATRIX_0:def 8
.= A*(k,j)+B*(k,j) by A5,A14,MATRIX_1:def 6;
A16: k in dom A by A11,A12,FINSEQ_1:def 3;
then Col(A,j).k=A*(k,j) by MATRIX_0:def 8;
hence thesis by A15,A13,A10,A16,MATRIX_0:def 8;
end;
A17: len (Col(A,j)+Col(B,j)) = len (a+b) .= len A by CARD_1:def 7;
len (Col(A+B,j)) = len A by A1,MATRIX_0:def 8;
hence thesis by A17,A6,FINSEQ_1:14;
end;
theorem Th61:
for V1 being Ring,P1,P2 be FinSequence of V1 st len P1 = len P2
holds Sum(P1+P2) = (Sum P1) + (Sum P2)
proof
let V1 be Ring, P1,P2 be FinSequence of V1;
assume len P1 = len P2;
then reconsider
R1 = P1, R2 = P2 as Element of (len P1)-tuples_on (the carrier of
V1) by FINSEQ_2:92;
thus Sum(P1+P2) = Sum (R1 + R2) .= Sum P1 + Sum P2 by FVSUM_1:76;
end;
Lm1:
for K being Ring,A,B,C being Matrix of K st len B=len C & width B=
width C & width A=len B & len A>0 holds A*(B+C)=A*B + A*C
proof
let K be Ring,A,B,C be Matrix of K;
assume that
A1: len B=len C and
A2: width B=width C and
A3: width A=len B and
A4: len A>0;
A5: len (B+C)=len B by MATRIX_1:def 6;
then
A6: len (A*(B+C))=len A by A3,MATRIX_3:def 4;
A7: width (B+C)=width B & width (A*(B+C))=width (B+C) by A3,A5,MATRIX_1:def 6
,MATRIX_3:def 4;
then reconsider M1=A*(B+C) as Matrix of (len A),(width B),K by A4,A6,
MATRIX_0:20;
A8: len (A*B)=len A & width (A*B)=width (B) by A3,MATRIX_3:def 4;
then
A9: Indices(M1)=Indices(A*B) by A6,A7,Th55;
A10: len (A*B +A*C)=len (A*B) & width(A*B+A*C)=width (A*B) by MATRIX_1:def 6;
then reconsider M2= A*B+A*C as Matrix of (len A),(width B),K by A4,A8,
MATRIX_0:20;
len (A*C)=len A & width (A*C)=width (C) by A1,A3,MATRIX_3:def 4;
then
A11: Indices(M1)=Indices(A*C) by A2,A6,A7,Th55;
for i,j st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
let i,j;
len Line(A,i) = len B by A3,MATRIX_0:def 7;
then
A12: len Line(A,i) =len Col(B,j) by MATRIX_0:def 8;
reconsider q1=Line(A,i),q2=Col(B,j),q3=Col(C,j) as Element of (len B)
-tuples_on (the carrier of K) by A1,A3;
A13: len (mlt(Line(A,i),Col(B,j)))=len (mlt(q1,q2)) .=len B by CARD_1:def 7
.=len (mlt(q1,q3)) by CARD_1:def 7
.= len(mlt(Line(A,i),Col(C,j)));
len Line(A,i) = len C by A1,A3,MATRIX_0:def 7;
then
A14: len Line(A,i) = len Col(C,j) by MATRIX_0:def 8;
assume
A15: [i,j] in Indices M1;
then
A16: M2*(i,j)=(A*B)*(i,j)+(A*C)*(i,j) by A9,MATRIX_1:def 6
.=(Line(A,i) "*" Col(B,j)) +(A*C)*(i,j) by A3,A9,A15,MATRIX_3:def 4
.=(Line(A,i) "*" Col(B,j)) +(Line(A,i) "*" Col(C,j)) by A1,A3,A11,A15,
MATRIX_3:def 4
.=(Line(A,i) "*" Col(B,j)) +Sum(mlt(Line(A,i),Col(C,j))) by FVSUM_1:def 9
.= Sum(mlt(Line(A,i),Col(B,j))) +Sum(mlt(Line(A,i),Col(C,j))) by
FVSUM_1:def 9;
A17: j in Seg width B by A7,A15,ZFMISC_1:87;
M1*(i,j)=Line(A,i) "*" Col(B+C,j) by A3,A5,A15,MATRIX_3:def 4
.=Sum(mlt(Line(A,i),Col(B+C,j))) by FVSUM_1:def 9
.=Sum(mlt(Line(A,i),Col(B,j)+Col(C,j))) by A1,A17,Th60
.=Sum(mlt(Line(A,i),Col(B,j))+mlt(Line(A,i),Col(C,j))) by A12,A14,Th57
.= Sum(mlt(Line(A,i),Col(B,j)))+ Sum(mlt(Line(A,i),Col(C,j))) by A13,Th61
;
hence thesis by A16;
end;
hence thesis by A6,A7,A8,A10,MATRIX_0:21;
end;
theorem
for K being Ring,A,B,C being Matrix of K st len B=len C & width B=
width C & width A=len B holds A*(B+C)=A*B + A*C
proof
let K be Ring;
let A,B,C be Matrix of K;
assume that
A1: len B=len C and
A2: width B= width C and
A3: width A=len B;
set LHS = A*(B+C);
set RHS = A*B + A*C;
len (B+C) = len B by MATRIX_1:def 6;
then
len(A*B) = len A & len(A*C) = len A & len LHS = len A by A1,A3,MATRIX_3:def 4
;
then
A4: len LHS = len RHS & len LHS = len A by MATRIX_1:def 6;
per cases by NAT_1:3;
suppose len A = 0;
then len LHS = 0 & len RHS = 0 by A4;
hence A*(B+C)=A*B + A*C by CARD_2:64;
end;
suppose len A > 0;
hence thesis by A1,A2,A3,Lm1;
end;
end;
Lm2:
for K being Ring,A,B,C being Matrix of K st len B=len C & width B=
width C & len A=width B & len B>0 holds (B+C)*A=B*A + C*A
proof
let K be Ring,A,B,C be Matrix of K;
assume that
A1: len B=len C and
A2: width B=width C and
A3: len A=width B and
A4: len B>0;
A5: width (B+C)=width B by MATRIX_1:def 6;
then
A6: width ((B+C)*A)=width A by A3,MATRIX_3:def 4;
len (B+C)=len B by MATRIX_1:def 6;
then
A7: len ((B+C)*A)=len B by A3,A5,MATRIX_3:def 4;
then reconsider M1=(B+C)*A as Matrix of len B,width A,K by A4,A6,MATRIX_0:20;
A8: len (B*A)=len B by A3,MATRIX_3:def 4;
A9: width (B*A)=width A by A3,MATRIX_3:def 4;
then
A10: Indices(M1)=Indices(B*A) by A7,A6,A8,Th55;
A11: len (B*A +C*A)=len (B*A) & width(B*A+C*A)=width (B*A) by MATRIX_1:def 6;
then reconsider M2= B*A+C*A as Matrix of (len B),width A,K by A4,A8,A9,
MATRIX_0:20;
len (C*A)=len C & width (C*A)=width A by A2,A3,MATRIX_3:def 4;
then
A12: Indices(M1)=Indices(C*A) by A1,A7,A6,Th55;
for i,j st [i,j] in Indices M1 holds M1*(i,j)=M2*(i,j)
proof
let i,j;
assume
A13: [i,j] in Indices M1;
len Col(A,j) = width B by A3,MATRIX_0:def 8;
then
A14: len Col(A,j) =len Line(B,i) by MATRIX_0:def 7;
reconsider q1=Line(B,i),q2=Line(C,i),q3=Col(A,j) as Element of (len A)
-tuples_on (the carrier of K) by A2,A3;
A15: len (mlt(Line(B,i),Col(A,j)))=len (mlt(q1,q3)) .=len A by CARD_1:def 7
.=len (mlt(q2,q3)) by CARD_1:def 7
.= len(mlt(Line(C,i),Col(A,j)));
len Col(A,j) = width C by A2,A3,MATRIX_0:def 8;
then
A16: len Col(A,j) = len Line(C,i) by MATRIX_0:def 7;
A17: M2*(i,j)=(B*A)*(i,j)+(C*A)*(i,j) by A10,A13,MATRIX_1:def 6
.=(Line(B,i) "*" Col(A,j)) +(C*A)*(i,j) by A3,A10,A13,MATRIX_3:def 4
.=(Line(B,i) "*" Col(A,j)) +(Line(C,i) "*" Col(A,j)) by A2,A3,A12,A13,
MATRIX_3:def 4
.=(Line(B,i) "*" Col(A,j)) +Sum(mlt(Line(C,i),Col(A,j))) by FVSUM_1:def 9
.= Sum(mlt(Line(B,i),Col(A,j))) +Sum(mlt(Line(C,i),Col(A,j))) by
FVSUM_1:def 9;
i in dom (B*A) by A10,A13,ZFMISC_1:87;
then i in Seg len B by A8,FINSEQ_1:def 3;
then
A18: i in dom B by FINSEQ_1:def 3;
M1*(i,j)=Line(B+C,i) "*" Col(A,j) by A3,A5,A13,MATRIX_3:def 4
.=Sum(mlt(Line(B+C,i),Col(A,j))) by FVSUM_1:def 9
.=Sum(mlt(Line(B,i)+Line(C,i),Col(A,j))) by A2,A18,Th59
.=Sum(mlt(Line(B,i),Col(A,j))+mlt(Line(C,i),Col(A,j))) by A14,A16,Th56
.= Sum(mlt(Line(B,i),Col(A,j)))+ Sum(mlt(Line(C,i),Col(A,j))) by A15,Th61
;
hence thesis by A17;
end;
hence thesis by A7,A6,A8,A9,A11,MATRIX_0:21;
end;
theorem
for K being Ring,A,B,C being Matrix of K st len B=len C & width B=
width C & len A=width B holds (B+C)*A=B*A + C*A
proof
let K be Ring;
let A,B,C be Matrix of K;
assume that
A1: len B=len C and
A2: width B= width C and
A3: len A=width B;
set LHS = (B+C)*A;
set RHS = B*A + C*A;
A4: len LHS = len RHS & len LHS = len B
proof
width (B + C) = len A by A3,MATRIX_1:def 6;
then
A5: len LHS = len (B + C) by MATRIX_3:def 4
.= len B by MATRIX_1:def 6;
len(C*A) = len B & len(B*A) = len B by A1,A2,A3,MATRIX_3:def 4;
then len RHS = len B by MATRIX_1:def 6;
hence thesis by A5;
end;
per cases by NAT_1:3;
suppose len B = 0;
hence thesis by A4,CARD_2:64;
end;
suppose len B > 0;
hence thesis by A1,A2,A3,Lm2;
end;
end;
theorem
for K being Ring,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
proof
let K be Ring,n,m,k be Nat, M1 be Matrix of n,m,K, M2 be Matrix
of m,k,K;
assume that
A1: width M1=len M2 and
A2: 0< len M1 and
A3: 0< len M2;
width M1=m by A1,MATRIX_0:def 2;
then
A4: len M1=n & width M2=k by A1,A3,MATRIX_0:20,def 2;
len (M1*M2)=len M1 & width (M1*M2)=width M2 by A1,MATRIX_3:def 4;
hence thesis by A2,A4,MATRIX_0:20;
end;
registration
let n be Nat;
let R be Ring;
let A,B be Matrix of n,R;
let X,Y be Matrix of R;
identify A + B with X + Y when A = X, B = Y;
correctness
proof
assume A1: A = X;
assume A2: B = Y;
len (A + B) = n & len A = n & width (A + B) = n & width A = n
by MATRIX_0:24;
then A3: len (A + B) = len A & width (A + B) = width A;
A4: len X = len A & width X = width A by A1;
A5: len (X + Y) = len X & width (X + Y) = width X by MATRIX_1:def 6;
A6: len (X + Y) = len (A + B) & width (X + Y) = width (A + B) by A3,A4,A5;
for i,j being Nat st [i,j] in Indices (X + Y) holds
(X + Y) * (i,j) = (A + B) * (i,j)
proof
let i,j be Nat;
assume A7: [i,j] in Indices (X + Y);
then [i,j] in [:(dom (X + Y)),(Seg (width (X + Y))):];
then i in dom (X + Y) & j in Seg (width (X + Y)) by ZFMISC_1:87;
then 1 <= i & i <= len (X + Y) & 1 <= j & j <= width (X + Y)
by FINSEQ_1:1,FINSEQ_3:25;
then A8: [i,j] in Indices X by A5,MATRIX_0:30;
then A9: [i,j] in Indices A by A1;
thus (X + Y) * (i,j) = (X * (i,j)) + (Y * (i,j)) by A8,MATRIX_1:def 6
.= (A * (i,j)) + (Y * (i,j)) by A1
.= (A * (i,j)) + (B * (i,j)) by A2
.= (A + B) * (i,j) by A9,MATRIX_1:def 8;
end;
then X + Y = A + B by A6,MATRIX_0:21;
hence A + B = X + Y;
end;
end;