:: Block Diagonal Matrices
:: by Karol P\c{a}k
::
:: Received May 13, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

Lm1:  for K being non empty addLoopStr
for p1, p2 being FinSequence of K holds dom (p1 + p2) = (dom p1) /\ (dom p2)
proofend;

theorem Th1: :: MATRIXJ1:1
for K being non empty addLoopStr
for f1, f2, g1, g2 being FinSequence of K st len f1 = len f2 holds
(f1 + f2) ^ (g1 + g2) = (f1 ^ g1) + (f2 ^ g2)
proofend;

theorem Th2: :: MATRIXJ1:2
for i being Nat
for D being non empty set
for f, g being FinSequence of D st i in dom f holds
Del ((f ^ g),i) = (Del (f,i)) ^ g
proofend;

theorem Th3: :: MATRIXJ1:3
for i being Nat
for D being non empty set
for f, g being FinSequence of D st i in dom g holds
Del ((f ^ g),(i + (len f))) = f ^ (Del (g,i))
proofend;

theorem Th4: :: MATRIXJ1:4
for i, n being Nat
for D being non empty set
for d being Element of D st i in Seg (n + 1) holds
Del (((n + 1) |-> d),i) = n |-> d
proofend;

theorem :: MATRIXJ1:5
for n being Nat
for K being Field
for a being Element of K holds Product (n |-> a) = (power K) . (a,n)
proofend;

definition
let f be FinSequence of NAT ;
let i be Nat;
assume B1: i in Seg (Sum f) ;
func min (f,i) ->  Element of NAT  means :Def1: :: MATRIXJ1:def 1
( i <= Sum (f | it) &amp; it in dom f &amp; ( for j being Nat st i <= Sum (f | j) holds
it <= j ) );
existence
 ex b1 being Element of NAT st
