:: Associated Matrix of Linear Map
:: by Robert Milewski
::
:: Received June 30, 1995
:: Copyright (c) 1995-2026 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;
definitions TARSKI;
equalities FVSUM_1, FUNCOP_1, ALGSTR_0;
expansions 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, MATRIX_1;
schemes FINSEQ_1, FINSEQ_2, FUNCT_2, MATRIX_0, NAT_1, FINSEQ_4;
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; :: redefines Del (FINSEQ_3, definition)
coherence
proof
ex n st for x st x in rng Del(M,k) ex p be FinSequence of D st x = p &
len p = n
proof
consider n such that
A1: for x st x in rng M ex p be FinSequence of D st x = p & len p =
n by MATRIX_0:9;
take n;
let x such that
A2: x in rng Del(M,k);
Del(M,k) is FinSequence of D* by FINSEQ_3:105;
then rng Del(M,k) c= D* by FINSEQ_1:def 4;
then reconsider p = x as FinSequence of D by A2,FINSEQ_1:def 11;
take p;
rng Del(M,k) c= rng M by FINSEQ_3:106;
then ex p1 be FinSequence of D st x = p1 & len p1 = n by A1,A2;
hence thesis;
end;
hence thesis by MATRIX_0:9;
end;
end;
::$CT
Th1: for M be FinSequence st len M = n+1 holds len Del(M,n+1) = n
by PRE_POLY:12;
theorem Th2:
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 )
proof
let M be Matrix of n+1,m,D;
let M1 be Matrix of D;
A1: len M = n + 1 by MATRIX_0:def 2;
then n + 1 in Seg len M by FINSEQ_1:4;
then n + 1 in dom M by FINSEQ_1:def 3;
then
A2: M.(n+1) = Line(M,n+1) by MATRIX_0:60;
now
assume
A3: n > 0;
len Del(M,n+1) = n by A1,Th1;
then consider s be FinSequence such that
A4: s in rng Del(M,n+1) and
A5: len s = width Del(M,n+1) by A3,MATRIX_0:def 3;
consider n1 be Nat such that
A6: for x st x in rng M ex p be FinSequence of D st x = p & len p = n1
by MATRIX_0:9;
consider s1 be FinSequence such that
A7: s1 in rng M and
A8: len s1 = width M by A1,MATRIX_0:def 3;
A9: ex p2 be FinSequence of D st s1 = p2 & len p2 = n1 by A7,A6;
rng Del(M,n+1) c= rng M by FINSEQ_3:106;
then ex p1 be FinSequence of D st s = p1 & len p1 = n1 by A4,A6;
hence width M = width Del(M,n+1) by A5,A8,A9;
end;
hence n > 0 implies width M = width Del(M,n+1);
assume M1 = <*M.(n+1)*>;
then reconsider M2 = M1 as Matrix of 1,len(Line(M,n+1)),D by A2,MATRIX_0:11;
thus width M = len(Line(M,n+1)) by MATRIX_0:def 7
.= width M2 by MATRIX_0:23
.= width M1;
end;
theorem Th3:
for M be Matrix of n+1,m,D holds Del(M,n+1) is Matrix of n,m,D
proof
let M be Matrix of n+1,m,D;
A1: len M = n + 1 by MATRIX_0:def 2;
then
A2: len Del(M,n+1) = n by Th1;
per cases;
suppose
A3: n = 0;
then Del(M,n+1) = {} by A2;
hence thesis by A3,MATRIX_0:13;
end;
suppose
A4: n > 0;
width M = m by A1,MATRIX_0:20;
then width Del(M,n+1) = m by A4,Th2;
hence thesis by A2,A4,MATRIX_0:20;
end;
end;
::$CT
Th4:
for M being FinSequence st M <> {} holds M = Del(M,len M) ^ <*M.(len M)*>
by PRE_POLY:13;
definition
let D;
let P be FinSequence of D;
redefine func <*P*> -> Matrix of 1,len P,D; :: redefines <* (FINSEQ_1, definition)
coherence by MATRIX_0:11;
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 Th5:
X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X &
Sum KL1 = Sum KL2 implies KL1 = KL2
proof
assume that
A1: X is linearly-independent and
A2: Carrier KL1 c= X & Carrier KL2 c= X and
A3: Sum KL1 = Sum KL2;
Sum(KL1) - Sum(KL2) = 0.V by A3,VECTSP_1:19;
then
A4: KL1 - KL2 is Linear_Combination of Carrier(KL1 - KL2) & Sum(KL1 - KL2) =
0.V by VECTSP_6:7,47;
A5: Carrier(KL1 - KL2) c= Carrier(KL1) \/ Carrier(KL2) by VECTSP_6:41;
Carrier(KL1) \/ Carrier(KL2) c= X by A2,XBOOLE_1:8;
then
A6: Carrier(KL1 - KL2) is linearly-independent by A1,A5,VECTSP_7:1,XBOOLE_1:1;
now
let v be Vector of V;
not v in Carrier(KL1 - KL2) by A6,A4,VECTSP_7:def 1;
then (KL1 - KL2).v = 0.K by VECTSP_6:2;
then KL1.v - KL2.v = 0.K by VECTSP_6:40;
hence KL1.v = KL2.v by RLVECT_1:21;
end;
hence thesis by VECTSP_6:def 7;
end;
theorem Th6:
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
proof
assume that
A1: X is linearly-independent & Carrier KL1 c= X and
A2: Carrier KL2 c= X & Carrier KL3 c= X and
A3: Sum KL1 = Sum(KL2) + Sum(KL3);
Carrier(KL2 + KL3) c= Carrier(KL2) \/ Carrier(KL3) & Carrier(KL2) \/
Carrier (KL3) c= X by A2,VECTSP_6:23,XBOOLE_1:8;
then
A4: Carrier(KL2 + KL3) c= X;
Sum(KL1) = Sum(KL2 + KL3) by A3,VECTSP_6:44;
hence thesis by A1,A4,Th5;
end;
theorem Th7:
X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X
& a <> 0.K & Sum KL1 = a * Sum KL2 implies KL1 = a * KL2
proof
assume that
A1: X is linearly-independent & Carrier KL1 c= X and
A2: Carrier KL2 c= X & a <> 0.K & Sum(KL1) = a * Sum(KL2);
Carrier(a * KL2) c= X & Sum(KL1) = Sum(a * KL2) by A2,VECTSP_6:29,45;
hence thesis by A1,Th5;
end;
theorem Th8:
for b2 be Basis of V ex KL be Linear_Combination of V st W = Sum
KL & Carrier KL c= b2
proof
let b2 be Basis of V;
W in the ModuleStr of V by RLVECT_1:1;
then W in Lin b2 by VECTSP_7:def 3;
then consider KL1 being Linear_Combination of b2 such that
A1: W = Sum KL1 by VECTSP_7:7;
take KL = KL1;
thus W = Sum KL by A1;
thus thesis by VECTSP_6:def 4;
end;
definition
let K be Field;
let V be VectSp of K;
attr V is finite-dimensional means
:Def1:
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;
existence
proof
set V = the VectSp of K;
take (0).V;
thus (0).V is strict;
take A = {}(the carrier of (0).V);
Lin A = (0).(0).V by VECTSP_7:9;
then Lin A = the ModuleStr of (0).V by VECTSP_4:36;
hence thesis by VECTSP_7:def 3;
end;
end;
definition
let K be Field;
let V be finite-dimensional VectSp of K;
mode OrdBasis of V -> FinSequence of V means
:Def2:
it is one-to-one & rng it is Basis of V;
existence
proof
consider A being finite Subset of V such that
A1: A is Basis of V by Def1;
consider p be FinSequence such that
A2: rng p = A and
A3: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of V by A2,FINSEQ_1:def 4;
take f = p;
thus f is one-to-one by A3;
thus thesis by A1,A2;
end;
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
:Def3:
for v be Element of V1 holds it .v = f1.v + f2.v;
existence
proof
deffunc F(Element of V1) = f1.$1 + f2.$1;
consider F be Function of V1, V2 such that
A1: for v be Element of V1 holds F.v = F(v) from FUNCT_2:sch 4;
reconsider F as Function of V1,V2;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Function of V1,V2 such that
A2: for v be Element of V1 holds F.v = f1.v + f2.v and
A3: for v be Element of V1 holds G.v = f1.v + f2.v;
now
let v be Element of V1;
thus F.v = f1.v + f2.v by A2
.= G.v by A3;
end;
hence F = G by FUNCT_2:63;
end;
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
:Def4:
for v be Element of V1 holds it.v = a * (f.v);
existence
proof
deffunc F(Element of V1) = a * (f.$1);
consider F be Function of V1, V2 such that
A1: for v be Element of V1 holds F.v = F(v) from FUNCT_2:sch 4;
reconsider F as Function of V1,V2;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F,G be Function of V1,V2 such that
A2: for v be Element of V1 holds F.v = a * (f.v) and
A3: for v be Element of V1 holds G.v = a * (f.v);
now
let v be Element of V1;
thus F.v = a * (f.v) by A2
.= G.v by A3;
end;
hence F = G by FUNCT_2:63;
end;
end;
theorem Th9:
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
proof
let a be Element of V1;
let F be FinSequence of V1;
let G be FinSequence of K;
defpred P[Nat] means for H being FinSequence of V1, I being FinSequence of K
st len H = len I & len H = $1 & (for k for v be Element of K st k in dom H & v
= I.k holds H.k = v * a ) holds Sum(H) = Sum(I) * a;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: for H being FinSequence of V1, I being FinSequence of K st len H =
len I & len H = n & (for k for v being Element of K st k in dom H & v = I.k
holds H.k = v * a) holds Sum(H) = Sum(I) * a;
let H be FinSequence of V1, I be FinSequence of K;
assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k for v being Element of K st k in dom H & v = I.k holds H.k = v * a;
reconsider q = I | (Seg n) as FinSequence of K by FINSEQ_1:18;
reconsider p = H | (Seg n) as FinSequence of V1 by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
then
A7: len p = n by A4,FINSEQ_1:17;
A8: dom p = Seg n by A4,A6,FINSEQ_1:17;
A9: len q = n by A3,A4,A6,FINSEQ_1:17;
A10: dom q = Seg n by A3,A4,A6,FINSEQ_1:17;
A11: now
len p <= len H by A4,A6,FINSEQ_1:17;
then
A12: dom p c= dom H by FINSEQ_3:30;
let k;
let v be Element of K;
assume that
A13: k in dom p and
A14: v = q.k;
I.k = q.k by A8,A10,A13,FUNCT_1:47;
then H.k = v * a by A5,A13,A14,A12;
hence p.k = v * a by A13,FUNCT_1:47;
end;
reconsider n as Element of NAT by ORDINAL1:def 12;
n + 1 in Seg(n + 1) by FINSEQ_1:4;
then
A15: n + 1 in dom H by A4,FINSEQ_1:def 3;
then reconsider v1 = H.(n + 1) as Element of V1 by FINSEQ_2:11;
dom H = dom I by A3,FINSEQ_3:29;
then reconsider v2 = I.(n + 1) as Element of K by A15,FINSEQ_2:11;
A16: v1 = v2 * a by A5,A15;
thus Sum(H) = Sum(p) + v1 by A4,A7,A8,RLVECT_1:38
.= Sum(q) * a + v2 * a by A2,A7,A9,A11,A16
.= (Sum(q) + v2) * a by VECTSP_1:def 15
.= Sum(I) * a by A3,A4,A9,A10,RLVECT_1:38;
end;
A17: P[0]
proof
let H be FinSequence of V1, I be FinSequence of K;
assume that
A18: len H = len I and
A19: len H = 0 and
for k for v being Element of K st k in dom H & v = I.k holds H.k = v * a;
H = <*>(the carrier of V1) by A19;
then
A20: Sum(H) = 0.V1 by RLVECT_1:43;
I = <*>(the carrier of K) by A18,A19;
then Sum(I) = 0.K by RLVECT_1:43;
hence thesis by A20,VECTSP_1:14;
end;
for n holds P[n] from NAT_1:sch 2(A17,A1);
hence thesis;
end;
theorem Th10:
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
proof
let a be Element of V1;
let F be FinSequence of K;
let G be FinSequence of V1;
assume that
A1: len F = len G and
A2: for k st k in dom F holds G.k = (F/.k) * a;
now
let k;
let v be Element of K;
assume that
A3: k in dom G and
A4: v = F.k;
A5: k in dom F by A1,A3,FINSEQ_3:29;
then v = F/.k by A4,PARTFUN1:def 6;
hence G.k = v * a by A2,A5;
end;
hence thesis by A1,Th9;
end;
theorem Th11:
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
proof
let V1 be add-associative right_zeroed right_complementable non empty
addLoopStr;
let F be FinSequence of V1;
assume
A1: for k st k in dom F holds F/.k = 0.V1;
defpred P[FinSequence of V1] means (( for k st k in dom $1 holds $1/.k = 0.
V1) implies Sum($1) = 0.V1 );
A2: for p being FinSequence of V1, x being Element of V1 holds P[p] implies
P[p^<*x*>]
proof
let p be FinSequence of V1;
let x be Element of V1;
assume
A3: (for k st k in dom p holds p/.k = 0.V1) implies Sum(p) = 0.V1;
A4: len p + 1 in Seg (len p + 1) by FINSEQ_1:4;
assume
A5: for k st k in dom(p^<*x*>) holds (p^<*x*>)/.k = 0.V1;
A6: for k st k in dom p holds p/.k = 0.V1
proof
A7: dom p c= dom(p^<*x*>) by FINSEQ_1:26;
let k such that
A8: k in dom p;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
thus p/.k = p.k by A8,PARTFUN1:def 6
.= (p^<*x*>).k1 by A8,FINSEQ_1:def 7
.= (p^<*x*>)/.k by A8,A7,PARTFUN1:def 6
.= 0.V1 by A5,A8,A7;
end;
len(p^<*x*>) = len p + len<*x*> by FINSEQ_1:22
.= len p + 1 by FINSEQ_1:39;
then
A9: len p + 1 in dom(p^<*x*>) by A4,FINSEQ_1:def 3;
A10: x = (p^<*x*>).(len p + 1) by FINSEQ_1:42;
thus Sum(p^<*x*>) = Sum(p) + Sum(<*x*>) by RLVECT_1:41
.= Sum(p) + x by RLVECT_1:44
.= Sum(p) + (p^<*x*>)/.(len p + 1) by A9,A10,PARTFUN1:def 6
.= 0.V1 + 0.V1 by A3,A5,A6,A9
.= 0.V1 by RLVECT_1:def 4;
end;
A11: P[<*>the carrier of V1] by RLVECT_1:43;
for p being FinSequence of V1 holds P[p] from FINSEQ_2:sch 2(A11,A2 );
hence thesis by A1;
end;
definition
let K, V1, p1,p2;
func lmlt(p1,p2) -> FinSequence of V1 equals
(the lmult of V1).:(p1,p2);
coherence;
end;
theorem Th12:
dom p1 = dom p2 implies dom lmlt(p1,p2) = dom p1
proof
assume
A1: dom p1 = dom p2;
rng p1 c= the carrier of K & rng p2 c= the carrier of V1 by FINSEQ_1:def 4;
then
A2: [:rng p1,rng p2:] c= [:the carrier of K,the carrier of V1:] by ZFMISC_1:96;
rng <:p1,p2:> c= [:rng p1,rng p2:] & [:the carrier of K,the carrier of
V1:] = dom (the lmult of V1) by FUNCT_2:def 1,FUNCT_3:51;
hence dom lmlt(p1,p2) = dom <:p1,p2:> by A2,RELAT_1:27,XBOOLE_1:1
.= dom p1 /\ dom p2 by FUNCT_3:def 7
.= dom p1 by A1;
end;
definition
let V1 be non empty addLoopStr, M be FinSequence of (the carrier of V1)*;
func Sum M -> FinSequence of V1 means
:Def6:
len it = len M & for k st k in dom it
holds it/.k = Sum (M/.k);
existence
proof
deffunc F(Nat) = Sum (M/.$1);
consider F being FinSequence of V1 such that
A1: len F = len M & for k be Nat st k in dom F holds F.k = F(k) from
FINSEQ_2:sch 1;
take F;
thus len F = len M by A1;
hereby
let k;
assume
A2: k in dom F;
hence F/.k = F.k by PARTFUN1:def 6
.= Sum (M/.k) by A1,A2;
end;
end;
uniqueness
proof
let F1,F2 be FinSequence of V1 such that
A3: len F1 = len M and
A4: for k st k in dom F1 holds F1/.k = Sum (M/.k) and
A5: len F2 = len M and
A6: for k st k in dom F2 holds F2/.k = Sum (M/.k);
A7: dom F1 = Seg len F1 by FINSEQ_1:def 3;
now
let k be Nat;
assume
A8: k in dom F1;
then
A9: k in dom F2 by A3,A5,A7,FINSEQ_1:def 3;
thus F1.k = F1/.k by A8,PARTFUN1:def 6
.= Sum (M/.k) by A4,A8
.= F2/.k by A6,A9
.= F2.k by A9,PARTFUN1:def 6;
end;
hence thesis by A3,A5,FINSEQ_2:9;
end;
end;
theorem Th13:
for M be Matrix of the carrier of V1 st len M = 0 holds Sum Sum M = 0.V1
proof
let M be Matrix of the carrier of V1;
assume len M = 0;
then len Sum M = 0 by Def6;
then Sum M = <*>(the carrier of V1);
hence thesis by RLVECT_1:43;
end;
theorem Th14:
for M be Matrix of m+1,0,the carrier of V1 holds Sum Sum M = 0.V1
proof
let M be Matrix of m+1,0,the carrier of V1;
for k st k in dom Sum M holds (Sum M)/.k = 0.V1
proof
let k such that
A1: k in dom Sum M;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
len M = len Sum M by Def6;
then dom M = dom Sum M by FINSEQ_3:29;
then M/.k1 in rng M by A1,PARTFUN2:2;
then len(M/.k) = 0 by MATRIX_0:def 2;
then
A2: M/.k = <*>(the carrier of V1);
thus (Sum M)/.k = Sum (M/.k) by A1,Def6
.= 0.V1 by A2,RLVECT_1:43;
end;
hence thesis by Th11;
end;
theorem Th15:
for x be Element of D holds <*<*x*>*> = <*<*x*>*>@
proof
let x be Element of D;
set P = <*<*x*>*>, R = (<*<*x*>*>@);
A1: len P = 1 by FINSEQ_1:40;
then
A2: width P = len <*x*> by MATRIX_0:20
.= 1 by FINSEQ_1:40;
then
A3: len R = 1 by MATRIX_0:54;
A4: now
let i,j;
assume
A5: [i,j] in Indices P;
then
A6: [i,j] in [:dom P,Seg 1:] by A2,MATRIX_0:def 4;
then i in dom P by ZFMISC_1:87;
then i in Seg 1 by A1,FINSEQ_1:def 3;
then
A7: i = 1 by FINSEQ_1:2,TARSKI:def 1;
j in Seg 1 by A6,ZFMISC_1:87;
then j = 1 by FINSEQ_1:2,TARSKI:def 1;
hence P*(i,j) = R*(i,j) by A5,A7,MATRIX_0:def 6;
end;
width R = 1 by A1,A2,MATRIX_0:54;
hence thesis by A1,A2,A3,A4,MATRIX_0:21;
end;
theorem Th16:
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)
proof
let V1,V2 be VectSp of K, f be Function of V1,V2;
let p be FinSequence of V1;
defpred P[FinSequence of V1] means f.Sum($1) = Sum(f*$1);
assume
A1: f is additive homogeneous;
A2: for p being FinSequence of V1 for w being Element of V1 st P[p] holds P[
p^<*w*>]
proof
let p be FinSequence of V1;
let w be Element of V1 such that
A3: f.Sum p = Sum (f*p);
thus f.Sum(p^<*w*>) = f.(Sum(p) + Sum<*w*>) by RLVECT_1:41
.= Sum(f*p) + f.Sum<*w*> by A1,A3,VECTSP_1:def 20
.= Sum(f*p) + f.w by RLVECT_1:44
.= Sum(f*p) + Sum<*f.w*> by RLVECT_1:44
.= Sum(f*p^<*f.w*>) by RLVECT_1:41
.= Sum(f*(p^<*w*>)) by FINSEQOP:8;
end;
f.Sum(<*>(the carrier of V1)) = f.(0.V1) by RLVECT_1:43
.= f.(0.K*0.V1) by VECTSP_1:14
.= 0.K*f.(0.V1) by A1,MOD_2:def 2
.= 0.V2 by VECTSP_1:14
.= Sum(<*>(the carrier of V2)) by RLVECT_1:43
.= Sum(f*<*>(the carrier of V1));
then
A4: P[<*>(the carrier of V1)];
for p being FinSequence of V1 holds P[p] from FINSEQ_2:sch 2(A4,A2 );
hence thesis;
end;
theorem Th17:
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)
proof
let a be FinSequence of K, p be FinSequence of V1;
assume len p = len a;
then
A1: dom p = dom a by FINSEQ_3:29;
dom f = the carrier of V1 by FUNCT_2:def 1;
then rng p c= dom f by FINSEQ_1:def 4;
then
A2: dom p = dom (f*p) by RELAT_1:27;
assume
A3: f is additive homogeneous;
A4: now
set P = f*p;
let k be Nat;
assume
A5: k in dom (f*lmlt(a,p));
A6: dom (f*lmlt(a,p)) c= dom lmlt(a,p) by RELAT_1:25;
then k in dom lmlt(a,p) by A5;
then
A7: k in dom p by A1,Th12;
then
A8: p/.k = p.k by PARTFUN1:def 6;
A9: k in dom lmlt(a,f*p) by A1,A2,A7,Th12;
A10: a/.k = a.k by A1,A7,PARTFUN1:def 6;
A11: P/.k = (f*p).k by A2,A7,PARTFUN1:def 6;
thus (f*lmlt(a,p)).k = f.(lmlt(a,p).k) by A5,FUNCT_1:12
.= f.((the lmult of V1).(a.k,p.k)) by A5,A6,FUNCOP_1:22
.= f.((a/.k)*(p/.k)) by A10,A8,VECTSP_1:def 12
.= (a/.k)*(f.(p/.k)) by A3,MOD_2:def 2
.= (a/.k)*(P/.k) by A7,A8,A11,FUNCT_1:13
.= (the lmult of V2).(a.k,(f*p).k) by A10,A11,VECTSP_1:def 12
.= lmlt(a,f*p).k by A9,FUNCOP_1:22;
end;
dom lmlt(a,p) = dom p by A1,Th12
.= dom lmlt(a,f*p) by A1,A2,Th12;
then len lmlt(a,p) = len lmlt(a,f*p) by FINSEQ_3:29;
then len (f*lmlt(a,p)) = len lmlt(a,f*p) by FINSEQ_2:33;
hence thesis by A4,FINSEQ_2:9;
end;
theorem Th18:
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))
proof
let a be FinSequence of K such that
A1: len a = len b2 and
A2: g is additive homogeneous;
thus g.Sum(lmlt(a,b2)) = Sum(g*lmlt(a,b2)) by A2,Th16
.= Sum(lmlt(a,g*b2)) by A1,A2,Th17;
end;
theorem Th19:
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
proof
let F, F1 be FinSequence of V1;
let KL be Linear_Combination of V1;
let p be Permutation of dom F such that
A1: F1 = F * p;
dom F = Seg len F by FINSEQ_1:def 3;
then dom F = Seg len (KL (#) F) by VECTSP_6:def 5;
then
A2: dom F = dom (KL (#) F) by FINSEQ_1:def 3;
then reconsider F2 = (KL (#) F) * p as FinSequence of V1 by FINSEQ_2:47;
len (KL (#) F1) = len F1 by VECTSP_6:def 5
.= len F by A1,FINSEQ_2:44
.= len (KL (#) F) by VECTSP_6:def 5
.= len F2 by A2,FINSEQ_2:44;
then
A3: dom (KL (#) F1) = dom ((KL (#) F) * p) by FINSEQ_3:29;
len (KL (#) F1) = len F1 by VECTSP_6:def 5;
then
A4: dom (KL (#) F1) = dom F1 by FINSEQ_3:29;
now
let k be Nat;
reconsider k0=k as Element of NAT by ORDINAL1:def 12;
assume
A5: k in dom (KL (#) F1);
then k in dom p by A3,FUNCT_1:11;
then p.k in rng p by FUNCT_1:def 3;
then
A6: p.k in dom F by FUNCT_2:def 3;
then reconsider k1 = p.k0 as Element of NAT by FINSEQ_3:23;
F1/.k = F1.k by A4,A5,PARTFUN1:def 6
.= F.(p.k) by A1,A4,A5,FUNCT_1:12
.= F/.(p.k) by A6,PARTFUN1:def 6;
hence (KL (#) F1).k = KL.(F/.k1) * (F/.k1) by A5,VECTSP_6:def 5
.= (KL (#) F).k1 by A2,A6,VECTSP_6:def 5
.= F2.k by A3,A5,FUNCT_1:12;
end;
hence thesis by A3,FINSEQ_1:13;
end;
theorem Th20:
F is one-to-one & Carrier KL c= rng F implies Sum(KL (#) F) = Sum KL
proof
assume
A1: F is one-to-one;
assume
A2: Carrier KL c= rng F;
then reconsider A = Carrier KL as Subset of rng F;
consider p1 being Permutation of dom F such that
A3: (F-A`)^(F-A) = F * p1 by FINSEQ_3:115;
reconsider G1 = F - A`, G2 = F - A as FinSequence of V1 by FINSEQ_3:86;
A4: G1 is one-to-one by A1,FINSEQ_3:87;
len (KL (#) F) = len F by VECTSP_6:def 5;
then dom (KL (#) F) = dom F by FINSEQ_3:29;
then reconsider p1 as Permutation of dom (KL (#) F);
A5: rng G1 = rng F \ A` by FINSEQ_3:65
.= rng F \ ((rng F) \ Carrier KL) by SUBSET_1:def 4
.= rng F /\ Carrier KL by XBOOLE_1:48
.= Carrier KL by A2,XBOOLE_1:28;
for k st k in dom (KL (#) G2) holds (KL (#) G2)/.k = 0.V1
proof
let k such that
A6: k in dom (KL (#) G2);
len (KL (#) G2) = len G2 by VECTSP_6:def 5;
then
A7: dom (KL (#) G2) = dom G2 by FINSEQ_3:29;
then G2.k in rng G2 by A6,FUNCT_1:def 3;
then G2.k in rng F \ Carrier KL by FINSEQ_3:65;
then not G2.k in Carrier KL by XBOOLE_0:def 5;
then
A8: not G2/.k in Carrier KL by A6,A7,PARTFUN1:def 6;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
thus (KL (#) G2)/.k = (KL (#) G2).k by A6,PARTFUN1:def 6
.= KL.(G2/.k1) * (G2/.k1) by A6,VECTSP_6:def 5
.= 0.K * (G2/.k) by A8,VECTSP_6:2
.= 0.V1 by VECTSP_1:14;
end;
then
A9: Sum(KL (#) G2) = 0.V1 by Th11;
KL (#) (G1^G2) = (KL (#) F) * p1 by A3,Th19;
hence Sum(KL (#) F) = Sum(KL (#) (G1 ^ G2)) by RLVECT_2:7
.= Sum((KL (#) G1) ^ (KL (#) G2)) by VECTSP_6:13
.= Sum(KL (#) G1) + Sum(KL (#) G2) by RLVECT_1:41
.= Sum(KL) + 0.V1 by A4,A5,A9,VECTSP_6:def 6
.= Sum KL by RLVECT_1:4;
end;
theorem Th21:
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
proof
let A be set;
let p be FinSequence of V1 such that
A1: rng p c= A;
defpred P[FinSequence of V1] means rng $1 c= A implies f1.Sum($1) = f2.Sum(
$1);
assume
A2: f1 is additive homogeneous;
assume
A3: f2 is additive homogeneous;
assume
A4: for v st v in A holds f1.v = f2.v;
A5: for p being FinSequence of V1, x being Element of V1 st P[p]holds P[p^<*
x*>]
proof
let p be FinSequence of V1, x be Element of V1 such that
A6: rng p c= A implies f1.Sum p = f2.Sum p;
A7: rng p c= rng p \/ rng <*x*> by XBOOLE_1:7;
assume rng (p^<*x*>) c= A;
then
A8: rng p \/ rng <*x*> c= A by FINSEQ_1:31;
rng <*x*> c= rng p \/ rng <*x*> by XBOOLE_1:7;
then rng <*x*> c= A by A8;
then {x} c= A by FINSEQ_1:39;
then
A9: x in A by ZFMISC_1:31;
thus f1.Sum(p^<*x*>) = f1.(Sum(p) + Sum(<*x*>)) by RLVECT_1:41
.= f2.(Sum p) + f1.(Sum(<*x*>)) by A2,A6,A8,A7,VECTSP_1:def 20
.= f2.(Sum p) + f1.x by RLVECT_1:44
.= f2.(Sum p) + f2.x by A4,A9
.= f2.(Sum p) + f2.(Sum(<*x*>)) by RLVECT_1:44
.= f2.(Sum(p) + Sum(<*x*>)) by A3,VECTSP_1:def 20
.= f2.Sum(p^<*x*>) by RLVECT_1:41;
end;
A10: P[<*>(the carrier of V1)]
proof
assume rng<*>(the carrier of V1) c= A;
thus f1.Sum(<*>(the carrier of V1)) = f1.(0.V1) by RLVECT_1:43
.= f1.(0.K*0.V1) by VECTSP_1:14
.= 0.K*f1.(0.V1) by A2,MOD_2:def 2
.= 0.V2 by VECTSP_1:14
.= 0.K*f2.(0.V1) by VECTSP_1:14
.= f2.(0.K*0.V1) by A3,MOD_2:def 2
.= f2.(0.V1) by VECTSP_1:14
.= f2.Sum(<*>(the carrier of V1)) by RLVECT_1:43;
end;
for p being FinSequence of V1 holds P[p] from FINSEQ_2:sch 2(A10,A5 );
hence thesis by A1;
end;
theorem Th22:
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
proof
assume that
A1: f1 is additive homogeneous and
A2: f2 is additive homogeneous;
let b1 be OrdBasis of V1 such that
A3: len b1 > 0;
reconsider b = rng b1 as Basis of V1 by Def2;
assume
A4: f1*b1 = f2*b1;
now
len b1 in Seg len b1 by A3,FINSEQ_1:3;
then reconsider D = dom b1 as non empty set by FINSEQ_1:def 3;
let v be Element of V1;
Lin(b) = the ModuleStr of V1 by VECTSP_7:def 3;
then v in Lin(b) by RLVECT_1:1;
then consider KL be Linear_Combination of b such that
A5: v = Sum(KL) by VECTSP_7:7;
set p = KL (#) b1;
set A = the set of all KL.(b1/.i)*(b1/.i) where i is Element of D ;
A6: rng p c= A
proof
let x be object;
assume x in rng p;
then consider i be Nat such that
A7: i in dom p and
A8: p.i = x by FINSEQ_2:10;
dom p = Seg len p by FINSEQ_1:def 3;
then i in Seg len b1 by A7,VECTSP_6:def 5;
then
A9: i in dom b1 by FINSEQ_1:def 3;
(KL (#) b1).i = KL.(b1/.i) * (b1/.i) by A7,VECTSP_6:def 5;
hence thesis by A8,A9;
end;
A10: for w st w in A holds f1.w = f2.w
proof
let w;
assume w in A;
then consider i be Element of D such that
A11: w = KL.(b1/.i)*(b1/.i);
f1.(b1/.i) = f1.(b1.i) by PARTFUN1:def 6
.= (f2*b1).i by A4,FUNCT_1:13
.= f2.(b1.i) by FUNCT_1:13
.= f2.(b1/.i) by PARTFUN1:def 6;
then f1.(KL.(b1/.i)*(b1/.i)) = KL.(b1/.i)*(f2.(b1/.i)) by A1,MOD_2:def 2
.= f2.(KL.(b1/.i)*(b1/.i)) by A2,MOD_2:def 2;
hence thesis by A11;
end;
A12: b1 is one-to-one & Carrier KL c= rng b1 by Def2,VECTSP_6:def 4;
hence f1.v = f1.Sum(KL (#) b1) by A5,Th20
.= f2.Sum p by A1,A2,A6,A10,Th21
.= f2.v by A5,A12,Th20;
end;
hence thesis by FUNCT_2:63;
end;
registration
let D be non empty set;
cluster -> FinSequence-yielding for Matrix of D;
coherence;
end;
definition
let D be non empty set;
let F,G be Matrix of D;
redefine func F^^G -> Matrix of D; :: redefines ^^ (PRE_POLY, definition)
coherence
proof
reconsider M = F^^G as FinSequence;
ex n st for x st x in rng M ex p be FinSequence of D st x = p & len p = n
proof
take n = width F + width G;
let x;
A1: rng F c= D* & rng G c= D* by FINSEQ_1:def 4;
assume x in rng M;
then consider y being object such that
A2: y in dom M and
A3: x = M.y by FUNCT_1:def 3;
A4: dom M = dom F /\ dom G by PRE_POLY:def 4;
then
A5: y in dom G by A2,XBOOLE_0:def 4;
then
A6: G.y in rng G by FUNCT_1:def 3;
A7: y in dom F by A2,A4,XBOOLE_0:def 4;
then F.y in rng F by FUNCT_1:def 3;
then reconsider f = F.y, g = G.y as FinSequence of D by A6,A1,
FINSEQ_1:def 11;
reconsider y as Nat by A2,FINSEQ_3:23;
A8: G.y = Line(G,y) by A5,MATRIX_0:60;
A9: x = f ^ g by A2,A3,PRE_POLY:def 4;
then reconsider p = x as FinSequence of D;
take p;
thus x = p;
F.y = Line(F,y) by A7,MATRIX_0:60;
hence len p = len Line(F,y) + len Line(G,y) by A9,A8,FINSEQ_1:22
.= width F + len Line(G,y) by MATRIX_0:def 7
.= n by MATRIX_0:def 7;
end;
hence thesis by MATRIX_0:9;
end;
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; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
per cases;
suppose
A1: n = 0;
then len M1 = 0 by MATRIX_0:def 2;
then M1 = {};
hence thesis by A1,FINSEQ_1:34;
end;
suppose
A2: m = 0;
then len M2 = 0 by MATRIX_0:def 2;
then M2 = {};
hence thesis by A2,FINSEQ_1:34;
end;
suppose that
A3: n <> 0 and
A4: m <> 0;
len M2 = m by MATRIX_0:def 2;
then
A5: width M2 = k by A4,MATRIX_0:20;
len M1 = n by MATRIX_0:def 2;
then
A6: width M1 = k by A3,MATRIX_0:20;
ex n st for x st x in rng (M1^M2) ex p be FinSequence of D st x = p
& len p = n
proof
take k;
let x such that
A7: x in rng (M1^M2);
rng (M1^M2) c= D* by FINSEQ_1:def 4;
then reconsider p = x as FinSequence of D by A7,FINSEQ_1:def 11;
take p;
A8: x in rng M1 \/ rng M2 by A7,FINSEQ_1:31;
now
per cases by A8,XBOOLE_0:def 3;
suppose
x in rng M1;
then consider y1 being object such that
A9: y1 in dom M1 and
A10: x = M1.y1 by FUNCT_1:def 3;
reconsider y1 as Nat by A9,FINSEQ_3:23;
x = Line(M1,y1) by A9,A10,MATRIX_0:60;
hence len p = k by A6,MATRIX_0:def 7;
end;
suppose
x in rng M2;
then consider y2 being object such that
A11: y2 in dom M2 and
A12: x = M2.y2 by FUNCT_1:def 3;
reconsider y2 as Nat by A11,FINSEQ_3:23;
x = Line(M2,y2) by A11,A12,MATRIX_0:60;
hence len p = k by A5,MATRIX_0:def 7;
end;
end;
hence thesis;
end;
then reconsider M3 = M1^M2 as Matrix of D by MATRIX_0:9;
len M1 = n & len M2 = m by MATRIX_0:def 2;
then
A13: len M3 = n + m by FINSEQ_1:22;
then consider s be FinSequence such that
A14: s in rng M3 and
A15: len s = width M3 by A3,MATRIX_0:def 3;
A16: s in rng M1 \/ rng M2 by A14,FINSEQ_1:31;
now
per cases by A16,XBOOLE_0:def 3;
suppose
s in rng M1;
then consider y1 being object such that
A17: y1 in dom M1 and
A18: s = M1.y1 by FUNCT_1:def 3;
reconsider y1 as Nat by A17,FINSEQ_3:23;
s = Line(M1,y1) by A17,A18,MATRIX_0:60;
hence width M3 = k by A6,A15,MATRIX_0:def 7;
end;
suppose
s in rng M2;
then consider y2 being object such that
A19: y2 in dom M2 and
A20: s = M2.y2 by FUNCT_1:def 3;
reconsider y2 as Nat by A19,FINSEQ_3:23;
s = Line(M2,y2) by A19,A20,MATRIX_0:60;
hence width M3 = k by A5,A15,MATRIX_0:def 7;
end;
end;
hence thesis by A3,A13,MATRIX_0:20;
end;
end;
end;
theorem
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)
proof
let M1 be Matrix of n,k,D;
let M2 be Matrix of m,k,D such that
A1: i in dom M1;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
dom M1 c= dom (M1^M2) by FINSEQ_1:26;
hence Line(M1^M2,i) = (M1^M2).i by A1,MATRIX_0:60
.= M1.i1 by A1,FINSEQ_1:def 7
.= Line(M1,i) by A1,MATRIX_0:60;
end;
theorem Th24:
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
proof
let M1 be Matrix of n,k,D;
let M2 be Matrix of m,k,D such that
A1: width M1 = width M2;
consider n such that
A2: for x st x in rng (M1^M2) ex P be FinSequence of D st x = P & len P
= n by MATRIX_0:9;
per cases;
suppose
A3: len (M1^M2) = 0;
then len M1 + len M2 = 0 by FINSEQ_1:22;
then
A4: len M1 = 0;
width (M1^M2) = 0 by A3,MATRIX_0:def 3
.= width M1 by A4,MATRIX_0:def 3;
hence thesis;
end;
suppose
A5: len (M1^M2) > 0;
then
A6: len M1 + len M2 > 0+0 by FINSEQ_1:22;
consider s be FinSequence such that
A7: s in rng (M1^M2) and
A8: len s = width (M1^M2) by A5,MATRIX_0:def 3;
A9: ex P be FinSequence of D st s = P & len P = n by A2,A7;
per cases by A6;
suppose
len M1 > 0;
then consider s1 be FinSequence such that
A10: s1 in rng M1 and
A11: len s1 = width M1 by MATRIX_0:def 3;
rng M1 c= rng (M1^M2) by FINSEQ_1:29;
then ex P1 be FinSequence of D st s1 = P1 & len P1 = n by A2,A10;
hence thesis by A8,A9,A11;
end;
suppose
len M2 > 0;
then consider s2 be FinSequence such that
A12: s2 in rng M2 and
A13: len s2 = width M2 by MATRIX_0:def 3;
rng M2 c= rng (M1^M2) by FINSEQ_1:30;
then ex P2 be FinSequence of D st s2 = P2 & len P2 = n by A2,A12;
hence thesis by A1,A8,A9,A13;
end;
end;
end;
theorem
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)
proof
let M1 be Matrix of t,k,D;
let M2 be Matrix of m,k,D;
assume that
A1: n in dom M2 and
A2: i = len M1 + n;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
i in dom (M1^M2) by A1,A2,FINSEQ_1:28;
hence Line(M1^M2,i) = (M1^M2).i by MATRIX_0:60
.= M2.n1 by A1,A2,FINSEQ_1:def 7
.= Line(M2,n) by A1,MATRIX_0:60;
end;
theorem Th26:
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)
proof
let M1 be Matrix of n,k,D;
let M2 be Matrix of m,k,D such that
A1: width M1 = width M2;
let i such that
A2: i in Seg width M1;
A3: dom Col(M1^M2,i) = Seg len Col(M1^M2,i) by FINSEQ_1:def 3;
A4: len Col(M1^M2,i) = len (M1^M2) by MATRIX_0:def 8
.= len M1 + len M2 by FINSEQ_1:22
.= len M1 + len Col(M2,i) by MATRIX_0:def 8
.= len Col(M1,i) + len Col(M2,i) by MATRIX_0:def 8
.= len (Col(M1,i)^Col(M2,i)) by FINSEQ_1:22;
now
let j be Nat;
assume
A5: j in dom Col(M1^M2,i);
then j in Seg len (M1^M2) by A3,MATRIX_0:def 8;
then
A6: j in dom (M1^M2) by FINSEQ_1:def 3;
i in Seg width (M1^M2) by A1,A2,Th24;
then [j,i] in [:dom(M1^M2),Seg width(M1^M2):] by A6,ZFMISC_1:87;
then [j,i] in Indices (M1^M2) by MATRIX_0:def 4;
then consider P be FinSequence of D such that
A7: P = (M1^M2).j and
A8: (M1^M2)*(j,i) = P.i by MATRIX_0:def 5;
A9: j in dom (Col(M1,i)^Col(M2,i)) by A4,A3,A5,FINSEQ_1:def 3;
now
per cases by A9,FINSEQ_1:25;
suppose
A10: j in dom Col(M1,i);
then j in Seg len Col(M1,i) by FINSEQ_1:def 3;
then j in Seg len M1 by MATRIX_0:def 8;
then
A11: j in dom M1 by FINSEQ_1:def 3;
then [j,i] in [:dom M1,Seg width M1:] by A2,ZFMISC_1:87;
then [j,i] in Indices M1 by MATRIX_0:def 4;
then consider P1 be FinSequence of D such that
A12: P1 = M1.j and
A13: M1*(j,i) = P1.i by MATRIX_0:def 5;
P = P1 by A7,A11,A12,FINSEQ_1:def 7;
hence Col(M1^M2,i).j = M1*(j,i) by A6,A8,A13,MATRIX_0:def 8
.= Col(M1,i).j by A11,MATRIX_0:def 8
.= (Col(M1,i)^Col(M2,i)).j by A10,FINSEQ_1:def 7;
end;
suppose
ex n be Nat st n in dom Col(M2,i) & j = len Col(M1,i) + n;
then consider n be Nat such that
A14: n in dom Col(M2,i) and
A15: j = len Col(M1,i) + n;
n in Seg len Col(M2,i) by A14,FINSEQ_1:def 3;
then n in Seg len M2 by MATRIX_0:def 8;
then
A16: n in dom M2 by FINSEQ_1:def 3;
then [n,i] in [:dom M2,Seg width M2:] by A1,A2,ZFMISC_1:87;
then [n,i] in Indices M2 by MATRIX_0:def 4;
then consider P2 be FinSequence of D such that
A17: P2 = M2.n and
A18: M2*(n,i) = P2.i by MATRIX_0:def 5;
len Col(M2,i) = len M2 by MATRIX_0:def 8;
then len Col(M1,i) = len M1 & dom Col(M2,i) = dom M2 by FINSEQ_3:29
,MATRIX_0:def 8;
then P = P2 by A7,A14,A15,A17,FINSEQ_1:def 7;
hence Col(M1^M2,i).j = M2*(n,i) by A6,A8,A18,MATRIX_0:def 8
.= Col(M2,i).n by A16,MATRIX_0:def 8
.= (Col(M1,i)^Col(M2,i)).j by A14,A15,FINSEQ_1:def 7;
end;
end;
hence Col(M1^M2,i).j = (Col(M1,i)^Col(M2,i)).j;
end;
hence thesis by A4,FINSEQ_2:9;
end;
theorem Th27:
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)
proof
let M1 be Matrix of n,k,the carrier of V;
let M2 be Matrix of m,k,the carrier of V;
A1: dom Sum(M1^M2) = Seg len Sum(M1^M2) by FINSEQ_1:def 3;
A2: now
let i be Nat;
assume
A3: i in dom Sum(M1^M2);
then i in Seg len (M1^M2) by A1,Def6;
then
A4: i in dom (M1^M2) by FINSEQ_1:def 3;
now
per cases by A4,FINSEQ_1:25;
suppose
A5: i in dom M1;
len M1 = len Sum M1 by Def6;
then
A6: dom M1 = dom Sum M1 by FINSEQ_3:29;
thus Sum(M1^M2).i = (Sum(M1^M2))/.i by A3,PARTFUN1:def 6
.= Sum ((M1^M2)/.i) by A3,Def6
.= Sum (M1/.i) by A5,FINSEQ_4:68
.= (Sum M1)/.i by A5,A6,Def6
.= (Sum M1).i by A5,A6,PARTFUN1:def 6
.= ((Sum M1)^(Sum M2)).i by A5,A6,FINSEQ_1:def 7;
end;
suppose
A7: ex n be Nat st n in dom M2 & i = len M1 + n;
A8: len M1 = len Sum M1 by Def6;
len M2 = len Sum M2 by Def6;
then
A9: dom M2 = dom Sum M2 by FINSEQ_3:29;
consider n be Nat such that
A10: n in dom M2 and
A11: i = len M1 + n by A7;
thus Sum(M1^M2).i = (Sum(M1^M2))/.i by A3,PARTFUN1:def 6
.= Sum ((M1^M2)/.i) by A3,Def6
.= Sum (M2/.n) by A10,A11,FINSEQ_4:69
.= (Sum M2)/.n by A10,A9,Def6
.= (Sum M2).n by A10,A9,PARTFUN1:def 6
.= ((Sum M1)^(Sum M2)).i by A10,A11,A8,A9,FINSEQ_1:def 7;
end;
end;
hence Sum(M1^M2).i = ((Sum M1)^(Sum M2)).i;
end;
len Sum(M1^M2) = len (M1^M2) by Def6
.= len M1 + len M2 by FINSEQ_1:22
.= len Sum M1 + len M2 by Def6
.= len Sum M1 + len Sum M2 by Def6
.= len ((Sum M1)^(Sum M2)) by FINSEQ_1:22;
hence thesis by A2,FINSEQ_2:9;
end;
theorem Th28:
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@
proof
let M1 be Matrix of n,k,D;
let M2 be Matrix of m,k,D such that
A1: width M1 = width M2;
A2: Seg len (M1@ ^^ M2@) = dom (M1@ ^^ M2@) by FINSEQ_1:def 3
.= dom (M1@) /\ dom (M2@) by PRE_POLY:def 4
.= dom (M1@) /\ Seg len (M2@) by FINSEQ_1:def 3
.= Seg len (M1@) /\ Seg len (M2@) by FINSEQ_1:def 3
.= Seg width M1 /\ Seg len (M2@) by MATRIX_0:def 6
.= Seg width M1 /\ Seg width M2 by MATRIX_0:def 6
.= Seg width M1 by A1;
A3: dom ((M1^M2)@) = Seg len ((M1^M2)@) by FINSEQ_1:def 3;
A4: len ((M1^M2)@) = width (M1^M2) by MATRIX_0:def 6
.= width M1 by A1,Th24
.= len (M1@ ^^ M2@) by A2,FINSEQ_1:6;
now
let i be Nat;
assume
A5: i in dom ((M1^M2)@);
then
A6: i in Seg width (M1^M2) by A3,MATRIX_0:def 6;
A7: i in dom (M1@ ^^ M2@) by A4,A3,A5,FINSEQ_1:def 3;
then
A8: i in dom (M1@) /\ dom (M2@) by PRE_POLY:def 4;
then
A9: i in dom (M2@) by XBOOLE_0:def 4;
A10: i in dom (M1@) by A8,XBOOLE_0:def 4;
reconsider m1 = M1@.i,m2 = M2@.i as FinSequence;
i in Seg len (M1@) /\ dom (M2@) by A8,FINSEQ_1:def 3;
then i in Seg len (M1@) /\ Seg len (M2@) by FINSEQ_1:def 3;
then i in Seg width M1 /\ Seg len (M2@) by MATRIX_0:def 6;
then
A11: i in Seg width M1 /\ Seg width M2 by MATRIX_0:def 6;
thus (M1^M2)@.i = Line((M1^M2)@,i) by A5,MATRIX_0:60
.= Col(M1^M2,i) by A6,MATRIX_0:59
.= Col(M1,i)^Col(M2,i) by A1,A11,Th26
.= Line(M1@,i)^Col(M2,i) by A1,A11,MATRIX_0:59
.= Line(M1@,i)^Line(M2@,i) by A1,A11,MATRIX_0:59
.= Line(M1@,i)^m2 by A9,MATRIX_0:60
.= m1^m2 by A10,MATRIX_0:60
.= (M1@ ^^ M2@).i by A7,PRE_POLY:def 4;
end;
hence thesis by A4,FINSEQ_2:9;
end;
theorem Th29:
for M1,M2 be Matrix of the carrier of V1 holds Sum M1 + Sum M2 =
Sum(M1 ^^ M2)
proof
let M1,M2 be Matrix of the carrier of V1;
reconsider m = min(len M1,len M2) as Element of NAT by ORDINAL1:def 12;
A1: Seg m = Seg len M1 /\ Seg len M2 by FINSEQ_2:2
.= Seg len M1 /\ dom M2 by FINSEQ_1:def 3
.= dom M1 /\ dom M2 by FINSEQ_1:def 3
.= dom (M1 ^^ M2) by PRE_POLY:def 4
.= Seg len (M1 ^^ M2) by FINSEQ_1:def 3;
A2: len (Sum M1+Sum M2) = min(len Sum M1,len Sum M2) by FINSEQ_2:71
.= min(len M1,len Sum M2) by Def6
.= min(len M1,len M2) by Def6
.= len (M1 ^^ M2) by A1,FINSEQ_1:6
.= len Sum(M1 ^^ M2) by Def6;
A3: dom (Sum M1 + Sum M2) = Seg len(Sum M1 + Sum M2) by FINSEQ_1:def 3;
now
let i be Nat;
assume
A4: i in dom (Sum M1+Sum M2);
then
A5: i in dom Sum(M1 ^^ M2) by A2,A3,FINSEQ_1:def 3;
i in Seg len (M1 ^^ M2) by A2,A3,A4,Def6;
then
A6: i in dom (M1 ^^ M2) by FINSEQ_1:def 3;
then
A7: i in dom M1 /\ dom M2 by PRE_POLY:def 4;
then
A8: i in dom M1 by XBOOLE_0:def 4;
A9: i in dom M2 by A7,XBOOLE_0:def 4;
reconsider m1 = M1.i,m2 = M2.i as FinSequence;
A10: ((M1/.i) ^ (M2/.i)) = m1 ^ (M2/.i) by A8,PARTFUN1:def 6
.= m1 ^ m2 by A9,PARTFUN1:def 6
.= (M1 ^^ M2).i by A6,PRE_POLY:def 4
.= (M1 ^^ M2)/.i by A6,PARTFUN1:def 6;
i in Seg len M2 by A9,FINSEQ_1:def 3;
then i in Seg len (Sum M2) by Def6;
then
A11: i in dom (Sum M2) by FINSEQ_1:def 3;
then
A12: (Sum M2)/.i = (Sum M2).i by PARTFUN1:def 6;
i in Seg len M1 by A8,FINSEQ_1:def 3;
then i in Seg len (Sum M1) by Def6;
then
A13: i in dom (Sum M1) by FINSEQ_1:def 3;
then (Sum M1)/.i = (Sum M1).i by PARTFUN1:def 6;
hence (Sum M1 + Sum M2).i = ((Sum M1)/.i) + ((Sum M2)/.i)
by A4,A12,FUNCOP_1:22
.= Sum (M1/.i) + (Sum M2/.i) by A13,Def6
.= Sum (M1/.i) + Sum (M2/.i) by A11,Def6
.= Sum ((M1 ^^ M2)/.i) by A10,RLVECT_1:41
.= Sum(M1 ^^ M2)/.i by A5,Def6
.= (Sum(M1 ^^ M2)).i by A5,PARTFUN1:def 6;
end;
hence thesis by A2,FINSEQ_2:9;
end;
theorem Th30:
for P1,P2 be FinSequence of V1 st len P1 = len P2 holds
Sum(P1 + P2) = (Sum P1) + (Sum P2)
proof
let P1,P2 be FinSequence of V1;
assume len P1 = len P2;
then reconsider
R1 = P1, R2 = P2 as Element of (len P1)-tuples_on (the carrier of
V1) by FINSEQ_2:92;
thus Sum(P1+P2) = Sum (R1 + R2) .= Sum P1 + Sum P2 by FVSUM_1:76;
end;
theorem Th31:
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)
proof
let M1,M2 be Matrix of the carrier of V1 such that
A1: len M1 = len M2;
len Sum M1 = len M1 by Def6
.= len Sum M2 by A1,Def6;
hence Sum Sum M1 + Sum Sum M2 = Sum (Sum M1 + Sum M2) by Th30
.= Sum Sum(M1 ^^ M2) by Th29;
end;
theorem Th32:
for M be Matrix of the carrier of V1 holds Sum Sum M = Sum Sum (M@)
proof
defpred X[Nat] means for M be Matrix of the carrier of V1 st len M = $1
holds Sum Sum M = Sum Sum (M@);
let M be Matrix of the carrier of V1;
A1: for P be FinSequence of V1 holds Sum Sum <*P*> = Sum Sum (<*P*>@)
proof
defpred X[FinSequence of V1] means Sum Sum <*$1*> = Sum Sum(<*$1*>@);
let P be FinSequence of V1;
len <*<*>(the carrier of V1)*> = 1 by MATRIX_0:def 2;
then width <*<*>(the carrier of V1)*> = 0 by MATRIX_0:20;
then
A2: len (<*<*>(the carrier of V1)*>@) = 0 by MATRIX_0:def 6;
A3: for P being FinSequence of V1, x being Element of V1 st X[P] holds X[P
^<*x*>]
proof
let P be FinSequence of V1, x be Element of V1 such that
A4: Sum Sum <*P*> = Sum Sum (<*P*>@);
Seg len (<*P*> ^^ <*<*x*>*>) = dom (<*P*> ^^ <*<*x*>*>) by FINSEQ_1:def 3
.= dom <*P*> /\ dom <*<*x*>*> by PRE_POLY:def 4
.= Seg 1 /\ dom <*<*x*>*> by FINSEQ_1:38
.= Seg 1 /\ Seg 1 by FINSEQ_1:38
.= Seg 1;
then
A5: len (<*P*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6
.= len <*P^<*x*>*> by FINSEQ_1:39;
then
A6: dom (<*P*> ^^ <*<*x*>*>) = Seg len <*P^<*x*>*> by FINSEQ_1:def 3;
A7: now
let i be Nat;
assume
A8: i in dom (<*P*> ^^ <*<*x*>*>);
then i in { 1 } by A6,FINSEQ_1:2,40;
then
A9: i = 1 by TARSKI:def 1;
reconsider m1 = <*P*>.i, m2 = <*<*x*>*>.i as FinSequence;
thus (<*P*> ^^ <*<*x*>*>).i = m1 ^ m2 by A8,PRE_POLY:def 4
.= P ^ m2 by A9
.= P ^ <*x*> by A9
.= <*P^<*x*>*>.i by A9;
end;
per cases;
suppose
len P = 0;
then
A10: P = {};
hence Sum Sum <*P^<*x*>*> = Sum Sum <*<*x*>*> by FINSEQ_1:34
.= Sum Sum (<*<*x*>*>@) by Th15
.= Sum Sum (<*P^<*x*>*>@) by A10,FINSEQ_1:34;
end;
suppose
A11: len P <> 0;
A12: len <*<*x*>*> = 1 by FINSEQ_1:40;
then
A13: width <*<*x*>*> = len <*x*> by MATRIX_0:20
.= 1 by FINSEQ_1:40;
then
A14: len (<*<*x*>*>@) = 1 by MATRIX_0:def 6;
A15: len <*P*> = 1 by FINSEQ_1:40;
then
A16: width <*P*> = len P by MATRIX_0:20;
then
A17: len (<*P*>@) = len P by MATRIX_0:def 6;
width (<*P*>@) = 1 by A11,A15,A16,MATRIX_0:54;
then reconsider
d1 = <*P*>@ as Matrix of len P,1,the carrier of V1 by A11,A17,
MATRIX_0:20;
A18: len <*P^<*x*>*> = 1 by FINSEQ_1:40;
then
A19: width <*P^<*x*>*> = len (P^<*x*>) by MATRIX_0:20
.= len P + len <*x*> by FINSEQ_1:22
.= len P + 1 by FINSEQ_1:40;
A20: (<*<*x*>*>@)@ = <*<*x*>*> by A12,A13,MATRIX_0:57;
A21: width (<*P*>@) = len <*P*> by A11,A16,MATRIX_0:54
.= width (<*<*x*>*>@) by A15,A12,A13,MATRIX_0:54;
then width (<*<*x*>*>@) = 1 by A11,A15,A16,MATRIX_0:54;
then reconsider
d2 = <*<*x*>*>@ as Matrix of 1,1,the carrier of V1 by A14,MATRIX_0:20;
A22: (d1 ^ d2)@ = ((<*P*>@)@) ^^ ((<*<*x*>*>@)@) by A21,Th28
.= <*P*> ^^ <*<*x*>*> by A11,A15,A16,A20,MATRIX_0:57
.= <*P^<*x*>*> by A5,A7,FINSEQ_2:9
.= (<*P^<*x*>*>@)@ by A18,A19,MATRIX_0:57;
A23: len ((<*P*>@) ^ (<*<*x*>*>@)) = len (<*P*>@) + len (<*<*x*>*>@)
by FINSEQ_1:22
.= width <*P*> + len (<*<*x*>*>@) by MATRIX_0:def 6
.= width <*P*> + width <*<*x*>*> by MATRIX_0:def 6
.= len (<*P^<*x*>*>@) by A16,A13,A19,MATRIX_0:def 6;
thus Sum Sum <*P^<*x*>*> = Sum Sum (<*P*> ^^ <*<*x*>*>) by A5,A7,
FINSEQ_2:9
.= Sum Sum (<*P*>@) + Sum Sum <*<*x*>*> by A4,A15,A12,Th31
.= Sum Sum (<*P*>@) + Sum Sum (<*<*x*>*>@) by Th15
.= Sum (Sum d1 ^ Sum d2) by RLVECT_1:41
.= Sum Sum (d1 ^ d2) by Th27
.= Sum Sum (<*P^<*x*>*>@) by A23,A22,MATRIX_0:53;
end;
end;
<*<*>(the carrier of V1)*> is Matrix of 0+1,0,the carrier of V1;
then Sum Sum <*<*>(the carrier of V1)*> = 0.V1 by Th14
.= Sum Sum (<*<*>(the carrier of V1)*>@) by A2,Th13;
then
A24: X[<*>(the carrier of V1)];
for P be FinSequence of V1 holds X[P] from FINSEQ_2:sch 2(A24,A3);
hence thesis;
end;
A25: for n st X[n] holds X[n+1]
proof
let n such that
A26: for M be Matrix of the carrier of V1 st len M = n holds Sum Sum M
= Sum Sum (M@);
thus for M be Matrix of the carrier of V1 st len M = n+1 holds Sum Sum M =
Sum Sum (M@)
proof
let M be Matrix of the carrier of V1 such that
A27: len M = n+1;
A28: M <> {} by A27;
A29: dom M = Seg len M by FINSEQ_1:def 3;
per cases;
suppose
A30: n = 0;
then M.1 = Line(M,1) by A27,A29,FINSEQ_1:4,MATRIX_0:60;
then reconsider G = M.1 as FinSequence of V1;
M = <*G*> by A27,A30,FINSEQ_1:40;
hence thesis by A1;
end;
suppose
A31: n > 0;
A32: M.(n+1) = Line(M,n+1) by A27,A29,FINSEQ_1:4,MATRIX_0:60;
then reconsider M1 = M.(n+1) as FinSequence of V1;
len M1 = width M by A32,MATRIX_0:def 7;
then reconsider R = <*M1*> as Matrix of 1,width M,the carrier of V1;
reconsider M9 = M as Matrix of n+1,width M,the carrier of V1 by A27,
MATRIX_0:20;
reconsider W = Del(M9,n+1) as Matrix of n,width M,the carrier of V1
by Th3;
A33: width W = width M9 by A31,Th2
.= width R by Th2;
A34: len (W@) = width W by MATRIX_0:def 6
.= len (R@) by A33,MATRIX_0:def 6;
A35: len Del(M,n+1) = n by A27,Th1;
thus Sum Sum M = Sum Sum (W ^ R) by A28,Th4,A27
.= Sum (Sum W ^ Sum R) by Th27
.= Sum Sum Del(M,n+1) + Sum Sum R by RLVECT_1:41
.= Sum Sum (Del(M,n+1)@) + Sum Sum R by A26,A35
.= Sum Sum (Del(M,n+1)@) + Sum Sum (R@) by A1
.= Sum Sum ((W@) ^^ (R@)) by A34,Th31
.= Sum Sum ((W ^ R)@) by A33,Th28
.= Sum Sum (M@) by A28,Th4,A27;
end;
end;
end;
A36: X[0]
proof
let M be Matrix of the carrier of V1;
assume
A37: len M = 0;
then width M = 0 by MATRIX_0:def 3;
then
A38: len (M@) = 0 by MATRIX_0:def 6;
thus Sum Sum M = 0.V1 by A37,Th13
.= Sum Sum (M@) by A38,Th13;
end;
for n holds X[n] from NAT_1:sch 2(A36,A25);
then X[len M];
hence thesis;
end;
theorem Th33:
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)
proof
let M be Matrix of n,m,the carrier of K such that
A1: n > 0 and
A2: m > 0;
A3: len M = n by A1,MATRIX_0:23;
reconsider n1=n, m1=m as Element of NAT by ORDINAL1:def 12;
let p,d be FinSequence of K such that
A4: len p = n and
A5: len d = m and
A6: for j st j in dom d holds d/.j = Sum mlt(p,Col(M,j));
let b,c be FinSequence of V1 such that
A7: len b = m and
A8: len c = n and
A9: for i st i in dom c holds c/.i = Sum lmlt(Line(M,i),b);
deffunc V(Nat,Nat) = (p/.$1) * (M*($1,$2)) * (b/.$2);
consider M1 being Matrix of n1,m1,the carrier of V1 such that
A10: for i,j st [i,j] in Indices M1 holds M1*(i,j) = V(i,j) from MATRIX_0
:sch 1;
A11: width M1 = len (M1@) by MATRIX_0:def 6
.= len Sum (M1@) by Def6;
A12: dom d = dom b by A5,A7,FINSEQ_3:29;
then
A13: dom lmlt(d,b) = dom b by Th12;
then
A14: len lmlt(d,b) = len b by FINSEQ_3:29
.= len Sum (M1@) by A1,A7,A11,MATRIX_0:23;
then
A15: dom lmlt(d,b) = Seg len Sum(M1@) by FINSEQ_1:def 3;
A16: width M1 = m by A1,MATRIX_0:23;
A17: len M1 = n by A1,MATRIX_0:23;
A18: dom lmlt(d,b) = dom d by A12,Th12;
A19: now
A20: Seg len Sum(M1@) = dom Sum(M1@) by FINSEQ_1:def 3;
let j be Nat such that
A21: j in dom lmlt(d,b);
A22: j in dom Sum(M1@) by A15,A21,FINSEQ_1:def 3;
A23: j in dom d by A12,A21,Th12;
A24: d/.j = d.j & b/.j = b.j by A18,A13,A21,PARTFUN1:def 6;
len Sum(M1@) = len (M1@) by Def6;
then
A25: dom Sum(M1@) = dom (M1@) by FINSEQ_3:29;
then
A26: M1@/.j = M1@.j by A22,PARTFUN1:def 6
.= Line(M1@,j) by A22,A25,MATRIX_0:60;
reconsider H = mlt(p,Col(M,j)) as FinSequence of K;
deffunc V(Nat) = (H/.$1) * (b/.j);
consider G be FinSequence of V1 such that
A27: len G = len p & for i be Nat st i in dom G holds G.i = V(i) from
FINSEQ_2:sch 1;
A28: len p = len Col(M,j) by A4,A3,MATRIX_0:def 8;
then
A29: len ((the multF of K).:(p,Col(M,j))) = len p by FINSEQ_2:72;
then
A30: dom H = dom G by A27,FINSEQ_3:29;
A31: dom p = dom G by A27,FINSEQ_3:29;
A32: len Line(M1@,j) = width (M1@) by MATRIX_0:def 7
.= len ((M1@)@) by MATRIX_0:def 6
.= len G by A1,A2,A4,A17,A16,A27,MATRIX_0:57;
then
A33: dom Line(M1@,j) = Seg len G by FINSEQ_1:def 3;
A34: dom G = Seg len p by A27,FINSEQ_1:def 3;
A35: now
let i be Nat;
A36: dom M = Seg len M by FINSEQ_1:def 3;
assume
A37: i in dom Line(M1@,j);
then
A38: i in Seg len ((the multF of K).:(p,Col(M,j))) by A27,A28,A33,FINSEQ_2:72;
then
A39: i in dom H by FINSEQ_1:def 3;
A40: i in dom ((the multF of K).:(p,Col(M,j))) by A38,FINSEQ_1:def 3;
A41: Seg len G = dom G by FINSEQ_1:def 3;
then
A42: (p/.i) * (M*(i,j)) = (the multF of K).(p.i,M*(i,j)) by A31,A33,A37,
PARTFUN1:def 6
.= (the multF of K).(p.i,Col(M,j).i) by A4,A3,A27,A33,A37,A36,
MATRIX_0:def 8
.= ((the multF of K).:(p,Col(M,j))).i by A40,FUNCOP_1:22
.= H/.i by A39,PARTFUN1:def 6;
dom M1 = dom G by A4,A17,A27,FINSEQ_3:29;
then [i,j] in [:dom M1,Seg width M1:] by A11,A15,A21,A33,A37,A41,
ZFMISC_1:87;
then
A43: [i,j] in Indices M1 by MATRIX_0:def 4;
i in Seg width (M1@) by A32,A33,A37,MATRIX_0:def 7;
hence Line(M1@,j).i = (M1@)*(j,i) by MATRIX_0:def 7
.= M1*(i,j) by A43,MATRIX_0:def 6
.= (H/.i) * (b/.j) by A10,A43,A42
.= G.i by A27,A34,A33,A37;
end;
thus lmlt(d,b).j = (the lmult of V1).(d.j,b.j) by A21,FUNCOP_1:22
.= (d/.j) * (b/.j) by A24,VECTSP_1:def 12
.= Sum H * (b/.j) by A6,A23
.= Sum G by A27,A29,A30,Th10
.= Sum (M1@/.j) by A32,A35,A26,FINSEQ_2:9
.= Sum (M1@)/.j by A22,Def6
.= (Sum (M1@)).j by A15,A21,A20,PARTFUN1:def 6;
end;
A44: dom p = dom c by A4,A8,FINSEQ_3:29;
then
A45: dom lmlt(p,c) = dom p by Th12;
then
A46: len lmlt(p,c) = len p by FINSEQ_3:29
.= len M1 by A4,MATRIX_0:def 2
.= len Sum M1 by Def6;
now
let i be Nat such that
A47: i in dom Sum M1;
A48: i in dom c by A44,A45,A46,A47,FINSEQ_3:29;
then
A49: c.i = c/.i & p.i = p/.i by A44,PARTFUN1:def 6;
i in Seg len Sum M1 by A47,FINSEQ_1:def 3;
then i in Seg len M1 by Def6;
then
A50: i in dom M1 by FINSEQ_1:def 3;
then
A51: M1/.i = M1.i by PARTFUN1:def 6
.= Line(M1,i) by A50,MATRIX_0:60;
deffunc V(Nat) = (p/.i) * (lmlt(Line(M,i),b)/.$1);
consider F be FinSequence of V1 such that
A52: len F = len b & for j be Nat st j in dom F holds F.j = V(j) from
FINSEQ_2:sch 1;
A53: len F = width M by A1,A7,A52,MATRIX_0:23;
A54: dom Line(M,i) = Seg len Line(M,i) by FINSEQ_1:def 3
.= Seg len F by A53,MATRIX_0:def 7
.= dom b by A52,FINSEQ_1:def 3;
then dom lmlt(Line(M,i),b) = dom b by Th12;
then
A55: len F = len lmlt(Line(M,i),b) & dom F = dom lmlt(Line(M,i),b) by A52,
FINSEQ_3:29;
A56: len F = width M1 by A1,A7,A52,MATRIX_0:23;
then
A57: len Line(M1,i) = len F by MATRIX_0:def 7;
then
A58: dom (M1/.i) = Seg len F by A51,FINSEQ_1:def 3;
A59: dom F = Seg len b by A52,FINSEQ_1:def 3;
A60: now
let j be Nat;
assume
A61: j in dom (M1/.i);
then
A62: Line(M,i).j = M*(i,j) by A53,A58,MATRIX_0:def 7;
[i,j] in [:dom M1,Seg width M1:] by A56,A50,A58,A61,ZFMISC_1:87;
then
A63: [i,j] in Indices M1 by MATRIX_0:def 4;
A64: j in dom b by A52,A58,A61,FINSEQ_1:def 3;
then
A65: b.j = b/.j by PARTFUN1:def 6;
A66: j in dom (lmlt(Line(M,i),b)) by A54,A64,Th12;
then
A67: (lmlt(Line(M,i),b)/.j) = lmlt(Line(M,i),b).j by PARTFUN1:def 6
.= (the lmult of V1).(Line(M,i).j,b.j) by A66,FUNCOP_1:22
.= M*(i,j) * (b/.j) by A65,A62,VECTSP_1:def 12;
thus (M1/.i).j = M1*(i,j) by A56,A51,A58,A61,MATRIX_0:def 7
.= (p/.i) * (M*(i,j)) * (b/.j) by A10,A63
.= (p/.i) * (lmlt(Line(M,i),b)/.j) by A67,VECTSP_1:def 16
.= F.j by A52,A59,A58,A61;
end;
A68: for j be Nat st j in dom F holds F.j = (p/.i) * (lmlt(Line
(M,i),b)/.j) by A52;
i in dom ((the lmult of V1).:(p,c)) by A46,A47,FINSEQ_3:29;
hence lmlt(p,c).i = (the lmult of V1).(p.i,c.i) by FUNCOP_1:22
.= (p/.i) * (c/.i) by A49,VECTSP_1:def 12
.= (p/.i) * Sum lmlt(Line(M,i),b) by A9,A48
.= Sum F by A55,A68,RLVECT_2:67
.= Sum (M1/.i) by A57,A51,A60,FINSEQ_2:9
.= (Sum M1)/.i by A47,Def6
.= (Sum M1).i by A47,PARTFUN1:def 6;
end;
hence Sum lmlt(p,c) = Sum Sum M1 by A46,FINSEQ_2:9
.= Sum Sum (M1@) by Th32
.= Sum lmlt(d,b) by A14,A19,FINSEQ_2:9;
end;
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
:Def7:
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);
existence
proof
reconsider b2 = rng b1 as Basis of V by Def2;
consider KL be Linear_Combination of V such that
A1: W = Sum(KL) and
A2: Carrier KL c= b2 by Th8;
deffunc V(Nat) = KL.(b1/.$1);
consider A be FinSequence of K such that
A3: len A = len b1 and
A4: for k be Nat st k in dom A holds A.k = V(k) from FINSEQ_2:sch 1;
take A;
thus len A = len b1 by A3;
take KL;
thus W = Sum(KL) by A1;
thus Carrier KL c= rng b1 by A2;
let k;
A5: dom A = Seg len b1 by A3,FINSEQ_1:def 3;
assume 1<=k & k<=len A;
then
A6: k in Seg len b1 by A3,FINSEQ_1:1;
then k in dom A by A3,FINSEQ_1:def 3;
then A.k = A/.k by PARTFUN1:def 6;
hence thesis by A4,A5,A6;
end;
uniqueness
proof
reconsider b = rng b1 as Basis of V by Def2;
let F1,F2 be FinSequence of K;
assume
A7: len F1 = len b1;
given KL1 be Linear_Combination of V such that
A8: W = Sum(KL1) & Carrier(KL1) c= rng b1 and
A9: for k st 1<=k & k<=len F1 holds F1/.k=KL1.(b1/.k);
assume
A10: len F2 = len b1;
given KL2 be Linear_Combination of V such that
A11: W = Sum(KL2) & Carrier(KL2) c= rng b1 and
A12: for k st 1<=k & k<=len F2 holds F2/.k=KL2.(b1/.k);
A13: b is linearly-independent by VECTSP_7:def 3;
for k be Nat st 1<=k & k<=len F1 holds F1.k = F2.k
proof
let k be Nat;
assume
A14: 1<=k & k<=len F1;
then
A15: k in dom F2 by A7,A10,FINSEQ_3:25;
k in dom F1 by A14,FINSEQ_3:25;
hence F1.k = F1/.k by PARTFUN1:def 6
.= KL1.(b1/.k) by A9,A14
.= KL2.(b1/.k) by A8,A11,A13,Th5
.= F2/.k by A7,A10,A12,A14
.= F2.k by A15,PARTFUN1:def 6;
end;
hence thesis by A7,A10,FINSEQ_1:14;
end;
end;
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
proof
let K be Field, V be finite-dimensional VectSp of K, b be OrdBasis of V,
W be Element of V;
len (W|--b) = len b by Def7;
hence thesis by FINSEQ_3:29;
end;
theorem Th34:
v1|--b2 = v2|--b2 implies v1 = v2
proof
consider KL1 be Linear_Combination of V2 such that
A1: v1 = Sum(KL1) and
A2: Carrier KL1 c= rng b2 and
A3: for t st 1<=t & t<=len (v1|--b2) holds (v1|--b2)/.t = KL1.(b2/.t) by Def7;
consider KL2 be Linear_Combination of V2 such that
A4: v2 = Sum(KL2) and
A5: Carrier KL2 c= rng b2 and
A6: for t st 1<=t & t<=len (v2|--b2) holds (v2|--b2)/.t = KL2.(b2/.t) by Def7;
assume
A7: v1|--b2 = v2|--b2;
A8: now
let t be Nat;
assume
A9: 1<=t & t<=len (v1|--b2);
hence KL1.(b2/.t) = (v2|--b2)/.t by A7,A3
.= KL2.(b2/.t) by A7,A6,A9;
end;
A10: Carrier KL1 \/ Carrier KL2 c= rng b2 by A2,A5,XBOOLE_1:8;
now
let v be Vector of V2;
per cases;
suppose
A11: not v in Carrier KL1 \/ Carrier KL2;
then not v in Carrier KL2 by XBOOLE_0:def 3;
then
A12: KL2.v = 0.K by VECTSP_6:2;
not v in Carrier KL1 by A11,XBOOLE_0:def 3;
hence KL1.v = KL2.v by A12,VECTSP_6:2;
end;
suppose
v in Carrier KL1 \/ Carrier KL2;
then consider x being object such that
A13: x in dom b2 and
A14: v = b2.x by A10,FUNCT_1:def 3;
reconsider x as Nat by A13,FINSEQ_3:23;
x<=len b2 by A13,FINSEQ_3:25;
then
A15: x<=len (v1|--b2) by Def7;
v = b2/.x & 1<=x by A13,A14,FINSEQ_3:25,PARTFUN1:def 6;
hence KL1.v = KL2.v by A8,A15;
end;
end;
hence thesis by A1,A4,VECTSP_6:def 7;
end;
theorem Th35:
v = Sum lmlt(v|--b1,b1)
proof
consider KL be Linear_Combination of V1 such that
A1: v = Sum KL & Carrier KL c= rng b1 and
A2: for k st 1<=k & k<=len (v|--b1) holds (v|--b1)/.k=KL.(b1/.k) by Def7;
len (v|--b1) = len b1 by Def7;
then
A3: dom (v|--b1) = dom b1 by FINSEQ_3:29;
then
A4: dom b1 = dom lmlt(v|--b1,b1) by Th12;
len (KL (#) b1) = len b1 by VECTSP_6:def 5
.= len lmlt(v|--b1,b1) by A4,FINSEQ_3:29; then
A5: dom (KL (#) b1) = dom lmlt(v|--b1,b1) by FINSEQ_3:29;
A6: now
let t be Nat;
assume
A7: t in dom lmlt(v|--b1,b1);
then
A8: b1/.t = b1.t by A4,PARTFUN1:def 6;
t in dom (v|--b1) by A3,A7,Th12;
then
A9: t<=len (v|--b1) by FINSEQ_3:25;
A10: 1<=t by A7,FINSEQ_3:25;
then
A11: (v|--b1)/.t = (v|--b1).t by A9,FINSEQ_4:15;
t in dom (KL (#) b1) by A5,A7;
hence (KL (#) b1).t = KL.(b1/.t) * (b1/.t) by VECTSP_6:def 5
.= ((v|--b1)/.t) * (b1/.t) by A2,A10,A9
.= (the lmult of V1).((v|--b1).t,b1.t) by A8,A11,VECTSP_1:def 12
.= lmlt(v|--b1,b1).t by A7,FUNCOP_1:22;
end;
b1 is one-to-one by Def2;
hence v = Sum(KL (#) b1) by A1,Th20
.= Sum lmlt(v|--b1,b1) by A5,A6,FINSEQ_1:13;
end;
theorem Th36:
len d = len b1 implies d = Sum(lmlt(d,b1)) |-- b1
proof
reconsider T = rng b1 as finite Subset of V1 by Def2;
defpred X[Element of V1, Element of K] means ($1 in rng b1 implies (for k st
k in dom b1 & b1/.k = $1 holds $2 = d/.k)) & (not $1 in rng b1 implies $2 = 0.K
);
A1: for v ex u being Element of K st X[v,u]
proof
let v be Element of V1;
per cases;
suppose
A2: v in rng b1;
then consider k be Element of NAT such that
A3: k in dom b1 and
A4: b1/.k = v by PARTFUN2:2;
take u = d/.k;
now
A5: b1 is one-to-one by Def2;
let i;
assume that
A6: i in dom b1 and
A7: b1/.i = v;
b1.i = b1/.k by A4,A6,A7,PARTFUN1:def 6
.= b1.k by A3,PARTFUN1:def 6;
hence u = d/.i by A3,A6,A5,FUNCT_1:def 4;
end;
hence thesis by A2;
end;
suppose
A8: not v in rng b1;
take 0.K;
thus thesis by A8;
end;
end;
consider KL be Function of V1, K such that
A9: for v holds X[v,KL.v] from FUNCT_2:sch 3(A1);
A10: now
take T;
let v be Element of V1;
assume not v in T;
hence KL.v = 0.K by A9;
end;
now
take f = KL;
thus KL = f & dom f = the carrier of V1 & rng f c= the carrier of K by
FUNCT_2:def 1,RELAT_1:def 19;
end;
then KL in Funcs(the carrier of V1, the carrier of K) by FUNCT_2:def 2;
then reconsider KL1 = KL as Linear_Combination of V1 by A10,VECTSP_6:def 1;
assume
A11: len d = len b1;
now
take KL1;
A12: b1 is one-to-one by Def2;
thus
A13: for k st 1<=k & k<=len d holds d/.k=KL1.(b1/.k)
proof
let k;
assume 1<=k & k<=len d;
then
A14: k in dom b1 by A11,FINSEQ_3:25;
then b1.k = b1/.k by PARTFUN1:def 6;
then b1/.k in rng b1 by A14,FUNCT_1:def 3;
hence thesis by A9,A14;
end;
for x being object holds x in Carrier KL1 implies x in rng b1
proof
let x be object;
assume x in Carrier KL1;
then
A15: ex v st x = v & KL1.v <> 0.K by VECTSP_6:1;
assume not x in rng b1;
hence contradiction by A9,A15;
end;
hence
A16: Carrier KL1 c= rng b1;
A17: dom d = dom b1 by A11,FINSEQ_3:29;
then
A18: dom lmlt(d,b1) = dom b1 by Th12;
then
A19: len lmlt(d,b1) = len b1 by FINSEQ_3:29
.= len (KL1 (#) b1) by VECTSP_6:def 5;
now
let k be Nat;
assume
A20: k in dom lmlt(d,b1);
then
A21: k in dom (KL1 (#) b1) by A19,FINSEQ_3:29;
A22: 1<=k & k<=len d by A11,A18,A20,FINSEQ_3:25;
A23: d/.k = d.k & b1/.k = b1.k by A17,A18,A20,PARTFUN1:def 6;
thus lmlt(d,b1).k = (the lmult of V1).(d.k,b1.k) by A20,FUNCOP_1:22
.= (d/.k) * (b1/.k) by A23,VECTSP_1:def 12
.= KL1.(b1/.k) * (b1/.k) by A13,A22
.= (KL1 (#) b1).k by A21,VECTSP_6:def 5;
end;
hence Sum(lmlt(d,b1)) = Sum(KL1 (#) b1) by A19,FINSEQ_2:9
.= Sum KL1 by A16,A12,Th20;
end;
hence thesis by A11,Def7;
end;
Lm2: for p be FinSequence, k be set st k in dom p holds len p > 0
proof
let p be FinSequence, k be set;
assume k in dom p;
then p <> {};
hence thesis;
end;
theorem Th37:
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))
proof
let a,d be FinSequence of K such that
A1: len a = len b1;
reconsider B3 = f*b1 as FinSequence of V2;
deffunc V(Nat,Nat) = ((B3/.$1) |-- b2)/.$2;
consider M being Matrix of len b1,len b2,the carrier of K such that
A2: for i,j st [i,j] in Indices M holds M*(i,j) = V(i,j) from MATRIX_0:
sch 1;
deffunc W(Nat) = Sum mlt(a,Col(M,$1));
consider dd being FinSequence of K such that
A3: len dd = len b2 & for j be Nat st j in dom dd holds dd/.j = W(j)
from FINSEQ_4:sch 2;
let j be Nat such that
A4: j in dom b2;
A5: j in dom dd by A4,A3,FINSEQ_3:29;
assume that
A6: len d = len b1 and
A7: for k st k in dom b1 holds d.k = (f.(b1/.k) |-- b2)/.j;
A8: len Col(M,j) = len M by MATRIX_0:def 8
.= len d by A6,MATRIX_0:def 2;
len M = len b1 by MATRIX_0:def 2;
then
A9: dom M = dom b1 by FINSEQ_3:29;
A10: len b1 = len B3 by FINSEQ_2:33;
then
A11: dom b1 = dom B3 by FINSEQ_3:29;
assume
A12: len b1 > 0;
then
A13: width M = len b2 by MATRIX_0:23;
A14: now
let i such that
A15: i in dom B3;
A16: now
let j be Nat;
assume
A17: j in dom ((B3/.i) |-- b2);
then j in Seg len ((B3/.i) |-- b2) by FINSEQ_1:def 3;
then
A18: j in Seg width M by A13,Def7;
then [i,j] in [:dom M,Seg width M:] by A9,A11,A15,ZFMISC_1:87;
then
A19: [i,j] in Indices M by MATRIX_0:def 4;
thus Line(M,i).j = M*(i,j) by A18,MATRIX_0:def 7
.= ((B3/.i) |-- b2)/.j by A2,A19
.= ((B3/.i) |-- b2).j by A17,PARTFUN1:def 6;
end;
A20: len Line(M,i) = width M by MATRIX_0:def 7
.= len ((B3/.i) |-- b2) by A13,Def7;
thus B3/.i = Sum lmlt((B3/.i) |-- b2,b2) by Th35
.= Sum lmlt(Line(M,i),b2) by A20,A16,FINSEQ_2:9;
end;
Seg len b2 = dom b2 by FINSEQ_1:def 3;
then
A21: j in Seg width M by A4,A12,MATRIX_0:23;
A22: now
let i be Nat;
assume i in dom d;
then
A23: i in dom b1 by A6,FINSEQ_3:29;
then
A24: B3/.i = B3.i by A11,PARTFUN1:def 6
.= f.(b1.i) by A23,FUNCT_1:13
.= f.(b1/.i) by A23,PARTFUN1:def 6;
[i,j] in [:dom M,Seg width M:] by A9,A21,A23,ZFMISC_1:87;
then
A25: [i,j] in Indices M by MATRIX_0:def 4;
thus Col(M,j).i = M*(i,j) by A9,A23,MATRIX_0:def 8
.= (f.((b1/.i)) |-- b2)/.j by A2,A24,A25
.= d.i by A7,A23;
end;
len b2 > 0 by A4,Lm2;
hence (Sum(lmlt(a,f*b1)) |-- b2)/.j = (Sum(lmlt(dd,b2)) |-- b2)/.j
by A1,A12,A3,A10,A14,Th33
.= dd/.j by A3,Th36
.= Sum(mlt(a,Col(M,j))) by A3,A5
.= Sum(mlt(a,d)) by A8,A22,FINSEQ_2:9;
end;
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
:Def8:
len it = len b1 & for k st k in dom b1 holds it/.k = f.(b1/.k) |-- b2;
existence
proof
deffunc V(Nat) = f.(b1/.$1) |-- b2;
consider M be FinSequence such that
A1: len M = len b1 and
A2: for k be Nat st k in dom M holds M.k = V(k) from FINSEQ_1:sch 2;
A3: dom M = Seg len b1 by A1,FINSEQ_1:def 3;
ex n being Nat st for x st x in rng M ex s st s=x & len s = n
proof
take n = len(f.(b1/.1) |-- b2);
let x be object;
assume x in rng M;
then consider y being object such that
A4: y in dom M and
A5: x = M.y by FUNCT_1:def 3;
reconsider y as Nat by A4,FINSEQ_3:23;
M.y = f.(b1/.y) |-- b2 by A2,A4;
then reconsider s = M.y as FinSequence;
take s;
thus s = x by A5;
thus len s = len (f.(b1/.y) |-- b2) by A2,A4
.= len b2 by Def7
.= n by Def7;
end;
then reconsider M as tabular FinSequence by MATRIX_0:def 1;
now
let x be object;
assume x in rng M;
then consider y being object such that
A6: y in dom M and
A7: x = M.y by FUNCT_1:def 3;
reconsider y as Nat by A6,FINSEQ_3:23;
M.y = f.(b1/.y) |-- b2 by A2,A6;
then reconsider s = M.y as FinSequence of K;
s = x by A7;
hence x in (the carrier of K)* by FINSEQ_1:def 11;
end;
then rng M c= (the carrier of K)*;
then reconsider M as Matrix of K by FINSEQ_1:def 4;
take M1 = M;
for k st k in dom b1 holds M1/.k = f.(b1/.k) |-- b2
proof
let k be Nat;
assume
A8: k in dom b1;
then
A9: k in Seg len b1 by FINSEQ_1:def 3;
dom M1 = dom b1 by A1,FINSEQ_3:29;
hence M1/.k = M1.k by A8,PARTFUN1:def 6
.= f.(b1/.k) |-- b2 by A2,A3,A9;
end;
hence thesis by A1;
end;
uniqueness
proof
let K1,K2 be Matrix of K such that
A10: len K1 = len b1 and
A11: for k st k in dom b1 holds K1/.k = f.(b1/.k) |-- b2 and
A12: len K2 = len b1 and
A13: for k st k in dom b1 holds K2/.k = f.(b1/.k) |-- b2;
for k be Nat st 1 <= k & k <= len K1 holds K1.k = K2.k
proof
let k be Nat;
assume
A14: 1 <= k & k <= len K1;
then
A15: k in dom b1 by A10,FINSEQ_3:25;
A16: k in dom K2 by A10,A12,A14,FINSEQ_3:25;
k in dom K1 by A14,FINSEQ_3:25;
hence K1.k = K1/.k by PARTFUN1:def 6
.= f.(b1/.k) |-- b2 by A11,A15
.= K2/.k by A13,A15
.=K2.k by A16,PARTFUN1:def 6;
end;
hence thesis by A10,A12,FINSEQ_1:14;
end;
end;
Lm3: dom AutMt(f,b1,b2) = dom b1
proof
len AutMt(f,b1,b2) = len b1 by Def8;
hence thesis by FINSEQ_3:29;
end;
theorem Th38:
len b1 = 0 implies AutMt(f,b1,b2) = {}
proof
assume len b1 = 0;
then len AutMt(f,b1,b2) = 0 by Def8;
hence thesis;
end;
theorem Th39:
len b1 > 0 implies width AutMt(f,b1,b2) = len b2
proof
assume len b1 > 0;
then len AutMt(f,b1,b2) > 0 by Def8;
then consider s being FinSequence such that
A1: s in rng AutMt(f,b1,b2) and
A2: len s = width AutMt(f,b1,b2) by MATRIX_0:def 3;
consider i be Nat such that
A3: i in dom AutMt(f,b1,b2) and
A4: AutMt(f,b1,b2).i = s by A1,FINSEQ_2:10;
len AutMt(f,b1,b2) = len b1 by Def8;
then
A5: i in dom b1 by A3,FINSEQ_3:29;
s = (AutMt(f,b1,b2))/.i by A3,A4,PARTFUN1:def 6
.= f.(b1/.i) |-- b2 by A5,Def8;
hence thesis by A2,Def7;
end;
theorem
f1 is additive homogeneous & f2 is additive homogeneous &
AutMt(f1,b1,b2) = AutMt(f2,b1,b2) & len b1 > 0 implies f1 = f2
proof
assume that
A1: f1 is additive homogeneous & f2 is additive homogeneous and
A2: AutMt(f1,b1,b2) = AutMt(f2,b1,b2) and
A3: len b1 > 0;
rng b1 is Basis of V1 by Def2;
then
A4: rng b1 c= the carrier of V1;
then
A5: rng b1 c= dom f2 by FUNCT_2:def 1;
rng b1 c= dom f1 by A4,FUNCT_2:def 1;
then
A6: dom (f1*b1) = dom b1 by RELAT_1:27
.= dom (f2*b1) by A5,RELAT_1:27;
now
let x be object;
assume
A7: x in dom (f1*b1);
then reconsider k=x as Nat by FINSEQ_3:23;
A8: dom (f1*b1) c= dom b1 by RELAT_1:25;
then
A9: f1.(b1/.k) |-- b2 = (AutMt(f2,b1,b2))/.k by A2,A7,Def8
.= f2.(b1/.k) |-- b2 by A7,A8,Def8;
thus (f1*b1).x = f1.(b1.x) by A7,FUNCT_1:12
.= f1.(b1/.x) by A7,A8,PARTFUN1:def 6
.= f2.(b1/.x) by A9,Th34
.= f2.(b1.x) by A7,A8,PARTFUN1:def 6
.= (f2*b1).x by A6,A7,FUNCT_1:12;
end;
hence thesis by A1,A3,A6,Th22,FUNCT_1:2;
end;
theorem
g is additive homogeneous & len b1 > 0 & len b2 > 0 implies
AutMt(g*f,b1,b3) = AutMt(f,b1,b2) * AutMt(g,b2,b3)
proof
assume
A1: g is additive homogeneous;
assume that
A2: len b1 > 0 and
A3: len b2 > 0;
A4: width AutMt(f,b1,b2) = len b2 by A2,Th39
.= len AutMt(g,b2,b3) by Def8;
A5: width AutMt(g*f,b1,b3) = len b3 by A2,Th39
.= width AutMt(g,b2,b3) by A3,Th39;
then
A6: width AutMt(g*f,b1,b3) = width (AutMt(f,b1,b2) * AutMt(g,b2,b3)) by A4,
MATRIX_3:def 4;
A7: len AutMt(g*f,b1,b3) = len b1 by Def8
.= len AutMt(f,b1,b2) by Def8
.= len (AutMt(f,b1,b2) * AutMt(g,b2,b3)) by A4,MATRIX_3:def 4;
then
A8: dom AutMt(g*f,b1,b3) = dom (AutMt(f,b1,b2) * AutMt(g,b2,b3)) by FINSEQ_3:29
;
for i,j st [i,j] in Indices AutMt(g*f,b1,b3) holds AutMt(g*f,b1,b3)*(i,j
) = (AutMt(f,b1,b2) * AutMt(g,b2,b3))*(i,j)
proof
let i,j;
deffunc V(Nat) = (g.((b2/.$1)) |-- b3)/.j;
consider d be FinSequence of K such that
A9: len d = len b2 & for k be Nat st k in dom d holds d.k = V(k) from
FINSEQ_2:sch 1;
assume
A10: [i,j] in Indices AutMt(g*f,b1,b3);
then
A11: [i,j] in [:dom AutMt(g*f,b1,b3), Seg width AutMt(g*f,b1,b3):] by
MATRIX_0:def 4;
then
A12: j in Seg width AutMt(g*f,b1,b3) by ZFMISC_1:87;
A13: len Col(AutMt(g,b2,b3),j) = len AutMt(g,b2,b3) by MATRIX_0:def 8
.= len d by A9,Def8;
A14: dom d = Seg len b2 by A9,FINSEQ_1:def 3;
A15: [i,j] in Indices (AutMt(f,b1,b2) * AutMt(g,b2,b3)) by A8,A6,A11,
MATRIX_0:def 4;
A16: i in dom AutMt(g*f,b1,b3) by A11,ZFMISC_1:87;
A17: width AutMt(g*f,b1,b3) <> {} by A12;
len b1 = len AutMt(g*f,b1,b3) by Def8;
then len b1 > 0 by A17,MATRIX_0:def 3;
then
A18: j in Seg len b3 by A12,Th39;
then
A19: j in dom b3 by FINSEQ_1:def 3;
A20: now
let k be Nat;
assume
A21: 1 <=k & k <= len d;
then
A22: k in dom d by FINSEQ_3:25;
A23: k in dom b2 by A9,A21,FINSEQ_3:25;
A24: len AutMt(g,b2,b3) = len b2 by Def8;
then
A25: k in dom AutMt(g,b2,b3) by A9,A21,FINSEQ_3:25;
j in Seg width AutMt(g,b2,b3) by A5,A11,ZFMISC_1:87;
then
[k,j] in [:dom AutMt(g,b2,b3),Seg width AutMt(g,b2,b3):] by A25,ZFMISC_1:87;
then [k,j] in Indices AutMt(g,b2,b3) by MATRIX_0:def 4;
then consider p2 be FinSequence of K such that
A26: p2= AutMt(g,b2,b3).k and
A27: AutMt(g,b2,b3)*(k,j) = p2.j by MATRIX_0:def 5;
A28: p2 = (AutMt(g,b2,b3))/.k by A25,A26,PARTFUN1:def 6
.= g.(b2/.k) |-- b3 by A23,Def8;
then j in Seg len p2 by A18,Def7;
then
A29: j in dom p2 by FINSEQ_1:def 3;
k in dom AutMt(g,b2,b3) by A9,A21,A24,FINSEQ_3:25;
hence Col(AutMt(g,b2,b3),j).k = p2.j by A27,MATRIX_0:def 8
.= (g.(b2/.k) |-- b3)/.j by A28,A29,PARTFUN1:def 6
.= d.k by A9,A22;
end;
b1/.i in the carrier of V1;
then
A30: b1/.i in dom f by FUNCT_2:def 1;
consider p1 be FinSequence of K such that
A31: p1 = AutMt(g*f,b1,b3).i and
A32: AutMt(g*f,b1,b3)*(i,j) = p1.j by A10,MATRIX_0:def 5;
A33: len (f.(b1/.i) |-- b2) = len b2 by Def7;
A34: len AutMt(g*f,b1,b3) = len b1 by Def8;
then
A35: i in dom b1 by A16,FINSEQ_3:29;
A36: p1 = (AutMt(g*f,b1,b3))/.i by A16,A31,PARTFUN1:def 6
.= (g*f).(b1/.i) |-- b3 by A35,Def8;
len AutMt(f,b1,b2) = len b1 by Def8;
then
A37: i in dom AutMt(f,b1,b2) by A16,A34,FINSEQ_3:29;
then
A38: Line(AutMt(f,b1,b2),i) = AutMt(f,b1,b2).i by MATRIX_0:60
.= (AutMt(f,b1,b2))/.i by A37,PARTFUN1:def 6
.= f.(b1/.i) |-- b2 by A35,Def8;
A39: Seg len b2 = dom b2 by FINSEQ_1:def 3;
j in Seg len ((g*f).(b1/.i) |-- b3) by A18,Def7;
then j in dom p1 by A36,FINSEQ_1:def 3;
hence AutMt(g*f,b1,b3)*(i,j) = ((g*f).(b1/.i) |-- b3)/.j by A32,A36,
PARTFUN1:def 6
.= (g.(f.(b1/.i)) |-- b3)/.j by A30,FUNCT_1:13
.= (g.Sum(lmlt(f.(b1/.i) |-- b2,b2)) |-- b3)/.j by Th35
.= (Sum(lmlt(f.(b1/.i) |-- b2,g*b2)) |-- b3)/.j by A1,A33,Th18
.= Sum(mlt(f.(b1/.i) |-- b2,d)) by A3,A19,A9,A14,A39,A33,Th37
.= Line(AutMt(f,b1,b2),i) "*" Col(AutMt(g,b2,b3),j) by A38,A13,A20,
FINSEQ_1:14
.= (AutMt(f,b1,b2) * AutMt(g,b2,b3))*(i,j) by A4,A15,MATRIX_3:def 4;
end;
hence thesis by A7,A6,MATRIX_0:21;
end;
theorem
AutMt(f1+f2,b1,b2) = AutMt(f1,b1,b2) + AutMt(f2,b1,b2)
proof
A1: len AutMt(f1+f2,b1,b2) = len b1 by Def8
.= len AutMt(f1,b1,b2) by Def8;
then
A2: dom AutMt(f1+f2,b1,b2) = dom AutMt(f1,b1,b2) by FINSEQ_3:29;
A3: width AutMt(f1,b1,b2) = width AutMt(f2,b1,b2)
proof
per cases;
suppose
A4: len b1 = 0;
then AutMt(f1,b1,b2) = {} by Th38
.= AutMt(f2,b1,b2) by A4,Th38;
hence thesis;
end;
suppose
A5: len b1 > 0;
hence width AutMt(f1,b1,b2) = len b2 by Th39
.= width AutMt(f2,b1,b2) by A5,Th39;
end;
end;
A6: width AutMt(f1+f2,b1,b2) = width AutMt(f1,b1,b2)
proof
per cases;
suppose
A7: len b1 = 0;
then AutMt(f1+f2,b1,b2) = {} by Th38
.= AutMt(f1,b1,b2) by A7,Th38;
hence thesis;
end;
suppose
A8: len b1 > 0;
hence width AutMt(f1+f2,b1,b2) = len b2 by Th39
.= width AutMt(f1,b1,b2) by A8,Th39;
end;
end;
then
A9: width AutMt(f1+f2,b1,b2) = width (AutMt(f1,b1,b2) + AutMt(f2,b1,b2) )
by MATRIX_1:def 6;
len AutMt(f1,b1,b2) = len b1 by Def8
.= len AutMt(f2,b1,b2) by Def8;
then
A10: dom AutMt(f1,b1,b2) = dom AutMt(f2,b1,b2) by FINSEQ_3:29;
A11: for i,j st [i,j] in Indices AutMt(f1+f2,b1,b2) holds AutMt(f1+f2,b1,b2)
*(i,j) = (AutMt(f1,b1,b2) + AutMt(f2,b1,b2))*(i,j)
proof
let i,j;
assume
A12: [i,j] in Indices AutMt(f1+f2,b1,b2);
then
A13: [i,j] in [:dom AutMt(f1+f2,b1,b2), Seg width AutMt(f1+f2,b1,b2):] by
MATRIX_0:def 4;
then
A14: [i,j] in Indices AutMt(f1,b1,b2) by A2,A6,MATRIX_0:def 4;
A15: [i,j] in Indices AutMt(f2,b1,b2) by A10,A3,A2,A6,A13,MATRIX_0:def 4;
AutMt(f1+f2,b1,b2)*(i,j) = AutMt(f1,b1,b2)*(i,j)+AutMt(f2,b1,b2)*(i,j )
proof
consider KL3 be Linear_Combination of V2 such that
A16: f2.(b1/.i) = Sum(KL3) & Carrier KL3 c= rng b2 and
A17: for t st 1<=t & t<=len (f2.(b1/.i) |-- b2) holds (f2.(b1/.i) |-- b2
)/.t=KL3.(b2/.t) by Def7;
consider KL2 be Linear_Combination of V2 such that
A18: f1.(b1/.i) = Sum(KL2) & Carrier KL2 c= rng b2 and
A19: for t st 1<=t & t<=len (f1.(b1/.i) |-- b2) holds (f1.(b1/.i) |-- b2
)/.t=KL2.(b2/.t) by Def7;
A20: i in dom AutMt(f1+f2,b1,b2) by A13,ZFMISC_1:87;
then
A21: i in dom b1 by Lm3;
reconsider b4 = rng b2 as Basis of V2 by Def2;
consider p1 be FinSequence of K such that
A22: p1 = AutMt(f1+f2,b1,b2).i and
A23: AutMt(f1+f2,b1,b2)*(i,j) = p1.j by A12,MATRIX_0:def 5;
consider KL1 be Linear_Combination of V2 such that
A24: (f1+f2).(b1/.i) = Sum(KL1) & Carrier KL1 c= rng b2 and
A25: for t st 1<=t & t<=len ((f1+f2).(b1/.i) |-- b2) holds ((f1+f2).(
b1/.i) |-- b2)/.t=KL1.(b2/.t) by Def7;
b4 is linearly-independent & (f1+f2).(b1/.i) = f1.(b1/.i) + f2.(b1
/.i) by Def3,VECTSP_7:def 3;
then
A26: KL1.(b2/.j) = (KL2 + KL3).(b2/.j) by A24,A18,A16,Th6
.= KL2.(b2/.j) + KL3.(b2/.j) by VECTSP_6:22;
A27: p1 = (AutMt(f1+f2,b1,b2))/.i by A22,A20,PARTFUN1:def 6
.= (f1+f2).(b1/.i) |-- b2 by A21,Def8;
consider p3 be FinSequence of K such that
A28: p3 = (AutMt(f2,b1,b2)).i and
A29: AutMt(f2,b1,b2)*(i,j) = p3.j by A15,MATRIX_0:def 5;
consider p2 be FinSequence of K such that
A30: p2 = (AutMt(f1,b1,b2)).i and
A31: AutMt(f1,b1,b2)*(i,j) = p2.j by A14,MATRIX_0:def 5;
A32: j in Seg width AutMt(f1+f2,b1,b2) by A13,ZFMISC_1:87;
then A33: 1<=j by FINSEQ_1:1;
len b1 = len AutMt(f1+f2,b1,b2) by Def8;
then dom b1 = dom AutMt(f1+f2,b1,b2) by FINSEQ_3:29;
then dom b1 <> {} by A13,ZFMISC_1:87;
then Seg len b1 <> {} by FINSEQ_1:def 3;
then len b1 > 0;
then
A34: j in Seg len b2 by A32,Th39;
then
A35: j<=len b2 by FINSEQ_1:1;
then j<=len ((f1+f2).(b1/.i) |-- b2) by Def7;
then
A36: p1/.j = KL1.(b2/.j) by A33,A27,A25;
A37: j in dom b2 by A34,FINSEQ_1:def 3;
i in dom AutMt(f2,b1,b2) by A21,Lm3;
then
A38: p3 = AutMt(f2,b1,b2)/.i by A28,PARTFUN1:def 6
.= f2.(b1/.i) |-- b2 by A21,Def8;
then j in dom p3 by A37,Lm1;
then
A39: AutMt(f2,b1,b2)*(i,j) = p3/.j by A29,PARTFUN1:def 6;
i in dom AutMt(f1,b1,b2) by A21,Lm3;
then
A40: p2 = (AutMt(f1,b1,b2))/.i by A30,PARTFUN1:def 6
.= f1.(b1/.i) |-- b2 by A21,Def8;
then j in dom p2 by A37,Lm1;
then
A41: AutMt(f1,b1,b2)*(i,j) = p2/.j by A31,PARTFUN1:def 6;
j<=len (f2.(b1/.i) |-- b2) by A35,Def7;
then
A42: p3/.j = KL3.(b2/.j) by A33,A38,A17;
j<=len (f1.(b1/.i) |-- b2) by A35,Def7;
then
A43: p2/.j = KL2.(b2/.j) by A33,A40,A19;
j in dom p1 by A37,A27,Lm1;
hence thesis by A23,A41,A39,A36,A43,A42,A26,PARTFUN1:def 6;
end;
hence thesis by A14,MATRIX_1:def 6;
end;
len AutMt(f1+f2,b1,b2) = len (AutMt(f1,b1,b2) + AutMt(f2,b1,b2)) by A1,
MATRIX_1:def 6;
hence thesis by A9,A11,MATRIX_0:21;
end;
theorem
a <> 0.K implies AutMt(a*f,b1,b2) = a * AutMt(f,b1,b2)
proof
assume
A1: a <> 0.K;
A2: width AutMt(a*f,b1,b2) = width AutMt(f,b1,b2)
proof
per cases;
suppose
A3: len b1 = 0;
then AutMt(a*f,b1,b2) = {} by Th38
.= AutMt(f,b1,b2) by A3,Th38;
hence thesis;
end;
suppose
A4: len b1 > 0;
hence width AutMt(a*f,b1,b2) = len b2 by Th39
.= width AutMt(f,b1,b2) by A4,Th39;
end;
end;
then
A5: width AutMt(a*f,b1,b2) = width (a * AutMt(f,b1,b2)) by MATRIX_3:def 5;
A6: len AutMt(a*f,b1,b2) = len b1 by Def8
.= len AutMt(f,b1,b2) by Def8;
then
A7: dom AutMt(a*f,b1,b2) = dom AutMt(f,b1,b2) by FINSEQ_3:29;
A8: for i,j st [i,j] in Indices AutMt(a*f,b1,b2) holds AutMt(a*f,b1,b2)*(i,
j) = (a * AutMt(f,b1,b2))*(i,j)
proof
let i,j;
assume
A9: [i,j] in Indices AutMt(a*f,b1,b2);
then
A10: [i,j] in [:dom AutMt(a*f,b1,b2),Seg width AutMt(a*f,b1,b2):] by
MATRIX_0:def 4;
then
A11: [i,j] in Indices AutMt(f,b1,b2) by A7,A2,MATRIX_0:def 4;
AutMt(a*f,b1,b2)*(i,j) = a * (AutMt(f,b1,b2)*(i,j))
proof
consider p2 be FinSequence of K such that
A12: p2 = (AutMt(f,b1,b2)).i and
A13: AutMt(f,b1,b2)*(i,j) = p2.j by A11,MATRIX_0:def 5;
A14: i in dom AutMt(a*f,b1,b2) by A10,ZFMISC_1:87;
then
A15: i in dom b1 by Lm3;
then i in dom AutMt(f,b1,b2) by Lm3;
then
A16: p2 = (AutMt(f,b1,b2))/.i by A12,PARTFUN1:def 6
.= f.(b1/.i) |-- b2 by A15,Def8;
reconsider b4 = rng b2 as Basis of V2 by Def2;
consider p1 be FinSequence of K such that
A17: p1 = AutMt(a*f,b1,b2).i and
A18: AutMt(a*f,b1,b2)*(i,j) = p1.j by A9,MATRIX_0:def 5;
consider KL1 be Linear_Combination of V2 such that
A19: (a*f).(b1/.i) = Sum(KL1) & Carrier KL1 c= rng b2 and
A20: for t st 1<=t & t<=len ((a*f).(b1/.i) |-- b2) holds ((a*f).(b1/.i)
|-- b2)/.t=KL1.(b2/.t) by Def7;
consider KL2 be Linear_Combination of V2 such that
A21: f.(b1/.i) = Sum(KL2) & Carrier KL2 c= rng b2 and
A22: for t st 1<=t & t<=len (f.(b1/.i) |-- b2) holds (f.(b1/.i) |-- b2)
/.t= KL2.(b2/.t) by Def7;
b4 is linearly-independent & (a*f).(b1/.i) = a * (f.(b1/.i)) by Def4,
VECTSP_7:def 3;
then
A23: KL1.(b2/.j) = (a * KL2).(b2/.j) by A1,A19,A21,Th7
.= a * KL2.(b2/.j) by VECTSP_6:def 9;
A24: j in Seg width AutMt(a*f,b1,b2) by A10,ZFMISC_1:87;
then
A25: 1<=j by FINSEQ_1:1;
len b1 = len AutMt(a*f,b1,b2) by Def8;
then dom b1 = dom AutMt(a*f,b1,b2) by FINSEQ_3:29;
then dom b1 <> {} by A10,ZFMISC_1:87;
then Seg len b1 <> {} by FINSEQ_1:def 3;
then len b1 > 0;
then
A26: j in Seg len b2 by A24,Th39;
then
A27: j<=len b2 by FINSEQ_1:1;
then j<=len (f.(b1/.i) |-- b2) by Def7;
then
A28: p2/.j = KL2.(b2/.j) by A25,A16,A22;
A29: j in dom b2 by A26,FINSEQ_1:def 3;
then j in dom (f.(b1/.i) |-- b2) by Lm1;
then
A30: AutMt(f,b1,b2)*(i,j) = p2/.j by A13,A16,PARTFUN1:def 6;
A31: p1 = (AutMt(a*f,b1,b2))/.i by A17,A14,PARTFUN1:def 6
.= (a*f).(b1/.i) |-- b2 by A15,Def8;
then
A32: j in dom p1 by A29,Lm1;
j<=len ((a*f).(b1/.i) |-- b2) by A27,Def7;
then p1/.j = KL1.(b2/.j) by A25,A31,A20;
hence thesis by A18,A32,A30,A28,A23,PARTFUN1:def 6;
end;
hence thesis by A11,MATRIX_3:def 5;
end;
len AutMt(a*f,b1,b2) = len (a * AutMt(f,b1,b2)) by A6,MATRIX_3:def 5;
hence thesis by A5,A8,MATRIX_0:21;
end;