:: Linear Map of Matrices
:: by Karol P\c{a}k
::
:: Received May 13, 2008
:: Copyright (c) 2008-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, VECTSP_1, SUBSET_1, RLSUB_1, XBOOLE_0, ARYTM_3,
STRUCT_0, TARSKI, RLVECT_3, RLVECT_2, CARD_3, SUPINF_2, FINSET_1,
FUNCT_1, RLSUB_2, FUNCT_2, RLVECT_5, MATRLIN, RELAT_1, CARD_1, XXREAL_0,
FINSEQ_1, ZFMISC_1, ALGSTR_0, PARTFUN1, ORDINAL4, FINSEQ_2, INCSP_1,
MESFUNC1, TREES_1, MATRIX_1, GROUP_1, ARYTM_1, FINSEQ_4, RFINSEQ,
RANKNULL, MATRIXJ1, MATRIX_3, MATRIX_6, FVSUM_1, RVSUM_1, MATRIXR1,
VECTSP10, MATRIX15, QC_LANG1, CLASSES1, PRVECT_1, MATRIX13, LMOD_7,
VALUED_1, RLVECT_1, BINOP_1, LATTICES, MATRLIN2, UNIALG_1, MSSUBFAM,
MATRIX_0, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_1,
XCMPLX_0, ALGSTR_0, XXREAL_0, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, NAT_1, FINSEQ_1, BINOP_1, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1,
FINSEQ_2, MATRIX_0, MATRIX_1, FVSUM_1, MATRIX_3, MATRIX_6, DOMAIN_1,
VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, FINSEQOP, PRVECT_1, MATRIX13,
MATRLIN, MATRIX15, RFINSEQ, WSIERP_1, MOD_2, VECTSP_5, RANKNULL,
MATRIXJ1, GCD_1;
constructors FVSUM_1, VECTSP_9, MATRIX_6, LAPLACE, MATRIX15, VECTSP_2, GCD_1,
RANKNULL, VECTSP10, MATRIXJ1, REALSET1, RELSET_1, MATRIX13, MATRIX_1,
MATRIX_3;
registrations XBOOLE_0, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, FUNCT_2,
ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, FINSEQ_2, MATRLIN,
VECTSP_2, MATRIX13, XREAL_0, VECTSP_9, CARD_1, MOD_2, PRVECT_1, GRCAT_1,
MATRIX_6, MATRIX_1, MATRIX_3, LAPLACE;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI, FUNCT_1, VECTSP_7, VECTSP_6;
equalities STRUCT_0, RLVECT_1, FINSEQ_1, VECTSP_4, FVSUM_1, VECTSP_1,
MATRIX_0, MATRIX13, MATRLIN, MATRIX15, RANKNULL, VECTSP_6, ORDINAL1;
expansions STRUCT_0, TARSKI, FINSEQ_1, VECTSP_1, FUNCT_1, VECTSP_7;
theorems ZFMISC_1, RLVECT_1, MATRIX_0, MATRIX_4, MATRIX_3, VECTSP_1, NAT_1,
FINSEQ_2, CARD_1, FINSEQ_1, FINSEQ_3, FINSEQOP, FUNCT_1, FUNCT_2,
FUNCOP_1, FVSUM_1, LAPLACE, MATRIX_6, MATRIX_7, MATRIX11, MATRIX13,
MATRIXR1, MATRIXR2, MATRLIN, ORDINAL1, PARTFUN1, RELAT_1, STRUCT_0,
TARSKI, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, XBOOLE_0, XBOOLE_1,
XXREAL_0, MATRIX15, MOD_2, RLVECT_2, VECTSP10, MATRIX_8, RANKNULL,
VECTSP_5, FINSEQ_5, RFINSEQ, MATRIXJ1, MATRIX_1, CARD_2;
schemes NAT_1, MATRIX_0, FUNCT_2, FINSEQ_2;
begin :: Preliminaries
reserve i, j, m, n, k for Nat,
x, y for set,
K for Field,
a,a1 for Element of K;
theorem Th1:
for V be VectSp of K for W1,W2,W12 be Subspace of V for U1,U2 be
Subspace of W12 st U1 = W1 & U2 = W2 holds W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 +
U2
proof
let V be VectSp of K;
let W1,W2,W12 be Subspace of V;
let U1,U2 be Subspace of W12 such that
A1: U1 = W1 and
A2: U2 = W2;
reconsider U12=U1/\U2 as Subspace of V by VECTSP_4:26;
A3: the carrier of U12 c= the carrier of (W1/\W2)
proof
let x be object;
assume x in the carrier of U12;
then x in U1/\U2;
then x in U1 & x in U2 by VECTSP_5:3;
then x in (W1/\W2) by A1,A2,VECTSP_5:3;
hence thesis;
end;
the carrier of (W1/\W2) c= the carrier of U12
proof
let x be object;
assume x in the carrier of (W1/\W2);
then x in W1/\W2;
then x in W1 & x in W2 by VECTSP_5:3;
then x in U12 by A1,A2,VECTSP_5:3;
hence thesis;
end;
then the carrier of (W1/\W2)=the carrier of U12 by A3,XBOOLE_0:def 10;
hence W1/\W2=U1/\U2 by VECTSP_4:29;
reconsider U12=U1+U2 as Subspace of V by VECTSP_4:26;
A4: the carrier of (W1+W2) c= the carrier of U12
proof
let x be object;
assume x in the carrier of (W1+W2);
then x in W1+W2;
then consider v1,v2 be Vector of V such that
A5: v1 in W1 and
A6: v2 in W2 and
A7: v1+v2=x by VECTSP_5:1;
U2 is Subspace of U12 by VECTSP_5:7;
then
A8: v2 in U12 by A2,A6,VECTSP_4:8;
U1 is Subspace of U12 by VECTSP_5:7;
then v1 in U12 by A1,A5,VECTSP_4:8;
then reconsider w1=v1,w2=v2 as Vector of U12 by A8;
v1+v2=w1+w2 by VECTSP_4:13;
hence thesis by A7;
end;
the carrier of U12 c= the carrier of (W1+W2)
proof
let x be object;
assume x in the carrier of U12;
then x in U1+U2;
then consider v1,v2 be Vector of W12 such that
A9: v1 in U1 & v2 in U2 & v1+v2=x by VECTSP_5:1;
reconsider w1=v1,w2=v2 as Vector of V by VECTSP_4:10;
v1+v2=w1+w2 by VECTSP_4:13;
then x in W1+W2 by A1,A2,A9,VECTSP_5:1;
hence thesis;
end;
then the carrier of (W1+W2)=the carrier of U12 by A4,XBOOLE_0:def 10;
hence thesis by VECTSP_4:29;
end;
theorem Th2:
for V be VectSp of K for W1,W2 be Subspace of V st W1/\W2=(0).V
for B1 be linearly-independent Subset of W1, B2 be linearly-independent Subset
of W2 holds B1\/B2 is linearly-independent Subset of W1+W2
proof
let V be VectSp of K;
let W1,W2 be Subspace of V such that
A1: W1/\W2=(0).V;
reconsider W19=W1,W29=W2 as Subspace of W1+W2 by VECTSP_5:7;
let B1 be linearly-independent Subset of W1;
let B2 be linearly-independent Subset of W2;
A2: W2 is Subspace of W1+W2 by VECTSP_5:7;
then the carrier of W2 c= the carrier of W1+W2 by VECTSP_4:def 2;
then
A3: B2 c= the carrier of W1+W2;
A4: W1 is Subspace of W1+W2 by VECTSP_5:7;
then the carrier of W1 c= the carrier of W1+W2 by VECTSP_4:def 2;
then B1 c= the carrier of W1+W2;
then reconsider B12=B1\/B2,B19=B1,B29=B2 as Subset of (W1+W2) by A3,
XBOOLE_1:8;
B12 is linearly-independent
proof
let L be Linear_Combination of B12;
assume Sum(L)=0.(W1+W2);
then
A5: Sum L=0.(W1+W2)+0.(W1+W2) by RLVECT_1:def 4;
set C = Carrier(L) /\ B1;
defpred P[object] means $1 in C;
C c= Carrier L by XBOOLE_1:17;
then reconsider C as finite Subset of W1+W2 by XBOOLE_1:1;
set D = Carrier(L) \ B1;
deffunc G(object) = L.$1;
defpred C[object] means $1 in D;
reconsider D as finite Subset of W1+W2;
A6: D c= B29
proof
let x be object;
assume x in D;
then
A7: x in Carrier(L) & not x in B19 by XBOOLE_0:def 5;
Carrier(L) c= B12 by VECTSP_6:def 4;
hence thesis by A7,XBOOLE_0:def 3;
end;
(0).V=(0).(W1+W2) by VECTSP_4:36;
then
A8: W19/\W29=(0).(W1+W2) by A1,Th1;
W19+W29=W1+W2 by Th1;
then
A9: W1+W2 is_the_direct_sum_of W19,W29 by A8,VECTSP_5:def 4;
A10: B29 is linearly-independent by A2,VECTSP_9:11;
A11: B19 is linearly-independent by A4,VECTSP_9:11;
deffunc F(object) = 0.K;
A12: 0.W1 in W19 & 0.W2 in W29;
A13: now
let x be object;
assume x in the carrier of W1+W2;
then reconsider v = x as Vector of W1+W2;
L.v in the carrier of K;
hence P[x] implies G(x) in the carrier of K;
assume not P[x];
thus F(x) in the carrier of K;
end;
consider f be Function of the carrier of W1+W2, the carrier of K such that
A14: for x being object st x in the carrier of W1+W2
holds (P[x] implies f.x = G(x)
) & (not P[x] implies f.x = F(x)) from FUNCT_2:sch 5(A13);
deffunc G(object) = L.$1;
A15: now
let x be object;
assume x in the carrier of W1+W2;
then reconsider v = x as Vector of W1+W2;
L.v in the carrier of K;
hence C[x] implies G(x) in the carrier of K;
assume not C[x];
thus F(x) in the carrier of K;
end;
consider g be Function of the carrier of W1+W2, the carrier of K such that
A16: for x being object st x in the carrier of W1+W2
holds (C[x] implies g.x = G(x)
) & (not C[x] implies g.x = F(x)) from FUNCT_2:sch 5(A15);
reconsider g as Element of Funcs(the carrier of W1+W2, the carrier of K)
by FUNCT_2:8;
for u be Vector of W1+W2 holds not u in D implies g.u = 0.K by A16;
then reconsider g as Linear_Combination of W1+W2 by VECTSP_6:def 1;
A17: Carrier(g) c= D
proof
let x be object;
assume x in Carrier(g);
then
A18: ex u be Vector of W1+W2 st x = u & g.u <> 0.K;
assume not x in D;
hence thesis by A16,A18;
end;
then Carrier(g) c= B29 by A6;
then reconsider g as Linear_Combination of B29 by VECTSP_6:def 4;
reconsider f as Element of Funcs(the carrier of W1+W2, the carrier of K)
by FUNCT_2:8;
for u be Vector of W1+W2 holds not u in C implies f.u = 0.K by A14;
then reconsider f as Linear_Combination of W1+W2 by VECTSP_6:def 1;
A19: Carrier(f) c= B19
proof
let x be object;
assume x in Carrier(f);
then
A20: ex u be Vector of W1+W2 st x = u & f.u <> 0.K;
assume not x in B19;
then not x in C by XBOOLE_0:def 4;
hence thesis by A14,A20;
end;
then reconsider f as Linear_Combination of B19 by VECTSP_6:def 4;
ex f1 be Linear_Combination of W19 st Carrier(f1) = Carrier(f) & Sum(
f) = Sum (f1) by A19,VECTSP_9:9,XBOOLE_1:1;
then
A21: Sum f in W19;
A22: L = f + g
proof
let v be Vector of W1+W2;
now
per cases;
suppose
A23: v in C;
A24: now
assume v in D;
then not v in B19 by XBOOLE_0:def 5;
hence contradiction by A23,XBOOLE_0:def 4;
end;
thus (f + g).v = f.v + g.v by VECTSP_6:22
.= L.v + g.v by A14,A23
.= L.v + 0.K by A16,A24
.= L.v by RLVECT_1:4;
end;
suppose
A25: not v in C;
now
per cases;
suppose
A26: v in Carrier(L);
A27: now
assume not v in D;
then not v in Carrier(L) or v in B19 by XBOOLE_0:def 5;
hence contradiction by A25,A26,XBOOLE_0:def 4;
end;
thus (f + g). v = f.v + g.v by VECTSP_6:22
.= g.v + 0.K by A14,A25
.= g.v by RLVECT_1:4
.= L.v by A16,A27;
end;
suppose
A28: not v in Carrier(L);
then
A29: not v in D by XBOOLE_0:def 5;
A30: not v in C by A28,XBOOLE_0:def 4;
thus (f + g).v = f.v + g.v by VECTSP_6:22
.= 0.K + g.v by A14,A30
.= 0.K + 0.K by A16,A29
.= 0.K by RLVECT_1:4
.= L.v by A28;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A31: Sum L = Sum(f) + Sum(g) by VECTSP_6:44;
Carrier g c= B2 by A17,A6;
then
ex g1 be Linear_Combination of W29 st Carrier(g1) = Carrier(g) & Sum(
g) = Sum (g1) by VECTSP_9:9,XBOOLE_1:1;
then
A32: Sum g in W29;
A33: 0.(W1+W2)=0.W19 & 0.(W1+W2)=0.W29 by VECTSP_4:11;
then Sum f=0.(W1+W2) by A31,A21,A32,A9,A12,A5,VECTSP_5:48;
then
A34: Carrier f={} by A11;
Sum g=0.(W1+W2) by A31,A21,A32,A9,A33,A12,A5,VECTSP_5:48;
then
A35: Carrier g={} by A10;
{}\/{}={};
hence thesis by A22,A34,A35,VECTSP_6:23,XBOOLE_1:3;
end;
hence thesis;
end;
theorem Th3:
for V be VectSp of K for W1,W2 be Subspace of V st W1/\W2 = (0).V
for B1 be Basis of W1,B2 be Basis of W2 holds B1\/B2 is Basis of W1+W2
proof
let V be VectSp of K;
let W1,W2 be Subspace of V such that
A1: W1/\W2=(0).V;
let B1 be Basis of W1,B2 be Basis of W2;
A2: W2 is Subspace of W1+W2 by VECTSP_5:7;
then the carrier of W2 c= the carrier of W1+W2 by VECTSP_4:def 2;
then
A3: B2 c= the carrier of W1+W2;
A4: W1 is Subspace of W1+W2 by VECTSP_5:7;
then the carrier of W1 c= the carrier of W1+W2 by VECTSP_4:def 2;
then B1 c= the carrier of W1+W2;
then reconsider B12=B1\/B2,B19=B1,B29=B2 as Subset of W1+W2 by A3,XBOOLE_1:8;
A5: (Omega).W2 = Lin(B2) by VECTSP_7:def 3
.= Lin(B29) by A2,VECTSP_9:17;
A6: Lin(B12) = Lin(B19)+Lin(B29) by VECTSP_7:15;
A7: (Omega).W1 = Lin(B1) by VECTSP_7:def 3
.= Lin(B19) by A4,VECTSP_9:17;
A8: the carrier of W1+W2 c= the carrier of Lin(B12)
proof
let x be object such that
A9: x in the carrier of W1+W2;
reconsider x as Vector of W1+W2 by A9;
x in W1+W2;
then consider v1,v2 be Vector of V such that
A10: v1 in W1 and
A11: v2 in W2 and
A12: x=v1+v2 by VECTSP_5:1;
v1 is Vector of W1 & v2 is Vector of W2 by A10,A11;
then reconsider w1 = v1,w2 = v2 as Vector of W1+W2 by A4,A2,VECTSP_4:10;
A13: v1+v2=w1+w2 by VECTSP_4:13;
v2 in the carrier of Lin(B29) by A5,A11;
then
A14: v2 in Lin(B29);
v1 in the carrier of Lin(B19) by A7,A10;
then v1 in Lin(B19);
then w1+w2 in Lin(B12) by A6,A14,VECTSP_5:1;
hence thesis by A12,A13;
end;
the carrier of Lin(B12) c= the carrier of W1+W2 by VECTSP_4:def 2;
then the carrier of Lin(B12)=the carrier of W1+W2 by A8,XBOOLE_0:def 10;
then
A15: Lin(B12) = the ModuleStr of W1+W2 by VECTSP_4:31;
B2 is linearly-independent & B1 is linearly-independent by VECTSP_7:def 3;
then B1\/B2 is linearly-independent Subset of W1+W2 by A1,Th2;
hence thesis by A15,VECTSP_7:def 3;
end;
theorem
for V be finite-dimensional VectSp of K, B be OrdBasis of (Omega).V
holds B is OrdBasis of V
proof
let V be finite-dimensional VectSp of K, B be OrdBasis of (Omega).V;
reconsider r=rng B as Basis of (Omega).V by MATRLIN:def 2;
r is linearly-independent by VECTSP_7:def 3;
then reconsider R=r as linearly-independent Subset of V by VECTSP_9:11;
Lin R = Lin r by VECTSP_9:17
.= the ModuleStr of V by VECTSP_7:def 3;
then R is Basis of V by VECTSP_7:def 3;
hence thesis by MATRLIN:def 2;
end;
theorem
for V1 be VectSp of K for A be finite Subset of V1 st dim Lin(A) =
card A holds A is linearly-independent
proof
let V1 be VectSp of K;
let A be finite Subset of V1 such that
A1: dim Lin(A) = card A;
set L=Lin(A);
A c= the carrier of L
proof
let x be object;
assume x in A;
then x in L by VECTSP_7:8;
hence thesis;
end;
then reconsider A9=A as Subset of L;
Lin(A9)=L by VECTSP_9:17;
then consider B be Subset of L such that
A2: B c= A9 and
A3: B is linearly-independent and
A4: Lin(B) = L by VECTSP_7:18;
reconsider B as finite Subset of L by A2;
B is Basis of L by A3,A4,VECTSP_7:def 3;
then reconsider L as finite-dimensional VectSp of K by MATRLIN:def 1;
card A = dim L by A1
.= card B by A3,A4,VECTSP_9:26;
then A=B by A2,CARD_2:102;
hence thesis by A3,VECTSP_9:11;
end;
theorem
for V be VectSp of K for A be finite Subset of V holds dim Lin A <= card A
proof
let V be VectSp of K;
let A be finite Subset of V;
set L=Lin(A);
A c= the carrier of L
proof
let x be object;
assume x in A;
then x in L by VECTSP_7:8;
hence thesis;
end;
then reconsider A9=A as Subset of L;
Lin(A9)=L by VECTSP_9:17;
then consider B be Subset of L such that
A1: B c= A9 and
A2: B is linearly-independent & Lin(B) = L by VECTSP_7:18;
reconsider B as finite Subset of L by A1;
B is Basis of L by A2,VECTSP_7:def 3;
then reconsider L as finite-dimensional VectSp of K by MATRLIN:def 1;
card B = dim L & Segm card B c= Segm card A by A1,A2,CARD_1:11,VECTSP_9:26;
hence thesis by NAT_1:39;
end;
begin :: More on the Product of Finite Sequence of Scalars and Vectors
reserve V1,V2,V3 for finite-dimensional VectSp of K,
f for Function of V1,V2,
b1,b19 for OrdBasis of V1,
B1 for FinSequence of V1,
b2 for OrdBasis of V2,
B2 for FinSequence of V2,
B3 for FinSequence of V3,
v1,w1 for Element of V1,
R,R1,R2 for FinSequence of V1,
p,p1,p2 for FinSequence of K;
Lm1: dom lmlt(p,R)=(dom p)/\(dom R)
proof
rng p c= the carrier of K & rng R c= the carrier of V1 by FINSEQ_1:def 4;
then [:rng p,rng R:]c=[:the carrier of K,the carrier of V1:] by ZFMISC_1:96;
then [:rng p, rng R:] c= dom (the lmult of V1) by FUNCT_2:def 1;
hence thesis by FUNCOP_1:69;
end;
Lm2: dom (p1+p2)=(dom p1)/\(dom p2)
proof
rng p1 c= the carrier of K & rng p2 c= the carrier of K by FINSEQ_1:def 4;
then [:rng p1,rng p2:]c=[:the carrier of K,the carrier of K:]by ZFMISC_1:96;
then [:rng p1, rng p2:] c= dom (the addF of K) by FUNCT_2:def 1;
hence thesis by FUNCOP_1:69;
end;
Lm3: dom (R1+R2)=(dom R1)/\(dom R2)
proof
rng R1 c= the carrier of V1 & rng R2 c= the carrier of V1 by FINSEQ_1:def 4;
then [:rng R1,rng R2:]c=[:the carrier of V1,the carrier of V1:] by
ZFMISC_1:96;
then [:rng R1, rng R2:] c= dom (the addF of V1) by FUNCT_2:def 1;
hence thesis by FUNCOP_1:69;
end;
theorem Th7:
lmlt(p1 + p2,R) = lmlt(p1,R) + lmlt(p2,R)
proof
set L12=lmlt(p1+p2,R);
set L1=lmlt(p1,R);
set L2=lmlt(p2,R);
A1: dom (L1+L2)=dom L1/\dom L2 by Lm3;
A2: dom L12=dom (p1+p2)/\dom R by Lm1;
A3: dom L1=dom p1/\dom R by Lm1;
A4: dom L2=dom p2/\dom R by Lm1;
then
A5: dom(L1+L2) = dom p1/\dom R/\dom p2/\dom R by A1,A3,XBOOLE_1:16
.= dom p1/\dom p2/\dom R/\dom R by XBOOLE_1:16
.= (dom p1/\dom p2)/\(dom R/\dom R) by XBOOLE_1:16
.= dom L12 by A2,Lm2;
now
let x be object such that
A6: x in dom (L1+L2);
A7: x in dom L2 by A1,A6,XBOOLE_0:def 4;
then
A8: L2/.x=L2.x by PARTFUN1:def 6;
x in dom p2 by A4,A7,XBOOLE_0:def 4;
then
A9: p2/.x=p2.x by PARTFUN1:def 6;
A10: x in dom (p1+p2) by A2,A5,A6,XBOOLE_0:def 4;
then
A11: (p1+p2).x=(p1+p2)/.x by PARTFUN1:def 6;
A12: x in dom L1 by A1,A6,XBOOLE_0:def 4;
then x in dom p1 by A3,XBOOLE_0:def 4;
then
A13: p1/.x=p1.x by PARTFUN1:def 6;
x in dom R by A3,A12,XBOOLE_0:def 4;
then
A14: R/.x=R.x by PARTFUN1:def 6;
A15: L1/.x=L1.x by A12,PARTFUN1:def 6;
hence (L1+L2).x = L1/.x+L2/.x by A6,A8,FVSUM_1:17
.= (the lmult of V1).(p1/.x,R/.x)+L2/.x by A12,A15,A13,A14,FUNCOP_1:22
.= ((p1/.x)*(R/.x))+((p2/.x)*(R/.x)) by A7,A8,A9,A14,FUNCOP_1:22
.= (p1/.x+p2/.x)*R/.x by VECTSP_1:def 15
.= (p1+p2)/.x*R/.x by A10,A13,A9,A11,FVSUM_1:17
.= L12.x by A5,A6,A14,A11,FUNCOP_1:22;
end;
hence thesis by A5;
end;
theorem
lmlt(p,R1 + R2) = lmlt(p,R1) + lmlt(p,R2)
proof
set L12=lmlt(p,R1+R2);
set L1=lmlt(p,R1);
set L2=lmlt(p,R2);
A1: dom (L1+L2)=dom L1/\dom L2 by Lm3;
A2: dom L12=dom p/\dom (R1+R2) by Lm1;
A3: dom (R1+R2)=dom R1/\dom R2 by Lm3;
A4: dom L1=dom p/\dom R1 by Lm1;
A5: dom L2=dom p/\dom R2 by Lm1;
then
A6: dom(L1+L2) = dom p/\dom R1/\dom p/\dom R2 by A1,A4,XBOOLE_1:16
.= dom p/\dom p/\dom R1/\dom R2 by XBOOLE_1:16
.= dom L12 by A3,A2,XBOOLE_1:16;
now
let x be object such that
A7: x in dom (L1+L2);
A8: x in dom L2 by A1,A7,XBOOLE_0:def 4;
then
A9: L2/.x=L2.x by PARTFUN1:def 6;
x in dom R2 by A5,A8,XBOOLE_0:def 4;
then
A10: R2/.x=R2.x by PARTFUN1:def 6;
A11: x in dom (R1+R2) by A2,A6,A7,XBOOLE_0:def 4;
then
A12: (R1+R2).x=(R1+R2)/.x by PARTFUN1:def 6;
A13: x in dom L1 by A1,A7,XBOOLE_0:def 4;
then x in dom p by A4,XBOOLE_0:def 4;
then
A14: p/.x=p.x by PARTFUN1:def 6;
x in dom R1 by A4,A13,XBOOLE_0:def 4;
then
A15: R1/.x=R1.x by PARTFUN1:def 6;
A16: L1/.x=L1.x by A13,PARTFUN1:def 6;
hence (L1+L2).x = L1/.x+L2/.x by A7,A9,FVSUM_1:17
.= (the lmult of V1).(p/.x,R1/.x)+L2/.x by A13,A16,A14,A15,FUNCOP_1:22
.= ((p/.x)*(R1/.x))+((p/.x)*(R2/.x)) by A8,A9,A14,A10,FUNCOP_1:22
.= p/.x*(R1/.x+R2/.x) by VECTSP_1:def 14
.= p/.x*(R1+R2)/.x by A11,A15,A10,A12,FVSUM_1:17
.= L12.x by A6,A7,A14,A12,FUNCOP_1:22;
end;
hence thesis by A6;
end;
theorem Th9:
len p1 = len R1 & len p2 = len R2 implies lmlt(p1^p2,R1^R2) =
lmlt(p1,R1)^lmlt(p2,R2)
proof
assume that
A1: len p1=len R1 and
A2: len p2=len R2;
reconsider r2=R2 as Element of (len p2)-tuples_on the carrier of V1 by A2,
FINSEQ_2:92;
reconsider r1=R1 as Element of (len p1)-tuples_on the carrier of V1 by A1,
FINSEQ_2:92;
reconsider P1=p1 as Element of (len p1)-tuples_on the carrier of K by
FINSEQ_2:92;
reconsider P2=p2 as Element of (len p2)-tuples_on the carrier of K by
FINSEQ_2:92;
thus lmlt(p1^p2,R1^R2) = ((the lmult of V1).:(P1,r1))^((the lmult of V1).:(
P2,r2)) by FINSEQOP:11
.= lmlt(p1,R1)^lmlt(p2,R2);
end;
theorem
len R1 = len R2 implies Sum (R1+R2)=Sum R1 + Sum R2
proof
assume len R1=len R2;
then reconsider
r1=R1,r2=R2 as Element of (len R1)-tuples_on the carrier of V1 by FINSEQ_2:92
;
thus Sum (R1+R2) = Sum (r1+r2) .= Sum R1+Sum R2 by FVSUM_1:76;
end;
theorem
Sum lmlt(len R|->a,R) = a * Sum R
proof
defpred P[Nat] means for R,a st len R=$1 holds Sum lmlt(len R|->a,R) = a *
Sum R;
A1: for n st P[n] holds P[n+1]
proof
let n such that
A2: P[n];
set n1=n+1;
let R,a such that
A3: len R=n1;
A4: len (R|n)=n by A3,FINSEQ_1:59,NAT_1:11;
then
A5: dom (R|n)=Seg n by FINSEQ_1:def 3;
1<=n1 by NAT_1:11;
then n1 in dom R by A3,FINSEQ_3:25;
then
A6: R/.n1=R.n1 by PARTFUN1:def 6;
A7: lmlt(<*a*>,<*R/.n1*>) = <*a*R/.n1*> by FINSEQ_2:74;
A8: len <*a*>=1 & len <*R.n1*>=1 by FINSEQ_1:39;
A9: (n1|->a)=(n|->a)^<*a*> & len (n|->a)=n by CARD_1:def 7,FINSEQ_2:60;
R=(R|n)^<*R.n1*> by A3,FINSEQ_3:55;
hence
Sum lmlt(len R|->a,R) = Sum(lmlt(n|->a,R|n)^lmlt(<*a*>,<*R/.n1*>)) by A3,A6
,A4,A9,A8,Th9
.= Sum lmlt(n|->a,R|n) + Sum lmlt(<*a*>,<*R/.n1*>) by RLVECT_1:41
.= a*Sum (R|n)+Sum <*a*R/.n1*> by A2,A4,A7
.= a*Sum (R|n)+ a* R/.n1 by RLVECT_1:44
.= a*(Sum (R|n)+R/.n1) by VECTSP_1:def 14
.= a* Sum R by A3,A6,A4,A5,RLVECT_1:38;
end;
A10: P[0]
proof
let R,a such that
A11: len R=0;
set L=len R|->a;
set M=lmlt(L,R);
len L=len R by CARD_1:def 7;
then dom L=dom R by FINSEQ_3:29;
then dom M=dom R by MATRLIN:12;
then len R=len M by FINSEQ_3:29;
then M=<*>(the carrier of V1) by A11;
then
A12: Sum M=0.V1 by RLVECT_1:43;
R=<*>(the carrier of V1) by A11;
then Sum R=0.V1 by RLVECT_1:43;
hence thesis by A12,VECTSP_1:14;
end;
for n holds P[n] from NAT_1:sch 2(A10,A1);
hence thesis;
end;
theorem
Sum lmlt(p,len p|->v1) = (Sum p) * v1
proof
set L=len p|->v1;
set M=lmlt(p,L);
len L = len p by CARD_1:def 7;
then dom L=dom p by FINSEQ_3:29;
then
A1: dom M=dom p by MATRLIN:12;
A2: now
let k, a1 such that
A3: k in dom M and
A4: a1=p.k;
k in Seg len p by A1,A3,FINSEQ_1:def 3;
then L.k=v1 by FINSEQ_2:57;
hence M.k = a1*v1 by A3,A4,FUNCOP_1:22;
end;
len p=len M by A1,FINSEQ_3:29;
hence thesis by A2,MATRLIN:9;
end;
theorem
Sum lmlt(a*p,R) = a * Sum lmlt(p,R)
proof
set Ma=lmlt(a*p,R);
set M=lmlt(p,R);
len (a*p)=len p by MATRIXR1:16;
then
A1: dom (a*p)=dom p by FINSEQ_3:29;
A2: dom Ma=dom (a*p)/\dom R by Lm1;
A3: dom M=dom p /\dom R by Lm1;
A4: for k be Nat for v1 st k in dom Ma & v1 = M.k holds Ma.k = a * v1
proof
let k be Nat;
let v1 such that
A5: k in dom Ma and
A6: v1=M.k;
k in dom R by A2,A5,XBOOLE_0:def 4;
then
A7: R/.k=R.k by PARTFUN1:def 6;
k in dom p by A1,A2,A5,XBOOLE_0:def 4;
then
A8: p/.k=p.k by PARTFUN1:def 6;
k in dom (a*p) by A2,A5,XBOOLE_0:def 4;
then (a*p).k=a*(p/.k) by A8,FVSUM_1:50;
hence Ma.k = (a*(p/.k))*R/.k by A5,A7,FUNCOP_1:22
.= a*((p/.k)*R/.k) by VECTSP_1:def 16
.= a*v1 by A1,A3,A2,A5,A6,A8,A7,FUNCOP_1:22;
end;
len M=len Ma by A1,A3,A2,FINSEQ_3:29;
hence thesis by A4,RLVECT_2:66;
end;
theorem
for B1 be FinSequence of V1,W1 be Subspace of V1, B2 be FinSequence of
W1 st B1 = B2 holds lmlt(p,B1) = lmlt(p,B2)
proof
let B1 be FinSequence of V1,W1 be Subspace of V1, B2 be FinSequence of W1
such that
A1: B1 = B2;
set M2=lmlt(p,B2);
set M1=lmlt(p,B1);
A2: dom M1=dom p/\dom B1 by Lm1;
A3: dom M2=dom p/\dom B2 by Lm1;
now
let i such that
A4: i in dom M1;
i in dom p by A2,A4,XBOOLE_0:def 4;
then
A5: p.i=p/.i by PARTFUN1:def 6;
A6: i in dom B1 by A2,A4,XBOOLE_0:def 4;
then
A7: B2.i=B2/.i by A1,PARTFUN1:def 6;
A8: B1.i=B1/.i by A6,PARTFUN1:def 6;
hence M1.i = p/.i * B1/.i by A4,A5,FUNCOP_1:22
.= p/.i * B2/.i by A1,A6,A8,PARTFUN1:def 6,VECTSP_4:14
.= M2.i by A1,A2,A3,A4,A5,A7,FUNCOP_1:22;
end;
hence thesis by A1,A3,Lm1;
end;
theorem
for B1 be FinSequence of V1,W1 be Subspace of V1, B2 be FinSequence of
W1 st B1 = B2 holds Sum B1 = Sum B2
proof
let B1 be FinSequence of V1,W1 be Subspace of V1, B2 be FinSequence of W1
such that
A1: B1 = B2;
defpred P[Nat] means for B1 be FinSequence of V1,W1 be Subspace of V1, B2 be
FinSequence of W1 st B1 = B2 & len B1=$1 holds Sum B1 = Sum B2;
A2: for n st P[n] holds P[n+1]
proof
let n such that
A3: P[n];
set n1=n+1;
let B1 be FinSequence of V1,W1 be Subspace of V1, B2 be FinSequence of W1
such that
A4: B1 = B2 and
A5: len B1=n1;
A6: len (B1|n)=n by A5,FINSEQ_1:59,NAT_1:11;
then
A7: Sum (B1|n)=Sum (B2|n) by A3,A4;
1<=n1 by NAT_1:11;
then
A8: n1 in dom B1 by A5,FINSEQ_3:25;
then
A9: B2.n1=B2/.n1 by A4,PARTFUN1:def 6;
A10: B1.n1=B1/.n1 by A8,PARTFUN1:def 6;
A11: dom (B1|n)=Seg n by A6,FINSEQ_1:def 3;
hence Sum B1 = Sum (B1|n)+B1/.n1 by A5,A10,A6,RLVECT_1:38
.= Sum (B2|n)+B2/.n1 by A4,A10,A9,A7,VECTSP_4:13
.=Sum B2 by A4,A5,A9,A6,A11,RLVECT_1:38;
end;
A12: P[0]
proof
let B1 be FinSequence of V1,W1 be Subspace of V1, B2 be FinSequence of W1;
assume B1 = B2 & len B1=0;
then Sum B1=0.V1 & Sum B2=0.W1 by RLVECT_1:75;
hence thesis by VECTSP_4:11;
end;
for n holds P[n] from NAT_1:sch 2(A12,A2);
then P[len B1];
hence thesis by A1;
end;
theorem
i in dom R implies Sum lmlt(Line(1.(K,len R),i),R) = R/.i
proof
set ONE=1.(K,len R);
set L=Line(ONE,i);
set M=lmlt(L,R);
A1: width ONE=len R by MATRIX_0:24;
len L=width ONE by CARD_1:def 7;
then dom L=dom R by A1,FINSEQ_3:29;
then
A2: dom M=dom R by MATRLIN:12;
then
A3: len M=len R by FINSEQ_3:29;
consider f be sequence of the carrier of V1 such that
A4: Sum M= f.(len M) and
A5: f.0 = 0.V1 and
A6: for j be Nat, v1 st j < len M & v1 = M.(j + 1) holds f.(
j + 1) = f.j + v1 by RLVECT_1:def 12;
defpred Q[Nat] means $1<=len M implies f.$1=R/.i;
defpred P[Nat] means $1<i implies f.$1=0.V1;
assume
A7: i in dom R;
then
A8: 1<=i by FINSEQ_3:25;
len ONE=len R by MATRIX_0:24;
then
A9: dom R=dom ONE by FINSEQ_3:29;
A10: for n st i<=n holds Q[n] implies Q[n+1]
proof
let n such that
A11: i <=n;
set n1=n+1;
A12: i<n1 by A11,NAT_1:13;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
assume
A13: Q[n];
assume
A14: n1<=len M;
then
A15: n<len M by NAT_1:13;
A16: 1<=n1 by NAT_1:11;
then n1 in Seg len R by A3,A14;
then L.n1=ONE*(i,n1) & [i,n1] in Indices ONE by A7,A1,A9,MATRIX_0:def 7
,ZFMISC_1:87;
then
A17: L.n1=0.K by A12,MATRIX_1:def 3;
A18: n1 in dom R by A2,A14,A16,FINSEQ_3:25;
then R.n1=R/.n1 by PARTFUN1:def 6;
then M.n1 = 0.K * R/.n1 by A2,A18,A17,FUNCOP_1:22
.= 0.V1 by VECTSP_1:14;
hence f.n1 = f.N + 0.V1 by A6,A15
.= R/.i by A13,A14,NAT_1:13,RLVECT_1:def 4;
end;
A19: i<=len M by A7,A2,FINSEQ_3:25;
A20: for n st P[n] holds P[n+1]
proof
let n such that
A21: P[n];
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set n1=n+1;
assume
A22: n1<i;
then n1<len M by A19,XXREAL_0:2;
then
A23: n<len M by NAT_1:13;
A24: 1<=n1 & n1<=len R by A19,A3,A22,NAT_1:11,XXREAL_0:2;
then n1 in Seg len R;
then L.n1=ONE*(i,n1) & [i,n1] in Indices ONE by A7,A1,A9,MATRIX_0:def 7
,ZFMISC_1:87;
then
A25: L.n1=0.K by A22,MATRIX_1:def 3;
A26: n1 in dom R by A24,FINSEQ_3:25;
then R.n1=R/.n1 by PARTFUN1:def 6;
then M.n1 = 0.K * R/.n1 by A2,A26,A25,FUNCOP_1:22
.= 0.V1 by VECTSP_1:14;
hence f.n1 = f.N + 0.V1 by A6,A23
.= 0.V1 by A21,A22,NAT_1:13,RLVECT_1:def 4;
end;
A27: P[0] by A5;
A28: for n holds P[n] from NAT_1:sch 2(A27,A20);
A29: Q[i]
proof
i in Seg len R by A8,A19,A3;
then L.i=ONE*(i,i) & [i,i] in Indices ONE by A7,A1,A9,MATRIX_0:def 7
,ZFMISC_1:87;
then
A30: L.i=1_K by MATRIX_1:def 3;
reconsider i1=i-1 as Element of NAT by A8,NAT_1:21;
A31: i1+1=i;
then i1<i by NAT_1:13;
then
A32: f.i1=0.V1 by A28;
assume i<=len M;
then
A33: i1<len M by A31,NAT_1:13;
R.i=R/.i by A7,PARTFUN1:def 6;
then M.i = 1_K * R/.i by A7,A2,A30,FUNCOP_1:22
.= R/.i;
then f.(i1+1) = f.i1+R/.i by A6,A33;
hence thesis by A32,RLVECT_1:def 4;
end;
for n st i<=n holds Q[n] from NAT_1:sch 8(A29,A10);
hence thesis by A19,A4;
end;
begin :: More on the Decomposition of a Vector in a Basis
theorem Th17:
v1 + w1 |-- b1 = (v1 |-- b1) + (w1 |-- b1)
proof
set vb=v1 |-- b1;
set wb=w1 |-- b1;
set vwb=v1+w1 |-- b1;
consider L1 be Linear_Combination of V1 such that
A1: v1 = Sum(L1) & Carrier L1 c= rng b1 and
A2: for k st 1<=k & k<=len vb holds vb/.k = L1.(b1/.k) by MATRLIN:def 7;
consider L3 be Linear_Combination of V1 such that
A3: v1+w1 = Sum(L3) & Carrier L3 c= rng b1 and
A4: for k st 1<=k & k<=len vwb holds vwb/.k = L3.(b1/.k) by MATRLIN:def 7;
A5: len wb=len b1 by MATRLIN:def 7;
reconsider rb1=rng b1 as Basis of V1 by MATRLIN:def 2;
consider L2 be Linear_Combination of V1 such that
A6: w1 = Sum(L2) & Carrier L2 c= rng b1 and
A7: for k st 1<=k & k<=len wb holds wb/.k = L2.(b1/.k) by MATRLIN:def 7;
A8: len vb=len b1 by MATRLIN:def 7;
A9: len vwb=len b1 by MATRLIN:def 7;
then reconsider
vb,wb,vwb as Element of (len b1)-tuples_on the carrier of K by A8,A5,
FINSEQ_2:92;
rb1 is linearly-independent by VECTSP_7:def 3;
then
A10: L3=L1+L2 by A1,A6,A3,MATRLIN:6;
now
A11: dom b1=Seg len b1 by FINSEQ_1:def 3;
let i such that
A12: i in Seg len b1;
A13: 1<=i & i<=len b1 by A12,FINSEQ_1:1;
dom wb=dom b1 by A5,FINSEQ_3:29;
then
A14: wb.i=wb/.i by A12,A11,PARTFUN1:def 6;
dom vb=dom b1 by A8,FINSEQ_3:29;
then
A15: vb.i=vb/.i by A12,A11,PARTFUN1:def 6;
dom vwb=dom b1 by A9,FINSEQ_3:29;
then vwb.i=vwb/.i by A12,A11,PARTFUN1:def 6;
hence vwb.i = (L1+L2).(b1/.i) by A4,A9,A10,A13
.= L1.(b1/.i)+L2.(b1/.i) by VECTSP_6:22
.= vb/.i +L2.(b1/.i) by A2,A8,A13
.= vb/.i +wb/.i by A7,A5,A13
.= (vb+wb).i by A12,A15,A14,FVSUM_1:18;
end;
hence thesis by FINSEQ_2:119;
end;
theorem Th18:
a * v1 |-- b1 = a * (v1 |-- b1)
proof
set vb=v1 |-- b1;
set avb=(a*v1) |-- b1;
consider L1 be Linear_Combination of V1 such that
A1: v1 = Sum(L1) & Carrier L1 c= rng b1 and
A2: for k st 1<=k & k<=len vb holds vb/.k = L1.(b1/.k) by MATRLIN:def 7;
A3: len vb=len b1 by MATRLIN:def 7;
reconsider rb1=rng b1 as Basis of V1 by MATRLIN:def 2;
consider L2 be Linear_Combination of V1 such that
A4: a*v1 = Sum(L2) and
A5: Carrier L2 c= rng b1 and
A6: for k st 1<=k & k<=len avb holds avb/.k = L2.(b1/.k) by MATRLIN:def 7;
A7: len avb=len b1 by MATRLIN:def 7;
len (a*vb)=len vb by MATRIXR1:16;
then reconsider
vb9=vb,avb,Avb=a*vb as Element of (len b1)-tuples_on the carrier
of K by A3,A7,FINSEQ_2:92;
A8: rb1 is linearly-independent by VECTSP_7:def 3;
now
let i such that
A9: i in Seg len b1;
A10: 1<=i & i<=len b1 by A9,FINSEQ_1:1;
A11: now
per cases;
suppose
a<>0.K;
then a*L1=L2 by A1,A4,A5,A8,MATRLIN:7;
hence L2.(b1/.i) = a*L1.(b1/.i) by VECTSP_6:def 9
.= a*(vb9/.i) by A2,A3,A10;
end;
suppose
A12: a=0.K;
then
A13: a*v1=0.V1 by VECTSP_1:14;
L2 is Linear_Combination of Carrier L2 & Carrier L2 is
linearly-independent by A5,A8,VECTSP_6:7,VECTSP_7:1;
then not b1/.i in Carrier L2 by A4,A13;
hence L2.(b1/.i) = 0.K .= a*(vb9/.i) by A12;
end;
end;
A14: dom b1=Seg len b1 by FINSEQ_1:def 3;
dom vb=dom b1 by A3,FINSEQ_3:29;
then
A15: vb.i=vb/.i by A9,A14,PARTFUN1:def 6;
dom avb=dom b1 by A7,FINSEQ_3:29;
then avb.i=avb/.i by A9,A14,PARTFUN1:def 6;
hence avb.i = L2.(b1/.i) by A6,A7,A10
.= Avb.i by A9,A15,A11,FVSUM_1:51;
end;
hence thesis by FINSEQ_2:119;
end;
theorem Th19:
i in dom b1 implies b1/.i|-- b1 = Line(1.(K,len b1),i)
proof
set ONE=1.(K,len b1);
set bb=b1/.i|-- b1;
consider KL be Linear_Combination of V1 such that
A1: b1/.i = Sum(KL) & Carrier KL c= rng b1 and
A2: for k st 1<=k & k<=len bb holds bb/.k=KL.(b1/.k) by MATRLIN:def 7;
reconsider rb1=rng b1 as Basis of V1 by MATRLIN:def 2;
A3: rb1 is linearly-independent by VECTSP_7:def 3;
b1/.i in {b1/.i} by TARSKI:def 1;
then b1/.i in Lin{b1/.i} by VECTSP_7:8;
then consider Lb be Linear_Combination of {b1/.i} such that
A4: b1/.i=Sum Lb by VECTSP_7:7;
assume
A5: i in dom b1;
then
A6: b1.i=b1/.i by PARTFUN1:def 6;
then
A7: Carrier Lb c= {b1.i} by VECTSP_6:def 4;
A8: b1.i in rb1 by A5,FUNCT_1:def 3;
then {b1.i}c= rb1 by ZFMISC_1:31;
then Carrier Lb c= rb1 by A7;
then
A9: Lb = KL by A4,A1,A3,MATRLIN:5;
A10: width ONE=len b1 by MATRIX_0:24;
A11: Indices ONE=[:Seg len b1,Seg len b1:] by MATRIX_0:24;
A12: len b1=len bb by MATRLIN:def 7;
A13: b1/.i<>0.V1 by A6,A3,A8,VECTSP_7:2;
A14: now
let j such that
A15: 1<=j & j<=len bb;
A16: j in Seg len b1 by A12,A15;
i in Seg len b1 by A5,FINSEQ_1:def 3;
then
A17: [i,j] in Indices ONE by A11,A16,ZFMISC_1:87;
A18: j in dom b1 by A12,A15,FINSEQ_3:25;
A19: dom bb=dom b1 by A12,FINSEQ_3:29;
now
per cases;
suppose
A20: i=j;
Lb.(b1/.i) *(b1/.i) = b1/.i by A4,VECTSP_6:17
.= 1_K*(b1/.i);
then
A21: 1_K = KL.(b1/.i) by A13,A9,VECTSP10:4
.= bb/.j by A2,A15,A20;
1_K = ONE*(i,j) by A17,A20,MATRIX_1:def 3
.= Line(ONE,i).j by A10,A16,MATRIX_0:def 7;
hence Line(ONE,i).j=bb.j by A18,A19,A21,PARTFUN1:def 6;
end;
suppose
A22: i<>j;
b1 is one-to-one by MATRLIN:def 2;
then b1.i <> b1.j by A5,A18,A22;
then
A23: not b1.j in Carrier Lb by A7,TARSKI:def 1;
A24: 0.K = ONE*(i,j) by A17,A22,MATRIX_1:def 3
.= Line(ONE,i).j by A10,A16,MATRIX_0:def 7;
b1.j = b1/.j by A18,PARTFUN1:def 6;
then 0.K = KL.(b1/.j) by A9,A23
.= bb/.j by A2,A15;
hence Line(ONE,i).j=bb.j by A18,A19,A24,PARTFUN1:def 6;
end;
end;
hence Line(ONE,i).j=bb.j;
end;
len Line(ONE,i)=len b1 by A10,CARD_1:def 7;
hence thesis by A12,A14;
end;
theorem Th20:
0.V1|-- b1 = len b1 |-> 0.K
proof
per cases;
suppose
A1: dom b1={};
then
A2: len b1=0 by CARD_1:27,RELAT_1:41;
len (0.V1|--b1)=len b1 by MATRLIN:def 7;
hence 0.V1|-- b1 = {} by A1,CARD_1:27,RELAT_1:41
.= len b1 |-> 0.K by A2;
end;
suppose
dom b1<>{};
then consider x being object such that
A3: x in dom b1 by XBOOLE_0:def 1;
A4: width 1.(K,len b1)=len b1 by MATRIX_0:24;
reconsider x as Nat by A3;
0.V1 = b1/.x-b1/.x by VECTSP_1:16
.= b1/.x+(-1_K)*(b1/.x) by VECTSP_1:14;
hence 0.V1|-- b1 = (b1/.x |-- b1) + ((-1_K)*(b1/.x) |--b1) by Th17
.= (b1/.x |-- b1) + (-1_K)*((b1/.x) |--b1) by Th18
.= Line(1.(K,len b1),x)+(-1_K)*((b1/.x) |--b1) by A3,Th19
.= Line(1.(K,len b1),x)+(-1_K)*Line(1.(K,len b1),x) by A3,Th19
.= Line(1.(K,len b1),x)+-Line(1.(K,len b1),x) by FVSUM_1:59
.= len b1|->0.K by A4,FVSUM_1:26;
end;
end;
theorem Th21:
len b1 = dim V1
proof
reconsider R=rng b1 as Basis of V1 by MATRLIN:def 2;
A1: b1 is one-to-one by MATRLIN:def 2;
thus len b1 = card Seg len b1 by FINSEQ_1:57
.= card dom b1 by FINSEQ_1:def 3
.= card R by A1,CARD_1:70
.= dim V1 by VECTSP_9:def 1;
end;
Lm4: for V be VectSp of K for W1 be Subspace of V for L1 be Linear_Combination
of W1 ex K1 be Linear_Combination of V st Carrier K1=Carrier L1 & Sum K1=Sum L1
& K1|the carrier of W1=L1
proof
let V be VectSp of K;
let W1 be Subspace of V;
let L1 be Linear_Combination of W1;
defpred P[object, object] means
($1 in W1 & $2 = L1.$1) or (not $1 in W1 & $2 = 0.K);
reconsider L9= L1 as Function of W1,K;
A1: for x being object st x in the carrier of V
ex y being object st y in the carrier of K & P[x, y]
proof
let x be object such that
x in the carrier of V;
per cases;
suppose
A2: x in W1;
then reconsider x as Vector of W1;
P[x, L1.x] by A2;
hence thesis;
end;
suppose
not x in W1;
hence thesis;
end;
end;
consider K1 be Function of V,K such that
A3: for x being object st x in the carrier of V
holds P[x, K1.x] from FUNCT_2:sch 1(
A1 );
A4: the carrier of W1 c= the carrier of V by VECTSP_4:def 2;
then reconsider C = Carrier(L1) as finite Subset of V by XBOOLE_1:1;
A5: now
let v be Vector of V such that
A6: not v in C;
P[v, L1.v] & v in the carrier of W1 or P[v, 0.K] by STRUCT_0:def 5;
then P[v, L1.v] & L1.v = 0.K or P[v, 0.K] by A6;
hence K1.v = 0.K by A3;
end;
K1 is Element of Funcs(the carrier of V, the carrier of K) by FUNCT_2:8;
then reconsider K1 as Linear_Combination of V by A5,VECTSP_6:def 1;
reconsider K9= K1|the carrier of W1 as Function of the carrier of W1, the
carrier of K by A4,FUNCT_2:32;
take K1;
now
let x be object;
assume that
A7: x in Carrier(K1) and
A8: not x in the carrier of W1;
consider v being Vector of V such that
A9: x = v and
A10: K1.v <> 0.K by A7;
P[v, 0.K] by A8,A9,STRUCT_0:def 5;
hence contradiction by A3,A10;
end;
then
A11: Carrier(K1) c= the carrier of W1;
now
let x be object such that
A12: x in the carrier of W1;
P[x, K1.x] by A3,A4,A12;
hence L9.x = K9.x by A12,FUNCT_1:49,STRUCT_0:def 5;
end;
then L9 = K9 by FUNCT_2:12;
hence thesis by A11,VECTSP_9:7;
end;
theorem
rng(b1|m) is linearly-independent Subset of V1 & for A be Subset of V1
st A = rng(b1|m) holds b1|m is OrdBasis of Lin A
proof
reconsider RNG=rng b1 as Basis of V1 by MATRLIN:def 2;
A1: RNG is linearly-independent by VECTSP_7:def 3;
rng (b1|m) c= RNG by RELAT_1:70;
hence rng(b1|m) is linearly-independent Subset of V1 by A1,VECTSP_7:1
,XBOOLE_1:1;
let A be Subset of V1 such that
A2: A = rng(b1|m);
A3: A c= the carrier of Lin (A)
proof
let x be object;
assume x in A;
then x in Lin A by VECTSP_7:8;
hence thesis;
end;
A is linearly-independent by A1,A2,RELAT_1:70,VECTSP_7:1;
then reconsider A9=A as linearly-independent Subset of Lin A by A3,
VECTSP_9:12;
b1 is one-to-one by MATRLIN:def 2;
then
A4: b1|m is one-to-one by FUNCT_1:52;
Lin A9= the ModuleStr of Lin A by VECTSP_9:17;
then rng(b1|m) is Basis of Lin A & b1|m is FinSequence of Lin A by A2,
FINSEQ_1:def 4,VECTSP_7:def 3;
hence thesis by A4,MATRLIN:def 2;
end;
theorem
rng(b1/^m) is linearly-independent Subset of V1 & for A be Subset of
V1 st A = rng(b1/^m) holds b1/^m is OrdBasis of Lin A
proof
reconsider RNG=rng b1 as Basis of V1 by MATRLIN:def 2;
A1: RNG is linearly-independent by VECTSP_7:def 3;
rng (b1/^m) c= RNG by FINSEQ_5:33;
hence rng(b1/^m) is linearly-independent Subset of V1 by A1,VECTSP_7:1
,XBOOLE_1:1;
let A be Subset of V1 such that
A2: A = rng(b1 /^m);
A3: A c= the carrier of Lin (A)
proof
let x be object;
assume x in A;
then x in Lin A by VECTSP_7:8;
hence thesis;
end;
A is linearly-independent by A1,A2,FINSEQ_5:33,VECTSP_7:1;
then reconsider A9=A as linearly-independent Subset of Lin A by A3,
VECTSP_9:12;
b1 is one-to-one & b1=(b1|m)^(b1/^m) by MATRLIN:def 2,RFINSEQ:8;
then
A4: b1/^m is one-to-one by FINSEQ_3:91;
Lin A9= the ModuleStr of Lin A by VECTSP_9:17;
then rng(b1/^m) is Basis of Lin A & b1/^m is FinSequence of Lin A by A2,
FINSEQ_1:def 4,VECTSP_7:def 3;
hence thesis by A4,MATRLIN:def 2;
end;
theorem Th24:
for W1,W2 be Subspace of V1 st W1/\W2=(0).V1 for b1 be OrdBasis
of W1,b2 be OrdBasis of W2,b be OrdBasis of W1+W2 st b=b1^b2 for v,v1,v2 be
Vector of W1+W2, w1 be Vector of W1,w2 be Vector of W2 st v = v1+v2 & v1=w1 &
v2=w2 holds v|-- b = (w1|--b1)^(w2|-- b2)
proof
let W1,W2 be Subspace of V1 such that
A1: W1/\W2=(0).V1;
[#](0).V1 = {0.V1} by VECTSP_4:def 3;
then
A2: card ([#](0).V1) = 1 by CARD_1:30;
A3: dim W1 + dim W2 = dim(W1 + W2) + dim(W1 /\ W2) by VECTSP_9:32
.= dim (W1+W2)+0 by A1,A2,RANKNULL:5;
let b1 be OrdBasis of W1,b2 be OrdBasis of W2,b be OrdBasis of W1+W2 such
that
A4: b=b1^b2;
reconsider R=rng b as Basis of W1+W2 by MATRLIN:def 2;
let v,v1,v2 be Vector of W1+W2,w1 be Vector of W1,w2 be Vector of W2 such
that
A5: v=v1+v2 & v1=w1 & v2=w2;
set wb2=w2|--b2;
consider L2 be Linear_Combination of W2 such that
A6: w2 = Sum(L2) and
A7: Carrier L2 c= rng b2 and
A8: for k st 1<=k & k<=len wb2 holds wb2/.k=L2.(b2/.k) by MATRLIN:def 7;
A9: W2 is Subspace of W1+W2 by VECTSP_5:7;
then consider K2 be Linear_Combination of W1+W2 such that
A10: Carrier(K2) = Carrier(L2) and
A11: Sum(K2) = Sum (L2) and
A12: K2|the carrier of W2=L2 by Lm4;
rng b2 c= R by A4,FINSEQ_1:30;
then
A13: Carrier K2 c= R by A7,A10;
set wb1=w1|--b1;
set vb=v|--b;
consider L1 be Linear_Combination of W1 such that
A14: w1 = Sum(L1) and
A15: Carrier L1 c= rng b1 and
A16: for k st 1<=k & k<=len wb1 holds wb1/.k=L1.(b1/.k) by MATRLIN:def 7;
consider L be Linear_Combination of W1+W2 such that
A17: v = Sum(L) & Carrier L c= rng b and
A18: for k st 1<=k & k<=len vb holds vb/.k=L.(b/.k) by MATRLIN:def 7;
A19: len vb=len b by MATRLIN:def 7;
then
A20: dom vb=dom b by FINSEQ_3:29;
A21: len wb2=len b2 by MATRLIN:def 7;
then
A22: dom wb2=dom b2 by FINSEQ_3:29;
A23: R is linearly-independent by VECTSP_7:def 3;
A24: W1 is Subspace of W1+W2 by VECTSP_5:7;
then consider K1 be Linear_Combination of W1+W2 such that
A25: Carrier(K1) = Carrier(L1) and
A26: Sum(K1) = Sum (L1) and
A27: K1|the carrier of W1=L1 by Lm4;
A28: len wb1=len b1 by MATRLIN:def 7;
then
A29: dom wb1=dom b1 by FINSEQ_3:29;
A30: len (wb1^wb2)=len wb1+len wb2 by FINSEQ_1:22;
A31: len b1=dim W1 & len b2=dim W2 by Th21;
A32: len b=dim (W1+W2) by Th21;
then
A33: dom b=dom (wb1^wb2) by A28,A21,A31,A30,A3,FINSEQ_3:29;
rng b1 c= R by A4,FINSEQ_1:29;
then
A34: Carrier K1 c= R by A15,A25;
then
A35: L=K1+K2 by A5,A14,A26,A6,A11,A17,A13,A23,MATRLIN:6;
now
let k such that
A36: 1<=k & k<=len vb;
A37: k in dom (wb1^wb2) by A28,A21,A19,A31,A32,A30,A3,A36,FINSEQ_3:25;
now
per cases by A37,FINSEQ_1:25;
suppose
A38: k in dom wb1;
then 1<=k & k<=len wb1 by FINSEQ_3:25;
then
A39: L1.(b1/.k) = wb1/.k by A16
.= wb1.k by A38,PARTFUN1:def 6
.= (wb1^wb2).k by A38,FINSEQ_1:def 7;
reconsider b1k=b1/.k as Vector of W1+W2 by A24,VECTSP_4:10;
A40: K1.(b1/.k)=L1.(b1/.k) by A27,FUNCT_1:49;
not b1/.k in Carrier K2
proof
A41: b1/.k in W1;
assume
A42: b1/.k in Carrier K2;
then b1/.k in W2 by A10;
then b1/.k in W1/\W2 by A41,VECTSP_5:3;
then b1/.k in the carrier of (0).V1 by A1;
then b1/.k in {0.V1} by VECTSP_4:def 3;
then b1/.k = 0.V1 by TARSKI:def 1
.= 0.(W1+W2) by VECTSP_4:11;
hence thesis by A13,A23,A42,VECTSP_7:2;
end;
then K2.b1k=0.K;
then
A43: L.b1k = K1.b1k+0.K by A35,VECTSP_6:22
.= (wb1^wb2).k by A39,A40,RLVECT_1:def 4;
b1k = b1.k by A29,A38,PARTFUN1:def 6
.= b.k by A4,A29,A38,FINSEQ_1:def 7
.= b/.k by A33,A37,PARTFUN1:def 6;
hence (wb1^wb2).k = vb/.k by A18,A36,A43
.= vb.k by A33,A20,A37,PARTFUN1:def 6;
end;
suppose
ex n st n in dom wb2 & k=len wb1+n;
then consider n such that
A44: n in dom wb2 and
A45: k=len wb1+n;
1<=n & n<=len wb2 by A44,FINSEQ_3:25;
then
A46: L2.(b2/.n) = wb2/.n by A8
.= wb2.n by A44,PARTFUN1:def 6
.= (wb1^wb2).k by A44,A45,FINSEQ_1:def 7;
reconsider b2n=b2/.n as Vector of W1+W2 by A9,VECTSP_4:10;
A47: K2.(b2/.n)=L2.(b2/.n) by A12,FUNCT_1:49;
not b2/.n in Carrier K1
proof
assume
A48: b2/.n in Carrier K1;
then b2/.n in W2 & b2/.n in W1 by A25;
then b2/.n in W1/\W2 by VECTSP_5:3;
then b2/.n in the carrier of (0).V1 by A1;
then b2/.n in {0.V1} by VECTSP_4:def 3;
then b2/.n = 0.V1 by TARSKI:def 1
.= 0.(W1+W2) by VECTSP_4:11;
hence thesis by A34,A23,A48,VECTSP_7:2;
end;
then K1.b2n=0.K;
then
A49: L.b2n = 0.K+K2.b2n by A35,VECTSP_6:22
.= (wb1^wb2).k by A46,A47,RLVECT_1:def 4;
b2n = b2.n by A22,A44,PARTFUN1:def 6
.= b.k by A4,A28,A22,A44,A45,FINSEQ_1:def 7
.= b/.k by A33,A37,PARTFUN1:def 6;
hence (wb1^wb2).k = vb/.k by A18,A36,A49
.= vb.k by A33,A20,A37,PARTFUN1:def 6;
end;
end;
hence vb.k=(wb1^wb2).k;
end;
hence thesis by A28,A21,A19,A31,A30,A3,Th21;
end;
theorem Th25:
for W1 be Subspace of V1 st W1 = (Omega).V1 for w be Vector of
W1, v be Vector of V1,w1 be OrdBasis of W1 st v = w & b1 = w1 holds v|--b1 = w
|-- w1
proof
let W1 be Subspace of V1 such that
A1: W1 = (Omega).V1;
let w be Vector of W1,v be Vector of V1,w1 be OrdBasis of W1 such that
A2: v = w and
A3: b1 = w1;
consider KL be Linear_Combination of W1 such that
A4: w = Sum(KL) & Carrier KL c= rng w1 and
A5: for k st 1<=k & k<=len (w|--w1) holds (w|--w1)/.k=KL.(w1/.k) by
MATRLIN:def 7;
consider K1 be Linear_Combination of V1 such that
A6: Carrier K1=Carrier KL & Sum K1=Sum KL and
A7: K1|the carrier of W1=KL by Lm4;
A8: len w1 = len (w|-- w1) by MATRLIN:def 7;
now
let k such that
A9: 1<=k & k<=len (w|--w1);
A10: k in dom w1 by A8,A9,FINSEQ_3:25;
dom K1 = the carrier of W1 by A1,FUNCT_2:def 1;
then KL=K1 by A7;
hence (w|--w1)/.k = K1.(w1/.k) by A5,A9
.= K1.(w1.k) by A10,PARTFUN1:def 6
.= K1.(b1/.k) by A3,A10,PARTFUN1:def 6;
end;
hence thesis by A2,A3,A4,A6,A8,MATRLIN:def 7;
end;
theorem Th26:
for W1,W2 be Subspace of V1 st W1/\W2=(0).V1 for w1 be OrdBasis
of W1,w2 be OrdBasis of W2 holds w1^w2 is OrdBasis of W1+W2
proof
let W1,W2 be Subspace of V1 such that
A1: W1/\W2=(0).V1;
let w1 be OrdBasis of W1,w2 be OrdBasis of W2;
reconsider R1=rng w1 as Basis of W1 by MATRLIN:def 2;
reconsider R2=rng w2 as Basis of W2 by MATRLIN:def 2;
A2: R1\/R2=rng (w1^w2) by FINSEQ_1:31;
A3: R1 misses R2
proof
assume R1 meets R2;
then consider x being object such that
A4: x in R1 and
A5: x in R2 by XBOOLE_0:3;
x in W1 & x in W2 by A4,A5;
then x in W1/\W2 by VECTSP_5:3;
then x in the carrier of (0).V1 by A1;
then x in {0.V1} by VECTSP_4:def 3;
then x = 0.V1 by TARSKI:def 1
.= 0.W1 by VECTSP_4:11;
then not R1 is linearly-independent by A4,VECTSP_7:2;
hence thesis by VECTSP_7:def 3;
end;
A6: R1\/R2 is Basis of W1+W2 by A1,Th3;
then reconsider w12=w1^w2 as FinSequence of W1+W2 by A2,FINSEQ_1:def 4;
w1 is one-to-one & w2 is one-to-one by MATRLIN:def 2;
then w12 is one-to-one by A3,FINSEQ_3:91;
hence thesis by A6,A2,MATRLIN:def 2;
end;
begin :: Properties of Matrices of Linear Transformations
definition
let K,V1,V2,f,B1,b2;
redefine func AutMt(f,B1,b2) -> Matrix of len B1,len b2,K; :: redefines AutMt (MATRLIN, definition)
coherence
proof
reconsider A9=AutMt(f,B1,b2) as Matrix of len AutMt(f,B1,b2),width AutMt(f
,B1,b2),K by MATRIX_0:51;
A1: len A9=len B1 by MATRLIN:def 8;
per cases;
suppose
A2: len B1=0;
then AutMt(f,B1,b2)={} by A1;
hence thesis by A2,MATRIX_0:13;
end;
suppose
A3: len B1>0;
A4: dom B1=dom A9 by A1,FINSEQ_3:29;
A5: dom B1=Seg len B1 by FINSEQ_1:def 3;
A6: len B1 in Seg len B1 by A3,FINSEQ_1:3;
then f.(B1/.len B1) |--b2 = A9/.(len B1) by A5,MATRLIN:def 8
.= A9.(len B1) by A3,A5,A4,FINSEQ_1:3,PARTFUN1:def 6
.= Line(A9,len B1) by A1,A6,MATRIX_0:52;
then
A7: width A9= len (f.(B1/.len B1) |--b2) by CARD_1:def 7
.= len b2 by MATRLIN:def 7;
len A9 = len B1 by MATRLIN:def 8;
hence thesis by A7;
end;
end;
end;
definition
let S be 1-sorted;
let R be Relation;
func R|S -> set equals
R | (the carrier of S);
coherence;
end;
theorem
for f be linear-transformation of V1,V2 for W1,W2 be Subspace of V1,U1
,U2 be Subspace of V2 st ( dim W1 =0 implies dim U1 = 0 )& ( dim W2 =0 implies
dim U2 = 0 )& V2 is_the_direct_sum_of U1,U2 for fW1 be linear-transformation of
W1,U1, fW2 be linear-transformation of W2,U2 st fW1 = f | W1 & fW2 = f | W2 for
w1 be OrdBasis of W1, w2 be OrdBasis of W2, u1 be OrdBasis of U1, u2 be
OrdBasis of U2 st w1^w2 = b1 & u1^u2 = b2 holds AutMt(f,b1,b2) = block_diagonal
(<*AutMt(fW1,w1,u1),AutMt(fW2,w2,u2)*>,0.K)
proof
let f be linear-transformation of V1,V2;
let W1,W2 be Subspace of V1,U1,U2 be Subspace of V2 such that
A1: dim W1 =0 implies dim U1 = 0 and
A2: dim W2 =0 implies dim U2 = 0 and
A3: V2 is_the_direct_sum_of U1,U2;
A4: U1/\U2=(0).V2 by A3,VECTSP_5:def 4;
let fW1 be linear-transformation of W1,U1;
let fW2 be linear-transformation of W2,U2 such that
A5: fW1=f|W1 and
A6: fW2=f|W2;
let w1 be OrdBasis of W1,w2 be OrdBasis of W2, u1 be OrdBasis of U1,u2 be
OrdBasis of U2 such that
A7: w1^w2=b1 and
A8: u1^u2=b2;
A9: len b1=len w1+len w2 by A7,FINSEQ_1:22;
A10: U1 + U2=(Omega).V2 by A3,VECTSP_5:def 4;
set A=AutMt(f,b1,b2);
A11: len b1=len A by MATRLIN:def 8;
set A2=AutMt(fW2,w2,u2);
A12: len w2=dim W2 & len u2=dim U2 by Th21;
then
A13: len w2=len A2 by A2,MATRIX13:1;
set A1=AutMt(fW1,w1,u1);
A14: len w1=dim W1 & len u1=dim U1 by Th21;
then
A15: len w1=len A1 by A1,MATRIX13:1;
A16: len u2=width A2 by A2,A12,MATRIX13:1;
A17: len u1=width A1 by A1,A14,MATRIX13:1;
A18: now
reconsider uu=u1^u2 as OrdBasis of U1+U2 by A4,Th26;
let i;
A19: dom A=Seg len A by FINSEQ_1:def 3;
reconsider fb=f.(b1/.i),fbi=f.(b1/.(i+len A1)) as Vector of U1+U2 by A10;
A20: dom A=dom b1 by A11,FINSEQ_3:29;
A21: dom A1=dom w1 by A15,FINSEQ_3:29;
A22: dom fW1=the carrier of W1 by FUNCT_2:def 1;
thus i in dom A1 implies Line(A,i)=Line(A1,i)^(width A2 |-> 0.K)
proof
assume
A23: i in dom A1;
A24: dom A1=Seg len A1 by FINSEQ_1:def 3;
then
A25: Line(A1,i) = A1.i by A15,A23,MATRIX_0:52
.= A1/.i by A23,PARTFUN1:def 6
.= fW1.(w1/.i) |-- u1 by A21,A23,MATRLIN:def 8;
len A1 <=len A by A9,A15,A11,NAT_1:11;
then
A26: Seg len A1 c= Seg len A by FINSEQ_1:5;
then b1/.i = b1.i by A19,A20,A23,A24,PARTFUN1:def 6
.= w1.i by A7,A21,A23,FINSEQ_1:def 7
.= w1/.i by A21,A23,PARTFUN1:def 6;
then
A27: fb = fW1.(w1/.i) by A5,A22,FUNCT_1:47;
thus Line(A,i) = A.i by A11,A23,A24,A26,MATRIX_0:52
.= A/.i by A19,A23,A24,A26,PARTFUN1:def 6
.= f.(b1/.i) |--b2 by A19,A20,A23,A24,A26,MATRLIN:def 8
.= fb|--uu by A10,A8,Th25
.= (fb+0.(U1+U2)) |-- uu by RLVECT_1:def 4
.= (fW1.(w1/.i) |-- u1)^(0.U2|--u2) by A4,A27,Th24,VECTSP_4:12
.= Line(A1,i)^(width A2|->0.K) by A16,A25,Th20;
end;
A28: dom A2=dom w2 by A13,FINSEQ_3:29;
A29: dom fW2 = the carrier of W2 by FUNCT_2:def 1;
thus i in dom A2 implies Line(A,i+len A1)=(width A1|->0.K)^Line(A2,i)
proof
assume
A30: i in dom A2;
A31: dom A2=Seg len A2 by FINSEQ_1:def 3;
then
A32: i+len A1 in dom A by A9,A15,A13,A11,A19,A30,FINSEQ_1:60;
b1/.(i+len A1) = b1.(i+len A1) by A9,A15,A13,A11,A19,A20,A30,A31,
FINSEQ_1:60,PARTFUN1:def 6
.= w2.i by A7,A15,A28,A30,FINSEQ_1:def 7
.= w2/.i by A28,A30,PARTFUN1:def 6;
then
A33: fbi = fW2.(w2/.i) by A6,A29,FUNCT_1:47;
A34: Line(A2,i) = A2.i by A13,A30,A31,MATRIX_0:52
.= A2/.i by A30,PARTFUN1:def 6
.= fW2.(w2/.i) |-- u2 by A28,A30,MATRLIN:def 8;
thus Line(A,i+len A1) = A.(i+len A1) by A9,A15,A13,A11,A19,A30,A31,
FINSEQ_1:60,MATRIX_0:52
.= A/.(i+len A1) by A9,A15,A13,A11,A19,A30,A31,FINSEQ_1:60
,PARTFUN1:def 6
.= f.(b1/.(i+len A1)) |--b2 by A20,A32,MATRLIN:def 8
.= fbi|--uu by A10,A8,Th25
.= (0.(U1+U2)+fbi) |-- uu by RLVECT_1:def 4
.= (0.U1|--u1)^(fW2.(w2/.i) |-- u2) by A4,A33,Th24,VECTSP_4:12
.= (width A1|->0.K)^Line(A2,i) by A17,A34,Th20;
end;
end;
set A12=<*A1,A2*>;
A35: Sum Len A12=len A1+len A2 & Sum Width A12=width A1+width A2 by MATRIXJ1:16
,20;
len b2=len u1+len u2 by A8,FINSEQ_1:22;
hence thesis by A9,A15,A13,A17,A16,A35,A18,MATRIXJ1:23;
end;
definition
let K,V1,V2;
let f be Function of V1,V2;
let B1 be FinSequence of V1;
let b2 be OrdBasis of V2;
assume
A1: len B1 = len b2;
func AutEqMt(f,B1,b2) -> Matrix of len B1,len B1,K equals
:Def2:
AutMt(f,B1,
b2);
coherence by A1;
end;
theorem Th28:
AutMt(id V1,b1,b1) = 1.(K,len b1)
proof
set A=AutMt(id V1,b1,b1);
set ONE=1.(K,len b1);
A1: len A=len b1 by MATRIX_0:def 2;
A2: now
let i such that
A3: 1<=i & i<=len b1;
A4: i in dom b1 by A3,FINSEQ_3:25;
A5: i in Seg len b1 by A3;
i in dom A by A1,A3,FINSEQ_3:25;
hence A.i = A/.i by PARTFUN1:def 6
.= ((id V1).(b1/.i)) |-- b1 by A4,MATRLIN:def 8
.= (b1/.i) |-- b1
.= Line(ONE,i) by A4,Th19
.= ONE.i by A5,MATRIX_0:52;
end;
len ONE=len b1 by MATRIX_0:def 2;
hence thesis by A1,A2;
end;
theorem
AutEqMt(id V1,b1,b19) is invertible &
AutEqMt(id V1,b19,b1) = AutEqMt(id V1,b1,b19)~
proof
set A = AutEqMt(id V1,b1,b19);
A1: 1_K<>0.K;
A2: len b1 = dim V1 by Th21
.= len b19 by Th21;
then reconsider A9= AutEqMt(id V1,b19,b1) as Matrix of len b1,len b1,K;
A3: A=AutMt(id V1,b1,b19) & A9=AutMt(id V1,b19,b1) by A2,Def2;
per cases;
suppose
len b1=0;
then Det A=1_K & A9=A~ by MATRIXR2:41,MATRIX_0:45;
hence thesis by A1,LAPLACE:43;
end;
suppose
A4: len b1+0>0;
dom id V1=the carrier of V1;
then
A5: (id V1) * (id V1) = id V1 by RELAT_1:52;
len b1=dim V1 by Th21;
then len b1 = len b19 by Th21;
then
A6: A * A9 = AutMt((id V1)*(id V1),b1,b1) by A3,A4,MATRLIN:41
.= 1.(K,len b1) by A5,Th28;
len b1>=1 by A4,NAT_1:19;
then 1_K = Det (A * A9) by A6,MATRIX_7:16
.= Det A * Det A9 by A4,MATRIX11:62;
then Det A <> 0.K;
then Det A is non zero;
then
A7: A is invertible by LAPLACE:43;
then A~ is_reverse_of A by MATRIX_6:def 4;
then A * (A~)=1.(K,len b1) by MATRIX_6:def 2;
hence thesis by A6,A7,MATRIX_8:19;
end;
end;
theorem Th30:
len p1 = len p2 & len p1 = len B1 & len p1 > 0 & j in dom b1 & (
for i st i in dom p2 holds p2.i = (B1/.i|--b1).j) implies p1 "*" p2 = (Sum lmlt
(p1,B1) |-- b1).j
proof
assume that
A1: len p1 = len p2 and
A2: len p1 = len B1 and
A3: len p1>0 and
A4: j in dom b1 and
A5: for i st i in dom p2 holds p2.i = (B1/.i|--b1).j;
deffunc m(Nat,Nat) = (B1/.$1|--b1)/.$2;
consider M be Matrix of len p1,len b1,K such that
A6: for i,j st [i,j] in Indices M holds M*(i,j) = m(i,j) from MATRIX_0:
sch 1;
A7: len M=len p1 by A3,MATRIX_0:23;
then
A8: dom p1=dom M by FINSEQ_3:29;
A9: width M=len b1 by A3,MATRIX_0:23;
A10: dom b1 =Seg len b1 by FINSEQ_1:def 3;
A11: dom p1=Seg len p1 by FINSEQ_1:def 3;
A12: dom p1=dom p2 by A1,FINSEQ_3:29;
A13: now
let i;
assume 1<=i & i<=len p2;
then
A14: i in dom p1 by A1,A11;
then
A15: [i,j] in Indices M by A4,A9,A8,A10,ZFMISC_1:87;
len ((B1/.i) |--b1)=len b1 by MATRLIN:def 7;
then
A16: dom ((B1/.i) |--b1)=dom b1 by FINSEQ_3:29;
thus Col(M,j).i = M*(i,j) by A8,A14,MATRIX_0:def 8
.= ((B1/.i) |--b1)/.j by A6,A15
.= ((B1/.i) |--b1).j by A4,A16,PARTFUN1:def 6
.= p2.i by A5,A12,A14;
end;
deffunc mC(Nat) = Sum mlt(p1,Col(M,$1));
consider MC being FinSequence of K such that
A17: len MC = len b1 & for j be Nat st j in dom MC holds MC.j = mC(j)
from FINSEQ_2:sch 1;
A18: for j st j in dom MC holds MC/.j = mC(j)
proof
let j;
assume
A19: j in dom MC;
then MC.j = mC(j) by A17;
hence thesis by A19,PARTFUN1:def 6;
end;
A20: dom b1=dom MC by A17,FINSEQ_3:29;
A21: dom p1=dom B1 by A2,FINSEQ_3:29;
A22: now
let i such that
A23: i in dom B1;
A24: len Line(M,i) = width M by MATRIX_0:def 7;
len ((B1/.i) |--b1)=len b1 by MATRLIN:def 7;
then
A25: dom Line(M,i)=dom ((B1/.i) |--b1) by A9,A24,FINSEQ_3:29;
A26: dom Line(M,i)=Seg width M by A24,FINSEQ_1:def 3;
A27: now
let k such that
A28: k in dom ((B1/.i) |--b1);
A29: [i,k] in Indices M by A21,A8,A23,A25,A26,A28,ZFMISC_1:87;
thus Line(M,i).k = M*(i,k) by A25,A26,A28,MATRIX_0:def 7
.= ((B1/.i) |--b1)/.k by A6,A29
.= ((B1/.i) |--b1).k by A28,PARTFUN1:def 6;
end;
thus B1/.i = Sum lmlt((B1/.i) |--b1,b1) by MATRLIN:35
.= Sum lmlt(Line(M,i),b1) by A25,A27,FINSEQ_1:13;
end;
A30: b1 <> {} by A4;
A31: len Col(M,j) = len M by CARD_1:def 7;
len (Sum(lmlt(p1,B1)) |--b1)=len b1 by MATRLIN:def 7;
then dom (Sum(lmlt(p1,B1)) |--b1)=dom b1 by FINSEQ_3:29;
hence (Sum(lmlt(p1,B1)) |--b1).j = (Sum(lmlt(p1,B1)) |--b1)/.j by A4,
PARTFUN1:def 6
.= (Sum(lmlt(MC,b1)) |--b1)/.j by A2,A3,A17,A18,A30,A22,MATRLIN:33
.= MC/.j by A17,MATRLIN:36
.= MC.j by A4,A20,PARTFUN1:def 6
.= Sum(mlt(p1,Col(M,j))) by A4,A17,A20
.= p1"*"p2 by A1,A7,A31,A13,FINSEQ_1:14;
end;
theorem Th31:
len b1>0 & f is additive homogeneous implies LineVec2Mx(v1|-- b1)*AutMt(f,b1,
b2) = LineVec2Mx (f.v1 |-- b2)
proof
assume that
A1: len b1>0 and
A2: f is additive homogeneous;
set A=AutMt(f,b1,b2);
set fb=f.v1 |-- b2;
set vb=v1|-- b1;
set L=LineVec2Mx vb;
set LA=L*A;
set Lf=LineVec2Mx fb;
A3: len A=len b1 by MATRLIN:def 8;
len fb=len b2 by MATRLIN:def 7;
then
A4: width Lf=len b2 by MATRIX_0:23;
A5: len vb=len b1 by MATRLIN:def 7;
then
A6: width L=len b1 by MATRIX_0:23;
len L=1 by MATRIX_0:23;
then
A7: len LA=1 by A6,A3,MATRIX_3:def 4;
A8: width A = len b2 by A1,MATRLIN:39;
then
A9: width LA=len b2 by A6,A3,MATRIX_3:def 4;
A10: now
A11: dom b2=Seg len b2 by FINSEQ_1:def 3;
A12: dom LA=Seg 1 by A7,FINSEQ_1:def 3;
A13: len (f*b1)=len b1 by FINSEQ_2:33;
let i,j such that
A14: [i,j] in Indices LA;
A15: j in Seg len b2 by A9,A14,ZFMISC_1:87;
i in dom LA by A14,ZFMISC_1:87;
then
A16: i=1 by A12,FINSEQ_1:2,TARSKI:def 1;
A17: len Col(A,j)=len A by CARD_1:def 7;
A18: now
A19: dom (f*b1)=dom b1 by A13,FINSEQ_3:29;
A20: dom A=dom Col(A,j) by A17,FINSEQ_3:29;
let k such that
A21: k in dom Col(A,j);
A22: dom A=Seg len A & A.k=A/.k by A21,A20,FINSEQ_1:def 3,PARTFUN1:def 6;
A23: dom A=dom b1 by A3,FINSEQ_3:29;
then
A24: f.(b1/.k) = f.(b1.k) by A21,A20,PARTFUN1:def 6
.= (f*b1).k by A21,A20,A23,FUNCT_1:13
.= (f*b1)/.k by A21,A20,A23,A19,PARTFUN1:def 6;
thus Col(A,j).k = A*(k,j) by A21,A20,MATRIX_0:def 8
.= Line(A,k).j by A8,A15,MATRIX_0:def 7
.= (A/.k).j by A3,A21,A20,A22,MATRIX_0:52
.= ((f*b1)/.k|--b2).j by A21,A20,A23,A24,MATRLIN:def 8;
end;
thus Lf*(i,j) = Line(Lf,i).j by A4,A15,MATRIX_0:def 7
.= (f.v1 |-- b2).j by A16,MATRIX15:25
.= (f.(Sum(lmlt(v1|--b1,b1))) |--b2).j by MATRLIN:35
.= (Sum lmlt(v1|--b1,f*b1) |--b2).j by A2,A5,MATRLIN:18
.= (v1|-- b1)"*"Col(A,j) by A1,A5,A3,A11,A15,A13,A17,A18,Th30
.= Line(L,1)"*"Col(A,j) by MATRIX15:25
.= LA*(i,j) by A6,A3,A14,A16,MATRIX_3:def 4;
end;
len Lf=1 by MATRIX_0:23;
hence thesis by A7,A9,A4,A10,MATRIX_0:21;
end;
begin :: Linear Transformations of Matrices
definition
let K,V1,V2,b1,B2;
let M be Matrix of len b1,len B2,K;
func Mx2Tran(M,b1,B2) -> Function of V1, V2 means
:Def3:
for v be Vector of
V1 holds it.v = Sum lmlt (Line(LineVec2Mx(v|--b1) * M,1),B2);
existence
proof
deffunc F(Element of V1)=Sum lmlt(Line(LineVec2Mx($1|--b1) * M,1),B2);
consider f be Function of V1,V2 such that
A1: for x be Element of V1 holds f.x = F(x) from FUNCT_2:sch 4;
take f;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be Function of V1, V2 such that
A2: for v be Vector of V1 holds F1.v = Sum lmlt (Line(LineVec2Mx(v|--b1
) * M,1),B2) and
A3: for v be Vector of V1 holds F2.v = Sum lmlt (Line(LineVec2Mx(v|--b1
) * M,1),B2);
now
let x be object;
assume x in the carrier of V1;
then reconsider v=x as Vector of V1;
thus F1.x = Sum lmlt (Line(LineVec2Mx(v|--b1) * M,1),B2) by A2
.= F2.x by A3;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th32:
for M be Matrix of len b1,len b2,K st len b1 > 0 holds
LineVec2Mx(Mx2Tran(M,b1,b2).v1|--b2) = LineVec2Mx(v1|--b1) * M
proof
set L=LineVec2Mx(v1|--b1);
A1: width L=len (v1|--b1) & len (v1|--b1)=len b1 by MATRIX_0:23,MATRLIN:def 7;
let M be Matrix of len b1,len b2,K such that
A2: len b1 > 0;
A3: len M=len b1 by A2,MATRIX_0:23;
set LM=L*M;
width M=len b2 by A2,MATRIX_0:23;
then width LM=len b2 by A1,A3,MATRIX_3:def 4;
then len Line(LM,1)=len b2 by CARD_1:def 7;
then
A4: Sum lmlt (Line(LM,1),b2) |--b2=Line(LM,1) by MATRLIN:36;
len L=1 by MATRIX_0:23;
then len LM=1 by A1,A3,MATRIX_3:def 4;
hence LM = LineVec2Mx(Sum lmlt (Line(LM,1),b2) |--b2) by A4,MATRIX15:25
.= LineVec2Mx(Mx2Tran(M,b1,b2).v1|--b2) by Def3;
end;
theorem Th33:
for M be Matrix of len b1,len B2,K st len b1 = 0 holds Mx2Tran(M
,b1,B2).v1 = 0.V2
proof
let M be Matrix of len b1,len B2,K such that
A1: len b1 = 0;
set L=LineVec2Mx(v1|--b1);
set LM=L*M;
set LL=Line(LM,1);
A2: width L=len (v1|--b1) & len (v1|--b1)=len b1 by MATRIX_0:23,MATRLIN:def 7;
A3: len M=len b1 by MATRIX_0:def 2;
then width M=0 by A1,MATRIX_0:def 3;
then width LM=0 by A2,A3,MATRIX_3:def 4;
then
A4: dom LL={};
dom lmlt(LL,B2)=dom LL/\dom B2 by Lm1;
then lmlt(LL,B2)=<*>(the carrier of V2) by A4;
then Sum lmlt(LL,B2)=0.V2 by RLVECT_1:43;
hence thesis by Def3;
end;
Lm5: for A,B being Matrix of K st width A=width B holds for i st 1<=i & i<=len
A holds Line(A+B,i)=Line(A,i)+Line(B,i)
proof
let A,B be Matrix of K such that
A1: width A=width B;
let i;
assume 1<=i & i<=len A;
then i in dom A by FINSEQ_3:25;
hence thesis by A1,MATRIX_4:59;
end;
registration
let K,V1,V2,b1,B2;
let M be Matrix of len b1,len B2,K;
cluster Mx2Tran(M,b1,B2) -> homogeneous additive;
coherence
proof
set Mx=Mx2Tran(M,b1,B2);
per cases;
suppose
A1: len b1=0;
A2: now
let a be Scalar of K,v1 be Vector of V1;
thus Mx.(a*v1) = 0.V2 by A1,Th33
.= a*0.V2 by VECTSP_1:14
.= a*Mx.v1 by A1,Th33;
end;
now
let v1,w1 be Vector of V1;
thus Mx.(v1+w1) = 0.V2 by A1,Th33
.= 0.V2+0.V2 by RLVECT_1:def 4
.= Mx.v1+0.V2 by A1,Th33
.= Mx.v1+Mx.w1 by A1,Th33;
end;
then Mx is additive homogeneous by A2,MOD_2:def 2;
hence thesis;
end;
suppose
A3: len b1>0;
A4: now
let v1,w1 be Vector of V1;
set vb=v1|--b1;
set wb=w1|--b1;
set vwb=v1+w1|--b1;
set Lvw=LineVec2Mx vwb;
set Lv=LineVec2Mx vb;
set Lw=LineVec2Mx wb;
set LLvw=Line(Lvw * M,1);
set LLv=Line(Lv * M,1);
set LLw=Line(Lw * M,1);
A5: len Lw=1 by MATRIX_0:23;
A6: len b1=len vb by MATRLIN:def 7;
A7: len M=len b1 by A3,MATRIX_0:23;
A8: width Lv=len vb by MATRIX_0:23;
then
A9: width (Lv*M)=width M by A7,A6,MATRIX_3:def 4;
then
A10: len LLv= width M by CARD_1:def 7;
A11: len Lv=1 by MATRIX_0:23;
then
A12: len (Lv*M)=1 by A8,A7,A6,MATRIX_3:def 4;
A13: len b1=len wb by MATRLIN:def 7;
width Lvw=len vwb & len b1=len vwb by MATRIX_0:23,MATRLIN:def 7;
then width (Lvw*M)=width M by A7,MATRIX_3:def 4;
then
A14: len LLvw=width M by CARD_1:def 7;
A15: dom lmlt(LLvw,B2) = dom LLvw/\dom B2 by Lm1
.= dom LLv/\dom B2 by A14,A10,FINSEQ_3:29
.= dom lmlt(LLv,B2) by Lm1;
A16: width Lw=len wb by MATRIX_0:23;
then
A17: width(Lw*M)=width M by A7,A13,MATRIX_3:def 4;
then
A18: len LLw=width M by CARD_1:def 7;
A19: dom lmlt(LLvw,B2) = dom LLvw/\dom B2 by Lm1
.= dom LLw/\dom B2 by A14,A18,FINSEQ_3:29
.= dom lmlt(LLw,B2) by Lm1;
then
A20: len lmlt(LLvw,B2)=len lmlt(LLw,B2) by FINSEQ_3:29;
Lvw = LineVec2Mx (vb+wb) by Th17
.= Lv+Lw by A6,A13,MATRIX15:27;
then Lvw *M = Lv * M +Lw*M by A11,A8,A5,A16,A7,A6,A13,MATRIX_4:63;
then LLvw=LLv+LLw by A12,A9,A17,Lm5;
then
A21: lmlt(LLvw,B2)=lmlt(LLv,B2)+lmlt(LLw,B2) by Th7;
A22: now
let i be Nat such that
A23: i in dom lmlt(LLv,B2);
lmlt(LLv,B2)/.i=lmlt(LLv,B2).i & lmlt(LLw,B2)/.i=lmlt(LLw,B2).i
by A15,A19,A23,PARTFUN1:def 6;
hence lmlt(LLvw,B2).i= lmlt(LLv,B2)/.i + lmlt(LLw,B2)/.i by A21,A15
,A23,FVSUM_1:17;
end;
len lmlt(LLvw,B2)=len lmlt(LLv,B2) by A15,FINSEQ_3:29;
then Sum lmlt(LLvw,B2)= Sum (lmlt(LLv,B2))+Sum (lmlt(LLw,B2)) by A20
,A22,RLVECT_2:2;
hence Mx.(v1+w1) = Sum (lmlt(LLv,B2))+Sum(lmlt(LLw,B2)) by Def3
.= Mx.v1+Sum(lmlt(LLw,B2)) by Def3
.= Mx.v1+Mx.w1 by Def3;
end;
now
let a be Scalar of K,v1 be Vector of V1;
set vb=v1|--b1;
set avb=a*v1|--b1;
set Lav=LineVec2Mx avb;
set Lv=LineVec2Mx vb;
set LLav=Line(Lav * M,1);
set LLv=Line(Lv * M,1);
A24: len M=len b1 by A3,MATRIX_0:23;
width Lav=len avb & len b1=len avb by MATRIX_0:23,MATRLIN:def 7;
then width (Lav*M)=width M by A24,MATRIX_3:def 4;
then
A25: len LLav=width M by CARD_1:def 7;
A26: width Lv=len vb & len b1=len vb by MATRIX_0:23,MATRLIN:def 7;
then width (Lv*M)=width M by A24,MATRIX_3:def 4;
then len LLv= width M by CARD_1:def 7;
then
A27: dom LLav=dom LLv by A25,FINSEQ_3:29;
Lav = LineVec2Mx (a*vb) by Th18
.= a*Lv by MATRIX15:29;
then
A28: Lav *M = a*(Lv * M) by A24,A26,MATRIX15:1;
A29: dom lmlt(LLav,B2)=dom LLav/\dom B2 by Lm1;
A30: dom LLv/\dom B2=dom lmlt(LLv,B2) by Lm1;
len Lv=1 by MATRIX_0:23;
then len (Lv*M)=1 by A24,A26,MATRIX_3:def 4;
then
A31: LLav = a*LLv by A28,MATRIXR1:20;
A32: now
let i be Nat such that
A33: i in dom lmlt(LLv,B2);
A34: lmlt(LLv,B2).i=lmlt(LLv,B2)/.i by A33,PARTFUN1:def 6;
i in dom LLv by A30,A33,XBOOLE_0:def 4;
then
A35: LLv.i=LLv/.i by PARTFUN1:def 6;
i in dom B2 by A30,A33,XBOOLE_0:def 4;
then
A36: B2.i=B2/.i by PARTFUN1:def 6;
A37: i in dom LLav by A27,A30,A33,XBOOLE_0:def 4;
then
A38: LLav.i=LLav/.i by PARTFUN1:def 6;
hence
lmlt(LLav,B2).i = (the lmult of V2).(LLav/.i,B2/.i) by A29,A27,A30
,A33,A36,FUNCOP_1:22
.= (a*LLv/.i)*B2/.i by A31,A37,A35,A38,FVSUM_1:50
.= a*(LLv/.i*B2/.i) by VECTSP_1:def 16
.= a*lmlt(LLv,B2)/.i by A33,A35,A36,A34,FUNCOP_1:22;
end;
len lmlt(LLav,B2)=len lmlt(LLv,B2) by A29,A27,A30,FINSEQ_3:29;
then Sum lmlt(LLav,B2)= a*Sum lmlt(LLv,B2) by A32,RLVECT_2:67;
hence Mx.(a*v1) = a*Sum lmlt(LLv,B2) by Def3
.= a*Mx.v1 by Def3;
end;
then Mx is additive homogeneous by A4,MOD_2:def 2;
hence thesis;
end;
end;
end;
theorem Th34:
f is additive homogeneous implies Mx2Tran(AutMt(f,b1,b2),b1,b2) = f
proof
assume
A1: f is additive homogeneous;
set A=AutMt(f,b1,b2);
set M=Mx2Tran(A,b1,b2);
per cases;
suppose
A2: len b1=0;
now
A3: b1 is one-to-one by MATRLIN:def 2;
reconsider R=rng b1 as Basis of V1 by MATRLIN:def 2;
let x be object such that
A4: x in the carrier of V1;
A5: Seg len b1 = {} by A2;
dim V1 = card R by VECTSP_9:def 1
.= card dom b1 by A3,CARD_1:70
.= 0 by A5,CARD_1:27,FINSEQ_1:def 3;
then (Omega).V1 = (0).V1 by VECTSP_9:29;
then the carrier of V1 = {0.V1} by VECTSP_4:def 3;
then x=0.V1 by A4,TARSKI:def 1;
hence f.x = f.(0.K*0.V1) by VECTSP_1:15
.= 0.K*(f.(0.V1)) by A1,MOD_2:def 2
.= 0.V2 by VECTSP_1:15
.= M.x by A2,A4,Th33;
end;
hence thesis by FUNCT_2:12;
end;
suppose
A6: len b1>0;
reconsider fb=f*b1,Mf=M*b1 as FinSequence;
A7: rng b1 is Subset of V1 by FINSEQ_1:def 4;
dom f=the carrier of V1 by FUNCT_2:def 1;
then
A8: len fb=len b1 by A7,FINSEQ_2:29;
dom M=the carrier of V1 by FUNCT_2:def 1;
then
A9: len Mf=len b1 by A7,FINSEQ_2:29;
now
A10: dom fb=dom Mf by A8,A9,FINSEQ_3:29;
let i;
assume 1<=i & i<=len fb;
then
A11: i in dom fb by FINSEQ_3:25;
dom fb=dom b1 by A8,FINSEQ_3:29;
then
A12: b1.i = b1/.i by A11,PARTFUN1:def 6;
LineVec2Mx(M.(b1/.i) |--b2) = LineVec2Mx(b1/.i|--b1) * A by A6,Th32
.= LineVec2Mx (f.(b1/.i) |-- b2) by A1,A6,Th31;
then M.(b1/.i) |--b2 = Line(LineVec2Mx(f.(b1/.i) |--b2),1) by MATRIX15:25
.= f.(b1/.i) |--b2 by MATRIX15:25;
then M.(b1/.i)=f.(b1/.i) by MATRLIN:34;
hence fb.i = M.(b1/.i) by A11,A12,FUNCT_1:12
.= Mf.i by A11,A10,A12,FUNCT_1:12;
end;
hence thesis by A1,A6,A8,A9,FINSEQ_1:14,MATRLIN:22;
end;
end;
theorem Th35:
for A,B be Matrix of K st i in dom A & width A = len B holds
LineVec2Mx(Line(A,i)) * B = LineVec2Mx(Line(A*B,i))
proof
let A,B be Matrix of K such that
A1: i in dom A and
A2: width A = len B;
A3: width (A*B)=width B by A2,MATRIX_3:def 4;
set LAB=LineVec2Mx(Line(A*B,i));
A4: width LAB=len Line(A*B,i) & len Line(A*B,i) =width (A*B) by CARD_1:def 7
,MATRIX_0:23;
set L=LineVec2Mx(Line(A,i));
A5: width L=len Line(A,i) & len Line(A,i)=width A by CARD_1:def 7,MATRIX_0:23;
then
A6: width (L*B)=width B by A2,MATRIX_3:def 4;
len L=1 by CARD_1:def 7;
then
A7: len (L*B)=1 by A2,A5,MATRIX_3:def 4;
len (A*B)=len A by A2,MATRIX_3:def 4;
then
A8: dom A=dom (A*B) by FINSEQ_3:29;
A9: now
let j,k such that
A10: [j,k] in Indices (L*B);
A11: k in Seg width (A*B) by A3,A6,A10,ZFMISC_1:87;
then
A12: [i,k] in Indices (A*B) by A1,A8,ZFMISC_1:87;
Indices (L*B)=[:Seg 1,Seg width B:] by A7,A6,FINSEQ_1:def 3;
then j in Seg 1 by A10,ZFMISC_1:87;
then
A13: j=1 by FINSEQ_1:2,TARSKI:def 1;
hence (L*B)*(j,k) = Line(L,1)"*"Col(B,k) by A2,A5,A10,MATRIX_3:def 4
.= Line(A,i)"*"Col(B,k) by MATRIX15:25
.= (A*B)*(i,k) by A2,A12,MATRIX_3:def 4
.= Line(A*B,i).k by A11,MATRIX_0:def 7
.= Line(LAB,j).k by A13,MATRIX15:25
.= LAB*(j,k) by A4,A11,MATRIX_0:def 7;
end;
len LAB=1 by CARD_1:def 7;
hence thesis by A4,A3,A7,A6,A9,MATRIX_0:21;
end;
theorem Th36:
for M be Matrix of len b1,len b2,K holds AutMt(Mx2Tran(M,b1,b2), b1,b2) = M
proof
let M be Matrix of len b1,len b2,K;
set MX=Mx2Tran(M,b1,b2);
set A=AutMt(MX,b1,b2);
set ONE=1.(K,len b1);
A1: len M=len b1 by MATRIX_0:25;
A2: len A=len b1 by MATRIX_0:25;
A3: len ONE=len b1 by MATRIX_0:24;
now
let i such that
A4: 1<=i & i<=len M;
A5: i in Seg len b1 by A1,A4;
A6: i in dom ONE by A1,A3,A4,FINSEQ_3:25;
reconsider Ai = A/.i as FinSequence of K by FINSEQ_1:def 11;
A7: i in dom b1 by A1,A4,FINSEQ_3:25;
then A/.i=MX.(b1/.i) |--b2 by MATRLIN:def 8;
then LineVec2Mx(Ai qua FinSequence of K) = LineVec2Mx(b1/.i|--b1) * M
by A1,A4,Th32
.= LineVec2Mx(Line(ONE,i))*M by A7,Th19
.= LineVec2Mx(Line(ONE*M,i)) by A1,A6,Th35,MATRIX_0:24
.= LineVec2Mx(Line(M,i)) by A1,MATRIXR2:68;
then
A8: Ai = Line(LineVec2Mx(Line(M,i)),1) by MATRIX15:25
.= Line(M,i) by MATRIX15:25
.= M.i by A5,MATRIX_0:52;
i in dom A by A1,A2,A4,FINSEQ_3:25;
hence M.i = A.i by A8,PARTFUN1:def 6;
end;
hence thesis by A2,FINSEQ_1:14,MATRIX_0:25;
end;
theorem
for A,B be Matrix of len b1,len B2,K holds
Mx2Tran(A+B,b1,B2) = Mx2Tran(A,b1,B2) + Mx2Tran(B,b1,B2)
proof
let A,B be Matrix of len b1,len B2,K;
set AB=A+B;
set M=Mx2Tran(A+B,b1,B2);
set MA=Mx2Tran(A,b1,B2);
set MB=Mx2Tran(B,b1,B2);
now
let x be object such that
A1: x in the carrier of V1;
reconsider v=x as Element of V1 by A1;
now
per cases;
suppose
A2: len b1=0;
hence M.x = 0.V2 by A1,Th33
.= 0.V2+0.V2 by RLVECT_1:def 4
.= MA.v+0.V2 by A2,Th33
.= MA.v+MB.v by A2,Th33
.= (MA+MB).x by MATRLIN:def 3;
end;
suppose
A3: len b1>0;
set L=LineVec2Mx(v|--b1);
A4: width L=len (v|--b1) & len (v|--b1)=len b1 by MATRIX_0:23,MATRLIN:def 7
;
set mB=lmlt(Line(L*B,1),B2);
A5: len B=len b1 & width B=len B2 by A3,MATRIX_0:23;
then
A6: width (L*B)=len B2 by A4,MATRIX_3:def 4;
then len Line(L*B,1)=len B2 by CARD_1:def 7;
then dom Line(L*B,1)=dom B2 by FINSEQ_3:29;
then
A7: dom mB=dom B2 by MATRLIN:12;
then
A8: len mB=len B2 by FINSEQ_3:29;
A9: len A=len b1 by A3,MATRIX_0:23;
len L=1 by MATRIX_0:23;
then
A11: len (L*A)=1 by A9,A4,MATRIX_3:def 4;
set mA=lmlt(Line(L*A,1),B2);
A12: width A=len B2 by A3,MATRIX_0:23;
then
A13: width (L*A)=len B2 by A9,A4,MATRIX_3:def 4;
then len Line(L*A,1)=len B2 by CARD_1:def 7;
then dom Line(L*A,1)=dom B2 by FINSEQ_3:29;
then
A14: dom mA=dom B2 by MATRLIN:12;
then
A15: len mA=len B2 by FINSEQ_3:29;
A16: dom (mA+mB) = dom B2/\dom B2 by A14,A7,Lm3
.= dom B2;
then
A17: len (mA+mB)=len B2 by FINSEQ_3:29;
A18: now
let k be Nat such that
A19: k in dom mA;
mA/.k=mA.k & mB/.k=mB.k by A14,A7,A19,PARTFUN1:def 6;
hence (mA+mB).k = mA/.k + mB/.k by A14,A16,A19,FVSUM_1:17;
end;
thus M.x = Sum lmlt (Line(L * AB,1),B2) by Def3
.= Sum lmlt (Line(L * A+L*B,1),B2) by A9,A12,A5,A4,MATRIX_4:62
.= Sum lmlt (Line(L * A,1)+Line(L*B,1),B2)by A11,A13,A6,Lm5
.= Sum (mA + mB) by Th7
.= Sum mA +Sum mB by A15,A8,A17,A18,RLVECT_2:2
.= MA.v+Sum mB by Def3
.= MA.v+MB.v by Def3
.= (MA+MB).x by MATRLIN:def 3;
end;
end;
hence M.x=(MA+MB).x;
end;
hence thesis by FUNCT_2:12;
end;
theorem
for A be Matrix of len b1,len B2,K holds
a * Mx2Tran(A,b1,B2) = Mx2Tran(a * A,b1,B2)
proof
let A be Matrix of len b1,len B2,K;
set aA=a*A;
set aM=Mx2Tran(aA,b1,B2);
set M=Mx2Tran(A,b1,B2);
now
let x be object;
assume x in the carrier of V1;
then reconsider v=x as Element of V1;
set L=LineVec2Mx(v|--b1);
set amA=lmlt(a*Line(L*A,1),B2);
set mA=lmlt(Line(L*A,1),B2);
A1: width L=len (v|--b1) & len (v|--b1)=len b1 by MATRIX_0:23,MATRLIN:def 7;
A2: len A=len b1 by MATRIX_0:def 2;
len L=1 by MATRIX_0:23;
then
A3: len (L*A)=1 by A1,A2,MATRIX_3:def 4;
A4: dom mA=dom (Line(L*A,1))/\dom B2 by Lm1;
len (a*Line(L*A,1))=len Line(L*A,1) by MATRIXR1:16;
then
A5: dom (a*Line(L*A,1))=dom Line(L*A,1) by FINSEQ_3:29;
A6: dom amA=dom (a*Line(L*A,1))/\dom B2 by Lm1;
then
A7: len mA=len amA by A5,A4,FINSEQ_3:29;
A8: now
let k be Nat such that
A9: k in dom mA;
A10: mA.k=mA/.k by A9,PARTFUN1:def 6;
k in dom Line(L*A,1) by A4,A9,XBOOLE_0:def 4;
then
A11: Line(L*A,1).k=Line(L*A,1)/.k by PARTFUN1:def 6;
k in dom B2 by A4,A9,XBOOLE_0:def 4;
then
A12: B2.k=B2/.k by PARTFUN1:def 6;
k in dom (a*Line(L*A,1)) by A5,A4,A9,XBOOLE_0:def 4;
then (a*Line(L*A,1)).k=a*(Line(L*A,1)/.k) by A11,FVSUM_1:50;
hence amA.k = (a*(Line(L*A,1)/.k))*B2/.k by A6,A5,A4,A9,A12,FUNCOP_1:22
.= a*((Line(L*A,1)/.k)*B2/.k) by VECTSP_1:def 16
.= a*(mA/.k) by A9,A11,A12,A10,FUNCOP_1:22;
end;
thus aM.x = Sum lmlt (Line(L * aA,1),B2) by Def3
.= Sum lmlt (Line(a*(L*A),1),B2) by A1,A2,MATRIXR1:22
.= Sum amA by A3,MATRIXR1:20
.= a*Sum mA by A7,A8,RLVECT_2:67
.= a*M.v by Def3
.= (a*M).x by MATRLIN:def 4;
end;
hence thesis by FUNCT_2:12;
end;
theorem
for A,B be Matrix of len b1,len b2,K st
Mx2Tran(A,b1,b2) = Mx2Tran(B,b1,b2) holds A = B
proof
let A,B be Matrix of len b1,len b2,K;
assume Mx2Tran(A,b1,b2)=Mx2Tran(B,b1,b2);
hence A = AutMt(Mx2Tran(B,b1,b2),b1,b2) by Th36
.= B by Th36;
end;
theorem
for A be Matrix of len b1,len b2,K for B be Matrix of len b2,len B3,K
st width A = len B for AB be Matrix of len b1,len B3,K st AB = A*B holds
Mx2Tran(AB,b1,B3) = Mx2Tran(B,b2,B3) * Mx2Tran(A,b1,b2)
proof
let A be Matrix of len b1,len b2,K;
let B be Matrix of len b2,len B3,K such that
A1: width A = len B;
set MB=Mx2Tran(B,b2,B3);
set MA=Mx2Tran(A,b1,b2);
let AB be Matrix of len b1,len B3,K such that
A2: AB = A*B;
set MAB=Mx2Tran(AB,b1,B3);
now
let x be object;
assume x in the carrier of V1;
then reconsider v=x as Element of V1;
set L=LineVec2Mx(v|--b1);
A3: len A=len b1 by MATRIX_0:def 2;
A4: width L=len (v|--b1) & len (v|--b1)=len b1 by MATRIX_0:23,MATRLIN:def 7;
then len L=1 & len (L*A)=len L by A3,MATRIX_0:23,MATRIX_3:def 4;
then
A5: dom (L*A)=Seg 1 by FINSEQ_1:def 3;
A6: width (L*A)=width A by A4,A3,MATRIX_3:def 4;
then
A7: len B=len b2 & len Line(L * A,1)=width A by CARD_1:def 7,MATRIX_0:def 2;
A8: 1 in Seg 1;
dom (MB*MA) = the carrier of V1 by FUNCT_2:def 1;
hence (MB*MA).x = MB.(MA.v) by FUNCT_1:12
.= MB.Sum lmlt (Line(L * A,1),b2) by Def3
.= Sum lmlt (Line(LineVec2Mx(Sum lmlt(Line(L*A,1),b2) |--b2)*B,1),B3)
by Def3
.= Sum lmlt (Line(LineVec2Mx(Line(L*A,1))*B,1),B3) by A1,A7,MATRLIN:36
.= Sum lmlt (Line(LineVec2Mx(Line(L*A*B,1)),1),B3) by A1,A6,A5,A8,Th35
.= Sum lmlt (Line(LineVec2Mx(Line(L*AB,1)),1),B3) by A1,A2,A4,A3,
MATRIX_3:33
.= Sum lmlt (Line(L*AB,1),B3) by MATRIX15:25
.= MAB.x by Def3;
end;
hence thesis by FUNCT_2:12;
end;
theorem Th41:
for A be Matrix of len b1,len b2,K st len b1>0 & len b2>0 holds
v1 in ker Mx2Tran(A,b1,b2) iff v1|--b1 in Space_of_Solutions_of (A@)
proof
let A be Matrix of len b1,len b2,K such that
A1: len b1>0 and
A2: len b2>0;
set AT=A@;
A3: width A=len b2 by A1,MATRIX_0:23;
then
A4: len AT=len b2 by A2,MATRIX_0:54;
set L=LineVec2Mx(v1|--b1);
set M=Mx2Tran(A,b1,b2);
set SA=Space_of_Solutions_of AT;
A5: width L=len (v1|--b1) by MATRIX_0:23;
len (len b2|->0.K)=len b2 by CARD_1:def 7;
then
A6: width LineVec2Mx(len b2|->0.K)=len b2 by MATRIX_0:23;
A7: width ColVec2Mx(len b2|->0.K)=1 by A2,MATRIX_0:23;
A8: len (v1|--b1) =len b1 by MATRLIN:def 7;
then
A9: len ColVec2Mx(v1|--b1)=len (v1|--b1) & width ColVec2Mx(v1|--b1)=1 by A1,
MATRIX_0:23;
A10: len A=len b1 by A1,MATRIX_0:23;
then
A11: width AT=0 implies len AT=0 by A1,A2,A3,MATRIX_0:54;
A12: width AT=len b1 by A2,A10,A3,MATRIX_0:54;
thus v1 in ker M implies v1|--b1 in SA
proof
assume v1 in ker M;
then M.v1 = 0.V2 by RANKNULL:10;
then L * A = LineVec2Mx(0.V2|-- b2) by A1,Th32
.= LineVec2Mx(len b2|->0.K ) by Th20;
then ColVec2Mx(len b2|->0.K)= AT*ColVec2Mx(v1|--b1) by A2,A10,A3,A5,A8,
MATRIX_3:22;
then
ColVec2Mx(v1|--b1) in Solutions_of(AT,ColVec2Mx(len b2|->0.K)) by A12,A8,A9
,A7;
then v1|--b1 in Solutions_of(AT,len b2|->0.K);
then v1|--b1 in the carrier of SA by A4,A11,MATRIX15:def 5;
hence thesis;
end;
assume v1|--b1 in SA;
then v1|--b1 in the carrier of SA;
then v1|--b1 in Solutions_of(AT,len b2|->0.K) by A4,A11,MATRIX15:def 5;
then
ex f be FinSequence of K st f=v1|--b1 & ColVec2Mx f in Solutions_of(AT,
ColVec2Mx(len b2|->0.K));
then ex X be Matrix of K st X = ColVec2Mx(v1|--b1) & len X = width AT &
width X = width ColVec2Mx(len b2|->0.K) & ColVec2Mx(len b2|->0.K)=AT*X;
then
A13: ColVec2Mx(len b2|->0.K)=(L*A)@ by A2,A10,A3,A5,A8,MATRIX_3:22;
width (L*A)=width A by A10,A5,A8,MATRIX_3:def 4;
then L*A = LineVec2Mx(len b2|->0.K) by A2,A3,A6,A13,MATRIX_0:56
.= LineVec2Mx(0.V2|--b2) by Th20;
then LineVec2Mx(0.V2|--b2)=LineVec2Mx(M.v1|-- b2) by A1,Th32;
then 0.V2|--b2 = Line(LineVec2Mx(M.v1|-- b2),1) by MATRIX15:25
.= M.v1|-- b2 by MATRIX15:25;
then M.v1=0.V2 by MATRLIN:34;
hence thesis by RANKNULL:10;
end;
theorem Th42:
V1 is trivial iff dim V1 = 0
proof
hereby
assume
A1: V1 is trivial;
the carrier of V1 c= {0.V1}
proof
let x be object;
assume
A2: x in the carrier of V1;
x=0.V1 by A1,A2;
hence thesis by TARSKI:def 1;
end;
then the carrier of (Omega).V1 = {0.V1} by ZFMISC_1:33
.= the carrier of (0).V1 by VECTSP_4:def 3;
then (Omega).V1=(0).V1 by VECTSP_4:29;
hence dim V1=0 by VECTSP_9:29;
end;
assume dim V1=0;
then
A3: (Omega).V1=(0).V1 by VECTSP_9:29;
for v1 holds v1=0.V1 by A3,STRUCT_0:def 5,VECTSP_4:35;
hence thesis;
end;
theorem Th43:
for V1,V2 be VectSp of K for f be linear-transformation of V1,V2
holds f is one-to-one iff ker f = (0).V1
proof
let V1,V2 be VectSp of K;
let f be linear-transformation of V1,V2;
ker f=(0).V1 implies f is one-to-one
proof
assume
A1: ker f=(0).V1;
let x,y be object such that
A2: x in dom f & y in dom f and
A3: f.x=f.y;
reconsider x9=x,y9=y as Element of V1 by A2,FUNCT_2:def 1;
x9-y9 in ker f by A3,RANKNULL:17;
then x9-y9 in the carrier of (0).V1 by A1;
then x9-y9 in {0.V1} by VECTSP_4:def 3;
then x9+-y9=0.V1 by TARSKI:def 1;
hence x = --y9 by VECTSP_1:16
.= y by RLVECT_1:17;
end;
hence thesis by RANKNULL:15;
end;
registration
let K;
let V1,V2 be VectSp of K;
let f,g be linear-transformation of V1,V2;
cluster f+g -> homogeneous additive;
coherence
proof
A1: now
let a be Scalar of K,v1 be Vector of V1;
thus (f+g).(a*v1) = f.(a*v1)+g.(a*v1) by MATRLIN:def 3
.= a*f.v1 +g.(a*v1) by MOD_2:def 2
.= a*f.v1 +a*g.v1 by MOD_2:def 2
.= a*(f.v1+g.v1) by VECTSP_1:def 14
.= a*(f+g).v1 by MATRLIN:def 3;
end;
now
let v1,w1 be Vector of V1;
thus (f+g).(v1+w1) = f.(v1+w1)+g.(v1+w1) by MATRLIN:def 3
.= f.v1+f.w1+g.(v1+w1) by VECTSP_1:def 20
.= f.v1+f.w1+(g.v1+g.w1) by VECTSP_1:def 20
.= f.v1+(f.w1+(g.v1+g.w1)) by RLVECT_1:def 3
.= f.v1+(g.v1+(g.w1+f.w1)) by RLVECT_1:def 3
.= (f.v1+g.v1)+(f.w1+g.w1) by RLVECT_1:def 3
.= (f+g).v1+(f.w1+g.w1) by MATRLIN:def 3
.= (f+g).v1+(f+g).w1 by MATRLIN:def 3;
end;
then f+g is additive homogeneous by A1,MOD_2:def 2;
hence thesis;
end;
end;
registration
let K;
let V1,V2 be VectSp of K;
let f be linear-transformation of V1,V2,a;
cluster a*f -> homogeneous additive;
coherence
proof
A1: now
let b be Scalar of K,v1 be Vector of V1;
thus (a*f).(b*v1) = a*(f.(b*v1)) by MATRLIN:def 4
.= a*(b*f.v1) by MOD_2:def 2
.= (a*b)*f.v1 by VECTSP_1:def 16
.= b*(a*f.v1) by VECTSP_1:def 16
.= b*(a*f).v1 by MATRLIN:def 4;
end;
now
let v1,w1 be Vector of V1;
thus (a*f).(v1+w1) = a*(f.(v1+w1)) by MATRLIN:def 4
.= a*(f.v1+f.w1) by VECTSP_1:def 20
.= a*f.v1+a*f.w1 by VECTSP_1:def 14
.= (a*f).v1+a*f.w1 by MATRLIN:def 4
.= (a*f).v1+(a*f).w1 by MATRLIN:def 4;
end;
then a*f is additive homogeneous by A1,MOD_2:def 2;
hence thesis;
end;
end;
definition
let K;
let V1,V2,V3 be VectSp of K;
let f1 be linear-transformation of V1, V2;
let f2 be linear-transformation of V2, V3;
redefine func f2*f1 -> linear-transformation of V1,V3; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence by MOD_2:2;
end;
theorem Th44:
for A be Matrix of len b1,len b2,K st the_rank_of A = len b1
holds Mx2Tran(A,b1,b2) is one-to-one
proof
let A be Matrix of len b1,len b2,K such that
A1: the_rank_of A = len b1;
set S=Space_of_Solutions_of (A@);
set M=Mx2Tran(A,b1,b2);
A2: now
per cases;
suppose
len b1=0;
then dim V1=0 by Th21;
then
A3: (Omega).V1=(0).V1 by VECTSP_9:29;
the carrier of ker M c= the carrier of V1 by VECTSP_4:def 2;
hence the carrier of ker M c= {0.V1} by A3,VECTSP_4:def 3;
end;
suppose
A4: len b1>0;
A5: len b1<= width A by A1,MATRIX13:74;
then
A6: width (A@) = len A by A4,MATRIX_0:54;
A7: len A=len b1 by A4,MATRIX_0:23;
A8: width A=len b2 by A4,MATRIX_0:23;
thus the carrier of ker M c= {0.V1}
proof
let x be object such that
A9: x in the carrier of ker M;
the carrier of ker M c= the carrier of V1 by VECTSP_4:def 2;
then reconsider v=x as Element of V1 by A9;
dim S = len b1 - the_rank_of (A@) by A4,A7,A6,MATRIX15:68
.= len b1 - len b1 by A1,MATRIX13:84
.= 0;
then
A10: (Omega).S=(0).S by VECTSP_9:29;
v in ker M by A9;
then v|--b1 in S by A4,A8,A5,Th41;
then v|--b1 in the carrier of (0).S by A10;
then v|--b1 in the carrier of (0).((len b1)-VectSp_over K) by A7,A6,
VECTSP_4:36;
then v|--b1 in {0.((len b1)-VectSp_over K)} by VECTSP_4:def 3;
then v|--b1 = 0.((len b1)-VectSp_over K) by TARSKI:def 1
.= len b1 |->0.K by MATRIX13:102
.= 0.V1|-- b1 by Th20;
then v=0.V1 by MATRLIN:34;
hence thesis by TARSKI:def 1;
end;
end;
end;
0.V1 in ker M by RANKNULL:11;
then 0.V1 in the carrier of ker M;
then {0.V1} c= the carrier of ker M by ZFMISC_1:31;
then the carrier of ker M = {0.V1} by A2,XBOOLE_0:def 10
.= the carrier of (0).V1 by VECTSP_4:def 3;
then ker M=(0).V1 by VECTSP_4:29;
hence thesis by Th43;
end;
Lm6: the_rank_of 1.(K,n)=n
proof
A1: 1_K<>0.K;
n+0>0 or n=0;
then
A2: n>=1 or n=0 by NAT_1:19;
Det 1.(K,n) = 1_K by A2,MATRIXR2:41,MATRIX_7:16;
hence thesis by A1,MATRIX13:83;
end;
theorem Th45:
MX2FinS 1.(K,n) is OrdBasis of n-VectSp_over K
proof
set ONE=1.(K,n);
A1: the_rank_of ONE=n by Lm6;
then
A2: ONE is one-to-one by MATRIX13:105;
for i,j st [i,j] in Indices ONE & ONE*(i,j) <> 0.K holds i=j
by MATRIX_1:def 3;
then ONE is diagonal by MATRIX_1:def 10;
then lines ONE is Basis of n-VectSp_over K by A1,MATRIX13:111;
hence thesis by A2,MATRLIN:def 2;
end;
theorem Th46:
for M be OrdBasis of (len b2)-VectSp_over K st
M = MX2FinS 1.(K,len b2)
for v1 be Vector of (len b2)-VectSp_over K holds v1|--M = v1
proof
let M be OrdBasis of (len b2)-VectSp_over K such that
A1: M = MX2FinS 1.(K,len b2);
let v1 be Vector of (len b2)-VectSp_over K;
set vM=v1|--M;
consider KL be Linear_Combination of (len b2)-VectSp_over K such that
A2: v1 = Sum(KL) & Carrier KL c= rng M and
A3: for k st 1<=k & k<=len (v1|--M) holds vM/.k=KL.(M/.k) by MATRLIN:def 7;
reconsider t1=v1 as Element of (len b2)-tuples_on the carrier of K by
MATRIX13:102;
A4: len t1=len b2 by CARD_1:def 7;
A5: len M=dim ((len b2)-VectSp_over K) & dim ((len b2)-VectSp_over K) =len
b2 by Th21,MATRIX13:112;
A6: len vM=len M by MATRLIN:def 7;
now
A7: dom M= dom vM by A6,FINSEQ_3:29;
A8: the_rank_of 1.(K,len b2)=len b2 by Lm6;
set F=FinS2MX(KL (#) M);
A9: Indices 1.(K,len b2)=[:Seg len b2,Seg len b2:] by MATRIX_0:24;
let i such that
A10: 1<=i & i<=len t1;
A11: i in Seg len b2 by A4,A10;
then
A12: [i,i] in [:Seg len b2,Seg len b2:] by ZFMISC_1:87;
A13: width 1.(K,len b2)=len b2 by MATRIX_0:24;
then
A14: Line(1.(K,len b2),i).i = 1.(K,len b2)*(i,i) by A11,MATRIX_0:def 7
.= 1_K by A9,A12,MATRIX_1:def 3;
A15: len Col(F,i)=len F by CARD_1:def 7;
then
A16: dom Col(F,i)=dom F by FINSEQ_3:29;
A17: len F=len M by VECTSP_6:def 5;
then
A18: dom F= dom M by FINSEQ_3:29;
A19: i in dom Col(F,i) by A4,A5,A10,A17,A15,FINSEQ_3:25;
A20: width F=len b2 by A5,A17,MATRIX_0:24;
now
let j such that
A21: j in dom Col(F,i) and
A22: j<>i;
A23: dom Col(F,i)=Seg len b2 by A5,A17,A15,FINSEQ_1:def 3;
then
A24: [j,i] in [:Seg len b2,Seg len b2:] by A11,A21,ZFMISC_1:87;
A25: Line(F,j) = (KL (#) M).j by A5,A17,A21,A23,MATRIX_0:52
.= KL.(M/.j) * M/.j by A16,A21,VECTSP_6:def 5;
A26: Col(F,i).j = F*(j,i) by A16,A21,MATRIX_0:def 8
.= Line(F,j).i by A11,A20,MATRIX_0:def 7;
A27: Line(1.(K,len b2),j).i = 1.(K,len b2)*(j,i) by A11,A13,MATRIX_0:def 7
.= 0.K by A9,A22,A24,MATRIX_1:def 3;
M/.j = M.j by A16,A18,A21,PARTFUN1:def 6
.= Line(1.(K,len b2),j) by A1,A21,A23,MATRIX_0:52;
hence Col(F,i).j = (KL.(M/.j) * Line(1.(K,len b2),j)).i by A13,A26,A25,
MATRIX13:102
.= KL.(M/.j)*0.K by A11,A13,A27,FVSUM_1:51
.= 0.K;
end;
then
A28: Col(F,i).i = Sum Col(F,i) by A19,MATRIX_3:12
.= v1.i by A1,A2,A11,A8,MATRIX13:105,107;
A29: Line(F,i) = (KL (#) M).i by A5,A11,A17,MATRIX_0:52
.= KL.(M/.i) * M/.i by A19,A16,VECTSP_6:def 5;
A30: Col(F,i).i = F*(i,i) by A19,A16,MATRIX_0:def 8
.= Line(F,i).i by A11,A20,MATRIX_0:def 7;
M/.i = M.i by A19,A16,A18,PARTFUN1:def 6
.= Line(1.(K,len b2),i) by A1,A11,MATRIX_0:52;
then Col(F,i).i = (KL.(M/.i) * Line(1.(K,len b2),i)).i by A30,A13,A29,
MATRIX13:102
.= KL.(M/.i)*1_K by A11,A13,A14,FVSUM_1:51
.= KL.(M/.i);
hence t1.i = vM/.i by A3,A4,A6,A5,A10,A28
.= vM.i by A19,A16,A18,A7,PARTFUN1:def 6;
end;
hence thesis by A4,A6,A5,FINSEQ_1:14;
end;
theorem Th47:
for M be OrdBasis of (len b2)-VectSp_over K st
M = MX2FinS 1.(K,len b2)
for A be Matrix of len b1,len M,K st A = AutMt(f,b1,b2) &
f is additive homogeneous
holds Mx2Tran(A,b1,M).v1 = f.v1 |-- b2
proof
let M be OrdBasis of (len b2)-VectSp_over K such that
A1: M = MX2FinS 1.(K,len b2);
let A be Matrix of len b1,len M,K such that
A2: A = AutMt(f,b1,b2) and
A3: f is additive homogeneous;
reconsider f9=f as linear-transformation of V1,V2 by A3;
set MM=Mx2Tran(A,b1,M);
per cases;
suppose
A4: len b1=0;
then dim V1=0 by Th21;
then (Omega).V1=(0).V1 by VECTSP_9:29;
then the carrier of V1={0.V1} by VECTSP_4:def 3;
then v1=0.V1 by TARSKI:def 1;
then v1 in ker f9 by RANKNULL:11;
hence f.v1|--b2 = 0.V2|--b2 by RANKNULL:10
.= len b2|-> 0.K by Th20
.= 0.((len b2)-VectSp_over K) by MATRIX13:102
.= MM.v1 by A4,Th33;
end;
suppose
A5: len b1>0;
then LineVec2Mx(MM.v1|--M) = LineVec2Mx(v1|--b1)*A by Th32
.= LineVec2Mx(f.v1|--b2) by A2,A3,A5,Th31;
hence f.v1|--b2 = Line(LineVec2Mx(MM.v1|--M),1) by MATRIX15:25
.= MM.v1|--M by MATRIX15:25
.= MM.v1 by A1,Th46;
end;
end;
definition
let K be add-associative right_zeroed right_complementable Abelian
associative well-unital distributive non empty doubleLoopStr,
V1,V2 be Abelian add-associative right_zeroed
right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital
non empty ModuleStr over K;
let W be Subspace of V1;
let f be Function of V1,V2;
redefine func f|W -> Function of W,V2; :: redefines | (MATRLIN2, definition)
coherence
proof
the carrier of W c= the carrier of V1 by VECTSP_4:def 2;
hence thesis by FUNCT_2:32;
end;
end;
definition
let K be Field;
let V1,V2 be VectSp of K;
let W be Subspace of V1;
let f be linear-transformation of V1, V2;
redefine func f|W -> linear-transformation of W,V2; :: redefines | (MATRLIN2, definition)
coherence
proof
set F=f|W;
A1: dom F=the carrier of W by FUNCT_2:def 1;
A2: now
let a be Scalar of K,v1 be Vector of W;
reconsider v2=v1 as Vector of V1 by VECTSP_4:10;
a*v1=a*v2 by VECTSP_4:14;
hence F.(a*v1) = f.(a*v2) by A1,FUNCT_1:47
.= a*f.v2 by MOD_2:def 2
.= a*F.v1 by A1,FUNCT_1:47;
end;
now
let v1,w1 be Vector of W;
reconsider v2=v1,w2=w1 as Vector of V1 by VECTSP_4:10;
v1+w1=v2+w2 by VECTSP_4:13;
hence F.(v1+w1) = f.(v2+w2) by A1,FUNCT_1:47
.= f.v2+f.w2 by VECTSP_1:def 20
.= F.v1+f.w2 by A1,FUNCT_1:47
.= F.v1+F.w1 by A1,FUNCT_1:47;
end;
then F is additive homogeneous by A2,MOD_2:def 2;
hence thesis;
end;
end;
Lm7: for A be Matrix of len b1,len b2,K st len b1>0 & len b2>0 holds nullity
Mx2Tran(A,b1,b2) = len b1 - the_rank_of A
proof
set I=id V1;
reconsider BB=MX2FinS 1.(K,len b1) as OrdBasis of (len b1)-VectSp_over K by
Th45;
let A be Matrix of len b1,len b2,K such that
A1: len b1>0 and
A2: len b2>0;
len BB = dim ((len b1)-VectSp_over K) by Th21
.= len b1 by MATRIX13:112;
then reconsider AI=AutMt(I,b1,b1) as Matrix of len b1,len BB,K;
A3: AutMt(I,b1,b1)=1.(K,len b1) & 0.K<>1_K by Th28;
len b1+0>0 by A1;
then len b1>=1 by NAT_1:19;
then Det 1.(K,len b1)=1_K by MATRIX_7:16;
then
A4: the_rank_of AI=len b1 by A3,MATRIX13:83;
set S=Space_of_Solutions_of (A@);
set KER=ker Mx2Tran(A,b1,b2);
set MAI=Mx2Tran(AI,b1,BB);
set MK=MAI|KER;
A5: dom MK=the carrier of KER by FUNCT_2:def 1;
A6: the carrier of im MK c= the carrier of S
proof
let x be object such that
A7: x in the carrier of im MK;
the carrier of im MK c= the carrier of (len b1)-VectSp_over K by
VECTSP_4:def 2;
then reconsider v=x as Element of (len b1)-VectSp_over K by A7;
v in im MK by A7;
then consider w be Element of KER such that
A8: v = MK.w by RANKNULL:13;
A9: w in KER;
then w in V1 by VECTSP_4:9;
then reconsider W=w as Vector of V1;
MK.w = MAI.w by A5,FUNCT_1:47
.= I.W |--b1 by Th47
.= W|--b1;
then MK.w in S by A1,A2,A9,Th41;
hence thesis by A8;
end;
len A = len b1 & width A=len b2 by A1,MATRIX_0:23;
then
A10: width (A@)=len b1 by A2,MATRIX_0:54;
A11: MAI is one-to-one by A4,Th44;
dim ((len b1)-VectSp_over K) = len b1 by MATRIX13:112
.= dim V1 by Th21
.= rank MAI by A11,RANKNULL:45
.= dim im MAI;
then
A12: (Omega).((len b1)-VectSp_over K) = (Omega).(im MAI) by VECTSP_9:28;
the carrier of S c= the carrier of im MK
proof
let x be object such that
A13: x in the carrier of S;
the carrier of S c= the carrier of (len b1)-VectSp_over K by A10,
VECTSP_4:def 2;
then reconsider v=x as Element of (len b1)-VectSp_over K by A13;
A14: v in S by A13;
v in im MAI by A12;
then consider w be Element of V1 such that
A15: v = MAI.w by RANKNULL:13;
MAI.w = I.w |-- b1 by Th47
.= w|--b1;
then w in KER by A1,A2,A15,A14,Th41;
then reconsider W=w as Element of KER;
v = MK.W by A5,A15,FUNCT_1:47;
then v in im MK by RANKNULL:13;
hence thesis;
end;
then the carrier of S = the carrier of im MK by A6,XBOOLE_0:def 10;
then
A16: im MK = S by A10,VECTSP_4:29;
MAI is one-to-one by A4,Th44;
then MK is one-to-one by FUNCT_1:52;
hence nullity Mx2Tran(A,b1,b2) = rank MK by RANKNULL:45
.= len b1-the_rank_of (A@) by A1,A10,A16,MATRIX15:68
.= len b1-the_rank_of A by MATRIX13:84;
end;
begin :: The Main Theorem
theorem Th48:
for f be linear-transformation of V1,V2 holds
rank f = the_rank_of AutMt(f,b1,b2)
proof
let f be linear-transformation of V1,V2;
set A=AutMt(f,b1,b2);
per cases;
suppose
A1: len b1=0;
then len A=0 by MATRIX_0:def 2;
then dim V1= rank(f) + nullity(f) & the_rank_of A=0 by MATRIX13:74
,RANKNULL:44;
hence thesis by A1,Th21;
end;
suppose
A2: len b1>0& len b2=0;
then width A=0 by MATRIX_0:23;
then
A3: the_rank_of A=0 by MATRIX13:74;
dim V2=0 by A2,Th21;
hence thesis by A3,VECTSP_9:25;
end;
suppose
A4: len b1>0 & len b2>0;
A5: rank f+nullity f = dim V1 by RANKNULL:44
.= len b1 by Th21;
nullity f = nullity Mx2Tran(A,b1,b2) by Th34
.= len b1 - the_rank_of A by A4,Lm7;
hence thesis by A5;
end;
end;
theorem
for M be Matrix of len b1,len b2,K holds
rank Mx2Tran(M,b1,b2) = the_rank_of M
proof
let M be Matrix of len b1,len b2,K;
thus rank Mx2Tran(M,b1,b2) = the_rank_of AutMt(Mx2Tran(M,b1,b2),b1,b2) by
Th48
.= the_rank_of M by Th36;
end;
theorem
for f be linear-transformation of V1,V2 st dim V1=dim V2 holds
ker f is non trivial iff Det AutEqMt(f,b1,b2) = 0.K
proof
let f be linear-transformation of V1,V2 such that
A1: dim V1=dim V2;
set A=AutEqMt(f,b1,b2);
dim V2=len b2 by Th21;
then
A2: A=AutMt(f,b1,b2) by A1,Def2,Th21;
A3: dim V1=rank f+nullity f by RANKNULL:44;
A4: len b1=dim V1 & rank f=the_rank_of AutMt(f,b1,b2) by Th21,Th48;
hereby
assume ker f is non trivial;
then rank f <> dim V1 by A3,Th42;
hence Det A = 0.K by A4,A2,MATRIX13:83;
end;
assume Det A=0.K;
then dim ker f<>0 by A4,A2,A3,MATRIX13:83;
hence thesis by Th42;
end;
Lm8: for f be linear-transformation of V1,V2,g be Function of V2,V3 holds g * f
= (g|im f)*f
proof
let f be linear-transformation of V1,V2,g be Function of V2,V3;
dom f=[#]V1 by FUNCT_2:def 1;
then [#]im f = f.:dom f by RANKNULL:def 2
.= rng f by RELAT_1:113;
hence (g|im f)* f = g*(id rng f)*f by RELAT_1:65
.= g*((id rng f)*f) by RELAT_1:36
.= g*f by RELAT_1:54;
end;
theorem
for f be linear-transformation of V1,V2,
g be linear-transformation of V2,V3 st
g|im f is one-to-one holds
rank (g*f) = rank f & nullity (g*f) = nullity f
proof
let f be linear-transformation of V1,V2, g be linear-transformation of V2,V3
such that
A1: g|im f is one-to-one;
the carrier of im (g*f) = [#]im (g*f) .= (g*f).:[#]V1 by RANKNULL:def 2
.= ((g|im f)*f).:([#]V1) by Lm8
.= (g|im f).:(f.:[#]V1) by RELAT_1:126
.= (g|im f).:([#]im f) by RANKNULL:def 2
.= [#]im (g|im f) by RANKNULL:def 2
.= the carrier of im(g|im f);
then
A2: rank(g*f) = rank (g|im f) by VECTSP_4:29
.= rank f by A1,RANKNULL:45;
nullity(f) + rank (f) = dim V1 by RANKNULL:44
.= nullity(g*f) + rank (g*f) by RANKNULL:44;
hence thesis by A2;
end;