( i <= Sum (f | b1) &amp; b1 in dom f &amp; ( for j being Nat st i <= Sum (f | j) holds
b1 <= j ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st i <= Sum (f | b1) &amp; b1 in dom f &amp; ( for j being Nat st i <= Sum (f | j) holds
b1 <= j ) &amp; i <= Sum (f | b2) &amp; b2 in dom f &amp; ( for j being Nat st i <= Sum (f | j) holds
b2 <= j ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines min MATRIXJ1:def_1_:_
 for f being FinSequence of NAT
for i being Nat st i in Seg (Sum f) holds
for b3 being Element of NAT holds
( b3 = min (f,i) iff ( i <= Sum (f | b3) &amp; b3 in dom f &amp; ( for j being Nat st i <= Sum (f | j) holds
b3 <= j ) ) );

theorem :: MATRIXJ1:6
for i being Nat
for f being FinSequence of NAT st i in dom f &amp; f . i <> 0 holds
min (f,(Sum (f | i))) = i
proofend;

theorem Th7: :: MATRIXJ1:7
for i being Nat
for f being FinSequence of NAT st i in Seg (Sum f) holds
( (min (f,i)) -' 1 = (min (f,i)) - 1 &amp; Sum (f | ((min (f,i)) -' 1)) < i )
proofend;

theorem Th8: :: MATRIXJ1:8
for i being Nat
for f, g being FinSequence of NAT st i in Seg (Sum f) holds
min ((f ^ g),i) = min (f,i)
proofend;

theorem Th9: :: MATRIXJ1:9
for i being Nat
for f, g being FinSequence of NAT st i in (Seg ((Sum f) + (Sum g))) \ (Seg (Sum f)) holds
( min ((f ^ g),i) = (min (g,(i -' (Sum f)))) + (len f) &amp; i -' (Sum f) = i - (Sum f) )
proofend;

Lm2:  for i being Nat
for f being FinSequence of NAT st i in dom f holds
Sum (f | i) = (Sum (f | (i -' 1))) + (f . i)
proofend;

theorem Th10: :: MATRIXJ1:10
for i, j being Nat
for f being FinSequence of NAT st i in dom f &amp; j in Seg (f /. i) holds
( j + (Sum (f | (i -' 1))) in Seg (Sum (f | i)) &amp; min (f,(j + (Sum (f | (i -' 1))))) = i )
proofend;

theorem :: MATRIXJ1:11
for f being FinSequence of NAT
for i, j being Nat st i <= len f &amp; j <= len f &amp; Sum (f | i) = Sum (f | j) &amp; ( i in dom f implies f . i <> 0 ) &amp; ( j in dom f implies f . j <> 0 ) holds
i = j
proofend;

begin

definition
let D be non empty set ;
let F be FinSequence of (D *) * ;
attrF is Matrix-yielding  means :Def2: :: MATRIXJ1:def 2
 for i being Nat st i in dom F holds
F . i is Matrix of D;
end;

:: deftheorem Def2 defines Matrix-yielding MATRIXJ1:def_2_:_
 for D being non empty set
for F being FinSequence of (D *) * holds
( F is Matrix-yielding iff for i being Nat st i in dom F holds
F . i is Matrix of D );

registration
let D be non empty set ;
cluster Relation-like NAT -defined (D *) * -valued Function-like V33() FinSequence-like FinSubsequence-like Matrix-yielding for FinSequence of (D *) * ;
existence
 ex b1 being FinSequence of (D *) * st b1 is Matrix-yielding
proofend;
end;

definition
let D be non empty set ;
mode FinSequence_of_Matrix of D is Matrix-yielding FinSequence of (D *) * ;
end;

definition
let K be Field;
mode FinSequence_of_Matrix of K is Matrix-yielding FinSequence of ( the carrier of K *) * ;
end;

theorem Th12: :: MATRIXJ1:12
for D being non empty set holds {} is FinSequence_of_Matrix of D
proofend;

definition
let D be non empty set ;
let F be FinSequence_of_Matrix of D;
let x be set ;
:: original:.
redefine funcF . x ->  Matrix of D;
coherence
 F . x is Matrix of D
proofend;
end;

definition
let D be non empty set ;
let F1, F2 be FinSequence_of_Matrix of D;
:: original:^
redefine funcF1 ^ F2 ->  FinSequence_of_Matrix of D;
coherence
 F1 ^ F2 is FinSequence_of_Matrix of D
proofend;
end;

Lm3:  for D being non empty set
for M being Matrix of D holds <*M*> is Matrix-yielding
proofend;

definition
let D be non empty set ;
let M1 be Matrix of D;
:: original:<*
redefine func<*M1*> ->  FinSequence_of_Matrix of D;
coherence
 <*M1*> is FinSequence_of_Matrix of D by Lm3;
let M2 be Matrix of D;
:: original:<*
redefine func<*M1,M2*> ->  FinSequence_of_Matrix of D;
coherence
 <*M1,M2*> is FinSequence_of_Matrix of D
proofend;
end;

definition
let D be non empty set ;
let n be Nat;
let F be FinSequence_of_Matrix of D;
:: original:|
redefine funcF | n ->  FinSequence_of_Matrix of D;
coherence
 F | n is FinSequence_of_Matrix of D
proofend;
:: original:/^
redefine funcF /^ n ->  FinSequence_of_Matrix of D;
coherence
 F /^ n is FinSequence_of_Matrix of D
proofend;
end;

begin

definition
let D be non empty set ;
let F be FinSequence_of_Matrix of D;
func Len F ->  FinSequence of NAT  means :Def3: :: MATRIXJ1:def 3
( dom it = dom F &amp; ( for i being Nat st i in dom it holds
it . i = len (F . i) ) );
existence
 ex b1 being FinSequence of NAT st
( dom b1 = dom F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = len (F . i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of NAT st dom b1 = dom F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = len (F . i) ) &amp; dom b2 = dom F &amp; ( for i being Nat st i in dom b2 holds
b2 . i = len (F . i) ) holds
b1 = b2
proofend;
func Width F ->  FinSequence of NAT  means :Def4: :: MATRIXJ1:def 4
( dom it = dom F &amp; ( for i being Nat st i in dom it holds
it . i = width (F . i) ) );
existence
 ex b1 being FinSequence of NAT st
( dom b1 = dom F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = width (F . i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of NAT st dom b1 = dom F &amp; ( for i being Nat st i in dom b1 holds
b1 . i = width (F . i) ) &amp; dom b2 = dom F &amp; ( for i being Nat st i in dom b2 holds
b2 . i = width (F . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines Len MATRIXJ1:def_3_:_
 for D being non empty set
for F being FinSequence_of_Matrix of D
for b3 being FinSequence of NAT holds
( b3 = Len F iff ( dom b3 = dom F &amp; ( for i being Nat st i in dom b3 holds
b3 . i = len (F . i) ) ) );

:: deftheorem Def4 defines Width MATRIXJ1:def_4_:_
 for D being non empty set
for F being FinSequence_of_Matrix of D
for b3 being FinSequence of NAT holds
( b3 = Width F iff ( dom b3 = dom F &amp; ( for i being Nat st i in dom b3 holds
b3 . i = width (F . i) ) ) );

definition
let D be non empty set ;
let F be FinSequence_of_Matrix of D;
:: original:Len
redefine func Len F ->  Element of (len F) -tuples_on NAT;
coherence
 Len F is Element of (len F) -tuples_on NAT
proofend;
:: original:Width
redefine func Width F ->  Element of (len F) -tuples_on NAT;
coherence
 Width F is Element of (len F) -tuples_on NAT
proofend;
end;

theorem Th13: :: MATRIXJ1:13
for D being non empty set
for F being FinSequence_of_Matrix of D st Sum (Len F) = 0 holds
Sum (Width F) = 0
proofend;

theorem Th14: :: MATRIXJ1:14
for D being non empty set
for F1, F2 being FinSequence_of_Matrix of D holds Len (F1 ^ F2) = (Len F1) ^ (Len F2)
proofend;

theorem Th15: :: MATRIXJ1:15
for D being non empty set
for M being Matrix of D holds Len <*M*> = <*(len M)*>
proofend;

Lm4:  for D being non empty set
for M being Matrix of D holds Sum (Len <*M*>) = len M
proofend;

theorem Th16: :: MATRIXJ1:16
for D being non empty set
for M1, M2 being Matrix of D holds Sum (Len <*M1,M2*>) = (len M1) + (len M2)
proofend;

theorem Th17: :: MATRIXJ1:17
for n being Nat
for D being non empty set
for F1 being FinSequence_of_Matrix of D holds Len (F1 | n) = (Len F1) | n
proofend;

theorem Th18: :: MATRIXJ1:18
for D being non empty set
for F1, F2 being FinSequence_of_Matrix of D holds Width (F1 ^ F2) = (Width F1) ^ (Width F2)
proofend;

theorem Th19: :: MATRIXJ1:19
for D being non empty set
for M being Matrix of D holds Width <*M*> = <*(width M)*>
proofend;

Lm5:  for D being non empty set
for M being Matrix of D holds Sum (Width <*M*>) = width M
proofend;

theorem Th20: :: MATRIXJ1:20
for D being non empty set
for M1, M2 being Matrix of D holds Sum (Width <*M1,M2*>) = (width M1) + (width M2)
proofend;

theorem Th21: :: MATRIXJ1:21
for n being Nat
for D being non empty set
for F1 being FinSequence_of_Matrix of D holds Width (F1 | n) = (Width F1) | n
proofend;

begin

definition
let D be non empty set ;
let d be Element of D;
let F be FinSequence_of_Matrix of D;
func block_diagonal (F,d) ->  Matrix of D means :Def5: :: MATRIXJ1:def 5
( len it = Sum (Len F) &amp; width it = Sum (Width F) &amp; ( for i, j being Nat 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 ) &amp; ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j &amp; 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
 ex b1 being Matrix of D st
( len b1 = Sum (Len F) &amp; width b1 = Sum (Width F) &amp; ( for i, j being Nat st [i,j] in Indices b1 holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b1 * (i,j) = d ) &amp; ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j &amp; j <= Sum ((Width F) | (min ((Len F),i))) implies b1 * (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))))) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Matrix of D st len b1 = Sum (Len F) &amp; width b1 = Sum (Width F) &amp; ( for i, j being Nat st [i,j] in Indices b1 holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b1 * (i,j) = d ) &amp; ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j &amp; j <= Sum ((Width F) | (min ((Len F),i))) implies b1 * (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))))) ) ) ) &amp; len b2 = Sum (Len F) &amp; width b2 = Sum (Width F) &amp; ( for i, j being Nat st [i,j] in Indices b2 holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b2 * (i,j) = d ) &amp; ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j &amp; j <= Sum ((Width F) | (min ((Len F),i))) implies b2 * (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))))) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines block_diagonal MATRIXJ1:def_5_:_
 for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D
