:: Matrices.
:: by Katarzyna Jankowska
::
:: Received June 8, 1991
:: Copyright (c) 1991-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, XBOOLE_0, FINSEQ_1, SUBSET_1, RELAT_1, CARD_1,
FINSEQ_2, TARSKI, TREES_1, XXREAL_0, ZFMISC_1, FUNCT_1, QC_LANG1,
INCSP_1, ARYTM_1, ARYTM_3, MATRIX_1, GOBRD13, CARD_3, FUNCT_6, FINSET_1,
CARD_2, MATRIX_0, PARTFUN1, FUNCOP_1, FINSEQ_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REAL_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, COMPLEX1, NAT_1, VALUED_0, RELAT_1, CARD_1, CARD_2,
FUNCT_1, INT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FINSEQ_1,
FINSEQ_2, FINSEQ_3, FINSEQ_4, CARD_3, FUNCT_6, BINOP_1, FINSEQOP;
constructors BINOP_1, XXREAL_0, FINSEQOP, RELSET_1, FINSEQ_3, INT_1, CARD_3,
FUNCT_6, CARD_2, WELLORD2, NAT_1, PRE_POLY, FINSEQ_4, XCMPLX_0, DOMAIN_1,
REAL_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, FINSEQ_1, FINSEQ_2,
ORDINAL1, CARD_1, FINSET_1, PRE_POLY, XXREAL_0, NAT_1, INT_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities BINOP_1, FINSEQ_2, ORDINAL1;
theorems FINSEQ_1, FINSEQ_2, FINSEQ_3, TARSKI, FUNCOP_1, FUNCT_1, FUNCT_2,
ZFMISC_1, NAT_1, RELAT_1, ORDINAL1, CARD_1, CARD_2, XXREAL_0, CARD_3,
FUNCT_6, FINSET_1, PARTFUN1, XBOOLE_0, XREAL_1, SEQM_3, INT_1;
schemes FINSEQ_1, BINOP_1, FINSEQ_2, FRAENKEL;
begin
reserve x,y,z for object,
i,j,n,m for Nat,
D for non empty set,
s,t for FinSequence,
a,a1,a2,b1,b2,d for Element of D,
p, p1,p2,q,r for FinSequence of D;
definition
let f be FinSequence;
attr f is tabular means
:Def1:
ex n being Nat st for x st x in rng f ex s
being FinSequence st s=x & len s = n;
end;
registration
cluster tabular for FinSequence;
existence
proof
take M={},0;
let x;
assume x in rng M;
hence thesis;
end;
end;
theorem Th1:
<*<*d*>*> is tabular
proof
take n = 1;
let x;
assume
A1: x in rng <*<*d*>*>;
A2: len <*d*> = n by FINSEQ_1:39;
rng <*<*d*>*> = {<*d*>} by FINSEQ_1:38;
then x = <*d*> by A1,TARSKI:def 1;
hence thesis by A2;
end;
theorem Th2:
m |-> (n |-> x) is tabular
proof
set s=m |-> (n |-> x);
reconsider n1=n as Nat;
take n1;
let z;
assume
A1: z in rng s;
take n|->x;
rng s c= {n |-> x} by FUNCOP_1:13;
hence thesis by A1,CARD_1:def 7,TARSKI:def 1;
end;
theorem Th3:
<*s*> is tabular
proof
take len s;
let x;
assume x in rng <*s*>;
then
A1: x in {s} by FINSEQ_1:38;
then reconsider t=x as FinSequence by TARSKI:def 1;
take t;
thus thesis by A1,TARSKI:def 1;
end;
theorem Th4:
for s1,s2 be FinSequence st len s1 =n & len s2 = n holds <*s1,s2
*> is tabular
proof
let s1,s2 be FinSequence;
assume
A1: len s1 =n & len s2 =n;
take n;
let x;
assume x in rng (<*s1,s2*>);
then
A2: x in { s1,s2} by FINSEQ_2:127;
then reconsider r=x as FinSequence by TARSKI:def 2;
take r;
thus x= r & len r=n by A1,A2,TARSKI:def 2;
end;
theorem Th5:
{} is tabular
proof
take n=0;
let x;
assume x in rng ({});
hence ex t st t=x & len t=n;
end;
theorem
<*{},{}*> is tabular by Th4,CARD_1:27;
theorem
<*<*a1*>,<*a2*>*> is tabular
proof
len <*a1*>=1 & len <*a2*>=1 by FINSEQ_1:39;
hence thesis by Th4;
end;
theorem
<*<*a1,a2*>,<*b1,b2*>*> is tabular
proof
len <*a1,a2*>=2 & len <*b1,b2*>=2 by FINSEQ_1:44;
hence thesis by Th4;
end;
registration
let D be set;
cluster tabular for FinSequence of D*;
existence
proof
take <*>(D*),0;
thus thesis;
end;
end;
definition
let D be set;
mode Matrix of D is tabular FinSequence of D*;
end;
registration let X be set;
cluster -> Function-yielding for Matrix of X;
coherence;
end;
registration
let D be non empty set;
cluster non empty-yielding for Matrix of D;
existence
proof
set d = the Element of D;
A1: rng <*<*d*>*>= {<*d*>} by FINSEQ_1:38;
<*d*> in D* by FINSEQ_1:def 11;
then rng <*<*d*>*> c= D* by A1,ZFMISC_1:31;
then reconsider p = <*<*d*>*> as FinSequence of D* by FINSEQ_1:def 4;
reconsider s = <*d*> as FinSequence;
reconsider p as tabular FinSequence of D* by Th1;
take p;
now
take s;
thus s in rng p by A1,TARSKI:def 1;
thus s <> {};
end;
hence thesis by RELAT_1:149;
end;
end;
theorem Th9:
s is Matrix of D iff ex n st for x st x in rng s ex p st x = p & len p = n
proof
thus s is Matrix of D implies ex n st for x st x in rng s ex p st x=p & len
p = n
proof
assume s is Matrix of D;
then reconsider s as tabular FinSequence of D*;
consider n such that
A1: for x st x in rng s ex t st t=x & len t = n by Def1;
take n;
for x st x in rng s ex p st x=p & len p = n
proof
let x;
assume
A2: x in rng s;
then consider v being FinSequence such that
A3: v=x and
A4: len v=n by A1;
rng s c= D* by FINSEQ_1:def 4;
then reconsider p=v as FinSequence of D by A2,A3,FINSEQ_1:def 11;
take p;
thus thesis by A3,A4;
end;
hence thesis;
end;
given n such that
A5: for x st x in rng s ex p st x = p & len p = n;
A6: s is tabular
proof
consider n such that
A7: for x st x in rng s ex p st x = p & len p = n by A5;
take n;
for x st x in rng s ex t st t= x & len t= n
proof
let x;
assume x in rng s;
then consider p such that
A8: x = p & len p = n by A7;
reconsider t=p as FinSequence;
take t;
thus thesis by A8;
end;
hence thesis;
end;
rng s c= D*
proof
let x be object;
assume x in rng s;
then ex p st x=p & len p = n by A5;
then reconsider q=x as FinSequence of D;
q in D* by FINSEQ_1:def 11;
hence thesis;
end;
hence thesis by A6,FINSEQ_1:def 4;
end;
definition let D; let m,n be Nat; let M be Matrix of D;
attr M is (m,n)-size means
:Def2: len M = m & for p st p in rng M holds len p = n;
end;
registration let D; let m,n be Nat;
cluster (m,n)-size for Matrix of D;
existence
proof
set a = the Element of D;
reconsider d= n |-> a as Element of D* by FINSEQ_1:def 11;
reconsider M= m |-> d as FinSequence of D*;
ex n be Nat st for x st x in rng M ex p st x =p & len p = n
proof
reconsider p=n |-> a as FinSequence of D;
take n;
let x;
assume
A1: x in rng M;
take p;
rng M c= {n |->a} by FUNCOP_1:13;
hence thesis by A1,CARD_1:def 7,TARSKI:def 1;
end;
then reconsider M as Matrix of D by Th9;
take M;
thus len M = m by CARD_1:def 7;
let p;
A2: rng M c= {n |-> a} by FUNCOP_1:13;
assume p in rng M;
then p = n |-> a by A2,TARSKI:def 1;
hence thesis by CARD_1:def 7;
end;
end;
definition
let D;
let m,n;
mode Matrix of m,n,D is (m,n)-size Matrix of D;
end;
definition
let D,n;
mode Matrix of n,D is Matrix of n,n,D;
end;
theorem Th10:
m |-> (n |-> a) is Matrix of m,n,D
proof
reconsider n1=n,m1=m as Nat;
reconsider d= n1 |-> a as Element of D* by FINSEQ_1:def 11;
reconsider M= m1 |-> d as FinSequence of D*;
reconsider M as Matrix of D by Th2;
M is (m,n)-size
proof
thus len M = m by CARD_1:def 7;
let p;
A1: rng M c= {n |-> a} by FUNCOP_1:13;
assume p in rng M;
then p = n |-> a by A1,TARSKI:def 1;
hence thesis by CARD_1:def 7;
end;
hence thesis;
end;
theorem Th11:
for p being FinSequence of D holds <*p*> is Matrix of 1,len p,D
proof
let p be FinSequence of D;
reconsider p9 = p as Element of (D)* by FINSEQ_1:def 11;
<*p9*> is tabular by Th3;
then reconsider M = <*p*> as Matrix of D;
M is (1,len p)-size
proof
thus len M = 1 by FINSEQ_1:39;
let q;
assume q in rng M;
then q in { p } by FINSEQ_1:38;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
theorem Th12:
for p1,p2 st len p1 =n & len p2 = n holds <*p1,p2*> is Matrix of 2,n,D
proof
let p1,p2;
reconsider q1 = p1,q2 = p2 as Element of D* by FINSEQ_1:def 11;
reconsider M = <*q1,q2*> as FinSequence of D*;
assume
A1: len p1 =n & len p2 =n;
then reconsider M as Matrix of D by Th4;
M is (2,n)-size
proof
thus len M = 2 by FINSEQ_1:44;
let r;
assume r in rng M;
then r in { p1,p2 } by FINSEQ_2:127;
hence thesis by A1,TARSKI:def 2;
end;
hence thesis;
end;
theorem Th13:
{} is Matrix of 0,m,D
proof
reconsider M =<*>(D*) as FinSequence of D*;
reconsider M as Matrix of D by Th5;
M is (0,m)-size;
hence thesis;
end;
theorem
<*{}*> is Matrix of 1,0,D
proof
len <*>D =0;
hence thesis by Th11;
end;
theorem
<*<*a*>*> is Matrix of 1,D
proof
len <*a*> =1 by FINSEQ_1:39;
hence thesis by Th11;
end;
theorem
<*{},{}*> is Matrix of 2,0,D
proof
len <*>D=0;
hence thesis by Th12;
end;
theorem
<*<*a1,a2*>*> is Matrix of 1,2,D
proof
<*a1,a2*> is FinSequence of D & len <*a1,a2*> =2 by FINSEQ_1:44;
hence thesis by Th11;
end;
theorem
<*<*a1*>,<*a2*>*> is Matrix of 2,1,D
proof
len <*a1*>=1 & len <*a2*>=1 by FINSEQ_1:39;
hence thesis by Th12;
end;
theorem Th19:
<*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D
proof
A1: len <*a1,a2*>=2 & len <*b1,b2*>=2 by FINSEQ_1:44;
thus thesis by A1,Th12;
end;
reserve M,M1,M2 for Matrix of D;
definition
let M be tabular FinSequence;
func width M -> Nat means
:Def3:
ex s st s in rng M & len s = it if len M > 0 otherwise it = 0;
existence
proof
thus len M > 0 implies ex n be Nat,s st s in rng M & len s = n
proof
set x = the Element of rng M;
consider n such that
A1: for x st x in rng M ex s st s=x & len s = n by Def1;
reconsider n as Nat;
assume len M > 0;
then
A2: rng M <>{} by CARD_1:27,RELAT_1:41;
then consider s such that
A3: s=x & len s = n by A1;
take n;
take s;
thus thesis by A2,A3;
end;
thus thesis;
end;
uniqueness
proof
let n1,n2 be Nat;
thus len M > 0 implies ((ex s st s in rng M & len s = n1) & (ex s st s in
rng M & len s = n2) implies n1 = n2)
proof
assume len M > 0;
given s such that
A4: s in rng M and
A5: len s = n1;
consider n such that
A6: for x st x in rng M ex s st s=x & len s=n by Def1;
A7: ex s1 be FinSequence st s1=s & len s1 =n by A6,A4;
given p be FinSequence such that
A8: p in rng M and
A9: len p=n2;
ex p1 be FinSequence st p1=p & len p1 = n by A6,A8;
hence thesis by A5,A9,A7;
end;
thus thesis;
end;
consistency;
end;
theorem Th20:
len M > 0 implies for n holds M is Matrix of len M, n, D iff n = width M
proof
assume
A1: len M > 0;
let n;
thus M is Matrix of len M, n, D implies n = width M
proof
consider s such that
A2: s in rng M and
A3: len s=width M by A1,Def3;
rng M c= D* by FINSEQ_1:def 4;
then reconsider q=s as FinSequence of D by A2,FINSEQ_1:def 11;
assume M is Matrix of len M, n, D;
then len q= n by A2,Def2;
hence thesis by A3;
end;
assume n=width M;
then for p st p in rng M holds len p=n by A1,Def3;
hence thesis by Def2;
end;
definition
let M be tabular FinSequence;
func Indices M -> set equals
[:dom M,Seg width M:];
coherence;
end;
definition
let D be set;
let M be Matrix of D;
let i,j;
assume
A1: [i,j] in Indices M;
func M*(i,j) -> Element of D means
:Def5:
ex p being FinSequence of D st p = M.i & it = p.j;
existence
proof
i in dom M by A1,ZFMISC_1:87;
then
A2: M.i in rng M by FUNCT_1:def 3;
rng M c= D* by FINSEQ_1:def 4;
then reconsider p=M.i as FinSequence of D by A2,FINSEQ_1:def 11;
A3: j in Seg width M by A1,ZFMISC_1:87;
M<> {} & len M >= 0 by A1,ZFMISC_1:87;
then len M > 0;
then consider s such that
A4: s in rng M and
A5: len s = width M by Def3;
consider n such that
A6: for x st x in rng M ex t st t=x & len t = n by Def1;
A7: ex v being FinSequence st p = v & len v = n by A2,A6;
ex t st s = t & len t = n by A4,A6;
then j in dom p by A3,A5,A7,FINSEQ_1:def 3;
then
A8: p.j in rng p by FUNCT_1:def 3;
rng p c=D by FINSEQ_1:def 4;
then reconsider a=p.j as Element of D by A8;
take a,p;
thus thesis;
end;
uniqueness;
end;
theorem Th21:
len M1 = len M2 & width M1 = width M2 & (for i,j st [i,j] in
Indices M1 holds M1*(i,j) = M2*(i,j)) implies M1 = M2
proof
assume that
A1: len M1 =len M2 and
A2: width M1= width M2 and
A3: for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j);
A4: dom M1= dom M2 by A1,FINSEQ_3:29;
for k be Nat st k in dom M1 holds M1.k = M2.k
proof
let k be Nat;
assume
A5: k in dom M1;
then
A6: M1.k in rng M1 by FUNCT_1:def 3;
rng M1 c= D* by FINSEQ_1:def 4;
then reconsider p = M1.k as FinSequence of D by A6,FINSEQ_1:def 11;
M1 <> {} by A5;
then
A7: len M1 > 0;
then M1 is Matrix of len M1,width M1,D by Th20;
then
A8: len p = width M1 by A6,Def2;
A9: M2.k in rng M2 by A4,A5,FUNCT_1:def 3;
rng M2 c= D* by FINSEQ_1:def 4;
then reconsider q = M2.k as FinSequence of D by A9,FINSEQ_1:def 11;
M2 is Matrix of len M1,width M1,D by A1,A2,A7,Th20;
then
A10: len q = width M1 by A9,Def2;
for l be Nat st 1 <= l & l <= len p holds p.l = q.l
proof
let l be Nat;
A11: rng p c= D by FINSEQ_1:def 4;
assume 1 <= l & l <= len p;
then
A12: l in Seg width M1 by A8,FINSEQ_1:1;
then l in dom p by A8,FINSEQ_1:def 3;
then p.l in rng p by FUNCT_1:def 3;
then reconsider a = p.l as Element of D by A11;
A13: rng q c= D by FINSEQ_1:def 4;
l in dom q by A10,A12,FINSEQ_1:def 3;
then q.l in rng q by FUNCT_1:def 3;
then reconsider b = q.l as Element of D by A13;
[k,l] in Indices M2 by A2,A4,A5,A12,ZFMISC_1:87;
then
A14: M2*(k,l)= b by Def5;
[k,l] in Indices M1 by A5,A12,ZFMISC_1:87;
then
A15: M1*(k,l)=a by Def5;
[k,l] in [:dom M1,Seg width M1:] by A5,A12,ZFMISC_1:87;
hence thesis by A3,A15,A14;
end;
hence thesis by A8,A10,FINSEQ_1:14;
end;
hence thesis by A4,FINSEQ_1:13;
end;
scheme
MatrixLambda { D() -> non empty set, n, m() -> Nat, f(set,set) ->
Element of D()} : ex M being Matrix of n(),m(),D() st for i,j st [i,j] in
Indices M holds M*(i,j) = f(i,j) proof
defpred P[set,object] means
ex p being FinSequence st $2=p & len p = m() & for
i st i in Seg m() holds p.i = f($1,i);
A1: for k be Nat st k in Seg n() ex y being object st P[k,y]
proof
let k be Nat;
assume k in Seg n();
deffunc F(Nat) = f(k,$1);
consider p being FinSequence such that
A2: len p =m() & for i be Nat st i in dom p holds p.i = F(i) from
FINSEQ_1:sch 2;
take p,p;
dom p = Seg m() by A2,FINSEQ_1:def 3;
hence thesis by A2;
end;
consider M being FinSequence such that
A3: dom M = Seg n() and
A4: for k be Nat st k in Seg n() holds P[k,M.k] from FINSEQ_1:sch 1(A1);
n() in NAT by ORDINAL1:def 12;
then
A5: len M = n() by A3,FINSEQ_1:def 3;
rng M c=D()*
proof
let x be object;
assume x in rng M;
then consider i be Nat such that
A6: i in dom M and
A7: M.i=x by FINSEQ_2:10;
consider p being FinSequence such that
A8: M.i=p and
A9: len p = m() & for j st j in Seg m() holds p.j = f(i,j) by A3,A4,A6;
rng p c= D()
proof
let z be object;
assume z in rng p;
then consider k be Nat such that
A10: k in dom p and
A11: p.k =z by FINSEQ_2:10;
k in Seg len p by A10,FINSEQ_1:def 3;
then z = f(i,k) by A9,A11;
hence thesis;
end;
then p is FinSequence of D() by FINSEQ_1:def 4;
hence thesis by A7,A8,FINSEQ_1:def 11;
end;
then reconsider M as FinSequence of D()* by FINSEQ_1:def 4;
ex n st for x st x in rng M ex p being FinSequence of D() st x=p & len p = n
proof
take m();
let x;
assume x in rng M;
then consider i be Nat such that
A12: i in dom M & M.i =x by FINSEQ_2:10;
consider p being FinSequence such that
A13: x=p and
A14: len p = m() and
A15: for j st j in Seg m() holds p.j = f(i,j) by A3,A4,A12;
rng p c= D()
proof
let z be object;
assume z in rng p;
then consider k be Nat such that
A16: k in dom p and
A17: p.k =z by FINSEQ_2:10;
k in Seg len p by A16,FINSEQ_1:def 3;
then z = f(i,k) by A14,A15,A17;
hence thesis;
end;
then reconsider p as FinSequence of D() by FINSEQ_1:def 4;
take p;
thus thesis by A13,A14;
end;
then reconsider M as Matrix of D() by Th9;
for p being FinSequence of D() st p in rng M holds len p= m()
proof
let p be FinSequence of D();
assume p in rng M;
then consider i be Nat such that
A18: i in dom M & M.i =p by FINSEQ_2:10;
P[i,p] by A3,A4,A18;
hence thesis;
end;
then reconsider M as Matrix of n(),m(),D() by A5,Def2;
take M;
let i,j;
assume
A19: [i,j] in Indices M;
then n() <> 0 by A3,ZFMISC_1:87;
then
A20: n() > 0;
i in Seg n() by A3,A19,ZFMISC_1:87;
then
A21: ex q being FinSequence st M.i=q & len q = m() & for j st j in Seg m()
holds q.j = f(i,j) by A4;
j in Seg width M by A19,ZFMISC_1:87;
then
A22: j in Seg m() by A5,A20,Th20;
ex p being FinSequence of D() st p=M.i & M*(i,j)=p.j by A19,Def5;
hence thesis by A21,A22;
end;
scheme
MatrixEx { D() -> non empty set, n, m() -> Nat,
P[object,object,object] }:
ex M being Matrix of n(),m(),D() st for i,j st [i,j] in Indices M holds P[i,j
,M*(i,j)]
provided
A1: for i,j st [i,j] in [:Seg n(), Seg m():] ex x being Element of D()
st P[i,j,x]
proof
defpred Q[object,object,object] means P[$1,$2,$3] & $3 in D();
A2: for x,y st x in Seg n() & y in Seg m() ex z st z in D() & Q[x,y,z]
proof
let x,y;
assume that
A3: x in Seg n() and
A4: y in Seg m();
reconsider y9=y as Nat by A4;
reconsider x9=x as Nat by A3;
[x9,y9] in [:Seg n(),Seg m():] by A3,A4,ZFMISC_1:87;
then consider z9 being Element of D() such that
A5: P[x9,y9,z9] by A1;
take z9;
thus thesis by A5;
end;
consider f being Function of [:Seg n(),Seg m():],D() such that
A6: for x,y st x in Seg n() & y in Seg m() holds Q[x,y,f.(x,y)] from
BINOP_1:sch 1(A2);
defpred R[set,object] means
ex p being FinSequence st $2=p & len p = m() & for
i st i in Seg m() holds p.i = f.($1,i);
A7: for k be Nat st k in Seg n() ex y being object st R[k,y]
proof
let k be Nat;
assume k in Seg n();
deffunc F(Nat) = f.[k,$1];
consider p being FinSequence such that
A8: len p =m() & for i be Nat st i in dom p holds p.i = F(i) from
FINSEQ_1:sch 2;
take p,p;
dom p = Seg m() by A8,FINSEQ_1:def 3;
hence thesis by A8;
end;
consider M being FinSequence such that
A9: dom M = Seg n() and
A10: for k be Nat st k in Seg n() holds R[k,M.k] from FINSEQ_1:sch 1(A7);
n() in NAT by ORDINAL1:def 12;
then
A11: len M = n() by A9,FINSEQ_1:def 3;
rng M c=D()*
proof
let x be object;
assume x in rng M;
then consider i be Nat such that
A12: i in Seg n() and
A13: M.i=x by A9,FINSEQ_2:10;
consider p being FinSequence such that
A14: M.i=p and
A15: len p = m() and
A16: for j st j in Seg m() holds p.j = f.(i,j) by A10,A12;
rng p c= D()
proof
let z be object;
assume z in rng p;
then consider k be Nat such that
A17: k in dom p and
A18: p.k =z by FINSEQ_2:10;
A19: k in Seg len p by A17,FINSEQ_1:def 3;
then
A20: [i,k] in [:Seg n(),Seg m():] by A12,A15,ZFMISC_1:87;
z = f.(i,k) by A15,A16,A18,A19;
hence thesis by A20,FUNCT_2:5;
end;
then p is FinSequence of D() by FINSEQ_1:def 4;
hence thesis by A13,A14,FINSEQ_1:def 11;
end;
then reconsider M as FinSequence of (D())* by FINSEQ_1:def 4;
ex n st for x st x in rng M ex p being FinSequence of D() st x=p & len p = n
proof
take m();
let x;
assume x in rng M;
then consider i be Nat such that
A21: i in dom M and
A22: M.i = x by FINSEQ_2:10;
consider p being FinSequence such that
A23: x=p and
A24: len p = m() and
A25: for j st j in Seg m() holds p.j =f.(i,j) by A9,A10,A21,A22;
rng p c= D()
proof
let z be object;
assume z in rng p;
then consider k be Nat such that
A26: k in dom p and
A27: p.k =z by FINSEQ_2:10;
A28: k in Seg len p by A26,FINSEQ_1:def 3;
then
A29: [i,k] in [:Seg n(),Seg m():] by A9,A21,A24,ZFMISC_1:87;
z = f.(i,k) by A24,A25,A27,A28;
hence thesis by A29,FUNCT_2:5;
end;
then reconsider p as FinSequence of D() by FINSEQ_1:def 4;
take p;
thus thesis by A23,A24;
end;
then reconsider M as Matrix of D() by Th9;
for p being FinSequence of D() st p in rng M holds len p= m()
proof
let p be FinSequence of D();
assume p in rng M;
then consider i be Nat such that
A30: i in dom M & M.i = p by FINSEQ_2:10;
R[i,p] by A9,A10,A30;
hence thesis;
end;
then reconsider M as Matrix of n(),m(),D() by A11,Def2;
take M;
let i,j;
assume
A31: [i,j] in Indices M;
then n() <> 0 by A9,ZFMISC_1:87;
then
A32: n() > 0;
j in Seg width M by A31,ZFMISC_1:87;
then
A33: j in Seg m() by A11,A32,Th20;
A34: ex p being FinSequence of D() st p=M.i & M*(i,j)=p.j by A31,Def5;
A35: i in Seg n() by A9,A31,ZFMISC_1:87;
then ex q being FinSequence st M.i=q & len q = m() & for j st j in Seg m()
holds q.j = f.(i,j) by A10;
then f.(i,j)=M*(i,j) by A34,A33;
hence thesis by A6,A35,A33;
end;
theorem
for M being Matrix of 0,m,D holds len M = 0 & width M = 0 & Indices M = {}
proof
let M be Matrix of 0,m,D;
len M = 0 by Def2;
then width M = 0 by Def3;
then Seg width M = 0;
hence thesis by Def2,ZFMISC_1:90;
end;
theorem Th23:
n > 0 implies for M being Matrix of n,m,D holds len M = n &
width M = m & Indices M = [:Seg n, Seg m:]
proof
assume
A1: n > 0;
let M be Matrix of n,m,D;
Seg len M = dom M & len M = n by Def2,FINSEQ_1:def 3;
hence thesis by A1,Th20;
end;
theorem Th24:
for M being Matrix of n,D holds len M = n & width M = n &
Indices M = [:Seg n, Seg n:]
proof
let M be Matrix of n,D;
A1: len M = n by Def2;
A2: now
per cases;
case
n =0;
hence width M = 0 by A1,Def3;
end;
case
n > 0;
hence width M= n by A1,Th20;
end;
end;
Seg len M = dom M by FINSEQ_1:def 3;
hence thesis by A2,Def2;
end;
theorem Th25:
for M being Matrix of n,m,D holds len M = n & Indices M = [:Seg
n,Seg width M:]
proof
let M be Matrix of n,m,D;
len M = n by Def2;
hence thesis by FINSEQ_1:def 3;
end;
theorem
for M1,M2 being Matrix of n,m,D holds Indices M1 = Indices M2
proof
let M1,M2 be Matrix of n,m,D;
A1: len M1 = n by Def2;
A2: len M2 = n by Def2;
A3: now
per cases;
suppose
A4: n = 0;
then width M1 = 0 by A1,Def3;
hence width M1= width M2 by A2,A4,Def3;
end;
suppose
A5: n > 0;
then width M1= m by A1,Th20;
hence width M1 = width M2 by A2,A5,Th20;
end;
end;
dom M1 = Seg n by A1,FINSEQ_1:def 3;
hence thesis by A2,A3,FINSEQ_1:def 3;
end;
theorem
for M1,M2 being Matrix of n,m,D st (for i,j st [i,j] in Indices
M1 holds M1*(i,j) = M2*(i,j)) holds M1 = M2
proof
let M1,M2 be Matrix of n,m,D;
A1: len M1=n by Th25;
A2: len M2=n by Th25;
A3: now
per cases;
suppose
A4: n =0;
then width M1 = 0 by A1,Def3;
hence width M1= width M2 by A2,A4,Def3;
end;
suppose
A5: n > 0;
then width M1= m by A1,Th20;
hence width M1 = width M2 by A2,A5,Th20;
end;
end;
assume for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j);
hence thesis by A1,A2,A3,Th21;
end;
theorem
for M1 being Matrix of n,D holds for i,j st [i,j] in Indices M1 holds
[j,i] in Indices M1
proof
let M1 be Matrix of n,D;
let i,j;
assume [i,j] in Indices M1;
then [i,j] in [:Seg n,Seg n:] by Th24;
then
A1: j in Seg n & i in Seg n by ZFMISC_1:87;
Indices M1 =[:Seg n,Seg n:] by Th24;
hence thesis by A1,ZFMISC_1:87;
end;
definition
let D;
let M be Matrix of D;
func M@ -> Matrix of D means
:Def6:
len it = width M & (for i,j holds [i,j]
in Indices it iff [j,i] in Indices M) & for i,j st [j,i] in Indices M holds it*
(i,j) = M*(j,i);
existence
proof
now
per cases;
suppose
A1: width M > 0;
deffunc F(Nat,Nat) = M*($2,$1);
consider M1 being Matrix of width M,len M,D such that
A2: for i,j st [i,j] in Indices M1 holds M1*(i,j) = F(i,j) from
MatrixLambda;
reconsider M9 = M1 as Matrix of D;
Seg len M = dom M by FINSEQ_1:def 3;
then
A3: Indices M1=[:Seg width M,dom M:] by A1,Th23;
thus thesis
proof
take M9;
thus len M9 = width M by A1,Th23;
thus for i,j holds [i,j] in Indices M9 iff [j,i] in Indices M by A3,
ZFMISC_1:88;
let i,j;
assume [j,i] in Indices M;
then [i,j] in Indices M9 by A3,ZFMISC_1:88;
hence thesis by A2;
end;
end;
suppose
A4: width M =0;
reconsider M1 = {} as Matrix of D by Th13;
thus thesis
proof
take M1;
A5: Indices M1=[:{},Seg width M1:];
Seg width M = {} by A4;
hence thesis by A5,ZFMISC_1:90;
end;
end;
end;
hence thesis;
end;
uniqueness
proof
let M1,M2 be Matrix of D;
assume that
A6: len M1 = width M and
A7: for i,j holds [i,j] in Indices M1 iff [j,i] in Indices M and
A8: for i,j st [j,i] in Indices M holds M1*(i,j)=M*(j,i) and
A9: len M2 = width M and
A10: for i,j holds [i,j] in Indices M2 iff [j,i] in Indices M and
A11: for i,j st [j,i] in Indices M holds M2*(i,j)=M*(j,i);
A12: now
let i,j;
assume [i,j] in Indices M1;
then
A13: [j,i] in Indices M by A7;
then M1*(i,j)=M*(j,i) by A8;
hence M1*(i,j)=M2*(i,j) by A11,A13;
end;
now
let x,y be object;
thus [x,y] in [:dom M1,Seg width M1:] implies [x,y] in [:dom M2,Seg
width M2:]
proof
assume
A14: [x,y] in [:dom M1,Seg width M1:];
then x in dom M1 by ZFMISC_1:87;
then reconsider i=x as Nat;
y in Seg width M1 by A14,ZFMISC_1:87;
then reconsider j=y as Nat;
[j,i] in Indices M by A7,A14;
hence thesis by A10;
end;
thus [x,y] in [:dom M2,Seg width M2:] implies [x,y] in [:dom M1,Seg
width M1:]
proof
assume
A15: [x,y] in [:dom M2,Seg width M2:];
then x in dom M2 by ZFMISC_1:87;
then reconsider i=x as Nat;
y in Seg width M2 by A15,ZFMISC_1:87;
then reconsider j=y as Nat;
[j,i] in Indices M by A10,A15;
hence thesis by A7;
end;
end;
then
A16: [:dom M1,Seg width M1:] = [:dom M2,Seg width M2:] by ZFMISC_1:89;
A17: now
assume
A18: len M1 <> 0;
then Seg len M2 <> {} by A6,A9;
then
A19: dom M2 <> {} by FINSEQ_1:def 3;
now
per cases;
suppose
A20: Seg width M1 <> {};
Seg len M1 <> {} by A18;
then dom M1 <> {} by FINSEQ_1:def 3;
then Seg width M1 = Seg width M2 by A16,A20,ZFMISC_1:110;
hence width M1 = width M2 by FINSEQ_1:6;
end;
suppose
A21: Seg width M1 = {};
then [:dom M2,Seg width M2:]= {} by A16,ZFMISC_1:90;
then Seg width M2 = {} by A19,ZFMISC_1:90;
hence width M1=width M2 by A21,FINSEQ_1:6;
end;
end;
hence len M1=len M2 & width M1 =width M2 by A6,A9;
end;
len M1 = 0 implies len M2= 0 & width M1 = 0 & width M2 = 0 by A6,A9,Def3;
hence thesis by A17,A12,Th21;
end;
end;
theorem Th29:
for M being Matrix of D st width M > 0
holds len (M@)=width M & width (M@)=len M
proof
let M be Matrix of D;
assume
A1: width M>0;
thus len (M@)=width M by Def6;
per cases;
suppose
len M=0;
hence thesis by A1,Def3;
end;
suppose
A2: len M>0;
A3: width (M@) in NAT by ORDINAL1:def 12;
for i,j being object holds [i,j]in [:dom (M@),Seg width (M@):] iff [i,j]
in [:Seg width M,dom M:]
proof
let i,j be object;
thus [i,j] in [:dom (M@),Seg width (M@):] implies [i,j] in [:Seg width M
,dom M:]
proof
assume
A4: [i,j]in [:dom (M@),Seg width (M@):];
then i in dom (M@) & j in Seg width (M@) by ZFMISC_1:87;
then reconsider i,j as Nat;
[i,j] in Indices (M@) by A4;
then [j,i] in Indices M by Def6;
hence thesis by ZFMISC_1:88;
end;
assume
A5: [i,j] in [:Seg width M,dom M:];
then i in Seg width M & j in dom M by ZFMISC_1:87;
then reconsider i,j as Nat;
[j,i] in Indices M by A5,ZFMISC_1:88;
then [i,j] in Indices (M@) by Def6;
hence thesis;
end;
then
dom M = Seg len M & [:Seg width M,dom M:]=[:dom (M@),Seg width (M@):]
by FINSEQ_1:def 3,ZFMISC_1:89;
then dom M=Seg width (M@) by A1,A2,ZFMISC_1:110;
hence thesis by FINSEQ_1:def 3,A3;
end;
end;
registration let n,D;
let M be Matrix of n,D;
cluster M@ -> (n,n)-size;
coherence
proof
set K = D, A = M;
A1: len A = n by Def2;
A2: for p being FinSequence of K st p in rng (A@) holds len p = n
proof
let p be FinSequence of K;
consider n2 being Nat such that
A3: for x st x in rng (A@) ex s being FinSequence st s=x &
len s = n2 by Def1;
A4: for p2 being FinSequence of K st p2 in rng (A@) holds len p2 = n2
proof
let p2 be FinSequence of K;
assume p2 in rng (A@);
then ex s being FinSequence st s=p2 & len s = n2 by A3;
hence thesis;
end;
assume
A5: p in rng (A@);
then
A6: ex s being FinSequence st s=p & len s = n2 by A3;
per cases;
suppose
A7: n>0;
then
A8: width A=n by A1,Th20;
then
A9: width (A@)=len A by A7,Th29;
A10: len (A@)=width A by A7,A8,Th29;
then A@ is Matrix of n,n2,K by A4,A8,Def2;
hence thesis by A1,A6,A7,A8,A10,A9,Th20;
end;
suppose
A11: n<=0;
A12: len (A@) = width A & ex x0 being object st x0 in dom (A@) & p=(A@).
x0 by A5,Def6,FUNCT_1:def 3;
width A=0 by A1,A11,Def3;
then Seg width A = {};
hence thesis by A12,FINSEQ_1:def 3;
end;
end;
A13: len (A@)=width A by Def6;
now
per cases;
suppose
n>0;
hence len (A@)=n by A13,A1,Th20;
end;
suppose
n=0;
hence len (A@)=n by A13,A1,Def3;
end;
end;
hence thesis by A2;
end;
end;
definition
let D,M,i;
func Line(M,i) -> FinSequence of D means
:Def7:
len it = width M & for j st j in Seg width M holds it.j = M*(i,j);
existence
proof
deffunc F(Nat) = M*(i,$1);
consider f being FinSequence of D such that
A1: len f = width M and
A2: for j be Nat st j in dom f holds f.j = F(j) from FINSEQ_2:sch 1;
take f;
thus len f = width M by A1;
let j;
dom f = Seg width M by A1,FINSEQ_1:def 3;
hence thesis by A2;
end;
uniqueness
proof
let p1,p2 be FinSequence of D;
assume that
A3: len p1=width M and
A4: for j st j in Seg width M holds p1.j = M*(i,j) and
A5: len p2=width M and
A6: for j st j in Seg width M holds p2.j = M*(i,j);
A7: dom p1 = Seg width M by A3,FINSEQ_1:def 3;
for j be Nat st j in dom p1 holds p1.j=p2.j
proof
let j be Nat;
assume
A8: j in dom p1;
then p1.j = M*(i,j) by A4,A7;
hence thesis by A6,A7,A8;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
func Col(M,i) -> FinSequence of D means
:Def8:
len it = len M & for j st j in dom M holds it.j = M*(j,i);
existence
proof
deffunc F(Nat) = M*($1,i);
consider z being FinSequence of D such that
A9: len z = len M and
A10: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
take z;
thus len z = len M by A9;
let j;
A11: Seg len M = dom M by FINSEQ_1:def 3;
dom z = Seg len M by A9,FINSEQ_1:def 3;
hence thesis by A10,A11;
end;
uniqueness
proof
let p1,p2 be FinSequence of D;
assume that
A12: len p1 = len M and
A13: for j st j in dom M holds p1.j = M*(j,i) and
A14: len p2= len M and
A15: for j st j in dom M holds p2.j = M*(j,i);
A16: dom p1 = Seg len M by A12,FINSEQ_1:def 3;
for j be Nat st j in dom p1 holds p1.j=p2.j
proof
let j be Nat;
assume j in dom p1;
then
A17: j in dom M by A16,FINSEQ_1:def 3;
then p1.j = M*(j,i) by A13;
hence thesis by A15,A17;
end;
hence thesis by A12,A14,FINSEQ_2:9;
end;
end;
definition
let D;
let M be Matrix of D;
let i;
redefine func Line(M,i) -> Element of (width M)-tuples_on D; :: redefines Line (MATRIX_0, definition)
coherence
proof
len Line(M,i) = width M & Line(M,i) is Element of D* by Def7,
FINSEQ_1:def 11;
then Line(M,i) in { p where p is Element of D*: len p = width M };
hence thesis;
end;
redefine func Col(M,i) -> Element of (len M)-tuples_on D; :: redefines Col (MATRIX_0, definition)
coherence
proof
len Col(M,i) = len M & Col(M,i) is Element of D* by Def8,FINSEQ_1:def 11;
then Col(M,i) in { p where p is Element of D*: len p = len M };
hence thesis;
end;
end;
theorem Th30:
for D being set for i,j for M being Matrix of D st 1 <= i & i <=
len M & 1 <= j & j <= width M holds [i,j] in Indices M
proof
let D be set;
let i,j;
let M be Matrix of D;
assume 1 <= i & i <= len M & 1 <= j & j <= width M;
then i in dom M & j in Seg width M by FINSEQ_1:1,FINSEQ_3:25;
hence thesis by ZFMISC_1:87;
end;
theorem
for M being Matrix of n,m,D st 1 <= i & i <= n & 1 <= j & j <= m holds
[i,j] in Indices M
proof
let M be Matrix of n,m,D such that
A1: 1 <= i & i <= n and
A2: 1 <= j & j <= m;
A3: len M = n by Def2;
per cases;
suppose
n = 0;
hence thesis by A1;
end;
suppose
n > 0;
then m = width M by Th23;
hence thesis by A1,A2,A3,Th30;
end;
end;
:: from GOBOARD5, 2008.03.08, A.T.
theorem Th32:
for M being tabular FinSequence, i,j st [i,j] in Indices M holds
1 <= i & i <= len M & 1 <= j & j <= width M
proof
let M be tabular FinSequence, i,j;
assume [i,j] in Indices M;
then i in dom M & j in Seg width M by ZFMISC_1:87;
hence thesis by FINSEQ_1:1,FINSEQ_3:25;
end;
theorem
for M being Matrix of n,m,D st [i,j] in Indices M holds 1 <= i & i <=
n & 1 <= j & j <= m
proof
let M be Matrix of n,m,D such that
A1: [i,j] in Indices M;
A2: len M = n by Def2;
per cases;
suppose
A3: n = 0;
A4: i in dom M by A1,ZFMISC_1:87;
then
A5: 1 <= i by FINSEQ_3:25;
i <= 0 by A2,A3,A4,FINSEQ_3:25;
hence thesis by A5;
end;
suppose
n > 0;
then m = width M by Th23;
hence thesis by A1,A2,Th32;
end;
end;
:: from GOBRD13, 2011.07.26, A.T.
definition
let F be Function-yielding Function;
func Values F -> set equals
Union rngs F;
correctness;
end;
theorem Th34:
for M being FinSequence of D* holds M.i is FinSequence of D
proof
let M be FinSequence of D*;
per cases;
suppose
not i in dom M;
then M.i = <*>D by FUNCT_1:def 2;
hence thesis;
end;
suppose
A1: i in dom M;
A2: rng M c= D* by FINSEQ_1:def 4;
M.i in rng M by A1,FUNCT_1:def 3;
hence thesis by A2,FINSEQ_1:def 11;
end;
end;
theorem Th35:
for M being FinSequence of D* holds Values M = union {rng f where
f is Element of D*: f in rng M}
proof
let M be FinSequence of D*;
set R = {rng f where f is Element of D*: f in rng M};
A1: Union rngs M = union rng rngs M by CARD_3:def 4;
now
let y be object;
hereby
assume y in Values M;
then consider Y being set such that
A2: y in Y and
A3: Y in rng rngs M by A1,TARSKI:def 4;
consider i being object such that
A4: i in dom rngs M and
A5: (rngs M).i = Y by A3,FUNCT_1:def 3;
A6: i in dom M by A4,FUNCT_6:60;
then reconsider i as Nat;
reconsider f = M.i as FinSequence of D by Th34;
A7: Y = rng f by A5,A6,FUNCT_6:22;
A8: f in D* by FINSEQ_1:def 11;
f in rng M by A6,FUNCT_1:def 3;
then rng f in R by A8;
hence y in union R by A2,A7,TARSKI:def 4;
end;
assume y in union R;
then consider Y being set such that
A9: y in Y and
A10: Y in R by TARSKI:def 4;
consider f being Element of D* such that
A11: Y = rng f and
A12: f in rng M by A10;
consider i being Nat such that
A13: i in dom M & M.i = f by A12,FINSEQ_2:10;
i in dom rngs M & (rngs M).i = rng f by A13,FUNCT_6:22;
then rng f in rng rngs M by FUNCT_1:def 3;
hence y in Values M by A1,A9,A11,TARSKI:def 4;
end;
hence thesis by TARSKI:2;
end;
registration
let D be non empty set, M be FinSequence of D*;
cluster Values M -> finite;
coherence
proof
deffunc F(Function) = rng $1;
set A = {F(f) where f is Element of D*: f in rng M};
A1: now
let X be set;
assume X in A;
then ex f being Element of D* st X = rng f & f in rng M;
hence X is finite;
end;
A2: rng M is finite;
{F(f) where f is Element of D*: f in rng M} is finite
from FRAENKEL:sch 21(A2);
then union A is finite by A1,FINSET_1:7;
hence thesis by Th35;
end;
end;
reserve f for FinSequence of D;
theorem Th36:
for M being Matrix of D st i in dom M & M.i = f holds len f = width M
proof
let M be Matrix of D such that
A1: i in dom M and
A2: M.i = f;
M is non empty by A1;
then len M > 0;
then consider p being FinSequence such that
A3: p in rng M and
A4: len p = width M by Def3;
consider n being Nat such that
A5: for x st x in rng M ex s being FinSequence st s=x & len s
= n by Def1;
M.i in rng M by A1,FUNCT_1:def 3;
then
A6: ex s being FinSequence st s = M.i & len s = n by A5;
ex s being FinSequence st s = p & len s = n by A3,A5;
hence thesis by A2,A4,A6;
end;
theorem Th37:
for M being Matrix of D st i in dom M & M.i = f & j in dom f
holds [i,j] in Indices M
proof
let M be Matrix of D such that
A1: i in dom M and
A2: M.i = f & j in dom f;
M is non empty by A1;
then len M > 0;
then consider p being FinSequence such that
A3: p in rng M and
A4: len p = width M by Def3;
consider n being Nat such that
A5: for x st x in rng M ex s being FinSequence st s=x & len s
= n by Def1;
M.i in rng M by A1,FUNCT_1:def 3;
then
A6: ex s being FinSequence st s = M.i & len s = n by A5;
ex s being FinSequence st s = p & len s = n by A3,A5;
then Indices M = [:dom M,Seg width M:] & j in Seg width M by A2,A4,A6,
FINSEQ_1:def 3;
hence thesis by A1,ZFMISC_1:87;
end;
theorem Th38:
for M being Matrix of D st [i,j] in Indices M & M.i = f holds len
f = width M & j in dom f
proof
let M be Matrix of D such that
A1: [i,j] in Indices M;
A2: j in Seg width M by A1,ZFMISC_1:87;
M is non empty by A1,ZFMISC_1:87;
then len M > 0;
then consider p being FinSequence such that
A3: p in rng M and
A4: len p = width M by Def3;
consider n being Nat such that
A5: for x st x in rng M ex s being FinSequence st s=x & len s
= n by Def1;
i in dom M by A1,ZFMISC_1:87;
then M.i in rng M by FUNCT_1:def 3;
then
A6: ex s being FinSequence st s = M.i & len s = n by A5;
ex s being FinSequence st s = p & len s = n by A3,A5;
hence thesis by A2,A4,A6,FINSEQ_1:def 3;
end;
theorem Th39:
for M being Matrix of D
holds Values M =
{ M*(i,j) where i is Nat, j is Nat:
[i,j] in Indices M }
proof
let M be Matrix of D;
set V = { M*(i,j) where i is Nat, j is Nat:
[i,j] in Indices M },
R = {rng f where f is Element of D* : f in rng M};
A1: Values M = union R by Th35;
now
let y be object;
hereby
assume y in Values M;
then consider Y being set such that
A2: y in Y and
A3: Y in R by A1,TARSKI:def 4;
consider f being Element of D* such that
A4: Y = rng f and
A5: f in rng M by A3;
consider j being Nat such that
A6: j in dom f and
A7: f.j = y by A2,A4,FINSEQ_2:10;
consider i being Nat such that
A8: i in dom M and
A9: M.i = f by A5,FINSEQ_2:10;
reconsider i,j as Nat;
A10: [i,j] in Indices M by A8,A9,A6,Th37;
then ex p being FinSequence of D st p = M.i & M*(i,j) = p.j by Def5;
hence y in V by A9,A7,A10;
end;
assume y in V;
then consider i,j being Nat such that
A11: y = M*(i,j) and
A12: [i,j] in Indices M;
consider f being FinSequence of D such that
A13: f = M.i and
A14: M*(i,j) = f.j by A12,Def5;
j in dom f by A12,A13,Th38;
then
A15: f.j in rng f by FUNCT_1:def 3;
i in dom M by A12,ZFMISC_1:87;
then
A16: M.i in rng M by FUNCT_1:def 3;
f in D* by FINSEQ_1:def 11;
then rng f in R by A13,A16;
hence y in Values M by A1,A11,A14,A15,TARSKI:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem
for D being non empty set, M being Matrix of D
holds card Values M <= (len M)*(width M)
proof
let D be non empty set, M be Matrix of D;
A1: now
let x be object;
assume x in dom rngs M;
then
A2: x in dom M by FUNCT_6:60;
then reconsider i = x as Element of NAT;
reconsider f = M.i as FinSequence of D by Th34;
card rng f c= card dom f by CARD_2:61;
then card rng f c= card Seg len f by FINSEQ_1:def 3;
then card rng f c= card len f by FINSEQ_1:55;
then card rng f c= card width M by A2,Th36;
hence card ((rngs M).x) c= card width M by A2,FUNCT_6:22;
end;
card dom rngs M = card dom M by FUNCT_6:60
.= card len M by CARD_1:62;
then card Union rngs M c= card(len M)*`card(width M) by A1,CARD_2:86;
then Segm card Values M c= Segm card((len M)*(width M)) by CARD_2:39;
then card Values M <= card((len M)*(width M)) by NAT_1:39;
hence thesis;
end;
reserve i,j,i1,j1 for Nat;
theorem
for M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M
holds M*(i,j) in Values M
proof
let M be Matrix of D;
assume 1 <= i & i <= len M & 1 <= j & j <= width M;
then
A1: [i,j] in Indices M by Th30;
Values M = { M*(i1,j1) where i1,j1 is Nat
: [i1,j1] in Indices M } by Th39;
hence thesis by A1;
end;
:: from GOBOARD1, 2012.02.25, A.T.
theorem Th42:
for D being non empty set,M being Matrix of D holds for i,j st j
in dom M & i in Seg width M holds Col(M,i).j = Line(M,j).i
proof
let D be non empty set,M be Matrix of D;
let i,j;
assume that
A1: j in dom M and
A2: i in Seg width M;
thus Col(M,i).j = M*(j,i) by A1,Def8
.= Line(M,j).i by A2,Def7;
end;
definition
let D be non empty set;
let M be Matrix of D;
redefine attr M is empty-yielding means :: redefines empty-yielding (FUNCT_1, redefinition) → empty-yielding (RELAT_1, definition)
0 = len M or 0 = width M;
compatibility
proof
consider n being Nat such that
A1: for x st x in rng M ex s being FinSequence st s=x & len
s = n by Def1;
hereby
set s = the Element of rng M;
assume
A2: M is empty-yielding;
assume
A3: 0 <> len M;
then
A4: M <> {};
then ex p being FinSequence st p=s & len p = n by A1;
then reconsider s as FinSequence;
s = 0 by A2,A4,RELAT_1:149;
then len s = 0;
hence 0 = width M by A3,A4,Def3;
end;
assume
A5: 0 = len M or 0 = width M;
now
let s be set;
assume
A6: s in rng M;
then M <> {};
then len M > 0;
then consider p being FinSequence such that
A7: p in rng M and
A8: len p = 0 by A5,Def3;
ex q being FinSequence st q=p & len q = n by A1,A7;
then ex q being FinSequence st q=s & len q = 0 by A1,A6,A8;
hence s = {};
end;
hence thesis by RELAT_1:149;
end;
end;
reserve k for Nat, G for Matrix of D;
theorem Th43:
rng f misses rng Col(G,i) & f/.n = G*(m,k) & n in dom f & m in
dom G implies i<>k
proof
assume that
A1: rng f /\ rng Col(G,i)={} and
A2: f/.n=G*(m,k) and
A3: n in dom f and
A4: m in dom G and
A5: i=k;
f.n = G*(m,k) by A2,A3,PARTFUN1:def 6;
then
A6: G*(m,i) in rng f by A3,A5,FUNCT_1:def 3;
A7: dom G = Seg len G & dom Col(G,i)=Seg len Col(G,i) by FINSEQ_1:def 3;
len Col(G,i)=len G & Col(G,i).m=G*(m,i) by A4,Def8;
then G*(m,i) in rng Col(G,i) by A4,A7,FUNCT_1:def 3;
hence contradiction by A1,A6,XBOOLE_0:def 4;
end;
theorem
for D being non empty set, M being Matrix of D holds
M is non empty-yielding iff 0 < len M & 0 < width M;
theorem
for M1 being Matrix of 0, n, D, M2 being Matrix of 0, m, D holds M1 = M2
proof
let M1 be Matrix of 0, n, D, M2 be Matrix of 0, m, D;
len M1 = 0 & len M2 = 0 by Def2;
hence thesis by CARD_2:64;
end;
begin :: Some Examples of Matrices, from MATRIX_2, 2012.02.26, A.T.
reserve x,y,x1,x2,y1,y2 for object,
i,j,k,l,n,m for Nat,
D for non empty set,
s,s2 for FinSequence,
a,b,c,d for Element of D,
q,r for FinSequence of D,
a9,b9 for Element of D;
definition
let n,m;
let a be object;
func (n,m) --> a -> tabular FinSequence equals
n |-> (m |-> a);
coherence by Th2;
end;
definition
let D,n,m;
let d;
redefine func (n,m) --> d -> Matrix of n,m,D; :: redefines --> (MATRIX_0, definition)
coherence by Th10;
end;
theorem
[i,j] in Indices ((n,m)-->a) implies ((n,m)-->a) * (i,j)=a
proof
reconsider m1=m as Nat;
set M=(n,m)-->a;
assume
A1: [i,j] in Indices M;
then i in dom M by ZFMISC_1:87;
then i in Seg len M by FINSEQ_1:def 3;
then
A2: i in Seg n by Def2;
then
A3: n > 0;
j in Seg width M by A1,ZFMISC_1:87;
then j in Seg m by A3,Th23;
then
A4: (m1|->a).j = a by FUNCOP_1:7;
M.i=m1|->a by A2,FUNCOP_1:7;
hence thesis by A1,A4,Def5;
end;
definition
let a,b,c,d be object;
func (a,b)][(c,d) ->tabular FinSequence equals
<*<*a,b*>,<*c,d*>*>;
correctness
proof
len <*a,b*>=2 & len <*c,d*>=2 by FINSEQ_1:44;
hence thesis by Th4;
end;
end;
theorem Th47:
len (x1,x2)][(y1,y2)=2 & width (x1,x2)][(y1,y2)=2 & Indices (x1,
x2)][(y1,y2)=[:Seg 2,Seg 2:]
proof
set M = (x1,x2)][(y1,y2);
thus
A1: len M=2 by FINSEQ_1:44;
rng M = { <*x1,x2*>,<*y1,y2*>} by FINSEQ_2:127;
then
A2: <*x1,x2*> in rng M by TARSKI:def 2;
len <*x1,x2*>=2 by FINSEQ_1:44;
hence width M=2 by A1,A2,Def3;
hence thesis by A1,FINSEQ_1:def 3;
end;
theorem Th48:
[1,1] in Indices (x1,x2)][(y1,y2) & [1,2] in Indices (x1,x2)][(y1
,y2) & [2,1] in Indices (x1,x2)][(y1,y2) & [2,2] in Indices (x1,x2)][(y1,y2)
proof
A1: 2 in Seg 2 by FINSEQ_1:2,TARSKI:def 2;
Indices (x1,x2)][(y1,y2)=[:Seg 2,Seg 2:] & 1 in Seg 2 by Th47,FINSEQ_1:2
,TARSKI:def 2;
hence thesis by A1,ZFMISC_1:87;
end;
definition
let D;
let a be Element of D;
redefine func <*a*> -> Element of 1-tuples_on D; :: redefines <* (FINSEQ_1, definition)
coherence by FINSEQ_2:98;
end;
definition
let D;
let n;
let p be Element of n-tuples_on D;
redefine func <*p*> -> Matrix of 1,n,D; :: redefines <* (FINSEQ_1, definition)
coherence
proof
len p = n by CARD_1:def 7;
hence thesis by Th11;
end;
end;
theorem
[1,1] in Indices <*<*a*>*> & <*<*a*>*>*(1,1)=a
proof
set M=<*<*a*>*>;
Indices M= [:Seg 1,Seg 1:] & 1 in Seg 1 by Th24,FINSEQ_1:2,TARSKI:def 1;
hence
A1: [1,1] in Indices <*<*a*>*> by ZFMISC_1:87;
M.1= <*a*> & <*a*>.1=a;
hence thesis by A1,Def5;
end;
definition
let D;
let a,b,c,d be Element of D;
redefine func (a,b)][(c,d) -> Matrix of 2,D; :: redefines ][ (MATRIX_0, definition)
coherence by Th19;
end;
theorem
(a,b)][(c,d)*(1,1)=a & (a,b)][(c,d)*(1,2)=b & (a,b)][(c,d)*(2,1)=c & (
a,b)][(c,d)*(2,2)=d
proof
set M=(a,b)][(c,d);
A1: M.1= <*a,b*> & M.2=<*c,d*>;
A2: <*a,b*>.1=a & <*a,b*>.2=b;
A3: [2,1] in Indices M & [2,2] in Indices M by Th48;
A4: <*c,d*>.1=c & <*c,d*>.2=d;
[1,1] in Indices M & [1,2] in Indices M by Th48;
hence thesis by A1,A2,A4,A3,Def5;
:: assume
:: A1: [i,j] in Indices M;
:: func M*(i,j) -> Element of D means
:: :Def5:
:: ex p being FinSequence of D st p = M.i & it = p.j;
end;
theorem
for M being Matrix of D st len M=n holds M is Matrix of n,width M,D
proof
let M be Matrix of D;
assume that
A1: len M=n and
A2: not M is Matrix of n,width M,D;
set m= width M;
per cases by A2,Def2;
suppose
len M<>n;
hence contradiction by A1;
end;
suppose
A3: ex p be FinSequence of D st p in rng M & not len p=m;
consider k such that
A4: for x st x in rng M ex q st x = q & len q = k by Th9;
consider p be FinSequence of D such that
A5: p in rng M and
A6: len p<>m by A3;
reconsider x=p as set;
A7: ex q st x = q & len q = k by A5,A4;
now
per cases;
suppose
n= 0;
then M={} by A1;
hence len p= m by A5;
end;
suppose
n>0;
then consider s being FinSequence such that
A8: s in rng M and
A9: len s = width M by A1,Def3;
reconsider y=s as set;
ex r st y = r & len r = k by A4,A8;
hence len p= m by A7,A9;
end;
end;
hence contradiction by A6;
end;
end;
begin :: Deleting of Rows and Columns in a Matrix
theorem Th52:
for M be Matrix of n,m,D holds for k st k in Seg n holds M.k= Line(M,k)
proof
let M be Matrix of n,m,D;
let k;
assume
A1: k in Seg n;
len M = n & dom M = Seg len M by Th25,FINSEQ_1:def 3;
then
A2: M.k in rng M by A1,FUNCT_1:def 3;
per cases;
suppose
n=0;
hence thesis by A1;
end;
suppose
A3: 0 < n;
consider l such that
A4: for x st x in rng M ex p be FinSequence of D st x = p & len p = l
by Th9;
consider p being FinSequence of D such that
A5: M.k = p and
len p= l by A2,A4;
A6: width M=m by A3,Th23;
A7: for j st j in Seg width M holds p.j = M*(k,j)
proof
let j;
assume j in Seg width M;
then [k,j] in [:Seg n,Seg m:] by A1,A6,ZFMISC_1:87;
then [k,j] in Indices M by A3,Th23;
then ex q being FinSequence of D st q=M.k & M*(k,j)=q.j by Def5;
hence thesis by A5;
end;
len p=width M by A2,A6,A5,Def2;
hence thesis by A5,A7,Def7;
end;
end;
Lm1: for M be Matrix of D holds for k st k in dom M holds M.k=Line(M,k)
proof
let M be Matrix of D;
let k;
assume
A1: k in dom M;
then 1 <= k & k <= len M by FINSEQ_3:25;
then reconsider N = M as Matrix of len M, width M, D by Th20;
k in Seg len N by A1,FINSEQ_1:def 3;
hence thesis by Th52;
end;
definition
let i, D;
let M be Matrix of D;
func DelCol(M,i) -> Matrix of D means
:Def13: len it=len M & for k st k in dom M holds it.k=Del(Line(M,k),i);
existence
proof
per cases;
suppose
A1: not i in Seg width M;
take M;
thus len M = len M;
let k such that
A2: k in dom M;
len Line(M,k) = width M by Def7;
then
A3: not i in dom Line(M,k) by A1,FINSEQ_1:def 3;
thus M.k = Line(M,k) by A2,Lm1
.= Del(Line(M,k),i) by A3,FINSEQ_3:104;
end;
suppose
A4: i in Seg width M;
defpred P[Nat,Nat,Element of D] means $3=Del(Line(M,$1),i).$2;
per cases;
suppose
A5: len M=0;
then Seg len M = {};
hence thesis by A4,A5,Def3;
end;
suppose
A6: len M>0;
set n1=width M;
per cases;
suppose
n1=0;
hence thesis by A4;
end;
suppose
n1>0;
then consider m being Nat such that
A7: n1=m+1 by NAT_1:6;
reconsider m as Nat;
A8: for k st k in dom M holds len (Del(Line(M,k),i))=m
proof
let k;
assume k in dom M;
A9: len Line(M,k) = n1 by Def7;
then i in dom Line(M,k) by A4,FINSEQ_1:def 3;
then ex l being Nat st len Line(M,k)=l+1 & len Del(Line(M,k),i)=l
by FINSEQ_3:104;
hence thesis by A7,A9;
end;
A10: for k,l st [k,l] in [:Seg len M, Seg m:] ex x being Element of
D st P[k,l,x]
proof
let k,l;
assume
A11: [k,l] in [:Seg len M, Seg m:];
reconsider p=Del(Line(M,k),i) as FinSequence of D by FINSEQ_3:105;
dom M = Seg len M by FINSEQ_1:def 3;
then k in dom M by A11,ZFMISC_1:87;
then
A12: len p = m by A8;
A13: dom p = Seg len p by FINSEQ_1:def 3;
l in Seg m by A11,ZFMISC_1:87;
then reconsider x=p.l as Element of D by A12,A13,FINSEQ_2:11;
take x;
thus thesis;
end;
consider N being Matrix of len M,m,D such that
A14: for k,l st [k,l] in Indices N holds P[k,l,N*(k,l)]
from MatrixEx(A10);
dom M = Seg len M by FINSEQ_1:def 3;
then
A15: Indices N = [:dom M, Seg m :] by A6,Th23;
A16: for k,l st k in dom M & l in Seg m holds N*(k,l)=Del(Line(M,k), i).l
proof
let k,l;
assume k in dom M & l in Seg m;
then [k,l] in Indices N by A15,ZFMISC_1:87;
hence thesis by A14;
end;
A17: width N = m by A6,Th23;
reconsider N as Matrix of D;
take N;
for k st k in dom M holds N.k=Del(Line(M,k),i)
proof
let k;
assume
A18: k in dom M;
then k in Seg len M by FINSEQ_1:def 3;
then
A19: N.k=Line(N,k) by Th52;
reconsider s=N.k as FinSequence;
A20: len s= m by A17,A19,Def7;
then
A21: dom s = Seg m by FINSEQ_1:def 3;
A22: now
let j be Nat;
assume
A23: j in dom s;
then Line(N,k).j=N*(k,j) by A17,A21,Def7;
hence s.j=Del(Line(M,k),i).j by A16,A18,A19,A21,A23;
end;
len Del (Line(M,k),i)=m by A8,A18;
hence thesis by A20,A22,FINSEQ_2:9;
end;
hence thesis by A6,Th23;
end;
end;
end;
end;
uniqueness
proof
let M1,M2 be Matrix of D;
assume that
A24: len M1=len M and
A25: for k st k in dom M holds M1.k=Del(Line(M,k),i) and
A26: len M2=len M and
A27: for k st k in dom M holds M2.k=Del(Line(M,k),i);
A28: dom M1 = dom M by A24,FINSEQ_3:29;
now
let k be Nat;
assume
A29: k in dom M1;
hence M1.k=Del(Line(M,k),i) by A25,A28
.=M2.k by A27,A28,A29;
end;
hence thesis by A24,A26,FINSEQ_2:9;
end;
end;
theorem Th53:
for M1,M2 being Matrix of D st M1@=M2@ & len M1=len M2 holds M1 = M2
proof
let M1,M2 be Matrix of D;
assume that
A1: M1@=M2@ and
A2: len M1=len M2;
len (M1@) = width M1 by Def6;
then
A3: width M1=width M2 by A1,Def6;
A4: Indices M2=[:dom M2,Seg width M2:];
for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j)
proof
let i,j;
assume
A5: [i,j] in Indices M1;
dom M1 = Seg len M2 by A2,FINSEQ_1:def 3
.= dom M2 by FINSEQ_1:def 3;
then M2@*(j,i) = M2*(i,j) by A3,A4,A5,Def6;
hence thesis by A1,A5,Def6;
end;
hence thesis by A2,A3,Th21;
end;
theorem Th54:
for M being Matrix of D st width M > 0 holds len (M@)=width M &
width (M@)=len M
proof
let M be Matrix of D;
assume
A1: width M>0;
thus len (M@)=width M by Def6;
per cases;
suppose
len M=0;
hence thesis by A1,Def3;
end;
suppose
A2: len M>0;
A3: width (M@) in NAT by ORDINAL1:def 12;
for i,j being object holds [i,j]in [:dom (M@),Seg width (M@):] iff [i,j]
in [:Seg width M,dom M:]
proof
let i,j be object;
thus [i,j] in [:dom (M@),Seg width (M@):] implies [i,j] in [:Seg width M
,dom M:]
proof
assume
A4: [i,j]in [:dom (M@),Seg width (M@):];
then i in dom (M@) & j in Seg width (M@) by ZFMISC_1:87;
then reconsider i,j as Nat;
[i,j] in Indices (M@) by A4;
then [j,i] in Indices M by Def6;
hence thesis by ZFMISC_1:88;
end;
assume
A5: [i,j] in [:Seg width M,dom M:];
then i in Seg width M & j in dom M by ZFMISC_1:87;
then reconsider i,j as Nat;
[j,i] in Indices M by A5,ZFMISC_1:88;
then [i,j] in Indices (M@) by Def6;
hence thesis;
end;
then
dom M = Seg len M & [:Seg width M,dom M:]=[:dom (M@),Seg width (M@):]
by FINSEQ_1:def 3,ZFMISC_1:89;
then dom M=Seg width (M@) by A1,A2,ZFMISC_1:110;
hence thesis by FINSEQ_1:def 3,A3;
end;
end;
theorem
for M1,M2 being Matrix of D st width M1>0 & width M2>0 & M1@=M2@ holds M1=M2
proof
let M1,M2 be Matrix of D;
assume width M1>0 & width M2>0;
then
A1: width (M1@)=len M1 & width (M2@)=len M2 by Th54;
assume M1@=M2@;
hence thesis by A1,Th53;
end;
theorem
for M1,M2 being Matrix of D st width M1>0 & width M2>0 holds M1=M2 iff
M1@=M2@ & width M1 = width M2
proof
let M1,M2 be Matrix of D;
assume that
A1: width M1>0 and
A2: width M2>0;
thus M1=M2 implies M1@=M2@ & width (M1) =width (M2);
assume that
A3: M1@=M2@ and
A4: width (M1) =width (M2);
len M1=width (M1@) by A1,Th54;
then
A5: len M1=len M2 by A2,A3,Th54;
A6: Indices M2=[:dom M2,Seg width M2:];
for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j)
proof
let i,j;
assume
A7: [i,j] in Indices M1;
dom M1 = Seg len M2 by A5,FINSEQ_1:def 3
.= dom M2 by FINSEQ_1:def 3;
then M2@*(j,i)=M2*(i,j) by A4,A6,A7,Def6;
hence thesis by A3,A7,Def6;
end;
hence thesis by A4,A5,Th21;
end;
theorem Th57:
for M being Matrix of D st len M>0 & width M>0 holds (M@)@=M
proof
let M be Matrix of D;
assume that
A1: len M>0 and
A2: width M>0;
set N=M@;
A3: width N= len M by A2,Th54;
A4: len (N@) = width N by Def6;
A5: len N = width M by Def6;
dom M = Seg len M & dom (N@) = Seg len (N@) by FINSEQ_1:def 3;
then
A6: Indices (N@)=Indices M by A1,A5,A3,A4,Th54;
A7: for i,j st [i,j] in Indices (N@) holds (N@)*(i,j) = M*(i,j)
proof
let i,j;
assume
A8: [i,j] in Indices (N@);
then [j,i] in Indices N by Def6;
then (N@)*(i,j)=N*(j,i) by Def6;
hence thesis by A6,A8,Def6;
end;
width N>0 by A1,A2,Th54;
then width (N@)=width M by A5,Th54;
hence thesis by A3,A4,A7,Th21;
end;
theorem Th58:
for M being Matrix of D holds for i st i in dom M holds Line(M,i )=Col(M@,i)
proof
let M be Matrix of D;
let i;
A1: len (M@)=width M by Def6;
len Col(M@,i) = len (M@) by Def8;
then
A2: len Col(M@,i)=width M by Def6;
then
A3: dom Col(M@,i) = Seg width M by FINSEQ_1:def 3;
assume
A4: i in dom M;
A5: now
let j be Nat;
A6: dom (M@) = Seg len (M@) by FINSEQ_1:def 3;
assume
A7: j in dom Col(M@,i);
then Line(M,i).j=M*(i,j) & [i,j] in Indices M by A4,A3,Def7,ZFMISC_1:87;
hence Line(M,i).j=M@*(j,i) by Def6
.=Col(M@,i).j by A1,A3,A7,A6,Def8;
end;
len Line(M,i) = width M by Def7;
hence thesis by A2,A5,FINSEQ_2:9;
end;
theorem
for M being Matrix of D holds for j st j in Seg width M holds Line(M@,
j)=Col(M,j)
proof
let M be Matrix of D;
let j;
assume
A1: j in Seg width M;
then j in Seg len (M@) by Def6;
then
A2: j in dom (M@) by FINSEQ_1:def 3;
per cases;
suppose
A3: len M=0;
then Seg len M = {};
hence thesis by A1,A3,Def3;
end;
suppose
A4: len M>0;
per cases;
suppose
width M=0;
hence thesis by A1;
end;
suppose
width M>0;
then (M@)@=M by A4,Th57;
hence thesis by A2,Th58;
end;
end;
end;
theorem Th60:
for M being Matrix of D holds for i st i in dom M holds M.i=Line(M,i)
proof
let M be Matrix of D;
let i;
assume
A1: i in dom M;
then
A2: M.i in rng M by FUNCT_1:def 3;
rng M c= D* by FINSEQ_1:def 4;
then reconsider p=M.i as FinSequence of D by A2,FINSEQ_1:def 11;
M<> {} by A1;
then M is Matrix of len M,width M,D by Th20;
then
A3: len p = width M by A2,Def2;
A4: len Line(M,i)= width M by Def7;
then
A5: dom Line(M,i) = Seg width M by FINSEQ_1:def 3;
A6: for j st j in Seg (width M) holds M*(i,j) =p.j
proof
let j;
assume j in Seg(width M);
then [i,j] in Indices M by A1,ZFMISC_1:87;
then ex q being FinSequence of D st q=M.i & q.j=M*(i,j) by Def5;
hence thesis;
end;
now
let j be Nat;
assume
A7: j in dom Line(M,i);
hence (Line(M,i)).j=M*(i,j) by A5,Def7
.=p.j by A6,A5,A7;
end;
hence thesis by A3,A4,FINSEQ_2:9;
end;
notation
let D, i;
let M be Matrix of D;
synonym DelLine(M,i) for Del(M,i);
end;
registration
let D, i;
let M be Matrix of D;
cluster DelLine(M,i) -> tabular;
coherence
proof
consider n being Nat such that
A1: for x st x in rng M ex s being FinSequence st s=x & len s = n by Def1;
take n;
let x;
A2: rng DelLine(M,i) c= rng M by FINSEQ_3:106;
assume x in rng DelLine(M,i);
hence thesis by A1,A2;
end;
end;
definition
let D, i;
let M be Matrix of D;
redefine func DelLine(M,i) -> Matrix of D; :: redefines DelLine (MATRIX_0, synonym) → Del (FINSEQ_3, definition)
coherence by FINSEQ_3:105;
end;
definition
let i,j,n,D;
let M be Matrix of n,D;
func Deleting(M,i,j) -> Matrix of D equals
DelCol(DelLine(M,i),j);
coherence;
end;
theorem
not i in Seg width M implies DelCol(M,i) = M
proof assume
A1: not i in Seg width M;
A2: len DelCol(M,i) = len M by Def13;
for k st 1 <= k & k <= len M holds M.k = DelCol(M,i).k
proof let k such that
A3: 1 <= k & k <= len M;
A4: k in dom M by A3,FINSEQ_3:25;
len Line(M,k) = width M by Def7;
then
A5: not i in dom Line(M,k) by A1,FINSEQ_1:def 3;
thus M.k = Line(M,k) by A4,Lm1
.= Del(Line(M,k),i) by A5,FINSEQ_3:104
.= DelCol(M,i).k by A4,Def13;
end;
hence DelCol(M,i) = M by A2,FINSEQ_1:14;
end;
:: from GOBOARD1, 2012.03.01, A.T.
theorem Th62:
k in dom G implies Line(DelCol(G,i),k) = Del(Line(G,k),i)
proof
set D = DelCol(G,i);
assume that
A1: k in dom G;
len D = len G by Def13;
then
A2: dom D = dom G by FINSEQ_3:29;
D.k = Del(Line(G,k),i) by A1,Def13;
hence thesis by A1,A2,Th60;
end;
theorem Th63:
i in Seg width G & width G = m+1 implies width DelCol(G,i) = m
proof
set D = DelCol(G,i);
assume that
A1: i in Seg width G and
A2: width G = m+1;
width G <> 0 by A2;
then 0<len G by Def3;
then 0+1<=len G by NAT_1:13;
then
1 in dom G by FINSEQ_3:25;
then
A3: Line(D,1) = Del(Line(G,1),i) by Th62;
A4: dom Line(G,1) = Seg len Line(G,1) & len Line(D,1) = width D by Def7,
FINSEQ_1:def 3;
len Line(G,1) = m+1 by A2,Def7;
hence thesis by A1,A2,A3,A4,FINSEQ_3:109;
end;
theorem Th64:
i in Seg width G & width G > 0 implies width G = width DelCol(G,i) + 1
proof
assume that
A1: i in Seg width G and
A2: width G > 0;
ex m st width G = m+1 by A2,NAT_1:6;
hence thesis by A1,Th63;
end;
theorem
width G > 1 & i in Seg width G implies DelCol(G,i) is not empty-yielding
proof assume that
A1: width G > 1 and
A2:i in Seg width G;
width DelCol(G,i)+1 > 0+1 by A1,A2,Th64;
then
A3: width DelCol(G,i) > 0;
then len DelCol(G,i) > 0 by Def3;
hence DelCol(G,i) is not empty-yielding by A3;
end;
theorem Th66:
i in Seg width G & width G > 1 & n in dom G & m in Seg width
DelCol(G,i) implies DelCol(G,i)*(n,m)=Del(Line(G,n),i).m
proof
assume that
A1: i in Seg width G & width G > 1 & n in dom G and
A2: m in Seg width (DelCol(G,i));
thus DelCol(G,i)*(n,m) = Line(DelCol(G,i),n).m by A2,Def7
.= Del(Line(G,n),i).m by A1,Th62;
end;
reserve m for Nat;
theorem Th67:
i in Seg width G & width G = m+1 & m>0 & 1<=k & k<i implies Col(
DelCol(G,i),k) = Col(G,k) & k in Seg width DelCol(G,i) & k in Seg width G
proof
set N = DelCol(G,i);
assume that
A1: i in Seg width G and
A2: width G = m+1 and
A3: m>0 and
A4: 1<=k and
A5: k<i;
A6: width N = m by A1,A2,Th63;
A7: 1<width G by A2,A3,SEQM_3:43;
A8: len N = len G by Def13;
i<=m+1 by A1,A2,FINSEQ_1:1;
then
A9: k<m+1 by A5,XXREAL_0:2;
then
A10: k in Seg width G by A2,A4,FINSEQ_1:1;
A11: len Col(G,k)=len G by Def8;
A12: len Col(N,k) = len N by Def8;
A13: k<=m by A9,NAT_1:13;
then
A14: k in Seg width N by A4,A6,FINSEQ_1:1;
now
let j be Nat;
A15: dom N = Seg len N & dom G = Seg len G by FINSEQ_1:def 3;
assume 1<=j & j<=len Col(N,k);
then
A16: j in dom N by A12,FINSEQ_3:25;
hence Col(N,k).j= N*(j,k) by Def8
.= Del(Line(G,j),i).k by A1,A14,A7,A8,A16,A15,Th66
.= Line(G,j).k by A5,FINSEQ_3:110
.= Col(G,k).j by A10,A8,A16,A15,Th42;
end;
hence thesis by A2,A4,A6,A9,A13,A12,A11,A8,FINSEQ_1:1,14;
end;
theorem Th68:
i in Seg width G & width G = m+1 & m>0 & i<=k & k<=m implies Col
(DelCol(G,i),k) = Col(G,k+1) & k in Seg width DelCol(G,i) & k+1 in Seg width G
proof
set N = DelCol(G,i);
assume that
A1: i in Seg width G and
A2: width G = m+1 and
A3: m>0 and
A4: i<=k and
A5: k<=m;
A6: len Col(N,k) = len N by Def8;
A7: 1<width G by A2,A3,SEQM_3:43;
A8: len N = len G by Def13;
A9: 1<=k+1 & k+1<=m+1 by A5,NAT_1:11,XREAL_1:6;
then
A10: k+1 in Seg width G by A2,FINSEQ_1:1;
1<=i by A1,FINSEQ_1:1;
then
A11: 1<=k by A4,XXREAL_0:2;
A12: len Col(G,k+1)=len G by Def8;
A13: width N = m by A1,A2,Th63;
then
A14: k in Seg width N by A5,A11,FINSEQ_1:1;
now
let j be Nat;
A15: dom N = Seg len N & dom G = Seg len G by FINSEQ_1:def 3;
A16: len Line(G,j) = m+1 & dom Line(G,j) = Seg len Line(G,j) by A2,Def7,
FINSEQ_1:def 3;
assume 1<=j & j<=len Col(N,k);
then
A17: j in dom N by A6,FINSEQ_3:25;
hence Col(N,k).j= N*(j,k) by Def8
.= Del(Line(G,j),i).k by A1,A14,A7,A8,A17,A15,Th66
.= Line(G,j).(k+1) by A1,A2,A4,A5,A16,FINSEQ_3:111
.= Col(G,k+1).j by A10,A8,A17,A15,Th42;
end;
hence thesis by A2,A5,A13,A9,A11,A6,A12,A8,FINSEQ_1:1,14;
end;
theorem Th69:
i in Seg width G & width G = m+1 & m>0 & n in dom G & 1<=k & k<i
implies DelCol(G,i)*(n,k) = G*(n,k) & k in Seg width G
proof
assume that
A1: i in Seg width G and
A2: width G = m+1 & m>0 and
A3: n in dom G and
A4: 1<=k & k<i;
A5: len (DelCol(G,i)) = len G by Def13;
A6: dom G = Seg len G & Seg len(DelCol(G,i)) = dom(DelCol(G,i)) by
FINSEQ_1:def 3;
Col(DelCol(G,i),k) = Col(G,k) by A1,A2,A4,Th67;
hence DelCol(G,i)*(n,k) = Col(G,k).n by A3,A6,A5,Def8
.= G*(n,k) by A3,Def8;
thus thesis by A1,A2,A4,Th67;
end;
theorem Th70:
i in Seg width G & width G = m+1 & m>0 & n in dom G & i<=k & k<=
m implies DelCol(G,i)*(n,k) = G*(n,k+1) & k+1 in Seg width G
proof
assume that
A1: i in Seg width G and
A2: width G = m+1 & m>0 and
A3: n in dom G and
A4: i<=k & k<=m;
A5: len (DelCol(G,i)) = len G by Def13;
A6: dom G = Seg len G & Seg len(DelCol(G,i)) = dom(DelCol(G,i)) by
FINSEQ_1:def 3;
Col(DelCol(G,i),k)=Col(G,k+1) by A1,A2,A4,Th68;
hence DelCol(G,i)*(n,k) = Col(G,k+1).n by A3,A6,A5,Def8
.= G*(n,k+1) by A3,Def8;
thus thesis by A1,A2,A4,Th68;
end;
theorem
width G = m+1 & m>0 & k in Seg m implies Col(DelCol(G,1),k) = Col(G,k+
1) & k in Seg width DelCol(G,1) & k+1 in Seg width G
proof
assume that
A1: width G = m+1 and
A2: m>0 and
A3: k in Seg m;
1<=width G by A1,A2,SEQM_3:43;
then
A4: 1 in Seg width G by FINSEQ_1:1;
1<=k & k<=m by A3,FINSEQ_1:1;
hence thesis by A1,A4,Th68;
end;
theorem
width G = m+1 & m>0 & k in Seg m & n in dom G implies DelCol(G,1)*(n,k
) = G*(n,k+1) & 1 in Seg width G
proof
assume that
A1: width G = m+1 and
A2: m>0 and
A3: k in Seg m and
A4: n in dom G;
1<=width G by A1,A2,SEQM_3:43;
then
A5: 1 in Seg width G by FINSEQ_1:1;
1<=k & k<=m by A3,FINSEQ_1:1;
hence thesis by A1,A4,A5,Th70;
end;
theorem
width G = m+1 & m>0 & k in Seg m implies Col(DelCol(G,width G),k) =
Col(G,k) & k in Seg width DelCol(G,width G)
proof
assume that
A1: width G = m+1 and
A2: m>0 and
A3: k in Seg m;
k<=m by A3,FINSEQ_1:1;
then
A4: k<width G by A1,NAT_1:13;
1<=width G by A1,A2,SEQM_3:43;
then
A5: width G in Seg width G by FINSEQ_1:1;
1<=k by A3,FINSEQ_1:1;
hence thesis by A1,A2,A5,A4,Th67;
end;
theorem
width G = m+1 & m>0 & k in Seg m & n in dom G implies k in Seg
width G & DelCol(G,width G)*(n,k) = G*(n,k) & width G in Seg width G
proof
assume that
A1: width G = m+1 and
A2: m>0 and
A3: k in Seg m and
A4: n in dom G;
k<=m by A3,FINSEQ_1:1;
then
A5: k<width G by A1,NAT_1:13;
1<=width G by A1,A2,SEQM_3:43;
then
A6: width G in Seg width G by FINSEQ_1:1;
1<=k by A3,FINSEQ_1:1;
hence thesis by A1,A2,A4,A6,A5,Th69;
end;
reserve f for FinSequence of D,
G for Matrix of D;
theorem
rng f misses rng Col(G,i) & f/.n in rng Line(G,m) & n in dom f & i in
Seg width G & m in dom G & width G>1 implies f/.n in rng Line(DelCol(G,i),m)
proof
set D = DelCol(G,i);
assume that
A1: rng f misses rng Col(G,i) and
A2: f/.n in rng Line(G,m) and
A3: n in dom f and
A4: i in Seg width G and
A5: m in dom G and
A6: width G>1;
A7: len Line(D,m)=width D & dom Line(D,m) = Seg len Line(D,m) by Def7,
FINSEQ_1:def 3;
consider j being Nat such that
A8: j in dom Line(G,m) and
A9: f/.n=Line(G,m).j by A2,FINSEQ_2:10;
reconsider j as Nat;
A10: len Line(G,m) = width G by Def7;
then
A11: j<=width G by A8,FINSEQ_3:25;
A12: dom Line(G,m) = Seg len Line(G,m) by FINSEQ_1:def 3;
then
A13: 1<=i by A4,A10,FINSEQ_3:25;
A14: f/.n=G*(m,j) by A8,A9,A12,A10,Def7;
A15: i<=width G by A4,A12,A10,FINSEQ_3:25;
A16: 1<=j by A8,FINSEQ_3:25;
consider M be Nat such that
A17: width G = M+1 and
A18: M>0 by A6,SEQM_3:43;
A19: width D = M by A4,A17,Th63;
i <> j by A1,A3,A5,A14,Th43;
then per cases by XXREAL_0:1;
suppose
A20: j<i;
then j<width G by A15,XXREAL_0:2;
then j<=M by A17,NAT_1:13;
then
A21: j in Seg width D by A16,A19,FINSEQ_1:1;
f/.n=D*(m,j) by A4,A5,A14,A16,A17,A18,A20,Th69;
then Line(D,m).j=f/.n by A21,Def7;
hence thesis by A7,A21,FUNCT_1:def 3;
end;
suppose
A22: i<j;
reconsider l=j-1 as Element of NAT by A16,INT_1:5;
A23: l<=M by A11,A17,XREAL_1:20;
i+1<=j by A22,NAT_1:13;
then
A24: i<=l by XREAL_1:19;
then 1<=l by A13,XXREAL_0:2;
then
A25: l in Seg width D by A19,A23,FINSEQ_1:1;
l+1=j;
then f/.n=D*(m,l) by A4,A5,A14,A13,A17,A24,A23,Th70;
then Line(D,m).l=f/.n by A25,Def7;
hence thesis by A7,A25,FUNCT_1:def 3;
end;
end;