:: by Karol P\c{a}k

::

:: Received May 13, 2008

:: Copyright (c) 2008-2018 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)

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

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))

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

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)

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

ex b_{1} being Element of NAT st

( i <= Sum (f | b_{1}) & b_{1} in dom f & ( for j being Nat st i <= Sum (f | j) holds

b_{1} <= j ) )

for b_{1}, b_{2} being Element of NAT st i <= Sum (f | b_{1}) & b_{1} in dom f & ( for j being Nat st i <= Sum (f | j) holds

b_{1} <= j ) & i <= Sum (f | b_{2}) & b_{2} in dom f & ( for j being Nat st i <= Sum (f | j) holds

b_{2} <= j ) holds

b_{1} = b_{2}

end;
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 ( i <= Sum (f | it) & it in dom f & ( for j being Nat st i <= Sum (f | j) holds

it <= j ) );

ex b

( i <= Sum (f | b

b

proof end;

uniqueness for b

b

b

b

proof 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_{3} being Element of NAT holds

( b_{3} = min (f,i) iff ( i <= Sum (f | b_{3}) & b_{3} in dom f & ( for j being Nat st i <= Sum (f | j) holds

b_{3} <= j ) ) );

for f being FinSequence of NAT

for i being Nat st i in Seg (Sum f) holds

for b

( b

b

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

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 )

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)

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) )

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 )

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

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

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

for i being Nat st i in dom F holds

F . i is Matrix of D;

:: 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 );

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 ;

ex b_{1} being FinSequence of (D *) * st b_{1} is Matrix-yielding

end;
cluster Relation-like NAT -defined (D *) * -valued Function-like V37() FinSequence-like FinSubsequence-like Matrix-yielding for of ;

existence ex b

proof end;

definition
end;

definition

let K be Field;

mode FinSequence_of_Matrix of K is Matrix-yielding FinSequence of ( the carrier of K *) * ;

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

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

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

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

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

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

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

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

redefine func F /^ n -> FinSequence_of_Matrix of D;

coherence

F /^ n is FinSequence_of_Matrix of D

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

definition

let D be non empty set ;

let F be FinSequence_of_Matrix of D;

ex b_{1} being FinSequence of NAT st

( dom b_{1} = dom F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = len (F . i) ) )

for b_{1}, b_{2} being FinSequence of NAT st dom b_{1} = dom F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = len (F . i) ) & dom b_{2} = dom F & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = len (F . i) ) holds

b_{1} = b_{2}

ex b_{1} being FinSequence of NAT st

( dom b_{1} = dom F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = width (F . i) ) )

for b_{1}, b_{2} being FinSequence of NAT st dom b_{1} = dom F & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = width (F . i) ) & dom b_{2} = dom F & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = width (F . i) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom F & ( for i being Nat st i in dom it holds

it . i = len (F . i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

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 ( dom it = dom F & ( for i being Nat st i in dom it holds

it . i = width (F . i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines Len MATRIXJ1:def 3 :

for D being non empty set

for F being FinSequence_of_Matrix of D

for b_{3} being FinSequence of NAT holds

( b_{3} = Len F iff ( dom b_{3} = dom F & ( for i being Nat st i in dom b_{3} holds

b_{3} . i = len (F . i) ) ) );

for D being non empty set

for F being FinSequence_of_Matrix of D

for b

( b

b

:: deftheorem Def4 defines Width MATRIXJ1:def 4 :

for D being non empty set

for F being FinSequence_of_Matrix of D

for b_{3} being FinSequence of NAT holds

( b_{3} = Width F iff ( dom b_{3} = dom F & ( for i being Nat st i in dom b_{3} holds

b_{3} . i = width (F . i) ) ) );

for D being non empty set

for F being FinSequence_of_Matrix of D

for b

( b

b

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

redefine func Width F -> Element of (len F) -tuples_on NAT;

coherence

Width F is Element of (len F) -tuples_on NAT

end;
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: Widthredefine func Width F -> Element of (len F) -tuples_on NAT;

coherence

Width F is Element of (len F) -tuples_on NAT

proof 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

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)

for F1, F2 being FinSequence_of_Matrix of D holds Len (F1 ^ F2) = (Len F1) ^ (Len F2)

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)

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

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)

for F1, F2 being FinSequence_of_Matrix of D holds Width (F1 ^ F2) = (Width F1) ^ (Width F2)

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)

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

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;

ex b_{1} being Matrix of D st

( len b_{1} = Sum (Len F) & width b_{1} = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices b_{1} holds

( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b_{1} * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies b_{1} * (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))))) ) ) ) )

