Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### Associated Matrix of Linear Map

**by****Robert Milewski**- Received June 30, 1995
- MML identifier: MATRLIN

- [ Mizar article, MML identifier index ]

environ vocabulary FINSEQ_2, PARTFUN1, FINSEQ_4, MATRIX_1, RELAT_1, FUNCT_1, INCSP_1, FINSEQ_1, MATRIX_2, BOOLE, TREES_1, ARYTM_1, FUNCT_2, CARD_1, SUBSET_1, FUNCOP_1, MEASURE6, VECTSP_1, RLVECT_2, RLVECT_3, RLVECT_1, FINSET_1, RLSUB_1, PRE_TOPC, BINOP_1, LATTICES, QC_LANG1, SEQ_1, SQUARE_1, RVSUM_1, RLSUB_2, CAT_3, MATRLIN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, MOD_2, STRUCT_0, FINSEQ_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, MATRIX_1, MATRIX_2, MATRIX_3, FVSUM_1, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, FINSET_1, FINSEQ_4, FUNCOP_1, FINSEQ_3, CARD_1, FINSEQ_2, FINSEQOP, BINOP_1, SQUARE_1, PRE_TOPC; constructors REAL_1, NAT_1, MOD_2, FUNCT_3, MATRIX_3, FVSUM_1, VECTSP_6, VECTSP_7, FINSEQ_3, BINOP_1, SQUARE_1, TOPS_2, FINSEQ_4, MEMBERED, PARTFUN1; clusters FINSET_1, MATRIX_1, FUNCT_1, VECTSP_1, FINSEQ_3, RELSET_1, STRUCT_0, FINSEQ_1, FUNCOP_1, XREAL_0, FUNCT_2, NAT_1, MEMBERED, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: PRELIMINARIES definition let A be set; let X be set, D be FinSequence-DOMAIN of A, p be PartFunc of X,D, i be set; redefine func p/.i -> Element of D; end; reserve k,t,i,j,m,n for Nat; reserve x,y,y1,y2 for set; reserve D for non empty set; canceled; theorem :: MATRLIN:2 for p be FinSequence holds rng Del(p,i) c= rng p; definition let D be non empty set; let k; let M be Matrix of D; redefine func Del(M,k) -> Matrix of D; end; theorem :: MATRLIN:3 for M be FinSequence st len M = n+1 holds len Del(M,n+1) = n; theorem :: MATRLIN:4 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:5 for M be Matrix of n+1,m,D holds Del(M,n+1) is Matrix of n,m,D; theorem :: MATRLIN:6 for M being FinSequence st len M = n + 1 holds M = Del(M,len M) ^ <*M.(len M)*>; definition let D; let P be FinSequence of D; redefine func <*P*> -> Matrix of 1,len P,D; end; begin :: MORE ON FINITE SEQUENCE theorem :: MATRLIN:7 for A being set, F being FinSequence holds Sgm(F"A)^Sgm(F"(rng F \ A)) is Permutation of dom F; theorem :: MATRLIN:8 for F being FinSequence, A be Subset of rng F st F is one-to-one ex p being Permutation of dom F st (F-A`)^(F-A) = F*p; definition let IT be Function; attr IT is FinSequence-yielding means :: MATRLIN:def 1 for x st x in dom IT holds IT.x is FinSequence; end; definition cluster FinSequence-yielding Function; end; definition let F,G be FinSequence-yielding Function; func F^^G -> FinSequence-yielding Function means :: MATRLIN:def 2 dom it = dom F /\ dom G & for i being set st i in dom it for f,g being FinSequence st f = F.i & g = G.i holds it.i = f^g; end; begin :: CIAGI I MACIERZE DOTYCZACE PRZESTRZENI LINIOWYCH reserve K for Field; reserve V for VectSp of K; reserve a for Element of K; reserve W for Element of V; reserve KL1,KL2,KL3 for Linear_Combination of V; reserve X for Subset of V; theorem :: MATRLIN:9 X is linearly-independent & Carrier(KL1) c= X & Carrier(KL2) c= X & Sum(KL1) = Sum(KL2) implies KL1 = KL2; theorem :: MATRLIN:10 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:11 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:12 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 3 ex A being finite Subset of V st A is Basis of V; end; definition let K be Field; cluster strict finite-dimensional VectSp of K; end; definition let K be Field; let V be finite-dimensional VectSp of K; mode OrdBasis of V -> FinSequence of the carrier of V means :: MATRLIN:def 4 it is one-to-one & rng it is Basis of V; end; reserve s,p for FinSequence; reserve V1,V2,V3 for finite-dimensional VectSp of K; reserve f,f1,f2 for map of V1,V2; reserve g for map of V2,V3; reserve b1 for OrdBasis of V1; reserve b2 for OrdBasis of V2; reserve b3 for OrdBasis of V3; reserve v1,v2 for Vector of V2; reserve v,w for Element of V1; reserve p2,F for FinSequence of the carrier of V1; reserve p1,d for FinSequence of the carrier of K; reserve KL for Linear_Combination of V1; definition let K be add-associative right_zeroed right_complementable Abelian associative left_unital distributive (non empty doubleLoopStr); let V1,V2 be VectSp of K; let f1,f2 be map of V1, V2; func f1+f2 -> map of V1,V2 means :: MATRLIN:def 5 for v be Element of V1 holds it.v = f1.v + f2.v; end; definition let K; let V1,V2; let f; let a be Element of K; func a*f -> map of V1,V2 means :: MATRLIN:def 6 for v be Element of V1 holds it.v = a * (f.v); end; theorem :: MATRLIN:13 for a being Element of V1 for F being FinSequence of the carrier of V1 for G being FinSequence of the carrier 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:14 for a be Element of V1 for F being FinSequence of the carrier of K for G being FinSequence of the carrier 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:15 for V1 being add-associative right_zeroed right_complementable (non empty LoopStr) for F being FinSequence of the carrier of V1 st for k st k in dom F holds F/.k = 0.V1 holds Sum(F) = 0.V1; definition let K; let V1; let p1,p2; func lmlt(p1,p2) -> FinSequence of the carrier of V1 equals :: MATRLIN:def 7 (the lmult of V1).:(p1,p2); end; theorem :: MATRLIN:16 dom p1 = dom p2 implies dom lmlt(p1,p2) = dom p1; definition let V1 be non empty LoopStr; let M be FinSequence of (the carrier of V1)*; func Sum M -> FinSequence of the carrier of V1 means :: MATRLIN:def 8 len it = len M & for k st k in dom it holds it/.k = Sum (M/.k); end; theorem :: MATRLIN:17 for M be Matrix of the carrier of V1 st len M = 0 holds Sum Sum M = 0.V1; theorem :: MATRLIN:18 for M be Matrix of m+1,0,the carrier of V1 holds Sum Sum M = 0.V1; theorem :: MATRLIN:19 for x be Element of V1 holds <*<*x*>*> = <*<*x*>*>@; theorem :: MATRLIN:20 for p being FinSequence of the carrier of V1 st f is linear holds f.Sum(p) = Sum(f*p); theorem :: MATRLIN:21 for a be FinSequence of the carrier of K for p being FinSequence of the carrier of V1 st len p = len a holds f is linear implies f*lmlt(a,p) = lmlt(a,f*p); theorem :: MATRLIN:22 for a be FinSequence of the carrier of K st len a = len b2 holds ( g is linear implies g.Sum(lmlt(a,b2)) = Sum(lmlt(a,g*b2))); theorem :: MATRLIN:23 for F, F1 being FinSequence of the carrier 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:24 F is one-to-one & Carrier(KL) c= rng F implies Sum(KL (#) F) = Sum(KL); theorem :: MATRLIN:25 for A be set for p be FinSequence of the carrier of V1 st rng p c= A holds f1 is linear & f2 is linear & (for v st v in A holds f1.v = f2.v ) implies f1.Sum(p) = f2.Sum(p); theorem :: MATRLIN:26 f1 is linear & f2 is linear implies for b1 being OrdBasis of V1 st len b1 > 0 holds f1*b1 = f2*b1 implies f1 = f2; definition let D be non empty set; cluster -> FinSequence-yielding 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:27 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:28 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:29 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:30 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:31 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:32 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:33 for M1,M2 be Matrix of the carrier of V1 holds (the add of V1).:(Sum M1,Sum M2) = Sum(M1 ^^ M2); definition let D be non empty set, F be BinOp of D, P1,P2 be FinSequence of D; redefine func F.:(P1,P2) -> FinSequence of D; end; theorem :: MATRLIN:34 for P1,P2 be FinSequence of the carrier of V1 st len P1 = len P2 holds Sum((the add of V1).:(P1,P2)) = (Sum P1) + (Sum P2); theorem :: MATRLIN:35 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:36 for P be FinSequence of the carrier of V1 holds Sum Sum <*P*> = Sum Sum (<*P*>@); theorem :: MATRLIN:37 for M be Matrix of the carrier of V1 st len M = n holds Sum Sum M = Sum Sum (M@); theorem :: MATRLIN:38 for M being Matrix of n,m,the carrier of K st n > 0 & m > 0 for p,d being FinSequence of the carrier 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 the carrier 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 the carrier of K means :: MATRLIN:def 9 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:39 v1|--b2 = v2|--b2 implies v1 = v2; theorem :: MATRLIN:40 v = Sum lmlt(v|--b1,b1); theorem :: MATRLIN:41 len d = len b1 implies d = Sum(lmlt(d,b1))|--b1; theorem :: MATRLIN:42 for a,d be FinSequence of the carrier of K st len a = len b2 for j be Nat st j in dom b3 & len d = len b2 & for k st k in dom b2 holds d.k = (g.((b2/.k))|--b3)/.j holds len b2 > 0 implies (Sum(lmlt(a,g*b2))|--b3)/.j = Sum(mlt(a,d)); begin :: MACIERZE PRZEKSZTALCEN LINIOWYCH definition let K be Field; let V1,V2 be finite-dimensional VectSp of K; let f be Function of the carrier of V1 ,the carrier of V2; let b1 be FinSequence of the carrier of V1; let b2 be OrdBasis of V2; func AutMt(f,b1,b2) -> Matrix of K means :: MATRLIN:def 10 len it = len b1 & for k st k in dom b1 holds it/.k = f.(b1/.k)|--b2; end; theorem :: MATRLIN:43 len b1 = 0 implies AutMt(f,b1,b2) = {}; theorem :: MATRLIN:44 len b1 > 0 implies width AutMt(f,b1,b2) = len b2; theorem :: MATRLIN:45 f1 is linear & f2 is linear & AutMt(f1,b1,b2) = AutMt(f2,b1,b2) & len b1 > 0 implies f1 = f2; theorem :: MATRLIN:46 f is linear & g is linear & len b1 > 0 & len b2 > 0 & len b3 > 0 implies AutMt(g*f,b1,b3) = AutMt(f,b1,b2) * AutMt(g,b2,b3); theorem :: MATRLIN:47 AutMt(f1+f2,b1,b2) = AutMt(f1,b1,b2) + AutMt(f2,b1,b2); theorem :: MATRLIN:48 a <> 0.K implies AutMt(a*f,b1,b2) = a * AutMt(f,b1,b2);

Back to top