:: Block Diagonal Matrices
:: by Karol P\c{a}k
::
:: Received May 13, 2008
:: Copyright (c) 2008 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)
proof end;

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)
proof end;

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
proof end;

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)
proof end;

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
proof end;

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
proof end;

definition
let f be FinSequence of NAT ;
let i be Nat;
assume A1: i in Seg (Sum f) ;
func min f,i -> Element of NAT means :Def1: :: MATRIXJ1:def 1
( i <= Sum (f | it) & it in dom f & ( for j being Nat st i <= Sum (f | j) holds
it <= j ) );
existence
ex b1 being Element of NAT st
( i <= Sum (f | b1) & b1 in dom f & ( for j being Nat st i <= Sum (f | j) holds
b1 <= j ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st i <= Sum (f | b1) & b1 in dom f & ( for j being Nat st i <= Sum (f | j) holds
b1 <= j ) & i <= Sum (f | b2) & b2 in dom f & ( for j being Nat st i <= Sum (f | j) holds
b2 <= j ) holds
b1 = b2
proof end;
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) & b3 in dom f & ( 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 & f . i <> 0 holds
min f,(Sum (f | i)) = i
proof end;

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 & Sum (f | ((min f,i) -' 1)) < i )
proof end;

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
proof end;

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) & i -' (Sum f) = i - (Sum f) )
proof end;

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)
proof end;

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

theorem :: MATRIXJ1:11
for f being FinSequence of NAT
for i, j being Nat 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 end;

begin

definition
let D be non empty set ;
let F be FinSequence of (D * ) * ;
attr F 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 Matrix-yielding FinSequence of (D * ) * ;
existence
ex b1 being FinSequence of (D * ) * st b1 is Matrix-yielding
proof end;
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
proof end;

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

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

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

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
proof end;
end;

definition
let D be non empty set ;
let F be FinSequence_of_Matrix of D;
let n be Nat;
:: original: |
redefine func F | n -> FinSequence_of_Matrix of D;
coherence
F | n is FinSequence_of_Matrix of D
proof end;
:: original: /^
redefine func F /^ n -> FinSequence_of_Matrix of D;
coherence
F /^ n is FinSequence_of_Matrix of D
proof end;
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 & ( 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 & ( for i being Nat st i in dom b1 holds
b1 . i = len (F . i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st dom b1 = dom F & ( for i being Nat st i in dom b1 holds
b1 . i = len (F . i) ) & dom b2 = dom F & ( for i being Nat st i in dom b2 holds
b2 . i = len (F . i) ) holds
b1 = b2
proof end;
func Width F -> FinSequence of NAT means :Def4: :: MATRIXJ1:def 4
( dom it = dom F & ( 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 & ( for i being Nat st i in dom b1 holds
b1 . i = width (F . i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st dom b1 = dom F & ( for i being Nat st i in dom b1 holds
b1 . i = width (F . i) ) & dom b2 = dom F & ( for i being Nat st i in dom b2 holds
b2 . i = width (F . i) ) holds
b1 = b2
proof end;
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 & ( 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 & ( 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
proof end;
:: original: Width
redefine func Width F -> Element of (len F) -tuples_on NAT ;
coherence
Width F is Element of (len F) -tuples_on NAT
proof end;
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
proof end;

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)
proof end;

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

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

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)
proof end;

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
proof end;

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)
proof end;

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

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

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)
proof end;

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
proof end;

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) & width it = Sum (Width F) & ( 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 ) & ( 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
ex b1 being Matrix of D st
( len b1 = Sum (Len F) & width b1 = Sum (Width F) & ( 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 ) & ( Sum ((Width F) | ((min (Len F),i) -' 1)) < j & 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)))) ) ) ) )
proof end;
uniqueness
for b1, b2 being Matrix of D st len b1 = Sum (Len F) & width b1 = Sum (Width F) & ( 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 ) & ( Sum ((Width F) | ((min (Len F),i) -' 1)) < j & 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)))) ) ) ) & len b2 = Sum (Len F) & width b2 = Sum (Width F) & ( 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 ) & ( Sum ((Width F) | ((min (Len F),i) -' 1)) < j & 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
proof end;
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) & width b4 = Sum (Width F) & ( 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 ) & ( Sum ((Width F) | ((min (Len F),i) -' 1)) < j & 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
proof end;
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 = {}
proof end;

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) ) & ( i in dom M2 implies Line M,(i + (len M1)) = ((width M1) |-> d) ^ (Line M2,i) ) ) )
proof end;

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) ) & ( i in Seg (width M2) implies Col M,(i + (width M1)) = ((len M1) |-> d) ^ (Col M2,i) ) ) )
proof end;

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))
proof end;

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
proof end;

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 & j > 0 & [(i + (Sum (Len F1))),(j + (Sum (Width F1)))] in Indices (block_diagonal (F1 ^ F2),d2) ) )
proof end;

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)))
proof end;

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) & ( ( i <= Sum (Len F1) & j > Sum (Width F1) ) or ( i > Sum (Len F1) & j <= Sum (Width F1) ) ) holds
(block_diagonal (F1 ^ F2),d) * i,j = d
proof end;

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 & [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 end;

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)))))
proof end;

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))
proof end;

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))))
proof end;

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
proof end;

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
proof end;

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
proof end;

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)) & 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)
proof end;

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)) & 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)
proof end;

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 & 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 end;

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 & block_diagonal (<*M*> ^ F),d = block_diagonal F,d )
proof end;

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 & width A = width (DelLine A,i) holds
DelLine (block_diagonal (<*A*> ^ G),a),i = block_diagonal (<*(DelLine A,i)*> ^ G),a
proof end;

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 & width A = width (DelLine A,i) holds
DelLine (block_diagonal (G ^ <*A*>),a),((Sum (Len G)) + i) = block_diagonal (G ^ <*(DelLine A,i)*>),a
proof end;

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
proof end;

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
proof end;

