environ
vocabularies HIDDEN, NUMBERS, NAT_1, VECTSP_1, SUBSET_1, XBOOLE_0, MATRIX_1, FINSEQ_1, ALGSTR_0, RELAT_1, ARYTM_3, TARSKI, STRUCT_0, ZFMISC_1, ORDINAL4, XXREAL_0, FUNCT_1, PARTFUN1, FINSEQ_3, CARD_1, ARYTM_1, FINSEQ_2, CARD_3, GROUP_1, RFINSEQ, TREES_1, INCSP_1, MATRIX_3, SUPINF_2, LAPLACE, MATRIX11, MESFUNC1, RVSUM_1, MATHMORP, VALUED_1, FVSUM_1, MATRIXJ1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_2, MATRIX_0, MATRIX_1, FVSUM_1, NAT_D, GROUP_4, MATRIX_3, MATRIX11, FINSEQOP, MATRIX13, LAPLACE, RFINSEQ, WSIERP_1;
definitions TARSKI;
theorems CARD_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, FINSEQ_6, FINSEQOP, FUNCT_1, FVSUM_1, GROUP_1, GROUP_4, LAPLACE, MATRIX_0, MATRIX_3, MATRIX_9, MATRIX11, MATRIX13, MATRIX15, MATRIXR2, NAT_1, ORDINAL1, PARTFUN1, POLYNOM3, PRGCOR_1, RELAT_1, RFINSEQ, RLVECT_1, RVSUM_1, TARSKI, VECTSP_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ZFMISC_1, MATRIX_4, FUNCT_2, FUNCOP_1, MATRIXR1, CARD_1, NAT_D, MATRIX_1;
schemes FINSEQ_1, FINSEQ_2, NAT_1, MATRIX_0;
registrations XBOOLE_0, FINSET_1, STRUCT_0, VECTSP_1, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, FINSEQ_2, MATRIX13, XREAL_0, VALUED_0, CARD_1;
constructors HIDDEN, GROUP_4, MATRIX11, MATRIX13, LAPLACE, RFINSEQ, WSIERP_1, REAL_1, BINARITH, RELSET_1, FVSUM_1, MATRIX_1, NUMBERS, RECDEF_1;
requirements HIDDEN, ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
equalities FINSEQ_1, MATRIX_0, LAPLACE, MATRIX13, FVSUM_1;
expansions FINSEQ_1;
Lm1:
for K being non empty addLoopStr
for p1, p2 being FinSequence of K holds dom (p1 + p2) = (dom p1) /\ (dom p2)
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)
Lm3:
for D being non empty set
for M being Matrix of D holds <*M*> is Matrix-yielding
Lm4:
for D being non empty set
for M being Matrix of D holds Sum (Len <*M*>) = len M
Lm5:
for D being non empty set
for M being Matrix of D holds Sum (Width <*M*>) = width M
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:
(
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 Th23:
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:
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)) ) ) )
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
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))
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))
theorem Th71:
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))
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:
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))