:: Block Diagonal Matrices
:: by Karol P\c{a}k
::
:: Received May 13, 2008
:: Copyright (c) 2008-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, VECTSP_1, SUBSET_1, XBOOLE_0, MATRIX_1, FINSEQ_1,
ALGSTR_0, RELAT_1, ARYTM_3, TARSKI, STRUCT_0, ZFMISC_1, ORDINAL4,
XXREAL_0, FUNCT_1, PARTFUN1, FINSEQ_3, CARD_1, ARYTM_1, FINSEQ_2, CARD_3,
GROUP_1, RFINSEQ, TREES_1, INCSP_1, MATRIX_3, SUPINF_2, LAPLACE,
MATRIX11, MESFUNC1, RVSUM_1, MATHMORP, VALUED_1, FVSUM_1, MATRIXJ1,
FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, NAT_1, RELAT_1, FUNCT_1,
PARTFUN1, FINSEQ_1, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1,
VECTSP_2, FINSEQ_2, MATRIX_0, MATRIX_1, FVSUM_1, NAT_D, GROUP_4,
MATRIX_3, MATRIX11, FINSEQOP, MATRIX13, LAPLACE, RFINSEQ,
WSIERP_1;
constructors VECTSP_2, GROUP_4, MATRIX11, MATRIX13, LAPLACE, RFINSEQ,
WSIERP_1, REAL_1, BINARITH, RELSET_1, FVSUM_1, MATRIX_1, NUMBERS,
RECDEF_1, MATRIX_3;
registrations XBOOLE_0, FINSET_1, STRUCT_0, VECTSP_1, ORDINAL1,
XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, FINSEQ_2, MATRIX13, XREAL_0,
VALUED_0, CARD_1, MATRIX_3, VECTSP_2;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI;
equalities FINSEQ_1, MATRIX_0, LAPLACE, MATRIX13, FVSUM_1;
expansions FINSEQ_1;
theorems CARD_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, FINSEQ_6, FINSEQOP,
FUNCT_1, FVSUM_1, GROUP_1, GROUP_4, LAPLACE, MATRIX_0, MATRIX_3,
MATRIX_9, MATRIX11, MATRIX13, MATRIX15, MATRIXR2, NAT_1, ORDINAL1,
PARTFUN1, POLYNOM3, PRGCOR_1, RELAT_1, RFINSEQ, RLVECT_1, RVSUM_1,
TARSKI, VECTSP_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ZFMISC_1,
MATRIX_4, FUNCT_2, FUNCOP_1, MATRIXR1, CARD_1, NAT_D, MATRIX_1;
schemes FINSEQ_1, FINSEQ_2, NAT_1, MATRIX_0;
begin :: Preliminaries
reserve i,j,m,n,k for Nat,
x,y for set,
K for Field,
a,a1,a2 for Element of K,
D for non empty set,
d,d1,d2 for Element of D,
M,M1,M2 for (Matrix of D),
A,A1,A2,B1,B2 for (Matrix of K),
f,g for FinSequence of NAT;
Lm1: for K be non empty addLoopStr for p1,p2 be FinSequence of K holds dom (p1+
p2)=(dom p1)/\(dom p2)
proof
let K be non empty addLoopStr;
let p1,p2 be FinSequence of K;
A1: rng p2 c= the carrier of K by FINSEQ_1:def 4;
rng p1 c= the carrier of K by FINSEQ_1:def 4;
then [:rng p1,rng p2:]c=[:the carrier of K,the carrier of K:]by A1,
ZFMISC_1:96;
then [:rng p1, rng p2:] c= dom (the addF of K) by FUNCT_2:def 1;
hence thesis by FUNCOP_1:69;
end;
theorem Th1:
for K be non empty addLoopStr for f1,f2,g1,g2 be FinSequence of K
st len f1 = len f2 holds (f1+f2)^(g1+g2)=(f1^g1)+(f2^g2)
proof
let K be non empty addLoopStr;
let f1,f2,g1,g2 be FinSequence of K such that
A1: len f1 = len f2;
A2: dom f1=dom f2 by A1,FINSEQ_3:29;
A3: dom g2=Seg len g2 by FINSEQ_1:def 3;
A4: dom g1=Seg len g1 by FINSEQ_1:def 3;
A5: dom (f1^g1)=Seg(len f1+len g1) by FINSEQ_1:def 7;
A6: dom (f2^g2)=Seg(len f2+len g2) by FINSEQ_1:def 7;
A7: dom (g1+g2)=dom g1/\dom g2 by Lm1;
A8: dom (f1+f2)=dom f1/\dom f2 by Lm1;
then
A9: len (f1+f2)=len f1 by A2,FINSEQ_3:29;
A10: dom((f1^g1)+(f2^g2))=dom (f1^g1)/\dom (f2^g2) by Lm1;
A11: now
per cases;
suppose
A12: len g1<=len g2;
then Seg len g1 c= Seg len g2 by FINSEQ_1:5;
then dom (g1+g2)=dom g1 by A7,A4,A3,XBOOLE_1:28;
then
A13: len (g1+g2)=len g1 by FINSEQ_3:29;
len f1+len g1 <= len f2+len g2 by A1,A12,XREAL_1:7;
then dom (f1^g1) c= dom (f2^g2) by A5,A6,FINSEQ_1:5;
then dom ((f1^g1)+(f2^g2))=dom (f1^g1) by A10,XBOOLE_1:28;
hence dom ((f1+f2)^(g1+g2))=dom ((f1^g1)+(f2^g2)) by A9,A5,A13,
FINSEQ_1:def 7;
end;
suppose
A14: len g1> len g2;
then Seg len g2 c= Seg len g1 by FINSEQ_1:5;
then dom (g1+g2)=dom g2 by A7,A4,A3,XBOOLE_1:28;
then
A15: len (g1+g2)=len g2 by FINSEQ_3:29;
len f1+len g1 > len f2+len g2 by A1,A14,XREAL_1:8;
then dom (f2^g2) c= dom (f1^g1) by A5,A6,FINSEQ_1:5;
then dom ((f1^g1)+(f2^g2))=dom (f2^g2) by A10,XBOOLE_1:28;
hence dom ((f1+f2)^(g1+g2))=dom ((f1^g1)+(f2^g2)) by A1,A9,A6,A15,
FINSEQ_1:def 7;
end;
end;
now
let i such that
A16: i in dom ((f1+f2)^(g1+g2));
now
per cases by A16,FINSEQ_1:25;
suppose
A17: i in dom (f1+f2);
then
A18: f2.i=(f2^g2).i by A8,A2,FINSEQ_1:def 7;
A19: f2/.i=f2.i by A8,A2,A17,PARTFUN1:def 6;
A20: f1.i=(f1^g1).i by A8,A2,A17,FINSEQ_1:def 7;
A21: f1/.i=f1.i by A8,A2,A17,PARTFUN1:def 6;
thus ((f1+f2)^(g1+g2)).i = (f1+f2).i by A17,FINSEQ_1:def 7
.= f1/.i + f2/.i by A17,A21,A19,FVSUM_1:17
.= ((f1^g1)+(f2^g2)).i by A11,A16,A21,A19,A20,A18,FVSUM_1:17;
end;
suppose
ex n st n in dom (g1+g2) & i=len (f1+f2) + n;
then consider n such that
A22: n in dom (g1+g2) and
A23: i=len (f1+f2)+n;
A24: n in dom g1 by A7,A22,XBOOLE_0:def 4;
then
A25: (f1^g1).i=g1.n by A9,A23,FINSEQ_1:def 7;
A26: g1.n=g1/.n by A24,PARTFUN1:def 6;
A27: n in dom g2 by A7,A22,XBOOLE_0:def 4;
then
A28: (f2^g2).i=g2.n by A1,A9,A23,FINSEQ_1:def 7;
A29: g2.n=g2/.n by A27,PARTFUN1:def 6;
thus ((f1+f2)^(g1+g2)).i = (g1+g2).n by A22,A23,FINSEQ_1:def 7
.= g1/.n + g2/.n by A22,A26,A29,FVSUM_1:17
.= ((f1^g1)+(f2^g2)).i by A11,A16,A26,A29,A25,A28,FVSUM_1:17;
end;
end;
hence ((f1+f2)^(g1+g2)).i=((f1^g1)+(f2^g2)).i;
end;
hence thesis by A11,FINSEQ_1:13;
end;
theorem Th2:
for f,g be FinSequence of D st i in dom f holds Del(f^g,i) = Del( f,i)^g
proof
let f,g be FinSequence of D such that
A1: i in dom f;
set Df=Del(f,i);
consider m such that
A2: len f = m + 1 and
A3: len Df = m by A1,FINSEQ_3:104;
set Dg=Df^g;
set fg=f^g;
set Dfg=Del(fg,i);
A4: Seg len fg=dom fg by FINSEQ_1:def 3;
A5: len fg=len f+len g by FINSEQ_1:22;
then len f <=len fg by NAT_1:12;
then
A6: Seg len f c= Seg len fg by FINSEQ_1:5;
A7: len fg=len g+m+1 by A2,A5;
A8: Seg len f=dom f by FINSEQ_1:def 3;
A9: now
let j such that
A10: 1<=j and
A11: j<=m+len g;
now
per cases;
suppose
A12: j<i;
i<=len f by A1,FINSEQ_3:25;
then
A13: j<len f by A12,XXREAL_0:2;
then
A14: j in dom f by A10,FINSEQ_3:25;
j<=m by A2,A13,NAT_1:13;
then
A15: j in dom Df by A3,A10,FINSEQ_3:25;
thus Dfg.j = fg.j by A12,FINSEQ_3:110
.= f.j by A14,FINSEQ_1:def 7
.= Df.j by A12,FINSEQ_3:110
.= Dg.j by A15,FINSEQ_1:def 7;
end;
suppose
A16: j>=i;
now
per cases;
suppose
A17: j<=m;
A18: 0+1<=j+1 by XREAL_1:7;
j+1<=len f by A2,A17,XREAL_1:7;
then
A19: j+1 in dom f by A18,FINSEQ_3:25;
A20: j in dom Df by A3,A10,A17,FINSEQ_3:25;
thus Dfg.j = fg.(j+1) by A1,A6,A8,A4,A7,A11,A16,FINSEQ_3:111
.= f.(j+1) by A19,FINSEQ_1:def 7
.= Df.j by A1,A2,A16,A17,FINSEQ_3:111
.= Dg.j by A20,FINSEQ_1:def 7;
end;
suppose
A21: j>m;
then j>=len f by A2,NAT_1:13;
then j+1>len f by NAT_1:13;
then reconsider jL=j+1-len f as Element of NAT by NAT_1:21;
j+1<=m+len g+1 by A11,XREAL_1:7;
then jL+len f<=len f+len g by A2;
then
A22: jL<=len g by XREAL_1:8;
jL<>0 by A2,A21;
then jL>=1 by NAT_1:14;
then
A23: jL in dom g by A22,FINSEQ_3:25;
thus Dfg.j = fg.(jL+len f) by A1,A6,A8,A4,A7,A11,A16,FINSEQ_3:111
.= g.jL by A23,FINSEQ_1:def 7
.= Dg.(m+jL) by A3,A23,FINSEQ_1:def 7
.= Dg.j by A2;
end;
end;
hence Dg.j=Dfg.j;
end;
end;
hence Dg.j=Dfg.j;
end;
A24: len Dg=len Df+len g by FINSEQ_1:22;
len Dfg=m+len g by A1,A6,A8,A4,A7,FINSEQ_3:109;
hence thesis by A3,A24,A9;
end;
theorem Th3:
for f,g be FinSequence of D st i in dom g holds Del(f^g,i+len f)= f^Del(g,i)
proof
let f,g be FinSequence of D such that
A1: i in dom g;
set Dg=Del(g,i);
consider m such that
A2: len g = m + 1 and
A3: len Dg = m by A1,FINSEQ_3:104;
set fD=f^Dg;
set iL=i+len f;
set fg=f^g;
set Dfg=Del(fg,iL);
A4: dom fg=Seg len fg by FINSEQ_1:def 3;
A5: len fg=len f+len g by FINSEQ_1:22;
then
A6: len fg=m+len f+1 by A2;
A7: i in Seg len g by A1,FINSEQ_1:def 3;
then
A8: i>0;
A9: now
let j such that
A10: 1<=j and
A11: j<=m+len f;
now
per cases;
suppose
A12: j<=len f;
then
A13: j in dom f by A10,FINSEQ_3:25;
0+len f<iL by A8,XREAL_1:8;
then j<iL by A12,XXREAL_0:2;
hence Dfg.j = fg.j by FINSEQ_3:110
.= f.j by A13,FINSEQ_1:def 7
.= fD.j by A13,FINSEQ_1:def 7;
end;
suppose
A14: j>len f;
then reconsider jL=j-len f as Element of NAT by NAT_1:21;
A15: 1<=jL+1 by NAT_1:14;
jL+len f<=m+len f by A11;
then
A16: jL<=m by XREAL_1:6;
then jL+1<=len g by A2,XREAL_1:7;
then
A17: jL+1 in dom g by A15,FINSEQ_3:25;
jL<>0 by A14;
then
A18: jL>=1 by NAT_1:14;
then
A19: jL in dom Dg by A3,A16,FINSEQ_3:25;
jL<=len g by A2,A16,NAT_1:13;
then
A20: jL in dom g by A18,FINSEQ_3:25;
now
per cases;
suppose
A21: jL<i;
then jL+len f<iL by XREAL_1:8;
hence Dfg.j = fg.(jL+len f) by FINSEQ_3:110
.= g.jL by A20,FINSEQ_1:def 7
.= Dg.jL by A21,FINSEQ_3:110
.= fD.(jL+len f) by A19,FINSEQ_1:def 7
.= fD.j;
end;
suppose
A22: jL>=i;
then jL+len f>=iL by XREAL_1:7;
hence Dfg.j = fg.(jL+len f+1) by A5,A7,A4,A6,A11,FINSEQ_1:60
,FINSEQ_3:111
.= fg.((jL+1)+len f)
.= g.(jL+1) by A17,FINSEQ_1:def 7
.= Dg.jL by A1,A2,A16,A22,FINSEQ_3:111
.= fD.(jL+len f) by A19,FINSEQ_1:def 7
.=fD.j;
end;
end;
hence fD.j=Dfg.j;
end;
end;
hence fD.j=Dfg.j;
end;
A23: len fD=len f+len Dg by FINSEQ_1:22;
len Dfg=m+len f by A5,A7,A4,A6,FINSEQ_1:60,FINSEQ_3:109;
hence thesis by A3,A23,A9;
end;
theorem Th4:
i in Seg (n+1) implies Del((n+1) |->d,i)=n |-> d
proof
set n1=n+1;
set n1d=n1|->d;
set nd=n|->d;
set Dn=Del(n1d,i);
A1: len n1d=n1 by CARD_1:def 7;
A2: dom n1d=Seg len n1d by FINSEQ_1:def 3;
A3: len nd=n by CARD_1:def 7;
assume
A4: i in Seg (n+1);
A5: now
let j such that
A6: 1<=j and
A7: j<=n;
j<=n1 by A7,NAT_1:13;
then
A8: j in Seg n1 by A6;
A9: j in Seg n by A6,A7;
then
A10: j+1 in Seg (n+1) by FINSEQ_1:60;
now
per cases;
suppose
j<i;
hence Dn.j = n1d.j by FINSEQ_3:110
.= d by A8,FINSEQ_2:57
.= nd.j by A9,FINSEQ_2:57;
end;
suppose
j>=i;
hence Dn.j = n1d.(j+1) by A4,A1,A2,A7,FINSEQ_3:111
.= d by A10,FINSEQ_2:57
.= nd.j by A9,FINSEQ_2:57;
end;
end;
hence nd.j=Dn.j;
end;
len Dn=n by A4,A1,A2,FINSEQ_3:109;
hence thesis by A3,A5;
end;
theorem
Product (n|->a) = (power K).(a,n)
proof
defpred P[Nat] means Product ($1|->a) = (power K).(a,$1);
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
thus Product ((k+1) |->a) = (Product (k|->a)) * Product (1|->a) by
FVSUM_1:83
.= Product (k|->a)*Product<*a*> by FINSEQ_2:59
.= (power K).(a,k)*a by A2,GROUP_4:9
.= (power K).(a,k+1) by GROUP_1:def 7;
end;
0|->a=<*>(the carrier of K);
then Product (0|->a) = 1_K by GROUP_4:8
.= (power K).(a,0) by GROUP_1:def 7;
then
A3: P[0];
for k holds P[k] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
definition
let f;
let i be Nat such that
A1: i in Seg (Sum f);
func min(f,i) -> Element of NAT means
:Def1:
i <= Sum(f|it) & it in dom f & for j st i<=Sum (f|j) holds it <= j;
existence
proof
defpred P[Nat] means i<= Sum(f|$1) & $1>=1;
A2: f| (len f)=f by FINSEQ_1:58;
A3: i <= Sum f by A1,FINSEQ_1:1;
Sum f <> 0 by A1;
then
A4: len f>=1 by FINSEQ_1:20,RVSUM_1:72;
then
A5: ex k st P[k] by A3,A2;
consider k such that
A6: P[k] and
A7: for n st P[n] holds k<=n from NAT_1:sch 5(A5);
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
thus i<= Sum(f|k) by A6;
k<=len f by A4,A3,A2,A7;
hence k in dom f by A6,FINSEQ_3:25;
let j such that
A8: i<=Sum(f|j);
per cases;
suppose
j=0;
then f|j=<*>REAL;
hence thesis by A1,A8,RVSUM_1:72;
end;
suppose
j>0;
hence thesis by A7,A8,NAT_1:14;
end;
end;
uniqueness
proof
let n1,n2 be Element of NAT such that
A9: i <= Sum(f|n1) and
n1 in dom f and
A10: for j st i<=Sum (f|j) holds n1 <= j and
A11: i <= Sum(f|n2) and
n2 in dom f and
A12: for j st i<=Sum (f|j) holds n2 <= j;
A13: n2<=n1 by A9,A12;
n1<=n2 by A10,A11;
hence thesis by A13,XXREAL_0:1;
end;
end;
theorem
i in dom f & f.i <> 0 implies min(f,Sum(f|i)) = i
proof
assume that
A1: i in dom f and
A2: f.i<>0;
A3: i<=len f by A1,FINSEQ_3:25;
then
A4: len (f|i) =i by FINSEQ_1:59;
1<=i by A1,FINSEQ_3:25;
then
A5: i in dom (f|i) by A4,FINSEQ_3:25;
then Sum (f|i) >= (f|i).i by POLYNOM3:4;
then Sum(f|i)<>0 by A2,A5,FUNCT_1:47;
then
A6: Sum(f|i)>=1 by NAT_1:14;
A7: f| (len f) = f by FINSEQ_1:58;
Sum(f|i) <= Sum(f| (len f)) by A3,POLYNOM3:18;
then
A8: Sum(f|i) in Seg Sum f by A7,A6;
then
A9: min(f,Sum(f|i))<=i by Def1;
thus min(f,Sum(f|i))=i
proof
assume
A10: min(f,Sum(f|i))<>i;
then min(f,Sum(f|i))<i by A9,XXREAL_0:1;
then reconsider i1=i-1 as Element of NAT by NAT_1:20;
min(f,Sum(f|i))<i1+1 by A9,A10,XXREAL_0:1;
then min(f,Sum(f|i)) <=i1 by NAT_1:13;
then
A11: Sum(f|min(f,Sum(f|i)))<=Sum (f|i1) by POLYNOM3:18;
Sum(f|i) <= Sum(f|min(f,Sum(f|i))) by A8,Def1;
then
A12: Sum(f|i) <=Sum (f|i1) by A11,XXREAL_0:2;
f| (i1+1)=(f|i1)^<*f.i*> by A1,FINSEQ_5:10;
then
A13: Sum (f|i)=Sum (f|i1)+ f.i by RVSUM_1:74;
then Sum (f|i)>=Sum (f|i1) by NAT_1:11;
then Sum (f|i)=Sum (f|i1) by A12,XXREAL_0:1;
hence thesis by A2,A13;
end;
end;
theorem Th7:
i in Seg (Sum f) implies min(f,i)-'1 = min(f,i) - 1 & Sum(f| (min(
f,i)-'1))<i
proof
set F=min(f,i);
assume
A1: i in Seg (Sum f);
then F in dom f by Def1;
then 1<=F by FINSEQ_3:25;
hence
A2: F-'1=F-1 by XREAL_1:233;
assume Sum(f| (F-'1))>=i;
then F-'1>=F-0 by A1,Def1;
hence thesis by A2,XREAL_1:10;
end;
theorem Th8:
i in Seg (Sum f) implies min(f^g,i)=min(f,i)
proof
reconsider fg=f^g as FinSequence of NAT;
assume
A1: i in Seg Sum f;
then
A2: i<=Sum(f|min(f,i)) by Def1;
Sum fg=Sum f+Sum g by RVSUM_1:75;
then Sum fg>=Sum f+0 by XREAL_1:6;
then
A3: Seg Sum f c= Seg Sum fg by FINSEQ_1:5;
min(f,i) in dom f by A1,Def1;
then
A4: min(f,i)<=len f by FINSEQ_3:25;
then fg|min(f,i)=f|min(f,i) by FINSEQ_5:22;
then
A5: min(fg,i)<=min(f,i) by A1,A3,A2,Def1;
then fg|min(fg,i)=f|min(fg,i) by A4,FINSEQ_5:22,XXREAL_0:2;
then i<=Sum(f|min(fg,i)) by A1,A3,Def1;
then min(f,i)<=min(fg,i) by A1,Def1;
hence thesis by A5,XXREAL_0:1;
end;
theorem Th9:
i in Seg (Sum f +Sum g)\Seg Sum f implies min(f^g,i)=min(g,i-'Sum
f)+len f & i-'Sum f = i - Sum f
proof
reconsider fg=f^g as FinSequence of NAT;
assume
A1: i in Seg (Sum f +Sum g)\Seg Sum f;
then not i in Seg Sum f by XBOOLE_0:def 5;
then
A2: 1>i or i>Sum f;
A3: Sum fg=Sum f+Sum g by RVSUM_1:75;
then
A4: i in Seg Sum fg by A1,XBOOLE_0:def 5;
then reconsider j=i-Sum f as Element of NAT by A2,FINSEQ_1:1,NAT_1:21;
A5: i=j+Sum f;
fg| (len f+min(g,j))=f^(g|min(g,j)) by FINSEQ_6:14;
then
A6: Sum (fg| (len f+min(g,j)))=Sum f + Sum(g|min(g,j)) by RVSUM_1:75;
j<>0 by A4,A2,FINSEQ_1:1;
then
A7: j in Seg Sum g by A3,A4,A5,FINSEQ_1:61;
then j<=Sum(g|min(g,j)) by Def1;
then Sum (fg| (len f+min(g,j)))>=Sum f+j by A6,XREAL_1:7;
then
A8: len f+min(g,j)>=min(fg,i) by A4,Def1;
A9: i <= Sum(fg|min(fg,i)) by A4,Def1;
min(fg,i)>len f
proof
A10: f|len f=f by FINSEQ_1:58;
assume
A11: min(fg,i)<=len f;
then
A12: Sum(f|min(fg,i))<=Sum (f|len f) by POLYNOM3:18;
fg|min(fg,i)=f|min(fg,i) by A11,FINSEQ_5:22;
hence thesis by A4,A9,A2,A12,A10,FINSEQ_1:1,XXREAL_0:2;
end;
then reconsider m=min(fg,i)-len f as Element of NAT by NAT_1:21;
fg| (len f+m)=f^(g|m) by FINSEQ_6:14;
then i<=Sum f+Sum(g|m) by A9,RVSUM_1:75;
then j<=(Sum f+Sum (g|m))-Sum f by XREAL_1:9;
then m >= min(g,j) by A7,Def1;
then
A13: m+len f>=min(g,j)+len f by XREAL_1:7;
j=i-'Sum f by A4,A2,FINSEQ_1:1,XREAL_1:233;
hence thesis by A13,A8,XXREAL_0:1;
end;
Lm2: i in dom f implies Sum (f|i) = Sum (f| (i-'1))+(f.i)
proof
set g = <*f/.i*>;
set h = f| (i-'1);
assume
A1: i in dom f;
then i>=1 by FINSEQ_3:25;
then i-'1=i-1 by XREAL_1:233;
then
A2: i=i-'1+1;
A3: f/.i = f.i by A1,PARTFUN1:def 6;
hence Sum(f| (i-'1))+f.i = Sum (h^g) by RVSUM_1:74
.= Sum(f|i) by A1,A2,A3,FINSEQ_5:10;
end;
theorem Th10:
i in dom f & j in Seg (f/.i) implies j +Sum (f| (i-'1)) in Seg
Sum (f|i) & min(f,j+Sum (f| (i-'1)))=i
proof
assume that
A1: i in dom f and
A2: j in Seg (f/.i);
set fi=f/.i;
fi=f.i by A1,PARTFUN1:def 6;
then
A3: fi+Sum(f| (i-'1))= Sum(f|i) by A1,Lm2;
A4: f| (len f)=f by FINSEQ_1:58;
i<=len f by A1,FINSEQ_3:25;
then Sum(f|i)<=Sum(f| (len f)) by POLYNOM3:18;
then
A5: Seg Sum (f|i) c= Seg Sum f by A4,FINSEQ_1:5;
set jj=j+Sum(f| (i-'1));
j<=fi by A2,FINSEQ_1:1;
then
A6: jj<=fi+Sum(f| (i-'1)) by XREAL_1:7;
1<=j by A2,FINSEQ_1:1;
then 1+0<= jj by XREAL_1:7;
hence
A7: jj in Seg Sum (f|i) by A3,A6;
i>=1 by A1,FINSEQ_3:25;
then i-'1=i-1 by XREAL_1:233;
then
A8: i=(i-'1)+1;
A9: i<=min(f,jj)
proof
assume i> min(f,jj);
then min(f,jj)<=i-'1 by A8,NAT_1:13;
then
A10: Sum(f|min(f,jj))<=Sum(f| (i-'1)) by POLYNOM3:18;
0<j by A2;
then Sum (f| (i-'1))+0 < jj by XREAL_1:8;
then Sum(f|min(f,jj))<jj by A10,XXREAL_0:2;
hence thesis by A7,A5,Def1;
end;
min(f,jj)<=i by A3,A6,A7,A5,Def1;
hence thesis by A9,XXREAL_0:1;
end;
theorem
for i,j st i <= len f & j <= len f & Sum (f|i) = Sum (f|j) & ( i in
dom f implies f.i <> 0) & ( j in dom f implies f.j <> 0) holds i = j
proof
A1: now
let i,j such that
A2: i <= len f and
j <= len f and
A3: Sum (f|i) = Sum (f|j) and
A4: i in dom f implies f.i <> 0 and
j in dom f implies f.j <> 0;
assume
A5: i>j;
then reconsider i1=i-1 as Element of NAT by NAT_1:20;
A6: i=i1+1;
then j <= i1 by A5,NAT_1:13;
then
A7: Sum (f|j)<=Sum(f|i1) by POLYNOM3:18;
A8: i>=1 by A6,NAT_1:14;
then i in dom f by A2,FINSEQ_3:25;
then f| (i1+1)=(f|i1)^<*f.i*> by FINSEQ_5:10;
then
A9: Sum (f|j)=Sum (f|i1)+ f.i by A3,RVSUM_1:74;
then Sum (f|i1)<=Sum (f|j) by NAT_1:11;
then Sum (f|i1)=Sum (f|j) by A7,XXREAL_0:1;
hence contradiction by A2,A4,A8,A9,FINSEQ_3:25;
end;
let i,j such that
A10: i <= len f and
A11: j <= len f and
A12: Sum (f|i) = Sum (f|j) and
A13: i in dom f implies f.i <> 0 and
A14: j in dom f implies f.j <> 0;
A15: j<=i by A1,A10,A11,A12,A13,A14;
i<=j by A1,A10,A11,A12,A13,A14;
hence thesis by A15,XXREAL_0:1;
end;
begin :: Finite Sequences of Matrices
definition
let D;
let F be FinSequence of (D**);
attr F is Matrix-yielding means
:Def2:
for i st i in dom F holds F.i is Matrix of D;
end;
registration
let D;
cluster Matrix-yielding for FinSequence of D**;
existence
proof
reconsider F=<*>(D**) as FinSequence of D**;
take F;
thus thesis;
end;
end;
definition
let D;
mode FinSequence_of_Matrix of D is Matrix-yielding FinSequence of D**;
end;
definition
let K;
mode FinSequence_of_Matrix of K is Matrix-yielding FinSequence of (the
carrier of K)**;
end;
theorem Th12:
{} is FinSequence_of_Matrix of D
proof
set F=<*>(D**);
for i st i in dom F holds F.i is Matrix of D;
hence thesis by Def2;
end;
reserve F,F1,F2 for FinSequence_of_Matrix of D,
G,G9,G1,G2 for FinSequence_of_Matrix of K;
definition
let D,F,x;
redefine func F.x -> Matrix of D; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases;
suppose
A1: x in dom F;
thus thesis by A1,Def2;
end;
suppose
not x in dom F;
then F.x={} by FUNCT_1:def 2;
hence thesis by MATRIX_0:13;
end;
end;
end;
definition
let D,F1,F2;
redefine func F1^F2 -> FinSequence_of_Matrix of D; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
F1^F2 is Matrix-yielding
proof
let i such that
A1: i in dom (F1^F2);
per cases by A1,FINSEQ_1:25;
suppose
i in dom F1;
then (F1^F2).i=F1.i by FINSEQ_1:def 7;
hence thesis;
end;
suppose
ex n st n in dom F2 & i=len F1 + n;
then consider n such that
A2: n in dom F2 and
A3: i=len F1+n;
(F1^F2).i=F2.n by A2,A3,FINSEQ_1:def 7;
hence thesis;
end;
end;
hence thesis;
end;
end;
Lm3: <*M*> is Matrix-yielding
proof
now
A1: <*M*>.1=M;
A2: dom <*M*> ={1} by FINSEQ_1:2,def 8;
let i;
assume i in dom <*M*>;
hence <*M*>.i is Matrix of D by A2,A1,TARSKI:def 1;
end;
hence thesis;
end;
definition
let D,M1;
redefine func <* M1 *> -> FinSequence_of_Matrix of D; :: redefines <* (FINSEQ_1, definition)
coherence by Lm3;
let M2;
redefine func <* M1,M2 *> -> FinSequence_of_Matrix of D; :: redefines <* (FINSEQ_1, definition)
coherence
proof
reconsider F1=<*M1*>,F2=<*M2*> as FinSequence_of_Matrix of D by Lm3;
<*M1,M2*>=F1^F2;
hence thesis;
end;
end;
definition
let D,n,F;
redefine func F|n -> FinSequence_of_Matrix of D; :: redefines | (FINSEQ_1, definition)
coherence
proof
now
let i;
assume i in dom (F|n);
then (F|n).i=F.i by FUNCT_1:47;
hence (F|n).i is Matrix of D;
end;
hence thesis by Def2;
end;
redefine func F/^n -> FinSequence_of_Matrix of D; :: redefines /^ (RFINSEQ, definition)
coherence
proof
now
let i such that
A1: i in dom (F/^n);
i+n in dom F by A1,FINSEQ_5:26;
then F.(n+i)=F/.(n+i) by PARTFUN1:def 6;
hence (F/^n).i is Matrix of D by A1,FINSEQ_5:27;
end;
hence thesis by Def2;
end;
end;
begin :: Sequences of Sizes of Matrices in a Finite Sequence
definition
let D,F;
func Len F -> FinSequence of NAT means
:Def3:
dom it = dom F & for i st i in dom it holds it.i=len (F.i);
existence
proof
deffunc F(Nat)=len (F.$1);
consider p be FinSequence of NAT such that
A1: len p=len F and
A2: for i st i in dom p holds p.i=F(i) from FINSEQ_2:sch 1;
take p;
thus thesis by A1,A2,FINSEQ_3:29;
end;
uniqueness
proof
let F1,F2 be FinSequence of NAT such that
A3: dom F1=dom F and
A4: for i st i in dom F1 holds F1.i=len (F.i) and
A5: dom F2=dom F and
A6: for i st i in dom F2 holds F2.i=len (F.i);
now
let x being object such that
A7: x in dom F1;
reconsider i=x as Element of NAT by A7;
thus F1.x = len (F.i) by A4,A7
.= F2.x by A3,A5,A6,A7;
end;
hence thesis by A3,A5,FUNCT_1:2;
end;
func Width F -> FinSequence of NAT means
:Def4:
dom it = dom F & for i st i in dom it holds it.i=width (F.i);
existence
proof
deffunc F(Nat)=In(width (F.$1),NAT);
consider p be FinSequence of NAT such that
A8: len p=len F and
A9: for i st i in dom p holds p.i=F(i) from FINSEQ_2:sch 1;
take p;
thus dom p = dom F by A8,FINSEQ_3:29;
let i;
assume i in dom p;
then p.i=F(i) by A9;
hence thesis;
end;
uniqueness
proof
let F1,F2 be FinSequence of NAT such that
A10: dom F1=dom F and
A11: for i st i in dom F1 holds F1.i=width (F.i) and
A12: dom F2=dom F and
A13: for i st i in dom F2 holds F2.i=width (F.i);
now
let x being object such that
A14: x in dom F1;
reconsider i=x as Element of NAT by A14;
thus F1.x = width (F.i) by A11,A14
.= F2.x by A10,A12,A13,A14;
end;
hence thesis by A10,A12,FUNCT_1:2;
end;
end;
definition
let D,F;
redefine func Len F -> Element of (len F)-tuples_on NAT; :: redefines Len (MATRIXJ1, definition)
coherence
proof
dom Len F=dom F by Def3;
then len Len F=len F by FINSEQ_3:29;
hence thesis by FINSEQ_2:92;
end;
redefine func Width F -> Element of (len F)-tuples_on NAT; :: redefines Width (MATRIXJ1, definition)
coherence
proof
dom Width F=dom F by Def4;
then len Width F=len F by FINSEQ_3:29;
hence thesis by FINSEQ_2:92;
end;
end;
theorem Th13:
Sum Len F = 0 implies Sum Width F = 0
proof
set LF=Len F;
set WF=Width F;
assume
A1: Sum LF=0;
per cases by A1,RVSUM_1:85;
suppose
ex i st i in dom LF & 0> LF.i;
hence thesis;
end;
suppose
A2: for i st i in dom LF holds 0>=LF.i;
set F0=len F|->0;
A3: len WF=len F by CARD_1:def 7;
A4: dom LF=dom F by Def3;
A5: dom WF=dom F by Def4;
A6: now
let j such that
A7: 1<=j and
A8: j<=len WF;
A9: j in dom WF by A7,A8,FINSEQ_3:25;
then
A10: WF.j=width (F.j) by Def4;
j in Seg len F by A3,A7,A8;
then
A11: F0.j=0 by FINSEQ_2:57;
A12: 0>= LF.j by A2,A5,A4,A9;
LF.j=len (F.j) by A5,A4,A9,Def3;
hence WF.j=F0.j by A10,A12,A11,MATRIX_0:def 3;
end;
len F0=len F by CARD_1:def 7;
then WF=F0 by A3,A6;
hence thesis by RVSUM_1:81;
end;
end;
theorem Th14:
Len (F1 ^ F2) = Len F1 ^ Len F2
proof
set F12=F1^F2;
A1: len F12=len F1+len F2 by FINSEQ_1:22;
len F2=len Len F2 by CARD_1:def 7;
then
A2: dom (Len F2)=dom F2 by FINSEQ_3:29;
A3: len (Len F1^Len F2)=len F1+len F2 by CARD_1:def 7;
A4: len Len F12=len F12 by CARD_1:def 7;
then
A5: dom (Len F1 ^ Len F2)= dom Len F12 by A1,A3,FINSEQ_3:29;
A6: len F1=len Len F1 by CARD_1:def 7;
then
A7: dom (Len F1)=dom F1 by FINSEQ_3:29;
now
let k such that
A8: 1<=k and
A9: k<=len F1+len F2;
A10: k in dom (Len F1 ^ Len F2) by A3,A8,A9,FINSEQ_3:25;
now
per cases by A10,FINSEQ_1:25;
suppose
A11: k in dom (Len F1);
hence (Len F1 ^ Len F2).k = (Len F1).k by FINSEQ_1:def 7
.= len (F1.k) by A11,Def3
.= len(F12.k) by A7,A11,FINSEQ_1:def 7
.= (Len F12).k by A5,A10,Def3;
end;
suppose
ex n st n in dom (Len F2) & k=len (Len F1)+n;
then consider n such that
A12: n in dom (Len F2) and
A13: k=len F1+n by A6;
thus (Len F1 ^ Len F2).k = (Len F2).n by A6,A12,A13,FINSEQ_1:def 7
.= len (F2.n) by A12,Def3
.= len(F12.k) by A2,A12,A13,FINSEQ_1:def 7
.= (Len F12).k by A5,A10,Def3;
end;
end;
hence (Len F12).k=(Len F1 ^ Len F2).k;
end;
hence thesis by A4,A1,A3;
end;
theorem Th15:
Len <*M*> = <*len M*>
proof
set F=<*M*>;
A1: len F=1 by FINSEQ_1:40;
A3: len F=len (Len F) by CARD_1:def 7;
A4: dom (Len F)=Seg len F by FINSEQ_2:124;
1 in Seg 1;
then (Len F).1 = len (F.1) by A1,A4,Def3;
hence thesis by A1,A3,FINSEQ_1:40;
end;
Lm4: Sum Len <*M*> = len M
proof
Len <*M*>=<*len M*> by Th15;
hence thesis by RVSUM_1:73;
end;
theorem Th16:
Sum Len <*M1,M2*> = len M1 + len M2
proof
thus Sum Len <*M1,M2*> = Sum ((Len <*M1*>)^(Len<*M2*>)) by Th14
.= Sum Len <*M1*>+Sum Len<*M2*> by RVSUM_1:75
.= len M1+Sum Len <*M2*> by Lm4
.= len M1+len M2 by Lm4;
end;
theorem Th17:
Len (F1|n) = (Len F1) |n
proof
A1: len Len F1=len F1 by CARD_1:def 7;
per cases;
suppose
A2: n>=len F1;
then F1|n=F1 by FINSEQ_1:58;
hence thesis by A1,A2,FINSEQ_1:58;
end;
suppose
A3: n<len F1;
F1=(F1|n)^(F1/^n) by RFINSEQ:8;
then
A4: Len F1=(Len (F1|n))^Len (F1/^n) by Th14;
len (F1|n) =n by A3,FINSEQ_1:59;
then len Len (F1|n)=n by CARD_1:def 7;
hence thesis by A4,FINSEQ_5:23;
end;
end;
theorem Th18:
Width (F1 ^ F2)= Width F1 ^ Width F2
proof
set F12=F1^F2;
A1: len F12=len F1+len F2 by FINSEQ_1:22;
len F2=len Width F2 by CARD_1:def 7;
then
A2: dom (Width F2)=dom F2 by FINSEQ_3:29;
A3: len (Width F1^Width F2)=len F1+len F2 by CARD_1:def 7;
A4: len Width F12=len F12 by CARD_1:def 7;
then
A5: dom (Width F1 ^ Width F2) =dom Width F12 by A1,A3,FINSEQ_3:29;
A6: len F1=len Width F1 by CARD_1:def 7;
then
A7: dom (Width F1)=dom F1 by FINSEQ_3:29;
now
let k such that
A8: 1<=k and
A9: k<=len F1+len F2;
A10: k in dom (Width F1 ^ Width F2) by A3,A8,A9,FINSEQ_3:25;
now
per cases by A10,FINSEQ_1:25;
suppose
A11: k in dom (Width F1);
hence (Width F1 ^ Width F2).k = (Width F1).k by FINSEQ_1:def 7
.= width (F1.k) by A11,Def4
.= width(F12.k) by A7,A11,FINSEQ_1:def 7
.= (Width F12).k by A5,A10,Def4;
end;
suppose
ex n st n in dom (Width F2) & k=len (Width F1)+n;
then consider n such that
A12: n in dom (Width F2) and
A13: k=len F1+n by A6;
thus (Width F1 ^ Width F2).k = (Width F2).n by A6,A12,A13,
FINSEQ_1:def 7
.= width (F2.n) by A12,Def4
.= width(F12.k) by A2,A12,A13,FINSEQ_1:def 7
.= (Width F12).k by A5,A10,Def4;
end;
end;
hence (Width F12).k=(Width F1 ^ Width F2).k;
end;
hence thesis by A4,A1,A3;
end;
theorem Th19:
Width <*M*> = <*width M*>
proof
set F=<*M*>;
A1: len F=1 by FINSEQ_1:40;
A3: len F=len (Width F) by CARD_1:def 7;
A4: dom (Width F)=Seg len F by FINSEQ_2:124;
1 in Seg 1;
then (Width F).1=width (F.1) by A1,A4,Def4;
hence thesis by A1,A3,FINSEQ_1:40;
end;
Lm5: Sum Width <*M*>=width M
proof
Width <*M*>=<*width M*> by Th19;
hence thesis by RVSUM_1:73;
end;
theorem Th20:
Sum Width <*M1,M2*>=width M1+width M2
proof
thus Sum Width <*M1,M2*> = Sum ((Width <*M1*>)^(Width<*M2*>)) by Th18
.= Sum Width <*M1*>+Sum Width<*M2*> by RVSUM_1:75
.= width M1+Sum Width <*M2*> by Lm5
.= width M1+width M2 by Lm5;
end;
theorem Th21:
Width (F1|n) =(Width F1) |n
proof
A1: len Width F1=len F1 by CARD_1:def 7;
per cases;
suppose
A2: n>=len F1;
then F1|n=F1 by FINSEQ_1:58;
hence thesis by A1,A2,FINSEQ_1:58;
end;
suppose
A3: n<len F1;
F1=(F1|n)^(F1/^n) by RFINSEQ:8;
then
A4: Width F1=(Width (F1|n))^Width (F1/^n) by Th18;
len (F1|n) =n by A3,FINSEQ_1:59;
then len Width (F1|n)=n by CARD_1:def 7;
hence thesis by A4,FINSEQ_5:23;
end;
end;
begin :: Block Diagonal Matrices
definition
let D;
let d be Element of D;
let F be FinSequence_of_Matrix of D;
func block_diagonal(F,d) -> Matrix of D means
:Def5:
len it = Sum Len F &
width it = Sum Width F & for i,j st [i,j] in Indices it holds (j<=Sum((Width F)
| (min(Len F,i)-'1)) or j>Sum ((Width F) |min(Len F,i)) implies it*(i,j) = d)
& (
Sum((Width F) | (min(Len F,i)-'1)) < j & j <= Sum((Width F) |min(Len F,i))
implies
it*(i,j) = F.min(Len F,i)*(i-'Sum((Len F) | (min(Len F,i)-'1)),
j-'Sum ((Width F) | (min(Len F,i)-'1))));
existence
proof
set M=Sum Width F;
set N=Sum Len F;
set L=Len F;
set W=Width F;
defpred P[Nat,Nat,Element of D] means ($2 <= Sum(W| (min(L,$1)-'1)) or$2>
Sum (W|min(L,$1)) implies $3 = d) & (Sum (W| (min(L,$1)-'1)) <$2 &$2<= Sum (W|
min(L,$1)) implies $3 = F.min(L,$1)*($1-'Sum(L| (min(L,$1)-'1)),
$2-'Sum (W| (min (L,$1)-'1))));
A1: for i,j st [i,j] in [:Seg N, Seg M:] ex x being Element of D st P[i,j, x]
proof
let i,j such that
[i,j] in [:Seg N,Seg M:];
per cases;
suppose
A2: j<= Sum(W| (min(L,i)-'1))or j>Sum (W|min(L,i));
take d;
thus thesis by A2;
end;
suppose
A3: Sum(W| (min(L,i)-'1))<j & j<=Sum (W|min(L,i));
take F.min(L,i)*(i-'Sum(L| (min(L,i)-'1)), j-'Sum (W| (min(L,i)-'1)));
thus thesis by A3;
end;
end;
consider MM being Matrix of N,M,D such that
A4: for i,j st [i,j] in Indices MM holds P[i,j,MM*(i,j)] from MATRIX_0
:sch 2(A1);
take MM;
per cases;
suppose
A5: N=0;
then M=0 by Th13;
hence thesis by A5,MATRIX_0:22;
end;
suppose
N>0;
hence thesis by A4,MATRIX_0:23;
end;
end;
uniqueness
proof
set W=Width F;
set L=Len F;
let M1,M2 be Matrix of D such that
A6: len M1=Sum L and
A7: width M1=Sum W and
A8: for i,j st [i,j] in Indices M1 holds (j<=Sum(W| (min(L,i)-'1))or j
>Sum(W|min(L,i)) implies M1*(i,j)=d)& (Sum(W| (min(L,i)-'1))<j &
j<=Sum (W|min(L
,i)) implies M1*(i,j)=F.min(L,i)*(i-'Sum(L| (min(L,i)-'1)),
j-'Sum (W| (min(L,i)-'1)))) and
A9: len M2=Sum L and
A10: width M2=Sum W and
A11: for i,j st [i,j] in Indices M2 holds (j<=Sum(W| (min(L,i)-'1)) or
j>Sum (W|min(L,i)) implies M2*(i,j) = d) & (Sum(W| (min(L,i)-'1))<j&j<=Sum (W|
min(L,i)) implies M2*(i,j)=F.min(L,i)*(i-'Sum(L| (min(L,i)-'1)),
j-'Sum (W| (min( L,i)-'1))));
A12: Indices M1 = [:Seg len M1,Seg width M1:] by FINSEQ_1:def 3
.= Indices M2 by A6,A7,A9,A10,FINSEQ_1:def 3;
now
let i,j such that
A13: [i,j] in Indices M1;
(j <= Sum(W| (min(L,i)-'1) ) or j > Sum (W|min(L,i))) or Sum(W| (min(
L,i)-'1)) < j & j <= Sum (W|min(L,i));
then
M1*(i,j)= d & M2*(i,j)=d or M1*(i,j) = F.min(L,i)*(i-'Sum(L| (min(L,
i)-'1)), j-'Sum (W| (min(L,i)-'1))) & M2*(i,j) =
F.min(L,i)*(i-'Sum(L| (min(L,i)
-'1)), j-'Sum (W| (min(L,i)-'1))) by A8,A11,A12,A13;
hence M1*(i,j)=M2*(i,j);
end;
hence thesis by A6,A7,A9,A10,MATRIX_0:21;
end;
end;
definition
let D;
let d be Element of D;
let F be FinSequence_of_Matrix of D;
redefine func block_diagonal(F,d) -> Matrix of Sum Len F,Sum Width F,D; :: redefines block_diagonal (MATRIXJ1, definition)
coherence
proof
A1: width block_diagonal(F,d)=Sum Width F by Def5;
len block_diagonal(F,d)=Sum Len F by Def5;
hence thesis by A1,MATRIX_0:51;
end;
end;
theorem
for F be FinSequence_of_Matrix of D st F={} holds block_diagonal(F,d)= {}
proof
let F be FinSequence_of_Matrix of D;
assume F={};
then len Len F=0;
then Len F=<*>REAL;
then 0 =len block_diagonal(F,d) by Def5,RVSUM_1:72;
hence thesis;
end;
theorem Th23:
for M be Matrix of Sum Len (<*M1,M2*>),Sum Width (<*M1,M2*>),D
holds M = block_diagonal(<*M1,M2*>,d) iff for i holds (i in dom M1 implies Line
(M,i)=Line(M1,i)^(width M2 |-> d)) & (i in dom M2 implies Line(M,i+len M1)=(
width M1|->d)^Line(M2,i))
proof
let M be Matrix of Sum Len (<*M1,M2*>),Sum Width (<*M1,M2*>),D;
set F1=<*M1*>;
set F2=<*M2*>;
set F12=<*M1,M2*>;
set B=block_diagonal(F12,d);
set L1=len M1;
set L2=len M2;
reconsider W1=width M1 as Element of NAT by ORDINAL1:def 12;
set W2=width M2;
A1: Sum <*W1*>=W1 by RVSUM_1:73;
len B=Sum Len F12 by Def5;
then
A2: len B=L1+L2 by Th16;
A3: len F12=len Len F12 by CARD_1:def 7;
A4: (Len F12) |0=<*>REAL;
A5: (Width F12) |0=<*>REAL;
A6: 1-'1=0 by XREAL_1:232;
A7: width B=Sum Width F12 by Def5;
then
A8: width B=W1+W2 by Th20;
A9: len <*W1*>=1 by FINSEQ_1:40;
A10: len F1=1 by FINSEQ_1:40;
A11: Len F1=<*L1*> by Th15;
A12: Len F12=(Len F1) ^(Len F2) by Th14;
then
A13: (Len F12).1=L1 by A11,FINSEQ_1:41;
A14: len <*L1*>=1 by FINSEQ_1:40;
then
A15: (Len F12) |1=<*L1*> by A12,A11,FINSEQ_5:23;
A16: Width F1=<*W1*> by Th19;
A17: Sum <*L1*>=L1 by RVSUM_1:73;
Width F12=(Width F1)^(Width F2) by Th18;
then
A18: (Width F12) |1=<*W1*> by A16,A9,FINSEQ_5:23;
A19: Len F2=<*L2*> by Th15;
then
A20: len Len F12=1+1 by A12,A11,A14,FINSEQ_2:16;
A21: (Len F12).2=L2 by A12,A11,A19,A14,FINSEQ_1:42;
len Width F12=len F12 by CARD_1:def 7;
then
A22: (Width F12) |2=Width F12 by A20,A3,FINSEQ_1:58;
A23: dom Len F12={1,2} by A20,FINSEQ_1:2,def 3;
then
A24: 1 in dom Len F12 by TARSKI:def 2;
then
A25: (Len F12)/.1=(Len F12).1 by PARTFUN1:def 6;
A26: 2-'1=2-1 by XREAL_1:233;
Sum Len F12=0 implies Sum Width F12=0 by Th13;
then
A27: width M=W1+W2 by A7,A8,MATRIX13:1;
A28: 2 in dom Len F12 by A23,TARSKI:def 2;
then
A29: (Len F12)/.2=(Len F12).2 by PARTFUN1:def 6;
hereby
assume
A30: M = B;
let i;
thus i in dom M1 implies Line(M,i)=Line(M1,i)^(W2|-> d)
proof
set W2d=W2|->d;
set LM1=Line(M1,i);
set LM=Line(M,i);
A31: L1<=L1+L2 by NAT_1:11;
A32: len LM1=W1 by CARD_1:def 7;
assume
A33: i in dom M1;
then
A34: 1<=i by FINSEQ_3:25;
i<=L1 by A33,FINSEQ_3:25;
then i<=L1+L2 by A31,XXREAL_0:2;
then
A35: i in dom B by A2,A34,FINSEQ_3:25;
A36: len W2d=W2 by CARD_1:def 7;
A37: len (LM1^W2d)= len LM1+len W2d by FINSEQ_1:22;
A38: len LM=W1+W2 by A27,CARD_1:def 7;
A39: i in Seg L1 by A33,FINSEQ_1:def 3;
now
A40: min(Len F12,i+0)=1 by A24,A6,A13,A25,A4,A39,Th10,RVSUM_1:72;
let j such that
A41: 1<=j and
A42: j<=len LM;
A43: j in Seg width B by A8,A38,A41,A42;
then
A44: [i,j] in Indices B by A35,ZFMISC_1:87;
A45: j in dom (LM1^W2d) by A38,A32,A36,A37,A41,A42,FINSEQ_3:25;
now
per cases;
suppose
A46: j<=W1;
then
A47: j in Seg width M1 by A41;
A48: j in dom LM1 by A32,A41,A46,FINSEQ_3:25;
thus LM.j = M*(i,j) by A8,A27,A43,MATRIX_0:def 7
.= F12.1*(i-'Sum((Len F12) |0),j-'Sum ((Width F12) |0)) by A1,A6
,A18,A30,A41,A44,A40,A46,Def5,RVSUM_1:72
.= F12.1*(i,j-'0) by NAT_D:40,RVSUM_1:72
.= F12.1*(i,j) by NAT_D:40
.= M1*(i,j)
.= LM1.j by A47,MATRIX_0:def 7
.= (LM1^W2d).j by A48,FINSEQ_1:def 7;
end;
suppose
A49: j>W1;
A50: dom W2d=Seg W2 by A36,FINSEQ_1:def 3;
not j in dom LM1 by A32,A49,FINSEQ_3:25;
then consider k such that
A51: k in dom W2d and
A52: j=len LM1+k by A45,FINSEQ_1:25;
thus LM.j = M*(i,j) by A8,A27,A43,MATRIX_0:def 7
.= d by A1,A18,A30,A44,A40,A49,Def5
.= W2d.k by A51,A50,FINSEQ_2:57
.= (LM1^W2d).j by A51,A52,FINSEQ_1:def 7;
end;
end;
hence LM.j=(LM1^W2d).j;
end;
hence thesis by A38,A32,A36,A37;
end;
thus i in dom M2 implies Line(M,i+len M1)=( width M1|->d)^Line(M2,i)
proof
set LM2=Line(M2,i);
set W1d=W1|->d;
set LM=Line(M,i+L1);
A53: len LM2=W2 by CARD_1:def 7;
A54: len (W1d^LM2)= len W1d + len LM2 by FINSEQ_1:22;
A55: len W1d=W1 by CARD_1:def 7;
A56: len LM=W1+W2 by A27,CARD_1:def 7;
assume i in dom M2;
then
A57: i in Seg L2 by FINSEQ_1:def 3;
then L1+i in Seg (L1+L2) by FINSEQ_1:60;
then
A58: L1+i in dom B by A2,FINSEQ_1:def 3;
now
A59: min(Len F12,i+L1)=2 by A17,A28,A26,A21,A29,A15,A57,Th10;
let j such that
A60: 1<=j and
A61: j<=len LM;
A62: j in Seg width B by A8,A56,A60,A61;
then
A63: [i+L1,j] in Indices B by A58,ZFMISC_1:87;
A64: j in dom (W1d^LM2) by A56,A53,A55,A54,A60,A61,FINSEQ_3:25;
per cases;
suppose
A65: j<=W1;
A66: dom W1d=Seg W1 by A55,FINSEQ_1:def 3;
A67: j in Seg W1 by A60,A65;
thus LM.j = B*(i+L1,j) by A30,A62,MATRIX_0:def 7
.= d by A1,A26,A18,A63,A59,A65,Def5
.= W1d.j by A67,FINSEQ_2:57
.= (W1d^LM2).j by A67,A66,FINSEQ_1:def 7;
end;
suppose
A68: j>W1;
A69: dom LM2=Seg W2 by A53,FINSEQ_1:def 3;
not j in dom W1d by A55,A68,FINSEQ_3:25;
then consider k such that
A70: k in dom LM2 and
A71: j=W1+k by A55,A64,FINSEQ_1:25;
thus LM.j = B*(i+L1,j) by A30,A62,MATRIX_0:def 7
.= F12.2*(i+L1-'L1,j-'W1) by A7,A8,A1,A17,A26,A15,A18,A22,A56,A61
,A63,A59,A68,Def5
.= F12.2*(i,j-'W1) by NAT_D:34
.= F12.(len F1+1)*(i,k) by A10,A71,NAT_D:34
.= M2*(i,k) by FINSEQ_1:42
.= LM2.k by A70,A69,MATRIX_0:def 7
.= (W1d^LM2).j by A55,A70,A71,FINSEQ_1:def 7;
end;
end;
hence thesis by A56,A53,A55,A54;
end;
end;
assume
A72: for i holds
(i in dom M1 implies Line(M,i)=Line(M1,i)^(width M2 |-> d)) &
(i in dom M2 implies Line(M,i+len M1)=(width M1|->d)^Line(M2,i));
A73: Sum ((Width F12) |2)=W1+W2 by A22,Th20;
now
set W1d=W1|->d;
set W2d=W2|->d;
A74: Indices M=Indices B by MATRIX_0:26;
let i,j such that
A75: [i,j] in Indices M;
A76: i in dom B by A75,A74,ZFMISC_1:87;
then
A77: 1<=i by FINSEQ_3:25;
A78: j in Seg width B by A75,A74,ZFMISC_1:87;
then
A79: 1<=j by FINSEQ_1:1;
A80: i in Seg (L1+L2) by A2,A76,FINSEQ_1:def 3;
set LM1=Line(M1,i);
A81: len LM1=W1 by CARD_1:def 7;
A82: len W1d=W1 by CARD_1:def 7;
A83: len W2d=W2 by CARD_1:def 7;
A84: len (LM1^W2d)=len LM1 + len W2d by FINSEQ_1:22;
A85: j<=width B by A78,FINSEQ_1:1;
now
per cases;
suppose
A86: i<=L1;
then i in Seg L1 by A77;
then
A87: min(Len F12,i+0)=1 by A24,A6,A13,A25,A4,Th10,RVSUM_1:72;
A88: now
per cases;
suppose
A89: j<=W1;
then
A90: j in Seg width M1 by A79;
A91: j in dom LM1 by A79,A81,A89,FINSEQ_3:25;
thus B*(i,j) = F12.1*(i-'0, j-'0) by A1,A6,A4,A5,A18,A75,A74,A79
,A87,A89,Def5,RVSUM_1:72
.= F12.1*(i,j-'0) by NAT_D:40
.= F12.1*(i,j) by NAT_D:40
.= M1*(i,j)
.= LM1.j by A90,MATRIX_0:def 7
.= (LM1^W2d).j by A91,FINSEQ_1:def 7;
end;
suppose
A92: j>W1;
then
A93: not j in dom LM1 by A81,FINSEQ_3:25;
A94: dom W2d=Seg W2 by A83,FINSEQ_1:def 3;
dom (LM1^W2d)=Seg width B by A8,A81,A83,A84,FINSEQ_1:def 3;
then consider k such that
A95: k in dom W2d and
A96: j=len LM1+k by A78,A93,FINSEQ_1:25;
thus B*(i,j) = d by A1,A18,A75,A74,A87,A92,Def5
.= W2d.k by A95,A94,FINSEQ_2:57
.= (LM1^W2d).j by A95,A96,FINSEQ_1:def 7;
end;
end;
i in dom M1 by A77,A86,FINSEQ_3:25;
then Line(M,i)=LM1^W2d by A72;
hence M*(i,j)=B*(i,j) by A8,A27,A78,A88,MATRIX_0:def 7;
end;
suppose
A97: i>L1;
then reconsider iL=i-L1 as Element of NAT by NAT_1:21;
A98: iL<>0 by A97;
set LM2=Line(M2,iL);
i=iL+L1;
then iL in Seg L2 by A80,A98,FINSEQ_1:61;
then
A99: min(Len F12,iL+L1)=2 by A17,A28,A26,A21,A29,A15,Th10;
A100: now
per cases;
suppose
A101: j<=W1;
then
A102: j in Seg W1 by A79;
A103: j in dom W1d by A79,A82,A101,FINSEQ_3:25;
thus B*(i,j) = d by A1,A26,A18,A75,A74,A99,A101,Def5
.= W1d.j by A102,FINSEQ_2:57
.= (W1d^LM2).j by A103,FINSEQ_1:def 7;
end;
suppose
A104: j>W1;
len LM2=W2 by MATRIX_0:def 7;
then
A105: dom W2d=dom LM2 by A83,FINSEQ_3:29;
A106: not j in dom LM1 by A81,A104,FINSEQ_3:25;
A107: dom W2d=Seg W2 by A83,FINSEQ_1:def 3;
dom (LM1^W2d)=Seg width B by A8,A81,A83,A84,FINSEQ_1:def 3;
then consider k such that
A108: k in dom W2d and
A109: j=W1+k by A78,A81,A106,FINSEQ_1:25;
thus B*(i,j) = F12.2*(iL+L1-'L1,j-'W1) by A8,A1,A17,A26,A15,A18,A73
,A75,A74,A85,A99,A104,Def5
.= F12.2*(iL,j-'W1) by NAT_D:34
.= F12.(len F1+1)*(iL,k) by A10,A109,NAT_D:34
.= M2*(iL,k) by FINSEQ_1:42
.= LM2.k by A108,A107,MATRIX_0:def 7
.= (W1d^LM2).j by A82,A108,A109,A105,FINSEQ_1:def 7;
end;
end;
Seg L2=dom M2 by FINSEQ_1:def 3;
then Line(M,iL+L1)=(W1|->d)^Line(M2,iL) by A72,A80,A98,FINSEQ_1:61;
hence M*(i,j)=B*(i,j) by A8,A27,A78,A100,MATRIX_0:def 7;
end;
end;
hence M*(i,j)=B*(i,j);
end;
hence thesis by MATRIX_0:27;
end;
theorem Th24:
for M be Matrix of Sum Len (<*M1,M2*>),Sum Width (<*M1,M2*>),D
holds M = block_diagonal(<*M1,M2*>,d) iff for i holds (i in Seg width M1
implies Col(M,i) = Col(M1,i)^(len M2 |-> d)) & (i in Seg width M2 implies Col(M
,i+width M1)=(len M1|->d)^Col(M2,i))
proof
let M be Matrix of Sum Len (<*M1,M2*>),Sum Width (<*M1,M2*>),D;
set m12=<*M1,M2*>;
set B=block_diagonal(m12,d);
A1: Seg len M=dom M by FINSEQ_1:def 3;
A2: Seg len M1=dom M1 by FINSEQ_1:def 3;
A3: dom M2=Seg len M2 by FINSEQ_1:def 3;
A4: Sum Len m12=len M1+len M2 by Th16;
A5: Sum Len m12=0 implies Sum Width m12=0 by Th13;
then
A6: len M=Sum Len m12 by MATRIX13:1;
A7: width M=Sum Width m12 by A5,MATRIX13:1;
A8: Sum Width m12=width M1+width M2 by Th20;
then width M1<=width M by A7,NAT_1:12;
then
A9: Seg width M1 c= Seg width M by FINSEQ_1:5;
thus M = B implies for i holds (i in Seg width M1 implies Col(M,i)=Col(M1,i)
^(len M2 |-> d)) & (i in Seg width M2 implies Col(M,i+width M1)=(len M1|->d)^
Col(M2,i))
proof
A10: dom (width M2 |-> d) =Seg width M2 by FINSEQ_2:124;
A11: dom (width M1 |-> d) =Seg width M1 by FINSEQ_2:124;
set L2=len M2|->d;
set L1=len M1|->d;
assume
A12: M=B;
let i;
set CM=Col(M,i);
set CM1=Col(M1,i);
A13: len CM=len M by CARD_1:def 7;
A14: dom L1=Seg len M1 by FINSEQ_2:124;
A15: dom L2=Seg len M2 by FINSEQ_2:124;
A16: len CM1=len M1 by CARD_1:def 7;
then
A17: dom CM1=dom M1 by FINSEQ_3:29;
A18: len L2=len M2 by CARD_1:def 7;
then
A19: dom L2=dom M2 by FINSEQ_3:29;
thus i in Seg width M1 implies CM=CM1^L2
proof
assume
A20: i in Seg width M1;
A21: len (CM1^L2)=len CM1+len L2 by FINSEQ_1:22;
now
let j such that
A22: 1<=j and
A23: j<=len CM;
j in dom M by A13,A22,A23,FINSEQ_3:25;
then
A24: CM.j=Line(M,j).i by A9,A20,MATRIX_0:42;
A25: dom Line(M1,j)=Seg width M1 by FINSEQ_2:124;
A26: j in dom (CM1^L2) by A6,A4,A13,A16,A18,A21,A22,A23,FINSEQ_3:25;
now
per cases by A26,FINSEQ_1:25;
suppose
A27: j in dom CM1;
hence CM.j = (Line(M1,j)^(width M2 |-> d)).i by A12,A17,A24,Th23
.= Line(M1,j).i by A20,A25,FINSEQ_1:def 7
.= CM1.j by A17,A20,A27,MATRIX_0:42
.= (CM1^L2).j by A27,FINSEQ_1:def 7;
end;
suppose
ex k st k in dom L2 & j=len CM1+k;
then consider k such that
A28: k in dom L2 and
A29: j = len CM1+k;
thus CM.j = ((width M1 |-> d)^Line(M2,k)).i by A12,A16,A19,A24,A28
,A29,Th23
.= (width M1|->d).i by A11,A20,FINSEQ_1:def 7
.= d by A20,FINSEQ_2:57
.= L2.k by A15,A28,FINSEQ_2:57
.= (CM1^L2).j by A28,A29,FINSEQ_1:def 7;
end;
end;
hence (CM1^L2).j=CM.j;
end;
hence thesis by A6,A13,A16,A18,A21,Th16;
end;
set CM2=Col(M2,i);
set CMi=Col(M,i+width M1);
A30: len CMi=len M by CARD_1:def 7;
A31: len CM2=len M2 by CARD_1:def 7;
then
A32: dom CM2=dom M2 by FINSEQ_3:29;
A33: len (L1^CM2)=len L1+len CM2 by FINSEQ_1:22;
assume
A34: i in Seg width M2;
A35: len L1=len M1 by CARD_1:def 7;
then
A36: dom L1=dom M1 by FINSEQ_3:29;
now
A37: len (width M1|->d)=width M1 by CARD_1:def 7;
let j such that
A38: 1<=j and
A39: j<=len CMi;
A40: j in dom M by A30,A38,A39,FINSEQ_3:25;
i+width M1 in Seg width M by A7,A8,A34,FINSEQ_1:60;
then
A41: CMi.j=Line(M,j).(i+width M1) by A40,MATRIX_0:42;
A42: len Line(M1,j)=width M1 by CARD_1:def 7;
A43: j in dom (L1^CM2) by A6,A4,A30,A31,A35,A33,A38,A39,FINSEQ_3:25;
now
per cases by A43,FINSEQ_1:25;
suppose
A44: j in dom L1;
hence CMi.j = (Line(M1,j)^(width M2 |-> d)).(i+width M1) by A12,A36
,A41,Th23
.= (width M2 |-> d).i by A10,A34,A42,FINSEQ_1:def 7
.= d by A34,FINSEQ_2:57
.= L1.j by A14,A44,FINSEQ_2:57
.= (L1^CM2).j by A44,FINSEQ_1:def 7;
end;
suppose
ex k st k in dom CM2 & j=len L1+k;
then consider k such that
A45: k in dom CM2 and
A46: j = len L1+k;
A47: dom Line(M2,k)=Seg width M2 by FINSEQ_2:124;
thus CMi.j = ((width M1 |-> d)^Line(M2,k)).(i+width M1) by A12,A35
,A32,A41,A45,A46,Th23
.= Line(M2,k).i by A34,A37,A47,FINSEQ_1:def 7
.= CM2.k by A32,A34,A45,MATRIX_0:42
.= (L1^CM2).j by A45,A46,FINSEQ_1:def 7;
end;
end;
hence (L1^CM2).j=CMi.j;
end;
hence thesis by A6,A30,A31,A35,A33,Th16;
end;
assume
A48: for i holds (i in Seg width M1 implies Col(M,i)=Col(M1,i)^(len M2
|-> d)) & (i in Seg width M2 implies Col(M,i+width M1)=(len M1|->d)^Col(M2,i));
len M1 <=len M by A6,A4,NAT_1:12;
then
A49: Seg len M1 c= Seg len M by FINSEQ_1:5;
now
set W2=width M2|->d;
set W1=width M1|->d;
let i;
set LM=Line(M,i);
set LMi=Line(M,i+len M1);
set LM1=Line(M1,i);
set LM2=Line(M2,i);
A50: len LMi=width M by CARD_1:def 7;
A51: len W2=width M2 by CARD_1:def 7;
then
A52: dom W2=Seg width M2 by FINSEQ_1:def 3;
A53: len LM=width M by CARD_1:def 7;
then
A54: dom LM=Seg width M by FINSEQ_1:def 3;
A55: len LM1=width M1 by CARD_1:def 7;
then
A56: dom LM1=Seg width M1 by FINSEQ_1:def 3;
thus i in dom M1 implies LM=LM1^W2
proof
assume
A57: i in dom M1;
A58: len (LM1^W2)=len LM1+len W2 by FINSEQ_1:22;
now
A59: dom (len M1|->d) =Seg len M1 by FINSEQ_2:124;
let j such that
A60: 1<=j and
A61: j<=len LM;
j in Seg width M by A54,A60,A61,FINSEQ_3:25;
then
A62: LM.j=Col(M,j).i by A49,A1,A2,A57,MATRIX_0:42;
A63: dom Col(M1,j)=Seg len M1 by FINSEQ_2:124;
A64: j in dom (LM1^W2) by A7,A8,A53,A55,A51,A58,A60,A61,FINSEQ_3:25;
now
per cases by A64,FINSEQ_1:25;
suppose
A65: j in dom LM1;
hence LM.j = (Col(M1,j)^(len M2 |-> d)).i by A48,A56,A62
.= Col(M1,j).i by A2,A57,A63,FINSEQ_1:def 7
.= LM1.j by A56,A57,A65,MATRIX_0:42
.= (LM1^W2).j by A65,FINSEQ_1:def 7;
end;
suppose
ex n st n in dom W2 & j=len LM1+n;
then consider n such that
A66: n in dom W2 and
A67: j=len LM1+n;
thus LM.j =((len M1|->d)^Col(M2,n)).i by A48,A55,A52,A62,A66,A67
.= (len M1|->d).i by A2,A57,A59,FINSEQ_1:def 7
.= d by A2,A57,FINSEQ_2:57
.= W2.n by A52,A66,FINSEQ_2:57
.= (LM1^W2).j by A66,A67,FINSEQ_1:def 7;
end;
end;
hence LM.j=(LM1^W2).j;
end;
hence thesis by A7,A53,A55,A51,A58,Th20;
end;
A68: len LM2=width M2 by CARD_1:def 7;
then
A69: dom LM2=Seg width M2 by FINSEQ_1:def 3;
A70: len W1=width M1 by CARD_1:def 7;
then
A71: dom W1=Seg width M1 by FINSEQ_1:def 3;
thus i in dom M2 implies LMi=W1^LM2
proof
assume
A72: i in dom M2;
A73: len (W1^LM2)=len W1 + len LM2 by FINSEQ_1:22;
now
A74: len (len M1|->d)=len M1 by CARD_1:def 7;
A75: dom (len M2|->d)=Seg len M2 by FINSEQ_2:124;
A76: dom M2=Seg len M2 by FINSEQ_1:def 3;
let j such that
A77: 1<=j and
A78: j<=len LMi;
j in Seg width M by A50,A77,A78;
then
A79: LMi.j=Col(M,j).(i+len M1) by A6,A4,A1,A72,A76,FINSEQ_1:60,MATRIX_0:42;
A80: len Col(M1,j)=len M1 by CARD_1:def 7;
A81: j in dom (W1^LM2) by A7,A8,A50,A68,A70,A73,A77,A78,FINSEQ_3:25;
now
per cases by A81,FINSEQ_1:25;
suppose
A82: j in dom W1;
hence LMi.j = (Col(M1,j)^(len M2 |-> d)).(i+len M1) by A48,A71,A79
.= (len M2 |-> d).i by A3,A72,A80,A75,FINSEQ_1:def 7
.= d by A3,A72,FINSEQ_2:57
.= W1.j by A71,A82,FINSEQ_2:57
.= (W1^LM2).j by A82,FINSEQ_1:def 7;
end;
suppose
ex n st n in dom LM2 & j=len W1+n;
then consider n such that
A83: n in dom LM2 and
A84: j=len W1+n;
A85: dom Col(M2,n)=Seg len M2 by FINSEQ_2:124;
thus LMi.j = ((len M1|->d)^Col(M2,n)).(i+len M1) by A48,A70,A69,A79
,A83,A84
.= Col(M2,n).i by A3,A72,A74,A85,FINSEQ_1:def 7
.= LM2.n by A69,A72,A83,MATRIX_0:42
.= (W1^LM2).j by A83,A84,FINSEQ_1:def 7;
end;
end;
hence LMi.j=(W1^LM2).j;
end;
hence thesis by A7,A50,A68,A70,A73,Th20;
end;
end;
hence thesis by Th23;
end;
theorem Th25:
Indices block_diagonal(F1,d1) is Subset of Indices block_diagonal(F1^F2,d2)
proof
set B1=block_diagonal(F1,d1);
set B2=block_diagonal(F1^F2,d2);
Indices B1 c= Indices B2
proof
(Len F1)^(Len F2)=Len (F1^F2) by Th14;
then Sum Len F1+Sum Len F2=Sum Len (F1^F2) by RVSUM_1:75;
then 0+Sum Len F1 <= Sum Len (F1^F2) by XREAL_1:6;
then
A1: Seg Sum Len F1 c= Seg Sum Len (F1^F2) by FINSEQ_1:5;
A2: dom B2=Seg len B2 by FINSEQ_1:def 3;
(Width F1)^(Width F2)=Width (F1^F2) by Th18;
then Sum Width F1+Sum Width F2= Sum Width (F1^F2) by RVSUM_1:75;
then 0+Sum Width F1<= Sum Width(F1^F2) by XREAL_1:6;
then
A3: Seg Sum Width F1 c= Seg Sum Width (F1^F2) by FINSEQ_1:5;
A4: len B1=Sum Len F1 by Def5;
let x be object;
assume x in Indices B1;
then
A5: ex i,j be object st i in dom B1 & j in Seg width B1 & x=[i,j] by
ZFMISC_1:def 2;
A6: dom B1=Seg len B1 by FINSEQ_1:def 3;
A7: width B1=Sum Width F1 by Def5;
A8: width B2=Sum Width (F1^F2) by Def5;
len B2=Sum Len (F1^F2) by Def5;
hence thesis by A5,A6,A2,A4,A8,A7,A1,A3,ZFMISC_1:87;
end;
hence thesis;
end;
theorem Th26:
[i,j] in Indices block_diagonal(F1,d) implies block_diagonal(F1,
d)*(i,j) = block_diagonal(F1^F2,d)*(i,j)
proof
set B1=block_diagonal(F1,d);
set L1=Len F1;
set W1=Width F1;
set L2=Len F2;
set W2=Width F2;
set F12=F1^F2;
set L=Len F12;
set W=Width F12;
set B12=block_diagonal(F12,d);
A1: len F1=len W1 by CARD_1:def 7;
A2: len B1= Sum L1 by Def5;
assume
A3: [i,j] in Indices block_diagonal(F1,d);
then i in dom B1 by ZFMISC_1:87;
then
A4: i in Seg len B1 by FINSEQ_1:def 3;
then
A5: min(L1,i) in dom L1 by A2,Def1;
then
A6: min(L1,i)<=len L1 by FINSEQ_3:25;
L1^L2=L by Th14;
then
A7: min(L1,i)=min(L,i) by A4,A2,Th8;
A8: dom L1=dom F1 by Def3;
A9: W1^W2=W by Th18;
A10: L1^L2=L by Th14;
A11: Indices B1 is Subset of Indices B12 by Th25;
A12: len L1=len F1 by CARD_1:def 7;
then
A13: (W1^W2) |min(L,i)=W1|min(L1,i) by A7,A6,A1,FINSEQ_5:22;
A14: min(L1,i)-'1<=min(L1,i) by NAT_D:35;
then
A15: (L1^L2) | (min(L,i)-'1)=L1| (min(L1,i)-'1) by A7,A6,FINSEQ_5:22,XXREAL_0:2
;
A16: (W1^W2) | (min(L,i)-'1)=W1| (min(L1,i)-'1) by A7,A6,A14,A12,A1,FINSEQ_5:22
,XXREAL_0:2;
per cases;
suppose
A17: j <= Sum(W1| (min(L1,i)-'1)) or j > Sum (W1|min(L1,i));
then B1*(i,j)=d by A3,Def5;
hence thesis by A3,A11,A13,A16,A9,A17,Def5;
end;
suppose
A18: j > Sum(W1| (min(L1,i)-'1)) & j<= Sum (W1|min(L1,i));
then
A19: B1*(i,j)= F1.min(L1,i)*(i-'Sum(L1| (min(L1,i)-'1)), j-'Sum (W1| (min(L1
,i )-'1))) by A3,Def5;
B12*(i,j)= F12.min(L1,i)*(i-'Sum(L1| (min(L1,i)-'1)), j-'Sum (W1| (min(
L1,i)-'1))) by A3,A11,A7,A13,A16,A15,A9,A10,A18,Def5;
hence thesis by A5,A8,A19,FINSEQ_1:def 7;
end;
end;
theorem Th27:
[i,j] in Indices block_diagonal(F2,d1) iff i>0 & j>0 & [i+Sum
Len F1,j+Sum Width F1] in Indices block_diagonal(F1^F2,d2)
proof
set B2=block_diagonal(F2,d1);
set B12=block_diagonal(F1^F2,d2);
A1: dom B12=Seg len B12 by FINSEQ_1:def 3;
A2: len B12=Sum Len (F1^F2) by Def5;
(Len F1)^Len F2=Len (F1^F2) by Th14;
then
A3: Sum Len F1+Sum Len F2=Sum Len (F1^F2) by RVSUM_1:75;
A4: len B2=Sum Len F2 by Def5;
(Width F1)^Width F2=Width (F1^F2) by Th18;
then
A5: Sum Width F1+Sum Width F2= Sum Width (F1^F2) by RVSUM_1:75;
A6: width B12=Sum Width (F1^F2) by Def5;
A7: width B2=Sum Width F2 by Def5;
A8: dom B2=Seg len B2 by FINSEQ_1:def 3;
hereby
assume
A9: [i,j] in Indices B2;
then
A10: j in Seg width B2 by ZFMISC_1:87;
then
A11: j+Sum Width F1 in Seg width B12 by A6,A7,A5,FINSEQ_1:60;
A12: i in Seg len B2 by A8,A9,ZFMISC_1:87;
then i +Sum Len F1 in Seg len B12 by A2,A4,A3,FINSEQ_1:60;
hence i>0 & j>0 & [i+Sum Len F1,j+Sum Width F1] in Indices B12 by A1,A12
,A10,A11,ZFMISC_1:87;
end;
assume that
A13: i>0 and
A14: j>0 and
A15: [i+Sum Len F1,j+Sum Width F1] in Indices B12;
i +Sum Len F1 in Seg len B12 by A1,A15,ZFMISC_1:87;
then
A16: i in Seg len B2 by A2,A4,A3,A13,FINSEQ_1:61;
j +Sum Width F1 in Seg width B12 by A15,ZFMISC_1:87;
then
A17: j in Seg width B2 by A6,A7,A5,A14,FINSEQ_1:61;
dom B2=Seg len B2 by FINSEQ_1:def 3;
hence thesis by A16,A17,ZFMISC_1:87;
end;
theorem Th28:
[i,j] in Indices block_diagonal(F2,d) implies block_diagonal(F2,
d)*(i,j) = block_diagonal(F1^F2,d)*(i+Sum Len F1,j+Sum Width F1)
proof
set L1=Len F1;
set W1=Width F1;
set L2=Len F2;
set W2=Width F2;
set F12=F1^F2;
set L=Len F12;
set W=Width F12;
set B2=block_diagonal(F2,d);
set B12=block_diagonal(F12,d);
A1: dom B12=Seg len B12 by FINSEQ_1:def 3;
A2: len B12=Sum L by Def5;
A3: L1^L2=L by Th14;
then
A4: Sum L=Sum L1+Sum L2 by RVSUM_1:75;
assume
A5: [i,j] in Indices B2;
then i>0 by Th27;
then i+Sum L1>0+Sum L1 by XREAL_1:6;
then
A6: not i+Sum L1 in Seg Sum L1 by FINSEQ_1:1;
A7: [i+Sum L1,j+Sum W1] in Indices B12 by A5,Th27;
then i+Sum L1 in dom B12 by ZFMISC_1:87;
then
A8: i+Sum L1 in Seg(Sum L1+Sum L2)\Seg Sum L1 by A4,A1,A2,A6,XBOOLE_0:def 5;
then
A9: min(L,i+Sum L1)=min(L2,(i+Sum L1)-'Sum L1)+len L1 by A3,Th9;
A10: len B2=Sum L2 by Def5;
A11: len W1=len F1 by CARD_1:def 7;
i in dom B2 by A5,ZFMISC_1:87;
then i in Seg len B2 by FINSEQ_1:def 3;
then
A12: min(L2,i) in dom L2 by A10,Def1;
then
A13: min(L2,i)<=len L2 by FINSEQ_3:25;
A14: (i+Sum L1)-'Sum L1=i+Sum L1-Sum L1 by A8,Th9;
A15: (j+Sum W1)-'(Sum W1+Sum (W2| (min(L2,i)-'1)))=j-'Sum (W2| (min(L2,i)-'1))
by PRGCOR_1:1;
A16: len L2=len F2 by CARD_1:def 7;
A17: (i+Sum L1)-'(Sum L1+Sum (L2| (min(L2,i)-'1)))=i-'Sum (L2| (min(L2,i)-'1))
by PRGCOR_1:1;
A18: len F1=len L1 by CARD_1:def 7;
A19: W1^W2=W by Th18;
then W1^(W2| (min(L2,i)))=W|min(L,i+Sum L1) by A11,A18,A9,A14,FINSEQ_6:14;
then
A20: Sum W1+Sum (W2| (min(L2,i))) = Sum (W|min(L,i+Sum L1)) by RVSUM_1:75;
A21: min(L2,i)>=1 by A12,FINSEQ_3:25;
then
A22: min(L2,i)+len L1-'1= (min(L2,i)-'1)+len L1 by NAT_D:38;
then L1^(L2| (min(L2,i)-'1))=L| (min(L,i+Sum L1)-'1) by A3,A9,A14,FINSEQ_6:14
;
then
A23: Sum L1+Sum (L2| (min(L2,i)-'1))=Sum (L| (min(L,i+Sum L1)-'1)) by
RVSUM_1:75;
W1^(W2| (min(L2,i)-'1))=W| (min(L,i+Sum L1)-'1) by A19,A11,A18,A9,A14,A22,
FINSEQ_6:14;
then
A24: Sum W1+Sum (W2| (min(L2,i)-'1))=Sum (W| (min(L,i+Sum L1)-'1)) by
RVSUM_1:75;
per cases;
suppose
A25: j <= Sum(W2| (min(L2,i)-'1)) or j > Sum (W2|min(L2,i));
then
j+Sum W1<= Sum (W| (min(L,i+Sum L1)-'1)) or j+Sum W1 > Sum (W|min(L,i+
Sum L1)) by A20,A24,XREAL_1:7,8;
then B12*(i+Sum L1,j+Sum W1)=d by A7,Def5;
hence thesis by A5,A25,Def5;
end;
suppose
A26: j > Sum(W2| (min(L2,i)-'1)) & j <= Sum (W2|min(L2,i));
then
A27: j+Sum W1 <= Sum (W|min(L,i+Sum L1)) by A20,XREAL_1:7;
A28: B2*(i,j)=F2.min(L2,i)*(i-'Sum(L2| (min(L2,i)-'1)), j-'Sum (W2| (min(L2,
i) -'1))) by A5,A26,Def5;
j+Sum W1> Sum (W| (min(L,i+Sum L1)-'1)) by A24,A26,XREAL_1:8;
then
B12*(i+Sum L1,j+Sum W1)=F12.min(L,i+Sum L1)* (i-'Sum (L2| (min(L2,i)-'
1) ), j-'Sum (W2| (min(L2,i)-'1))) by A7,A24,A23,A17,A15,A27,Def5;
hence thesis by A18,A16,A21,A13,A9,A14,A28,FINSEQ_1:65;
end;
end;
theorem Th29:
[i,j] in Indices block_diagonal(F1^F2,d) & (i <= Sum Len F1 & j
> Sum Width F1 or i > Sum Len F1 & j <= Sum Width F1) implies block_diagonal(F1
^F2,d)*(i,j) = d
proof
set L1=Len F1;
set W1=Width F1;
set L2=Len F2;
set W2=Width F2;
set F12=F1^F2;
set L=Len F12;
set W=Width F12;
set B12=block_diagonal(F12,d);
A1: dom B12=Seg len B12 by FINSEQ_1:def 3;
A2: len W1=len F1 by CARD_1:def 7;
A3: len B12=Sum L by Def5;
A4: len F1=len L1 by CARD_1:def 7;
assume that
A5: [i,j] in Indices block_diagonal(F1^F2,d) and
A6: i <= Sum Len F1 & j > Sum Width F1 or i > Sum Len F1 & j <= Sum Width F1;
i in dom B12 by A5,ZFMISC_1:87;
then
A7: 1<=i by FINSEQ_3:25;
A8: W1^W2=W by Th18;
A9: L1^L2=L by Th14;
then
A10: Sum L=Sum L1+Sum L2 by RVSUM_1:75;
per cases by A6;
suppose
A11: i <= Sum Len F1 & j > Sum Width F1;
then
A12: i in Seg Sum L1 by A7;
then min(L1,i) in dom L1 by Def1;
then min(L1,i)<=len L1 by FINSEQ_3:25;
then
A13: Sum (W|min(L1,i))<= Sum(W| (len L1)) by POLYNOM3:18;
A14: W| (len L1)=W1 by A8,A2,A4,FINSEQ_5:23;
min(L,i)=min(L1,i) by A9,A12,Th8;
then Sum(W|min(L,i))<j by A11,A14,A13,XXREAL_0:2;
hence thesis by A5,Def5;
end;
suppose
A15: i > Sum L1 & j <= Sum W1;
A16: i in Seg Sum L by A1,A3,A5,ZFMISC_1:87;
not i in Seg Sum L1 by A15,FINSEQ_1:1;
then
A17: i in Seg (Sum L1+Sum L2)\Seg Sum L1 by A10,A16,XBOOLE_0:def 5;
then
A18: i-'Sum L1=i-Sum L1 by Th9;
then
A19: i=(i-'Sum L1)+Sum L1;
i-'Sum L1<>0 by A15,A18;
then i-'Sum L1 in Seg Sum L2 by A10,A16,A19,FINSEQ_1:61;
then min(L2,i-'Sum L1) in dom L2 by Def1;
then
A20: min(L2,i-'Sum L1) >=1 by FINSEQ_3:25;
min(L,i)=(min(L2,i-'Sum L1))+len L1 by A9,A17,Th9;
then min(L,i)-'1=(min(L2,i-'Sum L1)-'1)+len L1 by A20,NAT_D:38;
then min(L,i)-'1>=len L1+0 by XREAL_1:7;
then
A21: Sum(W| (min(L,i)-'1))>=Sum ((W1^W2) |len W1) by A8,A2,A4,POLYNOM3:18;
(W1^W2) |len W1=W1 by FINSEQ_5:23;
then Sum(W| (min(L,i)-'1))>=j by A15,A21,XXREAL_0:2;
hence thesis by A5,Def5;
end;
end;
theorem Th30:
for i,j,k st i in dom F & [j,k] in Indices F.i holds [j+Sum ((
Len F) | (i-'1)), k+Sum((Width F) | (i-'1))] in Indices block_diagonal(F,d) &
(F.i)*(j,k) = block_diagonal(F,d)*(j+Sum ((Len F) | (i-'1)), k+Sum((Width F) |
(i-'1)))
proof
let i,j,k such that
A1: i in dom F and
A2: [j,k] in Indices F.i;
set Fi=F.i;
A3: k in Seg width Fi by A2,ZFMISC_1:87;
set L=Len F;
len F=len L by CARD_1:def 7;
then
A4: L| (len F)=L by FINSEQ_1:58;
A5: i<=len F by A1,FINSEQ_3:25;
then Sum (L|i)<=Sum(L| (len F)) by POLYNOM3:18;
then
A6: Seg Sum (L|i) c= Seg Sum L by A4,FINSEQ_1:5;
A7: dom F=dom L by Def3;
then
A8: L.i=L/.i by A1,PARTFUN1:def 6;
set W=Width F;
A9: dom F=dom W by Def4;
then
A10: W.i=W/.i by A1,PARTFUN1:def 6;
set kS=k+Sum(W| (i-'1));
W.i=width Fi by A1,A9,Def4;
then
A11: kS in Seg Sum (W|i) by A1,A9,A3,A10,Th10;
then
A12: kS <= Sum(W|i) by FINSEQ_1:1;
len F=len W by CARD_1:def 7;
then
A13: W| (len F)=W by FINSEQ_1:58;
set B=block_diagonal(F,d);
A14: len B=Sum L by Def5;
A15: width B=Sum W by Def5;
set jS=j+Sum(L| (i-'1));
j in dom Fi by A2,ZFMISC_1:87;
then
A16: j in Seg len Fi by FINSEQ_1:def 3;
Sum(W|i)<=Sum (W| (len F)) by A5,POLYNOM3:18;
then
A17: Seg Sum (W|i) c= Seg Sum W by A13,FINSEQ_1:5;
Sum(L| (i-'1))+0<=jS by XREAL_1:6;
then
A18: jS-'Sum(L| (i-'1))=jS-Sum(L| (i-'1)) by XREAL_1:233;
A19: L.i=len Fi by A1,A7,Def3;
then
A20: min(L,jS)=i by A1,A7,A16,A8,Th10;
jS in Seg Sum (L|i) by A1,A7,A16,A8,A19,Th10;
then [jS,kS] in [:Seg len B,Seg width B:] by A14,A15,A11,A6,A17,ZFMISC_1:87;
hence
A21: [jS,kS] in Indices B by FINSEQ_1:def 3;
0<k by A3;
then
A22: Sum(W| (i-'1))+0<kS by XREAL_1:6;
then kS-'Sum(W| (i-'1))=kS- Sum(W| (i-'1)) by XREAL_1:233;
hence thesis by A20,A21,A22,A12,A18,Def5;
end;
theorem Th31:
i in dom F implies F.i = Segm(block_diagonal(F,d),(Seg Sum((Len
F) |i))\Seg Sum((Len F) | (i-'1)), (Seg Sum((Width F) |i))\Seg Sum((Width F)
| (i-'1)
))
proof
assume
A1: i in dom F;
set L=Len F;
set Fi=F.i;
A2: dom F=dom L by Def3;
then
A3: len Fi=L.i by A1,Def3;
set SL=Sum(L|i);
set SL1=Sum(L| (i-'1));
A4: SL1+L.i=SL by A1,A2,Lm2;
reconsider FI=Fi as Matrix of len Fi,width Fi,D by MATRIX_0:51;
set B=block_diagonal(F,d);
set W=Width F;
set SW1=Sum(W| (i-'1));
set SW=Sum(W|i);
A5: dom F=dom W by Def4;
then
A6: SW1+W.i=SW by A1,Lm2;
SL1 <= SL by NAT_D:35,POLYNOM3:18;
then Seg SL1 c= Seg SL by FINSEQ_1:5;
then
A7: card (Seg SL\Seg SL1) = card Seg SL-card Seg SL1 by CARD_2:44
.= SL-card Seg SL1 by FINSEQ_1:57
.= SL1+(L.i)-SL1 by A4,FINSEQ_1:57
.= len Fi by A1,A2,Def3;
SW1 <=SW by NAT_D:35,POLYNOM3:18;
then Seg SW1 c= Seg SW by FINSEQ_1:5;
then
A8: card (Seg SW\Seg SW1) = card Seg SW-card Seg SW1 by CARD_2:44
.= SW-card Seg SW1 by FINSEQ_1:57
.= SW1+(W.i)-SW1 by A6,FINSEQ_1:57
.= width Fi by A1,A5,Def4;
A9: width Fi=W.i by A1,A5,Def4;
now
A10: Indices FI = Indices Segm(B,Seg SL\Seg SL1,Seg SW\Seg SW1) by A7,A8,
MATRIX_0:26;
A11: dom FI=Seg (L.i) by A3,FINSEQ_1:def 3;
let j,k such that
A12: [j,k] in Indices FI;
k in Seg (W.i) by A9,A12,ZFMISC_1:87;
then
A13: Sgm(Seg SW\Seg SW1).k=k+SW1 by A6,MATRIX15:8;
j in dom FI by A12,ZFMISC_1:87;
then Sgm(Seg SL\Seg SL1).j=j+SL1 by A4,A11,MATRIX15:8;
hence
Segm(B,Seg SL\Seg SL1,Seg SW\Seg SW1)*(j,k) = B*(j+SL1,k+SW1) by A12,A10
,A13,MATRIX13:def 1
.= Fi*(j,k) by A1,A12,Th30;
end;
hence thesis by A7,A8,MATRIX_0:27;
end;
theorem Th32:
M = Segm(block_diagonal(<*M*>^F,d),Seg len M,Seg width M)
proof
set MF=<*M*>^F;
set L=Len MF;
set W=Width MF;
A1: Seg Sum (L|0)={} by RVSUM_1:72;
A2: Seg Sum (W|0)={} by RVSUM_1:72;
A3: Len<*M*>=<*len M*> by Th15;
A4: len <*len M*>=1 by FINSEQ_1:39;
L=Len<*M*>^Len F by Th14;
then L|1=<*len M*> by A3,A4,FINSEQ_5:23;
then
A5: Sum (L|1)=len M by RVSUM_1:73;
A6: len <*width M*>=1 by FINSEQ_1:39;
A7: Width <*M*>=<*width M*> by Th19;
A8: MF.1=M by FINSEQ_1:41;
1 in Seg 1;
then
A9: 1 in dom <*M*> by FINSEQ_1:38;
A10: dom <*M*> c= dom MF by FINSEQ_1:26;
W=Width <*M*>^Width F by Th18;
then
A11: W|1=<*width M*> by A7,A6,FINSEQ_5:23;
1-'1=0 by XREAL_1:232;
hence M = Segm(block_diagonal(MF,d),(Seg Sum (L|1))\{}, (Seg Sum (W|1))\{})
by A1,A2,A9,A10,A8,Th31
.= Segm(block_diagonal(MF,d),Seg len M,Seg width M) by A11,A5,RVSUM_1:73;
end;
theorem Th33:
M = Segm(block_diagonal(F^<*M*>,d),Seg (len M+Sum Len F)\Seg Sum
Len F, Seg (width M+Sum Width F)\Seg Sum Width F)
proof
set FM=F^<*M*>;
set L=Len FM;
set W=Width FM;
set 1F=1+len F;
A1: len FM=1F by FINSEQ_2:16;
len L=len FM by CARD_1:def 7;
then
A2: L|1F=L by A1,FINSEQ_1:58;
len W=len FM by CARD_1:def 7;
then
A3: W|1F=W by A1,FINSEQ_1:58;
1F in Seg (len F+1) by FINSEQ_1:4;
then
A4: 1F in dom FM by A1,FINSEQ_1:def 3;
A5: W=Width F^Width<*M*> by Th18;
len Width F=len F by CARD_1:def 7;
then
A6: W| (len F)=Width F by A5,FINSEQ_5:23;
Width <*M*>=<*width M*> by Th19;
then
A7: Sum W=Sum Width F+width M by A5,RVSUM_1:74;
A8: L = Len F ^ Len <*M*> by Th14;
len Len F=len F by CARD_1:def 7;
then
A9: L| (len F)=Len F by A8,FINSEQ_5:23;
Len <*M*>=<*len M*> by Th15;
then
A10: Sum L=Sum Len F+len M by A8,RVSUM_1:74;
A11: FM.1F=M by FINSEQ_1:42;
1F-'1=1F-1 by NAT_D:37;
hence thesis by A9,A6,A10,A7,A4,A11,A3,A2,Th31;
end;
theorem Th34:
block_diagonal(<*M*>,d) = M
proof
reconsider E=<*>(D**) as Matrix-yielding FinSequence of (D**) by Th12;
set ME=<*M*>^E;
set B=block_diagonal(<*M*>,d);
A1: len B = Sum Len <*M*> by Def5
.= len M by Lm4;
A2: width B = Sum Width <*M*> by Def5
.= width M by Lm5;
ME = <*M*> by FINSEQ_1:34;
hence M = Segm(B,Seg len M,Seg width M) by Th32
.= B by A1,A2,MATRIX13:46;
end;
theorem Th35:
block_diagonal(F1^F2,d) = block_diagonal(<*block_diagonal(F1,d) *>^F2,d)
proof
set F12=F1^F2;
set D1=block_diagonal(F1,d);
set D2=block_diagonal(F2,d);
set D12=block_diagonal(F12,d);
set DF=<*D1*>^F2;
set DF2=block_diagonal(DF,d);
set LF1=Len F1;
set WF1=Width F1;
set LF2=Len F2;
set WF2=Width F2;
set LF=Len F12;
set WF=Width F12;
A1: LF = LF1^LF2 by Th14;
len D12= Sum LF by Def5;
then
A2: len D12=Sum LF1+Sum LF2 by A1,RVSUM_1:75;
A3: Len <*D1*>=<*len D1*> by Th15;
then
A4: Sum Len<*D1*>=len D1 by RVSUM_1:73;
A5: block_diagonal(<*D1*>,d)=D1 by Th34;
A6: Sum WF1=width D1 by Def5;
A7: Len DF=(Len <*D1*>)^LF2 by Th14;
A8: WF=WF1^WF2 by Th18;
len DF2=Sum Len DF by Def5;
then
A9: len DF2=len D1+Sum LF2 by A7,A3,RVSUM_1:76;
A10: Width <*D1*>=<*width D1*> by Th19;
then
A11: Sum Width <*D1*> =width D1 by RVSUM_1:73;
A12: Sum LF1=len D1 by Def5;
A13: width D1=Sum WF1 by Def5;
A14: width D12 = Sum WF by Def5;
then
A15: width D12=Sum WF1+Sum WF2 by A8,RVSUM_1:75;
A16: Width DF=( Width<*D1*>)^WF2 by Th18;
A17: len D1=Sum LF1 by Def5;
width DF2=Sum Width DF by Def5;
then
A18: width DF2=width D1+Sum WF2 by A16,A10,RVSUM_1:76;
A19: Indices D12 = [:Seg len D12,Seg width D12:] by FINSEQ_1:def 3
.= Indices DF2 by A2,A15,A17,A13,A9,A18,FINSEQ_1:def 3;
now
A20: dom D12=Seg len D12 by FINSEQ_1:def 3;
let i,j such that
A21: [i,j] in Indices D12;
i in dom D12 by A21,ZFMISC_1:87;
then
A22: 1<=i by A20,FINSEQ_1:1;
j in Seg width D12 by A21,ZFMISC_1:87;
then
A23: 1<=j by FINSEQ_1:1;
now
per cases;
suppose
A24: i <= Sum LF1 & j<=Sum WF1;
then
A25: i in dom D1 by A12,A22,FINSEQ_3:25;
j in Seg width D1 by A6,A23,A24;
then
A26: [i,j] in Indices D1 by A25,ZFMISC_1:87;
hence D12*(i,j) = D1*(i,j) by Th26
.= DF2*(i,j) by A5,A26,Th26;
end;
suppose
A27: i> Sum LF1 & j <=Sum WF1 or i<= Sum LF1 & j >Sum WF1;
hence D12*(i,j) = d by A21,Th29
.= DF2*(i,j) by A17,A13,A4,A11,A19,A21,A27,Th29;
end;
suppose
A28: i > Sum LF1 & j>Sum WF1;
then reconsider ii=i-Sum LF1,jj=j-Sum WF1 as Element of NAT by NAT_1:21
;
A29: jj<>0 by A28;
A30: i=ii+Sum LF1;
A31: j=jj+Sum WF1;
ii<>0 by A28;
then
A32: [ii,jj] in Indices D2 by A21,A30,A31,A29,Th27;
hence D12*(i,j) = D2*(ii,jj) by A30,A31,Th28
.= DF2*(i,j) by A17,A13,A4,A11,A30,A31,A32,Th28;
end;
end;
hence D12*(i,j)=DF2*(i,j);
end;
hence thesis by A14,A8,A2,A17,A13,A9,A18,MATRIX_0:21,RVSUM_1:75;
end;
theorem Th36:
block_diagonal(F1^F2,d) = block_diagonal(F1^<*block_diagonal(F2, d)*>,d)
proof
set F12=F1^F2;
set D1=block_diagonal(F1,d);
set D2=block_diagonal(F2,d);
set D12=block_diagonal(F12,d);
set FD=F1^<*D2*>;
set FD2=block_diagonal(FD,d);
set LF1=Len F1;
set WF1=Width F1;
set LF2=Len F2;
set WF2=Width F2;
set LF=Len F12;
set WF=Width F12;
A1: LF = LF1^LF2 by Th14;
len D12= Sum LF by Def5;
then
A2: len D12=Sum LF1+Sum LF2 by A1,RVSUM_1:75;
A3: Sum Width <*D2*>=width D2 by Lm5;
A4: Len FD=LF1^Len <*D2*> by Th14;
len FD2=Sum Len FD by Def5;
then
A5: len FD2=Sum Len <*D2*>+Sum LF1 by A4,RVSUM_1:75;
A6: Sum LF1=len D1 by Def5;
A7: WF = WF1^WF2 by Th18;
A8: Width FD=WF1^Width<*D2*> by Th18;
width FD2=Sum Width FD by Def5;
then
A9: width FD2=Sum Width <*D2*> +Sum WF1 by A8,RVSUM_1:75;
A10: Sum WF1=width D1 by Def5;
A11: len D2=Sum LF2 by Def5;
A12: width D12 = Sum WF by Def5;
then
A13: width D12=Sum WF1+Sum WF2 by A7,RVSUM_1:75;
A14: Sum Len <*D2*> =len D2 by Lm4;
A15: block_diagonal(<*D2*>,d)=D2 by Th34;
A16: width D2=Sum WF2 by Def5;
A17: Indices D12 = [:Seg len D12,Seg width D12:] by FINSEQ_1:def 3
.= Indices FD2 by A2,A13,A11,A16,A5,A9,A14,A3,FINSEQ_1:def 3;
now
A18: dom D12=Seg len D12 by FINSEQ_1:def 3;
let i,j such that
A19: [i,j] in Indices D12;
i in dom D12 by A19,ZFMISC_1:87;
then
A20: 1<=i by A18,FINSEQ_1:1;
j in Seg width D12 by A19,ZFMISC_1:87;
then
A21: 1<=j by FINSEQ_1:1;
now
per cases;
suppose
A22: i <= Sum LF1 & j<=Sum WF1;
then
A23: i in dom D1 by A6,A20,FINSEQ_3:25;
j in Seg width D1 by A10,A21,A22;
then
A24: [i,j] in Indices D1 by A23,ZFMISC_1:87;
hence D12*(i,j) = D1*(i,j) by Th26
.= FD2*(i,j) by A24,Th26;
end;
suppose
A25: i> Sum LF1 & j <=Sum WF1 or i<= Sum LF1 & j >Sum WF1;
hence D12*(i,j) = d by A19,Th29
.= FD2*(i,j) by A17,A19,A25,Th29;
end;
suppose
A26: i > Sum LF1 & j>Sum WF1;
then reconsider ii=i-Sum LF1,jj=j-Sum WF1 as Element of NAT by NAT_1:21
;
A27: jj<>0 by A26;
A28: i=ii+Sum LF1;
A29: j=jj+Sum WF1;
ii<>0 by A26;
then
A30: [ii,jj] in Indices D2 by A19,A28,A29,A27,Th27;
hence D12*(i,j) = D2*(ii,jj) by A28,A29,Th28
.= FD2*(i,j) by A15,A28,A29,A30,Th28;
end;
end;
hence D12*(i,j)=FD2*(i,j);
end;
hence thesis by A12,A7,A2,A11,A16,A5,A9,A14,A3,MATRIX_0:21,RVSUM_1:75;
end;
theorem
i in Seg Sum Len F & m = min(Len F,i) implies Line(block_diagonal(F,d)
,i) = (Sum (Width F| (m-'1)) |->d)^ Line(F.m,i-'Sum (Len F| (m-'1)))^
((Sum Width F-'Sum (Width F|m)) |->d)
proof
assume that
A1: i in Seg Sum Len F and
A2: m = min(Len F,i);
set L=Len F;
A3: (L|m).m =L.m by FINSEQ_3:112;
set BF9m=block_diagonal(F/^m,d);
set BFm=block_diagonal(F|m,d);
A4: len BFm = Sum Len (F|m) by Def5
.= Sum (L|m) by Th17;
F=(F|m)^(F/^m) by RFINSEQ:8;
then
A5: block_diagonal(F,d) = block_diagonal((F|m)^<*BF9m*>,d) by Th36
.= block_diagonal(<*BFm,BF9m*>,d) by Th35;
then Sum Width F = width block_diagonal(<*BFm,BF9m*>,d) by Def5
.= Sum Width <*BFm,BF9m*> by Def5
.= width BFm + width BF9m by Th20
.= Sum (Width F|m)+width BF9m by Def5;
then
A6: Sum Width F-'Sum (Width F|m) = (Sum (Width F|m)+width BF9m)-Sum (Width
F|m) by NAT_1:11,XREAL_1:233
.= width BF9m;
Sum(L| (m-'1))<i by A1,A2,Th7;
then
A7: i-Sum(L| (m-'1))=i-'Sum(L| (m-'1)) by XREAL_1:233;
A8: m in dom L by A1,A2,Def1;
then 1 <= m by FINSEQ_3:25;
then m-'1=m-1 by XREAL_1:233;
then
A9: m=m-'1+1;
then m-'1<=m by NAT_1:11;
then
A10: Seg (m-'1) c= Seg m by FINSEQ_1:5;
then
A11: (F|m) | (m-'1)=F| (m-'1) by RELAT_1:74;
m <= len L by A8,FINSEQ_3:25;
then len (L|m)=m by FINSEQ_1:59;
then
A12: L|m=((L|m) | (m-'1))^<*(L|m).m*> by A9,FINSEQ_3:55;
(L|m) | (m-'1)=L| (m-'1) by A10,RELAT_1:74;
then Sum (L|m) = Sum (L| (m-'1))+L.m by A12,A3,RVSUM_1:74
.= Sum (L| (m-'1))+len (F.m) by A8,Def3;
then len (F.m)+Sum (L| (m-'1))>=i-'Sum(L| (m-'1))+Sum (L| (m-'1)) by A1,A2,A7
,Def1;
then
A13: len (F.m)>=i-'Sum(L| (m-'1)) by XREAL_1:6;
i-Sum(L| (m-'1))<>0 by A1,A2,Th7;
then i-'Sum(L| (m-'1))>=1 by A7,NAT_1:14;
then
A14: i-'Sum(L| (m-'1)) in dom (F.m) by A13,FINSEQ_3:25;
set BFm1=block_diagonal(F| (m-'1),d);
A15: (F|m).m =F.m by FINSEQ_3:112;
A16: width BFm1 = Sum Width (F| (m-'1)) by Def5
.= Sum ((Width F) | (m-'1)) by Th21;
A17: 1<=i by A1,FINSEQ_1:1;
i <= Sum(L|m) by A1,A2,Def1;
then i in dom BFm by A17,A4,FINSEQ_3:25;
then
A18: Line(block_diagonal(F,d),i) = Line(BFm,i)^(width BF9m|->d) by A5,Th23;
dom L=dom F by Def3;
then m <= len F by A8,FINSEQ_3:25;
then len (F|m)=m by FINSEQ_1:59;
then F|m=((F|m) | (m-'1))^<*(F|m).m*> by A9,FINSEQ_3:55;
then
A19: BFm=block_diagonal(<*BFm1,F.m*>,d) by A15,A11,Th35;
len BFm1 = Sum Len (F| (m-'1)) by Def5
.= Sum (L| (m-'1)) by Th17;
then (Sum ((Width F) | (m-'1)) |->d)^Line(F.m,i-'Sum(L| (m-'1))) =
Line(BFm,Sum
(L| (m-'1))+(i-'Sum(L| (m-'1)))) by A14,A16,A19,Th23
.= Line(BFm,i) by A7;
then Line(BFm,i)=(Sum (Width F| (m-'1)) |->d)^ Line(F.m,i-'Sum (L| (m-'1)))
by Th21;
hence thesis by A6,A18,Th17;
end;
theorem
i in Seg Sum Width F & m = min(Width F,i) implies Col(block_diagonal(F
,d),i) = (Sum (Len F| (m-'1)) |->d)^ Col(F.m,i-'Sum (Width F| (m-'1)))^
((Sum Len F-'Sum (Len F|m)) |->d)
proof
assume that
A1: i in Seg Sum Width F and
A2: m = min(Width F,i);
set W=Width F;
A3: (W|m).m =W.m by FINSEQ_3:112;
set BF9m=block_diagonal(F/^m,d);
set BFm=block_diagonal(F|m,d);
set L=Len F;
A4: width BFm = Sum Width (F|m) by Def5
.= Sum (W|m) by Th21;
F=(F|m)^(F/^m) by RFINSEQ:8;
then
A5: block_diagonal(F,d) = block_diagonal((F|m)^<*BF9m*>,d) by Th36
.= block_diagonal(<*BFm,BF9m*>,d) by Th35;
then Sum L = len block_diagonal(<*BFm,BF9m*>,d) by Def5
.= Sum Len <*BFm,BF9m*> by Def5
.= len BFm + len BF9m by Th16
.= Sum (Len F|m)+len BF9m by Def5;
then
A6: Sum Len F-'Sum (Len F|m) = (Sum (Len F|m)+len BF9m)-Sum (Len F|m) by
NAT_1:11,XREAL_1:233
.= len BF9m;
Sum(W| (m-'1))<i by A1,A2,Th7;
then
A7: i-Sum(W| (m-'1))=i-'Sum(W| (m-'1)) by XREAL_1:233;
A8: m in dom W by A1,A2,Def1;
then 1 <= m by FINSEQ_3:25;
then m-'1=m-1 by XREAL_1:233;
then
A9: m=m-'1+1;
then m -' 1<=m by NAT_1:11;
then
A10: Seg (m-'1) c= Seg m by FINSEQ_1:5;
then
A11: (F|m) | (m-'1)=F| (m-'1) by RELAT_1:74;
m <= len W by A8,FINSEQ_3:25;
then len (W|m)=m by FINSEQ_1:59;
then
A12: W|m=((W|m) | (m-'1))^<*(W|m).m*> by A9,FINSEQ_3:55;
(W|m) | (m-'1)=W| (m-'1) by A10,RELAT_1:74;
then Sum (W|m) = Sum (W| (m-'1))+W.m by A12,A3,RVSUM_1:74
.= Sum (W| (m-'1))+width (F.m) by A8,Def4;
then
width (F.m)+Sum (W| (m-'1))>=i-'Sum(W| (m-'1))+Sum (W| (m-'1)) by A1,A2,A7
,Def1;
then
A13: width (F.m)>=i-'Sum(W| (m-'1)) by XREAL_1:6;
i-Sum(W| (m-'1))<>0 by A1,A2,Th7;
then i-'Sum(W| (m-'1))>=1 by A7,NAT_1:14;
then
A14: i-'Sum(W| (m-'1)) in Seg width (F.m) by A13;
set BFm1=block_diagonal(F| (m-'1),d);
A15: (F|m).m =F.m by FINSEQ_3:112;
A16: width BFm1 = Sum Width (F| (m-'1)) by Def5
.= Sum (W| (m-'1)) by Th21;
A17: 1<=i by A1,FINSEQ_1:1;
i <= Sum(W|m) by A1,A2,Def1;
then i in Seg width BFm by A17,A4;
then
A18: Col(block_diagonal(F,d),i) = Col(BFm,i)^(len BF9m|->d) by A5,Th24;
dom W=dom F by Def4;
then m <= len F by A8,FINSEQ_3:25;
then len (F|m)=m by FINSEQ_1:59;
then F|m=((F|m) | (m-'1))^<*(F|m).m*> by A9,FINSEQ_3:55;
then
A19: BFm=block_diagonal(<*BFm1,F.m*>,d) by A15,A11,Th35;
len BFm1 = Sum Len (F| (m-'1)) by Def5
.= Sum (L| (m-'1)) by Th17;
then
(Sum (L| (m-'1)) |->d)^Col(F.m,i-'Sum(W| (m-'1))) = Col(BFm,Sum (W| (m-'1))
+(i-'Sum(W| (m-'1)))) by A14,A16,A19,Th24
.= Col(BFm,i) by A7;
then Col(BFm,i) = (Sum (Len F| (m-'1)) |->d)^Col(F.m,i-'Sum (W| (m-'1)))by
Th17;
hence thesis by A6,A18,Th21;
end;
theorem
for M1,M2,N1,N2 be Matrix of D st len M1=len N1 & width M1=width N1 &
len M2=len N2 & width M2=width N2 & block_diagonal(<*M1,M2*>,d1) =
block_diagonal(<*N1,N2*>,d2) holds M1 = N1 & M2= N2
proof
let M1,M2,N1,N2 be Matrix of D such that
A1: len M1=len N1 and
A2: width M1=width N1 and
A3: len M2=len N2 and
A4: width M2=width N2 and
A5: block_diagonal(<*M1,M2*>,d1) = block_diagonal(<*N1,N2*>,d2);
set G1=<*N1*>;
set F1=<*M1*>;
reconsider W1=width M1 as Element of NAT by ORDINAL1:def 12;
A6: Sum Width F1 = Sum <*W1*> by Th19
.= Sum Width G1 by A2,Th19;
set G2=<*N2*>;
set F2=<*M2*>;
thus M1 = Segm(block_diagonal(F1^F2,d1),Seg len M1,Seg width M1) by Th32
.= Segm(block_diagonal(G1^G2,d2),Seg len N1,Seg width N1) by A1,A2,A5
.= N1 by Th32;
A7: Sum Len F1 = Sum <*len M1*> by Th15
.= Sum Len G1 by A1,Th15;
thus M2 = Segm(block_diagonal(F1^F2,d1), Seg (len M2+Sum Len F1)\Seg Sum Len
F1, Seg (width M2+Sum Width F1)\Seg Sum Width F1) by Th33
.= N2 by A3,A4,A5,A7,A6,Th33;
end;
theorem Th40:
M={} implies block_diagonal(F^<*M*>,d) = block_diagonal(F,d) &
block_diagonal(<*M*>^F,d) = block_diagonal(F,d)
proof
set MM=<*M*>;
set bf=block_diagonal(F,d);
set BF=<*bf*>;
set bFM=block_diagonal(BF^MM,d);
set bMF=block_diagonal(MM^BF,d);
set BFM=block_diagonal(F^MM,d);
set BMF=block_diagonal(MM^F,d);
A1: width bMF=Sum Width(MM^BF) by Def5;
A2: Len(BF^MM)=Len BF^Len MM by Th14;
A3: Sum Len BF=len bf by Lm4;
assume
A4: M={};
then
A5: len M=0;
then
A6: Sum Len MM=0 by Lm4;
A7: width M=0 by A4,CARD_1:27,MATRIX_0:def 3;
then
A8: Sum Width MM=0 by Lm5;
A9: Sum Len MM=len M by Lm4;
A10: Seg Sum Width MM = {} by A8;
len bFM=Sum Len(BF^MM) by Def5;
then
A11: len bFM=len bf + len M by A2,A9,A3,RVSUM_1:75;
A12: Len(MM^BF) = Len MM^Len BF by Th14;
len bMF=Sum Len(MM^BF) by Def5;
then
A13: len bMF=len M+len bf by A12,A9,A3,RVSUM_1:75;
A14: Width (MM^BF)= Width MM^Width BF by Th18;
A15: Width(BF^MM)=Width BF^Width MM by Th18;
A16: Sum Width MM=width M by Lm5;
A17: Sum Width BF=width bf by Lm5;
width bFM=Sum Width(BF^MM) by Def5;
then
A18: width bFM=width bf+width M by A15,A16,A17,RVSUM_1:75;
thus BFM = bFM by Th35
.= Segm(bFM,Seg len bFM,Seg width bFM) by MATRIX13:46
.= bf by A5,A7,A11,A18,Th32;
thus BMF = bMF by Th36
.= Segm(bMF,Seg len bMF,Seg width bMF) by MATRIX13:46
.= Segm(bMF,Seg(len bf+Sum Len MM)\Seg Sum Len MM, Seg (width bf+Sum
Width MM)\Seg Sum Width MM) by A5,A1,A14,A17,A13,A6,A8,A10,RVSUM_1:75
.= bf by Th33;
end;
theorem Th41:
i in dom A & width A = width DelLine(A,i) implies DelLine(
block_diagonal(<*A*>^G,a),i) = block_diagonal(<*DelLine(A,i)*>^G,a)
proof
assume that
A1: i in dom A and
A2: width A= width DelLine(A,i);
A3: i in Seg len A by A1,FINSEQ_1:def 3;
set da=DelLine(A,i);
consider m such that
A4: len A = m + 1 and
A5: len da = m by A1,FINSEQ_3:104;
set bG=block_diagonal(G,a);
set DA=<*da*>;
set AA=<*A*>;
set BG=<*bG*>;
set bAG=block_diagonal(<*A,bG*>,a);
set bdAG=block_diagonal(<*da,bG*>,a);
A6: Seg len bAG=dom bAG by FINSEQ_1:def 3;
A7: len bAG=Sum Len (AA^BG) by Def5;
then
A8: len bAG=len A +len bG by Th16;
then len bAG>=len A by NAT_1:11;
then
A9: Seg len A c= Seg len bAG by FINSEQ_1:5;
A10: len bdAG=Sum Len (DA^BG) by Def5;
then
A11: len bdAG=m+len bG by A5,Th16;
A12: len bAG=(m+len bG) +1 by A4,A8;
A13: len bdAG=len da +len bG by A10,Th16;
A14: now
m+len bG <=len bAG by A12,NAT_1:11;
then
A15: Seg (m+len bG) c= Seg len bAG by FINSEQ_1:5;
reconsider da9=da as Matrix of len da,width da,K by MATRIX_0:51;
reconsider A9=A as Matrix of len A,width A,K by MATRIX_0:51;
let j such that
A16: 1<=j and
A17: j<=m+len bG;
A18: j in Seg (m+len bG) by A16,A17;
A19: 1<=1+j by NAT_1:11;
j+1<=len bAG by A12,A17,XREAL_1:7;
then
A20: j+1 in Seg len bAG by A19;
now
per cases;
suppose
A21: j<i;
i<=len A by A3,FINSEQ_1:1;
then
A22: j<len A by A21,XXREAL_0:2;
then
A23: j<=m by A4,NAT_1:13;
then
A24: j in dom da by A5,A16,FINSEQ_3:25;
A25: j in dom A by A16,A22,FINSEQ_3:25;
A26: j in Seg m by A16,A23;
j in Seg len A by A16,A22;
then
A27: Line(A9,j) = A.j by MATRIX_0:52
.= da9.j by A21,FINSEQ_3:110
.= Line(da,j) by A5,A26,MATRIX_0:52;
thus Del(bAG,i).j = bAG.j by A21,FINSEQ_3:110
.= Line(bAG,j) by A7,A18,A15,MATRIX_0:52
.= Line(da,j)^(width bG |-> a) by A25,A27,Th23
.= Line(bdAG,j) by A24,Th23
.= bdAG.j by A5,A10,A13,A18,MATRIX_0:52;
end;
suppose
A28: j>=i;
then
A29: Del(bAG,i).j = bAG.(j+1) by A12,A9,A3,A6,A17,FINSEQ_3:111
.= Line(bAG,j+1) by A7,A20,MATRIX_0:52;
now
per cases;
suppose
A30: j+1<=len A;
then
A31: j+1 in dom A by A19,FINSEQ_3:25;
A32: j<=m by A4,A30,XREAL_1:8;
then
A33: j in Seg m by A16;
A34: j in dom da by A5,A16,A32,FINSEQ_3:25;
j+1 in Seg len A by A19,A30;
then Line(A9,j+1) = A.(j+1) by MATRIX_0:52
.= da9.j by A1,A4,A28,A32,FINSEQ_3:111
.= Line(da,j) by A5,A33,MATRIX_0:52;
hence Del(bAG,i).j = Line(da,j)^(width bG |-> a) by A29,A31,Th23
.= Line(bdAG,j) by A34,Th23;
end;
suppose
A35: j+1>len A;
then reconsider jL=j+1-len A as Element of NAT by NAT_1:21;
jL<>0 by A35;
then
A36: jL>=1 by NAT_1:14;
jL+len A<=len bG+len A by A8,A12,A17,XREAL_1:7;
then jL<=len bG by XREAL_1:8;
then
A37: jL in dom bG by A36,FINSEQ_3:25;
thus Del(bAG,i).j = Line(bAG,jL+len A) by A29
.= (width da|->a)^Line(bG,jL) by A2,A37,Th23
.= Line(bdAG,jL+len da) by A37,Th23
.= Line(bdAG,j) by A4,A5;
end;
end;
hence Del(bAG,i).j=bdAG.j by A5,A10,A13,A18,MATRIX_0:52;
end;
end;
hence Del(bAG,i).j=bdAG.j;
end;
A38: block_diagonal(DA^G,a)=bdAG by Th36;
A39: block_diagonal(AA^G,a)=bAG by Th36;
len Del(bAG,i)=m+len bG by A12,A9,A3,A6,FINSEQ_3:109;
hence thesis by A11,A39,A38,A14;
end;
theorem Th42:
i in dom A & width A = width DelLine(A,i) implies DelLine(
block_diagonal(G^<*A*>,a),Sum Len G+i) = block_diagonal(G^<*DelLine(A,i)*>,a)
proof
assume that
A1: i in dom A and
A2: width A= width DelLine(A,i);
A3: i in Seg len A by A1,FINSEQ_1:def 3;
set da=DelLine(A,i);
consider m such that
A4: len A = m + 1 and
A5: len da = m by A1,FINSEQ_3:104;
set Si=Sum Len G+i;
set bG=block_diagonal(G,a);
set DA=<*da*>;
set AA=<*A*>;
set BG=<*bG*>;
set bGA=block_diagonal(<*bG,A*>,a);
set bGdA=block_diagonal(<*bG,da*>,a);
A6: Seg len bGA=dom bGA by FINSEQ_1:def 3;
A7: len bGdA=Sum Len (BG^DA) by Def5;
then
A8: len bGdA=m+len bG by A5,Th16;
A9: len bG=Sum Len G by Def5;
A10: len bGA=Sum Len (BG^AA) by Def5;
then
A11: len bGA=len A +len bG by Th16;
then
A12: len bGA=(m+len bG) +1 by A4;
A13: len bGdA=len da +len bG by A7,Th16;
A14: now
m+len bG <=len bGA by A12,NAT_1:11;
then
A15: Seg (m+len bG) c= Seg len bGA by FINSEQ_1:5;
reconsider da9=da as Matrix of len da,width da,K by MATRIX_0:51;
reconsider A9=A as Matrix of len A,width A,K by MATRIX_0:51;
let j such that
A16: 1<=j and
A17: j<=m+len bG;
A18: j in Seg (m+len bG) by A16,A17;
A19: 1<=1+j by NAT_1:11;
j+1<=len bGA by A12,A17,XREAL_1:7;
then
A20: j+1 in Seg len bGA by A19;
now
per cases;
suppose
A21: j<=len bG;
then
A22: j in dom bG by A16,FINSEQ_3:25;
0<i by A3;
then j+0<len bG+i by A21,XREAL_1:8;
then j<Si by Def5;
hence Del(bGA,Si).j = bGA.j by FINSEQ_3:110
.= Line(bGA,j) by A10,A18,A15,MATRIX_0:52
.= Line(bG,j)^(width da|-> a) by A2,A22,Th23
.= Line(bGdA,j) by A22,Th23
.= bGdA.j by A5,A7,A13,A18,MATRIX_0:52;
end;
suppose
A23: j>len bG;
then reconsider jL=j-len bG as Element of NAT by NAT_1:21;
A24: 0+1<=jL+1 by NAT_1:13;
jL+len bG <=m +len bG by A17;
then
A25: jL<=m by XREAL_1:8;
then
A26: jL+1<=len A by A4,XREAL_1:7;
then
A27: jL+1 in dom A by A24,FINSEQ_3:25;
jL<>0 by A23;
then
A28: 1<=jL by NAT_1:14;
then
A29: jL in dom da by A5,A25,FINSEQ_3:25;
A30: jL+1 in Seg len A by A24,A26;
A31: jL in Seg len da by A5,A28,A25;
A32: jL<=len A by A4,A25,NAT_1:13;
then
A33: jL in Seg len A by A28;
A34: jL in dom A by A28,A32,FINSEQ_3:25;
now
per cases;
suppose
A35: j<Si;
then jL+len bG<i+len bG by Def5;
then
A36: jL<i by XREAL_1:7;
A37: Line(A,jL) = A9.(jL) by A33,MATRIX_0:52
.= da9.(jL) by A36,FINSEQ_3:110
.= Line(da,jL) by A31,MATRIX_0:52;
thus Del(bGA,Si).j = bGA.j by A35,FINSEQ_3:110
.= Line(bGA,jL+len bG)by A10,A18,A15,MATRIX_0:52
.=(width bG|->a)^Line(da,jL) by A34,A37,Th23
.= Line(bGdA,jL+len bG) by A29,Th23;
end;
suppose
A38: j>=Si;
then jL+len bG>=i+len bG by Def5;
then
A39: jL>=i by XREAL_1:8;
A40: Line(A,1+jL) = A9.(1+jL) by A30,MATRIX_0:52
.= da9.jL by A1,A4,A25,A39,FINSEQ_3:111
.= Line(da,jL) by A31,MATRIX_0:52;
thus Del(bGA,Si).j = bGA.(j+1) by A9,A11,A12,A3,A6,A17,A38,
FINSEQ_1:60,FINSEQ_3:111
.= Line(bGA,jL+1+len bG) by A10,A20,MATRIX_0:52
.= (width bG|->a)^Line(da,jL) by A27,A40,Th23
.= Line(bGdA,jL+len bG) by A29,Th23;
end;
end;
hence Del(bGA,Si).j=bGdA.j by A5,A7,A13,A18,MATRIX_0:52;
end;
end;
hence Del(bGA,i+Sum Len G).j=bGdA.j;
end;
A41: block_diagonal(G^DA,a)=bGdA by Th35;
A42: block_diagonal(G^AA,a)=bGA by Th35;
len Del(bGA,Si)=m+len bG by A9,A11,A12,A3,A6,FINSEQ_1:60,FINSEQ_3:109;
hence thesis by A8,A42,A41,A14;
end;
theorem Th43:
i in Seg width A implies DelCol(block_diagonal(<*A*>^G,a),i) =
block_diagonal(<*DelCol(A,i)*>^G,a)
proof
assume
A1: i in Seg width A;
set bG=block_diagonal(G,a);
set Da=DelCol(A,i);
set AA=<*A*>;
set DA=<*Da*>;
set BG=<*bG*>;
set BAG=block_diagonal(<*A,bG*>,a);
set BDG=block_diagonal(<*Da,bG*>,a);
A2: len Da=len A by MATRIX_0:def 13;
len BAG=Sum Len (AA^BG) by Def5;
then
A3: len BAG=len A+len bG by Th16;
A4: len BDG=Sum Len (DA^BG) by Def5;
then
A5: len BDG=len Da+len bG by Th16;
A6: now
reconsider Da9=Da as Matrix of len Da,width Da,K by MATRIX_0:51;
let j such that
A7: 1<=j and
A8: j<= len BDG;
A9: j in Seg len BDG by A7,A8;
A10: now
per cases;
suppose
A11: j<=len A;
then
A12: j in Seg len A by A7;
A13: j in dom Da by A2,A7,A11,FINSEQ_3:25;
A14: dom Line(A,j)=Seg width A by FINSEQ_2:124;
A15: j in dom A by A7,A11,FINSEQ_3:25;
then
A16: Line(BAG,j)=Line(A,j)^(width bG|->a) by Th23;
Del(Line(A,j),i) = Da9.j by A15,MATRIX_0:def 13
.= Line(Da,j) by A2,A12,MATRIX_0:52;
hence Del(Line(BAG,j),i) = Line(Da,j)^(width bG|->a) by A1,A16,A14,Th2
.= Line(BDG,j) by A13,Th23
.= BDG.j by A4,A9,MATRIX_0:52;
end;
suppose
A17: j>len A;
then reconsider jL=j-len A as Element of NAT by NAT_1:21;
jL<>0 by A17;
then
A18: jL>=1 by NAT_1:14;
width A <> 0 by A1;
then
reconsider w1=width A-1 as Element of NAT by NAT_1:14,21;
A19: dom (width A |-> a) = Seg width A by FINSEQ_2:124;
A20: width Da = w1+1-'1 by A1,LAPLACE:3
.= w1 by NAT_D:34;
jL+len A <=len bG+len A by A5,A8,MATRIX_0:def 13;
then jL<=len bG by XREAL_1:8;
then
A21: jL in dom bG by A18,FINSEQ_3:25;
then Line(BAG,jL+len A)=(width A |-> a)^Line(bG,jL) by Th23;
hence Del(Line(BAG,j),i) = Del((w1+1) |->a,i)^Line(bG,jL) by A1,A19,Th2
.= (width Da|->a)^Line(bG,jL) by A1,A20,Th4
.= Line(BDG,len A+jL) by A2,A21,Th23
.= BDG.j by A4,A9,MATRIX_0:52;
end;
end;
j in dom BAG by A2,A5,A3,A7,A8,FINSEQ_3:25;
hence DelCol(BAG,i).j=BDG.j by A10,MATRIX_0:def 13;
end;
A22: block_diagonal(DA^G,a)=BDG by Th36;
A23: len DelCol(BAG,i)=len BAG by MATRIX_0:def 13;
block_diagonal(AA^G,a)=BAG by Th36;
hence thesis by A2,A23,A4,A3,A6,A22,Th16,FINSEQ_1:14;
end;
theorem Th44:
i in Seg width A implies DelCol(block_diagonal(G^<*A*>,a),i+Sum
Width G) = block_diagonal(G^<*DelCol(A,i)*>,a)
proof
assume
A1: i in Seg width A;
set iS=i+Sum Width G;
set bG=block_diagonal(G,a);
set Da=DelCol(A,i);
set AA=<*A*>;
set DA=<*Da*>;
set BG=<*bG*>;
set BGA=block_diagonal(<*bG,A*>,a);
set BGD=block_diagonal(<*bG,Da*>,a);
A2: len Da=len A by MATRIX_0:def 13;
len BGA=Sum Len (BG^AA) by Def5;
then
A3: len BGA=len bG+len A by Th16;
A4: width bG=Sum Width G by Def5;
A5: len BGD=Sum Len (BG^DA) by Def5;
then
A6: len BGD=len bG+len Da by Th16;
A7: now
width A <> 0 by A1;
then width A >= 1 by NAT_1:14;
then width A-'1=width A-1 by XREAL_1:233;
then
A8: width A=(width A-'1)+1;
A9: dom (width A|->a)=Seg width A by FINSEQ_2:124;
A10: len (width bG|->a)=width bG by CARD_1:def 7;
reconsider Da9=Da as Matrix of len Da,width Da,K by MATRIX_0:51;
let j such that
A11: 1<=j and
A12: j<= len BGD;
A13: j in Seg len BGD by A11,A12;
A14: len Line(bG,j)=width bG by MATRIX_0:def 7;
A15: now
per cases;
suppose
j<=len bG;
then
A16: j in dom bG by A11,FINSEQ_3:25;
then Line(BGA,j)=Line(bG,j)^(width A|->a) by Th23;
hence
Del(Line(BGA,j),iS) = Line(bG,j)^Del(width A|->a,i) by A1,A4,A9,A14,Th3
.= Line(bG,j)^((width A-'1) |->a) by A1,A8,Th4
.= Line(bG,j)^(width Da|->a) by A1,LAPLACE:3
.= Line(BGD,j) by A16,Th23
.= BGD.j by A5,A13,MATRIX_0:52;
end;
suppose
A17: j>len bG;
then reconsider jL=j-len bG as Element of NAT by NAT_1:21;
jL<>0 by A17;
then
A18: jL>=1 by NAT_1:14;
jL+len bG <=len bG+len A by A6,A12,MATRIX_0:def 13;
then
A19: jL<=len A by XREAL_1:8;
then
A20: jL in dom Da by A2,A18,FINSEQ_3:25;
A21: jL in Seg len A by A18,A19;
A22: jL in dom A by A18,A19,FINSEQ_3:25;
then
A23: Del(Line(A,jL),i) = Da9.jL by MATRIX_0:def 13
.= Line(Da,jL) by A2,A21,MATRIX_0:52;
A24: dom Line(A,jL)=Seg width A by FINSEQ_2:124;
Line(BGA,jL+len bG)=(width bG |-> a)^Line(A,jL) by A22,Th23;
hence Del(Line(BGA,j),iS) = (width bG|->a)^Del(Line(A,jL),i) by A1,A4
,A10,A24,Th3
.= Line(BGD,len bG+jL) by A20,A23,Th23
.= BGD.j by A5,A13,MATRIX_0:52;
end;
end;
j in dom BGA by A2,A6,A3,A11,A12,FINSEQ_3:25;
hence DelCol(BGA,iS).j=BGD.j by A15,MATRIX_0:def 13;
end;
A25: block_diagonal(G^DA,a)=BGD by Th35;
A26: len DelCol(BGA,iS)=len BGA by MATRIX_0:def 13;
block_diagonal(G^AA,a)=BGA by Th35;
hence thesis by A2,A26,A5,A3,A7,A25,Th16,FINSEQ_1:14;
end;
definition
let D;
let F be FinSequence of (D**);
attr F is Square-Matrix-yielding means
:Def6:
for i st i in dom F ex n st F. i is Matrix of n,D;
end;
registration
let D;
cluster Square-Matrix-yielding for FinSequence of D**;
existence
proof
reconsider F=<*>(D**) as FinSequence of D**;
take F;
thus thesis;
end;
end;
registration
let D;
cluster Square-Matrix-yielding -> Matrix-yielding for FinSequence of D**;
coherence
proof
let F be FinSequence of D** such that
A1: F is Square-Matrix-yielding;
let i;
assume i in dom F;
then ex n st F.i is Matrix of n,D by A1;
hence thesis;
end;
end;
definition
let D;
mode FinSequence_of_Square-Matrix of D is Square-Matrix-yielding FinSequence
of D**;
end;
definition
let K;
mode FinSequence_of_Square-Matrix of K is Square-Matrix-yielding FinSequence
of (the carrier of K)**;
end;
reserve S,S1,S2 for FinSequence_of_Square-Matrix of D,
R,R1,R2 for FinSequence_of_Square-Matrix of K;
theorem
{} is FinSequence_of_Square-Matrix of D
proof
set F=<*>(D**);
for i st i in dom F ex n st F.i is Matrix of n,D;
hence thesis by Def6;
end;
definition
let D,S,x;
redefine func S.x -> Matrix of len (S.x),D; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider E={} as Matrix of 0,D by MATRIX_0:13;
per cases;
suppose
A1: x in dom S;
then reconsider i=x as Element of NAT;
consider n such that
A2: S.i is Matrix of n,D by A1,Def6;
len (S.i)=n by A2,MATRIX_0:24;
hence thesis by A2;
end;
suppose
A3: not x in dom S;
S.x=E by A3,FUNCT_1:def 2;
hence thesis;
end;
end;
end;
definition
let D,S1,S2;
redefine func S1^S2 -> FinSequence_of_Square-Matrix of D; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
S1^S2 is Square-Matrix-yielding
proof
let i such that
A1: i in dom (S1^S2);
take len ((S1^S2).i);
per cases by A1,FINSEQ_1:25;
suppose
i in dom S1;
then (S1^S2).i=S1.i by FINSEQ_1:def 7;
hence thesis;
end;
suppose
ex n st n in dom S2 & i=len S1 + n;
then consider n such that
A2: n in dom S2 and
A3: i=len S1+n;
(S1^S2).i=S2.n by A2,A3,FINSEQ_1:def 7;
hence thesis;
end;
end;
hence thesis;
end;
end;
Lm6: for M be Matrix of n,D holds <*M*> is FinSequence_of_Square-Matrix of D
proof
let M be Matrix of n,D;
now
let i such that
A1: i in dom <*M*>;
take n;
A2: <*M*>.1=M;
dom <*M*> ={1} by FINSEQ_1:2,def 8;
hence <*M*>.i is Matrix of n,D by A1,A2,TARSKI:def 1;
end;
hence thesis by Def6;
end;
definition
let D,n;
let M1 be Matrix of n,D;
redefine func <* M1 *> -> FinSequence_of_Square-Matrix of D; :: redefines <* (FINSEQ_1, definition)
coherence by Lm6;
end;
definition
let D,n,m;
let M1 be Matrix of n,D;
let M2 be Matrix of m,D;
redefine func <* M1,M2 *> -> FinSequence_of_Square-Matrix of D; :: redefines <* (FINSEQ_1, definition)
coherence
proof
reconsider F1=<*M1*>,F2=<*M2*> as FinSequence_of_Square-Matrix of D;
<*M1,M2*>=F1^F2;
hence thesis;
end;
end;
definition
let D,n,S;
redefine func S|n -> FinSequence_of_Square-Matrix of D; :: redefines | (FINSEQ_1, definition)
coherence
proof
S|n is Square-Matrix-yielding
proof
let i such that
A1: i in dom (S|n);
take L=len (S.i);
thus (S|n).i is Matrix of L,D by A1,FUNCT_1:47;
end;
hence thesis;
end;
redefine func S/^n -> FinSequence_of_Square-Matrix of D; :: redefines /^ (RFINSEQ, definition)
coherence
proof
S/^n is Square-Matrix-yielding
proof
let i such that
A2: i in dom (S/^n);
take L=len (S.(n+i));
thus (S/^n).i is Matrix of L,D by A2,FINSEQ_5:27;
end;
hence thesis;
end;
end;
theorem Th46:
Len S = Width S
proof
set L=Len S;
set W=Width S;
A1: dom W=dom S by Def4;
A2: dom L=dom S by Def3;
now
let k such that
A3: k in dom L;
thus L.k = len (S.k) by A3,Def3
.= width (S.k) by MATRIX_0:24
.= W.k by A2,A1,A3,Def4;
end;
hence thesis by A2,A1,FINSEQ_1:13;
end;
definition
let D;
let d be Element of D;
let S be FinSequence_of_Square-Matrix of D;
redefine func block_diagonal(S,d) -> Matrix of Sum Len S,D; :: redefines block_diagonal (MATRIXJ1, definition)
coherence
proof
A1: block_diagonal(S,d) is Matrix of Sum Len S,Sum Width S,D;
Len S = Width S by Th46;
hence thesis by A1;
end;
end;
theorem Th47:
for A be (Matrix of n,K) st i in dom A & j in Seg n holds
Deleting(block_diagonal(<*A*>^R,a),i,j)= block_diagonal(<*Deleting(A,i,j)*>^R,a
)
proof
let A be (Matrix of n,K) such that
A1: i in dom A and
A2: j in Seg n;
n <> 0 by A2;
then
A3: n>=1 by NAT_1:14;
set AA=<*A*>;
set b=block_diagonal(R,a);
set B=<*b*>;
set LAR=Sum Len(AA^R);
set LAB=Sum Len(AA^B);
A4: width A=n by MATRIX_0:24;
Width AA=<*width A*> by Th19;
then
A5: Sum Width AA=width A by RVSUM_1:73;
A6: Width B=<*width b*> by Th19;
A7: Len AA=<*len A*> by Th15;
then
A8: Sum Len AA=len A by RVSUM_1:73;
Len(AA^B)=(Len AA)^Len B by Th14;
then
A9: LAB=len A+Sum Len B by A7,RVSUM_1:76;
A10: Len(AA^B)=Width(AA^B) by Th46;
Width(AA^B)=(Width AA)^Width B by Th18;
then
A11: LAB=Sum Width AA+width b by A6,A10,RVSUM_1:74;
Len B=<*len b*> by Th15;
then
A12: Sum Len B=len b by RVSUM_1:73;
A13: len A=n by MATRIX_0:24;
then
A14: dom A=Seg n by FINSEQ_1:def 3;
per cases by A3,XXREAL_0:1;
suppose
A15: n=1;
then
A16: i=1 by A1,A14,FINSEQ_1:2,TARSKI:def 1;
A17: j=1 by A2,A15,FINSEQ_1:2,TARSKI:def 1;
len Deleting(A,i,j) = 1-'1 by A1,A15,LAPLACE:2
.= 0 by XREAL_1:232;
then
A18: Deleting(A,i,j)={};
thus Deleting(block_diagonal(AA^R,a),i,j) = Deleting(block_diagonal(AA^B,a
),i,j) by Th36
.= Segm(block_diagonal(AA^B,a),Seg LAB\{i},Seg LAB\{j}) by MATRIX13:58
.= b by A13,A4,A9,A11,A12,A8,A5,A15,A16,A17,Th33,FINSEQ_1:2
.= block_diagonal(B,a) by Th34
.= block_diagonal(<*Deleting(A,i,j)*>^B,a) by A18,Th40
.= block_diagonal(<*Deleting(A,i,j)*>^R,a) by Th36;
end;
suppose
n>1;
then
A19: width A=width DelLine(A,i) by A13,LAPLACE:4;
thus Deleting(block_diagonal(AA^R,a),i,j) = DelCol(DelLine(block_diagonal(
AA^R,a),i),j)
.= DelCol(block_diagonal(<*DelLine(A,i)*>^R,a),j) by A1,A19,Th41
.= block_diagonal(<*DelCol(DelLine(A,i),j)*>^R,a) by A2,A4,A19,Th43
.= block_diagonal(<*Deleting(A,i,j)*>^R,a);
end;
end;
theorem
for A be Matrix of n,K st i in dom A & j in Seg n holds Deleting(
block_diagonal(R^<*A*>,a),i+Sum Len R,j+Sum Len R)= block_diagonal(R^<*Deleting
(A,i,j)*>,a)
proof
let A be Matrix of n,K such that
A1: i in dom A and
A2: j in Seg n;
n <> 0 by A2;
then
A3: n>=1 by NAT_1:14;
set jS=j+Sum Len R;
set iS=i+Sum Len R;
set AA=<*A*>;
set b=block_diagonal(R,a);
set B=<*b*>;
set LRA=Sum Len(R^AA);
set LBA=Sum Len(B^AA);
A4: width A=n by MATRIX_0:24;
A5: Len R=Width R by Th46;
A6: len A=n by MATRIX_0:24;
then
A7: dom A=Seg n by FINSEQ_1:def 3;
A8: Width AA=<*width A*> by Th19;
A9: len b=Sum Len R by Def5;
A10: Len(B^AA)=Width(B^AA) by Th46;
A11: Len AA=<*len A*> by Th15;
then
A12: Sum Len AA=len A by RVSUM_1:73;
Len(B^AA)=(Len B)^Len AA by Th14;
then
A13: LBA=len A+Sum Len B by A11,RVSUM_1:74;
A14: Width B=<*width b*> by Th19;
then
A15: Sum Width B=width b by RVSUM_1:73;
Width(B^AA)=(Width B)^Width AA by Th18;
then
A16: LBA=Sum Width AA+width b by A14,A10,RVSUM_1:76;
Len B=<*len b*> by Th15;
then
A17: Sum Len B=len b by RVSUM_1:73;
per cases by A3,XXREAL_0:1;
suppose
A18: n=1;
then
A19: i=1 by A1,A7,FINSEQ_1:2,TARSKI:def 1;
A20: j=1 by A2,A18,FINSEQ_1:2,TARSKI:def 1;
len Deleting(A,i,j) = 1-'1 by A1,A18,LAPLACE:2
.= 0 by XREAL_1:232;
then
A21: Deleting(A,i,j)={};
thus Deleting(block_diagonal(R^AA,a),iS,jS) = Deleting(block_diagonal(B^AA
,a),iS,jS) by Th35
.= Segm(block_diagonal(B^AA,a),Seg LBA\{iS},Seg LBA\{jS}) by MATRIX13:58
.= Segm(block_diagonal(B^AA,a),Seg Sum Len B,Seg LBA\{jS}) by A6,A9,A13
,A17,A18,A19,FINSEQ_1:10
.= Segm(block_diagonal(B^AA,a),Seg Sum Len B,Seg Sum Width B) by A6,A4,A9
,A11,A8,A13,A16,A17,A12,A15,A18,A20,FINSEQ_1:10
.= b by A17,A15,Th32
.= block_diagonal(B,a) by Th34
.= block_diagonal(B^<*Deleting(A,i,j)*>,a) by A21,Th40
.= block_diagonal(R^<*Deleting(A,i,j)*>,a) by Th35;
end;
suppose
n>1;
then
A22: width A=width DelLine(A,i) by A6,LAPLACE:4;
thus Deleting(block_diagonal(R^AA,a),iS,jS) = DelCol(DelLine(
block_diagonal(R^AA,a),iS),jS)
.= DelCol(block_diagonal(R^<*DelLine(A,i)*>,a),jS) by A1,A22,Th42
.= block_diagonal(R^<*DelCol(DelLine(A,i),j)*>,a)by A2,A4,A5,A22,Th44
.= block_diagonal(R^<*Deleting(A,i,j)*>,a);
end;
end;
definition
let K,R;
func Det R -> FinSequence of K means
:Def7:
dom it = dom R & for i st i in dom it holds it.i = Det R.i;
existence
proof
deffunc D(Nat)=Det (R.$1);
consider p be FinSequence of K such that
A1: len p=len R and
A2: for i st i in dom p holds p.i=D(i) from FINSEQ_2:sch 1;
take p;
thus thesis by A1,A2,FINSEQ_3:29;
end;
uniqueness
proof
let F1,F2 be FinSequence of K such that
A3: dom F1=dom R and
A4: for i st i in dom F1 holds F1.i=Det (R.i) and
A5: dom F2=dom R and
A6: for i st i in dom F2 holds F2.i=Det (R.i);
now
let x being object such that
A7: x in dom F1;
reconsider i=x as Element of NAT by A7;
thus F1.x = Det (R.i) by A4,A7
.= F2.x by A3,A5,A6,A7;
end;
hence thesis by A3,A5,FUNCT_1:2;
end;
end;
definition
let K,R;
redefine func Det R-> Element of (len R)-tuples_on the carrier of K; :: redefines Det (MATRIXJ1, definition)
coherence
proof
dom (Det R)=dom R by Def7;
then len (Det R)=len R by FINSEQ_3:29;
hence thesis by FINSEQ_2:92;
end;
end;
reserve N for (Matrix of n,K),
N1 for (Matrix of m,K);
theorem Th49:
Det <*N*> = <*Det N*>
proof
set F=<*N*>;
A1: len F=1 by FINSEQ_1:40;
A2: n=len N by MATRIX_0:def 2;
A4: len F=len (Det F) by CARD_1:def 7;
A5: dom (Det F)=Seg len F by FINSEQ_2:124;
1 in Seg 1;
then (Det F).1=Det (F.1) by A1,A5,Def7;
hence thesis by A1,A4,A2,FINSEQ_1:40;
end;
theorem Th50:
Det (R1^R2) = Det R1^Det R2
proof
set R12=R1^R2;
A1: len R12=len R1+len R2 by FINSEQ_1:22;
A2: len (Det R1^Det R2)=len R1+len R2 by CARD_1:def 7;
len R2=len Det R2 by CARD_1:def 7;
then
A3: dom (Det R2)=dom R2 by FINSEQ_3:29;
A4: len R1=len Det R1 by CARD_1:def 7;
then
A5: dom (Det R1)=dom R1 by FINSEQ_3:29;
A6: len Det R12=len R12 by CARD_1:def 7;
then
A7: dom (Det R1 ^ Det R2)= dom Det R12 by A1,A2,FINSEQ_3:29;
now
let k such that
A8: 1<=k and
A9: k<=len R1+len R2;
A10: k in dom (Det R1 ^ Det R2) by A2,A8,A9,FINSEQ_3:25;
now
per cases by A10,FINSEQ_1:25;
suppose
A11: k in dom (Det R1);
then
A12: len (R1.k)=len (R12.k) by A5,FINSEQ_1:def 7;
thus (Det R1 ^ Det R2).k = (Det R1).k by A11,FINSEQ_1:def 7
.= Det (R1.k) by A11,Def7
.= Det(R12.k) by A5,A11,A12,FINSEQ_1:def 7
.= (Det R12).k by A7,A10,Def7;
end;
suppose
ex n st n in dom (Det R2) & k=len (Det R1)+n;
then consider n such that
A13: n in dom (Det R2) and
A14: k=len R1+n by A4;
A15: len (R2.n)=len (R12.k) by A3,A13,A14,FINSEQ_1:def 7;
thus (Det R1 ^ Det R2).k = (Det R2).n by A4,A13,A14,FINSEQ_1:def 7
.= Det (R2.n) by A13,Def7
.= Det(R12.k) by A3,A13,A14,A15,FINSEQ_1:def 7
.= (Det R12).k by A7,A10,Def7;
end;
end;
hence (Det R12).k=(Det R1 ^ Det R2).k;
end;
hence thesis by A6,A1,A2;
end;
theorem
Det (R|n) = (Det R) |n
proof
A1: len Det R=len R by CARD_1:def 7;
per cases;
suppose
A2: n>=len R;
then R|n=R by FINSEQ_1:58;
hence thesis by A1,A2,FINSEQ_1:58;
end;
suppose
A3: n<len R;
R=(R|n)^(R/^n) by RFINSEQ:8;
then
A4: Det R=(Det (R|n))^Det(R/^n) by Th50;
len (R|n) =n by A3,FINSEQ_1:59;
then len Det (R|n)=n by CARD_1:def 7;
hence thesis by A4,FINSEQ_5:23;
end;
end;
theorem Th52:
Det block_diagonal(<*N,N1*>,0.K) = Det N * Det N1
proof
defpred P[Nat] means for n,m,N,N1 st n=$1 holds Det block_diagonal(<*N,N1*>,
0.K) = (Det N) * (Det N1);
A1: for i st P[i] holds P[i+1]
proof
let i such that
A2: P[i];
set i1=i+1;
let n,m,N,N1 such that
A3: n=i1;
1<=i+m+1 by NAT_1:11;
then
A4: 1 in Seg (n+m) by A3;
1<=i1 by NAT_1:11;
then
A5: 1 in Seg n by A3;
set L0=len N1|->0.K;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
set D=Det N1;
set L1=LaplaceExpL(N,1);
set NN=<*N,N1*>;
reconsider M=N as Matrix of K;
set bN=block_diagonal(NN,0.K);
set L=LaplaceExpL(bN,1);
A6: width N=n by MATRIX_0:24;
set Ln=L|n;
A7: len L1=n by LAPLACE:def 7;
set L9n=L/^n;
A8: L=(L|n)^(L/^n) by RFINSEQ:8;
A9: len N=n by MATRIX_0:24;
then
A10: dom N=Seg n by FINSEQ_1:def 3;
reconsider L1 as Element of nn-tuples_on the carrier of K by A7,FINSEQ_2:92
;
A11: len N1=m by MATRIX_0:24;
then
A12: len L0=m by CARD_1:def 7;
A13: Sum Len NN=len N+len N1 by Th16;
then
A14: len L=n+m by A9,A11,LAPLACE:def 7;
then
A15: len Ln=n by FINSEQ_1:59,NAT_1:11;
A16: width bN=Sum Len NN by MATRIX_0:24;
A17: now
A18: i=n-'1 by A3,NAT_D:34;
let j such that
A19: 1<=j and
A20: j<=n;
A21: len Delete(N,1,j)=n-'1 by MATRIX_0:def 2;
A22: j in dom Ln by A15,A19,A20,FINSEQ_3:25;
then j in dom L/\Seg n by RELAT_1:61;
then
A23: j in dom L by XBOOLE_0:def 4;
j in dom L1 by A7,A19,A20,FINSEQ_3:25;
then
A24: N*(1,j)*Cofactor(N,1,j)=L1.j by LAPLACE:def 7;
A25: i+m+1-'1=i+m by NAT_D:34;
A26: dom Line(N,1)=Seg n by A6,FINSEQ_2:124;
A27: dom Ln= Seg n by A15,FINSEQ_1:def 3;
A28: dom L=Seg (n+m) by A14,FINSEQ_1:def 3;
then
A29: Delete(bN,1,j) = Deleting(bN,1,j) by A13,A9,A11,A4,A23,LAPLACE:def 1
.= block_diagonal(<*Deleting(N,1,j)*>^<*N1*>,0.K) by A5,A10,A22,A27
,Th47
.= block_diagonal(<*Delete(N,1,j),N1*>,0.K) by A5,A22,A27,LAPLACE:def 1
;
Minor(N,1,j) *D = Det block_diagonal(<*Delete(N,1,j),N1*>,0.K) by A2,A3,
NAT_D:34
.= Minor(bN,1,j) by A3,A13,A9,A11,A29,A18,A25,A21,Th16;
then
A30: Cofactor(bN,1,j)= D*Cofactor(N,1,j) by GROUP_1:def 3;
A31: bN*(1,j) = Line(block_diagonal(<*M,N1*>,0.K),1).j by A16,A13,A9,A11,A23
,A28,MATRIX_0:def 7
.= (Line(N,1)^(width N1|->0.K)).j by A5,A10,Th23
.= Line(N,1).j by A22,A27,A26,FINSEQ_1:def 7
.= N*(1,j) by A6,A22,A27,MATRIX_0:def 7;
thus Ln.j = L.j by A22,FUNCT_1:47
.= N*(1,j)*(D*Cofactor(N,1,j)) by A23,A30,A31,LAPLACE:def 7
.= D*(N*(1,j)*Cofactor(N,1,j)) by GROUP_1:def 3
.= (D*L1).j by A22,A27,A24,FVSUM_1:51;
end;
n<=n+m by NAT_1:11;
then
A32: len L9n=(n+m)-n by A14,RFINSEQ:def 1;
A33: width N1=m by MATRIX_0:24;
now
A34: len Line(N,1)=n by A6,CARD_1:def 7;
let i such that
A35: 1<=i and
A36: i<=m;
A37: i in Seg m by A35,A36;
A38: i in dom L0 by A12,A35,A36,FINSEQ_3:25;
A39: i in dom L9n by A32,A35,A36,FINSEQ_3:25;
then
A40: n+i in dom L by FINSEQ_5:26;
dom L=Seg width bN by A16,A13,A9,A11,A14,FINSEQ_1:def 3;
then
A41: bN*(1,i+n) = Line(block_diagonal(<*M,N1*>,0.K),1).(i+n) by A40,
MATRIX_0:def 7
.= (Line(N,1)^L0).(i+n) by A11,A33,A5,A10,Th23
.= L0.i by A38,A34,FINSEQ_1:def 7
.= 0.K by A11,A37,FINSEQ_2:57;
thus L9n.i = L9n/.i by A39,PARTFUN1:def 6
.= L/.(i+n) by A39,FINSEQ_5:27
.= L.(i+n) by A40,PARTFUN1:def 6
.= bN*(1,i+n)*Cofactor(bN,1,i+n) by A40,LAPLACE:def 7
.= 0.K by A41
.= L0.i by A11,A37,FINSEQ_2:57;
end;
then
A42: L/^n=(len N1) |->0.K by A32,A12;
len (D*L1)=nn by A7,MATRIXR1:16;
then L|n=D*L1 by A15,A17;
then Sum L = Sum (D*L1)+Sum(len N1|->0.K) by A42,A8,RLVECT_1:41
.= Sum (D*L1)+Sum (len N1|->(0.K*0.K))
.= Sum (D*L1)+Sum (0.K*(len N1|->0.K)) by FVSUM_1:53
.= D*Sum L1+Sum (0.K*(len N1|->0.K)) by FVSUM_1:73
.= D*Sum L1+0.K*Sum (len N1|->0.K) by FVSUM_1:73
.= D*Sum L1+0.K
.= D*Sum L1 by RLVECT_1:def 4
.= D*Det N by A5,LAPLACE:25;
hence thesis by A13,A9,A11,A4,LAPLACE:25;
end;
A43: P[0]
proof
let n,m,N,N1 such that
A44: n=0;
A45: len N=n by MATRIX_0:def 2;
then N={} by A44;
then
A46: block_diagonal(<*N,N1*>,0.K) = block_diagonal(<*N1*>,0.K) by Th40
.= N1 by Th34;
len N1=m by MATRIX_0:def 2;
then Sum Len <*N,N1*>=0+m by A44,A45,Th16;
hence Det block_diagonal(<*N,N1*>,0.K) = (Det N1)*1_K by A46
.= Det N*Det N1 by A44,MATRIXR2:41;
end;
for i holds P[i] from NAT_1:sch 2(A43,A1);
hence thesis;
end;
theorem
Det block_diagonal(R,0.K) = Product (Det R)
proof
defpred P[Nat] means for R st len R=$1 holds Det block_diagonal(R,0.K) =
Product (Det R);
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
set n1=n+1;
let R such that
A3: len R=n1;
set Rn=R|n;
A4: len Rn=n by A3,FINSEQ_1:59,NAT_1:11;
set R1=R.n1;
set bR=block_diagonal(Rn,0.K);
A5: R=Rn^<*R1*> by A3,FINSEQ_3:55;
then
A6: block_diagonal(R,0.K)=block_diagonal(<*bR,R1*>,0.K) by Th35;
Sum Len <*bR,R1*> = len bR +len R1 by Th16
.= Sum Len Rn+len R1 by Def5
.= Sum (Len Rn^<*len R1*>) by RVSUM_1:74
.= Sum (Len Rn^Len <*R1*>) by Th15
.= Sum Len R by A5,Th14;
hence Det block_diagonal(R,0.K) = Det bR * Det R1 by A6,Th52
.= (Product Det Rn)*Det R1 by A2,A4
.= Product ((Det Rn)^<*Det R1*>)by GROUP_4:6
.= Product((Det Rn)^(Det <*R1*>)) by Th49
.= Product Det R by A5,Th50;
end;
A7: P[0]
proof
let R such that
A8: len R=0;
Len R = {} by A8;
hence Det block_diagonal(R,0.K) = 1_K by MATRIXR2:41,RVSUM_1:72
.= Product Det R by A8,FVSUM_1:80;
end;
for n holds P[n] from NAT_1:sch 2(A7,A1);
hence thesis;
end;
theorem Th54:
len A1 <> width A1 & N = block_diagonal(<*A1,A2*>,0.K) implies Det N = 0.K
proof
defpred P[Nat] means for A1 st len A1<>width A1 & width A1=$1 for n,N st N=
block_diagonal(<*A1,A2*>,0.K) holds Det N=0.K;
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
set k1=k+1;
let A1 such that
A3: len A1<>width A1 and
A4: width A1=k1;
A5: Sum Len <*A1,A2*>=len A1+len A2 by Th16;
1<=k1 by NAT_1:14;
then
A6: 1 in Seg width A1 by A4;
A7: len(A1^A2)=len A1+len A2 by FINSEQ_1:22;
A8: Sum Width <*A1,A2*>=width A1+width A2 by Th20;
let n,N such that
A9: N=block_diagonal(<*A1,A2*>,0.K);
A10: len N=Sum Len <*A1,A2*> by A9,Def5;
set C=LaplaceExpC(N,1);
A11: n=len N by MATRIX_0:24;
then
A12: len C=len N by LAPLACE:def 8;
A13: len A1<>0 by A3,MATRIX_0:def 3;
then
A14: 1+0<=len N by A10,A5,NAT_1:14;
then
A15: 1 in Seg n by A11;
A16: width N= Sum Width <*A1,A2*> by A9,Def5;
set L0=len N|->0.K;
A17: n=width N by MATRIX_0:24;
A18: len A1>=1 by A13,NAT_1:14;
A19: now
let i such that
A20: 1<=i and
A21: i<=len N;
A22: i in Seg n by A11,A20,A21;
i in dom C by A12,A20,A21,FINSEQ_3:25;
then
A23: C.i=N*(i,1)*Cofactor(N,i,1) by LAPLACE:def 8;
A24: N*(i,1)=Line(N,i).1 by A17,A15,MATRIX_0:def 7;
A25: i in dom (A1^A2) by A10,A5,A7,A20,A21,FINSEQ_3:25;
now
per cases by A25,FINSEQ_1:25;
suppose
A26: i in dom A1;
now
per cases by A18,XXREAL_0:1;
suppose
A27: len A1=1;
then k<>0 by A3,A4;
then k in Seg k by FINSEQ_1:3;
then
A28: 1<=k by FINSEQ_1:1;
then 1+1<=k1 by XREAL_1:7;
then
A29: 2 in Seg k1;
A30: 1<=i by A26,FINSEQ_3:25;
i<=1 by A26,A27,FINSEQ_3:25;
then
A31: i=1 by A30,XXREAL_0:1;
set Q=Seg n\{1};
Seg 1 c= Seg n by A11,A14,FINSEQ_1:5;
then
A32: card Q = card Seg n-card Seg 1 by CARD_2:44,FINSEQ_1:2
.= card Seg n-1 by FINSEQ_1:57
.= n-1 by FINSEQ_1:57
.= k+width A2 by A4,A17,A16,A8;
then
A33: card Q = k+width A2+1-'1 by NAT_D:34
.= n-'1 by A4,A9,A17,A8,Def5;
1+0<=card Q by A32,A28,XREAL_1:7;
then
A34: 1 in Seg card Q;
Delete(N,i,1) = Deleting(N,i,1) by A15,A22,LAPLACE:def 1
.= Segm(N,Q,Q) by A31,MATRIX13:58;
then
A35: Col(Delete(N,i,1),1) = Col(N,Sgm Q.1)*Sgm Q by A11,A34,
MATRIX13:49,XBOOLE_1:36;
now
A36: dom (len A2|->0.K)=Seg len A2 by FINSEQ_2:124;
A37: n=1+card Q by A4,A9,A17,A8,A32,Def5;
A38: len Col(A1,2)=1 by A27,CARD_1:def 7;
let j be Element of NAT such that
A39: j in Seg (n-'1);
dom Sgm Q=Seg card Q by FINSEQ_3:40;
hence Col(Delete(N,i,1),1).j = Col(N,Sgm Q.1).((Sgm Q).j)
by A33,A35,A39,FUNCT_1:13
.= Col(N,1+1).(Sgm Q.j) by A34,A37,FINSEQ_1:2,MATRIX15:8
.= Col(N,1+1).(j+1) by A33,A39,A37,FINSEQ_1:2,MATRIX15:8
.= (Col(A1,2)^(len A2|->0.K)).(j+1)by A4,A9,A29,Th24
.= (len A2|->0.K).j by A4,A10,A11,A17,A16,A5,A8,A27,A32,A33
,A39,A38,A36,FINSEQ_1:def 7
.= 0.K by A4,A10,A11,A17,A16,A5,A8,A27,A32,A33,A39,
FINSEQ_2:57;
end;
hence Det Delete(N,i,1)=0.K by A33,A34,MATRIX_9:53;
end;
suppose
A40: len A1>1;
set DL=DelLine(A1,i);
set DC=DelCol(DL,1);
A41: k1-'1=k by NAT_D:34;
reconsider L1=len A1-1 as Element of NAT by A40,NAT_1:21;
A42: len DC=len DL by MATRIX_0:def 13;
A43: width A1=width DL by A40,LAPLACE:4;
then
A44: width DC=width A1-'1 by A6,LAPLACE:3;
A45: Delete(N,i,1) = Deleting(N,i,1) by A15,A22,LAPLACE:def 1
.= DelCol(DelLine(N,i),1)
.= DelCol(block_diagonal(<*DL*>^<*A2*>,0.K),1) by A9,A26,A43
,Th41
.= block_diagonal(<*DC,A2*>,0.K) by A6,A43,Th43;
len A1=L1+1;
then len DC<>width DC by A3,A4,A26,A44,A42,A41,FINSEQ_3:109;
hence 0.K=Det Delete(N,i,1) by A2,A4,A44,A45,NAT_D:34;
end;
end;
then 0.K = Cofactor(N,i,1);
hence 0.K=C.i by A23;
end;
suppose
A46: ex j st j in dom A2 & i=len A1+j;
A47: dom (width A1|->0.K)=Seg width A1 by FINSEQ_2:124;
consider j such that
A48: j in dom A2 and
A49: i=len A1+j by A46;
N*(i,1) = ((width A1|->0.K)^Line(A2,j)).1 by A9,A24,A48,A49,Th23
.= (width A1|->0.K).1 by A6,A47,FINSEQ_1:def 7
.= 0.K by A6,FINSEQ_2:57;
hence 0.K=C.i by A23;
end;
end;
hence C.i=L0.i by A11,A22,FINSEQ_2:57;
end;
len L0=len N by CARD_1:def 7;
then C=L0 by A12,A19;
then C=len N|->(0.K*0.K);
then Sum C = Sum (0.K*(len N|->0.K)) by FVSUM_1:53
.= 0.K*Sum(len N|->0.K) by FVSUM_1:73
.= 0.K;
hence thesis by A15,LAPLACE:27;
end;
A50: P[0]
proof
let A1 such that
A51: len A1<>width A1 and
A52: width A1=0;
A53: len A1 in Seg len A1 by A51,A52,FINSEQ_1:3;
A54: Sum Width <*A1,A2*>= width A1+width A2 by Th20;
A55: Sum Len <*A1,A2*>=len A1+len A2 by Th16;
A56: len A1<=len A1+len A2 by NAT_1:11;
let n,N such that
A57: N=block_diagonal(<*A1,A2*>,0.K);
A58: width N=Sum Width <*A1,A2*> by A57,Def5;
len N=Sum Len <*A1,A2*> by A57,Def5;
then
A59: Seg len A1 c= Seg len N by A55,A56,FINSEQ_1:5;
A60: n=len N by MATRIX_0:def 2;
dom A1=Seg len A1 by FINSEQ_1:def 3;
then Line(N,len A1) = Line(A1,len A1)^(width A2|->0.K) by A57,A53,Th23
.= (<*>(the carrier of K))^(width A2|->0.K) by A52
.= width A2|->0.K by FINSEQ_1:34
.= 0.K * Line(N,len A1) by A52,A58,A54,FVSUM_1:58;
hence Det N = Det RLine(N,len A1,0.K*Line(N,len A1)) by MATRIX11:30
.= 0.K*Det N by A60,A53,A59,MATRIX11:35
.= 0.K;
end;
for n holds P[n] from NAT_1:sch 2(A50,A1);
hence thesis;
end;
theorem
Len G <> Width G implies for M be Matrix of n,K st M = block_diagonal(
G,0.K) holds Det M = 0.K
proof
set B= block_diagonal(G,0.K);
defpred P[Nat] means $1 in Seg len G & (Len G).$1<>(Width G).$1;
A1: Seg len G=dom G by FINSEQ_1:def 3;
assume Len G<>Width G;
then
A2: ex k st P[k] by FINSEQ_2:119;
consider k such that
A3: P[k] and
A4: for n st P[n] holds k<=n from NAT_1:sch 5(A2);
1<=k by A3,FINSEQ_1:1;
then reconsider k1=k-1 as Element of NAT by NAT_1:21;
set Gk=G|k1;
A5: len G=len (Width G) by CARD_1:def 7;
then k in dom (Width G) by A3,FINSEQ_1:def 3;
then
A6: width (G.k)=(Width G).k by Def4;
set bGk=block_diagonal(Gk,0.K);
set bGk1=block_diagonal(G/^k,0.K);
set bGG=block_diagonal(<*G.k,bGk1*>,0.K);
k1+1<=len G by A3,FINSEQ_1:1;
then
A7: k1<len G by NAT_1:13;
then len((Width G) |k1)=k1 by A5,FINSEQ_1:59;
then
A8: dom ((Width G) |k1)=Seg k1 by FINSEQ_1:def 3;
A9: len G=len (Len G) by CARD_1:def 7;
then len((Len G) |k1)=k1 by A7,FINSEQ_1:59;
then
A10: dom ((Len G) |k1)=Seg k1 by FINSEQ_1:def 3;
A11: Seg k1 c=Seg len G by A7,FINSEQ_1:5;
A12: now
let j such that
A13: j in Seg k1;
j<=k1 by A13,FINSEQ_1:1;
then j < k1+1 by NAT_1:13;
then
A14: (Len G).j=(Width G).j by A4,A11,A13;
thus (Len Gk).j = ((Len G) |k1).j by Th17
.= (Len G).j by A10,A13,FUNCT_1:47
.= ((Width G) |k1).j by A8,A13,A14,FUNCT_1:47
.= (Width Gk).j by Th21;
end;
len Gk=k1 by A7,FINSEQ_1:59;
then
Len Gk = Width Gk by A12,FINSEQ_2:119;
then reconsider bGk as Matrix of Sum Len Gk,K;
let M be Matrix of n,K;
assume M =B;
then
A15: M = block_diagonal(G| (k1+1)^(G/^k),0.K) by RFINSEQ:8
.= block_diagonal(Gk^<*G.k*>^(G/^k),0.K) by A3,A1,FINSEQ_5:10
.= block_diagonal(Gk^(<*G.k*>^(G/^k)),0.K) by FINSEQ_1:32
.= block_diagonal(<*bGk*>^(<*G.k*>^(G/^k)),0.K) by Th35
.= block_diagonal(<*bGk*>^<*block_diagonal(<*G.k*>^(G/^k),0.K)*>,0.K) by
Th36
.= block_diagonal(<*bGk,bGG*>,0.K) by Th36;
then
A16: len M=Sum Len <*bGk,bGG*> by Def5;
A17: Sum Width <*bGk,bGG*>=width bGk+width bGG by Th20;
A18: width bGk=Sum Len Gk by MATRIX_0:24;
A19: len bGk=Sum Len Gk by Def5;
A20: width M=n by MATRIX_0:24;
A21: Sum Len <*bGk,bGG*>=len bGk+len bGG by Th16;
A22: len M=n by MATRIX_0:24;
width M=Sum Width <*bGk,bGG*> by A15,Def5;
then reconsider bGG9=bGG as Matrix of len bGG,K by A16,A22,A20,A21,A19,A18
,A17,MATRIX_0:51;
k in dom (Len G) by A3,A9,FINSEQ_1:def 3;
then len (G.k)=(Len G).k by Def3;
then Det bGG9=0.K by A3,A6,Th54;
hence Det M = Det bGk * 0.K by A15,A16,A22,Th52
.= 0.K;
end;
begin :: An Example of a Finite Sequence of Matrices
definition
let K;
let f be FinSequence of NAT;
func 1.(K,f) -> FinSequence_of_Square-Matrix of K means
:Def8:
dom it = dom f & for i st i in dom it holds it.i = 1.(K,f.i);
existence
proof
deffunc G(Nat)=1.(K,f.$1);
consider IT be FinSequence such that
A1: len IT=len f and
A2: for k st k in dom IT holds IT.k=G(k) from FINSEQ_1:sch 2;
rng IT c= (the carrier of K)**
proof
let y be object;
assume y in rng IT;
then consider x being object such that
A3: x in dom IT and
A4: IT.x=y by FUNCT_1:def 3;
reconsider x as Nat by A3;
IT.x =1.(K,f.x) by A2,A3;
hence thesis by A4,FINSEQ_1:def 11;
end;
then reconsider IT as FinSequence of (the carrier of K)** by FINSEQ_1:def 4
;
now
let i;
assume i in dom IT;
then IT.i=1.(K,f.i) by A2;
hence IT.i is Matrix of K;
end;
then reconsider IT as FinSequence_of_Matrix of K by Def2;
now
let i;
assume i in dom IT;
then IT.i=1.(K,f.i) by A2;
hence ex n st IT.i is Matrix of n,K;
end;
then reconsider IT as FinSequence_of_Square-Matrix of K by Def6;
take IT;
thus thesis by A1,A2,FINSEQ_3:29;
end;
uniqueness
proof
let T1,T2 be FinSequence_of_Square-Matrix of K such that
A5: dom T1=dom f and
A6: for i st i in dom T1 holds T1.i= 1.(K,f.i) and
A7: dom T2=dom f and
A8: for i st i in dom T2 holds T2.i= 1.(K,f.i);
now
let i such that
A9: i in dom f;
thus T1.i = 1.(K,f.i) by A5,A6,A9
.= T2.i by A7,A8,A9;
end;
hence thesis by A5,A7,FINSEQ_1:13;
end;
end;
theorem
Len 1.(K,f) = f & Width 1.(K,f) = f
proof
set ONE=1.(K,f);
A1: dom ONE=dom f by Def8;
A2: dom Len ONE=dom ONE by Def3;
now
let i such that
A3: i in dom Len ONE;
thus (Len ONE).i = len (ONE.i) by A3,Def3
.= len (1.(K,f.i)) by A2,A3,Def8
.= f.i by MATRIX_0:24;
end;
hence Len ONE=f by A2,A1,FINSEQ_1:13;
A4: dom Width ONE=dom ONE by Def4;
now
let i such that
A5: i in dom Width ONE;
thus (Width ONE).i = width (ONE.i) by A5,Def4
.= width (1.(K,f.i)) by A4,A5,Def8
.= f.i by MATRIX_0:24;
end;
hence thesis by A4,A1,FINSEQ_1:13;
end;
theorem Th57:
for i be Element of NAT holds 1.(K,<*i*>) = <*1.(K,i)*>
proof
let i be Element of NAT;
A1: dom (1.(K,<*i*>)) = dom <*i*> by Def8
.= Seg 1 by FINSEQ_1:38;
then 1 in dom (1.(K,<*i*>));
then
A2: (1.(K,<*i*>)).1 = 1.(K,<*i*>.1) by Def8
.= 1.(K,i);
len (1.(K,<*i*>))=1 by A1,FINSEQ_1:def 3;
hence thesis by A2,FINSEQ_1:40;
end;
theorem Th58:
1.(K,f^g) = 1.(K,f)^1.(K,g)
proof
set F=1.(K,f);
set G=1.(K,g);
set FG=F^G;
set ONE=1.(K,f^g);
A1: len (f^g)=len f+len g by FINSEQ_1:22;
A2: dom ONE=dom (f^g) by Def8;
A3: dom G=dom g by Def8;
then
A4: len G=len g by FINSEQ_3:29;
A5: dom F=dom f by Def8;
then
A6: len F=len f by FINSEQ_3:29;
A7: len FG=len F+len G by FINSEQ_1:22;
A8: now
let i such that
A9: 1<=i and
A10: i<= len FG;
i in dom ONE by A2,A6,A4,A7,A1,A9,A10,FINSEQ_3:25;
then
A11: ONE.i=1.(K,(f^g).i) by Def8;
A12: i in dom FG by A9,A10,FINSEQ_3:25;
now
per cases by A12,FINSEQ_1:25;
suppose
A13: i in dom F;
hence ONE.i = 1.(K,f.i) by A5,A11,FINSEQ_1:def 7
.= F.i by A13,Def8
.= FG.i by A13,FINSEQ_1:def 7;
end;
suppose
ex n st n in dom G & i=len F+n;
then consider n such that
A14: n in dom G and
A15: i=len F+n;
thus ONE.i = 1.(K,g.n) by A3,A6,A11,A14,A15,FINSEQ_1:def 7
.= G.n by A14,Def8
.= FG.i by A14,A15,FINSEQ_1:def 7;
end;
end;
hence ONE.i=FG.i;
end;
len ONE=len (f^g) by A2,FINSEQ_3:29;
hence thesis by A6,A4,A1,A8,FINSEQ_1:14,22;
end;
theorem
1.(K,f|n) = 1.(K,f) |n
proof
dom 1.(K,f|n) = dom (f|n) by Def8;
then
A1: len 1.(K,f|n)=len (f|n) by FINSEQ_3:29;
dom 1.(K,f) = dom f by Def8;
then
A2: len 1.(K,f)=len f by FINSEQ_3:29;
per cases;
suppose
A3: n>len f;
then f|n=f by FINSEQ_1:58;
hence thesis by A2,A3,FINSEQ_1:58;
end;
suppose
A4: n<=len f;
f=(f|n)^(f/^n) by RFINSEQ:8;
then
A5: 1.(K,f)=(1.(K,f|n))^1.(K,f/^n) by Th58;
len (1.(K,f|n))=n by A1,A4,FINSEQ_1:59;
hence thesis by A5,FINSEQ_5:23;
end;
end;
theorem Th60:
block_diagonal(<*1.(K,i),1.(K,j)*>,0.K)=1.(K,i+j)
proof
set I=1.(K,i);
set J=1.(K,j);
set B=block_diagonal(<*I,J*>,0.K);
A1: len I=i by MATRIX_0:24;
A2: Sum Len <*J*>=len J by Lm4;
A3: len J=j by MATRIX_0:24;
then
A4: Indices block_diagonal(<*J*>,0.K)=[:Seg j,Seg j:] by A2,MATRIX_0:24;
Sum Len <*I,J*>=len I+len J by Th16;
then reconsider B as Matrix of i+j,K by A1,A3;
A5: Indices B=[:Seg (i+j),Seg (i+j):] by MATRIX_0:24;
A6: Indices J=[:Seg j,Seg j:] by MATRIX_0:24;
A7: width I=i by MATRIX_0:24;
A8: Indices I=[:Seg i,Seg i:] by MATRIX_0:24;
A9: Sum Width <*I*>=width I by Lm5;
A10: Sum Len <*I*>=len I by Lm4;
then
A11: Indices block_diagonal(<*I*>,0.K) =[:Seg i,Seg i:] by A1,MATRIX_0:24;
A12: now
let n,m such that
A13: [n,m] in Indices B and
A14: n <> m;
m in Seg (i+j) by A5,A13,ZFMISC_1:87;
then
A15: m>=1 by FINSEQ_1:1;
n in Seg (i+j) by A5,A13,ZFMISC_1:87;
then
A16: n>=1 by FINSEQ_1:1;
now
per cases;
suppose
A17: n<=i & m<=i;
then
A18: m in Seg i by A15;
n in Seg i by A16,A17;
then
A19: [n,m] in [:Seg i,Seg i:] by A18,ZFMISC_1:87;
hence B*(n,m) = block_diagonal(<*I*>,0.K)*(n,m) by A2,A11,Th26
.= I*(n,m) by Th34
.= 0.K by A8,A14,A19,MATRIX_1:def 3;
end;
suppose
A20: n>i & m>i;
then
A21: m-i<>0;
n-'i=n-i by A20,XREAL_1:233;
then
A22: n=n-'i+i;
m-'i=m-i by A20,XREAL_1:233;
then
A23: m=m-'i+i;
n-i<>0 by A20;
then
A24: [n-'i,m-'i] in [:Seg j,Seg j:] by A10,A9,A1,A7,A4,A13,A21,A22,A23,Th27;
hence B*(n,m) = block_diagonal(<*J*>,0.K)*(n-'i,m-'i) by A10,A9,A1,A7
,A4,A22,A23,Th28
.= J*(n-'i,m-'i) by Th34
.= 0.K by A6,A14,A22,A23,A24,MATRIX_1:def 3;
end;
suppose
n<=i & m>i or n>i & m<=i;
hence B*(n,m)=0.K by A10,A9,A2,A1,A7,A13,Th29;
end;
end;
hence B*(n,m) = 0.K;
end;
now
let n such that
A25: [n,n] in Indices B;
n in Seg (i+j) by A5,A25,ZFMISC_1:87;
then
A26: n >= 1 by FINSEQ_1:1;
now
per cases;
suppose
n<=i;
then n in Seg i by A26;
then
A27: [n,n] in [:Seg i,Seg i:] by ZFMISC_1:87;
hence B*(n,n) = block_diagonal(<*I*>,0.K)*(n,n) by A2,A11,Th26
.= I*(n,n) by Th34
.= 1_K by A8,A27,MATRIX_1:def 3;
end;
suppose
A28: n>i;
then n-'i=n-i by XREAL_1:233;
then
A29: n=n-'i+i;
n-i<>0 by A28;
then
A30: [n-'i,n-'i] in [:Seg j,Seg j:] by A10,A9,A1,A7,A4,A25,A29,Th27;
hence B*(n,n) = block_diagonal(<*J*>,0.K)*(n-'i,n-'i) by A10,A9,A1,A7
,A4,A29,Th28
.= J*(n-'i,n-'i) by Th34
.= 1_K by A6,A30,MATRIX_1:def 3;
end;
end;
hence B*(n,n) = 1_K;
end;
hence thesis by A12,MATRIX_1:def 3 ;
end;
theorem
block_diagonal(1.(K,f),0.K) = 1.(K,Sum f)
proof
defpred P[Nat] means for f st len f=$1 holds block_diagonal(1.(K,f),0.K) =
1.(K,Sum f);
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
set n1=n+1;
let f such that
A3: len f=n1;
A4: len (f|n)=n by A3,FINSEQ_1:59,NAT_1:11;
1 <= n1 by NAT_1:11;
then n1 in dom f by A3,FINSEQ_3:25;
then
A5: f/.n1 = f.n1 by PARTFUN1:def 6;
A6: f=(f|n)^<*f.n1*> by A3,FINSEQ_3:55;
hence block_diagonal(1.(K,f),0.K) = block_diagonal(1.(K,f|n)^(1.(K,<*f/.n1
*>)),0.K) by A5,Th58
.= block_diagonal(1.(K,f|n)^<*1.(K,f.n1)*>,0.K) by A5,Th57
.= block_diagonal(<*block_diagonal(1.(K,f|n),0.K)*>^<*1.(K,f.n1)*>,0.K
) by Th35
.= block_diagonal(<*1.(K,Sum (f|n)),1.(K,f.n1)*>,0.K) by A2,A4
.= 1.(K,Sum (f|n)+f.n1) by Th60
.= 1.(K,Sum f) by A6,RVSUM_1:74;
end;
A7: P[0]
proof
let f such that
A8: len f=0;
dom 1.(K,f)=dom f by Def8;
then len 1.(K,f)=0 by A8,FINSEQ_3:29;
then
A9: Sum Len 1.(K,f)=0 by RVSUM_1:72;
f = {} by A8;
hence thesis by A9,MATRIX_0:45,RVSUM_1:72;
end;
for n holds P[n] from NAT_1:sch 2(A7,A1);
then P[len f];
hence thesis;
end;
reserve p,p1 for FinSequence of K;
begin :: Operations On a Finite Sequence of Matrices
definition
let K,G,p;
func mlt(p,G) -> FinSequence_of_Matrix of K means
:Def9:
dom it = dom G & for i st i in dom it holds it.i = p/.i * G.i;
existence
proof
deffunc G(Nat)=p/.$1*G.$1;
consider IT be FinSequence such that
A1: len IT=len G and
A2: for k st k in dom IT holds IT.k=G(k) from FINSEQ_1:sch 2;
rng IT c= (the carrier of K)**
proof
let y be object;
assume y in rng IT;
then consider x being object such that
A3: x in dom IT and
A4: IT.x=y by FUNCT_1:def 3;
reconsider x as Nat by A3;
IT.x =p/.x*G.x by A2,A3;
hence thesis by A4,FINSEQ_1:def 11;
end;
then reconsider IT as FinSequence of (the carrier of K)** by FINSEQ_1:def 4
;
now
let i;
assume i in dom IT;
then IT.i=p/.i*G.i by A2;
hence IT.i is Matrix of K;
end;
then reconsider IT as FinSequence_of_Matrix of K by Def2;
take IT;
thus thesis by A1,A2,FINSEQ_3:29;
end;
uniqueness
proof
let T1,T2 be FinSequence_of_Matrix of K such that
A5: dom T1=dom G and
A6: for i st i in dom T1 holds T1.i= p/.i*G.i and
A7: dom T2=dom G and
A8: for i st i in dom T2 holds T2.i= p/.i*(G.i);
now
let i such that
A9: i in dom G;
thus T1.i = p/.i*G.i by A5,A6,A9
.= T2.i by A7,A8,A9;
end;
hence thesis by A5,A7,FINSEQ_1:13;
end;
end;
registration
let K;
let R,p;
cluster mlt(p,R) -> Square-Matrix-yielding;
coherence
proof
set M=mlt(p,R);
let i;
assume i in dom M;
then
A1: M.i=p/.i* R.i by Def9;
consider n such that
A2: R.i is Matrix of n,K;
take n;
len (R.i)=n by A2,MATRIX_0:24;
hence M.i is Matrix of n,K by A1;
end;
end;
theorem
Len mlt(p,G) = Len G & Width mlt(p,G) = Width G
proof
set M=mlt(p,G);
A1: dom Len M=dom M by Def3;
A2: dom M=dom G by Def9;
A3: dom Len G=dom G by Def3;
now
let i such that
A4: i in dom Len M;
thus (Len M).i = len (M.i) by A4,Def3
.= len (p/.i*G.i) by A1,A4,Def9
.= len (G.i) by MATRIX_3:def 5
.= (Len G).i by A1,A3,A2,A4,Def3;
end;
hence Len M=Len G by A1,A3,A2,FINSEQ_1:13;
A5: dom Width M=dom M by Def4;
A6: dom Width G=dom G by Def4;
now
let i such that
A7: i in dom Width M;
thus (Width M).i = width (M.i) by A7,Def4
.= width (p/.i*G.i) by A5,A7,Def9
.= width (G.i) by MATRIX_3:def 5
.= (Width G).i by A6,A5,A2,A7,Def4;
end;
hence thesis by A6,A5,A2,FINSEQ_1:13;
end;
theorem Th63:
mlt(p,<*A*>)=<*p/.1*A*>
proof
A1: dom mlt(p,<*A*>) = dom <*A*> by Def9
.= Seg 1 by FINSEQ_1:38;
then 1 in dom mlt(p,<*A*>);
then
A2: mlt(p,<*A*>).1 = p/.1*(<*A*>.1) by Def9
.= p/.1*A;
len mlt(p,<*A*>)=1 by A1,FINSEQ_1:def 3;
hence thesis by A2,FINSEQ_1:40;
end;
theorem Th64:
len G = len p & len G1 <=len p1 implies mlt(p^p1,G^G1) = mlt(p,G )^mlt(p1,G1)
proof
assume that
A1: len G=len p and
A2: len G1<=len p1;
A3: dom G=dom p by A1,FINSEQ_3:29;
dom G1=Seg len G1 by FINSEQ_1:def 3;
then dom G1 c= Seg len p1 by A2,FINSEQ_1:5;
then
A4: dom G1 c= dom p1 by FINSEQ_1:def 3;
set M1=mlt(p1,G1);
set M=mlt(p,G);
set GG1=G^G1;
set pp1=p^p1;
set MM=mlt(pp1,GG1);
A5: dom GG1=Seg len GG1 by FINSEQ_1:def 3;
A6: dom MM=dom GG1 by Def9;
A7: dom M1=dom G1 by Def9;
then
A8: len M1=len G1 by FINSEQ_3:29;
A9: dom M=dom G by Def9;
then
A10: len M=len G by FINSEQ_3:29;
len GG1=len G+len G1 by FINSEQ_1:22;
then len GG1<=len p+len p1 by A1,A2,XREAL_1:7;
then dom GG1 c= Seg (len p+len p1) by A5,FINSEQ_1:5;
then
A11: dom GG1 c= dom pp1 by FINSEQ_1:def 7;
A12: now
let i such that
A13: 1<=i and
A14: i<=len GG1;
A15: i in dom GG1 by A13,A14,FINSEQ_3:25;
then
A16: pp1/.i =pp1.i by A11,PARTFUN1:def 6;
A17: MM.i=pp1/.i*GG1.i by A6,A15,Def9;
now
per cases by A15,FINSEQ_1:25;
suppose
A18: i in dom G;
then
A19: GG1.i=G.i by FINSEQ_1:def 7;
A20: p.i=p/.i by A3,A18,PARTFUN1:def 6;
pp1.i=p.i by A3,A18,FINSEQ_1:def 7;
hence MM.i = M.i by A9,A17,A16,A18,A19,A20,Def9
.= (M^M1).i by A9,A18,FINSEQ_1:def 7;
end;
suppose
ex n st n in dom G1 & i=len G+n;
then consider n such that
A21: n in dom G1 and
A22: i=len G+n;
A23: GG1.i=G1.n by A21,A22,FINSEQ_1:def 7;
A24: p1/.n=p1.n by A4,A21,PARTFUN1:def 6;
pp1.i=p1.n by A1,A4,A21,A22,FINSEQ_1:def 7;
hence MM.i = M1.n by A7,A17,A16,A21,A23,A24,Def9
.= (M^M1).i by A7,A10,A21,A22,FINSEQ_1:def 7;
end;
end;
hence MM.i=(M^M1).i;
end;
A25: len (M^M1)=len M+len M1 by FINSEQ_1:22;
len MM=len GG1 by A6,FINSEQ_3:29;
hence thesis by A10,A8,A25,A12,FINSEQ_1:22;
end;
Lm7: a*block_diagonal(<*A1,A2*>,a1)=block_diagonal(<*a*A1,a*A2*>,a*a1)
proof
set AA1=a*A1;
set AA2=a*A2;
set aa1=a*a1;
set B=block_diagonal(<*A1,A2*>,a1);
A1: width AA2=width A2 by MATRIX_3:def 5;
A2: width AA1=width A1 by MATRIX_3:def 5;
then
A3: Sum Width <*AA1,AA2*> = width A1+width A2 by A1,Th20;
A4: len B = Sum Len <*A1,A2*> by Def5;
A5: len AA2=len A2 by MATRIX_3:def 5;
then
A6: dom AA2 = dom A2 by FINSEQ_3:29;
A7: Sum Width <*A1,A2*> = width A1+width A2 by Th20;
A8: Sum Len <*A1,A2*>=len A1+len A2 by Th16;
A9: len AA1=len A1 by MATRIX_3:def 5;
then
A10: dom AA1 = dom A1 by FINSEQ_3:29;
A11: now
let i;
thus i in dom AA1 implies Line(a*B,i)=Line(AA1,i)^(width AA2 |->aa1)
proof
assume
A12: i in dom AA1;
then
A13: 1<=i by FINSEQ_3:25;
A14: i<=len A1 by A9,A12,FINSEQ_3:25;
len A1<= len B by A8,A4,NAT_1:11;
then i<=len B by A14,XXREAL_0:2;
hence Line(a*B,i) = a*Line(B,i) by A13,MATRIXR1:20
.= a*(Line(A1,i)^(width A2 |->a1)) by A10,A12,Th23
.= (a*Line(A1,i))^(a*(width A2 |->a1)) by MATRIX15:4
.= Line(AA1,i)^(a*(width A2 |->a1))by A13,A14,MATRIXR1:20
.= Line(AA1,i)^(width AA2 |->aa1) by A1,FVSUM_1:53;
end;
thus i in dom AA2 implies Line(a*B,i+len AA1)=(width AA1|->aa1)^Line(AA2,i
)
proof
assume
A15: i in dom AA2;
then
A16: 1<=i by FINSEQ_3:25;
then
A17: 0+1<=i+len A1 by XREAL_1:7;
A18: i<=len A2 by A5,A15,FINSEQ_3:25;
then i+len A1<=len B by A8,A4,XREAL_1:7;
hence Line(a*B,i+len AA1) = a*Line(B,i+len A1) by A9,A17,MATRIXR1:20
.= a*((width A1|->a1)^Line(A2,i)) by A6,A15,Th23
.= (a*(width A1|->a1))^(a*Line(A2,i)) by MATRIX15:4
.= (width A1|->aa1)^(a*Line(A2,i)) by FVSUM_1:53
.= (width AA1|->aa1)^Line(AA2,i) by A2,A16,A18,MATRIXR1:20;
end;
end;
Sum Len <*AA1,AA2*>=len A1+len A2 by A9,A5,Th16;
hence thesis by A8,A3,A7,A11,Th23;
end;
theorem
a*block_diagonal(G,a1) = block_diagonal(mlt(len G|->a,G),a*a1)
proof
defpred P[Nat] means for a,a1,G st len G=$1 holds a*block_diagonal(G,a1) =
block_diagonal(mlt(len G|->a,G),a*a1);
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
set n1=n+1;
let a,a1,G such that
A3: len G=n1;
A4: G=(G|n)^<*G.n1*> by A3,FINSEQ_3:55;
n<=n1 by NAT_1:13;
then
A5: len (G|n)=n by A3,FINSEQ_1:59;
1 in Seg 1;
then 1 in dom <*a*> by FINSEQ_1:def 8;
then
A6: <*a*>.1=<*a*>/.1 by PARTFUN1:def 6;
A8: len <*a*>=1 by FINSEQ_1:39;
A9: len <*G.n1*>=1 by FINSEQ_1:39;
A10: len (n|->a)=n by CARD_1:def 7;
n1|->a=(n|->a)^<*a*> by FINSEQ_2:60;
hence
block_diagonal(mlt(len G|->a,G),a*a1) = block_diagonal(mlt(n|->a,G|n)
^mlt(<*a*>,<*G.n1*>),a*a1) by A3,A4,A5,A10,A9,A8,Th64
.= block_diagonal(mlt(n|->a,G|n)^<*a*(G.n1)*>,a*a1) by A6,Th63
.= block_diagonal(<*block_diagonal(mlt(n|->a,G|n),a*a1)*>^<*a*G.n1*>,
a*a1) by Th35
.= block_diagonal(<*a*block_diagonal(G|n,a1),a*G.n1*>,a*a1) by A2,A5
.= a*block_diagonal(<*block_diagonal(G|n,a1),G.n1*>,a1) by Lm7
.= a*block_diagonal(G,a1) by A4,Th35;
end;
A11: P[0]
proof
let a,a1,G such that
A12: len G=0;
dom mlt(len G|->a,G)=dom G by Def9;
then len mlt(len G|->a,G)=len G by FINSEQ_3:29;
then Len mlt(len G|->a,G)={} by A12;
then len block_diagonal(mlt(len G|->a,G),a*a1)=0 by Def5,RVSUM_1:72;
then
A13: block_diagonal(mlt(len G|->a,G),a*a1)={};
Len G={} by A12;
then len block_diagonal(G,a1)=0 by Def5,RVSUM_1:72;
then len (a*block_diagonal(G,a1))=0 by MATRIX_3:def 5;
hence thesis by A13;
end;
for n holds P[n] from NAT_1:sch 2(A11,A1);
hence thesis;
end;
definition
let K;
let G1,G2 be FinSequence_of_Matrix of K;
func G1(+)G2 -> FinSequence_of_Matrix of K means
:Def10:
dom it = dom G1 & for i st i in dom it holds it.i= G1.i + G2.i;
existence
proof
deffunc G(Nat)=G1.$1+G2.$1;
consider IT be FinSequence such that
A1: len IT=len G1 and
A2: for k st k in dom IT holds IT.k=G(k) from FINSEQ_1:sch 2;
rng IT c= (the carrier of K)**
proof
let y be object;
assume y in rng IT;
then consider x being object such that
A3: x in dom IT and
A4: IT.x=y by FUNCT_1:def 3;
reconsider x as Nat by A3;
IT.x =G1.x + G2.x by A2,A3;
hence thesis by A4,FINSEQ_1:def 11;
end;
then reconsider IT as FinSequence of (the carrier of K)** by FINSEQ_1:def 4
;
now
let i;
assume i in dom IT;
then IT.i=G1.i+G2.i by A2;
hence IT.i is Matrix of K;
end;
then reconsider IT as FinSequence_of_Matrix of K by Def2;
take IT;
thus thesis by A1,A2,FINSEQ_3:29;
end;
uniqueness
proof
let T1,T2 be FinSequence_of_Matrix of K such that
A5: dom T1=dom G1 and
A6: for i st i in dom T1 holds T1.i= G1.i + G2.i and
A7: dom T2=dom G1 and
A8: for i st i in dom T2 holds T2.i= G1.i + G2.i;
now
let i such that
A9: i in dom G1;
thus T1.i = G1.i+G2.i by A5,A6,A9
.= T2.i by A7,A8,A9;
end;
hence thesis by A5,A7,FINSEQ_1:13;
end;
end;
registration
let K;
let R,G;
cluster R(+)G -> Square-Matrix-yielding;
coherence
proof
set RG=R(+)G;
let i;
assume i in dom RG;
then
A1: RG.i=R.i+G.i by Def10;
consider n such that
A2: R.i is Matrix of n,K;
take n;
A3: len (R.i+G.i)=len (R.i) by MATRIX_1:def 6;
A4: width (R.i+G.i)=width (R.i) by MATRIX_1:def 6;
width (R.i)=n by A2,MATRIX_0:24;
hence RG.i is Matrix of n,K by A2,A1,A3,A4,MATRIX_0:24,51;
end;
end;
theorem Th66:
Len (G1(+)G2) = Len G1 & Width (G1(+)G2) = Width G1
proof
set G12=G1(+)G2;
A1: dom Len G12=dom G12 by Def3;
A2: dom G12=dom G1 by Def10;
A3: dom Len G1=dom G1 by Def3;
now
let i such that
A4: i in dom Len G12;
thus (Len G12).i = len (G12.i) by A4,Def3
.= len (G1.i+G2.i) by A1,A4,Def10
.= len (G1.i) by MATRIX_1:def 6
.= (Len G1).i by A3,A1,A2,A4,Def3;
end;
hence Len G12=Len G1 by A3,A1,A2,FINSEQ_1:13;
A5: dom Width G12=dom G12 by Def4;
A6: dom Width G1=dom G1 by Def4;
now
let i such that
A7: i in dom Width G12;
thus (Width G12).i = width (G12.i) by A7,Def4
.= width (G1.i+G2.i) by A5,A7,Def10
.= width (G1.i) by MATRIX_1:def 6
.= (Width G1).i by A6,A5,A2,A7,Def4;
end;
hence thesis by A6,A5,A2,FINSEQ_1:13;
end;
theorem Th67:
len G = len G9 implies (G^G1)(+)(G9^G2) = (G(+)G9)^(G1(+)G2)
proof
set GG9=G(+)G9;
set G12=G1(+)G2;
set GG1=G^G1;
set GG2=G9^G2;
A1: len GG1=len G+len G1 by FINSEQ_1:22;
A2: dom GG9=dom G by Def10;
then
A3: len GG9=len G by FINSEQ_3:29;
A4: dom (GG1(+)GG2)= dom GG1 by Def10;
then
A5: len (GG1(+)GG2)=len GG1 by FINSEQ_3:29;
assume
A6: len G=len G9;
then
A7: len GG2=len G+len G2 by FINSEQ_1:22;
A8: len (GG9^G12)=len GG9+len G12 by FINSEQ_1:22;
A9: dom G12=dom G1 by Def10;
A10: dom G=dom G9 by A6,FINSEQ_3:29;
A11: now
let i such that
A12: 1<=i and
A13: i<= len G+len G1;
A14: i in dom (GG1(+)GG2) by A4,A1,A12,A13,FINSEQ_3:25;
then
A15: (GG1(+)GG2).i=GG1.i + GG2.i by Def10;
now
per cases by A4,A14,FINSEQ_1:25;
suppose
A16: i in dom G;
hence (GG1(+)GG2).i = G.i+ GG2.i by A15,FINSEQ_1:def 7
.= G.i +G9.i by A10,A16,FINSEQ_1:def 7
.= GG9.i by A2,A16,Def10
.= (GG9^G12).i by A2,A16,FINSEQ_1:def 7;
end;
suppose
ex n st n in dom G1 & i=len G + n;
then consider n such that
A17: n in dom G1 and
A18: i=len G+n;
now
per cases;
suppose
n in dom G2;
hence GG2.i=G2.n by A6,A18,FINSEQ_1:def 7;
end;
suppose
A19: not n in dom G2;
then n<1 or n>len G2 by FINSEQ_3:25;
then i>len G+len G2 by A17,A18,FINSEQ_3:25,XREAL_1:8;
then not i in dom GG2 by A7,FINSEQ_3:25;
hence GG2.i = {} by FUNCT_1:def 2
.= G2.n by A19,FUNCT_1:def 2;
end;
end;
hence (GG1(+)GG2).i = G1.n+G2.n by A15,A17,A18,FINSEQ_1:def 7
.= G12.n by A9,A17,Def10
.= (GG9^G12).i by A9,A3,A17,A18,FINSEQ_1:def 7;
end;
end;
hence (GG1(+)GG2).i=(GG9^G12).i;
end;
len G12=len G1 by A9,FINSEQ_3:29;
hence thesis by A3,A5,A1,A8,A11;
end;
theorem Th68:
<*A*>(+)G = <*A + G.1*>
proof
dom (<*A*>(+) G)=dom <*A*> by Def10;
then
A1: len (<*A*>(+) G) = len <*A*> by FINSEQ_3:29
.= 1 by FINSEQ_1:39;
then dom (<*A*>(+) G)={1} by FINSEQ_1:2,def 3;
then 1 in dom (<*A*>(+) G) by TARSKI:def 1;
then (<*A*>(+) G).1 = (<*A*>.1)+G.1 by Def10
.= A+G.1;
hence thesis by A1,FINSEQ_1:40;
end;
theorem Th69:
<*A1*>(+)<*A2*> = <* A1+A2 *>
proof
thus <*A1*>(+)<*A2*> = <* A1 + (<*A2*>.1)*> by Th68
.= <*A1+A2*>;
end;
theorem Th70:
<*A1,B1*>(+)<*A2,B2*> = <*A1+A2,B1+B2*>
proof
A1: len <*A2*>=1 by FINSEQ_1:39;
len <*A1*>=1 by FINSEQ_1:39;
hence (<*A1,B1*>)(+)(<*A2,B2*>) = (<*A1*>(+)<*A2*>)^(<*B1*>(+)<*B2*>) by A1
,Th67
.= (<*A1*>(+)<*A2*>)^(<*B1+B2*>) by Th69
.= <*A1+A2,B1+B2*> by Th69;
end;
Lm8: width A1=width A2 & i in dom A1 implies Line(A1+A2,i)=Line(A1,i)+Line(A2,
i) by MATRIX_4:59;
theorem Th71:
len A1 = len B1 & len A2 = len B2 & width A1 = width B1 & width
A2 = width B2 implies block_diagonal(<*A1,A2*>,a1) + block_diagonal(<*B1,B2*>,
a2) = block_diagonal(<*A1,A2*>(+)<*B1,B2*>,a1+a2)
proof
assume that
A1: len A1 = len B1 and
A2: len A2 = len B2 and
A3: width A1 = width B1 and
A4: width A2 = width B2;
set b12=<*B1,B2*>;
set a12=<*A1,A2*>;
set AB2=A2+B2;
set AB1=A1+B1;
set ab=a12(+)b12;
set bA=block_diagonal(a12,a1);
set bB=block_diagonal(b12,a2);
set bAB=block_diagonal(ab,a1+a2);
A5: len (bA+bB)=len bA by MATRIX_1:def 6;
width (bA+bB)=width bA by MATRIX_1:def 6;
then reconsider bAbB=bA+bB as Matrix of len bA,width bA,K by A5,MATRIX_0:51;
A6: len AB1=len A1 by MATRIX_1:def 6;
A7: len bA=Sum Len a12 by Def5;
A8: Sum Len a12=len A1+len A2 by Th16;
A9: len AB2=len A2 by MATRIX_1:def 6;
A10: Sum Width b12=width B1+width B2 by Th20;
A11: len bAB=Sum Len ab by Def5;
A12: width bB=Sum Width b12 by Def5;
A13: width bA=Sum Width a12 by Def5;
A14: width AB2=width A2 by MATRIX_1:def 6;
A15: width AB1=width A1 by MATRIX_1:def 6;
A16: Len ab=Len a12 by Th66;
A17: ab = <*AB1,AB2*> by Th70;
now
A18: dom bA =Seg len bA by FINSEQ_1:def 3;
let i such that
A19: 1<= i and
A20: i<=len bAB;
A21: i in Seg len bAB by A19,A20;
then
A22: bAB.i=Line(block_diagonal(<*AB1,AB2*>,a1+a2),i) by A17,A11,MATRIX_0:52;
A23: bAbB.i=Line(bA+bB,i) by A16,A7,A11,A21,MATRIX_0:52;
A24: dom (A1^A2)=Seg len bAB by A8,A16,A11,FINSEQ_1:def 7;
now
per cases by A21,A24,FINSEQ_1:25;
suppose
A25: i in dom A1;
A26: len Line(B1,i)=width B1 by CARD_1:def 7;
A27: dom A1=dom B1 by A1,FINSEQ_3:29;
A28: len Line(A1,i)=width A1 by CARD_1:def 7;
dom A1=dom AB1 by A6,FINSEQ_3:29;
hence bAB.i = Line(AB1,i)^(width AB2|->(a1+a2)) by A22,A25,Th23
.= (Line(A1,i)+Line(B1,i))^(width AB2|->(a1+a2)) by A3,A25,Lm8
.= (Line(A1,i)+Line(B1,i))^ ((width AB2|->a1)+(width AB2|->a2)) by
FVSUM_1:20
.= (Line(A1,i)^(width A2|->a1))+ (Line(B1,i)^(width B2|->a2)) by A3
,A4,A14,A28,A26,Th1
.= Line(bA,i)+(Line(B1,i)^(width B2|->a2)) by A25,Th23
.= Line(bA,i)+Line(bB,i) by A25,A27,Th23
.= bAbB.i by A3,A4,A10,A16,A7,A13,A12,A11,A21,A18,A23,Lm8,Th20;
end;
suppose
A29: ex n st n in dom A2 & i=len A1+n;
A30: len (width AB1|->a1)=width AB1 by CARD_1:def 7;
A31: dom A2=dom B2 by A2,FINSEQ_3:29;
A32: len (width AB1|->a2)=width AB1 by CARD_1:def 7;
consider n such that
A33: n in dom A2 and
A34: i=len A1+n by A29;
dom A2=dom AB2 by A9,FINSEQ_3:29;
hence bAB.i = (width AB1|->(a1+a2))^Line(AB2,n) by A6,A22,A33,A34,Th23
.= (width AB1|->(a1+a2))^(Line(A2,n)+Line(B2,n)) by A4,A33,Lm8
.= ((width AB1|->a1)+(width AB1|->a2))^ (Line(A2,n)+Line(B2,n)) by
FVSUM_1:20
.= ((width AB1|->a1)^Line(A2,n))+ ((width AB1|->a2)^Line(B2,n)) by
A30,A32,Th1
.=Line(bA,i)+((width B1|->a2)^Line(B2,n)) by A3,A15,A33,A34,Th23
.=Line(bA,i)+Line(bB,i) by A1,A33,A34,A31,Th23
.=bAbB.i by A3,A4,A10,A16,A7,A13,A12,A11,A21,A18,A23,Lm8,Th20;
end;
end;
hence bAB.i=(bA+bB).i;
end;
hence thesis by A16,A7,A11,A5;
end;
theorem
Len R1 = Len R2 & Width R1 = Width R2 implies block_diagonal(R1,a1) +
block_diagonal(R2,a2) = block_diagonal(R1(+)R2,a1+a2)
proof
defpred P[Nat] means for R1,R2,a1,a2 st Len R1=Len R2 & Width R1=Width R2 &
len R1=$1 holds block_diagonal(R1,a1)+block_diagonal(R2,a2)= block_diagonal(R1
(+)R2,a1+a2);
assume that
A1: Len R1=Len R2 and
A2: Width R1=Width R2;
A3: for n st P[n] holds P[n+1]
proof
let n such that
A4: P[n];
set n1=n+1;
let R1,R2,a1,a2 such that
A5: Len R1=Len R2 and
A6: Width R1=Width R2 and
A7: len R1=n1;
A8: n1 in Seg n1 by FINSEQ_1:4;
set R2n=R2|n;
A9: R1=(R1|n)^<*R1.n1*> by A7,FINSEQ_3:55;
set R1n=R1|n;
set b2n=block_diagonal(R2n,a2);
set b1n=block_diagonal(R1n,a1);
A10: len R1n=n by A7,FINSEQ_1:59,NAT_1:11;
A11: dom Len R1=Seg n1 by A7,FINSEQ_2:124;
then
A12: len (R1.n1) = (Len R1).n1 by A8,Def3
.= len (R2.n1) by A5,A8,A11,Def3;
A13: len R1 = len Len R2 by A5,CARD_1:def 7
.= len R2 by CARD_1:def 7;
then
A14: len R2n=n by A7,FINSEQ_1:59,NAT_1:11;
A15: dom Width R1=Seg n1 by A7,FINSEQ_2:124;
then
A16: width (R1.n1) = (Width R1).n1 by A8,Def4
.= width (R2.n1) by A6,A8,A15,Def4;
A17: Len R1n = (Len R1) |n by Th17
.= Len R2n by A5,Th17;
then
A18: len b1n = Sum Len R2n by Def5
.= len b2n by Def5;
A19: Width R1n = (Width R1) |n by Th21
.= Width R2n by A6,Th21;
then
A20: width b1n = Sum Width R2n by Def5
.= width b2n by Def5;
A21: R2=(R2|n)^<*R2.n1*> by A7,A13,FINSEQ_3:55;
hence
block_diagonal(R1,a1)+block_diagonal(R2,a2) = block_diagonal(<*b1n,R1
.n1*>,a1)+block_diagonal(R2n^<*R2.n1*>,a2) by A9,Th35
.= block_diagonal(<*b1n,R1.n1*>,a1)+block_diagonal(<*b2n,R2.n1*>,a2)
by Th35
.= block_diagonal(<*b1n,R1.n1*>(+)<*b2n,R2.n1*>,a1+a2) by A18,A20,A12,A16
,Th71
.= block_diagonal(<*b1n+b2n,R1.n1+R2.n1*>,a1+a2) by Th70
.= block_diagonal(<*block_diagonal(R1n(+)R2n,a1+a2),R1.n1+R2.n1*>, a1+
a2) by A4,A10,A17,A19
.= block_diagonal((R1n(+)R2n)^<*R1.n1+R2.n1*>,a1+a2) by Th35
.= block_diagonal((R1n(+)R2n)^(<*R1.n1*>(+)<*R2.n1*>),a1+a2) by Th69
.= block_diagonal(R1(+)R2,a1+a2) by A10,A14,A9,A21,Th67;
end;
A22: P[0]
proof
let R1,R2,a1,a2 such that
Len R1=Len R2 and
Width R1=Width R2 and
A23: len R1=0;
set b12=block_diagonal(R1(+)R2,a1+a2);
set b2=block_diagonal(R2,a2);
set b1=block_diagonal(R1,a1);
A24: Len R1={} by A23;
Len R1=Len(R1(+)R2) by Th66;
then len b12=0 by A24,Def5,RVSUM_1:72;
then
A25: b12={};
len b1=0 by A24,Def5,RVSUM_1:72;
then len (b1+b2)=0 by MATRIX_1:def 6;
hence thesis by A25;
end;
for n holds P[n] from NAT_1:sch 2(A22,A3);
hence thesis by A1,A2;
end;
definition
let K;
let G1,G2 be FinSequence_of_Matrix of K;
func G1(#)G2 -> FinSequence_of_Matrix of K means
:Def11:
dom it = dom G1 & for i st i in dom it holds it.i= G1.i * G2.i;
existence
proof
deffunc G(Nat)=G1.$1*G2.$1;
consider IT be FinSequence such that
A1: len IT=len G1 and
A2: for k st k in dom IT holds IT.k=G(k) from FINSEQ_1:sch 2;
rng IT c= (the carrier of K)**
proof
let y be object;
assume y in rng IT;
then consider x being object such that
A3: x in dom IT and
A4: IT.x=y by FUNCT_1:def 3;
reconsider x as Nat by A3;
IT.x =G1.x * G2.x by A2,A3;
hence thesis by A4,FINSEQ_1:def 11;
end;
then reconsider IT as FinSequence of (the carrier of K)** by FINSEQ_1:def 4
;
now
let i;
assume i in dom IT;
then IT.i=G1.i*G2.i by A2;
hence IT.i is Matrix of K;
end;
then reconsider IT as FinSequence_of_Matrix of K by Def2;
take IT;
thus thesis by A1,A2,FINSEQ_3:29;
end;
uniqueness
proof
let T1,T2 be FinSequence_of_Matrix of K such that
A5: dom T1=dom G1 and
A6: for i st i in dom T1 holds T1.i= G1.i * G2.i and
A7: dom T2=dom G1 and
A8: for i st i in dom T2 holds T2.i= G1.i * G2.i;
now
let i such that
A9: i in dom G1;
thus T1.i = G1.i*G2.i by A5,A6,A9
.= T2.i by A7,A8,A9;
end;
hence thesis by A5,A7,FINSEQ_1:13;
end;
end;
theorem Th73:
Width G1 = Len G2 implies Len (G1(#)G2) = Len G1 & Width (G1(#)
G2) = Width G2
proof
assume
A1: Width G1=Len G2;
set G12=G1(#)G2;
A2: dom Len G12=dom G12 by Def3;
A3: dom G12=dom G1 by Def11;
A4: dom Width G2=dom G2 by Def4;
A5: dom Width G1=dom G1 by Def4;
A6: dom Len G1=dom G1 by Def3;
now
let i such that
A7: i in dom Len G12;
A8: width (G1.i) = (Width G1).i by A2,A5,A3,A7,Def4
.= len (G2.i) by A1,A2,A5,A3,A7,Def3;
thus (Len G12).i = len (G12.i) by A7,Def3
.= len (G1.i*G2.i) by A2,A7,Def11
.= len (G1.i) by A8,MATRIX_3:def 4
.= (Len G1).i by A6,A2,A3,A7,Def3;
end;
hence Len G12=Len G1 by A6,A2,A3,FINSEQ_1:13;
A9: dom Width G12=dom G12 by Def4;
A10: dom Len G2=dom G2 by Def3;
now
let i such that
A11: i in dom Width G12;
A12: width (G1.i) = (Width G1).i by A5,A9,A3,A11,Def4
.= len (G2.i) by A1,A5,A9,A3,A11,Def3;
thus (Width G12).i = width (G12.i) by A11,Def4
.= width (G1.i*G2.i) by A9,A11,Def11
.= width (G2.i) by A12,MATRIX_3:def 4
.= (Width G2).i by A1,A5,A10,A9,A4,A3,A11,Def4;
end;
hence thesis by A1,A5,A10,A9,A4,A3,FINSEQ_1:13;
end;
theorem Th74:
len G = len G9 implies (G^G1)(#)(G9^G2) = (G(#)G9)^(G1(#)G2)
proof
set GG9=G(#)G9;
set G12=G1(#)G2;
set GG1=G^G1;
set GG2=G9^G2;
A1: len GG1=len G+len G1 by FINSEQ_1:22;
A2: dom GG9=dom G by Def11;
then
A3: len GG9=len G by FINSEQ_3:29;
A4: dom (GG1(#)GG2)= dom GG1 by Def11;
then
A5: len (GG1(#)GG2)=len GG1 by FINSEQ_3:29;
assume
A6: len G=len G9;
then
A7: len GG2=len G+len G2 by FINSEQ_1:22;
A8: len (GG9^G12)=len GG9+len G12 by FINSEQ_1:22;
A9: dom G12=dom G1 by Def11;
A10: dom G=dom G9 by A6,FINSEQ_3:29;
A11: now
let i such that
A12: 1<=i and
A13: i<= len G+len G1;
A14: i in dom (GG1(#)GG2) by A4,A1,A12,A13,FINSEQ_3:25;
then
A15: (GG1(#)GG2).i=GG1.i * GG2.i by Def11;
now
per cases by A4,A14,FINSEQ_1:25;
suppose
A16: i in dom G;
hence (GG1(#)GG2).i = G.i* GG2.i by A15,FINSEQ_1:def 7
.= G.i *G9.i by A10,A16,FINSEQ_1:def 7
.= GG9.i by A2,A16,Def11
.= (GG9^G12).i by A2,A16,FINSEQ_1:def 7;
end;
suppose
ex n st n in dom G1 & i=len G + n;
then consider n such that
A17: n in dom G1 and
A18: i=len G+n;
now
per cases;
suppose
n in dom G2;
hence GG2.i=G2.n by A6,A18,FINSEQ_1:def 7;
end;
suppose
A19: not n in dom G2;
then n<1 or n>len G2 by FINSEQ_3:25;
then i>len G+len G2 by A17,A18,FINSEQ_3:25,XREAL_1:8;
then not i in dom GG2 by A7,FINSEQ_3:25;
hence GG2.i = {} by FUNCT_1:def 2
.= G2.n by A19,FUNCT_1:def 2;
end;
end;
hence (GG1(#)GG2).i = G1.n*G2.n by A15,A17,A18,FINSEQ_1:def 7
.= G12.n by A9,A17,Def11
.= (GG9^G12).i by A9,A3,A17,A18,FINSEQ_1:def 7;
end;
end;
hence (GG1(#)GG2).i=(GG9^G12).i;
end;
len G12=len G1 by A9,FINSEQ_3:29;
hence thesis by A3,A5,A1,A8,A11;
end;
theorem Th75:
<*A*>(#)G = <*A * G.1*>
proof
dom (<*A*>(#) G)=dom <*A*> by Def11;
then
A1: len (<*A*>(#) G) = len <*A*> by FINSEQ_3:29
.= 1 by FINSEQ_1:39;
then dom (<*A*>(#) G)={1} by FINSEQ_1:2,def 3;
then 1 in dom (<*A*>(#) G) by TARSKI:def 1;
then (<*A*>(#) G).1 = (<*A*>.1)*G.1 by Def11
.= A*G.1;
hence thesis by A1,FINSEQ_1:40;
end;
theorem Th76:
<*A1*>(#)<*A2*> = <* A1*A2 *>
proof
thus <*A1*>(#)<*A2*> = <* A1 * (<*A2*>.1)*> by Th75
.= <*A1*A2*>;
end;
theorem Th77:
<*A1,B1*>(#)<*A2,B2*> = <*A1*A2,B1*B2*>
proof
A1: len <*A2*>=1 by FINSEQ_1:39;
len <*A1*>=1 by FINSEQ_1:39;
hence (<*A1,B1*>)(#)(<*A2,B2*>) = (<*A1*>(#)<*A2*>)^(<*B1*>(#)<*B2*>) by A1
,Th74
.= (<*A1*>(#)<*A2*>)^(<*B1*B2*>) by Th76
.= <*A1*A2,B1*B2*> by Th76;
end;
Lm9: for R1,S1 be Element of i-tuples_on the carrier of K, R2,S2 be Element of
j-tuples_on the carrier of K holds Sum (mlt(R1^R2,S1^S2)) = Sum(mlt(R1,S1))+Sum
(mlt(R2,S2))
proof
let R1,S1 be Element of i-tuples_on the carrier of K, R2,S2 be Element of j
-tuples_on the carrier of K;
mlt(R1^R2,S1^S2)=mlt(R1,S1)^mlt(R2,S2) by FINSEQOP:11;
hence thesis by RLVECT_1:41;
end;
theorem Th78:
width A1 = len B1 & width A2 = len B2 implies block_diagonal(<*
A1,A2*>,0.K)*block_diagonal(<*B1,B2*>,0.K) = block_diagonal(<*A1,A2*>(#)(<*B1,
B2*>),0.K)
proof
assume that
A1: width A1=len B1 and
A2: width A2=len B2;
A3: width (A1*B1)=width B1 by A1,MATRIX_3:def 4;
set b12=<*B1,B2*>;
set a12=<*A1,A2*>;
set b2=<*B2*>;
set b1=<*B1*>;
set a2=<*A2*>;
set a1=<*A1*>;
set ab=a12(#)b12;
A4: Len b12=(Len b1)^Len b2 by Th14;
set bB=block_diagonal(b12,0.K);
set bA=block_diagonal(a12,0.K);
A5: Sum Width a12=width bA by Def5;
A6: Sum Len b12=len bB by Def5;
A7: Width a1= <*width A1*> by Th19;
set bAbB=bA*bB;
set bAB=block_diagonal(ab,0.K);
A8: Sum Len ab=len bAB by Def5;
A9: Sum Width ab=width bAB by Def5;
A10: Sum Len a12=len A1+len A2 by Th16;
A11: Sum Width b12= width B1+width B2 by Th20;
A12: len (A2*B2)=len A2 by A2,MATRIX_3:def 4;
A13: ab = <*A1*B1,A2*B2*> by Th77;
A14: Width a2=<*width A2*> by Th19;
A15: Len b2= <*len B2*> by Th15;
A16: Len b1=<*len B1*> by Th15;
A17: Width a12=(Width a1)^Width a2 by Th18;
then
A18: Len ab=Len a12 by A1,A2,A4,A7,A14,A16,A15,Th73;
A19: Width ab=Width b12 by A1,A2,A17,A4,A7,A14,A16,A15,Th73;
Sum Len a12=len bA by Def5;
then
A20: len (bA*bB)=Sum Len a12 by A1,A2,A17,A4,A7,A14,A16,A15,A5,A6,
MATRIX_3:def 4;
A21: len (A1*B1)=len A1 by A1,MATRIX_3:def 4;
Sum Width b12=width bB by Def5;
then
A22: width (bA*bB)=Sum Width b12 by A1,A2,A17,A4,A7,A14,A16,A15,A5,A6,
MATRIX_3:def 4;
A23: width (A2*B2)=width B2 by A2,MATRIX_3:def 4;
A24: Indices (A1*B1) = [:Seg len (A1*B1),Seg width (A1*B1):] by FINSEQ_1:def 3
.= [:dom A1,Seg width B1:] by A3,A21,FINSEQ_1:def 3;
now
A25: dom bAB=Seg len bAB by FINSEQ_1:def 3;
let i,j such that
A26: [i,j] in Indices bAB;
A27: j in Seg width bAB by A26,ZFMISC_1:87;
A28: i in dom bAB by A26,ZFMISC_1:87;
then
A29: 1<=i by A25,FINSEQ_1:1;
Indices bAB = [:Seg len bAB,Seg width bAB:] by FINSEQ_1:def 3
.= Indices bAbB by A8,A9,A20,A22,A18,A19,FINSEQ_1:def 3;
then
A30: bAbB*(i,j) = Line(bA,i) "*" Col(bB,j) by A1,A2,A17,A4,A7,A14,A16,A15,A5,A6
,A26,MATRIX_3:def 4
.= Sum(mlt(Line(bA,i),Col(bB,j)));
A31: 1<=j by A27,FINSEQ_1:1;
now
per cases;
suppose
A32: i<=len A1;
then
A33: i in dom (A1*B1) by A21,A29,FINSEQ_3:25;
A34: i in dom A1 by A29,A32,FINSEQ_3:25;
then
A35: Line(bA,i)=Line(A1,i)^(width A2 |-> 0.K) by Th23;
now
per cases;
suppose
j<=width B1;
then
A36: j in Seg width B1 by A31;
then
A37: [i,j] in Indices (A1*B1) by A24,A34,ZFMISC_1:87;
A38: dom Line(A1*B1,i)=Seg width B1 by A3,FINSEQ_2:124;
Col(bB,j)=Col(B1,j)^(len B2|->0.K) by A36,Th24;
hence
bAbB*(i,j) = Sum(mlt(Line(A1,i),Col(B1,j)))+ Sum(mlt(width A2
|->0.K,len B2|->0.K)) by A1,A2,A30,A35,Lm9
.= Sum(mlt(Line(A1,i),Col(B1,j)))+ Sum(0.K*(width A2|->0.K))
by A2,FVSUM_1:66
.= Sum(mlt(Line(A1,i),Col(B1,j)))+ 0.K*Sum(width A2|->0.K) by
FVSUM_1:73
.= Sum(mlt(Line(A1,i),Col(B1,j)))+0.K
.= Line(A1,i)"*"Col(B1,j) by RLVECT_1:def 4
.= (A1*B1)*(i,j) by A1,A37,MATRIX_3:def 4
.= Line(A1*B1,i).j by A3,A36,MATRIX_0:def 7
.= (Line(A1*B1,i)^(width (A2*B2) |-> 0.K)).j by A36,A38,
FINSEQ_1:def 7
.= Line(bAB,i).j by A13,A33,Th23
.= bAB*(i,j) by A27,MATRIX_0:def 7;
end;
suppose
A39: j>width B1;
then reconsider J=j-width B1 as Element of NAT by NAT_1:21;
A40: j=J+width B1;
A41: len Line(A1*B1,i)=width B1 by A3,CARD_1:def 7;
A42: dom (width (A2*B2) |-> 0.K)= Seg width B2 by A23,FINSEQ_2:124;
J<>0 by A39;
then
A43: J in Seg width B2 by A9,A19,A11,A27,A40,FINSEQ_1:61;
then Col(bB,J+width B1)=(len B1 |-> 0.K)^Col(B2,J) by Th24;
hence bAbB*(i,j) = Sum(mlt(Line(A1,i),len B1 |-> 0.K))+ Sum(mlt(
width A2|->0.K,Col(B2,J))) by A1,A2,A30,A35,Lm9
.= Sum(mlt(Line(A1,i),len B1 |-> 0.K))+ Sum(0.K*Col(B2,J)) by A2,
FVSUM_1:66
.= Sum(0.K*Line(A1,i))+Sum(0.K*Col(B2,J)) by A1,FVSUM_1:66
.= Sum(0.K*Line(A1,i))+0.K*Sum Col(B2,J) by FVSUM_1:73
.= 0.K*Sum Line(A1,i)+0.K*Sum Col(B2,J) by FVSUM_1:73
.= 0.K*Sum Line(A1,i)+0.K
.= 0.K+0.K
.= 0.K by RLVECT_1:def 4
.= (width (A2*B2) |-> 0.K).J by A23,A43,FINSEQ_2:57
.= (Line(A1*B1,i)^(width (A2*B2) |->0.K)). (J+width (A1*B1)) by
A3,A43,A41,A42,FINSEQ_1:def 7
.= Line(bAB,i).j by A13,A3,A33,Th23
.= bAB*(i,j) by A27,MATRIX_0:def 7;
end;
end;
hence bAbB*(i,j)=bAB*(i,j);
end;
suppose
A44: i>len A1;
then reconsider I=i-len A1 as Element of NAT by NAT_1:21;
A45: i=I+len A1;
A46: dom A2=dom (A2*B2) by A12,FINSEQ_3:29;
I<>0 by A44;
then I in Seg len A2 by A8,A18,A10,A28,A25,A45,FINSEQ_1:61;
then
A47: I in dom A2 by FINSEQ_1:def 3;
then
A48: Line(bA,I+len A1)=(width A1 |-> 0.K)^Line(A2,I) by Th23;
now
per cases;
suppose
A49: j<=width B1;
A50: dom (width (A1*B1) |->0.K)=Seg width B1 by A3,FINSEQ_2:124;
A51: j in Seg width B1 by A31,A49;
then Col(bB,j)=Col(B1,j)^(len B2 |-> 0.K) by Th24;
hence bAbB*(i,j) = Sum(mlt(width A1 |-> 0.K,Col(B1,j))) + Sum(mlt(
Line(A2,I),len B2|->0.K)) by A1,A2,A30,A48,Lm9
.= Sum(mlt(width A1 |-> 0.K,Col(B1,j))) + Sum(0.K*Line(A2,I))
by A2,FVSUM_1:66
.= Sum(0.K*Col(B1,j))+Sum(0.K*Line(A2,I)) by A1,FVSUM_1:66
.= Sum(0.K*Col(B1,j))+0.K*Sum Line(A2,I) by FVSUM_1:73
.= 0.K*Sum Col(B1,j)+0.K*Sum Line(A2,I) by FVSUM_1:73
.= 0.K*Sum Col(B1,j)+0.K
.= 0.K+0.K
.= 0.K by RLVECT_1:def 4
.= (width (A1*B1) |-> 0.K).j by A3,A51,FINSEQ_2:57
.= ((width (A1*B1) |-> 0.K)^Line(A2*B2,I)).j by A51,A50,
FINSEQ_1:def 7
.= Line(bAB,I+len A1).j by A13,A21,A47,A46,Th23
.= bAB*(i,j) by A27,MATRIX_0:def 7;
end;
suppose
A52: j>width B1;
then reconsider J=j-width B1 as Element of NAT by NAT_1:21;
A53: j=J+width B1;
J<>0 by A52;
then
A54: J in Seg width B2 by A9,A19,A11,A27,A53,FINSEQ_1:61;
then
A55: [I,J] in Indices (A2*B2) by A23,A47,A46,ZFMISC_1:87;
A56: len (width (A1*B1) |->0.K)=width B1 by A3,CARD_1:def 7;
A57: dom Line(A2*B2,I)=Seg width B2 by A23,FINSEQ_2:124;
Col(bB,J+width B1)=(len B1 |-> 0.K)^Col(B2,J) by A54,Th24;
hence bAbB*(i,j) = Sum(mlt(width A1 |-> 0.K,len B1|->0.K)) + Sum(
mlt(Line(A2,I),Col(B2,J))) by A1,A2,A30,A48,Lm9
.= Sum(0.K*(width A1 |-> 0.K)) + Sum(mlt(Line(A2,I),Col(B2,J))
) by A1,FVSUM_1:66
.= 0.K*Sum(width A1|->0.K) + Sum(mlt(Line(A2,I),Col(B2,J)))by
FVSUM_1:73
.= 0.K+Sum(mlt(Line(A2,I),Col(B2,J)))
.= Line(A2,I)"*"Col(B2,J) by RLVECT_1:def 4
.= (A2*B2)*(I,J) by A2,A55,MATRIX_3:def 4
.= Line(A2*B2,I).J by A23,A54,MATRIX_0:def 7
.= ((width (A1*B1) |->0.K)^Line(A2*B2,I)). (J+width B1) by A54
,A57,A56,FINSEQ_1:def 7
.= Line(bAB,I+len A1).j by A13,A21,A47,A46,Th23
.= bAB*(i,j) by A27,MATRIX_0:def 7;
end;
end;
hence bAbB*(i,j)=bAB*(i,j);
end;
end;
hence bAB*(i,j)=bAbB*(i,j);
end;
hence thesis by A8,A9,A20,A22,A18,A19,MATRIX_0:21;
end;
theorem
Width R1 = Len R2 implies block_diagonal(R1,0.K)*block_diagonal(R2,0.K
)= block_diagonal(R1(#)R2,0.K)
proof
defpred P[Nat] means for R1,R2 st Width R1=Len R2 & len R1=$1 holds
block_diagonal(R1,0.K)*block_diagonal(R2,0.K)= block_diagonal(R1(#)R2,0.K);
assume
A1: Width R1=Len R2;
A2: for n st P[n] holds P[n+1]
proof
let n such that
A3: P[n];
set n1=n+1;
let R1,R2 such that
A4: Width R1=Len R2 and
A5: len R1=n1;
A6: n1 in Seg n1 by FINSEQ_1:4;
set R1n=R1|n;
A7: len R1n=n by A5,FINSEQ_1:59,NAT_1:11;
set R2n=R2|n;
A8: len R1 = len Len R2 by A4,CARD_1:def 7
.= len R2 by CARD_1:def 7;
then
A9: len R2n=n by A5,FINSEQ_1:59,NAT_1:11;
set b2n=block_diagonal(R2n,0.K);
set b1n=block_diagonal(R1n,0.K);
A10: Width R1n = (Width R1) |n by Th21
.= Len R2n by A4,Th17;
A11: dom Width R1=Seg n1 by A5,FINSEQ_2:124;
then
A12: width (R1.n1) = (Len R2).n1 by A4,A6,Def4
.= len (R2.n1) by A4,A6,A11,Def3;
A13: R1=(R1|n)^<*R1.n1*> by A5,FINSEQ_3:55;
A14: width b1n = Sum Width R1n by Def5
.= len b2n by A10,Def5;
A15: R2=(R2|n)^<*R2.n1*> by A5,A8,FINSEQ_3:55;
hence
block_diagonal(R1,0.K)*block_diagonal(R2,0.K) = block_diagonal(<*b1n,
R1.n1*>,0.K)*block_diagonal(R2n^<*R2.n1*>,0.K) by A13,Th35
.= block_diagonal(<*b1n,R1.n1*>,0.K)*block_diagonal(<*b2n,R2.n1*>,0.K)
by Th35
.= block_diagonal((<*b1n,R1.n1*>)(#)(<*b2n,R2.n1*>),0.K) by A14,A12,Th78
.= block_diagonal(<*b1n*b2n,R1.n1*R2.n1*>,0.K) by Th77
.= block_diagonal(<*block_diagonal(R1n(#)R2n,0.K),R1.n1*R2.n1*>,0.K)
by A3,A7,A10
.= block_diagonal((R1n(#)R2n)^<*R1.n1*R2.n1*>,0.K) by Th35
.= block_diagonal((R1n(#)R2n)^(<*R1.n1*>(#)<*R2.n1*>),0.K) by Th76
.= block_diagonal(R1(#)R2,0.K) by A7,A9,A13,A15,Th74;
end;
A16: P[0]
proof
let R1,R2 such that
A17: Width R1=Len R2 and
A18: len R1=0;
A19: Sum Width R1=0 by A18,RVSUM_1:72;
set b2=block_diagonal(R2,0.K);
Len R2 ={} by A17,A18;
then
A20: len b2=0 by Def5,RVSUM_1:72;
set b1=block_diagonal(R1,0.K);
A21: Sum Width R1=width b1 by Def5;
set b12=block_diagonal(R1(#)R2,0.K);
A22: Len R1={} by A18;
Len R1=Len(R1(#)R2) by A17,Th73;
then len b12=0 by A22,Def5,RVSUM_1:72;
then
A23: b12={};
len b1=0 by A22,Def5,RVSUM_1:72;
then len (b1*b2)=0 by A20,A21,A19,MATRIX_3:def 4;
hence thesis by A23;
end;
for n holds P[n] from NAT_1:sch 2(A16,A2);
hence thesis by A1;
end;