definition
let D be non empty set ;
let F be FinSequence of (D * ) * ;
attr F 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 Square-Matrix-yielding FinSequence of (D * ) * ;
existence
ex b1 being FinSequence of (D * ) * st b1 is Square-Matrix-yielding
proof end;
end;

registration
let D be non empty set ;
cluster Square-Matrix-yielding -> Matrix-yielding FinSequence of (D * ) * ;
coherence
for b1 being FinSequence of (D * ) * st b1 is Square-Matrix-yielding holds
b1 is Matrix-yielding
proof end;
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
proof end;

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

definition
let D be non empty set ;
let S1, S2 be FinSequence_of_Square-Matrix of D;
:: original: ^
redefine func S1 ^ S2 -> FinSequence_of_Square-Matrix of D;
coherence
S1 ^ S2 is FinSequence_of_Square-Matrix of D
proof end;
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
proof end;

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
proof end;
end;

definition
let D be non empty set ;
let S be FinSequence_of_Square-Matrix of D;
let n be Nat;
:: original: |
redefine func S | n -> FinSequence_of_Square-Matrix of D;
coherence
S | n is FinSequence_of_Square-Matrix of D
proof end;
:: original: /^
redefine func S /^ n -> FinSequence_of_Square-Matrix of D;
coherence
S /^ n is FinSequence_of_Square-Matrix of D
proof end;
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
proof end;

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
proof end;
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 & j in Seg n holds
Deleting (block_diagonal (<*A*> ^ R),a),i,j = block_diagonal (<*(Deleting A,i,j)*> ^ R),a
proof end;

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 & 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 end;

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 & ( 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 & ( for i being Nat st i in dom b1 holds
b1 . i = Det (R . i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of K st dom b1 = dom R & ( for i being Nat st i in dom b1 holds
b1 . i = Det (R . i) ) & dom b2 = dom R & ( for i being Nat st i in dom b2 holds
b2 . i = Det (R . i) ) holds
b1 = b2
proof end;
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 & ( 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
proof end;
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)*>
proof end;

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)
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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 & N = block_diagonal <*A1,A2*>,(0. K) holds
Det N = 0. K
proof end;

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
proof end;

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 & ( 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 & ( for i being Nat st i in dom b1 holds
b1 . i = 1. K,(f . i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence_of_Square-Matrix of K st dom b1 = dom f & ( for i being Nat st i in dom b1 holds
b1 . i = 1. K,(f . i) ) & dom b2 = dom f & ( for i being Nat st i in dom b2 holds
b2 . i = 1. K,(f . i) ) holds
b1 = b2
proof end;
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 & ( 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 & Width (1. K,f) = f )
proof end;

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

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)
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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 & ( 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 & ( for i being Nat st i in dom b1 holds
b1 . i = (p /. i) * (G . i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence_of_Matrix of K st dom b1 = dom G & ( for i being Nat st i in dom b1 holds
b1 . i = (p /. i) * (G . i) ) & dom b2 = dom G & ( for i being Nat st i in dom b2 holds
b2 . i = (p /. i) * (G . i) ) holds
b1 = b2
proof end;
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 & ( for i being Nat st i in dom b4 holds
b4 . i = (p /. i) * (G . i) ) ) );

definition
let K be Field;
let R be FinSequence_of_Square-Matrix of K;
let p be FinSequence of K;
:: original: mlt
redefine func mlt p,R -> FinSequence_of_Square-Matrix of K;
coherence
mlt p,R is FinSequence_of_Square-Matrix of K
proof end;
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 & Width (mlt p,G) = Width G )
proof end;

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)*>
proof end;

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 & len G1 <= len p1 holds
mlt (p ^ p1),(G ^ G1) = (mlt p,G) ^ (mlt p1,G1)
proof end;

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)
proof end;

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)
proof end;

definition
let K be Field;
let G1, G2 be FinSequence_of_Matrix of K;
func G1 (+) G2 -> FinSequence_of_Matrix of K means :Def10: :: MATRIXJ1:def 10
( dom it = dom G1 & ( 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 & ( for i being Nat st i in dom b1 holds
b1 . i = (G1 . i) + (G2 . i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence_of_Matrix of K st dom b1 = dom G1 & ( for i being Nat st i in dom b1 holds
b1 . i = (G1 . i) + (G2 . i) ) & dom b2 = dom G1 & ( for i being Nat st i in dom b2 holds
b2 . i = (G1 . i) + (G2 . i) ) holds
b1 = b2
proof end;
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 & ( for i being Nat st i in dom b4 holds
b4 . i = (G1 . i) + (G2 . i) ) ) );

definition
let K be Field;
let R be FinSequence_of_Square-Matrix of K;
let G be FinSequence_of_Matrix of K;
:: original: (+)
redefine func R (+) G -> FinSequence_of_Square-Matrix of K;
coherence
R (+) G is FinSequence_of_Square-Matrix of K
proof end;
end;

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

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

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))*>
proof end;

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

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)*>
proof end;

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

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 & len A2 = len B2 & width A1 = width B1 & width A2 = width B2 holds
(block_diagonal <*A1,A2*>,a1) + (block_diagonal <*B1,B2*>,a2) = block_diagonal (<*A1,A2*> (+) <*B1,B2*>),(a1 + a2)
proof end;

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 & Width R1 = Width R2 holds
(block_diagonal R1,a1) + (block_diagonal R2,a2) = block_diagonal (R1 (+) R2),(a1 + a2)
proof end;

definition
let K be Field;
let G1, G2 be FinSequence_of_Matrix of K;
func G1 (#) G2 -> FinSequence_of_Matrix of K means :Def11: :: MATRIXJ1:def 11
( dom it = dom G1 & ( 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 & ( for i being Nat st i in dom b1 holds
b1 . i = (G1 . i) * (G2 . i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence_of_Matrix of K st dom b1 = dom G1 & ( for i being Nat st i in dom b1 holds
b1 . i = (G1 . i) * (G2 . i) ) & dom b2 = dom G1 & ( for i being Nat st i in dom b2 holds
b2 . i = (G1 . i) * (G2 . i) ) holds
b1 = b2
proof end;
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 & ( 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 & Width (G1 (#) G2) = Width G2 )
proof end;

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

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))*>
proof end;

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

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)*>
proof end;

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))
proof end;

theorem Th78: :: MATRIXJ1:78
for K being Field
for A1, B1, A2, B2 being Matrix of K st width A1 = len B1 & 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)
proof end;

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)
proof end;