:: Determinant and Inverse of Matrices of Real Elements
:: by Nobuyuki Tamura and Yatsuka Nakamura
::
:: Received July 17, 2007
:: Copyright (c) 2007-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 NUMBERS, XBOOLE_0, SUBSET_1, VECTSP_1, FINSEQ_1, ARYTM_1,
FUNCT_1, FINSEQ_2, ARYTM_3, EUCLID, MATRIX_1, XXREAL_0, INCSP_1, RELAT_1,
TREES_1, TARSKI, MATRIXR1, CARD_1, NAT_1, REAL_1, SUPINF_2, QC_LANG1,
ZFMISC_1, FVSUM_1, MATRIX_3, FUNCT_2, MESFUNC1, GROUP_1, ABIAN, BINOP_1,
ALGSTR_0, SETWISEO, CARD_3, RVSUM_1, FUNCT_4, AFINSQ_1, PRALG_1,
PARTFUN1, MATRIXR2, MATRIX_0, FUNCT_7, FUNCSDOM, FINSUB_1;
notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_0, ZFMISC_1, ORDINAL1, NUMBERS,
ENUMSET1, SETWOP_2, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, PARTFUN1,
BINOP_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_7, STRUCT_0,
ALGSTR_0, MATRIX_0, MATRIX_1, FVSUM_1, FINSEQ_7, SETWISEO, GROUP_1,
FINSUB_1, MATRIX_3, MATRIX_6, MATRIXR1, EUCLID, MATRIX_7, RVSUM_1,
VECTSP_1, MATRPROB;
constructors FVSUM_1, BINOP_2, FINSEQ_7, SETWISEO, FINSOP_1, FINSEQ_4,
MATRIX_7, MATRIXR1, MATRIX_6, REAL_1, RVSUM_1, EUCLID, RELSET_1, BINOP_1,
VECTSP_2, MATRIX_3;
registrations FINSEQ_2, NAT_1, RELSET_1, MEMBERED, STRUCT_0, VECTSP_1,
NUMBERS, XXREAL_0, MATRIX_1, FINSEQ_1, FVSUM_1, XBOOLE_0, VALUED_0,
CARD_1, MATRIX_0, MATRIX_6, XREAL_0, VECTSP_2, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, MATRIX_0;
equalities MATRIX_0, STRUCT_0, VECTSP_1, MATRIXR1, FINSEQ_1, VALUED_1;
expansions TARSKI, MATRIX_0, FINSEQ_1;
theorems MATRIX_3, VECTSP_1, MATRIX_0, MATRIX_4, GROUP_1, XREAL_0, FUNCT_1,
FINSEQ_1, NAT_1, FINSEQ_7, FINSEQ_2, TARSKI, FINSOP_1, FVSUM_1, SETWISEO,
XBOOLE_0, ENUMSET1, XCMPLX_0, ZFMISC_1, MATRIX_7, MATRIXR1, FINSEQ_3,
XXREAL_0, RVSUM_1, MATRIX10, MATRIX11, MATRPROB, FINSEQ_4, MATRIX_9,
MATRIXC1, PARTFUN1, FUNCT_7, CARD_1, MATRIX_1, FINSUB_1, SUBSET_1;
schemes FINSEQ_4;
begin :: Preliminaries
reserve x for set,
D for non empty set,
k,n,m,i,j,l for Nat,
K for Field;
Lm1: for F1,F2 being FinSequence of REAL,j st len F1=len F2 holds (F1-F2).j=F1
.j - F2.j
proof
let F1,F2 be FinSequence of REAL,j;
reconsider n=len F1 as Element of NAT;
reconsider G1=F1 as Element of n-tuples_on REAL by FINSEQ_2:92;
assume len F1=len F2;
then reconsider G2=F2 as Element of n-tuples_on REAL by FINSEQ_2:92;
(G1-G2).j=(G1.j) - (G2.j) by RVSUM_1:27;
hence thesis;
end;
theorem Th1:
for x,y being FinSequence of REAL st len x=len y & x+y=0*(len x)
holds x=-y & y=-x
proof
let x,y be FinSequence of REAL;
assume that
A1: len x=len y and
A2: x + y = 0* (len x);
A3: x = 0* (len x) - y by A1,A2,MATRIXR1:14;
hence x = -y by A1,MATRIXR1:6;
thus -x = --y by A1,A3,MATRIXR1:6
.=y;
end;
Lm2: for A being Matrix of D st 1<=i & i<=len A holds Line(A,i)=A.i
proof
let A be Matrix of D;
assume 1<=i & i<=len A;
then i in dom A by FINSEQ_3:25;
hence thesis by MATRIX_0:60;
end;
theorem Th2:
for A being Matrix of D for p being FinSequence of D st
p=A.i & 1<=i & i<=len A & 1<=j & j<=width A & len p=width A holds
A*(i,j)=p.j
proof
let A be Matrix of D;
let p be FinSequence of D;
assume that
A1: p=A.i and
A2: 1<=i & i<=len A and
A3: 1<=j & j<=width A and
A4: len p=width A;
A5: j in Seg width A by A3;
then j in dom p by A4,FINSEQ_1:def 3;
then rng p c= D & p.j in rng p by FINSEQ_1:def 4,FUNCT_1:def 3;
then reconsider xp=p.j as Element of D;
A6: xp=p.j;
i in dom A by A2,FINSEQ_3:25;
then [i,j] in Indices A by A5,ZFMISC_1:87;
hence thesis by A1,A6,MATRIX_0:def 5;
end;
theorem Th3:
for a being Real, A being Matrix of REAL st [i,j] in
Indices A holds (a*A)*(i,j) = a*(A*(i,j))
proof
let a be Real,A be Matrix of REAL;
assume
A1: [i,j] in Indices A;
reconsider aa=a as Element of F_Real by XREAL_0:def 1;
(a*A)*(i,j) = (MXF2MXR (aa*(MXR2MXF A)))*(i,j) by MATRIXR1:def 7
.= aa*((MXR2MXF A)*(i,j)) by A1,MATRIX_3:def 5
.= a*(A*(i,j));
hence thesis;
end;
theorem
for A,B being Matrix of n,REAL holds
len (A*B)=len A & width (A*B)=width B &
len (A*B)=n & width (A*B)=n
proof
let A,B be Matrix of n,REAL;
A1: len B=n by MATRIX_0:25;
A2: len A=n by MATRIX_0:25;
per cases;
suppose
A3: n>0;
then width MXR2MXF A =n by MATRIX_0:23
.=len MXR2MXF B by MATRIX_0:25;
then len (A*B)=len A & width (A*B)=width B by MATRIX_3:def 4;
hence thesis by A1,A3,MATRIX_0:20,25;
end;
suppose
A4: n<=0;
then
A5: width (MXR2MXF A) =0 by A2,MATRIX_0:def 3
.=len (MXR2MXF B) by A4,MATRIX_0:25;
then len (A*B) = len A by MATRIX_3:def 4;
hence thesis by A2,A4,A5,MATRIX_0:def 3,MATRIX_3:def 4;
end;
end;
theorem Th5:
for a being Real,A being Matrix of REAL holds
len (a*A) = len A & width (a*A) = width A
proof
let a be Real,A be Matrix of REAL;
reconsider ea=a as Element of F_Real by XREAL_0:def 1;
A1: width (a*A)= width MXR2MXF MXF2MXR (ea*(MXR2MXF A)) by MATRIXR1:def 7
.= width A by MATRIX_3:def 5;
len (a*A)= len MXR2MXF MXF2MXR (ea*(MXR2MXF A)) by MATRIXR1:def 7
.= len A by MATRIX_3:def 5;
hence thesis by A1;
end;
begin :: Calculation of Matrices
theorem Th6:
for A,B being Matrix of REAL st len A=len B & width A=width B
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)
proof
let A,B be Matrix of REAL;
assume
A1: len A=len B & width A=width B;
thus len (A - B) =len (MXF2MXR ((MXR2MXF A)+-(MXR2MXF B))) by MATRIX_1:def 7
.=len A by MATRIX_1:def 6;
thus width (A - B) =width (MXF2MXR ((MXR2MXF A)+-(MXR2MXF B))) by
MATRIX_1:def 7
.=width A by MATRIX_1:def 6;
thus thesis by A1,MATRIX10:3;
end;
definition
let n;
let A,B be Matrix of n,REAL;
redefine func A*B -> Matrix of n,REAL; :: redefines * (MATRIXR1, definition)
coherence;
end;
theorem Th7:
for A,B being Matrix of REAL st len A=len B & width A=width B &
len A>0 holds A + (B - B) = A
proof
let A,B be Matrix of REAL;
assume A1: len A=len B & width A=width B;
assume len A>0;
hence A=A+(0_Rmatrix(len B,width B)) by A1,MATRIXR1:36
.=MXF2MXR (MXR2MXF A)+ MXF2MXR ((MXR2MXF B)+(-(MXR2MXF B))) by MATRIX_4:2
.=A + (B - B) by MATRIX_1:def 7;
end;
theorem
for A,B being Matrix of REAL st
len A=len B & width A=width B & len A > 0 holds A + B - B = A
proof
let A,B be Matrix of REAL;
assume that
A1: len A=len B & width A=width B and
A2: len A>0;
thus A + B - B =A + B+ - B by MATRIX_1:def 7
.= A + (B +- B) by A1,MATRIX_3:3
.= A+(B-B) by MATRIX_1:def 7
.=A by A1,A2,Th7;
end;
Lm3: for A being Matrix of REAL st [i,j] in Indices A holds (-A)*(i,j)= -(A*(i
,j))
proof
let A be Matrix of REAL;
assume [i,j] in Indices A;
then (-A)*(i,j) = -((MXR2MXF A)*(i,j)) by MATRIX_1:def 4;
hence thesis;
end;
theorem Th9:
for A being Matrix of REAL holds (-1)*A = -A
proof
let A be Matrix of REAL;
A1: width ((-1)*A) = width A by Th5;
A2: len (((-1) qua Real)*A) = len A by Th5;
A3: now
let i,j be Nat;
reconsider i0=i,j0=j as Nat;
assume
A4: [i,j] in Indices ((-1)*A);
then
A5: 1<=j0 & j0<=width A by A1,MATRIXC1:1;
1<= i0 & i0<=len A by A2,A4,MATRIXC1:1;
then
A6: [i0,j0] in Indices A by A5,MATRIXC1:1;
hence ((-1)*A)*(i,j) = (-1)*(A*(i0,j0)) by Th3
.= -(A*(i,j))
.= (-A)*(i,j) by A6,Lm3;
end;
len (-A) = len A & width (-A) = width A by MATRIX_1:def 4;
hence thesis by A2,A1,A3,MATRIX_0:21;
end;
theorem Th10:
for A being (Matrix of REAL), i,j being Nat st
[i,j] in Indices A holds (-A)*(i,j)=-(A*(i,j))
proof
let A be (Matrix of REAL), i,j be Nat;
assume
A1: [i,j] in Indices A;
-A=(-1)*A by Th9;
then (-A)*(i,j)= (-1)*(A*(i,j)) by A1,MATRIXR1:29;
hence thesis;
end;
theorem
for a,b being Real,A being Matrix of REAL holds (a*b)*A=a*(b*A)
proof
let a,b be Real,A be Matrix of REAL;
A1: len ((a*b)*A)=len A & width ((a*b)*A)=width A by Th5;
A2: len (a*(b*A))=len (b*A) by Th5;
A3: width (a*(b*A))=width (b*A) by Th5;
then
A4: width (a*(b*A)) =width A by Th5;
A5: len (b*A)=len A & width (b*A)=width A by Th5;
A6: for i,j being Nat st [i,j] in Indices (a*(b*A)) holds (a*(b*A))*(i,j)=((
a*b)*A)*(i,j)
proof
let i,j be Nat;
assume
A7: [i,j] in Indices (a*(b*A));
A8: Indices ((b*A))=Indices (A) by A5,MATRIX_4:55;
reconsider i0=i,j0=j as Nat;
A9: Indices (a*(b*A))=Indices ((b*A)) by A2,A3,MATRIX_4:55;
then (a*(b*A))*(i,j) = (a*((b*A)*(i0,j0))) by A7,Th3
.= (a*(b*(A*(i0,j0)))) by A7,A9,A8,Th3
.= (a*b)*(A*(i0,j0))
.= ((a*b)*A)*(i,j) by A7,A9,A8,Th3;
hence thesis;
end;
len (a*(b*A)) =len A by A2,Th5;
hence thesis by A1,A4,A6,MATRIX_0:21;
end;
theorem Th12:
for a,b being Real,A being Matrix of REAL holds (a+b)*A=a*A + b* A
proof
let a,b be Real, A be Matrix of REAL;
A1: len (a*A)=len A & width (a*A)=width A by MATRIXR1:27;
A2: len ((a+b)*A)=len A & width ((a+b)*A)=width A by MATRIXR1:27;
A3: for i,j being Nat st [i,j] in Indices ((a+b)*A) holds ((a+b)*A)*(i,j)=(a
*A + b*A)*(i,j)
proof
let i,j be Nat;
assume
A4: [i,j] in Indices ((a+b)*A);
reconsider i0=i,j0=j as Nat;
A5: Indices ((a+b)*A)=Indices A by A2,MATRIX_4:55;
Indices (a*A)=Indices A by A1,MATRIX_4:55;
then (a*A + b*A)*(i,j) =(a*A)*(i0,j0)+(b*A)*(i0,j0) by A4,A5,MATRIXR1:25
.=a*(A*(i0,j0))+(b*A)*(i0,j0) by A4,A5,MATRIXR1:29
.=a*(A*(i0,j0))+b*(A*(i0,j0)) by A4,A5,MATRIXR1:29
.=(a+b)*(A*(i,j));
hence thesis by A4,A5,MATRIXR1:29;
end;
len (a*A + b*A) = len (a*A) & width (a*A + b*A) =width (a*A) by
MATRIX_1:def 6;
hence thesis by A2,A1,A3,MATRIX_0:21;
end;
theorem
for a,b being Real,A being Matrix of REAL holds (a-b)*A=a*A - b*A
proof
let a,b be Real, A be Matrix of REAL;
A1: len ((a-b)*A)=len (A) & width ((a-b)*A)=width A by MATRIXR1:27;
A2: len (a*A)=len A & width (a*A)=width (A) by MATRIXR1:27;
A3: len (b*A)=len A & width (b*A)=width A by MATRIXR1:27;
A4: for i,j being Nat st [i,j] in Indices ((a-b)*A) holds ((a-b)*A)*(i,j)=(a
*A - b*A)*(i,j)
proof
let i,j be Nat;
assume
A5: [i,j] in Indices ((a-b)*A);
reconsider i0=i,j0=j as Nat;
A6: Indices ((a-b)*A)=Indices A by A1,MATRIX_4:55;
Indices (a*A)=Indices A by A2,MATRIX_4:55;
then (a*A - b*A)*(i,j) =(a*A)*(i0,j0)-(b*A)*(i0,j0) by A2,A3,A5,A6,Th6
.=a*(A*(i0,j0))-(b*A)*(i0,j0) by A5,A6,MATRIXR1:29
.=a*(A*(i0,j0))-b*(A*(i0,j0)) by A5,A6,MATRIXR1:29
.=(a-b)*(A*(i,j));
hence thesis by A5,A6,MATRIXR1:29;
end;
A7: width (a*A - b*A) =width (MXF2MXR ((MXR2MXF (a*A))+-(MXR2MXF (b*A)))) by
MATRIX_1:def 7
.=width (a*A) by MATRIX_1:def 6;
len (a*A - b*A) =len (MXF2MXR ((MXR2MXF (a*A))+-(MXR2MXF (b*A)))) by
MATRIX_1:def 7
.=len (a*A) by MATRIX_1:def 6;
hence thesis by A1,A7,A2,A4,MATRIX_0:21;
end;
theorem Th14:
for K being Ring
for A being Matrix of K st n>0 holds
0.(K,n,len A)*A = 0.(K,n,width A)
proof
let K be Ring;
let A be Matrix of K;
assume
A1: n>0;
A3: len 0.(K,n,len A)=n by MATRIX_0:def 2;
then
A4: width 0.(K,n,len A)=len A by A1,MATRIX_0:20;
then
A5: len ((0.(K,n,len A))*A)=n by A3,MATRIX_3:def 4;
A6: width ((0.(K,n,len A))*A)=width A by A4,MATRIX_3:def 4;
0.(K,n,len A)*A + 0.(K,n,len A)*A =(0.(K,n,len A)+ 0.(K,n,len A))*A by A4,
MATRIX_4:63
.=0.(K,n,len A)*A by MATRIX_3:4;
hence thesis by A5,A6,MATRIX_4:6;
end;
theorem Th15:
for K being Ring
for A,C being Matrix of K st len A=width C & len C>0
holds (-C)*A = -(C*A)
proof
let K be Ring;
let A,C be Matrix of K;
assume that
A1: len A=width C and
A2: len C>0;
A4: len C=len (-C) by MATRIX_1:def 4;
A5: width (-C)=width C by MATRIX_1:def 4;
then width ((-C)*A)=width A by A1,MATRIX_3:def 4;
then
A6: width (C*A)=width ((-C)*A) by A1,MATRIX_3:def 4;
reconsider D=C as Matrix of (len C),(width C),K by A2,MATRIX_0:20;
A7: width (-C)=width C by MATRIX_1:def 4;
then
A8: len ((-C)*A)=len (-C) & width ((-C)*A)=width A by A1,MATRIX_3:def 4;
len (-C)=len ((-C)*A) by A1,A5,MATRIX_3:def 4;
then
A9: len (C*A)=len ((-C)*A) by A1,A4,MATRIX_3:def 4;
len C = len (-C) by MATRIX_1:def 4;
then C*A +((-C)*A) =(D+-D)*A by A1,A7,MATRIX_4:63
.= 0.(K,len C,width C)*A by MATRIX_3:5
.= 0.(K,len C,width A) by A1,A2,Th14;
hence thesis by A4,A8,A9,A6,MATRIX_4:8;
end;
theorem Th16:
for K being Ring
for 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
proof
let K be Ring;
let A,B,C be Matrix of K;
assume
A1: len B=len C & width B=width C & len A=width B & len B>0 & len A>0;
A2: width (-C)=width C & len C=len (-C) by MATRIX_1:def 4;
thus (B-C)*A=(B+-C)*A by MATRIX_1:def 7
.=B*A +(-C)*A by A1,A2,MATRIX_4:63
.=B*A +-(C*A) by A1,Th15
.=B*A -(C*A) by MATRIX_1:def 7;
end;
theorem
for A,B,C being Matrix of REAL st len A=len B & width A=width B & len
C=width A & len A>0 & len C>0 holds (A-B)*C=A*C - B*C by Th16;
theorem Th18:
for K being Ring
for m being Nat,A,C being Matrix of K st width A>0
holds A*(0.(K,width A,m)) = 0.(K,len A,m)
proof
let K be Ring;
let m be Nat, A,C be Matrix of K;
assume
A1: width A>0;
A3: len (0.(K,width A,m))= width A by MATRIX_0:def 2;
then m=width 0.(K,width A,m) by A1,MATRIX_0:20;
then
A4: width (A*((0.(K,width A,m))))=m by A3,MATRIX_3:def 4;
A5: (A * (0.(K,width A,m))) + (A * (0.(K,width A,m)))
= A * (0.(K,width A,m) + 0.(K,width A,m)) by A3,MATRIX_4:62
.= A * (0.(K,width A,m)) by MATRIX_3:4;
len (A*(0.(K,width A,m)))=len A by A3,MATRIX_3:def 4;
hence thesis by A4,A5,MATRIX_4:6;
end;
theorem Th19:
for K being Ring
for A,C being Matrix of K st width A=len C & len C>0
holds A*(-C) = -(A*C)
proof
let K be Ring;
let A,C be Matrix of K;
assume that
A1: width A=len C and
A3: len C>0;
A4: len C=len (-C) by MATRIX_1:def 4;
then
A5: len A=len (A*(-C)) by A1,MATRIX_3:def 4;
width (-C)=width C by MATRIX_1:def 4;
then
A6: width (A*(-C))=width C by A1,A4,MATRIX_3:def 4;
reconsider D=C as Matrix of (len C),(width C),K by A3,MATRIX_0:20;
A7: len (A*C)=len A & width (A*C)=width C by A1,MATRIX_3:def 4;
len C = len (-C) & width (-C)=width C by MATRIX_1:def 4;
then A*C +(A*(-C)) =A*(D+-D) by A1,MATRIX_4:62
.= A*(0.(K,len C,width C)) by MATRIX_3:5
.= 0.(K,len A,width C) by A1,A3,Th18;
hence thesis by A7,A5,A6,MATRIX_4:8;
end;
theorem Th20:
for K being Ring
for A,B,C being Matrix of K st len B=len C & width B=width C &
len B=width A & len B>0 & len A>0 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: len B=width A & len B>0 & len A>0;
A4: width (-C)=width C & len C=len (-C) by MATRIX_1:def 4;
thus A*(B-C)=A*(B+ (- C)) by MATRIX_1:def 7
.=A*B +A*(-C) by A1,A2,A3,A4,MATRIX_4:62
.=A*B +-(A*C) by A1,A3,Th19
.=A*B -(A*C) by MATRIX_1:def 7;
end;
theorem
for A,B,C being Matrix of REAL st len A=len B & width A=width B &
width C=len A & len C>0 & len A>0 holds C*(A-B)=C*A -C*B by Th20;
theorem Th22:
for A,B,C being Matrix of REAL st len A=len B & width A=width B
& len C = len A & width C = width A & (for i,j being Nat st [i,j] in
Indices A holds C*(i,j) = A*(i,j) - B*(i,j)) holds C=A-B
proof
let A,B,C be Matrix of REAL;
assume that
A1: len A=len B & width A=width B and
A2: len C =len A & width C=width A and
A3: for i,j being Nat st [i,j] in Indices A holds C*(i,j) = A
*(i,j) - B*(i,j);
A4: Indices B=Indices A by A1,MATRIX_4:55;
for i,j being Nat st [i,j] in Indices A holds C*(i,j) = A*(i,j) +((-B)*(
i,j))
proof
let i,j be Nat;
reconsider i0=i,j0=j as Nat;
assume
A5: [i,j] in Indices A;
hence C*(i,j) = A*(i0,j0) - B*(i0,j0) by A3
.=A*(i0,j0) +-B*(i0,j0)
.=A*(i,j)+(-B)*(i,j) by A4,A5,Th10;
end;
then C=(A+-B) by A2,MATRIXR1:26;
hence thesis by MATRIX_1:def 7;
end;
theorem Th23:
for x1,x2 being FinSequence of REAL st len x1=len x2 holds
LineVec2Mx (x1-x2)=LineVec2Mx (x1)-LineVec2Mx (x2)
proof
let x1,x2 be FinSequence of REAL;
A1: width LineVec2Mx x1=len x1 & len LineVec2Mx x1=1 by MATRIXR1:def 10;
A2: Seg width LineVec2Mx x1=Seg len x1 by MATRIXR1:def 10
.= dom x1 by FINSEQ_1:def 3;
A3: dom LineVec2Mx x1=Seg len LineVec2Mx x1 by FINSEQ_1:def 3
.=Seg 1 by MATRIXR1:def 10;
assume
A4: len x1=len x2;
then
A5: dom x1 = dom x2 by FINSEQ_3:29;
A6: width LineVec2Mx x2=len x2 & len LineVec2Mx x2=1 by MATRIXR1:def 10;
then
A7: Indices LineVec2Mx x2=Indices LineVec2Mx x1 by A4,A1,MATRIX_4:55;
A8: len (x1-x2)=len x1 by A4,RVSUM_1:116;
then
A9: dom (x1-x2)=dom x1 by FINSEQ_3:29;
A10: width LineVec2Mx (x1-x2)=len (x1-x2) & len LineVec2Mx (x1-x2)=1 by
MATRIXR1:def 10;
then
A11: Indices LineVec2Mx (x1-x2)=Indices LineVec2Mx x1 by A4,A1,MATRIX_4:55
,RVSUM_1:116;
for i,j holds [i,j] in Indices LineVec2Mx x1 implies (LineVec2Mx (x1-x2
))*(i,j) = (LineVec2Mx x1)*(i,j) - (LineVec2Mx x2)*(i,j)
proof
let i,j;
assume
A12: [i,j] in Indices LineVec2Mx x1;
then consider q1 being FinSequence of REAL such that
q1 = (LineVec2Mx x1).i and
A13: (LineVec2Mx x1)*(i,j) = q1.j by MATRIX_0:def 5;
i in Seg 1 by A3,A12,ZFMISC_1:87;
then 1<=i & i<=1 by FINSEQ_1:1;
then
A14: i=1 by XXREAL_0:1;
A15: j in dom x1 by A2,A12,ZFMISC_1:87;
then
A16: q1.j=x1.j by A14,A13,MATRIXR1:def 10;
consider p being FinSequence of REAL such that
p = (LineVec2Mx (x1-x2)).i and
A17: (LineVec2Mx (x1-x2))*(i,j) = p.j by A11,A12,MATRIX_0:def 5;
consider q2 being FinSequence of REAL such that
q2 = (LineVec2Mx x2).i and
A18: (LineVec2Mx x2)*(i,j) =q2.j by A7,A12,MATRIX_0:def 5;
A19: q2.j=x2.j by A5,A15,A14,A18,MATRIXR1:def 10;
p.j=(x1-x2).j by A9,A15,A14,A17,MATRIXR1:def 10;
hence thesis by A4,A17,A13,A16,A18,A19,Lm1;
end;
hence thesis by A4,A8,A10,A1,A6,Th22;
end;
theorem Th24:
for x1,x2 being FinSequence of REAL st len x1=len x2 & len x1>0
holds ColVec2Mx (x1-x2)=ColVec2Mx (x1)-ColVec2Mx (x2)
proof
let x1,x2 be FinSequence of REAL;
assume that
A1: len x1=len x2 and
A2: len x1>0;
A3: width ColVec2Mx x1=1 by A2,MATRIXR1:def 9;
A4: Seg width ColVec2Mx x1=Seg 1 by A2,MATRIXR1:def 9;
A5: dom x1=dom x2 by A1,FINSEQ_3:29;
A6: len (x1-x2)=len x1 by A1,RVSUM_1:116;
then
A7: dom (x1-x2)=dom x1 by FINSEQ_3:29;
A8: len ColVec2Mx x1=len x1 by A2,MATRIXR1:def 9;
then
A9: dom ColVec2Mx x1=dom x1 by FINSEQ_3:29;
A10: len ColVec2Mx x2=len x2 & width ColVec2Mx x2=1 by A1,A2,MATRIXR1:def 9;
then
A11: Indices ColVec2Mx x2=Indices ColVec2Mx x1 by A1,A8,A3,MATRIX_4:55;
A12: len ColVec2Mx (x1-x2)=len (x1-x2) & width ColVec2Mx (x1-x2)=1 by A2,A6,
MATRIXR1:def 9;
then
A13: Indices ColVec2Mx (x1-x2)=Indices ColVec2Mx x1 by A1,A8,A3,MATRIX_4:55
,RVSUM_1:116;
for i,j st [i,j] in Indices ColVec2Mx x1 holds (ColVec2Mx (x1-x2))*(i,j
) = (ColVec2Mx x1)*(i,j) - (ColVec2Mx x2)*(i,j)
proof
let i,j;
assume
A14: [i,j] in Indices ColVec2Mx x1;
then consider q1 being FinSequence of REAL such that
A15: q1 = (ColVec2Mx x1).i and
A16: (ColVec2Mx x1)*(i,j)=q1.j by MATRIX_0:def 5;
j in Seg 1 by A4,A14,ZFMISC_1:87;
then 1<=j & j<=1 by FINSEQ_1:1;
then
A17: j=1 by XXREAL_0:1;
A18: i in dom x1 by A9,A14,ZFMISC_1:87;
then (ColVec2Mx x1).i=<* x1.i *> by A2,MATRIXR1:def 9;
then
A19: q1.j=x1.i by A17,A15;
consider p being FinSequence of REAL such that
A20: p = (ColVec2Mx (x1-x2)).i and
A21: (ColVec2Mx (x1-x2))*(i,j) = p.j by A13,A14,MATRIX_0:def 5;
consider q2 being FinSequence of REAL such that
A22: q2 = (ColVec2Mx x2).i and
A23: (ColVec2Mx x2)*(i,j)=q2.j by A11,A14,MATRIX_0:def 5;
(ColVec2Mx x2).i=<* x2.i *> by A1,A2,A5,A18,MATRIXR1:def 9;
then
A24: q2.j=x2.i by A17,A22;
(ColVec2Mx (x1-x2)).i=<* (x1-x2).i *> by A2,A6,A7,A18,MATRIXR1:def 9;
then p.j=(x1-x2).i by A17,A20;
hence thesis by A1,A21,A16,A19,A23,A24,Lm1;
end;
hence thesis by A1,A6,A8,A12,A3,A10,Th22;
end;
theorem Th25:
for A,B being Matrix of REAL st len A=len B & 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)
proof
let A,B be Matrix of REAL;
assume that
A1: len A=len B and
A2: width A=width B;
A3: width (A-B)=width A by A1,A2,Th6;
let i be Nat;
A4: len Line(A,i)=width A by MATRIX_0:def 7;
A5: len Line(B,i)=width B by MATRIX_0:def 7;
assume 1<=i & i<=len A;
then
A6: i in dom A by FINSEQ_3:25;
A7: for j being Nat st j in Seg width (A-B) holds (Line(A,i)-Line(B,i)).j =
(A-B)*(i,j)
proof
reconsider i2=i as Nat;
let j be Nat;
reconsider j2=j as Nat;
A8: (Line(A,i2)-Line(B,i2)).j=Line(A,i2).j2-Line(B,i2).j2 by A2,A4,A5,Lm1;
assume
A9: j in Seg width (A-B);
then [i,j] in Indices A by A6,A3,ZFMISC_1:87;
then
A10: (A-B)*(i2,j2) = A*(i2,j2) - B*(i2,j2) by A1,A2,Th6;
A11: j in Seg width A by A1,A2,A9,Th6;
then Line(A,i).j=A*(i,j) by MATRIX_0:def 7;
hence thesis by A2,A11,A10,A8,MATRIX_0:def 7;
end;
len (Line(A,i)-Line(B,i))=len Line(A,i) by A2,A4,A5,RVSUM_1:116;
hence thesis by A4,A3,A7,MATRIX_0:def 7;
end;
theorem Th26:
for A,B being Matrix of REAL st len A=len B & width A=width B
holds for i being Nat st 1<=i & i<=width A holds Col(A-B,i)=Col(A,i)-Col(B,i)
proof
let A,B be Matrix of REAL;
assume that
A1: len A=len B and
A2: width A=width B;
A3: len (A-B)=len A by A1,A2,Th6;
let i be Nat;
A4: len Col(A,i)=len A by MATRIX_0:def 8;
assume 1<=i & i<=width A;
then
A5: i in Seg width A;
A6: len Col(B,i)=len B by MATRIX_0:def 8;
A7: dom A=dom B by A1,FINSEQ_3:29;
A8: for j being Nat st j in dom (A-B) holds (Col(A,i)-Col(B,i)).j = (A-B)*(
j,i)
proof
let j be Nat;
assume j in dom (A-B);
then j in Seg len (A-B) by FINSEQ_1:def 3;
then
A9: j in dom A by A3,FINSEQ_1:def 3;
then
A10: [j,i] in Indices A by A5,ZFMISC_1:87;
reconsider j as Nat;
Col(A,i).j=A*(j,i) & Col(B,i).j=B*(j,i) by A7,A9,MATRIX_0:def 8;
then Col(A,i).j-Col(B,i).j=(A-B)*(j,i) by A1,A2,A10,Th6;
hence thesis by A1,A4,A6,Lm1;
end;
len (Col(A,i)-Col(B,i))=len (Col(A,i)) by A1,A4,A6,RVSUM_1:116;
hence thesis by A4,A3,A8,MATRIX_0:def 8;
end;
theorem
for A being Matrix of n,k,REAL, B being Matrix of k,m,REAL,C being
Matrix of m,l,REAL st n>0 & k>0 & m>0 holds A*B*C=A*(B*C)
proof
let A be Matrix of n,k,REAL, B be Matrix of k,m,REAL,C be Matrix of m,l,REAL;
assume that
A1: n>0 and
A2: k>0 and
A3: m>0;
A4: width B=m & len C=m by A2,A3,MATRIX_0:23;
width A=k & len B=k by A1,A2,MATRIX_0:23;
hence thesis by A4,MATRIX_3:33;
end;
theorem Th28:
for A,B,C being Matrix of n,REAL holds A*B*C=A*(B*C)
proof
let A,B,C be Matrix of n,REAL;
A1: width B=n & len C=n by MATRIX_0:24;
width A=n & len B=n by MATRIX_0:24;
hence thesis by A1,MATRIX_3:33;
end;
theorem Th29:
for A being Matrix of n,D holds (A@)@=A
proof
let A be Matrix of n,D;
reconsider N=A@ as Matrix of n,D;
A1: len A=n & width A=n by MATRIX_0:24;
A2: Indices (N@)=[:Seg n,Seg n :] by MATRIX_0:24
.=Indices A by MATRIX_0:24;
A3: for i,j being Nat st [i,j] in Indices (N@) holds (N@)*(i,j) = A*(i,j)
proof
let i,j be Nat;
assume
A4: [i,j] in Indices (N@);
then [j,i] in Indices N by MATRIX_0:def 6;
then (N@)*(i,j)=N*(j,i) by MATRIX_0:def 6;
hence thesis by A2,A4,MATRIX_0:def 6;
end;
len (N@)=n & width (N@)=n by MATRIX_0:24;
hence thesis by A1,A3,MATRIX_0:21;
end;
theorem Th30:
for A,B being Matrix of n,REAL holds (A*B)@ = (B@)*(A@)
proof
let A,B be Matrix of n,REAL;
A1: len A=n by MATRIX_0:24;
A2: width A=n & len B=n by MATRIX_0:24;
A3: len (A*B)=n by MATRIX_0:24;
A4: width B=n by MATRIX_0:24;
A5: len (B@)=n by MATRIX_0:24;
then
A6: len ((B@)*(A@))=len (B@) by MATRIX_0:24;
A7: width (B@)=n by MATRIX_0:24
.=len (A@) by MATRIX_0:24;
A8: width (A*B)=n by MATRIX_0:24;
A9: width (A@)=n by MATRIX_0:24;
then
A10: width ((B@)*(A@))=width (A@) by MATRIX_0:24;
A11: now
let i,j be Nat;
A12: Indices ((A*B)@)=[:Seg n,Seg n :] by MATRIX_0:24;
assume
A13: [i,j] in Indices ((A*B)@);
then j in Seg len (A*B) by A3,A12,ZFMISC_1:87;
then
A14: j in dom (A*B) by FINSEQ_1:def 3;
i in Seg width (A*B) by A8,A13,A12,ZFMISC_1:87;
then
A15: [j,i]in Indices (A*B) by A14,ZFMISC_1:87;
Seg width (A@) = dom A by A1,A9,FINSEQ_1:def 3;
then j in dom A by A9,A13,A12,ZFMISC_1:87;
then
A16: Col(A@,j)=Line(A,j) by MATRIX_0:58;
reconsider i0=i,j0=j as Nat;
A17: Seg width B = dom (B@) by A4,A5,FINSEQ_1:def 3;
A18: Indices ((B@)*(A@))=[:Seg n,Seg n :] by MATRIX_0:24;
then [i,j] in [:dom (B@),Seg width (A@):] by A6,A10,A13,A12,FINSEQ_3:29;
then i in Seg width B by A17,ZFMISC_1:87;
then Line(B@,i)=Col(B,i) by MATRIX_0:59;
hence ((B@)*(A@))*(i,j)= Col(B,i0) "*" Line(A,j0) by A7,A13,A12,A18,A16,
MATRPROB:39
.=(A*B)*(j0,i0) by A2,A15,MATRPROB:39
.=((A*B)@)*(i,j) by A15,MATRIX_0:def 6;
end;
A19: len ((B@)*(A@))=n & width ((B@)*(A@))=n by MATRIX_0:24;
len ((A*B)@)=n & width ((A*B)@)=n by MATRIX_0:24;
hence thesis by A19,A11,MATRIX_0:21;
end;
theorem Th31:
for A being Matrix of REAL st len A=n & width A=m holds -A+A= 0_Rmatrix(n,m)
proof
let A be Matrix of REAL;
assume
A1: len A=n & width A=m;
len (-(MXR2MXF A)) =len A & width (-(MXR2MXF A)) = width A by MATRIX_1:def 4;
hence -A+A = MXF2MXR ((MXR2MXF A)+(-(MXR2MXF A))) by MATRIX_3:2
.=0_Rmatrix(n,m) by A1,MATRIX_4:2;
end;
begin :: Determinants
definition
let n;
let A be Matrix of n,REAL;
redefine func MXR2MXF A -> Matrix of n,F_Real; :: redefines MXR2MXF (MATRIXR1, definition)
coherence;
end;
definition
let n;
let A be Matrix of n,REAL;
func Det A -> Real equals
Det MXR2MXF A;
coherence;
end;
theorem
for A being Matrix of 2,REAL holds
Det A = (A*(1,1))*(A*(2,2))-(A*(1,2))*(A*(2,1))
proof
let A be Matrix of 2,REAL;
reconsider N=MXR2MXF A as Matrix of 2,F_Real;
Det A = (N*(1,1))*(N*(2,2))-(N*(1,2))*(N*(2,1)) by MATRIX_7:12;
hence thesis;
end;
theorem Th33:
for s1,s2,s3 be FinSequence st
len s1 = n & len s2 = n & len s3 = n holds <*s1,s2,s3*> is tabular
proof
let s1,s2,s3 be FinSequence;
assume
A1: len s1 = n & len s2 = n & len s3 = n;
now
take n;
let x be object;
assume x in rng (<*s1,s2,s3*>);
then
A2: x in { s1,s2,s3} by FINSEQ_2:128;
then reconsider r=x as FinSequence by ENUMSET1:def 1;
take r;
thus x= r & len r=n by A1,A2,ENUMSET1:def 1;
end;
hence thesis;
end;
theorem Th34:
for p1,p2,p3 being FinSequence of D st len p1 = n & len p2 = n &
len p3 = n holds <*p1,p2,p3*> is Matrix of 3,n,D
proof
let p1,p2,p3 be FinSequence of D;
reconsider q1 = p1,q2 = p2,q3=p3 as Element of D* by FINSEQ_1:def 11;
reconsider M = <*q1,q2,q3*> as FinSequence of D*;
assume
A1: len p1 =n & len p2 =n & len p3 =n;
then reconsider M as Matrix of D by Th33;
M is (3,n)-size
proof
thus len M = 3 by FINSEQ_1:45;
let r be FinSequence of D;
assume r in rng M;
then r in { p1,p2,p3 } by FINSEQ_2:128;
hence thesis by A1,ENUMSET1:def 1;
end;
hence thesis;
end;
theorem Th35:
for a1,a2,a3,b1,b2,b3,c1,c2,c3 being Element of D holds
<*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D
proof
let a1,a2,a3,b1,b2,b3,c1,c2,c3 be Element of D;
A1: len <*c1,c2,c3*>=3 by FINSEQ_1:45;
len <*a1,a2,a3*>=3 & len <*b1,b2,b3*>=3 by FINSEQ_1:45;
hence thesis by A1,Th34;
end;
theorem Th36:
for A being Matrix of n,D for p being FinSequence of D,
i being Nat st p=A.i & i in Seg n holds len p=n
proof
let A be Matrix of n,D;
let p be FinSequence of D, i be Nat;
assume that
A1: p=A.i and
A2: i in Seg n;
consider n2 being Nat such that
A3: for x being object st x in rng A ex s being FinSequence of D st s=x &
len s = n2 by MATRIX_0:9;
len A=n by MATRIX_0:24;
then
A4: i in dom A by A2,FINSEQ_1:def 3;
then A.i in rng A by FUNCT_1:def 3;
then consider s being FinSequence of D such that
A5: s=A.i and
len s = n2 by A3;
s in rng A by A4,A5,FUNCT_1:def 3;
hence thesis by A1,A5,MATRIX_0:def 2;
end;
theorem Th37:
for A being Matrix of 3,D holds
A=<* <* A*(1,1), A*(1,2), A*(1,3) *>,
<* A*(2,1), A*(2,2), A*(2,3) *>,
<* A*(3,1), A*(3,2), A*(3,3) *> *>
proof
let A be Matrix of 3,D;
reconsider B=<* <* A*(1,1), A*(1,2), A*(1,3) *>, <* A*(2,1), A*(2,2), A*(2,3
) *>, <* A*(3,1), A*(3,2), A*(3,3) *> *> as Matrix of 3,D by Th35;
A1: len A=3 & width A=3 by MATRIX_0:24;
A2: for i,j being Nat st [i,j] in Indices A holds A*(i,j) = B*(i,j)
proof
let i,j be Nat;
A3: Indices B=[: Seg 3,Seg 3 :] by MATRIX_0:24;
A4: Indices A=[: Seg 3,Seg 3 :] by MATRIX_0:24;
assume
A5: [i,j] in Indices A;
then
A6: i in Seg 3 by A4,ZFMISC_1:87;
2 in Seg 3;
then
A7: [i,2] in Indices A by A4,A6,ZFMISC_1:87;
1 in Seg 3;
then
A8: [i,1] in Indices A by A4,A6,ZFMISC_1:87;
3 in Seg 3;
then
A9: [i,3] in Indices A by A4,A6,ZFMISC_1:87;
A10: i in {1,2,3} by A5,A4,FINSEQ_3:1,ZFMISC_1:87;
now
per cases by A10,ENUMSET1:def 1;
case
A11: i=1;
reconsider p0=<* A*(1,1),A*(1,2), A*(1,3) *> as FinSequence of D;
A12: len p0=3 by FINSEQ_1:45;
A13: ex p23 being FinSequence of D st p23 = A.i & A*(i,3) = p23.3 by A9,
MATRIX_0:def 5;
consider p2 being FinSequence of D such that
A14: p2 = A.i and
A15: A*(i,1) = p2.1 by A8,MATRIX_0:def 5;
A16: ex p22 being FinSequence of D st p22 = A.i & A*(i,2) = p22.2 by A7,
MATRIX_0:def 5;
A17: for k be Nat st 1 <=k & k <= len p0 holds p0.k=p2.k
proof
let k be Nat;
assume
A18: 1 <=k & k <= len p0;
A19: k in Seg 3 by A12,A18;
per cases by A19,ENUMSET1:def 1,FINSEQ_3:1;
suppose
k=1;
hence thesis by A11,A15;
end;
suppose
k=2;
hence thesis by A11,A14,A16;
end;
suppose
k=3;
hence thesis by A11,A14,A13;
end;
end;
ex p being FinSequence of D st p = B.i & B*(i,j) = p.j by A5,A3,A4,
MATRIX_0:def 5;
then
A20: B*(i,j)=p0.j by A11;
len p2=3 by A6,A14,Th36;
hence
ex p being FinSequence of D st p = A.i & B*(i,j) = p.j by A12,A14,A17
,A20,FINSEQ_1:14;
end;
case
A21: i=2;
reconsider p0=<* A*(2,1),A*(2,2), A*(2,3) *> as FinSequence of D;
A22: len p0=3 by FINSEQ_1:45;
A23: ex p23 being FinSequence of D st p23 = A.i & A*(i,3) = p23.3 by A9,
MATRIX_0:def 5;
consider p2 being FinSequence of D such that
A24: p2 = A.i and
A25: A*(i,1) = p2.1 by A8,MATRIX_0:def 5;
A26: ex p22 being FinSequence of D st p22 = A.i & A*(i,2) = p22.2 by A7,
MATRIX_0:def 5;
A27: for k be Nat st 1 <=k & k <= len p0 holds p0.k=p2.k
proof
let k be Nat;
assume
A28: 1 <=k & k <= len p0;
A29: k in {1,2,3} by A22,A28,FINSEQ_3:1;
per cases by A29,ENUMSET1:def 1;
suppose
k=1;
hence thesis by A21,A25;
end;
suppose
k=2;
hence thesis by A21,A24,A26;
end;
suppose
k=3;
hence thesis by A21,A24,A23;
end;
end;
ex p being FinSequence of D st p = B.i & B*(i,j) = p.j by A5,A3,A4,
MATRIX_0:def 5;
then
A30: B*(i,j)=p0.j by A21;
len p2=3 by A6,A24,Th36;
hence
ex p being FinSequence of D st p = A.i & B*(i,j) = p.j by A22,A24,A27
,A30,FINSEQ_1:14;
end;
case
A31: i=3;
reconsider p0=<* A*(3,1),A*(3,2), A*(3,3) *> as FinSequence of D;
A32: len p0=3 by FINSEQ_1:45;
A33: ex p23 being FinSequence of D st p23 = A.i & A*(i,3) = p23.3 by A9,
MATRIX_0:def 5;
consider p2 being FinSequence of D such that
A34: p2 = A.i and
A35: A*(i,1) = p2.1 by A8,MATRIX_0:def 5;
A36: ex p22 being FinSequence of D st p22 = A.i & A*(i,2) = p22.2 by A7,
MATRIX_0:def 5;
A37: for k be Nat st 1 <=k & k <= len p0 holds p0.k=p2.k
proof
let k be Nat;
assume
A38: 1 <=k & k <= len p0;
A39: k in {1,2,3} by A32,A38,FINSEQ_3:1;
per cases by A39,ENUMSET1:def 1;
suppose
k=1;
hence thesis by A31,A35;
end;
suppose
k=2;
hence thesis by A31,A34,A36;
end;
suppose
k=3;
hence thesis by A31,A34,A33;
end;
end;
ex p being FinSequence of D st p = B.i & B*(i,j) = p.j by A5,A3,A4,
MATRIX_0:def 5;
then
A40: B*(i,j)=p0.j by A31;
len p2=3 by A6,A34,Th36;
hence
ex p being FinSequence of D st p = A.i & B*(i,j) = p.j by A32,A34,A37
,A40,FINSEQ_1:14;
end;
end;
hence thesis by A5,MATRIX_0:def 5;
end;
len B=3 & width B=3 by MATRIX_0:24;
hence thesis by A1,A2,MATRIX_0:21;
end;
theorem
for A being Matrix of 3,REAL holds
Det A = (A*(1,1))*(A*(2,2))*(A*(3,3))
- (A*(1,3))*(A*(2,2))*(A*(3,1))
- (A*(1,1))*(A*(2,3))*(A*(3,2))
+ (A*(1,2))*(A*(2,3))*(A*(3,1))
- (A*(1,2))*(A*(2,1))*(A*(3,3))
+ (A*(1,3))*(A*(2,1))*(A*(3,2))
proof
let A be Matrix of 3,REAL;
reconsider N=MXR2MXF A as Matrix of 3,F_Real;
reconsider N2=<* <* N*(1,1),N*(1,2), N*(1,3) *>, <* N*(2,1),N*(2,2), N*(2,3)
*>, <* N*(3,1),N*(3,2), N*(3,3) *> *> as Matrix of 3,F_Real by Th35;
Det A = Det N2 by Th37
.= (N*(1,1))*(N*(2,2))*(N*(3,3))-(N*(1,3))*(N*(2,2))*(N*(3,1)) -(N*(1,1)
)*(N*(2,3))*(N*(3,2))+(N*(1,2))*(N*(2,3))*(N*(3,1)) -(N*(1,2))*(N*(2,1))*(N*(3,
3))+(N*(1,3))*(N*(2,1))*(N*(3,2)) by MATRIX_9:46;
hence thesis;
end;
theorem
for f being Permutation of Seg 0 holds f=<*>NAT;
Lm4: idseq 0 is Permutation of Seg 0 by FINSEQ_2:55;
theorem Th40:
Permutations 0 = {<*>NAT}
proof
now
let p be object;
assume p in Permutations(0);
then reconsider q=p as Permutation of Seg 0 by MATRIX_1:def 16;
q=<*>NAT;
hence p in {<*>NAT} by TARSKI:def 1;
end;
then
A1: Permutations(0) c={<*>NAT};
{<*>NAT} c=Permutations(0)
proof
let x be object;
assume x in {<*>NAT};
then x is Permutation of Seg 0 by Lm4,TARSKI:def 1;
hence thesis by MATRIX_1:def 16;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th41:
for K being Ring
for A being Matrix of 0,K holds Det A = 1.K
proof
let K be Ring;
reconsider kk=idseq 0 as Element of Permutations(0) by Th40,TARSKI:def 1;
let A be Matrix of 0,K;
A1: (Path_product A).(idseq 0)=1.K
proof
reconsider p = idseq 0 as Element of Permutations(0)
by Lm4,MATRIX_1:def 16;
A2: -(1_K,p)=1_K
proof
reconsider q = id Seg 0 as Element of Permutations(0) by Lm4,
MATRIX_1:def 16;
len Permutations 0 = 0 by MATRIX_1:9;
then q is even by MATRIX_1:16;
hence thesis by MATRIX_1:def 20;
end;
1_K is_a_unity_wrt (the multF of K) by GROUP_1:21;
then len Path_matrix(p,A) = 0 & (the multF of K) is having_a_unity by
MATRIX_3:def 7,SETWISEO:def 2;
then
(the multF of K) $$ Path_matrix(p,A) = the_unity_wrt (the multF of K)
by FINSOP_1:def 1
.= 1_K by GROUP_1:22;
hence thesis by A2,MATRIX_3:def 8;
end;
Permutations 0 in Fin Permutations 0 by FINSUB_1:def 5; then
A3: In(Permutations(0),Fin Permutations 0) = Permutations(0)
by SUBSET_1:def 8
.= {. kk .} by Th40;
Det A=(the addF of K) $$ (In(Permutations(0),Fin Permutations 0),
Path_product(A)) by MATRIX_3:def 9
.=1.K by A1,A3,SETWISEO:17;
hence thesis;
end;
theorem
for A being Matrix of 0,REAL holds Det A = 1
proof
let A be Matrix of 0,REAL;
thus Det A = 1.F_Real by Th41
.=1;
end;
:: Removing condition n>=1 from MATRIX7:37
theorem Th43:
for K being commutative Ring
for n being Nat, A being Matrix of n,K holds Det A = Det (A@)
proof
let K be commutative Ring;
let n be Nat, A be Matrix of n,K;
n=0 or n>=1 & n is Nat by NAT_1:14;
then Det A=1_K & Det A@=1_K or Det A = Det A@ by Th41,MATRIX_7:37;
hence thesis;
end;
theorem
for A being Matrix of n,REAL holds Det A = Det (A@) by Th43;
:: Removing condition n>0 from MATRIX11:62
theorem Th45:
for K being commutative Ring
for A,B being Matrix of n,K holds Det(A*B) = (Det A)*(Det B)
proof
let K be commutative Ring;
let A,B be Matrix of n,K;
per cases;
suppose
n > 0;
hence thesis by MATRIX11:62;
end;
suppose
n<=0;
then
A1: n=0;
hence Det(A*B) = 1.K by Th41
.=1.K * 1.K
.=(Det A)*1.K by A1,Th41
.=(Det A)*(Det B) by A1,Th41;
end;
end;
theorem Th46:
for A,B being Matrix of n,REAL holds Det (A*B) = (Det A)*(Det B)
proof
set K=F_Real;
let A,B be Matrix of n,REAL;
reconsider Na=MXR2MXF A, Nb=MXR2MXF B as Matrix of n,K;
Det (A*B) = (Det Na) * (Det Nb) by Th45
.= (Det A)*(Det B);
hence thesis;
end;
begin :: Matrix as Operator
theorem
for x,y being FinSequence of REAL, A being Matrix of REAL st
len x=len A & len y=len x & len x>0 holds (x-y)*A=x*A - y*A
proof
let x,y be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: len x=len A and
A2: len y=len x and
A3: len x>0;
A4: width LineVec2Mx y=len y by MATRIXR1:def 10;
A5: width LineVec2Mx x=len x by MATRIXR1:def 10;
then
A6: width ((LineVec2Mx x)*A)=width A by A1,MATRIX_3:def 4
.=width ((LineVec2Mx y)*A) by A1,A2,A4,MATRIX_3:def 4;
A7: len LineVec2Mx y=1 by MATRIXR1:def 10;
A8: len LineVec2Mx x=1 by MATRIXR1:def 10;
then
A9: 1<=len((LineVec2Mx x)*A) by A1,A5,MATRIX_3:def 4;
A10: len ((LineVec2Mx x)*A)=len LineVec2Mx x by A1,A5,MATRIX_3:def 4
.=len LineVec2Mx y by A7,MATRIXR1:def 10
.=len((LineVec2Mx y)*A) by A1,A2,A4,MATRIX_3:def 4;
thus (x-y)*A=Line(((LineVec2Mx x)-(LineVec2Mx y))*A,1) by A2,Th23
.=Line((LineVec2Mx x)*A-(LineVec2Mx y)*A,1) by A1,A2,A3,A5,A4,A8,A7,Th16
.=x*A - y*A by A6,A10,A9,Th25;
end;
theorem
for x,y being FinSequence of REAL,A being Matrix of REAL st len x=
width A & len y=len x & len x >0 & len A >0 holds A*(x-y)=A*x - A*y
proof
let x,y be FinSequence of REAL, A be Matrix of REAL;
assume that
A1: len x=width A and
A2: len y=len x and
A3: len x >0 and
A4: len A >0;
A5: len ColVec2Mx y=len y by A2,A3,MATRIXR1:def 9;
A6: width ColVec2Mx y=1 by A2,A3,MATRIXR1:def 9;
A7: len ColVec2Mx x=len x by A3,MATRIXR1:def 9;
then
A8: len (A*(ColVec2Mx x))=len A by A1,MATRIX_3:def 4
.=len (A*(ColVec2Mx y)) by A1,A2,A5,MATRIX_3:def 4;
A9: width ColVec2Mx x=1 by A3,MATRIXR1:def 9;
then
A10: 1<=width(A*(ColVec2Mx x)) by A1,A7,MATRIX_3:def 4;
A11: width (A*(ColVec2Mx x))=width (ColVec2Mx (x)) by A1,A7,MATRIX_3:def 4
.=width (ColVec2Mx y) by A3,A6,MATRIXR1:def 9
.=width(A*(ColVec2Mx y)) by A1,A2,A5,MATRIX_3:def 4;
thus A*(x-y)=Col(A*((ColVec2Mx x)-(ColVec2Mx y)),1) by A2,A3,Th24
.=Col(A*(ColVec2Mx x)-A*(ColVec2Mx y),1) by A1,A2,A3,A4,A7,A5,A9,A6,Th20
.=A*x - A*y by A8,A11,A10,Th26;
end;
theorem
for x being FinSequence of REAL, A being Matrix of REAL st len A=len x
& len x>0 & width A>0 holds (-x)*A=-(x*A)
proof
let x be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: len A=len x and
A2: len x>0 and
A3: width A>0;
A4: (A@)*x=x*A by A1,A2,A3,MATRIXR1:52;
A5: width (A@)=len x by A1,A3,MATRIX_0:54;
then
A6: (A@)*(-x)=(-1)*((A@)*x) by A2,MATRIXR1:59;
A7: len (-x)=len x by RVSUM_1:114;
len (A@)>0 by A3,MATRIX_0:54;
then (-x)*((A@)@)=(A@)*(-x) by A2,A5,A7,MATRIXR1:53;
hence thesis by A1,A2,A3,A6,A4,MATRIX_0:57;
end;
theorem
for x being FinSequence of REAL,A being Matrix of REAL st len x=width
A & len x > 0 holds A*(-x)=-(A*x)
proof
let x be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: len x=width A and
A2: len x > 0;
A3: len ColVec2Mx x=len x by A2,MATRIXR1:def 9;
width ColVec2Mx x=1 by A2,MATRIXR1:def 9;
then
A4: 1<=width(A*(ColVec2Mx x)) by A1,A3,MATRIX_3:def 4;
thus A*(-x) =Col(A*((-1)*ColVec2Mx x),1) by A2,MATRIXR1:47
.=Col((-1)*(A*(ColVec2Mx x)),1) by A1,A3,MATRIXR1:40
.=-(A*x) by A4,MATRIXR1:56;
end;
theorem
for x being FinSequence of REAL,A being Matrix of REAL st len x=len A
& len x>0 holds x*(-A)=-(x*A)
proof
let x be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: len x=len A and
A2: len x>0;
A3: width A=len (x*A) by A1,MATRIXR1:62;
A4: len A=len (-A) & width A=width (-A) by MATRIX_1:def 4;
then
A5: len (x*(-A))=width A by A1,MATRIXR1:62;
x*(-A)+(x*A)=x*(-A+A) by A1,A4,MATRIXR1:64
.=x*(0_Rmatrix(len A,width A)) by Th31
.=0*(width A) by A1,A2,MATRIXR1:66;
hence thesis by A5,A3,Th1;
end;
theorem
for x being FinSequence of REAL,A being Matrix of REAL st len x=width
A & len A>0 & len x> 0 holds (-A)*x=-(A*x)
proof
let x be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: len x=width A and
A2: len A>0 and
A3: len x> 0;
A4: len ColVec2Mx x=len x & width ColVec2Mx x=1 by A3,MATRIXR1:def 9;
then
A5: 1<=width(A*(ColVec2Mx x)) by A1,MATRIX_3:def 4;
thus (-A)*x =Col(((-1)*A*(ColVec2Mx x)),1) by Th9
.=Col((-1)*(A*(ColVec2Mx x)),1) by A1,A2,A3,A4,MATRIXR1:41
.=-(A*x) by A5,MATRIXR1:56;
end;
theorem
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)
proof
let a be Real,x be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: width A=len x and
A2: len x>0;
A3: len ColVec2Mx x=len x by A2,MATRIXR1:def 9;
width ColVec2Mx x=1 by A2,MATRIXR1:def 9;
then
A4: 1<=width(A*(ColVec2Mx x)) by A1,A3,MATRIX_3:def 4;
thus A*(a*x)=Col(A*(a*ColVec2Mx x),1) by A2,MATRIXR1:47
.=Col(a*(A*(ColVec2Mx x)),1) by A1,A3,MATRIXR1:40
.=a*(A*x) by A4,MATRIXR1:56;
end;
theorem
for x being FinSequence of REAL, A,B being Matrix of REAL st len x=len
A & len A=len B & width A=width B & len A >0 holds x*(A-B)=(x*A) - (x*B)
proof
let x be FinSequence of REAL,A,B be Matrix of REAL;
assume that
A1: len x=len A and
A2: len A=len B and
A3: width A=width B and
A4: len A >0;
A5: width LineVec2Mx x=len x by MATRIXR1:def 10;
then
A6: len ((LineVec2Mx x)*A)=len LineVec2Mx x by A1,MATRIX_3:def 4
.=1 by MATRIXR1:def 10;
A7: len ((LineVec2Mx x)*A)= len LineVec2Mx x by A1,A5,MATRIX_3:def 4
.= len ((LineVec2Mx x)*B) by A1,A2,A5,MATRIX_3:def 4;
A8: width ((LineVec2Mx x)*A)=width A by A1,A5,MATRIX_3:def 4
.=width ((LineVec2Mx x)*B) by A1,A2,A3,A5,MATRIX_3:def 4;
len LineVec2Mx x=1 by MATRIXR1:def 10;
hence x*(A-B) =Line((LineVec2Mx x)*A-(LineVec2Mx x)*B,1) by A1,A2,A3,A4,A5
,Th20
.=(x*A) - (x*B) by A8,A7,A6,Th25;
end;
theorem
for x being FinSequence of REAL, A,B being Matrix of REAL st
len x = width A & len A = len B & width A = width B &
len x>0 & len A >0 holds (A-B)*x = A*x - B*x
proof
let x be FinSequence of REAL,A,B be Matrix of REAL;
assume that
A1: len x=width A and
A2: len A=len B and
A3: width A=width B and
A4: len x >0 and
A5: len A >0;
A6: len ColVec2Mx x=len x by A4,MATRIXR1:def 9;
then
A7: len (A*(ColVec2Mx x))=len A by A1,MATRIX_3:def 4
.=len (B*(ColVec2Mx x)) by A1,A2,A3,A6,MATRIX_3:def 4;
A8: width (A*(ColVec2Mx x))=width (ColVec2Mx x) by A1,A6,MATRIX_3:def 4
.=1 by A4,MATRIXR1:45;
A9: width (A*(ColVec2Mx x))= width (ColVec2Mx x) by A1,A6,MATRIX_3:def 4
.= width (B*(ColVec2Mx x)) by A1,A3,A6,MATRIX_3:def 4;
thus (A-B)*x =Col(A*(ColVec2Mx x)-B*(ColVec2Mx x),1) by A1,A2,A3,A4,A5,A6
,Th16
.=(A*x) - (B*x) by A7,A9,A8,Th26;
end;
theorem Th56:
for x being FinSequence of REAL,A being Matrix of REAL st
len A = len x holds (LineVec2Mx x)*A = LineVec2Mx (x*A)
proof
let x be FinSequence of REAL,A be Matrix of REAL;
A1: len LineVec2Mx (x*A)=1 by MATRIXR1:def 10;
assume
A2: len A=len x;
then
A3: width (MXR2MXF(LineVec2Mx x))=len MXR2MXF A by MATRIXR1:def 10;
width LineVec2Mx (x*A)=len (x*A) by MATRIXR1:def 10;
then
A4: width (LineVec2Mx (x*A))=width A by A2,MATRIXR1:62;
A5: len (x*A)=width A by A2,MATRIXR1:62;
then
A6: width (MXR2MXF (LineVec2Mx (x*A)))= width MXR2MXF A by MATRIXR1:def 10;
A7: width (LineVec2Mx x)=len x by MATRIXR1:def 10;
A8: for i,j being Nat st [i,j] in Indices (MXR2MXF (LineVec2Mx (x*A)))
holds MXR2MXF (LineVec2Mx (x*A))*(i,j) =Line(MXR2MXF(LineVec2Mx x),i) "*" Col((
MXR2MXF A),j)
proof
len ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)) =len MXR2MXF LineVec2Mx x
by A3,MATRIX_3:def 4;
then len ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)) = 1 by MATRIXR1:def 10;
then
A9: 1 in Seg len ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A));
let i,j be Nat;
A10: width ((LineVec2Mx x)*A)=width A by A2,A7,MATRIX_3:def 4;
assume
A11: [i,j] in Indices (MXR2MXF (LineVec2Mx (x*A)));
then
A12: j in Seg (width A) by A4,ZFMISC_1:87;
then j in dom (x*A) by A5,FINSEQ_1:def 3;
then
A13: (Line((LineVec2Mx x)*A,1)).j=(LineVec2Mx (x*A))*(1,j) by MATRIXR1:def 10;
Indices (LineVec2Mx (x*A))=[:Seg 1,Seg (width A):] by A1,A4,FINSEQ_1:def 3;
then i in Seg 1 by A11,ZFMISC_1:87;
then 1<=i & i<=1 by FINSEQ_1:1;
then
A14: i=1 by XXREAL_0:1;
width ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A))=width A by A3,MATRIX_3:def 4;
then [1,j] in [:Seg len ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)), Seg width
((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)):] by A12,A9,ZFMISC_1:87;
then
A15: [1,j] in Indices ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)) by FINSEQ_1:def 3;
width MXR2MXF LineVec2Mx x = len MXR2MXF A by A2,MATRIXR1:def 10;
then ((LineVec2Mx x)*A)*(1,j) =Line((MXR2MXF (LineVec2Mx x)),i) "*" Col((
MXR2MXF A),j) by A14,A15,MATRIX_3:def 4;
hence thesis by A12,A14,A13,A10,MATRIX_0:def 7;
end;
len MXR2MXF (LineVec2Mx (x*A)) = len (MXR2MXF(LineVec2Mx x)) by A1,
MATRIXR1:def 10;
hence thesis by A6,A3,A8,MATRIX_3:def 4;
end;
theorem Th57:
for x being FinSequence of REAL, A,B being Matrix of REAL st
len x = len A & width A = len B holds x*(A*B) = (x*A)*B
proof
let x be FinSequence of REAL,A,B be Matrix of REAL;
assume that
A1: len x=len A and
A2: width A=len B;
width LineVec2Mx x=len x by MATRIXR1:def 10;
hence x*(A*B) = Line((LineVec2Mx x)*A*B,1) by A1,A2,MATRIX_3:33
.=(x*A)*B by A1,Th56;
end;
theorem Th58:
for x being FinSequence of REAL,A being Matrix of REAL st width
A=len x & len x>0 & len A>0 holds A*(ColVec2Mx x)=ColVec2Mx (A*x)
proof
let x be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: width A=len x and
A2: len x>0 and
A3: len A>0;
A4: len ColVec2Mx x=len x by A2,MATRIXR1:def 9;
A5: len (MXR2MXF(ColVec2Mx x))=width MXR2MXF A by A1,A2,MATRIXR1:def 9;
then
A6: width ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x)))=width(ColVec2Mx x) by
MATRIX_3:def 4
.=1 by A2,MATRIXR1:def 9;
A7: len ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x)))=len A by A5,MATRIX_3:def 4;
A8: len (A*x)=len A by A1,A2,MATRIXR1:61;
then
A9: width (ColVec2Mx (A*x))=1 by A3,MATRIXR1:def 9;
A10: len (ColVec2Mx (A*x))=len A by A3,A8,MATRIXR1:def 9;
A11: len (ColVec2Mx (A*x))=len (A*x) by A3,A8,MATRIXR1:def 9;
A12: for i,j being Nat st [i,j] in Indices (MXR2MXF (ColVec2Mx (A*x))) holds
MXR2MXF (ColVec2Mx (A*x))*(i,j) =Line((MXR2MXF A),i) "*" Col(MXR2MXF(ColVec2Mx
x),j)
proof
let i,j be Nat;
A13: 1 in Seg 1 & Indices (ColVec2Mx (A*x))=[:Seg (len (ColVec2Mx (A*x))),
Seg 1:] by A9,FINSEQ_1:def 3;
assume
A14: [i,j] in Indices MXR2MXF (ColVec2Mx (A*x));
then
A15: j in Seg width ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x))) by A9,A6,ZFMISC_1:87;
A16: Indices (ColVec2Mx (A*x))=[:Seg len A,Seg 1:] by A8,A11,A9,FINSEQ_1:def 3;
then
A17: i in Seg (len A) by A14,ZFMISC_1:87;
then
A18: i in dom (A*x) by A8,FINSEQ_1:def 3;
i in Seg len ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x))) by A7,A14,A16,
ZFMISC_1:87;
then
[i,j] in [:Seg len ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x))), Seg width (
(MXR2MXF A)*(MXR2MXF (ColVec2Mx x))):] by A15,ZFMISC_1:87;
then
A19: [i,j] in Indices ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x))) by FINSEQ_1:def 3;
j in Seg 1 by A9,A14,ZFMISC_1:87;
then 1<=j & j<=1 by FINSEQ_1:1;
then
A20: j=1 by XXREAL_0:1;
i in Seg (len (ColVec2Mx (A*x))) by A10,A14,A16,ZFMISC_1:87;
then [i,1] in Indices (ColVec2Mx (A*x)) by A13,ZFMISC_1:87;
then
A21: ex p2 being FinSequence of REAL st p2=(ColVec2Mx (A*x)).i & (ColVec2Mx
(A*x))*(i,1)=p2.1 by MATRIX_0:def 5;
A22: (Col(A*(ColVec2Mx x),1)).i =(<*(A*x).i*>).1
.=(ColVec2Mx (A*x))*(i,1) by A3,A8,A18,A21,MATRIXR1:def 9;
len (A*(ColVec2Mx x))=len A by A1,A4,MATRIX_3:def 4;
then i in dom (A*(ColVec2Mx x)) by A17,FINSEQ_1:def 3;
then (Col(A*(ColVec2Mx x),1)).i=(A*(ColVec2Mx x))*(i,j) by A20,
MATRIX_0:def 8;
hence thesis by A5,A20,A22,A19,MATRIX_3:def 4;
end;
A23: len (MXR2MXF (ColVec2Mx (A*x))) = len (MXR2MXF A) by A3,A8,MATRIXR1:def 9;
width (MXR2MXF (ColVec2Mx (A*x))) = 1 by A3,A8,MATRIXR1:def 9
.= width (MXR2MXF(ColVec2Mx x)) by A2,MATRIXR1:def 9;
hence thesis by A23,A5,A12,MATRIX_3:def 4;
end;
theorem Th59:
for x being FinSequence of REAL, A,B being Matrix of REAL st len
x=width B & width A=len B & len x >0 & len B>0 holds (A*B)*x=A*(B*x)
proof
let x be FinSequence of REAL,A,B be Matrix of REAL;
assume that
A1: len x=width B and
A2: width A=len B and
A3: len x >0 and
A4: len B>0;
len ColVec2Mx x=len x by A3,MATRIXR1:def 9;
hence (A*B)*x = Col(A*(B*(ColVec2Mx x)),1) by A1,A2,MATRIX_3:33
.=A*(B*x) by A1,A3,A4,Th58;
end;
theorem
for B being (Matrix of n,m,REAL),A being (Matrix of m,k,REAL) st n>0
holds (for i,j st [i,j] in Indices (B*A) holds (B*A)*(i,j)=((Line(B,i))*A).j)
proof
let B be (Matrix of n,m,REAL),A be Matrix of m,k,REAL;
assume
A1: n>0;
then
A2: width B=m by MATRIX_0:23;
let i,j;
A3: len A=m by MATRIX_0:def 2;
then
A4: len A=len (Line(B,i)) by A2,MATRIX_0:def 7;
assume
A5: [i,j] in Indices (B*A);
then
A6: j in Seg width (B*A) by ZFMISC_1:87;
width B=len A by A1,A3,MATRIX_0:23;
then
A7: (B*A)*(i,j) =Line(B,i) "*" Col(A,j) by A5,MATRPROB:39;
width A=width (B*A) by A3,A2,MATRPROB:39;
then j in Seg len ((Line(B,i))*A) by A6,A4,MATRIXR1:62;
hence thesis by A7,A4,MATRPROB:40;
end;
theorem Th61:
for A, B being Matrix of n,REAL holds for i,j st [i,j] in
Indices (B*A) holds (B*A)*(i,j)=((Line(B,i))*A).j
proof
let A,B be Matrix of n,REAL;
let i,j;
assume
A1: [i,j] in Indices (B*A);
then
A2: j in Seg width (B*A) by ZFMISC_1:87;
A3: len A=n by MATRIX_0:def 2;
then width B=len A by MATRIX_0:24;
then
A4: (B*A)*(i,j) =Line(B,i) "*" Col(A,j) by A1,MATRPROB:39;
A5: width B=n by MATRIX_0:24;
then
A6: len A=len (Line(B,i)) by A3,MATRIX_0:def 7;
width A=width (B*A) by A3,A5,MATRPROB:39;
then j in Seg len ((Line(B,i))*A) by A2,A6,MATRIXR1:62;
hence thesis by A4,A6,MATRPROB:40;
end;
theorem
for A, B being Matrix of n,REAL st n>0 holds for i,j st [i,j] in
Indices (A*B) holds (A*B)*(i,j)=(A*(Col(B,j))).i
proof
let A, B be Matrix of n,REAL;
assume
A1: n>0;
let i,j;
A2: width A=n by MATRIX_0:24;
assume
A3: [i,j] in Indices (A*B);
then i in dom (A*B) by ZFMISC_1:87;
then
A4: i in Seg len (A*B) by FINSEQ_1:def 3;
A5: len B=n by MATRIX_0:def 2;
then
A6: width A=len (Col(B,j)) by A2,MATRIX_0:def 8;
width A=len B by A5,MATRIX_0:24;
then
A7: (A*B)*(i,j) = Line(A,i) "*" Col(B,j) by A3,MATRPROB:39;
len (A*B)=n & len A=n by MATRIX_0:24;
then i in Seg len (A*(Col(B,j))) by A1,A4,A2,A6,MATRIXR1:61;
hence thesis by A1,A2,A7,A6,MATRPROB:41;
end;
begin :: Identity and Zero of Matrix of REAL
definition
let n be Nat;
func 1_Rmatrix(n) -> Matrix of n,REAL equals
MXF2MXR (1.(F_Real,n));
correctness;
end;
theorem Th63:
(for i st [i,i] in Indices 1_Rmatrix n holds (1_Rmatrix n)*(i,i)
= 1) & for i,j st [i,j] in Indices (1_Rmatrix n) & i <> j holds (1_Rmatrix n)*(
i,j) = 0
proof
set K=F_Real;
thus for i st [i,i] in Indices 1_Rmatrix n holds (1_Rmatrix n)*(i,i) = 1
proof
let i;
assume [i,i] in Indices 1_Rmatrix n;
hence (1_Rmatrix n)*(i,i) = 1_ F_Real by MATRIX_1:def 3
.=1;
end;
let i,j;
assume [i,j] in Indices 1_Rmatrix n & i <> j;
hence (1_Rmatrix n)*(i,j) = 0.K by MATRIX_1:def 3
.=0;
end;
theorem Th64:
(1_Rmatrix(n))@=1_Rmatrix(n)
proof
per cases;
suppose
A1: n>0;
A2: len (1_Rmatrix(n))=n by MATRIX_0:24;
A3: Indices (1_Rmatrix(n)) = [:Seg n, Seg n:] by MATRIX_0:24;
A4: for i,j being Nat st [i,j] in Indices (1_Rmatrix(n)) holds (1_Rmatrix(
n))*(i,j)=((1_Rmatrix(n))@)*(i,j)
proof
let i,j be Nat;
reconsider i0=i,j0=j as Nat;
assume
A5: [i,j] in Indices (1_Rmatrix(n));
then i in Seg n & j in Seg n by A3,ZFMISC_1:87;
then
A6: [j,i] in Indices (1_Rmatrix(n) ) by A3,ZFMISC_1:87;
per cases;
suppose
i=j;
hence thesis by A5,MATRIX_0:def 6;
end;
suppose
i<>j;
then (1_Rmatrix(n))*(i0,j0)=0 & (1_Rmatrix(n))*(j0,i0)=0 by A5,A6,Th63;
hence thesis by A6,MATRIX_0:def 6;
end;
end;
A7: width (1_Rmatrix(n))=n by MATRIX_0:24;
then
len ((1_Rmatrix(n))@)=width (1_Rmatrix(n)) & width ((1_Rmatrix(n))@)=
len ( 1_Rmatrix n) by A1,MATRIX_0:54;
hence thesis by A7,A2,A4,MATRIX_0:21;
end;
suppose
n=0;
hence thesis by MATRIX_0:45;
end;
end;
theorem Th65:
for n,m being Nat st n>0 holds 0_Rmatrix(n,m)+
0_Rmatrix(n,m)=0_Rmatrix(n,m)
proof
let n,m be Nat;
assume
A1: n>0;
then width (0_Rmatrix(n,m))=m & len (0_Rmatrix(n,m))=n by MATRIX_0:23;
then (0+0) *(0_Rmatrix(n,m))=0_Rmatrix(n,m) by A1,MATRIXR1:44;
hence thesis by Th12;
end;
theorem
for a being Real st n>0 holds a*(0_Rmatrix(n,m)) = 0_Rmatrix(n,m)
proof
let a be Real;
A1: len (a*(0_Rmatrix(n,m)))=len (0_Rmatrix(n,m)) & width (a*(0_Rmatrix(n,m)
))= width (0_Rmatrix(n,m)) by MATRIXR1:27;
assume
A2: n>0;
then
A3: width (0_Rmatrix(n,m))=m & len (0_Rmatrix(n,m))=n by MATRIX_0:23;
a*(0_Rmatrix(n,m))=a*(0_Rmatrix(n,m)+0_Rmatrix(n,m)) by A2,Th65
.=a*(0_Rmatrix(n,m)) +a*(0_Rmatrix(n,m)) by MATRIXR1:43;
hence thesis by A3,A1,MATRIXR1:37;
end;
theorem Th67:
for K being commutative Ring, A being Matrix of K holds A*(1.(K,width A))=A
proof
let K be commutative Ring, A be Matrix of K;
set n=width A;
set B=1.(K,n);
A1: width B=n by MATRIX_0:24;
A2: len B=n by MATRIX_0:24;
then
A3: width (A*B)=width B by MATRIX_3:def 4;
A4: now
let i,j be Nat;
assume
A5: [i,j] in Indices (A*B);
then
A6: j in Seg width B by A3,ZFMISC_1:87;
then j in Seg len (Line(A,i)) by A1,MATRIX_0:def 7;
then
A7: j in dom (Line(A,i)) by FINSEQ_1:def 3;
A8: now
let k be Nat;
assume that
A9: k in dom (Col(B,j)) and
A10: k<>j;
k in Seg len (Col(B,j)) by A9,FINSEQ_1:def 3;
then k in Seg len B by MATRIX_0:def 8;
then k in dom B by FINSEQ_1:def 3;
then [k,j] in Indices B by A6,ZFMISC_1:87;
hence (Col(B,j)).k=0.K by A10,MATRIX_3:16;
end;
A11: j in Seg width A by A1,A3,A5,ZFMISC_1:87;
then j in dom B by A2,FINSEQ_1:def 3;
then [j,j] in Indices B by A1,A11,ZFMISC_1:87;
then
A12: (Col(B,j)).j=1_K by MATRIX_3:16;
j in Seg len (Col(B,j)) by A2,A1,A6,MATRIX_0:def 8;
then
A13: j in dom (Col(B,j)) by FINSEQ_1:def 3;
thus (A*B)*(i,j)= Line(A,i) "*" Col(B,j) by A2,A5,MATRIX_3:def 4
.=Col(B,j) "*" Line(A,i) by FVSUM_1:90
.=Sum(mlt(Col(B,j),Line(A,i))) by FVSUM_1:def 9
.=Line(A,i).j by A13,A7,A8,A12,MATRIX_3:17
.=A*(i,j) by A11,MATRIX_0:def 7;
end;
len (A*B)=len A by A2,MATRIX_3:def 4;
hence thesis by A1,A3,A4,MATRIX_0:21;
end;
theorem Th68:
for K being Ring
for A being Matrix of K holds (1.(K,len A))*A=A
proof
let K be Ring;
let A be Matrix of K;
set n=len A;
set B=1.(K,n);
A1: len B=n by MATRIX_0:24;
A2: width B=n by MATRIX_0:24;
then
A3: len (B*A)=len B by MATRIX_3:def 4;
A4: now
A5: dom A = Seg len A by FINSEQ_1:def 3;
let i,j be Nat;
assume
A6: [i,j] in Indices (B*A);
A7: dom (B*A) = Seg len (B*A) by FINSEQ_1:def 3;
then
A8: i in Seg width B by A1,A2,A3,A6,ZFMISC_1:87;
then i in Seg len(Line(B,i)) by MATRIX_0:def 7;
then
A9: i in dom (Line(B,i)) by FINSEQ_1:def 3;
A10: dom B = Seg len B by FINSEQ_1:def 3;
then
A11: i in dom B by A3,A6,A7,ZFMISC_1:87;
then [i,i] in Indices B by A8,ZFMISC_1:87;
then
A12: (Line(B,i)).i=1_K by MATRIX_3:15;
i in Seg len (Col(A,j)) by A2,A8,MATRIX_0:def 8;
then
A13: i in dom Col(A,j) by FINSEQ_1:def 3;
A14: now
let k be Nat;
assume that
A15: k in dom (Line (B,i)) and
A16: k<>i;
k in Seg len (Line (B,i)) by A15,FINSEQ_1:def 3;
then k in Seg width B by MATRIX_0:def 7;
then [i,k] in Indices B by A11,ZFMISC_1:87;
hence (Line(B,i)).k=0.K by A16,MATRIX_3:15;
end;
thus (B*A)*(i,j)= Line(B,i) "*" Col(A,j) by A2,A6,MATRIX_3:def 4
.=Sum(mlt(Line(B,i),Col(A,j))) by FVSUM_1:def 9
.=Col(A,j).i by A9,A13,A14,A12,MATRIX_3:17
.=A*(i,j) by A1,A5,A10,A11,MATRIX_0:def 8;
end;
width (B*A)=width A by A2,MATRIX_3:def 4;
hence thesis by A1,A3,A4,MATRIX_0:21;
end;
theorem
for A being Matrix of REAL holds (n=width A implies A*(1_Rmatrix n)=A)
& (m=len A implies (1_Rmatrix m)*A=A) by Th67,Th68;
theorem Th70:
for A being Matrix of n,REAL holds (1_Rmatrix n)*A=A
proof
let A be Matrix of n,REAL;
n=len A by MATRIX_0:def 2;
hence thesis by Th68;
end;
theorem Th71:
for A be Matrix of n,REAL holds A*(1_Rmatrix(n))=A
proof
let A be Matrix of n,REAL;
A1: n=len A by MATRIX_0:def 2;
now
per cases;
case
n<>0;
hence n=width A by A1,MATRIX_0:20;
end;
case
n=0;
hence n=width A by A1,MATRIX_0:def 3;
end;
end;
hence thesis by Th67;
end;
theorem Th72:
Det 1_Rmatrix n=1
proof
per cases;
suppose
n>=1;
hence Det 1_Rmatrix n=1_(F_Real) by MATRIX_7:16
.= 1;
end;
suppose
n<1;
then n=0 by NAT_1:25;
hence Det (1_Rmatrix n)=1.F_Real by Th41
.=1;
end;
end;
definition
let n be Nat;
func 0_Rmatrix(n) -> Matrix of n,REAL equals
0_Rmatrix(n,n);
correctness;
end;
theorem
n>0 implies Det 0_Rmatrix n = 0
proof
set K=F_Real;
assume n>0;
then n>=0+1 by NAT_1:13;
then Det (0_Rmatrix n)=0.K by MATRIX_7:15
.=0;
hence thesis;
end;
definition
let n,i be Nat;
func Base_FinSeq(n,i) -> FinSequence of REAL equals
(n |-> 0)+*(i,1);
coherence
proof
reconsider n as Nat;
(n |-> 0)+*(i,1) = Replace(n |-> In(0,REAL), i,In(1,REAL));
hence thesis;
end;
end;
reserve n,i,j for Nat;
theorem Th74:
len Base_FinSeq(n,i) = n
proof
len((n |-> 0)+*(i,1)) = len (n |-> 0) by FUNCT_7:97
.= n by CARD_1:def 7;
hence thesis;
end;
theorem Th75:
1<=i & i<=n implies (Base_FinSeq(n,i)).i=1
proof
A1: len (n |-> 0)=n by CARD_1:def 7;
assume 1<=i & i<=n;
then i in dom(n |-> 0) by A1,FINSEQ_3:25;
hence thesis by FUNCT_7:31;
end;
theorem Th76:
1<=j & j<=n & i<>j implies (Base_FinSeq(n,i)).j=0
proof
assume that
A1: 1<=j & j<=n and
A2: i<>j;
A3: j in Seg n by A1;
thus (Base_FinSeq(n,i)).j = (n |-> 0).j by A2,FUNCT_7:32
.= 0 by A3,FINSEQ_2:57;
end;
reserve n for Nat;
theorem
Base_FinSeq(1,1)= <* 1 *> & Base_FinSeq(2,1)= <* 1,0 *> & Base_FinSeq(
2,2)= <* 0,1 *> & Base_FinSeq(3,1)= <* 1,0,0 *> & Base_FinSeq(3,2)= <* 0,1,0 *>
& Base_FinSeq(3,3)= <* 0,0,1 *>
proof
thus Base_FinSeq(1,1) = Replace (<*In(0,REAL)*>,1,In(1,REAL))
by FINSEQ_2:59
.= <* 1 *> by FINSEQ_7:12;
thus Base_FinSeq(2,1)
= Replace (<* In(0,REAL),In(0,REAL)*>,1,In(1,REAL))
by FINSEQ_2:61
.= <* 1,0 *> by FINSEQ_7:13;
thus Base_FinSeq(2,2) = Replace (<* In(0,REAL),In(0,REAL) *>,2,In(1,REAL))
by FINSEQ_2:61
.= <* 0,1 *> by FINSEQ_7:14;
thus Base_FinSeq(3,1) = Replace (<* 0,0,0 *>,1,In(1,REAL)) by FINSEQ_2:62
.= <* 1,0,0 *> by FINSEQ_7:15;
thus Base_FinSeq(3,2) =
Replace (<* In(0,REAL),In(0,REAL), In(0,REAL )*>,2,In(1,REAL))
by FINSEQ_2:62
.= <* 0,1,0 *> by FINSEQ_7:16;
thus Base_FinSeq(3,3)
= Replace (<* In(0,REAL),In(0,REAL), In(0,REAL) *>,3,In(1,REAL))
by FINSEQ_2:62
.= <* 0,0,1 *> by FINSEQ_7:17;
end;
theorem Th78:
1<=i & i<=n implies (1_Rmatrix(n)).i=Base_FinSeq(n,i)
proof
assume
A1: 1<=i & i<=n;
then 1<=n by XXREAL_0:2;
then
A2: 1 in Seg n;
i in Seg n by A1;
then [i,1] in [:Seg n, Seg n:] by A2,ZFMISC_1:87;
then [i,1] in Indices (1.(F_Real,n)) by MATRIX_0:24;
then consider q being FinSequence of REAL such that
A3: q = (1_Rmatrix n).i and
(1_Rmatrix n)*(i,1) = q.1 by MATRIX_0:def 5;
len (1_Rmatrix(n))=n by MATRIX_0:24;
then i in dom 1_Rmatrix n by A1,FINSEQ_3:25;
then q in rng 1_Rmatrix n by A3,FUNCT_1:def 3;
then
A4: len q=n by MATRIX_0:def 2;
A5: for j be Nat st 1<=j & j<=n holds q.j=(Base_FinSeq(n,i)).j
proof
A6: i in Seg n by A1;
let j be Nat;
assume
A7: 1<=j & j<=n;
j in Seg n by A7;
then [i,j] in [:Seg n, Seg n:] by A6,ZFMISC_1:87;
then
A8: [i,j] in Indices (1.(F_Real,n)) by MATRIX_0:24;
then
A9: ex q0 being FinSequence of REAL st q0 = (1_Rmatrix(n)).i & (1_Rmatrix(
n))*(i,j) = q0.j by MATRIX_0:def 5;
per cases;
suppose
A10: i=j;
then (1.(F_Real,n))*(i,i) = 1_(F_Real) by A8,MATRIX_1:def 3;
hence thesis by A1,A3,A9,A10,Th75;
end;
suppose
A11: i<>j;
then (1.(F_Real,n))*(i,j) = 0.(F_Real) by A8,MATRIX_1:def 3;
hence thesis by A3,A7,A9,A11,Th76;
end;
end;
len Base_FinSeq(n,i)=n by Th74;
hence thesis by A3,A4,A5,FINSEQ_1:14;
end;
begin :: Inverse of Matrix
definition
let n be Nat,A be Matrix of n,REAL;
attr A is invertible means
ex B being Matrix of n,REAL st B*A= 1_Rmatrix(n) & A*B=1_Rmatrix(n);
end;
definition
let n be Nat,A be Matrix of n,REAL;
assume
A1: A is invertible;
func Inv(A) -> Matrix of n,REAL means
:Def6:
it*A=1_Rmatrix(n) & A*it= 1_Rmatrix(n);
existence by A1;
uniqueness
proof
let B1,B2 be Matrix of n,REAL;
assume that
B1*A=1_Rmatrix(n) and
A2: A*B1=1_Rmatrix(n) and
A3: B2*A=1_Rmatrix(n) and
A*B2=1_Rmatrix(n);
A4: len A=n & width A=n by MATRIX_0:24;
len B1=n & width B2=n by MATRIX_0:24;
then B2*A*B1=B2*1_Rmatrix(n) by A2,A4,MATRIX_3:33;
then B1=B2*1_Rmatrix(n) by A3,Th70;
hence thesis by Th71;
end;
end;
registration
let n;
cluster 1_Rmatrix n -> invertible;
coherence
proof
(1_Rmatrix(n))*(1_Rmatrix(n))=1_Rmatrix(n) by Th70;
hence thesis;
end;
end;
theorem
Inv(1_Rmatrix(n))=1_Rmatrix(n)
proof
(1_Rmatrix(n))*(1_Rmatrix n)=1_Rmatrix(n) by Th70;
hence thesis by Def6;
end;
theorem Th80:
for A,B1,B2 being Matrix of n,REAL st B1*A=1_Rmatrix(n) & A*B2=
1_Rmatrix(n) holds B1=B2 & A is invertible
proof
let A,B1,B2 be Matrix of n,REAL;
assume that
A1: B1*A=1_Rmatrix(n) and
A2: A*B2=1_Rmatrix(n);
A3: B1*A*B2=B1*(A*B2) by Th28
.= B1 by A2,Th71;
hence B1=B2 by A1,Th70;
B1*A*B2=B2 by A1,Th70;
hence thesis by A1,A2,A3;
end;
theorem
for A being Matrix of n,REAL st A is invertible holds Det Inv A = (Det A)"
proof
let A be Matrix of n,REAL;
assume A is invertible;
then A*(Inv A)=1_Rmatrix(n) by Def6;
then Det (A*(Inv A))=1 by Th72;
then
A1: Det(A)*Det (Inv A)=1 by Th46;
per cases;
suppose
Det A <> 0;
hence thesis by A1,XCMPLX_0:def 7;
end;
suppose
Det A=0;
hence thesis by A1;
end;
end;
theorem
for A being Matrix of n,REAL st A is invertible holds Det A <> 0
proof
let A be Matrix of n,REAL;
assume A is invertible;
then A*(Inv A)=1_Rmatrix(n) by Def6;
then Det (A*(Inv A))=1 by Th72;
then Det(A)*Det Inv A=1 by Th46;
hence thesis;
end;
theorem
for A,B being Matrix of n,REAL st A is invertible & B is invertible
holds A*B is invertible & Inv(A*B)=Inv(B)*(Inv A)
proof
let A,B be Matrix of n,REAL;
assume that
A1: A is invertible and
A2: B is invertible;
A3: (Inv(B)*(Inv(A)))*(A*B)=(Inv(B)*(Inv(A)))*A*B by Th28
.=(Inv(B))*((Inv(A))*A)*B by Th28
.=(Inv(B))*(1_Rmatrix(n))*B by A1,Def6
.=(Inv(B))*B by Th71
.=1_Rmatrix(n) by A2,Def6;
A4: (A*B)*(Inv(B)*(Inv(A)))=A*(B*(Inv(B)*(Inv(A)))) by Th28
.=A*((B*(Inv(B)))*(Inv(A))) by Th28
.=A*((1_Rmatrix(n))*(Inv(A))) by A2,Def6
.=A*(1_Rmatrix(n))*(Inv(A)) by Th28
.=A*(Inv(A)) by Th71
.=1_Rmatrix(n) by A1,Def6;
hence A*B is invertible by A3;
hence thesis by A3,A4,Def6;
end;
theorem
for A be Matrix of n,REAL st A is invertible holds Inv Inv A = A
proof
let A be Matrix of n,REAL;
assume A is invertible;
then
A1: Inv(A)*A=1_Rmatrix(n) & A*(Inv(A))=1_Rmatrix(n) by Def6;
then Inv(A) is invertible;
hence thesis by A1,Def6;
end;
theorem
1_Rmatrix(0)=0_Rmatrix(0) & 1_Rmatrix(0)={}
proof
A1: len 1_Rmatrix(0) = 0 by MATRIX_0:24;
len 0_Rmatrix(0) = 0 by MATRIX_0:24;
then 0_Rmatrix(0)={};
hence 1_Rmatrix(0)=0_Rmatrix(0) by A1;
thus thesis by A1;
end;
theorem Th86:
for x being FinSequence of REAL st len x=n & n>0 holds ( 1_Rmatrix n)*x=x
proof
let x be FinSequence of REAL;
assume that
A1: len x=n and
A2: n>0;
A3: len (ColVec2Mx x)=len x by A1,A2,MATRIXR1:def 9;
A4: len Col((ColVec2Mx x),1) = len (ColVec2Mx x) by MATRIX_0:def 8;
A5: for k being Nat st 1 <=k & k <= len (Col((ColVec2Mx x),1)) holds (Col((
ColVec2Mx x),1)).k=x.k
proof
let k be Nat;
assume
A6: 1 <=k & k <= len (Col((ColVec2Mx x),1));
A7: k in Seg len ColVec2Mx x by A4,A6;
then
A8: k in dom (ColVec2Mx x) by FINSEQ_1:def 3;
then
A9: Col((ColVec2Mx x),1).k = (ColVec2Mx x)*(k,1) by MATRIX_0:def 8;
1 in Seg 1 & Indices (ColVec2Mx x)=[:dom (ColVec2Mx x),Seg 1:] by A1,A2,
MATRIXR1:def 9;
then [k,1] in Indices (ColVec2Mx x) by A8,ZFMISC_1:87;
then consider p being FinSequence of REAL such that
A10: p=(ColVec2Mx x).k and
A11: (ColVec2Mx x)*(k,1)=p.1 by MATRIX_0:def 5;
k in dom x by A3,A7,FINSEQ_1:def 3;
then p=<* x.k *> by A1,A2,A10,MATRIXR1:def 9;
hence thesis by A9,A11;
end;
(1_Rmatrix n)*x =Col(MXF2MXR (MXR2MXF (ColVec2Mx x)),1) by A1,A3,Th68
.=x by A3,A4,A5;
hence thesis;
end;
theorem Th87:
for n being Nat,x,y being FinSequence of REAL, A be
Matrix of n,REAL st A is invertible & len x=n & len y=n & n>0 holds A*x=y iff x
=Inv(A)*y
proof
let n be Nat,x,y be FinSequence of REAL, A be Matrix of n,REAL;
assume that
A1: A is invertible and
A2: len x=n and
A3: len y=n and
A4: n>0;
A5: width A=n & width (Inv(A))=n by MATRIX_0:24;
A6: len A=n by MATRIX_0:24;
thus A*x=y implies x=Inv(A)*y
proof
assume
A7: A*x=y;
thus x=(1_Rmatrix(n))*x by A2,A4,Th86
.=((Inv A)*A) *x by A1,Def6
.=Inv(A)*y by A2,A4,A6,A5,A7,Th59;
end;
A8: len (Inv(A))=n by MATRIX_0:24;
x=Inv(A)*y implies A*x=y
proof
assume
A9: x=Inv(A)*y;
thus y=(1_Rmatrix(n))*y by A3,A4,Th86
.=(A*(Inv A))*y by A1,Def6
.=A*x by A3,A4,A8,A5,A9,Th59;
end;
hence thesis;
end;
theorem Th88:
for x being FinSequence of REAL st len x=n holds x*(1_Rmatrix n) =x
proof
let x be FinSequence of REAL;
A1: width (LineVec2Mx x)=len x by MATRIXR1:def 10;
assume len x=n;
then x*(1_Rmatrix n) =Line(MXF2MXR (MXR2MXF (LineVec2Mx x)),1) by A1,Th67
.=x by MATRIXR1:48;
hence thesis;
end;
theorem Th89:
for x,y being FinSequence of REAL,A be Matrix of n,REAL st A is
invertible & len x=n & len y=n holds x*A=y iff x=y*Inv(A)
proof
let x,y be FinSequence of REAL, A be Matrix of n,REAL;
assume that
A1: A is invertible and
A2: len x=n and
A3: len y=n;
A4: len A=n & len Inv A=n by MATRIX_0:24;
A5: width A=n by MATRIX_0:24;
thus x*A=y implies x=y*Inv(A)
proof
assume
A6: x*A=y;
thus x=x*(1_Rmatrix n) by A2,Th88
.=x*(A*(Inv A)) by A1,Def6
.=y*(Inv A) by A2,A5,A4,A6,Th57;
end;
assume
A7: x=y*(Inv A);
A8: width Inv A=n by MATRIX_0:24;
thus y=y*(1_Rmatrix(n)) by A3,Th88
.= y*((Inv A)*A) by A1,Def6
.= x*A by A3,A4,A8,A7,Th57;
end;
theorem
for A being Matrix of n,REAL st n>0 & A is invertible holds for y
being FinSequence of REAL st len y=n holds ex x being FinSequence of REAL st
len x=n & A*x=y
proof
let A be Matrix of n,REAL;
assume that
A1: n>0 and
A2: A is invertible;
let y be FinSequence of REAL;
assume
A3: len y=n;
reconsider x0=(Inv A)*y as FinSequence of REAL;
len Inv(A)=n & width Inv(A) =n by MATRIX_0:24;
then
A4: len x0=n by A1,A3,MATRIXR1:61;
then A*x0=y by A1,A2,A3,Th87;
hence thesis by A4;
end;
theorem
for A being Matrix of n,REAL st A is invertible holds for y being
FinSequence of REAL st len y=n holds ex x being FinSequence of REAL st len x=n
& x*A=y
proof
let A be Matrix of n,REAL;
assume
A1: A is invertible;
let y be FinSequence of REAL;
assume
A2: len y=n;
reconsider x0=y*(Inv A) as FinSequence of REAL;
len Inv(A)=n by MATRIX_0:24;
then
A3: len x0=width Inv A by A2,MATRIXR1:62
.=n by MATRIX_0:24;
then x0*A=y by A1,A2,Th89;
hence thesis by A3;
end;
theorem
for A being Matrix of n,REAL for x,y being FinSequence of REAL st len
x=n & len y=n & x*A=y holds for j being Nat st 1<=j & j<=n holds y.j
=|(x,Col(A,j))|
proof
let A be Matrix of n,REAL;
let x,y be FinSequence of REAL;
assume that
A1: len x=n and
A2: len y=n and
A3: x*A=y;
let j be Nat;
assume 1<=j & j<=n;
then j in Seg len (x*A) by A2,A3;
hence thesis by A1,A3,MATRIX_0:24,MATRPROB:40;
end;
theorem Th93:
for A being Matrix of n,REAL st (for y being FinSequence of REAL
st len y=n holds (ex x being FinSequence of REAL st len x=n & x*A=y)) holds ex
B being Matrix of n,REAL st B*A=1_Rmatrix(n)
proof
let A be Matrix of n,REAL;
defpred P[set,set] means for s being Nat,q being FinSequence of
REAL st s=$1 & q=$2 holds len q=n & q*A=Base_FinSeq(n,s);
assume
A1: for y being FinSequence of REAL st len y=n holds ex x being
FinSequence of REAL st len x=n & x*A=y;
A2: for i holds ex x being FinSequence of REAL st len x=n & x*A=Base_FinSeq(
n,i)
proof
let i;
len Base_FinSeq(n,i)=n by Th74;
hence thesis by A1;
end;
A3: for j being Nat st j in Seg n ex d being Element of REAL* st P[j,d]
proof
let j be Nat;
assume j in Seg n;
consider x being FinSequence of REAL such that
A4: len x=n & x*A=Base_FinSeq(n,j) by A2;
reconsider d0=x as Element of REAL* by FINSEQ_1:def 11;
for s being Nat,q being FinSequence of REAL st s=j & q=d0
holds len q=n & q*A=Base_FinSeq(n,s) by A4;
hence thesis;
end;
consider f being FinSequence of REAL* such that
A5: len f = n & for j being Nat st j in Seg n holds P[j,(f/.j)] from
FINSEQ_4:sch 1(A3);
for x being object st x in rng f ex p being FinSequence of REAL st x = p &
len p = n
proof
let x be object;
assume x in rng f;
then consider z being object such that
A6: z in dom f and
A7: f.z=x by FUNCT_1:def 3;
reconsider j0=z as Nat by A6;
reconsider q0=f/.j0 as FinSequence of REAL by FINSEQ_1:def 11;
z in Seg len f by A6,FINSEQ_1:def 3;
then
A8: len q0=n by A5;
q0=x by A6,A7,PARTFUN1:def 6;
hence thesis by A8;
end;
then reconsider M=f as Matrix of REAL by MATRIX_0:9;
for p being FinSequence of REAL st p in rng M holds len p = n
proof
let p be FinSequence of REAL;
assume p in rng M;
then consider z being object such that
A9: z in dom f and
A10: M.z=p by FUNCT_1:def 3;
reconsider j0=z as Nat by A9;
reconsider q0=f/.j0 as FinSequence of REAL by FINSEQ_1:def 11;
z in Seg len f & q0=p by A9,A10,FINSEQ_1:def 3,PARTFUN1:def 6;
hence thesis by A5;
end;
then reconsider B=M as Matrix of n,REAL by A5,MATRIX_0:def 2;
for i4,j4 being Nat st [i4,j4] in Indices (B*A) holds (B*A)*(i4,j4)=
1_Rmatrix(n)*(i4,j4)
proof
let i4,j4 be Nat;
reconsider i=i4,j=j4 as Nat;
consider n2 being Nat such that
A11: for x being object st x in rng (M*A) ex p being FinSequence of REAL
st x = p & len p = n2 by MATRIX_0:9;
assume
A12: [i4,j4] in Indices (B*A);
then j in Seg width (M*A) by ZFMISC_1:87;
then
A13: 1<=j & j<=width (M*A) by FINSEQ_1:1;
i in dom (M*A) by A12,ZFMISC_1:87;
then
A14: (M*A).i in rng (M*A) by FUNCT_1:def 3;
then consider p2 being FinSequence of REAL such that
A15: (M*A).i = p2 and
A16: len p2 = n2 by A11;
A17: len B=n by MATRIX_0:24;
A18: [i,j] in [:Seg n,Seg n:] by A12,MATRIX_0:24;
then [i,j] in Indices (1_Rmatrix(n)) by MATRIX_0:24;
then
A19: ex p3 being FinSequence of REAL st p3 = (1_Rmatrix(n)).i & 1_Rmatrix(n
)*(i,j) = p3.j by MATRIX_0:def 5;
A20: width (B*A)=n by MATRIX_0:24;
j in Seg n by A18,ZFMISC_1:87;
then
A21: 1<=j & j<=n by FINSEQ_1:1;
A22: i in Seg n by A18,ZFMISC_1:87;
then
A23: 1<=i & i<=n by FINSEQ_1:1;
A24: len (B*A) = n & for p being FinSequence of REAL st p in rng (B*A)
holds len p = n by MATRIX_0:def 2;
now
per cases;
case
A25: i=j;
reconsider g=f/.i as FinSequence of REAL by FINSEQ_1:def 11;
A26: g*A=Base_FinSeq(n,i) by A5,A22;
len B=n by MATRIX_0:24;
then f/.i=M.i by A23,FINSEQ_4:15;
then
A27: g=Line(B,i) by A23,A17,Lm2;
A28: 1_Rmatrix(n)*(i,j)=(Base_FinSeq(n,i)).i by A19,A23,A25,Th78
.=1 by A23,Th75;
p2.j=(B*A)*(i,j) by A24,A14,A15,A16,A13,A23,A20,Th2
.=(Base_FinSeq(n,i)).j by A12,A26,A27,Th61
.=1 by A23,A25,Th75;
hence 1_Rmatrix(n)*(i,j) = p2.j by A28;
end;
case
A29: i<>j;
reconsider g=f/.i as FinSequence of REAL by FINSEQ_1:def 11;
len B=n by MATRIX_0:24;
then f/.i=M.i by A23,FINSEQ_4:15;
then g=Line(B,i) by A23,A17,Lm2;
then
A30: (Line(B,i))*A=Base_FinSeq(n,i) by A5,A22;
A31: 1_Rmatrix(n)*(i,j)=(Base_FinSeq(n,i)).j by A19,A23,Th78
.=0 by A21,A29,Th76;
p2.j=(B*A)*(i,j) by A24,A14,A15,A16,A13,A23,A20,Th2
.=(Base_FinSeq(n,i)).j by A12,A30,Th61
.=0 by A21,A29,Th76;
hence 1_Rmatrix(n)*(i,j) = p2.j by A31;
end;
end;
hence thesis by A12,A15,MATRIX_0:def 5;
end;
hence thesis by MATRIX_0:27;
end;
theorem
for x being FinSequence of REAL, A being Matrix of n,REAL st n>0 & len
x=n holds (A@)*x = x*A
proof
let x be FinSequence of REAL,A be Matrix of n,REAL;
A1: len A=n & width A=n by MATRIX_0:24;
assume n>0 & len x=n;
hence thesis by A1,MATRIXR1:52;
end;
theorem Th95:
for x being FinSequence of REAL, A being Matrix of n,REAL st n>0
& len x=n holds x*(A@) = A*x
proof
let x be FinSequence of REAL,A be Matrix of n,REAL;
A1: len A=n & width A=n by MATRIX_0:24;
assume n>0 & len x=n;
hence thesis by A1,MATRIXR1:53;
end;
theorem Th96:
for A being Matrix of n,REAL st n>0 & (for y being FinSequence
of REAL st len y=n holds (ex x being FinSequence of REAL st len x=n & A*x=y))
holds ex B being Matrix of n,REAL st A*B=1_Rmatrix(n)
proof
let A be Matrix of n,REAL;
assume that
A1: n>0 and
A2: for y being FinSequence of REAL st len y=n holds ex x being
FinSequence of REAL st len x=n & A*x=y;
for y being FinSequence of REAL st len y=n holds ex x being FinSequence
of REAL st len x=n & x*A@=y
proof
let y be FinSequence of REAL;
assume len y=n;
then consider x0 being FinSequence of REAL such that
A3: len x0=n and
A4: A*x0=y by A2;
x0*A@=A*x0 by A1,A3,Th95;
hence thesis by A3,A4;
end;
then consider B being Matrix of n,REAL such that
A5: B*(A@)=1_Rmatrix n by Th93;
(B*(A@))@=1_Rmatrix n by A5,Th64;
then (A@@)*B@=1_Rmatrix n by Th30;
then A*(B@)=1_Rmatrix n by Th29;
hence thesis;
end;
theorem
for A being Matrix of n,REAL st n>0 & (for y being FinSequence of REAL
st len y=n holds (ex x1,x2 being FinSequence of REAL st len x1=n & len x2=n & A
*x1=y & x2*A=y)) holds A is invertible
proof
let A be Matrix of n,REAL;
assume that
A1: n>0 and
A2: for y being FinSequence of REAL st len y=n holds ex x1,x2 being
FinSequence of REAL st len x1=n & len x2=n & A*x1=y & x2*A=y;
for y being FinSequence of REAL st len y=n holds ex x being FinSequence
of REAL st len x=n & x*A=y
proof
let y be FinSequence of REAL;
assume len y=n;
then ex x1,x2 being FinSequence of REAL st len x1=n & len x2= n & A*x1=y &
x2*A=y by A2;
hence thesis;
end;
then
A3: ex B1 being Matrix of n,REAL st B1*A=1_Rmatrix(n) by Th93;
for y being FinSequence of REAL st len y=n holds ex x being FinSequence
of REAL st len x=n & A*x=y
proof
let y be FinSequence of REAL;
assume len y=n;
then ex x1,x2 being FinSequence of REAL st len x1=n & len x2= n & A*x1=y &
x2*A=y by A2;
hence thesis;
end;
then ex B2 being Matrix of n,REAL st A*B2=1_Rmatrix(n) by A1,Th96;
hence thesis by A3,Th80;
end;