for b4 being Matrix of D holds
( b4 = block_diagonal (F,d) iff ( len b4 = Sum (Len F) &amp; width b4 = Sum (Width F) &amp; ( for i, j being Nat st [i,j] in Indices b4 holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b4 * (i,j) = d ) &amp; ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j &amp; j <= Sum ((Width F) | (min ((Len F),i))) implies b4 * (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))))) ) ) ) ) );

definition
let D be non empty set ;
let d be Element of D;
let F be FinSequence_of_Matrix of D;
:: original:block_diagonal
redefine func block_diagonal (F,d) ->  Matrix of Sum (Len F), Sum (Width F),D;
coherence
 block_diagonal (F,d) is Matrix of Sum (Len F), Sum (Width F),D
proofend;
end;

theorem :: MATRIXJ1:22
for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D st F = {} holds
block_diagonal (F,d) = {}
proofend;

theorem Th23: :: MATRIXJ1:23
for D being non empty set
for d being Element of D
for M1, M2 being Matrix of D
for M being Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D holds
( M = block_diagonal (<*M1,M2*>,d) iff for i being Nat holds
( ( i in dom M1 implies Line (M,i) = (Line (M1,i)) ^ ((width M2) |-> d) ) &amp; ( i in dom M2 implies Line (M,(i + (len M1))) = ((width M1) |-> d) ^ (Line (M2,i)) ) ) )
proofend;

theorem Th24: :: MATRIXJ1:24
for D being non empty set
for d being Element of D
for M1, M2 being Matrix of D
for M being Matrix of Sum (Len <*M1,M2*>), Sum (Width <*M1,M2*>),D holds
( M = block_diagonal (<*M1,M2*>,d) iff for i being Nat holds
( ( i in Seg (width M1) implies Col (M,i) = (Col (M1,i)) ^ ((len M2) |-> d) ) &amp; ( i in Seg (width M2) implies Col (M,(i + (width M1))) = ((len M1) |-> d) ^ (Col (M2,i)) ) ) )
proofend;

theorem Th25: :: MATRIXJ1:25
for D being non empty set
for d1, d2 being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds Indices (block_diagonal (F1,d1)) is Subset of (Indices (block_diagonal ((F1 ^ F2),d2)))
proofend;

