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

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 b₁ being Element of NAT st
( i <= Sum (f | b₁) & b₁ in dom f & ( for j being Nat st i <= Sum (f | j) holds
b₁ <= j ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st i <= Sum (f | b₁) & b₁ in dom f & ( for j being Nat st i <= Sum (f | j) holds
b₁ <= j ) & i <= Sum (f | b₂) & b₂ in dom f & ( for j being Nat st i <= Sum (f | j) holds
b₂ <= j ) holds
b₁ = b₂

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 b₃ being Element of NAT holds
( b₃ = min (f,i) iff ( i <= Sum (f | b₃) & b₃ in dom f & ( for j being Nat st i <= Sum (f | j) holds
b₃ <= 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;

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 Relation-like NAT -defined (D *) * -valued Function-like V37() FinSequence-like FinSubsequence-like Matrix-yielding for FinSequence of (D *) * ;

existence
ex b₁ being FinSequence of (D *) * st b₁ 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 n be Nat;
let F be FinSequence_of_Matrix of D;
:: 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;

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 b₁ being FinSequence of NAT st
( dom b₁ = dom F & ( for i being Nat st i in dom b₁ holds
b₁ . i = len (F . i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st dom b₁ = dom F & ( for i being Nat st i in dom b₁ holds
b₁ . i = len (F . i) ) & dom b₂ = dom F & ( for i being Nat st i in dom b₂ holds
b₂ . i = len (F . i) ) holds
b₁ = b₂

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 b₁ being FinSequence of NAT st
( dom b₁ = dom F & ( for i being Nat st i in dom b₁ holds
b₁ . i = width (F . i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st dom b₁ = dom F & ( for i being Nat st i in dom b₁ holds
b₁ . i = width (F . i) ) & dom b₂ = dom F & ( for i being Nat st i in dom b₂ holds
b₂ . i = width (F . i) ) holds
b₁ = b₂

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 b₃ being FinSequence of NAT holds
( b₃ = Len F iff ( dom b₃ = dom F & ( for i being Nat st i in dom b₃ holds
b₃ . 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 b₃ being FinSequence of NAT holds
( b₃ = Width F iff ( dom b₃ = dom F & ( for i being Nat st i in dom b₃ holds
b₃ . 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;

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 b₁ being Matrix of D st
( len b₁ = Sum (Len F) & width b₁ = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices b₁ holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b₁ * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies b₁ * (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 b₁, b₂ being Matrix of D st len b₁ = Sum (Len F) & width b₁ = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices b₁ holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b₁ * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies b₁ * (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 b₂ = Sum (Len F) & width b₂ = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices b₂ holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b₂ * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies b₂ * (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
b₁ = b₂

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 b₄ being Matrix of D holds
( b₄ = block_diagonal (F,d) iff ( len b₄ = Sum (Len F) & width b₄ = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices b₄ holds
( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b₄ * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies b₄ * (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 F1, F2 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 F1, F2 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 Relation-like NAT -defined (D *) * -valued Function-like V37() FinSequence-like FinSubsequence-like Square-Matrix-yielding for FinSequence of (D *) * ;

existence
ex b₁ being FinSequence of (D *) * st b₁ is Square-Matrix-yielding

proof end;

end;

registration

let D be non empty set ;

cluster Square-Matrix-yielding -> Matrix-yielding for FinSequence of (D *) * ;

coherence
for b₁ being FinSequence of (D *) * st b₁ is Square-Matrix-yielding holds
b₁ 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 n be Nat;
let S be FinSequence_of_Square-Matrix of D;
:: 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 i, j, n 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 i, j, n 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 b₁ being FinSequence of K st
( dom b₁ = dom R & ( for i being Nat st i in dom b₁ holds
b₁ . i = Det (R . i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of K st dom b₁ = dom R & ( for i being Nat st i in dom b₁ holds
b₁ . i = Det (R . i) ) & dom b₂ = dom R & ( for i being Nat st i in dom b₂ holds
b₂ . i = Det (R . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Det MATRIXJ1:def 7 :
for K being Field
for R being FinSequence_of_Square-Matrix of K
for b₃ being FinSequence of K holds
( b₃ = Det R iff ( dom b₃ = dom R & ( for i being Nat st i in dom b₃ holds
b₃ . 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 m, n 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;

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 b₁ being FinSequence_of_Square-Matrix of K st
( dom b₁ = dom f & ( for i being Nat st i in dom b₁ holds
b₁ . i = 1. (K,(f . i)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence_of_Square-Matrix of K st dom b₁ = dom f & ( for i being Nat st i in dom b₁ holds
b₁ . i = 1. (K,(f . i)) ) & dom b₂ = dom f & ( for i being Nat st i in dom b₂ holds
b₂ . i = 1. (K,(f . i)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines 1. MATRIXJ1:def 8 :
for K being Field
for f being FinSequence of NAT
for b₃ being FinSequence_of_Square-Matrix of K holds
( b₃ = 1. (K,f) iff ( dom b₃ = dom f & ( for i being Nat st i in dom b₃ holds
b₃ . 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;

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 b₁ being FinSequence_of_Matrix of K st
( dom b₁ = dom G & ( for i being Nat st i in dom b₁ holds
b₁ . i = (p /. i) * (G . i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence_of_Matrix of K st dom b₁ = dom G & ( for i being Nat st i in dom b₁ holds
b₁ . i = (p /. i) * (G . i) ) & dom b₂ = dom G & ( for i being Nat st i in dom b₂ holds
b₂ . i = (p /. i) * (G . i) ) holds
b₁ = b₂

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 b₄ being FinSequence_of_Matrix of K holds
( b₄ = mlt (p,G) iff ( dom b₄ = dom G & ( for i being Nat st i in dom b₄ holds
b₄ . 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

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 b₁ being FinSequence_of_Matrix of K st
( dom b₁ = dom G1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = (G1 . i) + (G2 . i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence_of_Matrix of K st dom b₁ = dom G1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = (G1 . i) + (G2 . i) ) & dom b₂ = dom G1 & ( for i being Nat st i in dom b₂ holds
b₂ . i = (G1 . i) + (G2 . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines (+) MATRIXJ1:def 10 :
for K being Field
for G1, G2, b₄ being FinSequence_of_Matrix of K holds
( b₄ = G1 (+) G2 iff ( dom b₄ = dom G1 & ( for i being Nat st i in dom b₄ holds
b₄ . 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;

cluster R (+) G -> Square-Matrix-yielding ;

coherence
R (+) G is Square-Matrix-yielding

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, G9, G1, G2 being FinSequence_of_Matrix of K st len G = len G9 holds
(G ^ G1) (+) (G9 ^ G2) = (G (+) G9) ^ (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, A2, B1, 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, A2, B1, 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 b₁ being FinSequence_of_Matrix of K st
( dom b₁ = dom G1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = (G1 . i) * (G2 . i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence_of_Matrix of K st dom b₁ = dom G1 & ( for i being Nat st i in dom b₁ holds
b₁ . i = (G1 . i) * (G2 . i) ) & dom b₂ = dom G1 & ( for i being Nat st i in dom b₂ holds
b₂ . i = (G1 . i) * (G2 . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines (#) MATRIXJ1:def 11 :
for K being Field
for G1, G2, b₄ being FinSequence_of_Matrix of K holds
( b₄ = G1 (#) G2 iff ( dom b₄ = dom G1 & ( for i being Nat st i in dom b₄ holds
b₄ . 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, G9, G1, G2 being FinSequence_of_Matrix of K st len G = len G9 holds
(G ^ G1) (#) (G9 ^ G2) = (G (#) G9) ^ (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, A2, B1, 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, A2, B1, 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;