environ
vocabularies HIDDEN, NUMBERS, NAT_1, VECTSP_1, SUBSET_1, RLSUB_1, XBOOLE_0, ARYTM_3, STRUCT_0, TARSKI, RLVECT_3, RLVECT_2, CARD_3, SUPINF_2, FINSET_1, FUNCT_1, RLSUB_2, FUNCT_2, RLVECT_5, MATRLIN, RELAT_1, CARD_1, XXREAL_0, FINSEQ_1, ZFMISC_1, ALGSTR_0, PARTFUN1, ORDINAL4, FINSEQ_2, INCSP_1, MESFUNC1, TREES_1, MATRIX_1, GROUP_1, ARYTM_1, FINSEQ_4, RFINSEQ, RANKNULL, MATRIXJ1, MATRIX_3, MATRIX_6, FVSUM_1, RVSUM_1, MATRIXR1, VECTSP10, MATRIX15, QC_LANG1, CLASSES1, PRVECT_1, MATRIX13, LMOD_7, VALUED_1, RLVECT_1, BINOP_1, LATTICES, MATRLIN2, UNIALG_1, MSSUBFAM;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, FINSEQ_1, BINOP_1, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_2, MATRIX_0, MATRIX_1, FVSUM_1, MATRIX_3, MATRIX_6, DOMAIN_1, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, FINSEQOP, PRVECT_1, MATRIX13, MATRLIN, MATRIX15, RFINSEQ, WSIERP_1, MOD_2, VECTSP_5, RANKNULL, MATRIXJ1;
definitions TARSKI, FUNCT_1, VECTSP_7, VECTSP_6;
theorems ZFMISC_1, RLVECT_1, MATRIX_0, MATRIX_4, MATRIX_3, VECTSP_1, NAT_1, FINSEQ_2, CARD_1, FINSEQ_1, FINSEQ_3, FINSEQOP, FUNCT_1, FUNCT_2, FUNCOP_1, FVSUM_1, LAPLACE, MATRIX_6, MATRIX_7, MATRIX11, MATRIX13, MATRIXR1, MATRIXR2, MATRLIN, ORDINAL1, PARTFUN1, RELAT_1, STRUCT_0, TARSKI, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, XBOOLE_0, XBOOLE_1, XXREAL_0, MATRIX15, MOD_2, RLVECT_2, VECTSP10, MATRIX_8, RANKNULL, VECTSP_5, FINSEQ_5, RFINSEQ, MATRIXJ1, MATRIX_1, CARD_2;
schemes NAT_1, MATRIX_0, FUNCT_2, FINSEQ_2;
registrations XBOOLE_0, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, FUNCT_2, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, FINSEQ_2, MATRLIN, VECTSP_2, MATRIX13, XREAL_0, VECTSP_9, CARD_1, MOD_2, PRVECT_1, GRCAT_1, MATRIX_6;
constructors HIDDEN, FVSUM_1, VECTSP_9, MATRIX_6, LAPLACE, MATRIX15, VECTSP_2, RANKNULL, VECTSP10, MATRIXJ1, REALSET1, RELSET_1, MATRIX13, MATRIX_1;
requirements HIDDEN, ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
equalities STRUCT_0, RLVECT_1, FINSEQ_1, VECTSP_4, FVSUM_1, VECTSP_1, MATRIX_0, MATRIX13, MATRLIN, MATRIX15, RANKNULL, VECTSP_6, CARD_1, ORDINAL1;
expansions STRUCT_0, TARSKI, FINSEQ_1, VECTSP_1, FUNCT_1, VECTSP_7;
Lm1:
for K being Field
for V1 being finite-dimensional VectSp of K
for R being FinSequence of V1
for p being FinSequence of K holds dom (lmlt (p,R)) = (dom p) /\ (dom R)
Lm2:
for K being Field
for p1, p2 being FinSequence of K holds dom (p1 + p2) = (dom p1) /\ (dom p2)
Lm3:
for K being Field
for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1 holds dom (R1 + R2) = (dom R1) /\ (dom R2)
Lm4:
for K being Field
for V being VectSp of K
for W1 being Subspace of V
for L1 being Linear_Combination of W1 ex K1 being Linear_Combination of V st
( Carrier K1 = Carrier L1 & Sum K1 = Sum L1 & K1 | the carrier of W1 = L1 )
definition
let K be
Field;
let V1,
V2 be
finite-dimensional VectSp of
K;
let f be
Function of
V1,
V2;
let B1 be
FinSequence of
V1;
let b2 be
OrdBasis of
V2;
AutMtredefine func AutMt (
f,
B1,
b2)
-> Matrix of
len B1,
len b2,
K;
coherence
AutMt (f,B1,b2) is Matrix of len B1, len b2,K
end;
theorem
for
K being
Field for
V1,
V2 being
finite-dimensional VectSp of
K for
b1 being
OrdBasis of
V1 for
b2 being
OrdBasis of
V2 for
f being
linear-transformation of
V1,
V2 for
W1,
W2 being
Subspace of
V1 for
U1,
U2 being
Subspace of
V2 st (
dim W1 = 0 implies
dim U1 = 0 ) & (
dim W2 = 0 implies
dim U2 = 0 ) &
V2 is_the_direct_sum_of U1,
U2 holds
for
fW1 being
linear-transformation of
W1,
U1 for
fW2 being
linear-transformation of
W2,
U2 st
fW1 = f | W1 &
fW2 = f | W2 holds
for
w1 being
OrdBasis of
W1 for
w2 being
OrdBasis of
W2 for
u1 being
OrdBasis of
U1 for
u2 being
OrdBasis of
U2 st
w1 ^ w2 = b1 &
u1 ^ u2 = b2 holds
AutMt (
f,
b1,
b2)
= block_diagonal (
<*(AutMt (fW1,w1,u1)),(AutMt (fW2,w2,u2))*>,
(0. K))
definition
let K be
Field;
let V1,
V2 be
finite-dimensional VectSp of
K;
let b1 be
OrdBasis of
V1;
let B2 be
FinSequence of
V2;
let M be
Matrix of
len b1,
len B2,
K;
existence
ex b1 being Function of V1,V2 st
for v being Vector of V1 holds b1 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2))
uniqueness
for b1, b2 being Function of V1,V2 st ( for v being Vector of V1 holds b1 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) ) & ( for v being Vector of V1 holds b2 . v = Sum (lmlt ((Line (((LineVec2Mx (v |-- b1)) * M),1)),B2)) ) holds
b1 = b2
end;
Lm5:
for K being Field
for A, B being Matrix of K st width A = width B holds
for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
theorem
for
K being
Field for
V1,
V2 being
finite-dimensional VectSp of
K for
b1 being
OrdBasis of
V1 for
B2 being
FinSequence of
V2 for
A,
B being
Matrix of
len b1,
len B2,
K holds
Mx2Tran (
(A + B),
b1,
B2)
= (Mx2Tran (A,b1,B2)) + (Mx2Tran (B,b1,B2))
theorem
for
K being
Field for
V1,
V2,
V3 being
finite-dimensional VectSp of
K for
b1 being
OrdBasis of
V1 for
b2 being
OrdBasis of
V2 for
B3 being
FinSequence of
V3 for
A being
Matrix of
len b1,
len b2,
K for
B being
Matrix of
len b2,
len B3,
K st
width A = len B holds
for
AB being
Matrix of
len b1,
len B3,
K st
AB = A * B holds
Mx2Tran (
AB,
b1,
B3)
= (Mx2Tran (B,b2,B3)) * (Mx2Tran (A,b1,b2))
Lm6:
for n being Nat
for K being Field holds the_rank_of (1. (K,n)) = n
Lm7:
for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A being Matrix of len b1, len b2,K st len b1 > 0 & len b2 > 0 holds
nullity (Mx2Tran (A,b1,b2)) = (len b1) - (the_rank_of A)
Lm8:
for K being Field
for V1, V2, V3 being finite-dimensional VectSp of K
for f being linear-transformation of V1,V2
for g being Function of V2,V3 holds g * f = (g | (im f)) * f