theorem Th26: :: MATRIXJ1:26
for i, j being Nat
for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal (F1,d)) holds
(block_diagonal (F1,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * (i,j)
proofend;

theorem Th27: :: MATRIXJ1:27
for i, j being Nat
for D being non empty set
for d1, d2 being Element of D
for F2, F1 being FinSequence_of_Matrix of D holds
( [i,j] in Indices (block_diagonal (F2,d1)) iff ( i > 0 &amp; j > 0 &amp; [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal ((F1 ^ F2),d2)) ) )
proofend;

theorem Th28: :: MATRIXJ1:28
for i, j being Nat
for D being non empty set
for d being Element of D
for F2, F1 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal (F2,d)) holds
(block_diagonal (F2,d)) * (i,j) = (block_diagonal ((F1 ^ F2),d)) * ((i + (Sum (Len F1))),(j + (Sum (Width F1))))
proofend;

theorem Th29: :: MATRIXJ1:29
for i, j being Nat
for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D st [i,j] in Indices (block_diagonal ((F1 ^ F2),d)) &amp; ( ( i <= Sum (Len F1) &amp; j > Sum (Width F1) ) or ( i > Sum (Len F1) &amp; j <= Sum (Width F1) ) ) holds
(block_diagonal ((F1 ^ F2),d)) * (i,j) = d
proofend;

theorem Th30: :: MATRIXJ1:30
for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D
for i, j, k being Nat st i in dom F &amp; [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)) &amp; (F . i) * (j,k) = (block_diagonal (F,d)) * ((j + (Sum ((Len F) | (i -' 1)))),(k + (Sum ((Width F) | (i -' 1))))) )
proofend;

theorem Th31: :: MATRIXJ1:31
for i being Nat
for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D st i in dom F holds
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))))))
proofend;

theorem Th32: :: MATRIXJ1:32
for D being non empty set
for d being Element of D
for M being Matrix of D
for F being FinSequence_of_Matrix of D holds M = Segm ((block_diagonal ((<*M*> ^ F),d)),(Seg (len M)),(Seg (width M)))
proofend;

theorem Th33: :: MATRIXJ1:33
for D being non empty set
for d being Element of D
for M being Matrix of D
for F being FinSequence_of_Matrix of D holds 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)))))
proofend;

theorem Th34: :: MATRIXJ1:34
for D being non empty set
for d being Element of D
for M being Matrix of D holds block_diagonal (<*M*>,d) = M
proofend;

theorem Th35: :: MATRIXJ1:35
for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds block_diagonal ((F1 ^ F2),d) = block_diagonal ((<*(block_diagonal (F1,d))*> ^ F2),d)
proofend;

theorem Th36: :: MATRIXJ1:36
for D being non empty set
for d being Element of D
for F1, F2 being FinSequence_of_Matrix of D holds block_diagonal ((F1 ^ F2),d) = block_diagonal ((F1 ^ <*(block_diagonal (F2,d))*>),d)
proofend;

theorem :: MATRIXJ1:37
for i, m being Nat
for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D st i in Seg (Sum (Len F)) &amp; m = min ((Len F),i) holds
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)
proofend;

theorem :: MATRIXJ1:38
for i, m being Nat
for D being non empty set
for d being Element of D
for F being FinSequence_of_Matrix of D st i in Seg (Sum (Width F)) &amp; m = min ((Width F),i) holds
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)
proofend;

theorem :: MATRIXJ1:39
for D being non empty set
for d1, d2 being Element of D
for M1, M2, N1, N2 being Matrix of D st len M1 = len N1 &amp; width M1 = width N1 &amp; len M2 = len N2 &amp; width M2 = width N2 &amp; block_diagonal (<*M1,M2*>,d1) = block_diagonal (<*N1,N2*>,d2) holds
( M1 = N1 &amp; M2 = N2 )
proofend;

theorem Th40: :: MATRIXJ1:40
for D being non empty set
for d being Element of D
for M being Matrix of D
for F being FinSequence_of_Matrix of D st M = {} holds
( block_diagonal ((F ^ <*M*>),d) = block_diagonal (F,d) &amp; block_diagonal ((<*M*> ^ F),d) = block_diagonal (F,d) )
proofend;

theorem Th41: :: MATRIXJ1:41
for i being Nat
for K being Field
for a being Element of K
for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in dom A &amp; width A = width (DelLine (A,i)) holds
DelLine ((block_diagonal ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelLine (A,i))*> ^ G),a)
proofend;

theorem Th42: :: MATRIXJ1:42
for i being Nat
for K being Field
for a being Element of K
for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in dom A &amp; width A = width (DelLine (A,i)) holds
DelLine ((block_diagonal ((G ^ <*A*>),a)),((Sum (Len G)) + i)) = block_diagonal ((G ^ <*(DelLine (A,i))*>),a)
proofend;