for b_{1}, b_{2} being Matrix of D st len b_{1} = Sum (Len F) & width b_{1} = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices b_{1} holds

( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b_{1} * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies b_{1} * (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_{2} = Sum (Len F) & width b_{2} = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices b_{2} holds

( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b_{2} * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies b_{2} * (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_{1} = b_{2}

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

ex b

( len b

( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b

proof end;

uniqueness for b

( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b

( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b

b

proof 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_{4} being Matrix of D holds

( b_{4} = block_diagonal (F,d) iff ( len b_{4} = Sum (Len F) & width b_{4} = Sum (Width F) & ( for i, j being Nat st [i,j] in Indices b_{4} holds

( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b_{4} * (i,j) = d ) & ( Sum ((Width F) | ((min ((Len F),i)) -' 1)) < j & j <= Sum ((Width F) | (min ((Len F),i))) implies b_{4} * (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))))) ) ) ) ) );

for D being non empty set

for d being Element of D

for F being FinSequence_of_Matrix of D

for b

( b

( ( ( j <= Sum ((Width F) | ((min ((Len F),i)) -' 1)) or j > Sum ((Width F) | (min ((Len F),i))) ) implies b

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

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

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) = {}

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)) ) ) )

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)) ) ) )

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)))

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)

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)) ) )

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))))

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

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))))) )

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))))))

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)))

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)))))

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

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)

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)

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)

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)

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 )

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) )

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)

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)

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)

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)

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

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

for i being Nat st i in dom F holds

ex n being Nat st F . i is Matrix of n,D;

:: 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 );

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 ;

ex b_{1} being FinSequence of (D *) * st b_{1} is Square-Matrix-yielding

end;
cluster Relation-like NAT -defined (D *) * -valued Function-like V37() FinSequence-like FinSubsequence-like Square-Matrix-yielding for of ;

existence ex b

proof end;

registration

let D be non empty set ;

coherence

for b_{1} being FinSequence of (D *) * st b_{1} is Square-Matrix-yielding holds

b_{1} is Matrix-yielding

end;
coherence

for b

b

proof end;

definition

let D be non empty set ;

mode FinSequence_of_Square-Matrix of D is Square-Matrix-yielding FinSequence of (D *) * ;

end;
mode FinSequence_of_Square-Matrix of D is Square-Matrix-yielding FinSequence of (D *) * ;

definition

let K be Field;

mode FinSequence_of_Square-Matrix of K is Square-Matrix-yielding FinSequence of ( the carrier of K *) * ;

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

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

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

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

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

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

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

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

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

redefine func S /^ n -> FinSequence_of_Square-Matrix of D;

coherence

S /^ n is FinSequence_of_Square-Matrix of D

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

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

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

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)

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)

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;

ex b_{1} being FinSequence of K st

( dom b_{1} = dom R & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = Det (R . i) ) )

for b_{1}, b_{2} being FinSequence of K st dom b_{1} = dom R & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = Det (R . i) ) & dom b_{2} = dom R & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = Det (R . i) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom R & ( for i being Nat st i in dom it holds

it . i = Det (R . i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines Det MATRIXJ1:def 7 :

for K being Field

for R being FinSequence_of_Square-Matrix of K

for b_{3} being FinSequence of K holds

( b_{3} = Det R iff ( dom b_{3} = dom R & ( for i being Nat st i in dom b_{3} holds

b_{3} . i = Det (R . i) ) ) );

for K being Field

for R being FinSequence_of_Square-Matrix of K

for b

( b

b

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

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

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)

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

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)

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)

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

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

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 ;

ex b_{1} being FinSequence_of_Square-Matrix of K st

( dom b_{1} = dom f & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = 1. (K,(f . i)) ) )

