:: A Theory of Matrices of Real Elements
:: by Yatsuka Nakamura , Nobuyuki Tamura and Wenpai Chang
::
:: Received February 20, 2006
:: Copyright (c) 2006-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, NAT_1, REAL_1, SUBSET_1, VECTSP_1, ARYTM_3, RELAT_1,
FINSEQ_1, ARYTM_1, EUCLID, FINSEQ_2, CARD_1, XBOOLE_0, ALGSTR_0,
STRUCT_0, XXREAL_0, FUNCT_1, MATRIX_1, TREES_1, INCSP_1, FVSUM_1, CARD_3,
RVSUM_1, QC_LANG1, GROUP_1, SUPINF_2, MATRIXR1, FUNCSDOM;
notations TARSKI, SUBSET_1, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, ORDINAL1,
FUNCT_1, MATRIX_0, NUMBERS, VECTSP_1, RELSET_1, FINSEQ_1, STRUCT_0,
ALGSTR_0, RLVECT_1, GROUP_1, MATRIX_1, MATRIX_3, RVSUM_1, FINSEQ_2,
FVSUM_1, EUCLID;
constructors REAL_1, BINOP_2, FVSUM_1, GOBOARD1, MATRIX_3, RVSUM_1, RELSET_1;
registrations RELSET_1, NUMBERS, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2,
STRUCT_0, VECTSP_1, VALUED_0, ORDINAL1, XREAL_0, RVSUM_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities VECTSP_1, MATRIX_0, STRUCT_0, VALUED_1;
theorems MATRIX_3, MATRIX_0, MATRIX_4, MATRIX_5, XREAL_0, FUNCT_1, FINSEQ_1,
FINSEQ_2, TARSKI, FVSUM_1, ZFMISC_1, RVSUM_1, EUCLID, FINSEQ_3, XXREAL_0,
ORDINAL1, VALUED_1, MATRIX_1;
schemes FINSEQ_1, MATRIX_0;
begin :: Preliminaries
reserve i,j for Nat;
theorem
for r1,r2 being Real, fr1,fr2 being Element of F_Real
st r1=fr1 & r2=fr2 holds r1+r2=fr1+fr2;
theorem
for r1,r2 being Real, fr1,fr2 being Element of F_Real
st r1=fr1 & r2=fr2 holds r1*r2=fr1*fr2;
theorem Th3:
for F being FinSequence of REAL holds F + -F = 0*(len F) & F - F = 0*(len F)
proof
let F be FinSequence of REAL;
set n=len F;
reconsider R=F as Element of n-tuples_on REAL by FINSEQ_2:92;
A1: R + -R = (n|->(0 qua Real)) by RVSUM_1:22;
hence F + -F = 0*(len F) by EUCLID:def 4;
thus thesis by A1,EUCLID:def 4;
end;
theorem
for F1,F2 being FinSequence of REAL st len F1=len F2 holds
F1 - F2 = F1 + - F2;
theorem
for F being FinSequence of REAL holds F - 0*(len F) = F
proof
let F be FinSequence of REAL;
set n=len F;
reconsider R=F as Element of n-tuples_on REAL by FINSEQ_2:92;
R - (n|->(0 qua Real)) = R by RVSUM_1:32;
hence thesis by EUCLID:def 4;
end;
theorem
for F being FinSequence of REAL holds 0*(len F) -F = -F
proof
let F be FinSequence of REAL;
set n=len F;
reconsider R=F as Element of n-tuples_on REAL by FINSEQ_2:92;
(n|->(0 qua Real)) - R = -R by RVSUM_1:33;
hence thesis by EUCLID:def 4;
end;
theorem
for F1,F2 being FinSequence of REAL st len F1=len F2 holds
F1 - -F2 = F1 + F2;
theorem
for F1,F2 being FinSequence of REAL st len F1=len F2 holds
-(F1 - F2) = F2 - F1 by RVSUM_1:35;
theorem
for F1,F2 being FinSequence of REAL st len F1=len F2 holds -(F1 - F2)
= -F1 + F2 by RVSUM_1:36;
theorem
for F1,F2 being FinSequence of REAL st len F1=len F2 & F1 - F2 = 0*(
len F1) holds F1=F2
proof
let F1,F2 be FinSequence of REAL;
set n=len F1;
assume len F1=len F2;
then reconsider R1=F1, R2=F2 as Element of n-tuples_on REAL by FINSEQ_2:92;
R1 - R2 = (n|->0) implies R1 = R2 by RVSUM_1:38;
hence thesis by EUCLID:def 4;
end;
theorem
for F1,F2,F3 being FinSequence of REAL st len F1=len F2 & len F2=len
F3 holds F1 - F2 - F3 = F1 - (F2 + F3) by RVSUM_1:39;
theorem
for F1,F2,F3 being FinSequence of REAL st len F1=len F2 & len F2=len
F3 holds F1 + (F2 - F3) = F1 + F2 - F3 by RVSUM_1:40;
theorem
for F1,F2,F3 being FinSequence of REAL st len F1=len F2 & len F2=len
F3 holds F1 - (F2 - F3) = F1 - F2 + F3 by RVSUM_1:41;
theorem Th14:
for F1,F2 being FinSequence of REAL st len F1=len F2 holds F1 = F1 + F2 - F2
proof
let F1,F2 be FinSequence of REAL;
set n=len F1;
assume len F1=len F2;
then reconsider R1=F1, R2=F2 as Element of n-tuples_on REAL by FINSEQ_2:92;
R1 = R1 + R2 - R2 by RVSUM_1:42;
hence thesis;
end;
theorem
for F1,F2 being FinSequence of REAL st len F1=len F2 holds F1 = F1 - F2 + F2
proof
let F1,F2 be FinSequence of REAL;
set n=len F1;
assume len F1=len F2;
then reconsider R1=F1, R2=F2 as Element of n-tuples_on REAL by FINSEQ_2:92;
R1 = R1 - R2 + R2 by RVSUM_1:43;
hence thesis;
end;
begin :: Matrices of Real Elements
theorem Th16:
for K being non empty multMagma, p being FinSequence of K, a
being Element of K holds len (a*p)=len p
proof
let K be non empty multMagma, p be FinSequence of K, a be Element of K;
reconsider q=p as Element of (len p)-tuples_on the carrier of K by
FINSEQ_2:92;
a*q in (len p)-tuples_on the carrier of K;
then
a*q in { s where s is Element of (the carrier of K)*: len s = len p } by
FINSEQ_2:def 4;
then ex s being Element of (the carrier of K)* st a*q=s & len s = len p;
hence thesis;
end;
theorem Th17:
for r being Real, fr being Element of F_Real, p being
FinSequence of REAL, fp being FinSequence of F_Real st r=fr & p=fp holds r*p=fr
*fp
proof
let r be Real, fr be Element of F_Real, p be FinSequence of REAL,
fp be FinSequence of F_Real;
assume that
A1: r=fr and
A2: p=fp;
A3: len (r*p)=len fp by A2,RVSUM_1:117;
then
A4: len (r*p)=len (fr*fp) by Th16;
for i be Nat st 1<=i & i<=len (r*p) holds (r*p).i=(fr*fp).i
proof
let i be Nat;
assume 1<=i & i<=len (r*p);
then
i in Seg len fp by A3,FINSEQ_1:1;
then
A5: i in dom (fr*fp) by A3,A4,FINSEQ_1:def 3;
reconsider s=fp.i as Element of F_Real by XREAL_0:def 1;
thus (r*p).i=fr*s by A1,A2,RVSUM_1:44
.= (fr*fp).i by A5,FVSUM_1:50;
end;
hence thesis by A4,FINSEQ_1:14;
end;
theorem
for K being Field, a being Element of K, A being Matrix of K holds
Indices (a*A) = Indices A
proof
let K be Field, a be Element of K, A be Matrix of K;
len (a*A)=len A & width (a*A)=width A by MATRIX_3:def 5;
hence thesis by FINSEQ_3:29;
end;
theorem Th19:
for K being Ring, a being Element of K, M being Matrix of K st
1<=i & i<=width M holds Col(a*M,i)=a*Col(M,i)
proof
let K be Ring,a be Element of K, M be Matrix of K;
assume
A1: 1<=i & i<=width M;
A2: Seg len (a*M)=dom (a*M) by FINSEQ_1:def 3;
A3: len (a*M)=len M by MATRIX_3:def 5;
then
A4: dom M=dom (a*M) by FINSEQ_3:29;
A5: len (a*Col(M,i))=len (Col(M,i)) & len (Col(M,i))=len M by Th16,
MATRIX_0:def 8;
then
A6: dom (a*Col(M,i))=Seg len (a*M) by A3,FINSEQ_1:def 3;
for j st j in dom (a*M) holds (a*Col(M,i)).j = (a*M)*(j,i)
proof
let j;
assume
A7: j in dom (a*M);
i in Seg width M by A1,FINSEQ_1:1;
then [j,i] in Indices M by A4,A7,ZFMISC_1:87;
then
A8: (a*M)*(j,i)=a*(M*(j,i)) by MATRIX_3:def 5;
(Col(M,i)).j = M*(j,i) by A4,A7,MATRIX_0:def 8;
hence thesis by A6,A2,A7,A8,FVSUM_1:50;
end;
hence thesis by A5,A3,MATRIX_0:def 8;
end;
theorem
for K being non empty multMagma,
a being Element of K, M being (Matrix of K),
i being Nat st 1<=i & i<=len M holds
Line(a*M,i)=a*Line(M,i)
proof
let K be non empty multMagma, a be Element of K, M be Matrix of K;
let i be Nat;
assume
A1: 1<=i & i<=len M;
A2: width (a*M)=width M by MATRIX_3:def 5;
A3: Seg width M=Seg width (a*M) by MATRIX_3:def 5;
A4: len (a*Line(M,i))=len (Line(M,i)) & len (Line(M,i))=width M by Th16,
MATRIX_0:def 7;
then
A5: dom (a*Line(M,i))=Seg width (a*M) by A2,FINSEQ_1:def 3;
for j st j in Seg width (a*M) holds (a*Line(M,i)).j = (a*M)*(i,j)
proof
let j;
assume
A6: j in Seg width (a*M);
i in dom M by A1,FINSEQ_3:25;
then [i,j] in Indices M by A3,A6,ZFMISC_1:87;
then
A7: (a*M)*(i,j)=a*(M*(i,j)) by MATRIX_3:def 5;
(Line(M,i)).j = M*(i,j) by A3,A6,MATRIX_0:def 7;
hence thesis by A5,A6,A7,FVSUM_1:50;
end;
hence thesis by A4,A2,MATRIX_0:def 7;
end;
theorem
for K being Field, A,B being Matrix of K st width A=len B holds ex C
being Matrix of K st len C=len A & width C=width B & for i,j st [i,j] in
Indices C holds C*(i,j)=Line(A,i) "*" Col(B,j)
proof
let K be Field, A,B be Matrix of K;
assume
A1: width A=len B;
deffunc F(Nat,Nat) = Line(A,$1) "*" Col(B,$2);
consider M being Matrix of len A,width B,(the carrier of K) such that
A2: for i,j st [i,j] in Indices M holds M*(i,j) = F(i,j) from MATRIX_0:
sch 1;
per cases;
suppose
len A > 0;
then len M=len A & width M= width B by MATRIX_0:23;
hence thesis by A2;
end;
suppose
A3: len A=0;
then
A4: len M=0 by MATRIX_0:25;
len B=0 by A1,A3,MATRIX_0:def 3;
then width B=0 by MATRIX_0:def 3;
then width M= width B by A4,MATRIX_0:def 3;
hence thesis by A2,A3,A4;
end;
end;
theorem Th22:
for K being Field,a being Element of K,A,B being Matrix of K st
width A=len B holds A*(a*B)=a*(A*B)
proof
let K be Field,a be Element of K,A,B be Matrix of K;
set C=a*B;
set D=a*(A*B);
A1: len D=len (A*B) by MATRIX_3:def 5;
assume
A2: width A=len B;
then width (A*B)=width B by MATRIX_3:def 4;
then
A3: width D=width B by MATRIX_3:def 5
.=width C by MATRIX_3:def 5;
A4: width B=width (a*B) by MATRIX_3:def 5;
A5: for i,j st [i,j] in Indices D holds D*(i,j)=Line(A,i) "*" Col(C,j)
proof
let i,j;
reconsider xo=Col(B,j) as Element of (width A)-tuples_on the carrier of K
by A2;
assume
A6: [i,j] in Indices (a*(A*B));
then j in Seg width B by A4,A3,ZFMISC_1:87;
then
A7: 1<=j & j<=width B by FINSEQ_1:1;
dom (A*B)=dom (a*(A*B)) by A1,FINSEQ_3:29;
then
A8: [i,j] in Indices (A*B) by A6,MATRIX_3:def 5;
then (a*(A*B))*(i,j)=a*((A*B)*(i,j)) by MATRIX_3:def 5;
then (a*(A*B))*(i,j)=a*((Line(A,i)) "*" (Col(B,j))) by A2,A8,MATRIX_3:def 4
.=a*(Sum(mlt(Line(A,i),Col(B,j)))) by FVSUM_1:def 9
.=Sum(a*mlt(Line(A,i),Col(B,j))) by FVSUM_1:73
.=Sum(mlt(Line(A,i),a*xo)) by FVSUM_1:69
.=Sum(mlt(Line(A,i),Col(a*B,j))) by A7,Th19;
hence thesis by FVSUM_1:def 9;
end;
len C=len B & len (A*B)=len A by A2,MATRIX_3:def 4,def 5;
hence thesis by A2,A1,A3,A5,MATRIX_3:def 4;
end;
definition
let A be Matrix of REAL;
func MXR2MXF A -> Matrix of F_Real equals
A;
coherence;
end;
definition
let A be Matrix of F_Real;
func MXF2MXR A -> Matrix of REAL equals
A;
coherence;
end;
theorem
for D1,D2 being set, A being (Matrix of D1), B being Matrix of D2 st A
=B holds for i,j st [i,j] in Indices A holds A*(i,j)=B*(i,j)
proof
let D1,D2 be set, A be (Matrix of D1), B be Matrix of D2;
assume
A1: A=B;
let i,j;
assume
A2: [i,j] in Indices A;
then
A3: ex p being FinSequence of D1 st p= A.i & A*(i,j)=p.j by MATRIX_0:def 5;
ex q being FinSequence of D2 st q= B.i & B*(i,j)=q.j by A1,A2,MATRIX_0:def 5;
hence thesis by A1,A3;
end;
theorem
for K being Field, A,B being Matrix of K holds Indices (A+B)=Indices A
proof
let K be Field,A,B be Matrix of K;
len (A+B)=len A & width (A+B)=width A by MATRIX_1:def 6;
hence thesis by MATRIX_4:55;
end;
definition
let A,B be Matrix of REAL;
func A+B -> Matrix of REAL equals
MXF2MXR ((MXR2MXF A)+(MXR2MXF B));
coherence;
end;
theorem Th25:
for A,B being Matrix of REAL holds len (A+B) = len A & width (A+
B)=width A & for i,j holds [i,j] in Indices A implies (A+B)*(i,j) = A*(i,j) + B
*(i,j)
proof
let A,B be Matrix of REAL;
thus len (A+B) = len A & width (A+B)=width A by MATRIX_1:def 6;
let i,j;
assume [i,j] in Indices A;
then (A+B)*(i,j)=(MXR2MXF A)*(i,j) + (MXR2MXF B)*(i,j) by MATRIX_1:def 6;
hence thesis;
end;
theorem Th26:
for A,B,C being Matrix of REAL st len C = len A & width C =
width A & for i,j st [i,j] in Indices A holds C*(i,j) = A*(i,j) + B*(i,j) holds
C=A+B
proof
let A,B,C be Matrix of REAL;
assume that
A1: len C =len A & width C=width A and
A2: for i,j holds [i,j] in Indices A implies C*(i,j) = A*(i,j) + B*(i,j);
set B2=MXR2MXF B;
set A2=MXR2MXF A;
set D=MXR2MXF C;
for i,j st [i,j] in Indices A2 holds D*(i,j) = A2*(i,j) + B2*(i,j) by A2;
hence thesis by A1,MATRIX_1:def 6;
end;
definition
let A be Matrix of REAL;
func -A -> Matrix of REAL equals
MXF2MXR (-(MXR2MXF A));
coherence;
end;
definition
let A,B be Matrix of REAL;
func A - B -> Matrix of REAL equals
MXF2MXR ((MXR2MXF A)-(MXR2MXF B));
coherence;
func A*B -> Matrix of REAL equals
MXF2MXR ((MXR2MXF A)*(MXR2MXF B));
coherence;
end;
definition
let a be Real, A be Matrix of REAL;
func a * A -> Matrix of REAL means
:Def7:
for ea being Element of F_Real st ea=a holds it=MXF2MXR (ea*(MXR2MXF A));
existence
proof
reconsider aa=a as Element of F_Real by XREAL_0:def 1;
set C=MXF2MXR (aa*(MXR2MXF A));
for ea being Element of F_Real st ea=a holds C=MXF2MXR (ea*(MXR2MXF A) );
hence thesis;
end;
uniqueness
proof
reconsider aa=a as Element of F_Real by XREAL_0:def 1;
let C1,C2 be Matrix of REAL;
assume that
A1: for ea being Element of F_Real st ea=a holds C1=MXF2MXR (ea*(
MXR2MXF A) ) and
A2: for ea being Element of F_Real st ea=a holds C2=MXF2MXR (ea*( MXR2MXF A));
C2=MXF2MXR (aa*(MXR2MXF A)) by A2;
hence thesis by A1;
end;
end;
theorem Th27:
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;
thus len (a*A)=len(MXF2MXR (ea*(MXR2MXF A))) by Def7
.=len A by MATRIX_3:def 5;
thus width (a*A)=width(MXF2MXR (ea*(MXR2MXF A))) by Def7
.=width A by MATRIX_3:def 5;
end;
theorem Th28:
for a being Real, A being Matrix of REAL
holds Indices (a*A) = Indices A
proof
let a be Real, A be Matrix of REAL;
len A = len (a*A) & width (a*A)=width A by Th27;
hence thesis by MATRIX_4:55;
end;
theorem Th29:
for a being Real, A being (Matrix of REAL), i2,j2 being Nat st
[i2,j2] in Indices A holds (a*A)*(i2,j2)=a*(A*(i2,j2))
proof
let a be Real,A be Matrix of REAL;
let i2,j2 be Nat;
reconsider ea=a as Element of F_Real by XREAL_0:def 1;
assume [i2,j2] in Indices A;
then (MXF2MXR (ea*(MXR2MXF A)))*(i2,j2) = ea*((MXR2MXF A)*(i2,j2))
by MATRIX_3:def 5
.=a*(A*(i2,j2));
hence thesis by Def7;
end;
theorem Th30:
for a being Real, A being Matrix of REAL st width A>0
holds (a*A )@=a*(A@)
proof
let a be Real, A be Matrix of REAL;
assume width A>0;
then
A1: len (A@)= width A by MATRIX_0:54;
A2: for i,j holds [i,j] in Indices (a*(A@)) iff [j,i] in Indices (a*A)
proof
let i,j;
Indices (a*(A@))=Indices (A@) & Indices (a*A)=Indices A by Th28;
hence thesis by MATRIX_0:def 6;
end;
A3: for i,j st [j,i] in Indices (a*A) holds (a*(A@))*(i,j) = (a*A)*(j,i)
proof
let i,j;
assume [j,i] in Indices (a*A);
then
A4: [j,i] in Indices A by Th28;
then [i,j] in Indices (A@) by MATRIX_0:def 6;
then (a*(A@))*(i,j) = a*((A@)*(i,j)) by Th29;
then (a*(A@))*(i,j) = a*(A*(j,i)) by A4,MATRIX_0:def 6
.=(a*A)*(j,i) by A4,Th29;
hence thesis;
end;
len (a*(A@)) = len (A@) & width A= width (a*A) by Th27;
hence thesis by A1,A2,A3,MATRIX_0:def 6;
end;
theorem
for a being Real,i being Nat,A being Matrix of REAL
st len A>0 & i in
dom A holds (ex p being FinSequence of REAL st p=A.i) & for q being FinSequence
of REAL st q=A.i holds (a*A).i=a*q
proof
let a be Real,i be Nat,A be Matrix of REAL;
assume that
A1: len A>0 and
A2: i in dom A;
consider n3 being Nat such that
A3: for x being object st x in rng A ex s2 being FinSequence st s2=x & len
s2 = n3 by MATRIX_0:def 1;
A.i in rng A by A2,FUNCT_1:def 3;
then
A4: ex qq0 being FinSequence st qq0=A.i & len qq0=n3 by A3;
len (a*A)=len A by Th27;
then consider s being FinSequence such that
A5: s in rng (a*A) and
A6: len s = width (a*A) by A1,MATRIX_0:def 3;
A7: width (a*A)=width A by Th27;
consider s3 being FinSequence such that
A8: s3 in rng A and
A9: len s3 = width A by A1,MATRIX_0:def 3;
consider n2 being Nat such that
A10: for x being object st x in rng (a*A) ex s2 being FinSequence st s2=x &
len s2 = n2 by MATRIX_0:def 1;
len (a*A)=len A by Th27;
then
A11: dom (a*A) = dom A by FINSEQ_3:29;
then (a*A).i in rng (a*A) by A2,FUNCT_1:def 3;
then consider qq being FinSequence such that
A12: qq=(a*A).i and
A13: len qq=n2 by A10;
consider n being Nat such that
A14: for x being object st x in rng A ex p being FinSequence of REAL st x =
p & len p = n by MATRIX_0:9;
A.i in rng A by A2,FUNCT_1:def 3;
then ex p2 being FinSequence of REAL st A.i = p2 & len p2 = n by A14;
hence ex p being FinSequence of REAL st p=A.i;
let q be FinSequence of REAL;
assume
A15: q=A.i;
A16: ex s4 being FinSequence st s4=s3 & len s4 = n3 by A8,A3;
then
A17: len (a*q)=width A by A15,A9,A4,RVSUM_1:117;
A18: for j being Nat st 1<=j & j<=len (a*q) holds qq.j=(a*q).j
proof
let j be Nat;
assume 1<=j & j<=len (a*q);
then
A19: j in Seg width A by A17,FINSEQ_1:1;
then
A20: [i,j] in Indices A by A2,ZFMISC_1:87;
reconsider j as Element of NAT by ORDINAL1:def 12;
[i,j] in Indices (a*A) by A2,A7,A11,A19,ZFMISC_1:87;
then
A21: ex p being FinSequence of REAL st p= (a*A).i & (a*A)*(i,j ) =p.j by
MATRIX_0:def 5;
ex p2 being FinSequence of REAL st p2= A.i & A*(i,j) =p2. j by A20,
MATRIX_0:def 5;
then qq.j=a*(q.j) by A15,A12,A20,A21,Th29;
hence thesis by RVSUM_1:44;
end;
ex s2 being FinSequence st s2=s & len s2 = n2 by A5,A10;
then width A=len qq by A6,A13,Th27;
hence thesis by A15,A9,A16,A12,A4,A18,FINSEQ_1:14,RVSUM_1:117;
end;
theorem
for A being Matrix of REAL holds 1*A=A
proof
let A be Matrix of REAL;
1*A = MXF2MXR ((1_F_Real)*(MXR2MXF A)) by Def7;
hence thesis by MATRIX_5:9;
end;
theorem
for A being Matrix of REAL holds A+A=2*A
proof
set e2=(1_F_Real) + (1_F_Real);
let A be Matrix of REAL;
A1: (1_F_Real)*(MXR2MXF A)= MXR2MXF A by MATRIX_5:9;
2*A = MXF2MXR (e2*(MXR2MXF A)) by Def7
.= MXF2MXR ((MXR2MXF A)+(MXR2MXF A)) by A1,MATRIX_5:12;
hence thesis;
end;
theorem
for A being Matrix of REAL holds A+A+A=3*A
proof
reconsider e3=(1_F_Real) + (1_F_Real) + (1_F_Real) as Element of F_Real;
let A be Matrix of REAL;
A1: len A =len MXR2MXF A & width A=width MXR2MXF A;
3*A= MXF2MXR (e3*(MXR2MXF A)) by Def7
.=MXF2MXR ((1_F_Real)*(MXR2MXF A) + ((1_F_Real)+ (1_F_Real))*(MXR2MXF A)
) by MATRIX_5:12
.=MXF2MXR ((MXR2MXF A) + ((1_F_Real)+ (1_F_Real))*(MXR2MXF A)) by
MATRIX_5:9
.=MXF2MXR (MXR2MXF A + ((1_F_Real)*(MXR2MXF A)+ (1_F_Real)*(MXR2MXF A)))
by MATRIX_5:12
.=MXF2MXR (MXR2MXF A + (MXR2MXF A + (1_F_Real)*(MXR2MXF A))) by MATRIX_5:9
.=MXF2MXR (MXR2MXF A+(MXR2MXF A+MXR2MXF A)) by MATRIX_5:9
.=MXF2MXR (MXR2MXF A+MXR2MXF A+MXR2MXF A) by A1,MATRIX_3:3;
hence thesis;
end;
definition
let n,m be Nat;
func 0_Rmatrix(n,m) -> Matrix of REAL equals
MXF2MXR (0.(F_Real,n,m));
coherence;
end;
theorem
for A,B being Matrix of REAL holds A--B=A+B
proof
let A,B be Matrix of REAL;
A+B = MXF2MXR ((MXR2MXF A)+(MXR2MXF --B)) by MATRIX_4:1;
hence thesis by MATRIX_1:def 7;
end;
theorem Th36:
for n,m being Nat,A being Matrix of REAL st len A=n & width A=m
& n>0 holds A+ 0_Rmatrix(n,m)=A & 0_Rmatrix(n,m)+A=A
proof
let n,m be Nat,A be Matrix of REAL;
assume that
A1: len A=n & width A=m and
A2: n>0;
reconsider D=MXR2MXF A as Matrix of n,m,F_Real by A1,A2,MATRIX_0:20;
len (0.(F_Real,n,m))=n & width (0.(F_Real,n,m))=m by A2,MATRIX_0:23;
then
A3: 0_Rmatrix(n,m)+A=MXF2MXR (D+0.(F_Real,n,m)) by A1,MATRIX_3:2
.=A by MATRIX_3:4;
MXR2MXF A is Matrix of n,m,F_Real by A1,A2,MATRIX_0:20;
hence thesis by A3,MATRIX_3:4;
end;
theorem
for A,B being Matrix of REAL st len A=len B & width A=width B & A = A
+ B holds B = 0_Rmatrix(len A,width A)
proof
let A,B be Matrix of REAL;
assume that
A1: len A=len B & width A=width B and
A2: A = A + B;
0_Rmatrix(len A,width A)=A+B+(-A) by A2,MATRIX_4:2
.=MXF2MXR ((MXR2MXF B)+(MXR2MXF A)+ -(MXR2MXF A)) by A1,MATRIX_3:2
.=MXF2MXR ((MXR2MXF B)+(MXR2MXF A) -(MXR2MXF A)) by MATRIX_1:def 7
.=B by A1,MATRIX_4:21;
hence thesis;
end;
theorem
for A,B being Matrix of REAL st len A=len B & width A=width B & A+B=
0_Rmatrix(len A,width A) holds B=-A
proof
let A,B be Matrix of REAL;
assume that
A1: len A=len B & width A=width B and
A2: A + B = 0_Rmatrix(len A,width A);
A3: len -MXR2MXF B=len MXR2MXF B & width -MXR2MXF B=width MXR2MXF B by
MATRIX_1:def 4;
MXR2MXF(0_Rmatrix(len A,width A)) = (MXR2MXF A)+--(MXR2MXF B) by A2,
MATRIX_4:1
.= (MXR2MXF A)-(-(MXR2MXF B)) by MATRIX_1:def 7;
then MXR2MXF A = -MXR2MXF B by A1,A3,MATRIX_4:7;
hence thesis by MATRIX_4:1;
end;
theorem
for A,B being Matrix of REAL st len A=len B & width A=width B & B - A
= B holds A=0_Rmatrix(len A,width A)
proof
let A,B be Matrix of REAL;
assume that
A1: len A=len B & width A=width B and
A2: B - A = B;
MXR2MXF B + (MXR2MXF A) = MXR2MXF B by A1,A2,MATRIX_4:22;
hence thesis by A1,MATRIX_4:6;
end;
theorem Th40:
for a being Real,A,B being Matrix of REAL st width A=len B holds
A*(a*B)=a*(A*B)
proof
let a be Real,A,B be Matrix of REAL;
assume
A1: width A=len B;
reconsider ea=a as Element of F_Real by XREAL_0:def 1;
thus A*(a*B)=MXF2MXR((MXR2MXF A)*(MXR2MXF(MXF2MXR(ea*(MXR2MXF B))))) by Def7
.=MXF2MXR(ea*(MXR2MXF (MXF2MXR((MXR2MXF A)*(MXR2MXF B))))) by A1,Th22
.=a*(A*B) by Def7;
end;
theorem
for a being Real,A,B being Matrix of REAL
st width A=len B & len A>0 &
len B>0 & width B>0 holds (a*A)*B=a*(A*B)
proof
let a be Real,A,B be Matrix of REAL;
assume that
A1: width A=len B and
A2: len A>0 and
A3: len B>0 and
A4: width B>0;
len (A@)=width A & width (B@)=len B by A1,A3,A4,MATRIX_0:54;
then (B@)*(a*(A@))=a*((B@)*(A@)) by A1,Th40;
then
A5: (B@)*(a*(A@))=a*((A*B)@) by A1,A4,MATRIX_3:22;
A6: width (a*(A*B))=width (A*B) by Th27
.=width B by A1,MATRIX_3:def 4;
A7: len (a*(A*B))=len (A*B) by Th27
.=len A by A1,MATRIX_3:def 4;
A8: len (a*A)=len A by Th27;
A9: width (a*A)=width A by Th27;
width (A*B)=width B by A1,MATRIX_3:def 4;
then (B@)*(a*(A@))=(a*(A*B))@ by A4,A5,Th30;
then (B@)*((a*A)@)=(a*(A*B))@ by A1,A3,Th30;
then
A10: ((a*A)*B)@=(a*(A*B))@ by A1,A4,A9,MATRIX_3:22;
len ((a*A)*B)=len (a*A) & width ((a*A)*B)=width B by A1,A9,MATRIX_3:def 4;
then (a*A)*B=(a*(A*B))@@ by A2,A4,A8,A10,MATRIX_0:57;
hence thesis by A2,A4,A7,A6,MATRIX_0:57;
end;
theorem
for M being Matrix of REAL holds M + 0_Rmatrix(len M,width M) = M
proof
let M be Matrix of REAL;
A1: len M=len MXR2MXF M & width M=width MXR2MXF M;
M + 0_Rmatrix(len M,width M) = M +(-0_Rmatrix(len M,width M)) by MATRIX_4:9
.= M +(-(M-M)) by MATRIX_4:3
.= MXF2MXR ((MXR2MXF M)-(MXR2MXF M-MXR2MXF M)) by MATRIX_1:def 7
.= M by A1,MATRIX_4:11;
hence thesis;
end;
theorem
for a being Real, A,B being Matrix of REAL st len A=len B &
width A=width B holds a*(A + B) = a*A + a*B
proof
let a be Real, A,B be Matrix of REAL;
assume
A1: len A=len B & width A=width B;
reconsider ea=a as Element of F_Real by XREAL_0:def 1;
A2: a*A + a*B = MXF2MXR ((MXR2MXF (MXF2MXR (ea*(MXR2MXF A)))+(MXR2MXF (a*B))
)) by Def7
.= MXF2MXR (((ea*(MXR2MXF A))+(MXR2MXF (MXF2MXR (ea*(MXR2MXF B)))))) by
Def7
.= MXF2MXR ((ea*(MXR2MXF A)+(ea*(MXR2MXF B))));
a*(A + B) = MXF2MXR (ea*(MXR2MXF (A+B))) by Def7
.= MXF2MXR (ea*(MXR2MXF A)+ea*(MXR2MXF B)) by A1,MATRIX_5:20;
hence thesis by A2;
end;
theorem
for A being Matrix of REAL st len A>0 holds 0 * A = 0_Rmatrix (len A,
width A)
proof
let A be Matrix of REAL;
assume
A1: len A>0;
0 * A = MXF2MXR ((0.F_Real)*(MXR2MXF A)) by Def7
.= 0_Rmatrix(len A,width A) by A1,MATRIX_5:24;
hence thesis;
end;
definition
let x be FinSequence of REAL;
assume
A1: len x > 0;
func ColVec2Mx x -> Matrix of REAL means
:Def9:
len it=len x & width it=1 & for j st j in dom x holds it.j = <*x.j*>;
existence
proof
reconsider n=len x as Element of NAT;
deffunc F(Nat) = <*x.$1*>;
consider C being FinSequence such that
A2: len C=n & for j be Nat st j in dom C holds C.j = F(j) from
FINSEQ_1:sch 2;
for y being object st y in rng C ex p being FinSequence of REAL st y = p
& len p = 1
proof
let y be object;
assume y in rng C;
then consider z be object such that
A3: z in dom C and
A4: y=C.z by FUNCT_1:def 3;
reconsider z as Element of NAT by A3;
reconsider xz = x.z as Element of REAL by XREAL_0:def 1;
len <*xz*>=1 by FINSEQ_1:39;
hence thesis by A2,A3,A4;
end;
then reconsider B=C as Matrix of REAL by MATRIX_0:9;
for p being FinSequence of REAL st p in rng B holds len p = 1
proof
let p be FinSequence of REAL;
assume p in rng B;
then consider i be Nat such that
A5: i in dom B & B.i =p by FINSEQ_2:10;
len <*x.i*>=1 by FINSEQ_1:39;
hence thesis by A2,A5;
end;
then reconsider A=B as Matrix of len B,1,REAL by MATRIX_0:def 2;
A6: Seg len x = dom x by FINSEQ_1:def 3;
dom C = Seg n & width A = 1 by A1,A2,FINSEQ_1:def 3,MATRIX_0:23;
hence thesis by A2,A6;
end;
uniqueness
proof
let A,B be Matrix of REAL;
assume that
A7: len A = len x and
width A = 1 and
A8: for k being Nat st k in dom x holds A.k =<*x.k*> and
A9: len B = len x and
width B = 1 and
A10: for k being Nat st k in dom x holds B.k =<*x.k*>;
A11: now
let k be Nat;
assume
A12: k in dom x;
hence A.k=<*x.k*> by A8
.=B.k by A10,A12;
end;
dom A = dom x & dom B = dom x by A7,A9,FINSEQ_3:29;
hence thesis by A11,FINSEQ_1:13;
end;
end;
theorem
for x being FinSequence of REAL,M being Matrix of REAL st len x>0
holds M=ColVec2Mx x iff Col(M,1)=x & width M=1
proof
let x be FinSequence of REAL,M be Matrix of REAL;
consider n being Nat such that
A1: for x being object st x in rng M ex s2 being FinSequence st s2=x & len
s2 = n by MATRIX_0:def 1;
assume
A2: len x>0;
thus M=ColVec2Mx x implies Col(M,1)=x & width M=1
proof
assume
A3: M=ColVec2Mx x;
then
A4: width M=1 by A2,Def9;
A5: len M=len x by A2,A3,Def9;
then
A6: dom M = dom x by FINSEQ_3:29;
for j st j in dom M holds x.j = M*(j,1)
proof
let j;
reconsider xj = x.j as Element of REAL by XREAL_0:def 1;
assume
A7: j in dom M;
then reconsider j as Element of NAT;
A8: M.j=<*xj*> by A2,A3,A6,A7,Def9;
then reconsider q=M.j as FinSequence of REAL;
A9: q.1=xj by A8;
1 in Seg width M by A4,FINSEQ_1:1;
then [j,1] in Indices M by A7,ZFMISC_1:87;
hence thesis by A9,MATRIX_0:def 5;
end;
hence thesis by A2,A3,A5,Def9,MATRIX_0:def 8;
end;
assume that
A10: Col(M,1)=x and
A11: width M=1;
A12: len x = len M by A10,MATRIX_0:def 8;
then consider s being FinSequence such that
A13: s in rng M and
A14: len s = 1 by A2,A11,MATRIX_0:def 3;
A15: dom x = dom M by A12,FINSEQ_3:29;
A16: ex s2 being FinSequence st s2=s & len s2 = n by A13,A1;
for j st j in dom x holds M.j =<*x.j*>
proof
let j;
assume
A17: j in dom x;
then M.j in rng M by A15,FUNCT_1:def 3;
then
A18: ex s3 being FinSequence st s3=M.j & len s3 = 1 by A14,A1,A16;
1 in Seg width M by A11,FINSEQ_1:1;
then [j,1] in Indices M by A15,A17,ZFMISC_1:87;
then
A19: ex p being FinSequence of REAL st p= M.j & M*(j,1) =p.1 by MATRIX_0:def 5;
x.j=M*(j,1) by A10,A15,A17,MATRIX_0:def 8;
hence thesis by A19,A18,FINSEQ_1:40;
end;
hence thesis by A2,A11,A12,Def9;
end;
theorem Th46:
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,Def9;
A4: Seg width ColVec2Mx x1=Seg 1 by A2,Def9;
A5: dom x1=dom x2 by A1,FINSEQ_3:29;
A6: len ColVec2Mx x1=len x1 by A2,Def9;
then
A7: dom ColVec2Mx x1=dom x1 by FINSEQ_3:29;
len ColVec2Mx x2=len x2 & width ColVec2Mx x2=1 by A1,A2,Def9;
then
A8: Indices ColVec2Mx x2=Indices ColVec2Mx x1 by A1,A6,A3,MATRIX_4:55;
A9: len (x1+x2)=len x1 by A1,RVSUM_1:115;
then
A10: dom (x1+x2)=dom x1 by FINSEQ_3:29;
A11: len ColVec2Mx (x1+x2)=len (x1+x2) & width ColVec2Mx (x1+x2)=1 by A2,A9
,Def9;
then
A12: Indices ColVec2Mx (x1+x2)=Indices ColVec2Mx x1 by A1,A6,A3,MATRIX_4:55
,RVSUM_1:115;
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;
thus [i,j] in Indices ColVec2Mx x1 implies (ColVec2Mx (x1+x2))*(i,j) = (
ColVec2Mx x1)*(i,j) + (ColVec2Mx x2)*(i,j)
proof
assume
A13: [i,j] in Indices ColVec2Mx x1;
then consider q1 being FinSequence of REAL such that
A14: q1 = (ColVec2Mx x1).i and
A15: (ColVec2Mx x1)*(i,j)=q1.j by MATRIX_0:def 5;
j in Seg 1 by A4,A13,ZFMISC_1:87;
then 1<=j & j<=1 by FINSEQ_1:1;
then
A16: j=1 by XXREAL_0:1;
A17: i in dom x1 by A7,A13,ZFMISC_1:87;
then (ColVec2Mx x1).i=<* x1.i *> by A2,Def9;
then
A18: q1.j=x1.i by A16,A14;
consider p being FinSequence of REAL such that
A19: p = (ColVec2Mx (x1+x2)).i and
A20: (ColVec2Mx (x1+x2))*(i,j) = p.j by A12,A13,MATRIX_0:def 5;
consider q2 being FinSequence of REAL such that
A21: q2 = (ColVec2Mx x2).i and
A22: (ColVec2Mx x2)*(i,j)=q2.j by A8,A13,MATRIX_0:def 5;
(ColVec2Mx x2).i=<* x2.i *> by A1,A2,A5,A17,Def9;
then
A23: q2.j=x2.i by A16,A21;
(ColVec2Mx (x1+x2)).i=<* (x1+x2).i *> by A2,A9,A10,A17,Def9;
then p.j=(x1+x2).i by A16,A19;
hence thesis by A10,A17,A20,A15,A18,A22,A23,VALUED_1:def 1;
end;
end;
hence thesis by A1,A6,A11,A3,Th26,RVSUM_1:115;
end;
theorem Th47:
for a being Real,x being FinSequence of REAL st len x>0 holds
ColVec2Mx (a*x)=a*ColVec2Mx x
proof
let a be Real,x be FinSequence of REAL;
assume
A1: len x>0;
A2: len (a*ColVec2Mx x)=len ColVec2Mx x by Th27
.=len x by A1,Def9;
A3: len (a*x)=len x by RVSUM_1:117;
then
A4: dom (a*x)=dom x by FINSEQ_3:29;
A5: for j st j in dom (a*x) holds (a*ColVec2Mx x).j =<*(a*x).j*>
proof
len ColVec2Mx x=len x by A1,Def9;
then
A6: dom ColVec2Mx x=dom x by FINSEQ_3:29;
let j;
consider n being Nat such that
A7: for x2 being object st x2 in rng (a*ColVec2Mx x) ex s2 being
FinSequence st s2=x2 & len s2 = n by MATRIX_0:def 1;
assume
A8: j in dom (a*x);
then
A9: (ColVec2Mx x).j=<*x.j*> by A1,A4,Def9;
A10: j in dom (a*ColVec2Mx x) by A2,A3,A8,FINSEQ_3:29;
then (a*ColVec2Mx x).j in rng (a*ColVec2Mx x) by FUNCT_1:def 3;
then reconsider q=(a*ColVec2Mx x).j as FinSequence of REAL by
FINSEQ_1:def 11;
q in rng (a*ColVec2Mx x) by A10,FUNCT_1:def 3;
then
A11: ex s2 being FinSequence st s2=q & len s2 = n by A7;
consider s being FinSequence such that
A12: s in rng (a*ColVec2Mx x) and
A13: len s = width (a*ColVec2Mx x) by A1,A2,MATRIX_0:def 3;
ex s3 being FinSequence st s3=s & len s3 = n by A12,A7;
then
A14: len q = width ColVec2Mx x by A13,A11,Th27
.= 1 by A1,Def9
.= len (<*(a*x).j*>) by FINSEQ_1:40;
width ColVec2Mx x=1 by A1,Def9;
then
A15: 1 in Seg width MXR2MXF ColVec2Mx x by FINSEQ_1:1;
j in dom x by A3,A8,FINSEQ_3:29;
then
A16: [j,1] in Indices MXR2MXF ColVec2Mx x by A6,A15,ZFMISC_1:87;
then
A17: ex p3 being FinSequence of REAL st p3 = (ColVec2Mx x).j & (ColVec2Mx x
)*(j,1) = p3.1 by MATRIX_0:def 5;
[j,1] in Indices (a*ColVec2Mx x) by A16,Th28;
then
A18: ex p being FinSequence of REAL st p = (a*ColVec2Mx x).j & (a*ColVec2Mx
x)*(j,1) = p.1 by MATRIX_0:def 5;
reconsider j as Element of NAT by ORDINAL1:def 12;
A19: q.1= a*((ColVec2Mx x)*(j,1)) by A16,A18,Th29
.= a*(x.j) by A17,A9
.= (a*x).j by RVSUM_1:44
.= (<*(a*x).j*>).1;
for i be Nat st 1<=i & i<=len (<*(a*x).j*>) holds q.i= (<*(a*x).j*>). i
proof
let i be Nat;
A20: len (<*(a*x).j*>)=1 by FINSEQ_1:40;
assume 1<=i & i<=len (<*(a*x).j*>);
then i=1 by A20,XXREAL_0:1;
hence thesis by A19;
end;
hence thesis by A14,FINSEQ_1:14;
end;
width (a*ColVec2Mx x)=width ColVec2Mx x by Th27
.=1 by A1,Def9;
hence thesis by A1,A2,A3,A5,Def9;
end;
definition
let x be FinSequence of REAL;
func LineVec2Mx x -> Matrix of REAL means
:Def10:
width it=len x & len it=1 & for j st j in dom x holds it*(1,j) =x.j;
existence
proof
set B=<* x *>;
A1: rng B={x} by FINSEQ_1:39;
for y being object st y in rng B ex p being FinSequence of REAL st y = p
& len p = len x
proof
let y be object;
assume y in rng B;
then y=x by A1,TARSKI:def 1;
hence thesis;
end;
then reconsider C=B as Matrix of REAL by MATRIX_0:9;
take C;
A2: len B=1 by FINSEQ_1:39;
then dom C=Seg 1 by FINSEQ_1:def 3;
then
A3: 1 in dom C by FINSEQ_1:1;
for p being FinSequence of REAL st p in rng C holds len p = len x by A1,
TARSKI:def 1;
then len B=1 & C is Matrix of 1,len x,REAL by A2,MATRIX_0:def 2;
hence
A4: width C=len x by MATRIX_0:20;
thus len C=1 by FINSEQ_1:40;
let j be Nat;
A5: x.j in REAL by XREAL_0:def 1;
assume j in dom x;
then j in Seg len x by FINSEQ_1:def 3;
then B.1=x & [1,j] in Indices C by A4,A3,ZFMISC_1:def 2;
hence thesis by A5,MATRIX_0:def 5;
end;
uniqueness
proof
let A,B be Matrix of REAL;
assume that
A6: width A=len x and
A7: len A = 1 and
A8: for k being Nat st k in dom x holds A*(1,k) = x.k and
A9: width B=len x & len B = 1 and
A10: for k being Nat st k in dom x holds B*(1,k) = x.k;
A11: dom A=Seg 1 by A7,FINSEQ_1:def 3;
for i,j st [i,j] in Indices A holds A*(i,j) = B*(i,j)
proof
let i,j;
assume
A12: [i,j] in Indices A;
then i in Seg 1 by A11,ZFMISC_1:87;
then 1<=i & i<=1 by FINSEQ_1:1;
then
A13: i=1 by XXREAL_0:1;
j in Seg len x by A6,A12,ZFMISC_1:87;
then
A14: j in dom x by FINSEQ_1:def 3;
then A*(i,j)=x.j by A8,A13;
hence thesis by A10,A14,A13;
end;
hence thesis by A6,A7,A9,MATRIX_0:21;
end;
end;
theorem
for x being FinSequence of REAL, M being Matrix of REAL holds M=
LineVec2Mx x iff Line(M,1)=x & len M=1
proof
let x be FinSequence of REAL, M be Matrix of REAL;
thus M=LineVec2Mx x implies Line(M,1)=x & len M=1
proof
assume
A1: M=LineVec2Mx x;
then
A2: for j st j in dom x holds M*(1,j) = x.j by Def10;
A3: width M=len x by A1,Def10;
then dom x = Seg width M by FINSEQ_1:def 3;
hence thesis by A1,A3,A2,Def10,MATRIX_0:def 7;
end;
assume that
A4: Line(M,1)=x and
A5: len M=1;
A6: for j st j in Seg width M holds x.j = M*(1,j) by A4,MATRIX_0:def 7;
A7: len x = width M by A4,MATRIX_0:def 7;
then Seg width M = dom x by FINSEQ_1:def 3;
hence thesis by A5,A7,A6,Def10;
end;
theorem Th49:
for x being FinSequence of REAL st len x>0 holds (LineVec2Mx x)@
= ColVec2Mx x & (ColVec2Mx x)@=LineVec2Mx x
proof
let x be FinSequence of REAL;
A1: dom LineVec2Mx x=Seg len LineVec2Mx x by FINSEQ_1:def 3;
A2: width LineVec2Mx x=len x by Def10;
assume
A3: len x>0;
then
A4: len ColVec2Mx x=len x by Def9;
A5: len LineVec2Mx x=1 by Def10;
A6: width ColVec2Mx x=1 by A3,Def9;
A7: dom ColVec2Mx x=Seg len ColVec2Mx x by FINSEQ_1:def 3;
A8: for i,j holds [i,j] in Indices ColVec2Mx x iff [j,i] in Indices
LineVec2Mx x
proof
let i,j;
[i,j] in Indices ColVec2Mx x iff i in dom ColVec2Mx x & j in Seg width
ColVec2Mx x by ZFMISC_1:87;
hence thesis by A2,A5,A4,A6,A7,A1,ZFMISC_1:87;
end;
A9: for i,j st [j,i] in Indices LineVec2Mx x holds (ColVec2Mx x)*(i,j) = (
LineVec2Mx x)*(j,i)
proof
let i,j;
assume
A10: [j,i] in Indices LineVec2Mx x;
then [i,j] in Indices ColVec2Mx x by A8;
then
A11: ex p being FinSequence of REAL st p = (ColVec2Mx x).i & (ColVec2Mx x)*
(i,j) =p.j by MATRIX_0:def 5;
j in Seg 1 by A5,A1,A10,ZFMISC_1:87;
then 1<=j & j<=1 by FINSEQ_1:1;
then
A12: j=1 by XXREAL_0:1;
i in Seg len x by A2,A10,ZFMISC_1:87;
then
A13: i in dom x by FINSEQ_1:def 3;
then (ColVec2Mx x).i=<*x.i*> by A3,Def9;
hence (ColVec2Mx x)*(i,j) = x.i by A12,A11
.= (LineVec2Mx x)*(j,i) by A12,A13,Def10;
end;
hence (LineVec2Mx x)@ = ColVec2Mx x by A2,A4,A8,MATRIX_0:def 6;
A14: for i,j st [j,i] in Indices ColVec2Mx x holds (LineVec2Mx x)*(i,j) = (
ColVec2Mx x)*(j,i)
proof
let i,j;
assume [j,i] in Indices ColVec2Mx x;
then [i,j] in Indices LineVec2Mx x by A8;
hence thesis by A9;
end;
for i,j holds [i,j] in Indices LineVec2Mx x iff [j,i] in Indices
ColVec2Mx x by A8;
hence thesis by A5,A6,A14,MATRIX_0:def 6;
end;
theorem Th50:
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;
assume
A1: len x1=len x2;
then
A2: dom x1 = dom x2 by FINSEQ_3:29;
len (x1+x2)=len x1 by A1,RVSUM_1:115;
then
A3: dom (x1+x2)=dom x1 by FINSEQ_3:29;
A4: width LineVec2Mx x1=len x1 & len LineVec2Mx x1=1 by Def10;
width LineVec2Mx x2=len x2 & len LineVec2Mx x2=1 by Def10;
then
A5: Indices LineVec2Mx x2=Indices LineVec2Mx x1 by A1,A4,MATRIX_4:55;
A6: Seg width LineVec2Mx x1=Seg len x1 by Def10
.= dom x1 by FINSEQ_1:def 3;
A7: dom LineVec2Mx x1=Seg len LineVec2Mx x1 by FINSEQ_1:def 3
.=Seg 1 by Def10;
A8: width LineVec2Mx (x1+x2)=len (x1+x2) & len LineVec2Mx (x1+x2)=1 by Def10;
then
A9: Indices LineVec2Mx (x1+x2)=Indices LineVec2Mx x1 by A1,A4,MATRIX_4:55
,RVSUM_1:115;
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
A10: [i,j] in Indices LineVec2Mx x1;
then consider q1 being FinSequence of REAL such that
q1 = (LineVec2Mx x1).i and
A11: (LineVec2Mx x1)*(i,j) = q1.j by MATRIX_0:def 5;
consider p being FinSequence of REAL such that
p = (LineVec2Mx (x1+x2)).i and
A12: (LineVec2Mx (x1+x2))*(i,j) = p.j by A9,A10,MATRIX_0:def 5;
consider q2 being FinSequence of REAL such that
q2 = (LineVec2Mx x2).i and
A13: (LineVec2Mx x2)*(i,j) =q2.j by A5,A10,MATRIX_0:def 5;
A14: j in dom x1 by A6,A10,ZFMISC_1:87;
i in Seg 1 by A7,A10,ZFMISC_1:87;
then 1<=i & i<=1 by FINSEQ_1:1;
then
A15: i=1 by XXREAL_0:1;
then
A16: q1.j=x1.j by A14,A11,Def10;
A17: q2.j=x2.j by A2,A14,A15,A13,Def10;
p.j=(x1+x2).j by A3,A14,A15,A12,Def10;
hence thesis by A3,A14,A12,A11,A16,A13,A17,VALUED_1:def 1;
end;
hence thesis by A1,A8,A4,Th26,RVSUM_1:115;
end;
theorem
for a being Real, x being FinSequence of REAL
holds LineVec2Mx (a*x)=a*LineVec2Mx x
proof
let a be Real, x be FinSequence of REAL;
A1: len (a*LineVec2Mx x)=len LineVec2Mx x by Th27
.=1 by Def10;
A2: len (a*x)=len x by RVSUM_1:117;
then
A3: dom (a*x)=dom x by FINSEQ_3:29;
A4: for j st j in dom (a*x) holds (a*LineVec2Mx x)*(1,j) = (a*x).j
proof
len LineVec2Mx x=1 by Def10;
then 1 in Seg len LineVec2Mx x by FINSEQ_1:1;
then
A5: 1 in dom LineVec2Mx x by FINSEQ_1:def 3;
1 in Seg len (a*LineVec2Mx x) by A1,FINSEQ_1:1;
then 1 in dom (a*LineVec2Mx x) by FINSEQ_1:def 3;
then (a*LineVec2Mx x).1 in rng (a*LineVec2Mx x) by FUNCT_1:def 3;
then reconsider q=(a*LineVec2Mx x).1 as FinSequence of REAL by
FINSEQ_1:def 11;
let j;
A6: width LineVec2Mx x=len x by Def10;
A7: Indices (a*LineVec2Mx x)=Indices LineVec2Mx x by Th28;
assume
A8: j in dom (a*x);
then j in Seg len x by A2,FINSEQ_1:def 3;
then
A9: [1,j] in Indices (a*LineVec2Mx x) by A6,A5,A7,ZFMISC_1:87;
then
A10: ex p being FinSequence of REAL st p = (a*LineVec2Mx x).1 & (a*
LineVec2Mx x)*(1,j) =p.j by MATRIX_0:def 5;
reconsider j as Element of NAT by ORDINAL1:def 12;
A11: q.j in REAL by XREAL_0:def 1;
q.j = a*((LineVec2Mx x)*(1,j)) by A7,A9,A10,Th29
.= a*(x.j) by A3,A8,Def10
.= (a*x).j by RVSUM_1:44;
hence thesis by A9,A11,MATRIX_0:def 5;
end;
width (a*LineVec2Mx x)=width LineVec2Mx x by Th27
.=len x by Def10;
hence thesis by A1,A2,A4,Def10;
end;
definition
let M be Matrix of REAL;
let x be FinSequence of REAL;
func M*x -> FinSequence of REAL equals
Col(M*(ColVec2Mx x),1);
coherence;
func x*M -> FinSequence of REAL equals
Line((LineVec2Mx x)*M,1);
coherence;
end;
theorem Th52:
for x being FinSequence of REAL, A being Matrix of REAL st len A
>0 & width A>0 & (len A=len x or width (A@)=len x) holds (A@)*x = x*A
proof
let x be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: len A>0 and
A2: width A>0 and
A3: len A=len x or width (A@)=len x;
A4: len A=len x by A2,A3,MATRIX_0:54;
A5: len A=width (A@) by A2,MATRIX_0:54;
then len ColVec2Mx x=len x by A1,A3,Def9;
then
A6: width ((A@)*(ColVec2Mx x))=width ColVec2Mx x by A3,A5,MATRIX_3:def 4;
width ColVec2Mx x=1 by A1,A3,A5,Def9;
then
A7: 1 in Seg width ((A@)*(ColVec2Mx x)) by A6,FINSEQ_1:1;
A8: len LineVec2Mx x=1 by Def10;
A9: width LineVec2Mx x=len x by Def10;
then width LineVec2Mx x=len A by A2,A3,MATRIX_0:54;
then len ((LineVec2Mx x)*A)=len LineVec2Mx x & width ((LineVec2Mx x)*A)=
width A by MATRIX_3:def 4;
then Line((LineVec2Mx x)*A,1) = Line((((LineVec2Mx x)*A)@)@,1) by A2,A8,
MATRIX_0:57
.= Line(((A@)*((LineVec2Mx x)@))@,1) by A2,A4,A9,MATRIX_3:22
.= Line(((A@)*(ColVec2Mx x))@,1) by A1,A4,Th49
.= Col((A@)*(ColVec2Mx x),1) by A7,MATRIX_0:59;
hence thesis;
end;
theorem Th53:
for x being FinSequence of REAL,A being Matrix of REAL st len A>
0 & width A>0 & (width A=len x or len (A@)=len x) holds A*x = x*(A@)
proof
let x be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: len A>0 and
A2: width A>0 and
A3: width A=len x or len (A@)=len x;
len (A@) = width A & width (A@)=len A by A2,MATRIX_0:54;
then ((A@)@)*x=x*(A@) by A1,A2,A3,Th52;
hence thesis by A1,A2,MATRIX_0:57;
end;
theorem Th54:
for A,B being Matrix of REAL st len A=len B holds for i being
Nat st 1<=i & i<=width A holds Col(A+B,i)=Col(A,i)+Col(B,i)
proof
let A,B be Matrix of REAL;
assume
A1: len A=len B;
then
A2: dom A=dom B by FINSEQ_3:29;
let i be Nat;
A3: len Col(A,i)=len A by MATRIX_0:def 8;
len Col(B,i)=len B by MATRIX_0:def 8;
then
A4: len (Col(A,i)+Col(B,i))=len (Col(A,i)) by A1,A3,RVSUM_1:115;
assume 1<=i & i<=width A;
then
A5: i in Seg width A by FINSEQ_1:1;
A6: len (A+B)=len A by Th25;
Seg len (A+B)=dom (A+B) by FINSEQ_1:def 3;
then
A7: dom (Col(A,i)+Col(B,i))=dom (A+B) by A3,A6,A4,FINSEQ_1:def 3;
for j st j in dom (A+B) holds (Col(A,i)+Col(B,i)).j = (A+B)*(j,i)
proof
let j;
assume
A8: j in dom (A+B);
then j in Seg len (A+B) by FINSEQ_1:def 3;
then
A9: j in dom A by A6,FINSEQ_1:def 3;
then
A10: [j,i] in Indices A by A5,ZFMISC_1:87;
reconsider j as Element of NAT by ORDINAL1:def 12;
Col(A,i).j=A*(j,i) & Col(B,i).j=B*(j,i) by A2,A9,MATRIX_0:def 8;
then Col(A,i).j+Col(B,i).j=(A+B)*(j,i) by A10,Th25;
hence thesis by A7,A8,VALUED_1:def 1;
end;
hence thesis by A3,A6,A4,MATRIX_0:def 8;
end;
theorem Th55:
for A,B being Matrix of REAL st width A=width B holds for i
being Nat st 1<=i & i<=len A holds Line(A+B,i)=Line(A,i)+Line(B,i)
proof
let A,B be Matrix of REAL;
assume
A1: width A=width B;
let i be Nat;
A2: len Line(A,i)=width A by MATRIX_0:def 7;
assume 1<=i & i<=len A;
then
A3: i in dom A by FINSEQ_3:25;
A4: width (A+B)=width A by Th25;
len Line(B,i)=width B by MATRIX_0:def 7;
then
A5: len (Line(A,i)+Line(B,i))=len Line(A,i) by A1,A2,RVSUM_1:115;
then
A6: dom (Line(A,i)+Line(B,i))=Seg width A by A2,FINSEQ_1:def 3;
for j st j in Seg width (A+B) holds (Line(A,i)+Line(B,i)).j = (A+B)*(i,j )
proof
let j;
assume
A7: j in Seg width (A+B);
then
A8: j in Seg width A by Th25;
then
A9: [i,j] in Indices A & Line(A,i).j=A*(i,j) by A3,MATRIX_0:def 7,ZFMISC_1:87;
reconsider j as Element of NAT by ORDINAL1:def 12;
Line(B,i).j=B*(i,j) by A1,A8,MATRIX_0:def 7;
then Line(A,i).j+Line(B,i).j=(A+B)*(i,j) by A9,Th25;
hence thesis by A4,A6,A7,VALUED_1:def 1;
end;
hence thesis by A2,A4,A5,MATRIX_0:def 7;
end;
theorem Th56:
for a being Real, M being (Matrix of REAL), i being Nat st 1<=i
& i<=width M holds Col(a*M,i)=a*Col(M,i)
proof
let a be Real, M be Matrix of REAL;
reconsider ea=a as Element of F_Real by XREAL_0:def 1;
let i be Nat;
assume
A1: 1<=i & i<=width M;
Col(a*M,i)=Col(MXF2MXR (ea*(MXR2MXF M)),i) by Def7
.=ea*Col(MXR2MXF M,i) by A1,Th19;
hence thesis by Th17;
end;
theorem
for x1,x2 being FinSequence of REAL, A being Matrix of REAL st len x1=
len x2 & width A=len x1 & len x1>0 holds A*(x1+x2)=A*x1 + A*x2
proof
let x1,x2 be FinSequence of REAL, A be Matrix of REAL;
assume that
A1: len x1=len x2 and
A2: width A=len x1 and
A3: len x1 >0;
A5: len ColVec2Mx x2=len x2 by A1,A3,Def9;
A6: len ColVec2Mx x1=len x1 by A3,Def9;
then
A7: len (A*(ColVec2Mx x1))=len A by A2,MATRIX_3:def 4
.=len (A*(ColVec2Mx x2)) by A1,A2,A5,MATRIX_3:def 4;
A8: width ColVec2Mx x1=1 by A3,Def9;
then
A9: 1<=width(A*(ColVec2Mx x1)) by A2,A6,MATRIX_3:def 4;
A10: width ColVec2Mx x2=1 by A1,A3,Def9;
thus A*(x1+x2)=Col(A*(ColVec2Mx x1+ColVec2Mx x2),1) by A1,A3,Th46
.=Col(A*(ColVec2Mx x1)+A*(ColVec2Mx x2),1) by A1,A2,A6,A5,A8,A10,
MATRIX_4:62
.=A*x1 + A*x2 by A7,A9,Th54;
end;
theorem
for x1,x2 being FinSequence of REAL, A being Matrix of REAL st len x1=
len x2 & len A=len x1 holds (x1+x2)*A=x1*A + x2*A
proof
let x1,x2 be FinSequence of REAL,A be Matrix of REAL;
assume that
A1: len x1=len x2 and
A2: len A=len x1;
A4: width LineVec2Mx x2=len x2 by Def10;
A5: width LineVec2Mx x1=len x1 by Def10;
then
A6: width ((LineVec2Mx x1)*A)=width A by A2,MATRIX_3:def 4
.=width ((LineVec2Mx x2)*A) by A1,A2,A4,MATRIX_3:def 4;
A7: len LineVec2Mx x1=1 by Def10;
then
A8: 1<=len((LineVec2Mx x1)*A) by A2,A5,MATRIX_3:def 4;
A9: len LineVec2Mx x2=1 by Def10;
thus (x1+x2)*A=Line((LineVec2Mx x1+LineVec2Mx(x2))*A,1) by A1,Th50
.=Line((LineVec2Mx x1)*A+(LineVec2Mx x2)*A,1) by A1,A2,A5,A4,A7,A9,
MATRIX_4:63
.=x1*A + x2*A by A6,A8,Th55;
end;
theorem Th59:
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,Def9;
width ColVec2Mx x=1 by A2,Def9;
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,Th47
.=Col(a*(A*(ColVec2Mx x)),1) by A1,A3,Th40
.=a*(A*x) by A4,Th56;
end;
theorem
for a being Real, x being FinSequence of REAL,
A being Matrix of REAL
st len A=len x & len x>0 & width A>0 holds (a*x)*A=a*(x*A)
proof
let a be Real,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,Th52;
A5: width (A@)=len x by A1,A3,MATRIX_0:54;
then
A6: (A@)*(a*x)=a*((A@)*x) by A2,Th59;
A7: len (a*x)=len x by RVSUM_1:117;
len (A@)>0 by A3,MATRIX_0:54;
then (a*x)*((A@)@)=(A@)*(a*x) by A2,A5,A7,Th53;
hence thesis by A1,A2,A3,A6,A4,MATRIX_0:57;
end;
theorem Th61:
for x being FinSequence of REAL, A being Matrix of REAL st width
A=len x & len x>0 holds len (A*x) = len A
proof
let 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,Def9;
len (Col(A*(ColVec2Mx x),1))=len (A*(ColVec2Mx x)) by MATRIX_0:def 8
.=len A by A1,A3,MATRIX_3:def 4;
hence thesis;
end;
theorem Th62:
for x being FinSequence of REAL, A being Matrix of REAL st len A
=len x holds len (x*A) = width A
proof
let x be FinSequence of REAL, A be Matrix of REAL;
assume
A1: len A=len x;
A2: width LineVec2Mx x=len x by Def10;
len Line((LineVec2Mx x)*A,1)=width (MXF2MXR ((MXR2MXF (LineVec2Mx x))*(
MXR2MXF A))) by MATRIX_0:def 7
.=width A by A1,A2,MATRIX_3:def 4;
hence thesis;
end;
theorem Th63:
for x being FinSequence of REAL, A,B being Matrix of REAL st len
A=len B & width A=width B & width A=len x & len x>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 A=len B & width A=width B and
A2: width A=len x and
A4: len x>0;
A5: len ColVec2Mx x=len x by A4,Def9;
then
A6: len (A*(ColVec2Mx x))=len A by A2,MATRIX_3:def 4
.=len (B*(ColVec2Mx x)) by A1,A2,A5,MATRIX_3:def 4;
A7: width (A*(ColVec2Mx x))=width (ColVec2Mx x) by A2,A5,MATRIX_3:def 4
.=1 by A4,Def9;
thus (A+B)*x = Col(A*(ColVec2Mx x)+B*(ColVec2Mx x),1) by A1,A2,A5,MATRIX_4:63
.=A*x +B*x by A6,A7,Th54;
end;
theorem Th64:
for x being FinSequence of REAL, A,B being Matrix of REAL st len
A=len B & width A=width B & len A=len x 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 A=len B & width A=width B and
A2: len A=len x;
A4: width LineVec2Mx x=len x by Def10;
then
A5: len ((LineVec2Mx x)*A)=len LineVec2Mx x by A2,MATRIX_3:def 4
.=1 by Def10;
A6: width ((LineVec2Mx x)*A)=width A by A2,A4,MATRIX_3:def 4
.=width ((LineVec2Mx x)*B) by A1,A2,A4,MATRIX_3:def 4;
thus x*(A+B) =Line((LineVec2Mx x)*A+(LineVec2Mx x)*B,1) by A1,A2,A4,
MATRIX_4:62
.=x*A +x*B by A6,A5,Th55;
end;
theorem
for n,m being Nat, x being FinSequence of REAL st len x=m &
n>0 & m>0 holds (0_Rmatrix(n,m))*x=0*n
proof
let n,m be Nat, x be FinSequence of REAL;
assume that
A1: len x=m and
A2: n>0 and
A3: m>0;
A4: width 0_Rmatrix(n,m)=m by A2,MATRIX_0:23;
then
A5: len ((0_Rmatrix(n,m))*x)=len (0_Rmatrix(n,m)) by A1,A3,Th61;
A6: len 0_Rmatrix(n,m) = n by A2,MATRIX_0:23;
then (0_Rmatrix(n,m))*x=(0_Rmatrix(n,m)+0_Rmatrix(n,m))*x by A2,A4,Th36
.=(0_Rmatrix(n,m))*x +(0_Rmatrix(n,m))*x by A1,A3,A6,A4,Th63;
then
0*n =(0_Rmatrix(n,m))*x +(0_Rmatrix(n,m))*x - (0_Rmatrix(n,m))*x by A6,A5,Th3
;
hence thesis by A5,Th14;
end;
theorem
for n,m being Nat, x being FinSequence of REAL st len x=n &
n>0 holds x*(0_Rmatrix(n,m))=0*m
proof
let n,m be Nat,x be FinSequence of REAL;
assume that
A1: len x=n and
A2: n>0;
A3: len (0_Rmatrix(n,m))=n by A2,MATRIX_0:23;
then
A4: len (x*(0_Rmatrix(n,m)))=width (0_Rmatrix(n,m)) by A1,Th62;
A5: width (0_Rmatrix(n,m))=m by A2,MATRIX_0:23;
then x*(0_Rmatrix(n,m))=x*(0_Rmatrix(n,m)+0_Rmatrix(n,m)) by A2,A3,Th36
.=x*(0_Rmatrix(n,m)) +x*(0_Rmatrix(n,m)) by A1,A5,A3,Th64;
then
0*m =x*(0_Rmatrix(n,m)) +x*(0_Rmatrix(n,m)) - x*(0_Rmatrix(n,m)) by A5,A4,Th3
;
hence thesis by A4,Th14;
end;