theorem Th43: :: MATRIXJ1:43
for i being Nat
for K being Field
for a being Element of K
for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in Seg (width A) holds
DelCol ((block_diagonal ((<*A*> ^ G),a)),i) = block_diagonal ((<*(DelCol (A,i))*> ^ G),a)
proofend;

theorem Th44: :: MATRIXJ1:44
for i being Nat
for K being Field
for a being Element of K
for A being Matrix of K
for G being FinSequence_of_Matrix of K st i in Seg (width A) holds
DelCol ((block_diagonal ((G ^ <*A*>),a)),(i + (Sum (Width G)))) = block_diagonal ((G ^ <*(DelCol (A,i))*>),a)
proofend;

definition
let D be non empty set ;
let F be FinSequence of (D *) * ;
attrF is Square-Matrix-yielding  means :Def6: :: MATRIXJ1:def 6
 for i being Nat st i in dom F holds
ex n being Nat st F . i is Matrix of n,D;
end;

:: deftheorem Def6 defines Square-Matrix-yielding MATRIXJ1:def_6_:_
 for D being non empty set
for F being FinSequence of (D *) * holds
( F is Square-Matrix-yielding iff for i being Nat st i in dom F holds
ex n being Nat st F . i is Matrix of n,D );

registration
let D be non empty set ;
cluster Relation-like NAT -defined (D *) * -valued Function-like V33() FinSequence-like FinSubsequence-like Square-Matrix-yielding for FinSequence of (D *) * ;
existence
 ex b1 being FinSequence of (D *) * st b1 is Square-Matrix-yielding
proofend;
end;

registration
let D be non empty set ;
cluster Square-Matrix-yielding  ->  Matrix-yielding for FinSequence of (D *) * ;
coherence
 for b1 being FinSequence of (D *) * st b1 is Square-Matrix-yielding holds
b1 is Matrix-yielding
proofend;
end;

definition
let D be non empty set ;
mode FinSequence_of_Square-Matrix of D is Square-Matrix-yielding FinSequence of (D *) * ;
end;

definition
let K be Field;
mode FinSequence_of_Square-Matrix of K is Square-Matrix-yielding FinSequence of ( the carrier of K *) * ;
end;

theorem :: MATRIXJ1:45
for D being non empty set holds {} is FinSequence_of_Square-Matrix of D
proofend;

definition
let D be non empty set ;
let S be FinSequence_of_Square-Matrix of D;
let x be set ;
:: original:.
redefine funcS . x ->  Matrix of len (S . x),D;
coherence
 S . x is Matrix of len (S . x),D
proofend;
end;

definition
let D be non empty set ;
let S1, S2 be FinSequence_of_Square-Matrix of D;
:: original:^
redefine funcS1 ^ S2 ->  FinSequence_of_Square-Matrix of D;
coherence
 S1 ^ S2 is FinSequence_of_Square-Matrix of D
proofend;
end;

Lm6:  for n being Nat
for D being non empty set
for M being Matrix of n,D holds <*M*> is FinSequence_of_Square-Matrix of D
proofend;

definition
let D be non empty set ;
let n be Nat;
let M1 be Matrix of n,D;
:: original:<*
redefine func<*M1*> ->  FinSequence_of_Square-Matrix of D;
coherence
 <*M1*> is FinSequence_of_Square-Matrix of D by Lm6;
end;

definition
let D be non empty set ;
let n, m be Nat;
let M1 be Matrix of n,D;
let M2 be Matrix of m,D;
:: original:<*
redefine func<*M1,M2*> ->  FinSequence_of_Square-Matrix of D;
coherence
 <*M1,M2*> is FinSequence_of_Square-Matrix of D
proofend;
end;

definition
let D be non empty set ;
let n be Nat;
let S be FinSequence_of_Square-Matrix of D;
:: original:|
redefine funcS | n ->  FinSequence_of_Square-Matrix of D;
coherence
 S | n is FinSequence_of_Square-Matrix of D
proofend;
:: original:/^
redefine funcS /^ n ->  FinSequence_of_Square-Matrix of D;
coherence
 S /^ n is FinSequence_of_Square-Matrix of D
proofend;
end;

theorem Th46: :: MATRIXJ1:46
for D being non empty set
for S being FinSequence_of_Square-Matrix of D holds Len S = Width S
proofend;

definition
let D be non empty set ;
let d be Element of D;
let S be FinSequence_of_Square-Matrix of D;
:: original:block_diagonal
redefine func block_diagonal (S,d) ->  Matrix of Sum (Len S),D;
coherence
 block_diagonal (S,d) is Matrix of Sum (Len S),D
proofend;
end;

theorem Th47: :: MATRIXJ1:47
for n, i, j being Nat
for K being Field
for a being Element of K
for R being FinSequence_of_Square-Matrix of K
for A being Matrix of n,K st i in dom A &amp; j in Seg n holds
Deleting ((block_diagonal ((<*A*> ^ R),a)),i,j) = block_diagonal ((<*(Deleting (A,i,j))*> ^ R),a)
proofend;

