environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, MATRIX_1, FINSEQ_3, RELAT_1, FINSEQ_1, TARSKI, ARYTM_3, XXREAL_0, CARD_1, TREES_1, FUNCT_1, INCSP_1, ORDINAL4, SUBSET_1, VECTSP_1, RLVECT_2, RLVECT_3, CARD_3, ARYTM_1, SUPINF_2, RLVECT_5, FINSET_1, STRUCT_0, RLSUB_1, ALGSTR_0, PARTFUN1, RLVECT_1, ZFMISC_1, QC_LANG1, FUNCT_2, VALUED_1, PRE_POLY, FINSEQ_2, RVSUM_1, FINSEQ_4, FVSUM_1, MATRLIN, MSSUBFAM, UNIALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MOD_2, FINSEQ_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, MATRIX_0, STRUCT_0, ALGSTR_0, MATRIX_1, MATRIX_3, FVSUM_1, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, FINSET_1, FINSEQ_3, FINSEQ_2, FINSEQOP, BINOP_1, XXREAL_0, PRE_POLY, GRCAT_1;
definitions TARSKI;
theorems TARSKI, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, RLVECT_1, FUNCT_1, FUNCT_2, FUNCT_3, MATRIX_3, MOD_2, ZFMISC_1, NAT_1, FVSUM_1, SUBSET_1, FINSEQOP, FUNCOP_1, RELAT_1, PARTFUN2, XBOOLE_0, XBOOLE_1, RLVECT_2, ORDINAL1, PARTFUN1, PRE_POLY, MATRIX_0;
schemes FINSEQ_1, FINSEQ_2, FUNCT_2, MATRIX_0, NAT_1, FINSEQ_4;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, VECTSP_1, CARD_1, VECTSP_7, PRE_POLY, RELAT_1, FUNCT_1, MATRIX_0;
constructors HIDDEN, PARTFUN1, BINOP_1, FUNCT_3, SQUARE_1, NAT_1, VECTSP_6, VECTSP_7, MOD_2, FVSUM_1, MATRIX_3, RELSET_1, PRE_POLY, GRCAT_1, MATRIX_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FVSUM_1, FUNCOP_1, ALGSTR_0;
expansions TARSKI;
definition
let D be non
empty set ;
let n,
m,
k be
Nat;
let M1 be
Matrix of
n,
k,
D;
let M2 be
Matrix of
m,
k,
D;
^redefine func M1 ^ M2 -> Matrix of
n + m,
k,
D;
coherence
M1 ^ M2 is Matrix of n + m,k,D
end;
theorem
for
k,
t,
i,
m,
n being
Nat for
D being non
empty set for
M1 being
Matrix of
t,
k,
D for
M2 being
Matrix of
m,
k,
D st
n in dom M2 &
i = (len M1) + n holds
Line (
(M1 ^ M2),
i)
= Line (
M2,
n)
theorem Th33:
for
m,
n being
Nat for
K being
Field for
V1 being
finite-dimensional VectSp of
K for
M being
Matrix of
n,
m, the
carrier of
K st
n > 0 &
m > 0 holds
for
p,
d being
FinSequence of
K st
len p = n &
len d = m & ( for
j being
Nat st
j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for
b,
c being
FinSequence of
V1 st
len b = m &
len c = n & ( for
i being
Nat st
i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))
Lm1:
for K being Field
for V being finite-dimensional VectSp of K
for b being OrdBasis of V
for W being Element of V holds dom (W |-- b) = dom b
Lm2:
for p being FinSequence
for k being set st k in dom p holds
len p > 0
Lm3:
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for f being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 holds dom (AutMt (f,b1,b2)) = dom b1
theorem
for
K being
Field for
V1,
V2,
V3 being
finite-dimensional VectSp of
K for
f being
Function of
V1,
V2 for
g being
Function of
V2,
V3 for
b1 being
OrdBasis of
V1 for
b2 being
OrdBasis of
V2 for
b3 being
OrdBasis of
V3 st
g is
additive &
g is
homogeneous &
len b1 > 0 &
len b2 > 0 holds
AutMt (
(g * f),
b1,
b3)
= (AutMt (f,b1,b2)) * (AutMt (g,b2,b3))