:: Block Diagonal Matrices
:: by Karol P\c{a}k
::
:: Received May 13, 2008
:: Copyright (c) 2008 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)
theorem Th1: :: MATRIXJ1:1
theorem Th2: :: MATRIXJ1:2
theorem Th3: :: MATRIXJ1:3
theorem Th4: :: MATRIXJ1:4
theorem :: MATRIXJ1:5
:: deftheorem Def1 defines min MATRIXJ1:def 1 :
theorem :: MATRIXJ1:6
theorem Th7: :: MATRIXJ1:7
theorem Th8: :: MATRIXJ1:8
theorem Th9: :: MATRIXJ1:9
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)
theorem Th10: :: MATRIXJ1:10
theorem :: MATRIXJ1:11
:: deftheorem Def2 defines Matrix-yielding MATRIXJ1:def 2 :
theorem Th12: :: MATRIXJ1:12
Lm3:
for D being non empty set
for M being Matrix of D holds <*M*> is Matrix-yielding
:: deftheorem Def3 defines Len MATRIXJ1:def 3 :
:: deftheorem Def4 defines Width MATRIXJ1:def 4 :
theorem Th13: :: MATRIXJ1:13
theorem Th14: :: MATRIXJ1:14
theorem Th15: :: MATRIXJ1:15
Lm4:
for D being non empty set
for M being Matrix of D holds Sum (Len <*M*>) = len M
theorem Th16: :: MATRIXJ1:16
theorem Th17: :: MATRIXJ1:17
theorem Th18: :: MATRIXJ1:18
theorem Th19: :: MATRIXJ1:19
Lm5:
for D being non empty set
for M being Matrix of D holds Sum (Width <*M*>) = width M
theorem Th20: :: MATRIXJ1:20
theorem Th21: :: MATRIXJ1:21
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)))) ) ) ) )
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
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)))) ) ) ) ) );
theorem :: MATRIXJ1:22
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) ) ) )
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) ) ) )
theorem Th25: :: MATRIXJ1:25
theorem Th26: :: MATRIXJ1:26
theorem Th27: :: MATRIXJ1:27
theorem Th28: :: MATRIXJ1:28
theorem Th29: :: MATRIXJ1:29
theorem Th30: :: MATRIXJ1:30
theorem Th31: :: MATRIXJ1:31
theorem Th32: :: MATRIXJ1:32
theorem Th33: :: MATRIXJ1:33
theorem Th34: :: MATRIXJ1:34
theorem Th35: :: MATRIXJ1:35
theorem Th36: :: MATRIXJ1:36
theorem :: MATRIXJ1:37
theorem :: MATRIXJ1:38
theorem :: MATRIXJ1:39
theorem Th40: :: MATRIXJ1:40
theorem Th41: :: MATRIXJ1:41
theorem Th42: :: MATRIXJ1:42
theorem Th43: :: MATRIXJ1:43
theorem Th44: :: MATRIXJ1:44
:: deftheorem Def6 defines Square-Matrix-yielding MATRIXJ1:def 6 :
theorem :: MATRIXJ1:45
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
theorem Th46: :: MATRIXJ1:46
theorem Th47: :: MATRIXJ1:47
theorem :: MATRIXJ1:48
:: deftheorem Def7 defines Det MATRIXJ1:def 7 :
theorem Th49: :: MATRIXJ1:49
theorem Th50: :: MATRIXJ1:50
theorem :: MATRIXJ1:51
theorem Th52: :: MATRIXJ1:52
theorem :: MATRIXJ1:53
theorem Th54: :: MATRIXJ1:54
theorem :: MATRIXJ1:55
:: deftheorem Def8 defines 1. MATRIXJ1:def 8 :
theorem :: MATRIXJ1:56
theorem Th57: :: MATRIXJ1:57
theorem Th58: :: MATRIXJ1:58
theorem :: MATRIXJ1:59
theorem Th60: :: MATRIXJ1:60
theorem :: MATRIXJ1:61
:: deftheorem Def9 defines mlt MATRIXJ1:def 9 :
theorem :: MATRIXJ1:62
theorem Th63: :: MATRIXJ1:63
theorem Th64: :: MATRIXJ1:64
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)
theorem :: MATRIXJ1:65
:: deftheorem Def10 defines (+) MATRIXJ1:def 10 :
theorem Th66: :: MATRIXJ1:66
theorem Th67: :: MATRIXJ1:67
theorem Th68: :: MATRIXJ1:68
theorem Th69: :: MATRIXJ1:69
theorem Th70: :: MATRIXJ1:70
Lm8:
for i being Nat
for K being Field
for A1, A2 being Matrix of K st len A1 = len A2 & width A1 = width A2 & i in dom A1 holds
Line (A1 + A2),i = (Line A1,i) + (Line A2,i)
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)
theorem :: MATRIXJ1:72
:: deftheorem Def11 defines (#) MATRIXJ1:def 11 :
theorem Th73: :: MATRIXJ1:73
theorem Th74: :: MATRIXJ1:74
theorem Th75: :: MATRIXJ1:75
theorem Th76: :: MATRIXJ1:76
theorem Th77: :: MATRIXJ1:77
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))
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)
theorem :: MATRIXJ1:79