theorem :: MATRIXJ1:48
for n, i, j being Nat
for K being Field
for a being Element of K
for R being FinSequence_of_Square-Matrix of K
for A being Matrix of n,K st i in dom A &amp; 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)
proofend;

definition
let K be Field;
let R be FinSequence_of_Square-Matrix of K;
func Det R ->  FinSequence of K means :Def7: :: MATRIXJ1:def 7
( dom it = dom R &amp; ( for i being Nat st i in dom it holds
it . i = Det (R . i) ) );
existence
 ex b1 being FinSequence of K st
( dom b1 = dom R &amp; ( for i being Nat st i in dom b1 holds
b1 . i = Det (R . i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of K st dom b1 = dom R &amp; ( for i being Nat st i in dom b1 holds
b1 . i = Det (R . i) ) &amp; dom b2 = dom R &amp; ( for i being Nat st i in dom b2 holds
b2 . i = Det (R . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines Det MATRIXJ1:def_7_:_
 for K being Field
for R being FinSequence_of_Square-Matrix of K
for b3 being FinSequence of K holds
( b3 = Det R iff ( dom b3 = dom R &amp; ( for i being Nat st i in dom b3 holds
b3 . i = Det (R . i) ) ) );

definition
let K be Field;
let R be FinSequence_of_Square-Matrix of K;
:: original:Det
redefine func Det R ->  Element of (len R) -tuples_on the carrier of K;
coherence
 Det R is Element of (len R) -tuples_on the carrier of K
proofend;
end;

theorem Th49: :: MATRIXJ1:49
for n being Nat
for K being Field
for N being Matrix of n,K holds Det <*N*> = <*(Det N)*>
proofend;

theorem Th50: :: MATRIXJ1:50
for K being Field
for R1, R2 being FinSequence_of_Square-Matrix of K holds Det (R1 ^ R2) = (Det R1) ^ (Det R2)
proofend;

theorem :: MATRIXJ1:51
for n being Nat
for K being Field
for R being FinSequence_of_Square-Matrix of K holds Det (R | n) = (Det R) | n
proofend;

theorem Th52: :: MATRIXJ1:52
for n, m being Nat
for K being Field
for N being Matrix of n,K
for N1 being Matrix of m,K holds Det (block_diagonal (<*N,N1*>,(0. K))) = (Det N) * (Det N1)
proofend;

theorem :: MATRIXJ1:53
for K being Field
for R being FinSequence_of_Square-Matrix of K holds Det (block_diagonal (R,(0. K))) = Product (Det R)
proofend;

theorem Th54: :: MATRIXJ1:54
for n being Nat
for K being Field
for A1, A2 being Matrix of K
for N being Matrix of n,K st len A1 <> width A1 &amp; N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K
proofend;

theorem :: MATRIXJ1:55
for n being Nat
for K being Field
for G being FinSequence_of_Matrix of K st Len G <> Width G holds
for M being Matrix of n,K st M = block_diagonal (G,(0. K)) holds
Det M = 0. K
proofend;

begin

definition
let K be Field;
let f be FinSequence of NAT ;
func 1. (K,f) ->  FinSequence_of_Square-Matrix of K means :Def8: :: MATRIXJ1:def 8
( dom it = dom f &amp; ( for i being Nat st i in dom it holds
it . i = 1. (K,(f . i)) ) );
existence
 ex b1 being FinSequence_of_Square-Matrix of K st
( dom b1 = dom f &amp; ( for i being Nat st i in dom b1 holds
b1 . i = 1. (K,(f . i)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence_of_Square-Matrix of K st dom b1 = dom f &amp; ( for i being Nat st i in dom b1 holds
b1 . i = 1. (K,(f . i)) ) &amp; dom b2 = dom f &amp; ( for i being Nat st i in dom b2 holds
b2 . i = 1. (K,(f . i)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines 1. MATRIXJ1:def_8_:_
 for K being Field
for f being FinSequence of NAT
for b3 being FinSequence_of_Square-Matrix of K holds
( b3 = 1. (K,f) iff ( dom b3 = dom f &amp; ( for i being Nat st i in dom b3 holds
b3 . i = 1. (K,(f . i)) ) ) );

theorem :: MATRIXJ1:56
for K being Field
for f being FinSequence of NAT holds
( Len (1. (K,f)) = f &amp; Width (1. (K,f)) = f )
proofend;

theorem Th57: :: MATRIXJ1:57
for K being Field
for i being Element of NAT holds 1. (K,<*i*>) = <*(1. (K,i))*>
proofend;

theorem Th58: :: MATRIXJ1:58
for K being Field
for f, g being FinSequence of NAT holds 1. (K,(f ^ g)) = (1. (K,f)) ^ (1. (K,g))
proofend;

theorem :: MATRIXJ1:59
for n being Nat
for K being Field
for f being FinSequence of NAT holds 1. (K,(f | n)) = (1. (K,f)) | n
proofend;

theorem Th60: :: MATRIXJ1:60
for i, j being Nat
for K being Field holds block_diagonal (<*(1. (K,i)),(1. (K,j))*>,(0. K)) = 1. (K,(i + j))
proofend;

theorem :: MATRIXJ1:61
for K being Field
for f being FinSequence of NAT holds block_diagonal ((1. (K,f)),(0. K)) = 1. (K,(Sum f))
proofend;

begin

definition
let K be Field;
let G be FinSequence_of_Matrix of K;
let p be FinSequence of K;
func mlt (p,G) ->  FinSequence_of_Matrix of K means :Def9: :: MATRIXJ1:def 9
( dom it = dom G &amp; ( for i being Nat st i in dom it holds
it . i = (p /. i) * (G . i) ) );
existence
 ex b1 being FinSequence_of_Matrix of K st
( dom b1 = dom G &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (p /. i) * (G . i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence_of_Matrix of K st dom b1 = dom G &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (p /. i) * (G . i) ) &amp; dom b2 = dom G &amp; ( for i being Nat st i in dom b2 holds
b2 . i = (p /. i) * (G . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines mlt MATRIXJ1:def_9_:_
 for K being Field
for G being FinSequence_of_Matrix of K
for p being FinSequence of K
for b4 being FinSequence_of_Matrix of K holds
( b4 = mlt (p,G) iff ( dom b4 = dom G &amp; ( for i being Nat st i in dom b4 holds
b4 . i = (p /. i) * (G . i) ) ) );

registration
let K be Field;
let R be FinSequence_of_Square-Matrix of K;
let p be FinSequence of K;
cluster mlt (p,R) ->  Square-Matrix-yielding ;
coherence
 mlt (p,R) is Square-Matrix-yielding
proofend;
end;

theorem :: MATRIXJ1:62
for K being Field
for G being FinSequence_of_Matrix of K
for p being FinSequence of K holds
( Len (mlt (p,G)) = Len G &amp; Width (mlt (p,G)) = Width G )
proofend;

theorem Th63: :: MATRIXJ1:63
for K being Field
for A being Matrix of K
for p being FinSequence of K holds mlt (p,<*A*>) = <*((p /. 1) * A)*>
proofend;

theorem Th64: :: MATRIXJ1:64
for K being Field
for G, G1 being FinSequence_of_Matrix of K
for p, p1 being FinSequence of K st len G = len p &amp; len G1 <= len p1 holds
mlt ((p ^ p1),(G ^ G1)) = (mlt (p,G)) ^ (mlt (p1,G1))
proofend;

Lm7:  for K being Field
for a, a1 being Element of K
for A1, A2 being Matrix of K holds a * (block_diagonal (<*A1,A2*>,a1)) = block_diagonal (<*(a * A1),(a * A2)*>,(a * a1))
proofend;

theorem :: MATRIXJ1:65
for K being Field
for a, a1 being Element of K
for G being FinSequence_of_Matrix of K holds a * (block_diagonal (G,a1)) = block_diagonal ((mlt (((len G) |-> a),G)),(a * a1))
proofend;

definition
let K be Field;
let G1, G2 be FinSequence_of_Matrix of K;
funcG1 (+) G2 ->  FinSequence_of_Matrix of K means :Def10: :: MATRIXJ1:def 10
( dom it = dom G1 &amp; ( for i being Nat st i in dom it holds
it . i = (G1 . i) + (G2 . i) ) );
existence
 ex b1 being FinSequence_of_Matrix of K st
( dom b1 = dom G1 &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (G1 . i) + (G2 . i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence_of_Matrix of K st dom b1 = dom G1 &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (G1 . i) + (G2 . i) ) &amp; dom b2 = dom G1 &amp; ( for i being Nat st i in dom b2 holds
b2 . i = (G1 . i) + (G2 . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines (+) MATRIXJ1:def_10_:_
 for K being Field
for G1, G2, b4 being FinSequence_of_Matrix of K holds
( b4 = G1 (+) G2 iff ( dom b4 = dom G1 &amp; ( for i being Nat st i in dom b4 holds
b4 . i = (G1 . i) + (G2 . i) ) ) );

registration
let K be Field;
let R be FinSequence_of_Square-Matrix of K;
let G be FinSequence_of_Matrix of K;
clusterR (+) G ->  Square-Matrix-yielding ;
coherence
 R (+) G is Square-Matrix-yielding
proofend;
end;

theorem Th66: :: MATRIXJ1:66
for K being Field
for G1, G2 being FinSequence_of_Matrix of K holds
( Len (G1 (+) G2) = Len G1 &amp; Width (G1 (+) G2) = Width G1 )
proofend;

theorem Th67: :: MATRIXJ1:67
for K being Field
for G, G9, G1, G2 being FinSequence_of_Matrix of K st len G = len G9 holds
(G ^ G1) (+) (G9 ^ G2) = (G (+) G9) ^ (G1 (+) G2)
proofend;

theorem Th68: :: MATRIXJ1:68
for K being Field
for A being Matrix of K
for G being FinSequence_of_Matrix of K holds <*A*> (+) G = <*(A + (G . 1))*>
proofend;

theorem Th69: :: MATRIXJ1:69
for K being Field
for A1, A2 being Matrix of K holds <*A1*> (+) <*A2*> = <*(A1 + A2)*>
proofend;

theorem Th70: :: MATRIXJ1:70
for K being Field
for A1, B1, A2, B2 being Matrix of K holds <*A1,B1*> (+) <*A2,B2*> = <*(A1 + A2),(B1 + B2)*>
proofend;

Lm8:  for i being Nat
for K being Field
for A1, A2 being Matrix of K st width A1 = width A2 &amp; i in dom A1 holds
Line ((A1 + A2),i) = (Line (A1,i)) + (Line (A2,i))
proofend;

theorem Th71: :: MATRIXJ1:71
for K being Field
for a1, a2 being Element of K
for A1, B1, A2, B2 being Matrix of K st len A1 = len B1 &amp; len A2 = len B2 &amp; width A1 = width B1 &amp; width A2 = width B2 holds
(block_diagonal (<*A1,A2*>,a1)) + (block_diagonal (<*B1,B2*>,a2)) = block_diagonal ((<*A1,A2*> (+) <*B1,B2*>),(a1 + a2))
proofend;

theorem :: MATRIXJ1:72
for K being Field
for a1, a2 being Element of K
for R1, R2 being FinSequence_of_Square-Matrix of K st Len R1 = Len R2 &amp; Width R1 = Width R2 holds
(block_diagonal (R1,a1)) + (block_diagonal (R2,a2)) = block_diagonal ((R1 (+) R2),(a1 + a2))
proofend;

definition
let K be Field;
let G1, G2 be FinSequence_of_Matrix of K;
funcG1 (#) G2 ->  FinSequence_of_Matrix of K means :Def11: :: MATRIXJ1:def 11
( dom it = dom G1 &amp; ( for i being Nat st i in dom it holds
it . i = (G1 . i) * (G2 . i) ) );
existence
 ex b1 being FinSequence_of_Matrix of K st
( dom b1 = dom G1 &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (G1 . i) * (G2 . i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence_of_Matrix of K st dom b1 = dom G1 &amp; ( for i being Nat st i in dom b1 holds
b1 . i = (G1 . i) * (G2 . i) ) &amp; dom b2 = dom G1 &amp; ( for i being Nat st i in dom b2 holds
b2 . i = (G1 . i) * (G2 . i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines (#) MATRIXJ1:def_11_:_
 for K being Field
for G1, G2, b4 being FinSequence_of_Matrix of K holds
( b4 = G1 (#) G2 iff ( dom b4 = dom G1 &amp; ( for i being Nat st i in dom b4 holds
b4 . i = (G1 . i) * (G2 . i) ) ) );

theorem Th73: :: MATRIXJ1:73
for K being Field
for G1, G2 being FinSequence_of_Matrix of K st Width G1 = Len G2 holds
( Len (G1 (#) G2) = Len G1 &amp; Width (G1 (#) G2) = Width G2 )
proofend;

theorem Th74: :: MATRIXJ1:74
for K being Field
for G, G9, G1, G2 being FinSequence_of_Matrix of K st len G = len G9 holds
(G ^ G1) (#) (G9 ^ G2) = (G (#) G9) ^ (G1 (#) G2)
proofend;

theorem Th75: :: MATRIXJ1:75
for K being Field
for A being Matrix of K
for G being FinSequence_of_Matrix of K holds <*A*> (#) G = <*(A * (G . 1))*>
proofend;

theorem Th76: :: MATRIXJ1:76
for K being Field
for A1, A2 being Matrix of K holds <*A1*> (#) <*A2*> = <*(A1 * A2)*>
proofend;

theorem Th77: :: MATRIXJ1:77
for K being Field
for A1, B1, A2, B2 being Matrix of K holds <*A1,B1*> (#) <*A2,B2*> = <*(A1 * A2),(B1 * B2)*>
proofend;

Lm9:  for i, j being Nat
for K being Field
for R1, S1 being Element of i -tuples_on the carrier of K
for R2, S2 being Element of j -tuples_on the carrier of K holds Sum (mlt ((R1 ^ R2),(S1 ^ S2))) = (Sum (mlt (R1,S1))) + (Sum (mlt (R2,S2)))
proofend;

theorem Th78: :: MATRIXJ1:78
for K being Field
for A1, B1, A2, B2 being Matrix of K st width A1 = len B1 &amp; width A2 = len B2 holds
(block_diagonal (<*A1,A2*>,(0. K))) * (block_diagonal (<*B1,B2*>,(0. K))) = block_diagonal ((<*A1,A2*> (#) <*B1,B2*>),(0. K))
proofend;

theorem :: MATRIXJ1:79
for K being Field
for R1, R2 being FinSequence_of_Square-Matrix of K st Width R1 = Len R2 holds
(block_diagonal (R1,(0. K))) * (block_diagonal (R2,(0. K))) = block_diagonal ((R1 (#) R2),(0. K))
proofend;