for b_{1}, b_{2} being FinSequence_of_Square-Matrix of K st dom b_{1} = dom f & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = 1. (K,(f . i)) ) & dom b_{2} = dom f & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = 1. (K,(f . i)) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom f & ( for i being Nat st i in dom it holds

it . i = 1. (K,(f . i)) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines 1. MATRIXJ1:def 8 :

for K being Field

for f being FinSequence of NAT

for b_{3} being FinSequence_of_Square-Matrix of K holds

( b_{3} = 1. (K,f) iff ( dom b_{3} = dom f & ( for i being Nat st i in dom b_{3} holds

b_{3} . i = 1. (K,(f . i)) ) ) );

for K being Field

for f being FinSequence of NAT

for b

( b

b

theorem :: MATRIXJ1:56

for K being Field

for f being FinSequence of NAT holds

( Len (1. (K,f)) = f & Width (1. (K,f)) = f )

for f being FinSequence of NAT holds

( Len (1. (K,f)) = f & Width (1. (K,f)) = f )

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

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))

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))

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;

ex b_{1} being FinSequence_of_Matrix of K st

( dom b_{1} = dom G & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (p /. i) * (G . i) ) )

for b_{1}, b_{2} being FinSequence_of_Matrix of K st dom b_{1} = dom G & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (p /. i) * (G . i) ) & dom b_{2} = dom G & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (p /. i) * (G . i) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom G & ( for i being Nat st i in dom it holds

it . i = (p /. i) * (G . i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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_{4} being FinSequence_of_Matrix of K holds

( b_{4} = mlt (p,G) iff ( dom b_{4} = dom G & ( for i being Nat st i in dom b_{4} holds

b_{4} . i = (p /. i) * (G . i) ) ) );

for K being Field

for G being FinSequence_of_Matrix of K

for p being FinSequence of K

for b

( b

b

registration

let K be Field;

let R be FinSequence_of_Square-Matrix of K;

let p be FinSequence of K;

coherence

mlt (p,R) is Square-Matrix-yielding

end;
let R be FinSequence_of_Square-Matrix of K;

let p be FinSequence of K;

coherence

mlt (p,R) is Square-Matrix-yielding

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

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)*>

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))

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))

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;

ex b_{1} being FinSequence_of_Matrix of K st

( dom b_{1} = dom G1 & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (G1 . i) + (G2 . i) ) )

for b_{1}, b_{2} being FinSequence_of_Matrix of K st dom b_{1} = dom G1 & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (G1 . i) + (G2 . i) ) & dom b_{2} = dom G1 & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (G1 . i) + (G2 . i) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom G1 & ( for i being Nat st i in dom it holds

it . i = (G1 . i) + (G2 . i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def10 defines (+) MATRIXJ1:def 10 :

for K being Field

for G1, G2, b_{4} being FinSequence_of_Matrix of K holds

( b_{4} = G1 (+) G2 iff ( dom b_{4} = dom G1 & ( for i being Nat st i in dom b_{4} holds

b_{4} . i = (G1 . i) + (G2 . i) ) ) );

for K being Field

for G1, G2, b

( b

b

registration

let K be Field;

let R be FinSequence_of_Square-Matrix of K;

let G be FinSequence_of_Matrix of K;

coherence

R (+) G is Square-Matrix-yielding

end;
let R be FinSequence_of_Square-Matrix of K;

let G be FinSequence_of_Matrix of K;

coherence

R (+) G is Square-Matrix-yielding

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

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)

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))*>

for A being Matrix of K

for G being FinSequence_of_Matrix of K holds <*A*> (+) G = <*(A + (G . 1))*>

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)*>

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))

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))

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;

ex b_{1} being FinSequence_of_Matrix of K st

( dom b_{1} = dom G1 & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (G1 . i) * (G2 . i) ) )

for b_{1}, b_{2} being FinSequence_of_Matrix of K st dom b_{1} = dom G1 & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = (G1 . i) * (G2 . i) ) & dom b_{2} = dom G1 & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = (G1 . i) * (G2 . i) ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom G1 & ( for i being Nat st i in dom it holds

it . i = (G1 . i) * (G2 . i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def11 defines (#) MATRIXJ1:def 11 :

for K being Field

for G1, G2, b_{4} being FinSequence_of_Matrix of K holds

( b_{4} = G1 (#) G2 iff ( dom b_{4} = dom G1 & ( for i being Nat st i in dom b_{4} holds

b_{4} . i = (G1 . i) * (G2 . i) ) ) );

for K being Field

for G1, G2, b

( b

b

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 )

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)

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))*>

for A being Matrix of K

for G being FinSequence_of_Matrix of K holds <*A*> (#) G = <*(A * (G . 1))*>

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)*>

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))

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))

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;