Copyright (c) 1991 Association of Mizar Users
environ
vocabulary VECTSP_1, FINSEQ_1, RLVECT_1, RELAT_1, BOOLE, FINSEQ_2, FUNCOP_1,
CARD_1, TREES_1, FUNCT_1, QC_LANG1, INCSP_1, GROUP_1, ARYTM_1, BINOP_1,
MATRIX_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1, STRUCT_0,
RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, BINOP_1,
FINSEQOP, RLVECT_1, VECTSP_1, CARD_1;
constructors BINOP_1, FINSEQOP, VECTSP_1, XREAL_0, XCMPLX_0, MEMBERED,
XBOOLE_0;
clusters FINSEQ_1, VECTSP_1, STRUCT_0, FINSEQ_2, RELSET_1, GROUP_1, ARYTM_3,
RELAT_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, RLVECT_1;
theorems FINSEQ_1, FINSEQ_2, FINSEQ_3, TARSKI, FUNCOP_1, FUNCT_1, FUNCT_2,
ZFMISC_1, NAT_1, BINOP_1, REAL_1, RLVECT_1;
schemes FINSEQ_1, FUNCT_2, BINOP_1, FINSEQ_2;
begin
reserve x,y,z,y1,y2 for set,
i,j,k,l,n,m for Nat,
D for non empty set,
K for non empty doubleLoopStr,
s,t,v for FinSequence,
a,a1,a2,b1,b2,d for Element of D,
p,p1,p2,q,r for FinSequence of D,
F for add-associative right_zeroed right_complementable Abelian
(non empty doubleLoopStr);
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 st s=x & len s = n;
end;
definition
cluster tabular FinSequence;
existence
proof
take M={},0;
let x;
assume x in rng M;
hence thesis;
end;
end;
theorem
Th1: <*<*d*>*> is tabular
proof
A1: rng <*<*d*>*> = {<*d*>} by FINSEQ_1:55;
take n = 1; let x; assume x in rng <*<*d*>*>;
then x = <*d*> & len <*d*> = n by A1,FINSEQ_1:56,TARSKI:def 1;
hence thesis;
end;
theorem Th2:
m |-> (n |-> x) is tabular
proof
set s=m |-> (n |-> x);
take n;
let z;
assume A1:z in rng s;
s=Seg m --> (n |-> x) by FINSEQ_2:def 2;
then A2: rng s c= {n |-> x} by FUNCOP_1:19;
take t=n|->x;
thus z=t & len t =n by A1,A2,FINSEQ_2:69,TARSKI:def 1;
end;
theorem Th3:
for s holds <*s*> is tabular
proof
let s;
take len s;
let x;
assume x in rng <*s*>;
then A1:x in { s} by FINSEQ_1:55;
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 that A1:len s1 =n and
A2:len s2 =n;
now take n;
let x;
assume x in rng (<*s1,s2*>);
then A3: x in { s1,s2} by FINSEQ_2:147;
then reconsider r=x as FinSequence by TARSKI:def 2;
take r;
thus x= r & len r=n by A1,A2,A3,TARSKI:def 2;
end;
hence thesis by Def1;
end;
theorem Th5: {} is tabular
proof
now take n=0;
let x;
assume x in rng ({});
hence ex t st t=x & len t=n;
end;
hence thesis by Def1;
end;
theorem <*{},{}*> is tabular
proof
len {} =0 by FINSEQ_1:25;
hence thesis by Th4;
end;
theorem <*<*a1*>,<*a2*>*> is tabular
proof
len <*a1*>=1 & len <*a2*>=1 by FINSEQ_1:56;
hence thesis by Th4;
end;
theorem <*<*a1,a2*>,<*b1,b2*>*> is tabular
proof
len <*a1,a2*>=2 & len <*b1,b2*>=2 by FINSEQ_1:61;
hence thesis by Th4;
end;
definition let f be Relation;
attr f is empty-yielding means
for s being set st s in rng f holds Card s = 0;
end;
definition
let D be set;
cluster tabular 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;
definition
let D be non empty set;
cluster non empty-yielding Matrix of D;
existence
proof consider d be Element of D;
A1: rng <*<*d*>*>= {<*d*>} & <*d*> in D* by FINSEQ_1:55,def 11;
then rng <*<*d*>*> c= D* by ZFMISC_1:37;
then reconsider p = <*<*d*>*> as FinSequence of D* by FINSEQ_1:def 4;
reconsider p as tabular FinSequence of D* by Th1;
reconsider s = <*d*> as FinSequence;
take p,s; thus s in rng p by A1,TARSKI:def 1;
thus len s <> 0 by FINSEQ_1:56;
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 being Nat 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;
A3: rng s c= D* by FINSEQ_1:def 4;
consider v such that A4:v=x & len v=n by A1,A2;
reconsider p=v as FinSequence of D by A2,A3,A4,FINSEQ_1:def 11;
take p;
thus thesis by 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;
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 s is Matrix of D by A6,FINSEQ_1:def 4;
end;
definition let D,m,n;
mode Matrix of m,n,D -> Matrix of D means:
Def3:
len it = m & for p st p in rng it holds len p = n;
existence
proof consider a;
reconsider
d= n |-> a as Element of D* by FINSEQ_1:def 11;
reconsider
M= m |-> d as FinSequence of (D)*;
M is Matrix of D
proof
ex n st for x st x in rng M ex p st
x =p & len p = n
proof
take n;
let x;
assume A1:x in rng M;
M=Seg m --> (n |-> a) by FINSEQ_2:def 2;
then A2: rng M c= {n |->a} by FUNCOP_1:19;
reconsider p=n |-> a as FinSequence of D;
take p;
thus x=p & len p =n by A1,A2,FINSEQ_2:69,TARSKI:def 1;
end;
hence thesis by Th9;
end;
then reconsider M as Matrix of D;
take M;
thus len M = m by FINSEQ_2:69;
let p;
assume A3:p in rng M;
M=Seg m --> (n |-> a) by FINSEQ_2:def 2;
then rng M c= {n |-> a} by FUNCOP_1:19;
then p = n |-> a by A3,TARSKI:def 1;
hence len p =n by FINSEQ_2:69;
end;
end;
definition let D,n;
mode Matrix of n,D is Matrix of n,n,D;
end;
definition let K be non empty 1-sorted;
mode Matrix of K is Matrix of the carrier of K;
let n;
mode Matrix of n,K is Matrix of n,n,the carrier of K;
let m;
mode Matrix of n,m,K is Matrix of n,m,the carrier of K;
end;
theorem Th10:
m |-> (n |-> a) is Matrix of m,n,D
proof
reconsider d= n |-> a as Element of D* by FINSEQ_1:def 11;
reconsider M= m |-> d as FinSequence of D*;
reconsider M as Matrix of D by Th2;
M is Matrix of m,n,D
proof
thus len M = m by FINSEQ_2:69;
let p;
assume A1:p in rng M;
M=Seg m --> (n |-> a) by FINSEQ_2:def 2;
then rng M c= {n |-> a} by FUNCOP_1:19;
then p = n |-> a by A1,TARSKI:def 1;
hence len p =n by FINSEQ_2:69;
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 p' = p as Element of (D)* by FINSEQ_1:def 11;
(<*p'*>) is tabular by Th3;
then reconsider M = <*p*> as Matrix of D;
M is Matrix of 1,len p,D
proof
thus len M = 1 by FINSEQ_1:56;
let q;
assume q in rng M;
then q in { p } by FINSEQ_1:55;
hence len q = len p 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;
assume that A1:len p1 =n and
A2:len p2 =n;
reconsider q1 = p1,q2 = p2 as Element of (D)* by FINSEQ_1:def 11;
reconsider M = <*q1,q2*> as FinSequence of (D)*
by FINSEQ_2:15;
reconsider M as Matrix of D by A1,A2,Th4;
M is Matrix of 2,n,D
proof
thus len M = 2 by FINSEQ_1:61;
let r;
assume r in rng M;
then r in { p1,p2 } by FINSEQ_2:147;
hence len r = n by A1,A2,TARSKI:def 2;
end;
hence thesis;
end;
theorem Th13: {} is Matrix of 0,m,D
proof
reconsider M ={} as FinSequence of D* by FINSEQ_1:29;
M is tabular by Th5;
then reconsider M = {} as Matrix of D;
M is Matrix of 0,m,D
proof
thus len M =0 by FINSEQ_1:25;
let p;
assume p in rng M;
hence thesis by FINSEQ_1:27;
end;
hence thesis;
end;
theorem <*{}*> is Matrix of 1,0,D
proof
A1: {} is FinSequence of D by FINSEQ_1:29;
len {} =0 by FINSEQ_1:25;
hence <*{}*> is Matrix of 1,0,D by A1,Th11;
end;
theorem <*<*a*>*> is Matrix of 1,D
proof
len <*a*> =1 by FINSEQ_1:56;
hence thesis by Th11;
end;
theorem <*{},{}*> is Matrix of 2,0,D
proof
A1:{} is FinSequence of D by FINSEQ_1:29;
len {}=0 by FINSEQ_1:25;
hence thesis by A1,Th12;
end;
theorem <*<*a1,a2*>*> is Matrix of 1,2,D
proof
A1: <*a1,a2*> is FinSequence of D by FINSEQ_2:15;
len <*a1,a2*> =2 by FINSEQ_1:61;
hence thesis by A1,Th11;
end;
theorem <*<*a1*>,<*a2*>*> is Matrix of 2,1,D
proof
len <*a1*>=1 & len <*a2*>=1 by FINSEQ_1:56;
hence thesis by Th12;
end;
theorem <*<*a1,a2*>,<*b1,b2*>*> is Matrix of 2,D
proof
A1:<*a1,a2*> is FinSequence of D &
<*b1,b2*> is FinSequence of D by FINSEQ_2:15;
len <*a1,a2*>=2 & len <*b1,b2*>=2 by FINSEQ_1:61;
hence thesis by A1,Th12;
end;
reserve M,M1,M2 for Matrix of D;
definition let M be tabular FinSequence;
func width M -> Nat means:
Def4:
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,s st s in rng M & len s = n
proof
assume len M > 0;
then M <> {} by FINSEQ_1:25;
then A1:rng M <>{} by FINSEQ_1:27;
consider n being Nat such that
A2: for x st x in rng M ex s st s=x & len s = n by Def1;
take n;
consider x being Element of rng M;
consider s such that A3:s=x & len s = n by A1,A2;
take s;
thus thesis by A1,A3;
end;
thus not len M > 0 implies ex n st n = 0;
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;
consider n such that A4:for x st x in rng M ex s st s=x & len s=n
by Def1;
given s such that A5:s in rng M and A6:len s = n1;
given p be FinSequence such that A7:p in rng M and A8:len p=n2;
A9: ex s1 be FinSequence st s1=s & len s1 =n by A4,A5;
ex p1 be FinSequence st p1=p & len p1 = n by A4,A7;
hence thesis by A6,A8,A9;
end;
thus not len M > 0 & n1 = 0 & n2 = 0 implies n1 = n2;
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
assume A2: M is Matrix of len M, n, D;
consider s such that A3:s in rng M & len s=width M by A1,Def4;
rng M c= D* by FINSEQ_1:def 4;
then reconsider q=s as FinSequence of D by A3,FINSEQ_1:def 11;
len q= n by A2,A3,Def3;
hence n = width M by A3;
end;
assume n=width M;
then for p st p in rng M holds len p=n by A1,Def4;
hence M is Matrix of len M,n,D by Def3;
end;
definition let M be tabular FinSequence;
func Indices M -> set equals :Def5:
[: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 :Def6:
ex p being FinSequence of D st p= M.i & it =p.j;
existence
proof
[i,j] in [:dom M,Seg width M:] by A1,Def5;
then A2:i in dom M & j in Seg width M by ZFMISC_1:106;
then A3: M.i in rng M by FUNCT_1:def 5;
rng M c= D* by FINSEQ_1:def 4;
then reconsider p=M.i as FinSequence of D by A3,FINSEQ_1:def 11;
rng M <> {} by A2,FUNCT_1:12;
then M<> {} by FINSEQ_1:27;
then len M <> 0 & len M >= 0 by FINSEQ_1:25,NAT_1:18;
then len M > 0 by REAL_1:def 5;
then consider s such that
A4: s in rng M and
A5: len s = width M by Def4;
consider n being Nat such that
A6: for x st x in rng M ex t st t=x & len t = n by Def1;
A7: ex t st s = t & len t = n by A4,A6;
ex v st p = v & len v = n by A3,A6;
then j in dom p by A2,A5,A7,FINSEQ_1:def 3;
then p.j in rng p & rng p c=D by FINSEQ_1:def 4,FUNCT_1:def 5;
then reconsider a=p.j as Element of D;
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:31;
for k st k in dom M1 holds M1.k = M2.k
proof
let k;
assume A5:k in dom M1;
then A6:M1.k in rng M1 & M2.k in rng M2 by A4,FUNCT_1:def 5;
A7: rng M1 c=(D)* & rng M2 c=(D)* by FINSEQ_1:def 4;
then reconsider p = M1.k as FinSequence of D by A6,FINSEQ_1:def 11;
rng M1 <> {} by A5,FUNCT_1:12;
then M1 <> {} by FINSEQ_1:27;
then len M1 <> 0 & len M1 >= 0 by FINSEQ_1:25,NAT_1:18;
then A8:len M1 > 0 by REAL_1:def 5;
then M1 is Matrix of len M1,width M1,D by Th20;
then A9:len p = width M1 by A6,Def3;
reconsider q = M2.k as FinSequence of D
by A6,A7,FINSEQ_1:def 11;
M2 is Matrix of len M1,width M1,D by A1,A2,A8,Th20;
then A10:len q = width M1 by A6,Def3;
for l st 1 <= l & l <= len p holds p.l = q.l
proof let l;
assume 1 <= l & l <= len p;
then A11:l in Seg width M1 by A9,FINSEQ_1:3;
then l in dom p & l in dom q by A9,A10,FINSEQ_1:def 3;
then A12: p.l in rng p & rng p c= D & q.l in rng q & rng q c= D
by FINSEQ_1:def 4,FUNCT_1:def 5;
then reconsider a = p.l as Element of D;
reconsider b = q.l as Element of D by A12;
[k,l] in [:dom M1,Seg width M1:] &
[k,l] in [:dom M2,Seg width M2:] by A2,A4,A5,A11,ZFMISC_1:106;
then A13:[k,l] in Indices M1 & [k,l] in Indices M2 by Def5;
then M1*(k,l)=a & M2*(k,l)= b by Def6;
hence thesis by A3,A13;
end;
hence M1.k =M2.k by A9,A10,FINSEQ_1:18;
end;
hence thesis by A4,FINSEQ_1:17;
end;
scheme MatrixLambda { D() -> non empty set, n() -> Nat, 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,set] 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,y1,y2 st k in Seg n() & P[k,y1] & P[k,y2] holds y1=y2
proof
let k,y1,y2;
assume k in Seg n();
given p1 being FinSequence such that A2:y1 =p1 and A3:len p1 =m() and
A4:for i st i in Seg m() holds p1.i =f(k,i);
given p2 being FinSequence such that A5:y2 =p2 and A6:len p2 =m() and
A7:for i st i in Seg m() holds p2.i =f(k,i);
now let j; assume A8:j in Seg m();
then p1.j=f(k,j) by A4;
hence p1.j=p2.j by A7,A8;
end;
hence y1=y2 by A2,A3,A5,A6,FINSEQ_2:10;
end;
A9:for k st k in Seg n() ex y st P[k,y]
proof
let k;
assume k in Seg n();
deffunc F(Nat) = f(k,$1);
consider p being FinSequence such that
A10: len p =m() & for i st i in Seg m() holds p.i = F(i)
from SeqLambda;
reconsider y =p as set;
take y,p;
thus thesis by A10;
end;
consider M being FinSequence such that
A11:dom M = Seg n() and
A12:for k st k in Seg n() holds P[k,M.k] from SeqEx(A1,A9);
A13:len M = n() by A11,FINSEQ_1:def 3;
rng M c=D()*
proof
let x;
assume x in rng M;
then consider i such that
A14: i in dom M & M.i=x by FINSEQ_2:11;
consider p being FinSequence such that
A15: M.i=p & len p = m() & for j st j in Seg m() holds p.j = f(i,j)
by A11,A12,A14;
rng p c= D()
proof
let z;
assume z in rng p;
then consider k such that
A16:k in dom p and A17:p.k =z by FINSEQ_2:11;
k in Seg len p by A16,FINSEQ_1:def 3;
then z = f(i,k) by A15,A17;
hence thesis;
end;
then p is FinSequence of D() by FINSEQ_1:def 4;
hence x in D()* by A14,A15,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 such that A18:i in dom M and A19:M.i =x by FINSEQ_2:11;
consider p being FinSequence such that
A20: x=p & len p = m() & for j st j in Seg m() holds p.j = f(i,j)
by A11,A12,A18,A19;
rng p c= D()
proof
let z;
assume z in rng p;
then consider k such that
A21:k in dom p and A22:p.k =z by FINSEQ_2:11;
k in Seg len p by A21,FINSEQ_1:def 3;
then z = f(i,k) by A20,A22;
hence thesis;
end;
then reconsider p as FinSequence of D() by FINSEQ_1:def 4;
take p;
thus thesis by A20;
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 such that A23:i in dom M and A24:M.i =p by FINSEQ_2:11;
P[i,p] by A11,A12,A23,A24;
hence thesis;
end;
then reconsider M as Matrix of n(),m(),D() by A13,Def3;
take M;
let i,j;
assume A25:[i,j] in Indices M;
then A26: ex p being FinSequence of D() st p=M.i & M*(i,j)=p.j by Def6;
A27: Indices M = [:dom M, Seg width M:] by Def5;
then A28: i in Seg n() & j in Seg width M by A11,A25,ZFMISC_1:106;
then A29: 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 A12;
n() <> 0 & n() >= 0 by A11,A25,A27,FINSEQ_1:4,NAT_1:18,ZFMISC_1:106;
then n() > 0 by REAL_1:def 5;
then j in Seg m() by A13,A28,Th20;
hence thesis by A26,A29;
end;
scheme MatrixEx { D() -> non empty set, n() -> Nat, m() -> Nat,
P[set,set,set] } :
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
for i,j st [i,j] in [:Seg n(), Seg m():]
for x1,x2 being Element of D() st P[i,j,x1] & P[i,j,x2]
holds x1 = x2 and
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[set,set,set] 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 A3:x in Seg n() & y in Seg m();
then reconsider x'=x as Nat;
reconsider y'=y as Nat by A3;
[x',y'] in [:Seg n(),Seg m():] by A3,ZFMISC_1:106;
then consider z' being Element of D() such that
A4: P[x',y',z'] by A1;
reconsider z'' = z' as set;
take z'';
thus thesis by A4;
end;
consider f being Function of [:Seg n(),Seg m():],D()
such that
A5:for x,y st x in Seg n() & y in Seg m() holds Q[x,y,f.[x,y]]
from FuncEx2(A2);
defpred R[set,set] means
ex p being FinSequence st
$2=p & len p = m() & for i st i in Seg m() holds p.i = f.[$1,i];
A6: for k,y1,y2 st k in Seg n() & R[k,y1] & R[k,y2] holds y1=y2
proof
let k,y1,y2;
assume k in Seg n();
given p1 being FinSequence such that A7:y1 =p1 and A8:len p1 =m() and
A9:for i st i in Seg m() holds p1.i =f.[k,i];
given p2 being FinSequence such that A10:y2 =p2 and A11:len p2 =m() and
A12:for i st i in Seg m() holds p2.i =f.[k,i];
now let j; assume A13:j in Seg m();
then p1.j=f.[k,j] by A9;
hence p1.j=p2.j by A12,A13;
end;
hence y1=y2 by A7,A8,A10,A11,FINSEQ_2:10;
end;
A14:for k st k in Seg n() ex y st R[k,y]
proof
let k;
assume k in Seg n();
deffunc F(Nat) = f.[k,$1];
consider p being FinSequence such that
A15: len p =m() & for i st i in Seg m() holds p.i = F(i)
from SeqLambda;
reconsider y =p as set;
take y,p;
thus thesis by A15;
end;
consider M being FinSequence such that
A16:dom M = Seg n() and
A17:for k st k in Seg n() holds R[k,M.k] from SeqEx(A6,A14);
A18:len M = n() by A16,FINSEQ_1:def 3;
rng M c=D()*
proof
let x;
assume x in rng M;
then consider i such that
A19:i in Seg n() & M.i=x by A16,FINSEQ_2:11;
consider p being FinSequence such that
A20:M.i=p & len p = m() & for j st j in Seg m() holds p.j = f.[i,j]
by A17,A19;
rng p c= D()
proof
let z;
assume z in rng p;
then consider k such that
A21:k in dom p and A22:p.k =z by FINSEQ_2:11;
A23: k in Seg len p by A21,FINSEQ_1:def 3;
then A24:z = f.[i,k] by A20,A22;
[i,k] in [:Seg n(),Seg m():] by A19,A20,A23,ZFMISC_1:106;
hence thesis by A24,FUNCT_2:7;
end;
then p is FinSequence of D() by FINSEQ_1:def 4;
hence x in D()* by A19,A20,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 such that A25:i in dom M and A26:M.i =x by FINSEQ_2:
11;
consider p being FinSequence such that
A27:x=p & len p = m() & for j st j in Seg m() holds p.j =f.[i,j]
by A16,A17,A25,A26;
rng p c= D()
proof
let z;
assume z in rng p;
then consider k such that
A28:k in dom p and A29:p.k =z by FINSEQ_2:11;
A30: k in Seg len p by A28,FINSEQ_1:def 3;
then A31:z = f.[i,k] by A27,A29;
[i,k] in [:Seg n(),Seg m():] by A16,A25,A27,A30,ZFMISC_1:106;
hence thesis by A31,FUNCT_2:7;
end;
then reconsider p as FinSequence of D() by FINSEQ_1:def 4;
take p;
thus thesis by A27;
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 such that A32:i in dom M and A33:M.i =p by FINSEQ_2:
11;
R[i,p] by A16,A17,A32,A33;
hence thesis;
end;
then reconsider M as Matrix of n(),m(),D() by A18,Def3;
take M;
let i,j;
assume A34:[i,j] in Indices M;
then A35: ex p being FinSequence of D() st p=M.i & M*
(i,j)=p.j by Def6
;
A36: Indices M = [:dom M, Seg width M:] by Def5;
then A37: i in Seg n() & j in Seg width M by A16,A34,ZFMISC_1:106;
then A38: 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 A17;
n() <> 0 & n() >= 0 by A16,A34,A36,FINSEQ_1:4,NAT_1:18,ZFMISC_1:106;
then n() > 0 by REAL_1:def 5;
then A39: j in Seg m() by A18,A37,Th20;
then f.[i,j]=M*(i,j) by A35,A38;
hence thesis by A5,A37,A39;
end;
canceled;
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;
A1: Seg len M = dom M by FINSEQ_1:def 3;
A2:len M = 0 by Def3;
then width M = 0 by Def4;
then Indices M= [:Seg 0,Seg 0:] by A1,A2,Def5;
hence thesis by A2,Def4,FINSEQ_1:4,ZFMISC_1:113;
end;
theorem
Th24: 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;
A2: Seg len M = dom M by FINSEQ_1:def 3;
A3:len M = n by Def3;
then width M = m by A1,Th20;
hence thesis by A2,A3,Def5;
end;
theorem
Th25: 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: Seg len M = dom M by FINSEQ_1:def 3;
A2:len M =n by Def3;
A3: 0 <= n by NAT_1:18;
now per cases by A3,REAL_1:def 5;
case n =0;
hence width M = 0 by A2,Def4;
case n > 0;
hence width M= n by A2,Th20;
end;
hence thesis by A1,A2,Def5;
end;
theorem
Th26: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 Def3;
then dom M = Seg n by FINSEQ_1:def 3;
hence thesis by Def3,Def5;
end;
theorem
Th27: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 & len M2= n by Def3;
then A2: dom M1 = Seg n & dom M2 = Seg n by FINSEQ_1:def 3;
A3: 0 <= n by NAT_1:18;
now per cases by A3,REAL_1:def 5;
suppose n =0;
then width M1 = 0 & width M2 =0 by A1,Def4;
hence width M1= width M2;
suppose n > 0;
then width M1= m & width M2= m by A1,Th20;
hence width M1 = width M2;
end;
then Indices M1 =[:Seg n,Seg width M1:] & Indices M2=[:Seg n,Seg width M1:]
by A2,Def5;
hence thesis;
end;
theorem
Th28: 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;
assume A1:(for i,j st [i,j] in Indices M1 holds M1*(i,j) = M2*(i,j));
A2:len M1=n & len M2=n by Th26;
A3: 0 <= n by NAT_1:18;
now per cases by A3,REAL_1:def 5;
suppose n =0;
then width M1 = 0 & width M2 =0 by A2,Def4;
hence width M1= width M2;
suppose n > 0;
then width M1= m & width M2= m by A2,Th20;
hence width M1 = width M2;
end;
hence thesis by A1,A2,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 A1:[i,j] in Indices M1;
A2: Indices M1 =[:Seg n,Seg n:] by Th25;
[i,j] in [:Seg n,Seg n:] by A1,Th25;
then j in Seg n & i in Seg n by ZFMISC_1:106;
hence thesis by A2,ZFMISC_1:106;
end;
definition let D; let M be Matrix of D;
func M@ -> Matrix of D means
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 by NAT_1:19;
suppose A1:width M > 0;
A2: Seg len M = dom M by FINSEQ_1:def 3;
deffunc F(Nat,Nat) = M*($2,$1);
consider M1 being Matrix of width M,len M,D such that
A3: for i,j st [i,j] in Indices M1 holds M1*(i,j) = F(i,j)
from MatrixLambda;
A4:Indices M1=[:Seg width M,dom M:] by A1,A2,Th24;
A5:now let i,j;
A6:now assume [i,j] in Indices M1;
then [j,i] in [:dom M,Seg width M:] by A4,ZFMISC_1:107;
hence [j,i] in Indices M by Def5;
end;
now assume [j,i] in Indices M;
then [j,i] in [:dom M,Seg width M:] by Def5;
then [i,j] in [:Seg width M,dom M:] by ZFMISC_1:107;
hence [i,j] in Indices M1 by A1,A2,Th24;
end;
hence [i,j] in Indices M1 iff [j,i] in Indices M by A6;
end;
reconsider M' = M1 as Matrix of D;
thus thesis
proof take M';
thus len M' = width M by A1,Th24;
thus for i,j holds [i,j] in Indices M' iff [j,i] in Indices M by A5
;
let i,j; assume [j,i] in Indices M;
then [i,j] in Indices M' by A5;
hence thesis by A3;
end;
suppose A7: width M =0;
reconsider M1 = {} as Matrix of D by Th13;
thus thesis
proof take M1;
A8: [:dom M,Seg width M:]={} by A7,FINSEQ_1:4,ZFMISC_1:113;
len M1 = 0 by FINSEQ_1:25;
then dom M1 = {} by FINSEQ_1:4,def 3;
then Indices M1=[:{},Seg width M1:] by Def5;
hence thesis by A7,A8,Def5,FINSEQ_1:25,ZFMISC_1:113;
end;
end;
hence thesis;
end;
uniqueness
proof
let M1,M2 be Matrix of D;
assume that A9:len M1 = width M and
A10:for i,j holds [i,j] in Indices M1 iff [j,i] in Indices M
and
A11:for i,j st [j,i] in Indices M holds M1*(i,j)=M*
(j,i) and
A12:len M2 = width M and
A13:for i,j holds [i,j] in Indices M2 iff [j,i] in Indices M
and
A14:for i,j st [j,i] in Indices M holds M2*(i,j)=M*(j,i);
now let x,y;
thus [x,y] in [:dom M1,Seg width M1:] implies
[x,y] in [:dom M2,Seg width M2:]
proof
assume A15:[x,y] in [:dom M1,Seg width M1:];
then A16:x in dom M1 & y in Seg width M1 by ZFMISC_1:106;
then reconsider i=x as Nat;
reconsider j=y as Nat by A16;
[i,j] in Indices M1 by A15,Def5;
then [j,i] in Indices M by A10;
then [i,j] in Indices M2 by A13;
hence thesis by Def5;
end;
thus [x,y] in [:dom M2,Seg width M2:] implies
[x,y] in [:dom M1,Seg width M1:]
proof
assume A17:[x,y] in [:dom M2,Seg width M2:];
then A18:x in dom M2 & y in Seg width M2 by ZFMISC_1:106;
then reconsider i=x as Nat;
reconsider j=y as Nat by A18;
[i,j] in Indices M2 by A17,Def5;
then [j,i] in Indices M by A13;
then [i,j] in Indices M1 by A10;
hence thesis by Def5;
end;
end;
then A19:[:dom M1,Seg width M1:] = [:dom M2,Seg width M2:]
by ZFMISC_1:108;
A20:len M1 = 0 implies len M2= 0 & width M1 = 0 & width M2 = 0 by A9,A12,
Def4;
A21:now assume A22:len M1 <> 0;
then Seg len M2 <> {} by A9,A12,FINSEQ_1:5;
then A23: dom M2 <> {} by FINSEQ_1:def 3;
now per cases;
suppose A24:Seg width M1 <> {};
Seg len M1 <> {} by A22,FINSEQ_1:5;
then dom M1 <> {} by FINSEQ_1:def 3;
then Seg width M1 = Seg width M2 by A19,A24,ZFMISC_1:134;
hence width M1 = width M2 by FINSEQ_1:8;
suppose A25: Seg width M1 = {};
then [:dom M2,Seg width M2:]= {} by A19,ZFMISC_1:113;
then Seg width M2 = {} by A23,ZFMISC_1:113;
hence width M1=width M2 by A25,FINSEQ_1:8;
end;
hence len M1=len M2 & width M1 =width M2 by A9,A12;
end;
now let i,j;
assume [i,j] in Indices M1;
then A26:[j,i] in Indices M by A10;
then M1*(i,j)=M*(j,i) by A11;
hence M1*(i,j)=M2*(i,j) by A14,A26;
end;
hence thesis by A20,A21,Th21;
end;
end;
definition let D,M,i;
func Line(M,i) -> FinSequence of D means:
Def8:
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);
thus ex f being FinSequence of D st len f = width M &
for j st j in Seg width M holds f.j = F(j) from SeqLambdaD;
end;
uniqueness
proof
let p1,p2 be FinSequence of D;
assume that A1:len p1=width M and
A2:for j st j in Seg width M holds p1.j = M*(i,j) and
A3:len p2=width M and
A4:for j st j in Seg width M holds p2.j = M*(i,j);
for j st j in Seg width M holds p1.j=p2.j
proof
let j;
assume j in Seg width M;
then p1.j = M*(i,j) & p2.j = M*(i,j) by A2,A4;
hence thesis;
end;
hence thesis by A1,A3,FINSEQ_2:10;
end;
func Col(M,i) -> FinSequence of D means:
Def9:
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);
A5: ex z being FinSequence of D st
len z = len M & for j st j in Seg len M holds z.j = F(j)
from SeqLambdaD;
Seg len M = dom M by FINSEQ_1:def 3;
hence thesis by A5;
end;
uniqueness
proof
let p1,p2 be FinSequence of D;
assume that A6:len p1= len M and
A7:for j st j in dom M holds p1.j = M*(j,i) and
A8:len p2= len M and
A9:for j st j in dom M holds p2.j = M*(j,i);
for j st j in Seg len M holds p1.j=p2.j
proof
let j;
assume j in Seg len M;
then j in dom M by FINSEQ_1:def 3;
then p1.j = M*(j,i) & p2.j = M*(j,i) by A7,A9;
hence thesis;
end;
hence thesis by A6,A8,FINSEQ_2:10;
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;
coherence
proof
len Line(M,i) = width M & Line(M,i) is Element of D*
by Def8,FINSEQ_1:def 11;
then Line(M,i) in { p where p is Element of D*:
len p = width M };
hence Line(M,i) is Element of (width M)-tuples_on D by FINSEQ_2:def 4;
end;
func Col(M,i) -> Element of (len M)-tuples_on D;
coherence
proof
len Col(M,i) = len M & Col(M,i) is Element of D*
by Def9,FINSEQ_1:def 11;
then Col(M,i) in { p where p is Element of D*:
len p = len M };
hence Col(M,i) is Element of (len M)-tuples_on D by FINSEQ_2:def 4;
end;
end;
reserve A,B for Matrix of n,K;
definition let K,n;
func n-Matrices_over K -> set equals:
Def10:
n-tuples_on (n-tuples_on the carrier of K);
coherence;
func 0.(K,n) -> Matrix of n,K equals:
Def11:
n |-> (n |-> 0.K);
coherence by Th10;
func 1.(K,n) -> Matrix of n,K means:
Def12:
(for i st [i,i] in Indices it holds it*(i,i) = 1_ K) &
for i,j st [i,j] in Indices it & i <> j holds it*(i,j) = 0.K;
existence
proof
defpred P[set,set,set] means
($1 = $2 implies $3 = 1_ K) & ($1 <> $2 implies $3 = 0.K);
A1: for i,j st [i,j] in [:Seg n, Seg n:]
for x1,x2 being Element of K st P[i,j,x1] & P[i,j,x2]
holds x1 = x2;
A2: for i,j st [i,j] in [:Seg n, Seg n:]
ex x being Element of K st P[i,j,x]
proof
let i,j;
assume [i,j] in [:Seg n, Seg n:];
(i = j implies P[i,j,1_ K]) &
(i <> j implies P[i,j,0.K]);
hence thesis;
end;
consider M being Matrix of n,K such that
A3: for i,j st [i,j] in Indices M holds P[i,j,M*(i,j)]
from MatrixEx(A1,A2);
take M;
thus thesis by A3;
end;
uniqueness
proof
let M1,M2 be Matrix of n,K;
A4:Indices M1 =Indices M2 by Th27;
assume that
A5: (for i st [i,i] in Indices M1 holds M1*(i,i) = 1_ K) and
A6:for i,j st [i,j] in Indices M1 & i <> j holds M1*(i,j) = 0.K and
A7:for i st [i,i] in Indices M2 holds M2*(i,i) = 1_ K and
A8:for i,j st [i,j] in Indices M2 & i <> j holds M2*(i,j) = 0.K;
A9:now let i,j;
assume A10:[i,j] in Indices M1;
A11:now
assume i=j;
then M1*(i,j)=1_ K & M2*(i,j)=1_ K by A4,A5,A7,A10;
hence M1*(i,j)=M2*(i,j);
end;
now assume i<>j;
then M1*(i,j)=0.K & M2*(i,j)=0.K by A4,A6,A8,A10;
hence M1*(i,j)=M2*(i,j);
end;
hence M1*(i,j)=M2*(i,j) by A11;
end;
len M1=n & width M1=n & len M2=n & width M2=n by Th25;
hence thesis by A9,Th21;
end;
let A;
func -A -> Matrix of n,K means:
Def13:
for i,j holds [i,j] in Indices A implies it*(i,j) = -(A*(i,j));
existence
proof
deffunc F(Nat,Nat) = -(A*($1,$2));
consider M being Matrix of n,K such that
A12:for i,j st [i,j] in Indices M holds M*(i,j) = F(i,j)
from MatrixLambda;
Indices A=[:Seg n,Seg n:] by Th25;
then A13:Indices A = Indices M by Th25;
take M;
thus thesis by A12,A13;
end;
uniqueness
proof
let M1,M2 be Matrix of n,K;
assume that A14:for i,j st [i,j] in Indices A holds M1*(i,j) =-(A*(i,j))
and
A15:for i,j st [i,j] in Indices A holds M2*(i,j) =-(A*
(i,j));
Indices M1=[:Seg n,Seg n:] & Indices M2=[:Seg n,Seg n:] by Th25;
then A16:Indices A = Indices M1 & Indices M1= Indices M2 by Th25;
now let i,j;
assume [i,j] in Indices A;
then M1*(i,j) = -(A*(i,j)) & M2*(i,j) = -(A*(i,j)) by A14,A15;
hence M1*(i,j)=M2*(i,j);
end;
hence thesis by A16,Th28;
end;
let B;
func A+B -> Matrix of n,K means:
Def14:
for i,j holds [i,j] in Indices A implies it*(i,j) = A*(i,j) + B*(i,j);
existence
proof
deffunc F(Nat,Nat) = A*($1,$2) + B*($1,$2);
consider M being Matrix of n,K such that
A17: for i,j st [i,j] in Indices M holds M*(i,j)= F(i,j)
from MatrixLambda;
Indices A=[:Seg n,Seg n:] by Th25;
then A18:Indices A = Indices M by Th25;
take M;
thus thesis by A17,A18;
end;
uniqueness
proof let M1,M2 be Matrix of n,K;
assume that
A19:for i,j st [i,j] in Indices A holds M1*(i,j)=A*(i,j) + B*
(i,j)
and A20:
for i,j st [i,j] in Indices A holds M2*(i,j) = A*(i,j) + B*(i,j);
Indices M1=[:Seg n,Seg n:] & Indices M2=[:Seg n,Seg n:] by Th25;
then A21:Indices A = Indices M1 & Indices M1= Indices M2 by Th25;
now let i,j;
assume [i,j] in Indices A;
then M1*(i,j)=(A*(i,j) + B*(i,j)) & M2*(i,j)=(A*(i,j) + B*
(i,j)) by A19,A20;
hence M1*(i,j)=M2*(i,j);
end;
hence thesis by A21,Th28;
end;
end;
definition let K,n;
cluster n-Matrices_over K -> non empty;
coherence
proof
n-Matrices_over K= n-tuples_on (n-tuples_on the carrier of K) by Def10;
hence thesis;
end;
end;
theorem Th30: [i,j] in Indices (0.(K,n)) implies (0.(K,n))*(i,j)= 0.K
proof
assume A1:[i,j] in Indices (0.(K,n));
then [i,j] in [:Seg n,Seg n:] by Th25;
then A2:i in Seg n & j in Seg n by ZFMISC_1:106;
(0.(K,n))=n |->(n |-> 0.K) by Def11;
then A3:(0.(K,n)).i= n |-> 0.K by A2,FINSEQ_2:70;
(n |-> 0.K).j= 0.K by A2,FINSEQ_2:70;
hence (0.(K,n))*(i,j)=0.K by A1,A3,Def6;
end;
theorem Th31:x is Element of n-Matrices_over K iff
x is Matrix of n,K
proof
A1:n-Matrices_over K=(n-tuples_on (n-tuples_on the carrier of K))
by Def10;
thus x is Element of (n-Matrices_over K) implies
x is Matrix of n,K
proof
assume x is Element of (n-Matrices_over K);
then reconsider x as Element of
n-tuples_on (n-tuples_on the carrier of K) by Def10;
A2:len x=n by FINSEQ_2:109;
ex m st for y st y in rng x ex q being FinSequence of the carrier of
K
st y=q & len q =m
proof take n;let y;
assume A3:y in rng x;
rng x c= (n-tuples_on the carrier of K) by FINSEQ_1:def 4;
then reconsider q=y as Element of n-tuples_on the carrier of K
by A3;
reconsider q as FinSequence of the carrier of K;
take q;
thus thesis by FINSEQ_2:109;
end;
then reconsider x as Matrix of the carrier of K by Th9;
for q be FinSequence of the carrier of K st q in rng x holds len q=
n
proof
let q be FinSequence of the carrier of K;
assume A4:q in rng x;
rng x c= n-tuples_on the carrier of K by FINSEQ_1:def 4;
then reconsider q as Element of n-tuples_on the carrier of K by A4;
len q=n by FINSEQ_2:109;
hence thesis;
end;
hence thesis by A2,Def3;
end;
assume x is Matrix of n,K;
then reconsider x as Matrix of n,K;
A5:len x = n & for p be FinSequence of the carrier of K
st p in rng x holds len p = n by Def3;
reconsider x as FinSequence of (the carrier of K)*;
reconsider x as Element of n-tuples_on ((the carrier of K)*)
by A5,FINSEQ_2:110;
rng x c= n-tuples_on (the carrier of K)
proof let y;
assume A6:y in rng x;
rng x c= (the carrier of K)* by FINSEQ_1:def 4;
then reconsider p=y as FinSequence of (the carrier of K)
by A6,FINSEQ_1:def 11;
len p =n by A6,Def3;
then p is Element of n-tuples_on (the carrier of K)
by FINSEQ_2:110;
hence thesis;
end;
then x is FinSequence of
(n-tuples_on the carrier of K) by FINSEQ_1:def 4;
hence thesis by A1,A5,FINSEQ_2:110;
end;
definition let K,n;
mode Diagonal of n,K -> Matrix of n,K means
for i,j st [i,j] in Indices it & it*(i,j) <> 0.K holds i=j;
existence
proof
take 1.(K,n); thus thesis by Def12;
end;
end;
reserve A,A',B,B',C for Matrix of n,F;
theorem Th32: A + B = B + A
proof
A1:Indices A= Indices B & Indices A = Indices (A + B) by Th27;
now let i,j;
assume A2:[i,j] in Indices (A + B);
hence (A + B)*(i,j)=A*(i,j) + B*(i,j) by A1,Def14
.=(B + A)*(i,j) by A1,A2,Def14;
end;
hence thesis by Th28;
end;
theorem Th33: (A + B) + C = A + (B + C)
proof
A1:Indices A= Indices B & Indices A= Indices C by Th27;
A2:Indices A= Indices ((A + B) +C) & Indices A =Indices (A +(B + C)) by Th27;
A3:Indices A= Indices (A + B) & Indices A = Indices (B + C) by Th27;
now let i,j;
assume A4:[i,j] in Indices ((A + B) + C);
hence ((A + B)+C)*(i,j)=(A+B)*(i,j) + C*(i,j) by A2,A3,Def14
.=(A*(i,j) + B*(i,j)) + C*(i,j) by A2,A4,Def14
.=A*(i,j) + (B*(i,j) + C*(i,j)) by RLVECT_1:def 6
.=A*(i,j) + ( B + C)*(i,j) by A1,A2,A4,Def14
.=(A + ( B + C))*(i,j) by A2,A4,Def14;
end;
hence thesis by Th28;
end;
theorem Th34: A + 0.(F,n)= A
proof
A1:Indices A= Indices (A+0.(F,n)) by Th27;
A2:Indices A= Indices (0.(F,n)) by Th27;
now let i,j;
assume A3:[i,j] in Indices (A+ 0.(F,n));
hence (A+ 0.(F,n)) *(i,j)=A*(i,j) + 0.(F,n)*(i,j) by A1,Def14
.=A*(i,j) +0.F by A1,A2,A3,Th30
.=A*(i,j) by RLVECT_1:10;
end;
hence thesis by Th28;
end;
theorem Th35: A + (-A) = 0.(F,n)
proof
A1:Indices A= Indices (-A) & Indices A= Indices 0.(F,n) by Th27;
A2:Indices A= Indices (A + (-A)) by Th27;
now let i,j;
assume A3:[i,j] in Indices (A + (-A));
hence (A + (-A))*(i,j)=A*(i,j)+ (-A)*(i,j) by A2,Def14
.=A*(i,j)+ (-A*(i,j)) by A2,A3,Def13
.=0.F by RLVECT_1:def 10
.=(0.(F,n))*(i,j) by A1,A2,A3,Th30;
end;
hence thesis by Th28;
end;
definition let F,n;
func n-G_Matrix_over F -> strict AbGroup means
the carrier of it = n-Matrices_over F &
(for A,B holds (the add of it).(A,B) = A+B) &
the Zero of it = 0.(F,n);
existence
proof
defpred P[Element of n-Matrices_over F, Element of n-Matrices_over F,
Element of n-Matrices_over F]
means ex A,B st $1=A & $2=B & $3 = A + B;
A1:for a,b being Element of n-Matrices_over F
ex c being Element of n-Matrices_over F st P[a,b,c]
proof
let a,b be Element of (n-Matrices_over F);
reconsider A=a as Matrix of n,F by Th31;
reconsider B=b as Matrix of n,F by Th31;
reconsider c = A+B as Element of n-Matrices_over F by Th31;
take c;
thus thesis;
end;
consider h being BinOp of n-Matrices_over F such that
A2:for a,b being Element of n-Matrices_over F holds P[a,b,h.(a,b)]
from BinOpEx(A1);
A3:h.(A,B)=A+B
proof
A is Element of (n-Matrices_over F) &
B is Element of (n-Matrices_over F) by Th31;
then ex A',B' st A=A' & B=B' & h.(A,B)= A' + B' by A2;
hence thesis;
end;
A4:for a being Element of n-Matrices_over F
ex b being Element of n-Matrices_over F st ex A st a=A & b= -A
proof
let a be Element of n-Matrices_over F;
reconsider A=a as Matrix of n,F by Th31;
reconsider b=-A as Element of n-Matrices_over F by Th31;
take b;
thus thesis;
end;
reconsider A0=0.(F,n) as Element of n-Matrices_over F by Th31;
set G=LoopStr (# n-Matrices_over F,h,A0 #);
G is Abelian add-associative right_zeroed right_complementable
proof
thus G is Abelian
proof
let a,b be Element of G;
reconsider A=a,B=b as Matrix of n,F by Th31;
thus a+b=h.(A,B) by RLVECT_1:5 .=A+B by A3 .=B+A by Th32
.=h.(B,A) by A3 .=b+a by RLVECT_1:5;
end;
hereby let a,b,c be Element of G;
reconsider A=a,B=b,C=c as Matrix of n,F by Th31;
thus (a+b)+c =h.(a+b,c) by RLVECT_1:5 .=h.(h.(a,b),c) by RLVECT_1:5
.=h.(A+B,C) by A3 .=(A+B)+C by A3
.=A+(B+C) by Th33 .=h.(A,B+C) by A3
.=h.(a,h.(b,c)) by A3 .=h.(a,b+c) by RLVECT_1:5
.=a+(b+c) by RLVECT_1:5;
end;
hereby let a be Element of G;
reconsider A=a as Matrix of n,F by Th31;
thus a+ 0.G=h.(a,0.G) by RLVECT_1:5 .=h.(A,A0) by RLVECT_1:def 2
.=A + 0.(F,n) by A3 .=a by Th34;
end;
let a be Element of G;
consider b being Element of n-Matrices_over F such that
A5: ex A st a=A & b= -A by A4;
consider A such that A6:a=A & b= -A by A5;
reconsider b = -A as Element of G by A6;
take b;
thus a+b=h.(A,-A) by A6,RLVECT_1:5
.=A+-A by A3 .=A0 by Th35 .=0.G by RLVECT_1:def 2;
end;
then reconsider G as strict AbGroup;
take G;
thus thesis by A3;
end;
uniqueness
proof thus for G1,G2 being strict AbGroup st
(the carrier of G1 = n-Matrices_over F &
(for A,B holds (the add of G1).(A,B) = A+B) &
the Zero of G1 = 0.(F,n)) &
(the carrier of G2 = n-Matrices_over F &
(for A,B holds (the add of G2).(A,B) = A+B) &
the Zero of G2 = 0.(F,n)) holds G1=G2
proof let G1,G2 be strict AbGroup;
assume that
A7:the carrier of G1 = n-Matrices_over F and
A8:(for A,B holds (the add of G1).(A,B) = A+B) and
A9:the Zero of G1 = 0.(F,n) and
A10:the carrier of G2 = n-Matrices_over F and
A11:(for A,B holds (the add of G2).(A,B) = A+B) and
A12:the Zero of G2 = 0.(F,n);
now let a,b be Element of G1;
reconsider A = a, B = b as Matrix of n,F by A7,Th31;
thus (the add of G1).(a,b)= A+B by A8 .= (the add of G2).(a,b) by A11;
end;
hence G1 = G2 by A7,A9,A10,A12,BINOP_1:2;
end;
end;
end;