:: Associated Matrix of Linear Map
:: by Robert Milewski
::
:: Received June 30, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors 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;
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;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve k,t,i,j,m,n for Nat,
x,y,y1,y2 for object,
D for non empty set;
definition
let D be non empty set;
let k;
let M be Matrix of D;
redefine func Del(M,k) -> Matrix of D;
end;
::$CT
theorem :: MATRLIN:2
for M be Matrix of n+1,m,D for M1 be Matrix of D holds
( n > 0 implies width M = width Del(M,n+1) ) &
( M1 = <*M.(n+1)*> implies width M = width M1 );
theorem :: MATRLIN:3
for M be Matrix of n+1,m,D holds Del(M,n+1) is Matrix of n,m,D;
::$CT
definition
let D;
let P be FinSequence of D;
redefine func <*P*> -> Matrix of 1,len P,D;
end;
begin :: More on Finite Sequences
begin :: Sequences and Matrices Concerning Linear Transformations
reserve K for Field,
V for VectSp of K,
a for Element of K,
W for Element of V;
reserve KL1,KL2,KL3 for Linear_Combination of V,
X for Subset of V;
theorem :: MATRLIN:5
X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X &
Sum KL1 = Sum KL2 implies KL1 = KL2;
theorem :: MATRLIN:6
X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X
& Carrier KL3 c= X & Sum KL1 = Sum KL2 + Sum KL3 implies KL1 = KL2 + KL3;
theorem :: MATRLIN:7
X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X
& a <> 0.K & Sum KL1 = a * Sum KL2 implies KL1 = a * KL2;
theorem :: MATRLIN:8
for b2 be Basis of V ex KL be Linear_Combination of V st W = Sum
KL & Carrier KL c= b2;
definition
let K be Field;
let V be VectSp of K;
attr V is finite-dimensional means
:: MATRLIN:def 1
ex A being finite Subset of V st A is Basis of V;
end;
registration
let K be Field;
cluster strict finite-dimensional for VectSp of K;
end;
definition
let K be Field;
let V be finite-dimensional VectSp of K;
mode OrdBasis of V -> FinSequence of V means
:: MATRLIN:def 2
it is one-to-one & rng it is Basis of V;
end;
reserve s for FinSequence,
V1,V2,V3 for finite-dimensional VectSp of K,
f,f1,f2 for Function of V1,V2,
g for Function of V2,V3,
b1 for OrdBasis of V1,
b2 for OrdBasis of V2,
b3 for OrdBasis of V3,
v1,v2 for Vector of V2,
v,w for Element of V1;
reserve p2,F for FinSequence of V1,
p1,d for FinSequence of K,
KL for Linear_Combination of V1;
definition
let K be non empty doubleLoopStr;
let V1,V2 be non empty ModuleStr over K;
let f1,f2 be Function of V1, V2;
func f1+f2 -> Function of V1,V2 means
:: MATRLIN:def 3
for v be Element of V1 holds it .v = f1.v + f2.v;
end;
definition
let K be non empty doubleLoopStr;
let V1,V2 be non empty ModuleStr over K;
let f be Function of V1,V2;
let a be Element of K;
func a*f -> Function of V1,V2 means
:: MATRLIN:def 4
for v be Element of V1 holds it.v = a * (f.v);
end;
theorem :: MATRLIN:9
for a being Element of V1 for F being FinSequence of V1 for G
being FinSequence of K st len F = len G & for k for v being Element of K st k
in dom F & v = G.k holds F.k = v * a holds Sum(F) = Sum(G) * a;
theorem :: MATRLIN:10
for a be Element of V1 for F being FinSequence of K for G being
FinSequence of V1 st len F = len G & for k st k in dom F holds G.k = (F/.k) * a
holds Sum(G) = Sum(F) * a;
theorem :: MATRLIN:11
for V1 being add-associative right_zeroed right_complementable
non empty addLoopStr
for F being FinSequence of V1 st for k st k in dom F holds
F/.k = 0.V1 holds Sum(F) = 0.V1;
definition
let K, V1, p1,p2;
func lmlt(p1,p2) -> FinSequence of V1 equals
:: MATRLIN:def 5
(the lmult of V1).:(p1,p2);
end;
theorem :: MATRLIN:12
dom p1 = dom p2 implies dom lmlt(p1,p2) = dom p1;
definition
let V1 be non empty addLoopStr, M be FinSequence of (the carrier of V1)*;
func Sum M -> FinSequence of V1 means
:: MATRLIN:def 6
len it = len M & for k st k in dom it
holds it/.k = Sum (M/.k);
end;
theorem :: MATRLIN:13
for M be Matrix of the carrier of V1 st len M = 0 holds Sum Sum M = 0.V1;
theorem :: MATRLIN:14
for M be Matrix of m+1,0,the carrier of V1 holds Sum Sum M = 0.V1;
theorem :: MATRLIN:15
for x be Element of D holds <*<*x*>*> = <*<*x*>*>@;
theorem :: MATRLIN:16
for V1,V2 being VectSp of K, f being Function of V1,V2, p being
FinSequence of V1 st f is additive homogeneous holds f.Sum p = Sum(f*p);
theorem :: MATRLIN:17
for a be FinSequence of K, p being FinSequence of V1 st len p =
len a holds f is additive homogeneous implies f*lmlt(a,p) = lmlt(a,f*p);
theorem :: MATRLIN:18
for a be FinSequence of K st len a = len b2 & g is additive homogeneous holds
g.Sum(lmlt(a,b2)) = Sum(lmlt(a,g*b2));
theorem :: MATRLIN:19
for F, F1 being FinSequence of V1, KL being Linear_Combination
of V1, p being Permutation of dom F st F1 = F * p holds KL (#) F1 = (KL (#) F)
* p;
theorem :: MATRLIN:20
F is one-to-one & Carrier KL c= rng F implies Sum(KL (#) F) = Sum KL;
theorem :: MATRLIN:21
for A be set for p be FinSequence of V1 st rng p c= A holds f1
is additive homogeneous & f2 is additive homogeneous &
(for v st v in A holds f1.v = f2.v) implies f1.Sum p
= f2.Sum p;
theorem :: MATRLIN:22
f1 is additive homogeneous & f2 is additive homogeneous implies
for b1 being OrdBasis of V1
st len b1 > 0 holds f1*b1 = f2*b1 implies f1 = f2;
registration
let D be non empty set;
cluster -> FinSequence-yielding for Matrix of D;
end;
definition
let D be non empty set;
let F,G be Matrix of D;
redefine func F^^G -> Matrix of D;
end;
definition
let D be non empty set;
let n,m,k;
let M1 be Matrix of n,k,D, M2 be Matrix of m,k,D;
redefine func M1^M2 -> Matrix of n+m,k,D;
end;
theorem :: MATRLIN:23
for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st i in dom M1 holds
Line(M1^M2,i) = Line(M1,i);
theorem :: MATRLIN:24
for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st
width M1 = width M2 holds width (M1^M2) = width M1;
theorem :: MATRLIN:25
for M1 be Matrix of t,k,D, M2 be Matrix of m,k,D st n in dom M2 & i =
len M1 + n holds Line(M1^M2,i) = Line(M2,n);
theorem :: MATRLIN:26
for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st width M1 =
width M2 for i st i in Seg width M1 holds Col(M1^M2,i) = Col(M1,i)^Col(M2,i);
theorem :: MATRLIN:27
for M1 be Matrix of n,k,the carrier of V, M2 be Matrix of m,k,
the carrier of V holds Sum(M1^M2) = (Sum M1)^(Sum M2);
theorem :: MATRLIN:28
for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st width M1 =
width M2 holds (M1^M2)@ = M1@ ^^ M2@;
theorem :: MATRLIN:29
for M1,M2 be Matrix of the carrier of V1 holds Sum M1 + Sum M2 =
Sum(M1 ^^ M2);
theorem :: MATRLIN:30
for P1,P2 be FinSequence of V1 st len P1 = len P2 holds
Sum(P1 + P2) = (Sum P1) + (Sum P2);
theorem :: MATRLIN:31
for M1,M2 be Matrix of the carrier of V1 st len M1 = len M2
holds Sum Sum M1 + Sum Sum M2 = Sum Sum(M1 ^^ M2);
theorem :: MATRLIN:32
for M be Matrix of the carrier of V1 holds Sum Sum M = Sum Sum (M@);
theorem :: MATRLIN:33
for M being Matrix of n,m,the carrier of K st n > 0 & m > 0
for p,d being FinSequence of K st len p = n & len d = m &
for j st j in dom d holds d/.j = Sum mlt(p,Col(M,j))
for b,c being FinSequence of V1 st len b = m & len c = n &
for i st i in dom c holds c/.i = Sum lmlt(Line(M,i),b) holds
Sum lmlt(p,c) = Sum lmlt(d,b);
begin :: Decomposition of a Vector in Basis
definition
let K be Field;
let V be finite-dimensional VectSp of K;
let b1 be OrdBasis of V;
let W be Element of V;
func W|--b1 -> FinSequence of K means
:: MATRLIN:def 7
len it = len b1 & ex KL be
Linear_Combination of V st W = Sum(KL) & Carrier KL c= rng b1 & for k st 1<=k &
k<=len it holds it/.k=KL.(b1/.k);
end;
theorem :: MATRLIN:34
v1|--b2 = v2|--b2 implies v1 = v2;
theorem :: MATRLIN:35
v = Sum lmlt(v|--b1,b1);
theorem :: MATRLIN:36
len d = len b1 implies d = Sum(lmlt(d,b1)) |-- b1;
theorem :: MATRLIN:37
for a,d be FinSequence of K st len a = len b1
for j be Nat st j in dom b2 & len d = len b1 &
for k st k in dom b1 holds d.k = (f.((b1/.k)) |-- b2)/.j holds
len b1 > 0 implies (Sum(lmlt(a,f*b1)) |-- b2)/.j = Sum(mlt(a,d));
begin :: Matrices of Linear Transformations
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;
func AutMt(f,b1,b2) -> Matrix of K means
:: MATRLIN:def 8
len it = len b1 & for k st k in dom b1 holds it/.k = f.(b1/.k) |-- b2;
end;
theorem :: MATRLIN:38
len b1 = 0 implies AutMt(f,b1,b2) = {};
theorem :: MATRLIN:39
len b1 > 0 implies width AutMt(f,b1,b2) = len b2;
theorem :: MATRLIN:40
f1 is additive homogeneous & f2 is additive homogeneous &
AutMt(f1,b1,b2) = AutMt(f2,b1,b2) & len b1 > 0 implies f1 = f2;
theorem :: MATRLIN:41
g is additive homogeneous & len b1 > 0 & len b2 > 0 implies
AutMt(g*f,b1,b3) = AutMt(f,b1,b2) * AutMt(g,b2,b3);
theorem :: MATRLIN:42
AutMt(f1+f2,b1,b2) = AutMt(f1,b1,b2) + AutMt(f2,b1,b2);
theorem :: MATRLIN:43
a <> 0.K implies AutMt(a*f,b1,b2) = a * AutMt(f,b1,b2);