:: Linear Transformations of Euclidean Topological Spaces. Part {II}
:: by Karol P\kak
::
:: Received October 26, 2010
:: Copyright (c) 2010-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 ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1, ENTROPY1,
EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2,
FVSUM_1, INCSP_1, LMOD_7, MATRIX_1, MATRIX_3, MATRIX13, MATRLIN,
MATRLIN2, MESFUNC1, NAT_1, NUMBERS, ORDINAL4, PARTFUN1, PBOOLE, PRE_TOPC,
PRVECT_1, QC_LANG1, RANKNULL, RELAT_1, RLAFFIN1, RLSUB_1, RLVECT_1,
RLVECT_2, RLVECT_3, RLVECT_5, RVSUM_1, SEMI_AF1, STRUCT_0, SUBSET_1,
SUPINF_2, TARSKI, TREES_1, VALUED_0, VALUED_1, VECTSP_1, VECTSP10,
XBOOLE_0, XXREAL_0, FUNCT_7, GROUP_1, XCMPLX_0;
notations GCD_1, VECTSP_2, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, CARD_1,
ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FINSET_1, FUNCT_1,
RELSET_1, PARTFUN1, NAT_1, VALUED_0, FUNCT_2, FINSEQ_1, FINSEQ_2,
FINSEQ_3, STRUCT_0, RLVECT_1, RLVECT_2, RLVECT_3, VECTSP_1,
MATRIX_0, MATRIX_1, MATRIX_3, VECTSP_4, VECTSP_6, VECTSP_7,
MATRIX13, RVSUM_1, ALGSTR_0, FVSUM_1, RANKNULL, PRE_TOPC,
MATRIX_6, MATRLIN, MATRLIN2, NAT_D, EUCLID, GROUP_1, MATRIX11,
FINSEQOP, ENTROPY1, RLSUB_1, RUSUB_4, PRVECT_1, RLAFFIN1,
MATRTOP1;
constructors GCD_1, VECTSP_2, BINARITH, ENTROPY1, FVSUM_1, LAPLACE,
MATRIX_6, MATRIX11, MATRIX13, MATRLIN2, MATRTOP1, MONOID_0,
RANKNULL, REALSET1, RELSET_1, RLAFFIN1, RLVECT_3, RUSUB_5,
VECTSP10, MATRIX15, MATRIX_1, FUNCSDOM, PCOMPS_1, SQUARE_1,
BINOP_2, MATRIX_3;
registrations CARD_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1,
FUNCT_2, MATRIX13, MATRLIN2, MATRTOP1, MEMBERED, MONOID_0, NAT_1,
NUMBERS, PRVECT_1, RELAT_1, RELSET_1, RLAFFIN1, RLVECT_3, RVSUM_1,
STRUCT_0, RLVECT_2, VALUED_0, VECTSP_1, VECTSP_2, VECTSP_9,
XREAL_0, XXREAL_0, MATRIX_6, ORDINAL1, MATRIX_3, LAPLACE;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0;
equalities EUCLID, FINSEQ_1, MATRIX13, MATRTOP1, STRUCT_0, VECTSP_1, XBOOLE_0;
expansions FINSEQ_1, STRUCT_0, TARSKI, XBOOLE_0;
theorems CARD_1, CARD_2, ENTROPY1, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSEQ_4, FINSEQ_6, FUNCT_1, FUNCT_2, FVSUM_1, LAPLACE, MATRIX_0,
MATRIX_6, MATRIX13, MATRIXR1, MATRLIN, MATRLIN2, MATRPROB, MATRTOP1,
NAT_1, ORDINAL1, PARTFUN1, PRE_POLY, RANKNULL, RELAT_1, RLAFFIN1,
RLSUB_1, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, RVSUM_1, STRUCT_0,
SUBSET_1, TARSKI, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9,
XBOOLE_0, XBOOLE_1, XREAL_0, XREAL_1, ZFMISC_1, TOPREAL3;
schemes FINSEQ_1, FUNCT_2, NAT_1;
begin :: Correspondence Between Euclidean Topological Space and Vector
:: Space over F_Real
reserve X for set,
n,m,k for Nat,
K for Field,
f for n-element real-valued FinSequence,
M for Matrix of n,m,F_Real;
Lm1: the carrier of n-VectSp_over F_Real=the carrier of TOP-REAL n
proof
thus the carrier of n-VectSp_over F_Real=REAL n by MATRIX13:102
.=the carrier of TOP-REAL n by EUCLID:22;
end;
Lm2: 0.(n-VectSp_over F_Real)=0.(TOP-REAL n)
proof
thus 0.(n-VectSp_over F_Real)=n|->(0.F_Real) by MATRIX13:102
.=0*n
.=0.(TOP-REAL n) by EUCLID:70;
end;
Lm3: f is Point of TOP-REAL n
proof
len f=n & @@f = f by CARD_1:def 7;
hence thesis by TOPREAL3:46;
end;
theorem Th1:
X is Linear_Combination of n-VectSp_over F_Real
iff
X is Linear_Combination of TOP-REAL n
proof
set V=n-VectSp_over F_Real;
set T=TOP-REAL n;
hereby assume X is Linear_Combination of V;
then reconsider L=X as Linear_Combination of V;
consider S be finite Subset of V such that
A1: for v be Element of V st not v in S holds L.v=0.F_Real
by VECTSP_6:def 1;
A2: now let v be Element of T;
assume A3: not v in S;
v is Element of V by Lm1;
hence 0=L.v by A1,A3;
end;
(L is Element of Funcs(the carrier of T,REAL)) & S is finite Subset of T
by Lm1;
hence X is Linear_Combination of T by A2,RLVECT_2:def 3;
end;
assume X is Linear_Combination of T;
then reconsider L=X as Linear_Combination of T;
consider S be finite Subset of T such that
A4: for v be Element of T st not v in S holds L.v=0 by RLVECT_2:def 3;
A5: now let v be Element of V;
assume A6: not v in S;
v is Element of T by Lm1;
hence 0.F_Real=L.v by A4,A6;
end;
L is Element of Funcs(the carrier of V,the carrier of F_Real) &
S is finite Subset of V by Lm1;
hence thesis by A5,VECTSP_6:def 1;
end;
theorem Th2:
for Lv be Linear_Combination of n-VectSp_over F_Real,
Lr be Linear_Combination of TOP-REAL n st Lr = Lv
holds Carrier Lr = Carrier Lv
proof
set V=n-VectSp_over F_Real;
set T=TOP-REAL n;
let Lv be Linear_Combination of V,
Lr be Linear_Combination of T such that
A1: Lr=Lv;
thus Carrier Lr c=Carrier Lv
proof
let x be object;
assume A2: x in Carrier Lr;
then reconsider v=x as Element of T;
reconsider u=v as Element of V by Lm1;
Lv.u<>0.F_Real by A1,A2,RLVECT_2:19;
hence thesis by VECTSP_6:1;
end;
let x be object;
assume x in Carrier Lv;
then consider u be Element of V such that
A3: x=u and
A4: Lv.u<>0.F_Real by VECTSP_6:1;
reconsider v=u as Element of T by Lm1;
v in Carrier Lr by A1,A4,RLVECT_2:19;
hence thesis by A3;
end;
theorem Th3:
for F be FinSequence of TOP-REAL n,
fr be Function of TOP-REAL n,REAL,
Fv be FinSequence of n-VectSp_over F_Real,
fv be Function of n-VectSp_over F_Real,F_Real st fr = fv & F = Fv
holds fr(#)F = fv(#)Fv
proof
let F be FinSequence of TOP-REAL n,
fr be Function of TOP-REAL n,REAL,
Fv be FinSequence of n-VectSp_over F_Real,
fv be Function of n-VectSp_over F_Real,F_Real;
assume that
A1: fr=fv and
A2: F=Fv;
A3: len(fv(#)Fv)=len Fv by VECTSP_6:def 5;
A4: len(fr(#)F)=len F by RLVECT_2:def 7;
now reconsider T=TOP-REAL n as RealLinearSpace;
let i be Nat;
reconsider Fi=F/.i as FinSequence of REAL by EUCLID:24;
reconsider Fvi=Fv/.i as Element of n-tuples_on the carrier of F_Real
by MATRIX13:102;
reconsider Fii=F/.i as Element of T;
assume A5: 1<=i & i<=len F;
then A6: i in dom(fv(#)Fv) by A2,A3,FINSEQ_3:25;
i in dom F by A5,FINSEQ_3:25;
then A7: F/.i=F.i by PARTFUN1:def 6;
i in dom Fv by A2,A5,FINSEQ_3:25;
then A8: Fv/.i=Fv.i by PARTFUN1:def 6;
i in dom(fr(#)F) by A4,A5,FINSEQ_3:25;
hence (fr(#)F).i=fr.Fii*Fii by RLVECT_2:def 7
.=fr.Fi*Fi by EUCLID:65
.=fv.(Fv/.i)*Fvi by A1,A2,A7,A8,MATRIXR1:17
.=fv.(Fv/.i)*(Fv/.i) by MATRIX13:102
.=(fv(#)Fv).i by A6,VECTSP_6:def 5;
end;
hence thesis by A2,A4,A3;
end;
theorem Th4:
for F be FinSequence of TOP-REAL n,
Fv be FinSequence of n-VectSp_over F_Real st Fv = F
holds Sum F = Sum Fv
proof
set T=TOP-REAL n;
set V=n-VectSp_over F_Real;
let F be FinSequence of T;
let Fv be FinSequence of V such that
A1: Fv=F;
reconsider T=TOP-REAL n as RealLinearSpace;
consider f be sequence of the carrier of T such that
A2: Sum F=f.(len F) and
A3: f.0=0.T and
A4: for j be Nat,v be Element of T st j<len F & v=F.(j+1)
holds f.(j+1)=f.j+v by RLVECT_1:def 12;
consider fv be sequence of the carrier of V such that
A5: Sum Fv=fv.(len Fv) and
A6: fv.0=0.V and
A7: for j be Nat,v be Element of V st j<len Fv & v=Fv.(j+1)
holds fv.(j+1)=fv.j+v by RLVECT_1:def 12;
defpred P[Nat] means
$1<=len F implies f.$1=fv.$1;
A8: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A9: P[i];
set i1=i+1;
reconsider Fvi1=Fv/.i1,fvi=fv.i as Element of n-tuples_on
the carrier of F_Real by MATRIX13:102;
A10: @@Fvi1=Fvi1 & @@fvi=fvi;
reconsider Fi1=F/.i1 as Element of T;
assume A11: i1<=len F;
then A12: i<len F by NAT_1:13;
1<=i1 by NAT_1:11;
then A13: i1 in dom F by A11,FINSEQ_3:25;
then F.i1=F/.i1 by PARTFUN1:def 6;
then A14: f.i1=f.i+Fi1 by A4,A12;
A15: Fv/.i1=Fv.i1 by A1,A13,PARTFUN1:def 6;
then Fvi1=F/.i1 by A1,A13,PARTFUN1:def 6;
hence f.i1=@fvi+@Fvi1 by A9,A11,A14,EUCLID:64,NAT_1:13
.=fvi+Fvi1 by A10,MATRTOP1:1
.=fv.i+Fv/.i1 by MATRIX13:102
.=fv.i1 by A1,A7,A12,A15;
end;
A16: P[0] by A3,A6,Lm2;
for n be Nat holds P[n] from NAT_1:sch 2(A16,A8);
hence thesis by A1,A2,A5;
end;
theorem Th5:
for Lv be Linear_Combination of n-VectSp_over F_Real,
Lr be Linear_Combination of TOP-REAL n st Lr = Lv
holds Sum Lr = Sum Lv
proof
set V=n-VectSp_over F_Real;
set T=TOP-REAL n;
let Lv be Linear_Combination of V;
let Lr be Linear_Combination of T such that
A1: Lr=Lv;
consider F be FinSequence of the carrier of T such that
A2: (F is one-to-one) & rng F=Carrier(Lr) and
A3: Sum Lr=Sum(Lr(#)F) by RLVECT_2:def 8;
reconsider F1=F as FinSequence of the carrier of V by Lm1;
A4: Lr(#)F=Lv(#)F1 by A1,Th3;
Carrier(Lr)=Carrier(Lv) by A1,Th2;
hence Sum Lv=Sum(Lv(#)F1) by A2,VECTSP_6:def 6
.=Sum Lr by A3,A4,Th4;
end;
theorem Th6:
for Af be Subset of n-VectSp_over F_Real,
Ar be Subset of TOP-REAL n st Af = Ar
holds [#]Lin Ar = [#]Lin Af
proof
set V=n-VectSp_over F_Real;
set T=TOP-REAL n;
let Af be Subset of V;
let Ar be Subset of T such that
A1: Af=Ar;
hereby let x be object;
assume x in [#]Lin Ar;
then x in Lin Ar;
then consider L be Linear_Combination of Ar such that
A2: x=Sum L by RLVECT_3:14;
reconsider L1=L as Linear_Combination of V by Th1;
Carrier L1=Carrier L & Carrier L c=Ar by Th2,RLVECT_2:def 6;
then A3: L1 is Linear_Combination of Af by A1,VECTSP_6:def 4;
Sum L1=Sum L by Th5;
then x in Lin Af by A2,A3,VECTSP_7:7;
hence x in [#]Lin Af;
end;
let x be object;
assume x in [#]Lin Af;
then x in Lin Af;
then consider L be Linear_Combination of Af such that
A4: x=Sum L by VECTSP_7:7;
reconsider L1=L as Linear_Combination of T by Th1;
Carrier L1=Carrier L & Carrier L c=Af by Th2,VECTSP_6:def 4;
then A5: L1 is Linear_Combination of Ar by A1,RLVECT_2:def 6;
Sum L1=Sum L by Th5;
then x in Lin Ar by A4,A5,RLVECT_3:14;
hence thesis;
end;
theorem Th7:
for Af be Subset of n-VectSp_over F_Real,
Ar be Subset of TOP-REAL n st Af = Ar
holds
Af is linearly-independent
iff
Ar is linearly-independent
proof
set V=n-VectSp_over F_Real;
let AV be Subset of V;
set T=TOP-REAL n;
let AR be Subset of T such that
A1: AV=AR;
hereby assume A2: AV is linearly-independent;
now let L be Linear_Combination of AR;
reconsider L1=L as Linear_Combination of V by Th1;
A3: Carrier L1=Carrier L by Th2;
assume Sum L=0.T;
then A4: 0.V=Sum L by Lm2
.=Sum L1 by Th5;
Carrier L c=AR by RLVECT_2:def 6;
then L1 is Linear_Combination of AV by A1,A3,VECTSP_6:def 4;
hence Carrier L={} by A2,A3,A4,VECTSP_7:def 1;
end;
hence AR is linearly-independent by RLVECT_3:def 1;
end;
assume A5: AR is linearly-independent;
now let L be Linear_Combination of AV;
reconsider L1=L as Linear_Combination of T by Th1;
A6: Carrier L1=Carrier L by Th2;
Carrier L c=AV by VECTSP_6:def 4;
then reconsider L1 as Linear_Combination of AR by A1,A6,RLVECT_2:def 6;
assume Sum L=0.V;
then 0.T=Sum L by Lm2
.=Sum L1 by Th5;
hence Carrier L={} by A5,A6,RLVECT_3:def 1;
end;
hence thesis by VECTSP_7:def 1;
end;
theorem Th8:
for V be VectSp of K, W be Subspace of V, L be Linear_Combination of V
holds L|the carrier of W is Linear_Combination of W
proof
let V be VectSp of K;
let W be Subspace of V;
let L be Linear_Combination of V;
set cW=the carrier of W;
cW c=[#]V by VECTSP_4:def 2;
then L|cW is Function of cW,the carrier of K by FUNCT_2:32;
then reconsider L1=L|cW as Element of Funcs(cW,the carrier of K)
by FUNCT_2:8;
A1: for v be Element of W st not v in Carrier L/\cW holds L1.v=0.K
proof
let v be Element of W;
reconsider w=v as Element of V by VECTSP_4:10;
assume not v in Carrier L/\cW;
then A2: not v in Carrier L by XBOOLE_0:def 4;
L.w=L1.v by FUNCT_1:49;
hence thesis by A2,VECTSP_6:2;
end;
Carrier L/\cW c=cW by XBOOLE_1:17;
hence thesis by A1,VECTSP_6:def 1;
end;
theorem
for V be VectSp of K, A be linearly-independent Subset of V
for L1,L2 be Linear_Combination of V st
Carrier L1 c= A & Carrier L2 c= A & Sum L1 = Sum L2
holds L1 = L2
proof
let V be VectSp of K;
let A be linearly-independent Subset of V;
let L1,L2 be Linear_Combination of V such that
A1: Carrier L1 c=A & Carrier L2 c=A and
A2: Sum L1=Sum L2;
(L1 is Linear_Combination of A) & L2 is Linear_Combination of A
by A1,VECTSP_6:def 4;
then A3: L1-L2 is Linear_Combination of A by VECTSP_6:42;
Sum(L1-L2)=Sum L1-Sum L2 by VECTSP_6:47
.=0.V by A2,RLVECT_1:15;
then Carrier(L1-L2)={} by A3,VECTSP_7:def 1;
then ZeroLC(V)=L1-L2 by VECTSP_6:def 3
.=L1+-L2 by VECTSP_6:def 11
.=-L2+L1 by VECTSP_6:25;
then L1=--L2 by VECTSP_6:37;
hence thesis;
end;
theorem
for V be RealLinearSpace, W be Subspace of V
for L be Linear_Combination of V
holds L|the carrier of W is Linear_Combination of W
proof
let V be RealLinearSpace;
let W be Subspace of V;
let L be Linear_Combination of V;
set cW=the carrier of W;
cW c=[#]V by RLSUB_1:def 2;
then L|cW is Function of cW,REAL by FUNCT_2:32;
then reconsider L1=L|cW as Element of Funcs(cW,REAL) by FUNCT_2:8;
A1: for v be Element of W st not v in Carrier L/\cW holds L1.v=0
proof
let v be Element of W;
reconsider w=v as Element of V by RLSUB_1:10;
assume not v in Carrier L/\cW;
then A2: not v in Carrier L by XBOOLE_0:def 4;
L.w=L1.v by FUNCT_1:49;
hence thesis by A2,RLVECT_2:19;
end;
Carrier L/\cW c=cW by XBOOLE_1:17;
hence thesis by A1,RLVECT_2:def 3;
end;
theorem
for U be Subspace of n-VectSp_over F_Real,
W be Subspace of TOP-REAL n st [#]U = [#]W
holds
X is Linear_Combination of U
iff
X is Linear_Combination of W
proof
set V=n-VectSp_over F_Real;
set T=TOP-REAL n;
let U be Subspace of V,W be Subspace of T such that
A1: [#]U=[#]W;
hereby assume X is Linear_Combination of U;
then reconsider L=X as Linear_Combination of U;
ex S be finite Subset of U st
for v be Element of U st not v in S holds L.v=0.F_Real
by VECTSP_6:def 1;
hence X is Linear_Combination of W by A1,RLVECT_2:def 3;
end;
assume X is Linear_Combination of W;
then reconsider L=X as Linear_Combination of W;
consider S be finite Subset of W such that
A2: for v be Element of W st not v in S holds L.v=0 by RLVECT_2:def 3;
for v be Element of U st not v in S holds 0.F_Real=L.v by A1,A2;
hence thesis by A1,VECTSP_6:def 1;
end;
theorem
for U be Subspace of n-VectSp_over F_Real, W be Subspace of TOP-REAL n
for LU be Linear_Combination of U, LW be Linear_Combination of W st LU = LW
holds Carrier LU = Carrier LW & Sum LU = Sum LW
proof
set V=n-VectSp_over F_Real;
set T=TOP-REAL n;
let U be Subspace of V,W be Subspace of TOP-REAL n;
let LU be Linear_Combination of U,LW be Linear_Combination of W such that
A1: LU=LW;
reconsider LW9=LW as Function of the carrier of W,REAL;
defpred P[object,object] means
($1 in W & $2=LW.$1) or(not$1 in W & $2=In(0,REAL));
A2: dom LU=[#]U & dom LW=[#]W by FUNCT_2:def 1;
A3: for x be object st x in the carrier of T
ex y be object st y in REAL & P[x,y]
proof
let x be object;
assume x in the carrier of T;
then reconsider x as VECTOR of T;
per cases;
suppose A4: x in W;
then reconsider x as VECTOR of W;
P[x,LW.x] by A4;
hence thesis;
end;
suppose not x in W;
hence thesis;
end;
end;
consider L be Function of the carrier of T,REAL such that
A5: for x be object st x in the carrier of T holds P[x,L.x]
from FUNCT_2:sch 1
(A3);
A6: the carrier of W c=the carrier of T by RLSUB_1:def 2;
then reconsider C=Carrier(LW) as finite Subset of T by XBOOLE_1:1;
A7: L is Element of Funcs(the carrier of T,REAL) by FUNCT_2:8;
now let v be VECTOR of T;
assume not v in C;
then P[v,LW.v] & not v in C & v in the carrier of W or P[v,0]
by STRUCT_0:def 5;
then P[v,LW.v] & LW.v=0 or P[v,0] by RLVECT_2:19;
hence L.v=0 by A5;
end;
then reconsider L as Linear_Combination of T by A7,RLVECT_2:def 3;
reconsider L9=L|the carrier of W as Function of the carrier of W,REAL
by A6,FUNCT_2:32;
now let x be object;
assume A8: x in the carrier of W;
then P[x,L.x] by A6,A5;
hence LW9.x=L9.x by A8,FUNCT_1:49,STRUCT_0:def 5;
end;
then A9: LW=L9 by FUNCT_2:12;
reconsider K=L as Linear_Combination of V by Th1;
now let x be object;
assume that
A10: x in Carrier(L) and
A11: not x in the carrier of W;
consider v being VECTOR of T such that
A12: x=v and
A13: L.v<>0 by A10,RLVECT_5:3;
P[v,0] by A11,A12,STRUCT_0:def 5;
hence contradiction by A5,A13;
end;
then A14: Carrier(L)c=the carrier of W;
then A15: Carrier(L)=Carrier(LW) & Sum(L)=Sum(LW) by A9,RLVECT_5:10;
A16: Carrier(L)=Carrier(K) by Th2;
then Sum K=Sum LU by A1,A2,A14,A9,VECTSP_9:7;
hence thesis by A1,A2,A9,A15,A16,Th5,VECTSP_9:7;
end;
registration
let m,K;
let A be Subset of m-VectSp_over K;
cluster Lin A -> finite-dimensional;
coherence;
end;
Lm4: lines M c=[#]Lin lines M
proof
let x be object;
assume x in lines M;
then x in Lin lines M by VECTSP_7:8;
hence thesis;
end;
begin :: Correspondence Between the Mx2Tran Operator and Decomposition of
:: a Vector in Basis
theorem
the_rank_of M = n implies M is OrdBasis of Lin lines M
proof
A1: lines M c=[#]Lin lines M by Lm4;
then reconsider L=lines M as Subset of Lin lines M;
reconsider B=M as FinSequence of Lin lines M by A1,FINSEQ_1:def 4;
assume that
A2: the_rank_of M=n;
A3: M is one-to-one by A2,MATRIX13:121;
lines M is linearly-independent by A2,MATRIX13:121;
then A4: L is linearly-independent by VECTSP_9:12;
Lin L=Lin lines M by VECTSP_9:17;
then L is Basis of Lin lines M by A4,VECTSP_7:def 3;
then B is OrdBasis of Lin lines M by A3,MATRLIN:def 2;
hence thesis;
end;
theorem Th14:
for V,W be VectSp of K
for T be linear-transformation of V,W
for A be Subset of V for L be Linear_Combination of A st T|A is one-to-one
holds T.(Sum L) = Sum (T@L)
proof
let V,W be VectSp of K;
let T be linear-transformation of V,W;
let A be Subset of V;
let L be Linear_Combination of A;
consider G being FinSequence of V such that
A1: G is one-to-one and
A2: rng G=Carrier L and
A3: Sum L=Sum(L(#)G) by VECTSP_6:def 6;
set H=T*G;
reconsider H as FinSequence of W;
Carrier L c=A by VECTSP_6:def 4;
then A4: (T|A) | (Carrier L)=T| (Carrier L) by RELAT_1:74;
assume A5: T|A is one-to-one;
then A6: T| (Carrier L) is one-to-one by A4,FUNCT_1:52;
A7: rng H=T.:(Carrier L) by A2,RELAT_1:127
.=Carrier(T@L) by A6,RANKNULL:39;
dom T=[#]V by FUNCT_2:def 1;
then H is one-to-one by A5,A4,A1,A2,FUNCT_1:52,RANKNULL:1;
then A8: Sum(T@L)=Sum((T@L)(#)H) by A7,VECTSP_6:def 6;
T*(L(#)G)=(T@L)(#)H by A6,A2,RANKNULL:38;
hence thesis by A3,A8,MATRLIN:16;
end;
Lm5: card lines M=1 implies ex L be Linear_Combination of
lines M st Sum L=(Mx2Tran M).f &
for k st k in Seg n holds L.Line(M,k)=Sum f & M"{Line(M,k)}=dom f
proof
assume that
A1: card lines M=1;
per cases;
suppose A2: n<>0;
deffunc F(set)=0.F_Real;
A3: len M=n by A2,MATRIX13:1;
reconsider Sf=Sum f as Element of F_Real by XREAL_0:def 1;
set Mf=(Mx2Tran M).f;
A4: len Mf=m by CARD_1:def 7;
A5: len f=n by CARD_1:def 7;
set V=m-VectSp_over F_Real;
consider x be object such that
A6: lines M={x} by A1,CARD_2:42;
x in lines M by A6,TARSKI:def 1;
then consider j be object such that
A7: j in dom M and
A8: M.j=x by FUNCT_1:def 3;
reconsider j as Nat by A7;
A9: width M=m by A2,MATRIX13:1;
then reconsider LMj=Line(M,j) as Element of V by MATRIX13:102;
consider L be Function of the carrier of V,the carrier of F_Real such that
A10: L.LMj=1.F_Real and
A11: for z be Element of V st z<>LMj holds L.z=F(z) from FUNCT_2:sch 6;
reconsider L as Element of Funcs(the carrier of V,the carrier of F_Real)
by FUNCT_2:8;
A12: x=Line(M,j) by A7,A8,MATRIX_0:60;
A13: now let z be Vector of V such that
A14: not z in lines M;
z<>LMj by A6,A12,A14,TARSKI:def 1;
hence L.z=0.F_Real by A11;
end;
A15: len(Sf*Line(M,j))=m by A9,CARD_1:def 7;
A16: now len@f=n by CARD_1:def 7;
then reconsider F=@f as Element of n-tuples_on the carrier of F_Real
by FINSEQ_2:92;
let w be Nat;
set Mjw=M*(j,w);
assume A17: 1<=w & w<=m;
then A18: w in dom(Sf*Line(M,j)) by A15,FINSEQ_3:25;
A19: w in Seg m by A17;
then A20: Line(M,j).w=Mjw by A9,MATRIX_0:def 7;
A21: now let z be Nat;
assume A22: 1<=z & z<=n;
then A23: z in Seg n;
then A24: Line(M,z) in lines M by MATRIX13:103;
z in dom M by A3,A22,FINSEQ_3:25;
hence Col(M,w).z=M*(z,w) by MATRIX_0:def 8
.=Line(M,z).w by A9,A19,MATRIX_0:def 7
.=Mjw by A6,A12,A20,A24,TARSKI:def 1
.=(n|->Mjw).z by A23,FINSEQ_2:57;
end;
len Col(M,w)=n & len(n|->Mjw)=n by A3,CARD_1:def 7;
then A25: Col(M,w)=(n|->Mjw) by A21;
thus Mf.w=@f"*"Col(M,w) by A2,A17,MATRTOP1:18
.=Sum mlt(@f,Col(M,w)) by FVSUM_1:def 9
.=Sum(Mjw*F) by A25,FVSUM_1:66
.=Mjw*Sum@f by FVSUM_1:73
.=Mjw*Sf by MATRPROB:36
.=(Sf*Line(M,j)).w by A18,A20,FVSUM_1:50;
end;
reconsider L as Linear_Combination of V by A13,VECTSP_6:def 1;
Carrier L c={LMj}
proof
let x be object such that
A26: x in Carrier L;
L.x<>0.F_Real by A26,VECTSP_6:2;
then x=LMj by A11,A26;
hence thesis by TARSKI:def 1;
end;
then reconsider L as Linear_Combination of lines M by A6,A12,VECTSP_6:def 4;
A27: Sum L=1.F_Real*LMj by A6,A12,A10,VECTSP_6:17
.=LMj;
reconsider SfL=Sf*L as Linear_Combination of lines M by VECTSP_6:31;
take SfL;
Sum SfL=Sf*Sum L by VECTSP_6:45
.=Sf*Line(M,j) by A9,A27,MATRIX13:102;
hence Sum SfL=Mf by A15,A4,A16,FINSEQ_1:14;
let w be Nat such that
A28: w in Seg n;
Line(M,w) in lines M by A28,MATRIX13:103;
then A29: Line(M,w)=LMj by A6,A12,TARSKI:def 1;
thus Sum f = Sf*1
.= Sf*1.F_Real
.=SfL.Line(M,w) by A10,A29,VECTSP_6:def 9;
thus M"{Line(M,w)}=dom M by A6,A12,A29,RELAT_1:134
.=dom f by A3,A5,FINSEQ_3:29;
end;
suppose A30: n=0;
reconsider L=ZeroLC(m-VectSp_over F_Real)
as Linear_Combination of lines M by VECTSP_6:5;
take L;
thus Sum L = 0.(m-VectSp_over F_Real) by VECTSP_6:15
.= 0.(TOP-REAL m) by Lm2
.= (Mx2Tran M).f by A30,MATRTOP1:def 3;
thus thesis by A30;
end;
end;
theorem Th15:
for S be Subset of Seg n st M|S is one-to-one & rng(M|S) = lines M
ex L be Linear_Combination of lines M st
Sum L = (Mx2Tran M).f &
for k st k in S holds L.Line(M,k) = Sum Seq(f|M"{Line(M,k)})
proof
defpred P[Nat] means
for n,m,M,f for S be Subset of Seg n st
(n=0 implies m=0) & M|S is one-to-one
& rng(M|S)=lines M & card lines M=$1
ex L be Linear_Combination of lines M st
Sum L=(Mx2Tran M).f &
for i be Nat st i in S holds L.Line(M,i)=Sum Seq(f|M"{Line(M,i)});
A1: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A2: P[i];
let n,m,M,f;
let S be Subset of Seg n such that
A3: n=0 implies m=0 and
A4: M|S is one-to-one and
A5: rng(M|S)=lines M and
A6: card lines M=i+1;
A7: len M=n by A3,MATRIX13:1;
A8: width M=m by A3,MATRIX13:1;
per cases;
suppose i=0;
then consider L be Linear_Combination of lines M such that
A9: Sum L=(Mx2Tran M).f and
A10: for i be Nat st i in Seg n holds L.Line(M,i)=Sum f &
M"{Line(M,i)}= dom f by A6,Lm5;
take L;
thus Sum L=(Mx2Tran M).f by A9;
let w be Nat such that
A11: w in S;
M"{Line(M,w)}=dom f by A10,A11;
then A12: f|M"{Line(M,w)}=f;
L.Line(M,w)=Sum f by A10,A11;
hence Sum Seq(f|M"{Line(M,w)})=L.Line(M,w) by A12,FINSEQ_3:116;
end;
suppose A13: i>0;
lines M<>{} by A6;
then consider x be object such that
A14: x in lines M by XBOOLE_0:def 1;
reconsider LM={x} as Subset of lines M by A14,ZFMISC_1:31;
set n1=n-' card(M"LM);
reconsider ML1=M-LM as Matrix of n1,m,F_Real by MATRTOP1:14;
A15: LM`=(lines M)\LM by SUBSET_1:def 4;
then A16: LM misses LM` by XBOOLE_1:79;
LM\/LM`=[#]lines M by SUBSET_1:10
.=lines M by SUBSET_1:def 3;
then A17: M"LM\/M"(LM`)=M"(rng M) by RELAT_1:140
.=dom M by RELAT_1:134;
A18: len ML1=len M-card(M"LM) by FINSEQ_3:59;
then A19: n-card(M"LM)=n1 by A7,XREAL_1:49,233;
LM misses LM` by A15,XBOOLE_1:79;
then A20: card(M"LM)+card(M"(LM`))=card dom M by A17,CARD_2:40,FUNCT_1:71
.=n by A7,CARD_1:62;
A21: n1<>0
proof
assume n1=0;
then M"LM`={} by A7,A18,A20,XREAL_1:49,233;
then LM`misses rng M by RELAT_1:138;
then {}=(lines M)\LM by A15,XBOOLE_1:67;
then lines M c=LM by XBOOLE_1:37;
then lines M=LM;
then i+1=1 by A6,CARD_2:42;
hence contradiction by A13;
end;
set n2=n-' card(M"LM`);
reconsider ML2=M-LM` as Matrix of n2,m,F_Real by MATRTOP1:14;
rng ML2=rng M\LM` by FINSEQ_3:65;
then A22: rng ML2=LM`` by SUBSET_1:def 4;
reconsider FR=F_Real as Field;
set Mf=(Mx2Tran M).f;
set V=m-VectSp_over F_Real;
len f=n by CARD_1:def 7;
then A23: dom f=Seg n by FINSEQ_1:def 3;
consider j be object such that
A24: j in dom(M|S) and
A25: (M|S).j=x by A5,A14,FUNCT_1:def 3;
A26: x=M.j by A24,A25,FUNCT_1:47;
A27: j in dom M by A24,RELAT_1:57;
A28: j in S by A24;
reconsider j as Nat by A24;
A29: x=Line(M,j) by A27,A26,MATRIX_0:60;
A30: len ML2=len M-card(M"LM`) by FINSEQ_3:59;
then A31: n-card(M"LM`)=n2 by A7,XREAL_1:49,233;
A32: rng ML1=rng M\LM by FINSEQ_3:65;
then A33: rng ML1=LM` by SUBSET_1:def 4;
reconsider LMj=Line(M,j) as Element of V by A8,MATRIX13:102;
A34: card rng ML1=card(rng M)-card LM by A32,CARD_2:44
.=i+1-1 by A6,CARD_2:42;
LM``=LM;
then consider P be Permutation of dom M such that
A35: (M-LM)^(M-LM`)=M*P by FINSEQ_3:115;
dom M=Seg n by A7,FINSEQ_1:def 3;
then reconsider p=P as Permutation of Seg n;
A36: (M|S)*P=(M|S)*(p|dom p)
.=(M*p) | (dom p/\(p"S)) by FUNCT_1:100
.=(M*p) | (p"S) by RELAT_1:132,XBOOLE_1:28;
reconsider pp=P as one-to-one Function;
len(M*p)=n by MATRIX_0:def 2;
then A37: dom(M*p)=Seg n by FINSEQ_1:def 3;
set ppj=(pp").j;
A38: rng p=Seg n by FUNCT_2:def 3;
then A39: p"S=(pp").:S & dom(pp")=Seg n by FUNCT_1:33,85;
then A40: ppj in p"S by A28,FUNCT_1:def 6;
A41: p.ppj=j by A28,A38,FUNCT_1:35;
A42: not ppj in dom ML1
proof
assume A43: ppj in dom ML1;
(M*P).ppj=M.j by A40,A41,A37,FUNCT_1:12;
then (M*P).ppj=LMj by A27,MATRIX_0:60;
then ML1.ppj=LMj by A35,A43,FINSEQ_1:def 7;
then A44: ML1.ppj in LM by A29,TARSKI:def 1;
ML1.ppj in LM` by A33,A43,FUNCT_1:def 3;
hence contradiction by A16,A44,XBOOLE_0:3;
end;
set pSj=(p"S)\{ppj};
dom M=Seg n by A7,FINSEQ_1:def 3;
then A45: dom(M|S)=S by RELAT_1:62;
A46: pSj c=dom ML1
proof
let y be object;
assume A47: y in pSj;
then reconsider Y=y as Nat;
A48: (M*p).y=M.(p.y) by A37,A47,FUNCT_1:12;
not y in {ppj} by A47,XBOOLE_0:def 5;
then A49: y<>ppj by TARSKI:def 1;
A50: ppj in dom P by A40,FUNCT_1:def 7;
A51: y in p"S by A47,XBOOLE_0:def 5;
then A52: p.y in dom(M|S) by A45,FUNCT_1:def 7;
y in dom P by A51,FUNCT_1:def 7;
then p.y<>j by A41,A49,A50,FUNCT_1:def 4;
then (M|S).(p.y)<>(M|S).j by A4,A24,A52,FUNCT_1:def 4;
then (M*p).y<>LMj by A25,A29,A48,A52,FUNCT_1:47;
then A53: not(M*p).y in LM by A29,TARSKI:def 1;
assume not y in dom ML1;
then consider w be Nat such that
A54: w in dom ML2 and
A55: Y=len ML1+w by A35,A37,A47,FINSEQ_1:25;
(M*p).Y=ML2.w by A35,A54,A55,FINSEQ_1:def 7;
hence contradiction by A22,A53,A54,FUNCT_1:def 3;
end;
then (M*p) |pSj=((M*p) | (p"S)) |pSj & (M*p) |pSj=ML1|pSj
by A35,FINSEQ_6:11,RELAT_1:74,XBOOLE_1:36;
then A56: ML1|pSj is one-to-one by A4,A36,FUNCT_1:52;
dom p=Seg n & p.ppj=j by A28,A38,FUNCT_1:35,FUNCT_2:52;
then A57: ppj in dom((M|S)*p) by A24,A40,FUNCT_1:11;
then ((M|S)*p).ppj=LMj by A25,A29,A41,FUNCT_1:12;
then A58: LM=Im(((M|S)*p),ppj) by A29,A57,FUNCT_1:59
.=((M*p) | (p"S)).:{ppj} by A36,RELAT_1:def 16;
rng M = rng((M*p) | (p"S)) by A5,A36,A38,A45,RELAT_1:28
.=(M*p).:(p"S) by RELAT_1:115
.=((M*p) | (p"S)).:(p"S) by RELAT_1:129;
then A59: rng ML1=((M*p) | (p"S)).:pSj by A4,A36,A32,A58,FUNCT_1:64
.=rng((M*p) | (p"S) |pSj) by RELAT_1:115
.=rng((M*p) |pSj) by RELAT_1:74,XBOOLE_1:36
.=rng(ML1|pSj) by A35,A46,FINSEQ_6:11;
reconsider fp=f*p as n-element FinSequence of REAL by MATRTOP1:21;
A60: n1+n2=len(ML1^ML2) by MATRIX_0:def 2
.=len(M*p) by A35
.=n by MATRIX_0:def 2;
len fp=n by CARD_1:def 7;
then consider fp1,fp2 be FinSequence of REAL such that
A61: len fp1=n1 and
A62: len fp2=n2 and
A63: fp=fp1^fp2 by A60,FINSEQ_2:23;
A64: fp2 is n2-element by A62,CARD_1:def 7;
then A65: len((Mx2Tran ML2).fp2)=m by CARD_1:def 7;
card LM=1 by CARD_2:42;
then consider L2 be Linear_Combination of lines ML2 such that
A66: Sum L2=(Mx2Tran ML2).fp2 and
A67: for i be Nat st i in Seg n2 holds L2.Line(ML2,i)=Sum fp2 &
ML2"{Line(ML2,i)}=dom fp2 by A64,A22,Lm5;
A68: fp1 is n1-element by A61,CARD_1:def 7;
then len((Mx2Tran ML1).fp1)=m by CARD_1:def 7;
then reconsider Mf1=@((Mx2Tran ML1).fp1),Mf2=@((Mx2Tran ML2).fp2)
as Element of m-tuples_on the carrier of F_Real by A65,FINSEQ_2:92;
A69: Carrier L2 c=lines ML2 by VECTSP_6:def 4;
len ML1=n1 by A7,A18,XREAL_1:49,233;
then pSj is Subset of Seg n1 by A46,FINSEQ_1:def 3;
then consider L1 be Linear_Combination of lines ML1 such that
A70: Sum L1=(Mx2Tran ML1).fp1 and
A71: for i be Nat st i in pSj holds
L1.Line(ML1,i)=Sum Seq(fp1|ML1"{Line(ML1,i)}) by A2,A68,A21,A56,A59,A34;
A72: Carrier L1 c=lines ML1 by VECTSP_6:def 4;
rng ML1\/rng ML2=[#]lines M by A22,A33,SUBSET_1:10
.=lines M by SUBSET_1:def 3;
then (L1 is Linear_Combination of lines M) & L2 is Linear_Combination of
lines M by VECTSP_6:4,XBOOLE_1:7;
then reconsider L12=L1+L2 as Linear_Combination of lines M by VECTSP_6:24;
take L12;
thus(Mx2Tran M).f=(Mx2Tran(ML1^ML2)).(fp1^fp2)
by A35,A60,A63,MATRTOP1:21
.=(Mx2Tran ML1).fp1+(Mx2Tran ML2).fp2 by A68,A64,MATRTOP1:36
.=Mf1+Mf2 by MATRTOP1:1
.=Sum L1+Sum L2 by A70,A66,MATRIX13:102
.=Sum L12 by VECTSP_6:44;
let w be Nat such that
A73: w in S;
Line(M,w) in lines M by A73,MATRIX13:103;
then reconsider LMw=Line(M,w) as Element of V;
p"(M"{LMw})=(M*p)"{LMw} by RELAT_1:146;
then A74: Sum Seq(f|M"{LMw})=Sum Seq(fp| (M*p)"{LMw}) by A23,MATRTOP1:10
.=Sum(Seq(fp1|ML1"{LMw})^Seq(fp2|ML2"{LMw}))
by A7,A35,A61,A62,A63,A18,A30,A19,A31,MATRTOP1:13
.=Sum Seq(fp1|ML1"{LMw})+Sum Seq(fp2|ML2"{LMw}) by RVSUM_1:75;
set ppw=(pp").w;
A75: ppw in p"S by A39,A73,FUNCT_1:def 6;
p.ppw=w by A38,A73,FUNCT_1:35;
then A76: (M*P).ppw=M.w by A37,A75,FUNCT_1:12;
reconsider ppw as Nat by A75;
A77: M.w=LMw by A73,MATRIX_0:52;
reconsider L1w=L1.LMw,L2w=L2.LMw as Element of FR;
A78: L12.LMw=L1w+L2w by VECTSP_6:22;
per cases by A35,A37,A75,FINSEQ_1:25;
suppose A79: ppw in dom ML1;
then A80: ML1.ppw=LMw by A35,A76,A77,FINSEQ_1:def 7;
then A81: LMw in rng ML1 by A79,FUNCT_1:def 3;
then not LMw in Carrier L2 by A22,A33,A69,A16,XBOOLE_0:3;
then A82: L2.LMw=0.F_Real by VECTSP_6:2;
not LMw in rng ML2 by A22,A33,A16,A81,XBOOLE_0:3;
then {LMw}misses rng ML2 by ZFMISC_1:50;
then ML2"{LMw}={} by RELAT_1:138;
then A83: Sum Seq(fp2|ML2"{LMw})=0 by RVSUM_1:72;
Line(ML1,ppw)=ML1.ppw & ppw in pSj
by A75,A42,A79,MATRIX_0:60,ZFMISC_1:56;
then L1.LMw=Sum Seq(fp1|ML1"{LMw}) by A71,A80;
hence thesis by A74,A78,A82,A83,RLVECT_1:def 4;
end;
suppose ex z be Nat st z in dom ML2 & ppw=len ML1+z;
then consider z be Nat such that
A84: z in dom ML2 and
A85: ppw=len ML1+z;
A86: ML2.z=LMw by A35,A76,A77,A84,A85,FINSEQ_1:def 7;
then A87: LMw in rng ML2 by A84,FUNCT_1:def 3;
then not LMw in Carrier L1 by A22,A33,A72,A16,XBOOLE_0:3;
then A88: L1.LMw=0.F_Real by VECTSP_6:2;
not LMw in LM` by A22,A16,A87,XBOOLE_0:3;
then {LMw}misses rng ML1 by A33,ZFMISC_1:50;
then ML1"{LMw}={} by RELAT_1:138;
then A89: Seq(fp1|ML1"{LMw})=<*>REAL;
L1w+L2w=L2w+L1w by RLVECT_1:def 2;
then A90: L12.LMw=L2.LMw by A78,A88,RLVECT_1:def 4;
A91: dom ML2=Seg n2 by A7,A30,A31,FINSEQ_1:def 3;
A92: ML2.z=Line(ML2,z) by A84,MATRIX_0:60;
then ML2"{LMw}=dom fp2 by A67,A84,A86,A91;
then A93: fp2|ML2"{LMw}=fp2;
L2.LMw=Sum fp2 by A67,A84,A86,A92,A91;
hence thesis by A74,A90,A89,A93,FINSEQ_3:116,RVSUM_1:72;
end;
end;
end;
A94: P[0]
proof
let n,m,M,f;
let S be Subset of Seg n such that
A95: n=0 implies m=0 and
M|S is one-to-one and
rng(M|S)=lines M and
A96: card lines M=0;
reconsider L=ZeroLC(m-VectSp_over F_Real)
as Linear_Combination of lines M by VECTSP_6:5;
take L;
A97: Sum L=0.(m-VectSp_over F_Real) by VECTSP_6:15
.=0.(TOP-REAL m) by Lm2;
A98: len M=n & M={} by A95,A96,MATRIX13:1;
thus Sum L=(Mx2Tran M).f by A95,A98,A97;
let i be Nat;
thus thesis by A98;
end;
for i be Nat holds P[i] from NAT_1:sch 2(A94,A1);
then A99: P[card lines M];
per cases;
suppose n<>0; hence thesis by A99; end;
suppose A100: n=0;
let S be Subset of Seg n such that
M|S is one-to-one & rng(M|S) = lines M;
reconsider L=ZeroLC(m-VectSp_over F_Real)
as Linear_Combination of lines M by VECTSP_6:5;
take L;
thus Sum L = 0.(m-VectSp_over F_Real) by VECTSP_6:15
.= 0.(TOP-REAL m) by Lm2
.= (Mx2Tran M).f by A100,MATRTOP1:def 3;
thus thesis by A100;
end;
end;
theorem Th16:
M is without_repeated_line implies
ex L be Linear_Combination of lines M st
Sum L=(Mx2Tran M).f &
for k st k in dom f holds L.Line(M,k)=f.k
proof
assume that
A1: M is without_repeated_line;
A2: len M=n by MATRIX_0:def 2;
then dom M c=Seg n by FINSEQ_1:def 3;
then reconsider D=dom M as Subset of Seg n;
len f=n by CARD_1:def 7;
then A3: dom f=dom M by A2,FINSEQ_3:29;
M|dom M=M;
then consider L be Linear_Combination of lines M such that
A4: Sum L=(Mx2Tran M).f and
A5: for i be Nat st i in D holds L.Line(M,i)=Sum Seq(f|M"{Line(M,i)})
by A1,Th15;
take L;
thus Sum L=(Mx2Tran M).f by A4;
let i be Nat such that
A6: i in dom f;
i>=1 by A6,FINSEQ_3:25;
then A7: Sgm{i}=<*i*> by FINSEQ_3:44;
set LM=Line(M,i);
A8: LM in {LM} by TARSKI:def 1;
dom M=Seg n by A2,FINSEQ_1:def 3;
then LM in lines M by A3,A6,MATRIX13:103;
then consider x be object such that
A9: M"{LM}={x} by A1,FUNCT_1:74;
A10: dom(f|{i})=dom f/\{i} by RELAT_1:61;
{i}c=dom f by A6,ZFMISC_1:31;
then A11: dom(f|{i})={i} by A10,XBOOLE_1:28;
then i in dom(f|{i}) by TARSKI:def 1;
then A12: (f|{i}).i=f.i by FUNCT_1:47;
rng<*i*>={i} by FINSEQ_1:38;
then A13: <*i*> is FinSequence of{i} by FINSEQ_1:def 4;
rng(f|{i})<>{} & f|{i} is Function of{i},rng(f|{i})
by A11,FUNCT_2:1,RELAT_1:42;
then Seq(f|{i})=<*f.i*> by A11,A7,A13,A12,FINSEQ_2:35;
then A14: Sum Seq(f|{i})=f.i by RVSUM_1:73;
M.i=LM by A3,A6,MATRIX_0:60;
then i in M"{LM} by A3,A6,A8,FUNCT_1:def 7;
then f|M"{LM}=f|{i} by A9,TARSKI:def 1;
hence thesis by A5,A3,A6,A14;
end;
theorem
for B be OrdBasis of Lin lines M st B = M
for Mf be Element of Lin lines M st Mf = (Mx2Tran M).f holds Mf|--B = f
proof
set LM=lines M;
let B be OrdBasis of Lin LM such that
A1: B=M;
A2: B is one-to-one by MATRLIN:def 2;
let Mf be Element of Lin LM such that
A3: Mf=(Mx2Tran M).f;
consider L be Linear_Combination of LM such that
A4: Sum L=Mf and
A5: for i be Nat st i in dom f holds L.Line(M,i)=f.i by A1,A3,A2,Th16;
reconsider L1=L|the carrier of Lin LM as Linear_Combination of Lin LM by Th8;
A6: len M=n by MATRIX_0:def 2;
A7: len f=n by CARD_1:def 7;
A8: LM c=[#]Lin LM by Lm4;
A9: now let k;
assume A10: 1<=k & k<=n;
then k in Seg n;
then A11: M.k=Line(M,k) by MATRIX_0:52;
A12: k in dom M by A6,A10,FINSEQ_3:25;
then A13: B/.k=M.k by A1,PARTFUN1:def 6;
M.k in LM by A12,FUNCT_1:def 3;
then A14: L.(M.k)=L1.(M.k) by A8,FUNCT_1:49;
A15: k in dom f by A7,A10,FINSEQ_3:25;
then f.k=@f/.k by PARTFUN1:def 6;
hence @f/.k=L1.(B/.k) by A5,A15,A13,A11,A14;
end;
A16: Carrier L c=LM by VECTSP_6:def 4;
then Carrier L c=[#]Lin LM by A8;
then Carrier L=Carrier L1 & Sum L1=Sum L by VECTSP_9:7;
hence thesis by A1,A4,A6,A7,A16,A9,MATRLIN:def 7;
end;
theorem Th18:
rng(Mx2Tran M) = [#]Lin lines M
proof
consider X be set such that
A1: X c=dom M and
A2: lines M=rng(M|X) and
A3: M|X is one-to-one by MATRTOP1:6;
set V=m-VectSp_over F_Real;
set TM=Mx2Tran M;
A4: len M=n by MATRIX_0:def 2;
then reconsider X as Subset of Seg n by A1,FINSEQ_1:def 3;
hereby let y be object;
assume y in rng TM;
then consider x be object such that
A5: x in dom TM and
A6: TM.x=y by FUNCT_1:def 3;
reconsider x as Element of TOP-REAL n by A5;
consider L be Linear_Combination of lines M such that
A7: Sum L=y and
for i be Nat st i in X holds L.Line(M,i)=Sum Seq(x|M"{Line(M,i)})
by A2,A3,A6,Th15;
Sum L in Lin lines M by VECTSP_7:7;
hence y in [#]Lin lines M by A7;
end;
let y be object;
assume y in [#]Lin lines M;
then y in Lin lines M;
then consider L be Linear_Combination of lines M such that
A8: y=Sum L by VECTSP_7:7;
defpred P[set,object] means
($1 in X implies $2=L.(M.$1)) & (not$1 in X implies $2=0);
A9: for i be Nat st i in Seg n ex x be object st P[i,x]
proof
let i be Nat such that
i in Seg n;
i in X or not i in X;
hence thesis;
end;
consider f be FinSequence such that
A10: dom f=Seg n & for j be Nat st j in Seg n holds P[j,f.j]
from FINSEQ_1:sch 1(A9);
A11: dom M=Seg n by A4,FINSEQ_1:def 3;
rng f c=REAL
proof
let z be object;
assume z in rng f;
then consider x be object such that
A12: x in dom f and
A13: f.x=z by FUNCT_1:def 3;
reconsider x as Nat by A12;
A14: P[x,f.x] by A10,A12;
M.x=Line(M,x) by A11,A10,A12,MATRIX_0:60;
then M.x in lines M by A10,A12,MATRIX13:103;
then reconsider Mx=M.x as Element of V;
per cases;
suppose not x in X;
then f.x=In(0,REAL) by A10,A12;
hence thesis by A13;
end;
suppose x in X;
thus thesis by A13,A14,XREAL_0:def 1;
end;
end;
then reconsider f as FinSequence of REAL by FINSEQ_1:def 4;
len f=n by A4,A10,FINSEQ_1:def 3;
then A15: f is n-element by CARD_1:def 7;
then consider K be Linear_Combination of lines M such that
A16: Sum K=TM.f and
A17: for i be Nat st i in X holds K.Line(M,i)=Sum Seq(f|M"{Line(M,i)})
by A2,A3,Th15;
now let v be Element of V;
per cases;
suppose v in lines M;
then consider i be object such that
A18: i in dom(M|X) and
A19: (M|X).i=v by A2,FUNCT_1:def 3;
A20: M.i=v by A18,A19,FUNCT_1:47;
set D=dom(f|M"{v});
Seq(f|M"{v})=@@Seq(f|M"{v});
then reconsider F=Seq(f|M"{v}) as FinSequence of REAL;
A21: rng Sgm D=D by FINSEQ_1:50;
then A22: dom F=dom Sgm D by RELAT_1:27;
A23: i in dom M by A18,RELAT_1:57;
A24: i in X by A18;
reconsider i as Nat by A18;
M.i=Line(M,i) by A23,MATRIX_0:60;
then A25: K.v=Sum Seq(f|M"{v}) by A17,A24,A20;
v in {v} by TARSKI:def 1;
then i in M"{v} by A23,A20,FUNCT_1:def 7;
then i in D by A10,A24,RELAT_1:57;
then consider j be object such that
A26: j in dom Sgm D and
A27: (Sgm D).j=i by A21,FUNCT_1:def 3;
reconsider j as Element of NAT by A26;
F.j=(f|M"{v}).i & i in D by A22,A26,A27,FUNCT_1:11,12;
then A28: F.j=f.i by FUNCT_1:47;
A29: Sgm D is one-to-one by FINSEQ_3:92;
now let w be Nat;
assume that
A30: w in dom F and
A31: w<>j;
A32: (Sgm D).w in D by A21,A22,A30,FUNCT_1:def 3;
then (Sgm D).w in M"{v} by RELAT_1:57;
then M.((Sgm D).w) in {v} by FUNCT_1:def 7;
then A33: M.((Sgm D).w)=v by TARSKI:def 1;
A34: not(Sgm D).w in X
proof
assume(Sgm D).w in X;
then A35: (Sgm D).w in dom(M|X) by A11,RELAT_1:57;
then v=(M|X).((Sgm D).w) by A33,FUNCT_1:47;
then i=(Sgm D).w by A3,A18,A19,A35,FUNCT_1:def 4;
hence contradiction by A22,A29,A26,A27,A30,A31,FUNCT_1:def 4;
end;
F.w=(f|M"{v}).((Sgm D).w) by A30,FUNCT_1:12;
then A36: F.w=f.((Sgm D).w) by A32,FUNCT_1:47;
(Sgm D).w in dom f by A32,RELAT_1:57;
hence F.w=0 by A10,A36,A34;
end;
then A37: F has_onlyone_value_in j by A22,A26,ENTROPY1:def 2;
f.i=L.v by A10,A24,A20;
hence L.v=K.v by A25,A28,A37,ENTROPY1:13;
end;
suppose A38: not v in lines M;
Carrier L c=lines M by VECTSP_6:def 4;
then not v in Carrier L by A38;
then A39: L.v=0.F_Real by VECTSP_6:2;
Carrier K c=lines M by VECTSP_6:def 4;
then not v in Carrier K by A38;
hence L.v=K.v by A39,VECTSP_6:2;
end;
end;
then A40: Sum K=Sum L by VECTSP_6:def 7;
dom TM=[#](TOP-REAL n) & f is Point of TOP-REAL n by A15,Lm3,FUNCT_2:def 1;
hence thesis by A8,A16,A40,FUNCT_1:def 3;
end;
theorem Th19:
for F be one-to-one FinSequence of TOP-REAL n st
rng F is linearly-independent
ex M be Matrix of n,F_Real st M is invertible & M|len F = F
proof
let F be one-to-one FinSequence of TOP-REAL n such that
A1: rng F is linearly-independent;
reconsider f=F as FinSequence of n-VectSp_over F_Real by Lm1;
set M=FinS2MX f;
lines M is linearly-independent by A1,Th7;
then A2: the_rank_of M=len F by MATRIX13:121;
then consider A be Matrix of n-' len F,n,F_Real such that
A3: the_rank_of(M^A)=n by MATRTOP1:16;
len F<=width M by A2,MATRIX13:74;
then len F<=n by MATRIX_0:23;
then n-len F=n-' len F by XREAL_1:233;
then reconsider MA=M^A as Matrix of n,F_Real;
take MA;
Det MA<>0.F_Real by A3,MATRIX13:83;
then Det MA is non zero;
then Det MA is unital;
hence MA is invertible by LAPLACE:34;
thus F=MA|dom F by FINSEQ_1:21
.=MA|len F by FINSEQ_1:def 3;
end;
theorem Th20:
for B be OrdBasis of n-VectSp_over F_Real st B = MX2FinS 1.(F_Real,n) holds
f in Lin rng(B|k)
iff
f = (f|k)^((n-' k) |->0)
proof
set V=n-VectSp_over F_Real;
set nk0=(n-' k) |->0;
let B be OrdBasis of n-VectSp_over F_Real such that
A1: B=MX2FinS 1.(F_Real,n);
A2: len B=n by A1,MATRIX_0:def 2;
A3: f is Point of TOP-REAL n by Lm3;
then A4: f is Point of V by Lm1;
A5: rng B is Basis of V by MATRLIN:def 2;
then A6: rng B is linearly-independent by VECTSP_7:def 3;
Lin rng B=the ModuleStr of V by A5,VECTSP_7:def 3;
then A7: f in Lin rng B by A4;
A8: B is one-to-one by MATRLIN:def 2;
reconsider F=f as Point of V by A3,Lm1;
A9: len f=n by CARD_1:def 7;
per cases;
suppose A10: k>=n;
then n-k<=0 by XREAL_1:47;
then n-' k=0 by XREAL_0:def 2;
then A11: nk0={};
f|k=f by A9,A10,FINSEQ_1:58;
hence thesis by A2,A7,A10,A11,FINSEQ_1:34,58;
end;
suppose A12: k<n;
then A13: len(f|k)=k by A9,FINSEQ_1:59;
A14: len nk0=n-' k by CARD_1:def 7;
consider KL be Linear_Combination of V such that
A15: F=Sum(KL) and
A16: Carrier KL c=rng B and
A17: for k st 1<=k & k<=len(F|--B) holds(F|--B)/.k=KL.(B/.k)
by MATRLIN:def 7;
reconsider KL as Linear_Combination of rng B by A16,VECTSP_6:def 4;
A18: F|--B=F by A1,A2,MATRLIN2:46;
n-' k=n-k by A12,XREAL_1:233;
then len((f|k)^nk0)=k+(n-k) by A13,A14,FINSEQ_1:22;
then A19: dom((f|k)^nk0)=dom f by A9,FINSEQ_3:29;
hereby assume f in Lin rng(B|k);
then consider L be Linear_Combination of rng(B|k) such that
A20: Sum L=f by VECTSP_7:7;
reconsider L1=L as Linear_Combination of rng B by RELAT_1:70,VECTSP_6:4;
A21: KL-L1 is Linear_Combination of rng B by VECTSP_6:42;
Sum(KL-L1)=Sum KL-Sum L1 by VECTSP_6:47
.=0.V by A15,A20,VECTSP_1:19;
then Carrier(KL-L1)={} by A6,A21,VECTSP_7:def 1;
then A22: ZeroLC(V)=KL-L1 by VECTSP_6:def 3
.=KL+-L1 by VECTSP_6:def 11
.=-L1+KL by VECTSP_6:25;
reconsider M1=-1.F_Real as Element of F_Real;
A23: Carrier L c=rng(B|k) by VECTSP_6:def 4;
L1=--L1;
then A24: KL=L1 by A22,VECTSP_6:37;
now let i be Nat;
assume A25: i in dom f;
per cases by A13,A19,A25,FINSEQ_1:25;
suppose A26: i in dom(f|k);
then (f|k).i=f.i by FUNCT_1:47;
hence ((f|k)^nk0).i=f.i by A26,FINSEQ_1:def 7;
end;
suppose A27: ex j be Nat st j in dom nk0 & i=k+j;
A28: i in dom B by A9,A2,A25,FINSEQ_3:29;
then A29: B/.i=B.i by PARTFUN1:def 6;
consider j be Nat such that
A30: j in dom nk0 and
A31: i=k+j by A27;
A32: 1<=j by A30,FINSEQ_3:25;
not B.i in rng(B|k)
proof
assume B.i in rng(B|k);
then consider x be object such that
A33: x in dom(B|k) and
A34: (B|k).x=B.i by FUNCT_1:def 3;
B.x=B.i & x in dom B by A33,A34,FUNCT_1:47,RELAT_1:57;
then A35: i=x by A8,A28,FUNCT_1:def 4;
x in Seg k by A33,RELAT_1:57;
then A36: i<=k by A35,FINSEQ_1:1;
i>=k+1 by A31,A32,XREAL_1:6;
hence contradiction by A36,NAT_1:13;
end;
then A37: not B.i in Carrier L by A23;
1<=i & i<=n by A9,A25,FINSEQ_3:25;
then A38: (F|--B)/.i=KL.(B/.i) by A9,A18,A17;
f.i=(F|--B)/.i by A18,A25,PARTFUN1:def 6;
hence f.i=0.F_Real by A24,A38,A29,A37,VECTSP_6:2
.=nk0.j
.=((f|k)^nk0).i by A13,A30,A31,FINSEQ_1:def 7;
end;
end;
hence (f|k)^((n-' k) |->0)=f by A19,FINSEQ_1:13;
end;
assume A39: (f|k)^nk0=f;
Carrier KL c=rng(B|k)
proof
let x be object;
assume A40: x in Carrier KL;
Carrier KL c=rng B by VECTSP_6:def 4;
then consider i be object such that
A41: i in dom B and
A42: B.i=x by A40,FUNCT_1:def 3;
reconsider i as Element of NAT by A41;
A43: B/.i=B.i by A41,PARTFUN1:def 6;
A44: dom B=dom f by A9,A2,FINSEQ_3:29;
assume A45: not x in rng(B|k);
not i in Seg k
proof
assume i in Seg k;
then A46: i in dom(B|k) by A41,RELAT_1:57;
then (B|k).i=B.i by FUNCT_1:47;
hence contradiction by A42,A45,A46,FUNCT_1:def 3;
end;
then not i in dom(f|k) by A13,FINSEQ_1:def 3;
then consider j be Nat such that
A47: j in dom nk0 and
A48: i=k+j by A13,A19,A41,A44,FINSEQ_1:25;
A49: nk0.j=0;
A50: 1<=i & i<=n by A2,A41,FINSEQ_3:25;
(F|--B)/.i=(F|--B).i by A18,A41,A44,PARTFUN1:def 6;
then KL.(B/.i)=f.i by A9,A18,A17,A50
.=0.F_Real by A13,A39,A47,A48,A49,FINSEQ_1:def 7;
hence contradiction by A40,A42,A43,VECTSP_6:2;
end;
then KL is Linear_Combination of rng(B|k) by VECTSP_6:def 4;
hence thesis by A15,VECTSP_7:7;
end;
end;
theorem Th21:
for F be one-to-one FinSequence of TOP-REAL n st
rng F is linearly-independent
for B be OrdBasis of n-VectSp_over F_Real st B = MX2FinS 1.(F_Real,n)
for M be Matrix of n,F_Real st M is invertible & M|len F = F
holds (Mx2Tran M).:[#]Lin rng(B|len F) = [#]Lin rng F
proof
let F be one-to-one FinSequence of TOP-REAL n such that
A1: rng F is linearly-independent;
reconsider f=F as FinSequence of n-VectSp_over F_Real by Lm1;
set MF=FinS2MX f;
set n1=n-' len F;
set L=len F;
lines MF is linearly-independent by A1,Th7;
then the_rank_of MF=len F by MATRIX13:121;
then L<=width MF by MATRIX13:74;
then A2: L<=n by MATRIX_0:23;
then A3: n-L=n1 by XREAL_1:233;
set V=n-VectSp_over F_Real;
let B be OrdBasis of n-VectSp_over F_Real such that
A4: B=MX2FinS 1.(F_Real,n);
let M be Matrix of n,F_Real such that
M is invertible and
A5: M|len F=F;
consider q being FinSequence such that
A6: M=F^q by A5,FINSEQ_1:80;
M=MX2FinS M;
then reconsider q as FinSequence of n-VectSp_over F_Real by A6,FINSEQ_1:36;
A7: len M=len F+len q by A6,FINSEQ_1:22;
set Mq=FinS2MX q;
set MT=Mx2Tran M;
A8: len M=n by MATRIX_0:def 2;
A9: dom MT=[#]TOP-REAL n by FUNCT_2:52;
A10: dom Mx2Tran MF=[#]TOP-REAL L by FUNCT_2:def 1;
A11: the carrier of TOP-REAL n=REAL n by EUCLID:22
.=n-tuples_on REAL;
A12: rng(Mx2Tran MF)=[#]Lin lines MF by Th18
.=[#]Lin rng F by Th6;
A13: (n|->0)=0*n
.=0.TOP-REAL n by EUCLID:70;
A14: (n1|->0)=0*n1
.=0.TOP-REAL n1 by EUCLID:70;
then A15: (Mx2Tran Mq).(n1|->0)=0.TOP-REAL n by A3,A8,A7,MATRTOP1:29;
thus MT.:[#]Lin rng(B|L)c=[#]Lin rng F
proof
let y be object;
assume y in MT.:[#]Lin rng(B|L);
then consider x be object such that
A16: x in dom MT and
A17: x in [#]Lin rng(B|L) and
A18: MT.x=y by FUNCT_1:def 6;
reconsider x as Element of TOP-REAL n by A16;
len x=n by CARD_1:def 7;
then len(x|L)=L by A2,FINSEQ_1:59;
then A19: x|L is L-element by CARD_1:def 7;
then A20: x|L is Element of TOP-REAL L by Lm3;
A21: (Mx2Tran MF).(x|L) is Element of n-tuples_on REAL by A11,A19,Lm3;
x in Lin rng(B|L) by A17;
then x=(x|L)^((n-' L) |->0) by A4,Th20;
then y=(Mx2Tran MF).(x|L)+(Mx2Tran Mq).(n1|->0)
by A3,A8,A6,A7,A18,A19,MATRTOP1:36
.=(Mx2Tran MF).(x|L) by A13,A15,A21,RVSUM_1:16;
hence thesis by A12,A10,A20,FUNCT_1:def 3;
end;
let y be object;
assume y in [#]Lin rng F;
then consider x be object such that
A22: x in dom(Mx2Tran MF) and
A23: (Mx2Tran MF).x=y by A12,FUNCT_1:def 3;
reconsider x as Element of TOP-REAL L by A22;
(Mx2Tran MF).x is Element of TOP-REAL n by Lm3;
then A24: y=(Mx2Tran MF).x+0.TOP-REAL n by A11,A13,A23,RVSUM_1:16
.=(Mx2Tran MF).x+(Mx2Tran Mq).(n1|->0) by A3,A8,A7,A14,MATRTOP1:29
.=MT.(x^(n1|->0)) by A6,A3,A8,A7,MATRTOP1:36;
set xx=(x^(n1|->0));
len x=L by CARD_1:def 7;
then dom x=Seg L by FINSEQ_1:def 3;
then xx=(xx|L)^(n1|->0) by FINSEQ_1:21;
then xx in Lin rng(B|L) by A4,A3,Th20;
then A25: xx in [#]Lin rng(B|L);
xx is Element of TOP-REAL n by A3,Lm3;
hence thesis by A9,A24,A25,FUNCT_1:def 6;
end;
theorem
for A,B be linearly-independent Subset of TOP-REAL n st card A = card B
ex M be Matrix of n,F_Real st
M is invertible & (Mx2Tran M).:[#]Lin A = [#]Lin B
proof
set TRn=TOP-REAL n;
let A,B be linearly-independent Subset of TRn such that
A1: card A=card B;
reconsider BB=MX2FinS 1.(F_Real,n) as OrdBasis of n-VectSp_over F_Real
by MATRLIN2:45;
set V=n-VectSp_over F_Real;
A is linearly-independent Subset of V by Lm1,Th7;
then A is finite by VECTSP_9:21;
then consider fA be FinSequence such that
A2: rng fA=A and
A3: fA is one-to-one by FINSEQ_4:58;
A4: len fA=card A by A2,A3,PRE_POLY:19;
B is linearly-independent Subset of V by Lm1,Th7;
then B is finite by VECTSP_9:21;
then consider fB be FinSequence such that
A5: rng fB=B and
A6: fB is one-to-one by FINSEQ_4:58;
A7: len fB=card B by A5,A6,PRE_POLY:19;
reconsider fA,fB as FinSequence of TRn by A2,A5,FINSEQ_1:def 4;
consider MA be Matrix of n,F_Real such that
A8: MA is invertible and
A9: MA|len fA=fA by A2,A3,Th19;
A10: [#]Lin rng(BB|len fA)c=[#]V by VECTSP_4:def 2;
set Ma=Mx2Tran MA;
Det MA is unital by A8,LAPLACE:34;
then A11: Det MA<>0.F_Real by LAPLACE:42,43;
then A12: Ma is one-to-one by MATRTOP1:40;
then A13: rng(Ma")=dom Ma by FUNCT_1:33;
A14: [#]TOP-REAL n=[#]V & dom Ma=[#]TRn by Lm1,FUNCT_2:52;
(Ma")"[#]Lin rng(BB|len fA)=Ma.:[#]Lin rng(BB|len fA) by A12,FUNCT_1:84
.=[#]Lin A by A2,A3,A8,A9,Th21;
then A15: (Ma").:[#]Lin A=[#]Lin rng(BB|len fB)
by A1,A4,A7,A14,A13,A10,FUNCT_1:77;
consider MB be Matrix of n,F_Real such that
A16: MB is invertible and
A17: MB|len fB=fB by A5,A6,Th19;
set Mb=Mx2Tran MB;
A18: n=0 implies n=0;
then width(MA~) = n by MATRIX13:1;
then reconsider mb=MB as Matrix of width(MA~),n,F_Real;
A19: width MB=n by A18,MATRIX13:1;
reconsider MM=(MA~)*mb as Matrix of n,F_Real;
take MM;
MA~ is invertible by A8;
hence MM is invertible by A16,MATRIX_6:45;
Mb*(Ma")=(Mx2Tran mb)*(Ma") by A18,MATRIX13:1
.=(Mx2Tran mb)*(Mx2Tran(MA~)) by A11,MATRTOP1:43
.=Mx2Tran((MA~)*mb) by A18,MATRTOP1:32
.=Mx2Tran MM by A18,A19,MATRIX13:1;
hence (Mx2Tran MM).:[#]Lin A=Mb.:[#]Lin rng(BB|len fB) by A15,RELAT_1:126
.=[#]Lin B by A5,A6,A16,A17,Th21;
end;
begin :: Preservation of Linear and Affine Independence of Vectors by the
:: Mx2Tran Operator
theorem Th23:
for A be linearly-independent Subset of TOP-REAL n st the_rank_of M = n
holds (Mx2Tran M).:A is linearly-independent
proof
let A be linearly-independent Subset of TOP-REAL n such that
A1: the_rank_of M=n;
set nV=n-VectSp_over F_Real,mV=m-VectSp_over F_Real;
reconsider Bn=MX2FinS 1.(F_Real,n) as OrdBasis of nV by MATRLIN2:45;
reconsider Bm=MX2FinS 1.(F_Real,m) as OrdBasis of mV by MATRLIN2:45;
A2: len Bm = m by MATRTOP1:19;
len Bn=n by MATRTOP1:19;
then reconsider M1=M as Matrix of len Bn,len Bm,F_Real by A2;
set MT=Mx2Tran(M1,Bn,Bm);
A3: Mx2Tran M=MT by MATRTOP1:20;
reconsider A1=A as Subset of nV by Lm1;
A4: A1 is linearly-independent by Th7;
MT.:A1 is linearly-independent
proof
assume MT.:A1 is non linearly-independent;
then consider L be Linear_Combination of MT.:A1 such that
A5: Carrier L<>{} and
A6: Sum L=0.mV by RANKNULL:41;
A7: MT is one-to-one by A1,A3,MATRTOP1:39;
then A8: ker MT=(0).nV by RANKNULL:15;
A9: MT|A1 is one-to-one by A7,FUNCT_1:52;
then A10: MT@(MT#L)=L by RANKNULL:43;
MT|Carrier(MT#L) is one-to-one by A7,FUNCT_1:52;
then MT.:Carrier(MT#L)=Carrier L by A10,RANKNULL:39;
then A11: Carrier(MT#L)<>{} by A5;
MT.(Sum(MT#L))=0.mV by A6,A9,A10,Th14;
then Sum(MT#L) in ker MT by RANKNULL:10;
then Sum(MT#L)=0.nV by A8,VECTSP_4:35;
hence contradiction by A4,A11,VECTSP_7:def 1;
end;
hence thesis by A3,Th7;
end;
theorem Th24:
for A be affinely-independent Subset of TOP-REAL n st the_rank_of M = n
holds (Mx2Tran M).:A is affinely-independent
proof
set MT=Mx2Tran M;
set TRn=TOP-REAL n,TRm=TOP-REAL m;
let A be affinely-independent Subset of TRn such that
A1: the_rank_of M=n;
per cases;
suppose A is empty;
then MT.:A is empty;
hence thesis;
end;
suppose A is non empty;
then consider v be Element of TRn such that
A2: v in A and
A3: (-v+A)\{0.TRn} is linearly-independent by RLAFFIN1:def 4;
A4: dom MT=[#]TRn by FUNCT_2:def 1;
then A5: MT.v in MT.:A by A2,FUNCT_1:def 6;
MT.0.TRn=0.TRm by MATRTOP1:29;
then A6: {0.TRm}=Im(MT,0.TRn) by A4,FUNCT_1:59
.=MT.:{0.TRn} by RELAT_1:def 16;
-v=0.TRn-v by RLVECT_1:14;
then A7: MT.(-v)=(MT.(0.TRn))-(MT.v) by MATRTOP1:28
.=(0.TRm)-(MT.v) by MATRTOP1:29
.=-(MT.v) by RLVECT_1:14;
MT is one-to-one by A1,MATRTOP1:39;
then A8: MT.:((-v+A)\{0.TRn})=(MT.:(-v+A))\MT.:{0.TRn} by FUNCT_1:64
.=(-(MT.v)+MT.:A)\{0.TRm} by A6,A7,MATRTOP1:30;
MT.:((-v+A)\{0.TRn}) is linearly-independent by A1,A3,Th23;
hence thesis by A5,A8,RLAFFIN1:def 4;
end;
end;
theorem
for A be affinely-independent Subset of TOP-REAL n st the_rank_of M = n
for v be Element of TOP-REAL n st v in Affin A holds
(Mx2Tran M).v in Affin(Mx2Tran M).:A &
for f holds (v|--A).f = ((Mx2Tran M).v|--(Mx2Tran M).:A).((Mx2Tran M).f)
proof
reconsider Z=0 as Element of NAT;
set TRn=TOP-REAL n;
set TRm=TOP-REAL m;
let A be affinely-independent Subset of TRn such that
A1: the_rank_of M=n;
set MT=Mx2Tran M;
let v be Element of TRn such that
A2: v in Affin A;
set vA=v|--A;
set C=Carrier vA;
defpred P[object,object] means
(not$1 in rng MT implies $2=0) & ($1 in rng MT implies for f st MT.f=$1
holds $2=vA.f);
consider H be FinSequence of the carrier of TRn such that
A3: H is one-to-one and
A4: rng H=C and
A5: Sum(vA(#)H)=Sum vA by RLVECT_2:def 8;
A6: Sum vA=v by A2,RLAFFIN1:def 7;
reconsider MTR=MT*H as FinSequence of TRm;
A7: dom MT=[#]TRn by FUNCT_2:def 1;
then rng H c=dom MT;
then A8: len MTR=len H by FINSEQ_2:29;
A9: MT is one-to-one by A1,MATRTOP1:39;
A10: for x be object st x in the carrier of TRm
ex y be object st y in REAL & P[x,y]
proof
let y be object such that
y in the carrier of TRm;
per cases;
suppose A11: y in rng MT;
then consider x be object such that
A12: x in dom MT and
A13: MT.x=y by FUNCT_1:def 3;
reconsider x as Element of TRn by A12;
take vA.x;
thus vA.x in REAL & (not y in rng MT implies vA.x=0) by A11;
assume y in rng MT;
let f;
assume A14: MT.f=y;
f is Element of TRn by Lm3;
hence thesis by A7,A9,A13,A14,FUNCT_1:def 4;
end;
suppose A15: not y in rng MT;
take x=0;
thus thesis by A15;
end;
end;
consider F be Function of the carrier of TRm,REAL such that
A16: for x be object st x in the carrier of TRm holds P[x,F.x]
from FUNCT_2:sch 1(A10);
reconsider F as Element of Funcs(the carrier of TRm,REAL) by FUNCT_2:8;
A17: now let w be Element of TRm;
assume A18: not w in MT.:C;
assume A19: F.w<>0;
then w in rng MT by A16;
then consider f be object such that
A20: f in dom MT and
A21: MT.f=w by FUNCT_1:def 3;
reconsider f as Element of TRn by A20;
vA.f=F.w by A16,A19,A21;
then f in C by A19,RLVECT_2:19;
hence contradiction by A18,A20,A21,FUNCT_1:def 6;
end;
then reconsider F as Linear_Combination of TRm by RLVECT_2:def 3;
A22: MT.:C c=Carrier F
proof
let y be object;
assume A23: y in MT.:C;
then consider x be object such that
A24: x in dom MT and
A25: x in C and
A26: MT.x=y by FUNCT_1:def 6;
reconsider x as Element of TRn by A24;
A27: vA.x<>0 by A25,RLVECT_2:19;
reconsider f=y as Element of TRm by A23;
P[f,F.f] by A16;
then F.f=vA.x by A24,A26,FUNCT_1:def 3;
hence thesis by A27,RLVECT_2:19;
end;
Carrier F c=MT.:C
proof
let x be object;
assume A28: x in Carrier F;
then reconsider w=x as Element of TRm;
F.w<>0 by A28,RLVECT_2:19;
hence thesis by A17;
end;
then A29: Carrier F=MT.:C by A22;
C c=A by RLVECT_2:def 6;
then MT.:C c=MT.:A by RELAT_1:123;
then reconsider F as Linear_Combination of MT.:A by A29,RLVECT_2:def 6;
set Fm=F(#)MTR;
consider fm be sequence of TRm such that
A30: Sum Fm=fm.len Fm and
A31: fm.0=0.TRm and
A32: for j be Nat,v be Element of TRm st j<len Fm & v=Fm.(j+1)
holds fm.(j+1)=fm.j+v by RLVECT_1:def 12;
A33: rng MTR=MT.:C by A4,RELAT_1:127;
dom vA=[#]TRn by FUNCT_2:def 1;
then A34: len(vA*H)=len H by A4,FINSEQ_2:29;
set vAH=vA(#)H;
consider h be sequence of TRn such that
A35: Sum vAH=h.len vAH and
A36: h.0=0.TRn and
A37: for j be Nat,v be Element of TRn st j<len vAH & v=vAH.(j+1)
holds h.(j+1)=h.j+v by RLVECT_1:def 12;
A38: len vAH=len H by RLVECT_2:def 7;
defpred P[Nat] means
$1<=len Fm implies fm.$1=MT.(h.$1);
A39: len Fm=len MTR by RLVECT_2:def 7;
A40: MT.:C c=rng MT by RELAT_1:111;
A41: for j be Nat st P[j] holds P[j+1]
proof
reconsider TRM=TRm as RealLinearSpace;
reconsider TRN=TRn as RealLinearSpace;
let j be Nat;
reconsider J=j as Element of NAT by ORDINAL1:def 12;
set j1=J+1;
assume A42: P[j];
reconsider MTRj1=MTR/.j1 as Element of TRM;
reconsider hj1=H/.j1 as n-element real-valued FinSequence;
reconsider Hj1=H/.j1 as Element of TRN;
assume A43: j+1<=len Fm;
A44: 1<=j1 by NAT_1:11;
then A45: j1 in dom MTR by A39,A43,FINSEQ_3:25;
then A46: MTRj1=MTR.j1 by PARTFUN1:def 6;
A47: MTR.j1 in MT.:C by A33,A45,FUNCT_1:def 3;
j1 in dom H by A39,A8,A43,A44,FINSEQ_3:25;
then A48: Hj1=H.j1 by PARTFUN1:def 6;
then MTR.j1=MT.Hj1 by A45,FUNCT_1:12;
then A49: F.MTRj1=vA.Hj1 by A16,A40,A46,A47;
A50: j1 in dom vAH by A39,A38,A8,A43,A44,FINSEQ_3:25;
then vAH.j1 in rng vAH by FUNCT_1:def 3;
then reconsider vAHj1=vAH.j1 as Element of TRn;
A51: j1 in dom Fm by A43,A44,FINSEQ_3:25;
then Fm.j1 in rng Fm by FUNCT_1:def 3;
then reconsider Fmj1=Fm.j1 as Element of TRm;
A52: MT.vAHj1=MT.((vA.Hj1)*Hj1) by A50,RLVECT_2:def 7
.=MT.((vA.Hj1)*hj1) by EUCLID:65
.=(vA.Hj1)*MT.(hj1) by MATRTOP1:23
.=F.MTRj1*MTRj1 by A45,A48,A46,A49,EUCLID:65,FUNCT_1:12
.=Fmj1 by A51,RLVECT_2:def 7;
A53: j<len Fm by A43,NAT_1:13;
then h.j1=h.J+vAHj1 by A37,A39,A38,A8;
hence MT.(h.(j+1))=MT.(h.J)+MT.vAHj1 by MATRTOP1:27
.=fm.(j+1) by A32,A52,A53,A42;
end;
A54: P[0] by A36,A31,MATRTOP1:29;
for j be Nat holds P[j] from NAT_1:sch 2(A54,A41);
then Sum Fm=MT.(Sum vAH) by A35,A30,A39,A38,A8;
then A55: Sum F=MT.v by A9,A29,A3,A5,A6,A33,RLVECT_2:def 8;
A56: now let i be Nat;
assume A57: 1<=i & i<=len H;
then A58: i in dom H by FINSEQ_3:25;
then A59: (vA*H).i=vA.(H.i) by FUNCT_1:13;
H.i in rng H by A58,FUNCT_1:def 3;
then reconsider Hi=H.i as Element of TRn;
A60: MTR.i=MT.(H.i) by A58,FUNCT_1:13;
A61: i in dom MTR by A8,A57,FINSEQ_3:25;
then A62: MTR.i in rng MTR by FUNCT_1:def 3;
(F*MTR).i=F.(MTR.i) by A61,FUNCT_1:13;
then P[MT.Hi,(F*MTR).i] by A16,A60;
hence (F*MTR).i=(vA*H).i by A33,A40,A59,A60,A62;
end;
dom F=[#]TRm by FUNCT_2:def 1;
then len(F*MTR)=len MTR by A33,FINSEQ_2:29;
then vA*H=F*MTR by A8,A34,A56;
then Sum(F*MTR)=sum vA by A3,A4,RLAFFIN1:def 3
.=1 by A2,RLAFFIN1:def 7;
then A63: sum F=1 by A9,A29,A3,A33,RLAFFIN1:def 3;
then Sum F in {Sum L where L is Linear_Combination of MT.:A:sum L=1};
hence A64: MT.v in Affin(MT.:A) by A55,RLAFFIN1:59;
let f;
f is Element of TRn by Lm3;
then A65: MT.f in rng MT by A7,FUNCT_1:def 3;
MT.:A is affinely-independent by A1,Th24;
then F=MT.v|--MT.:A by A55,A63,A64,RLAFFIN1:def 7;
hence thesis by A16,A65;
end;
theorem Th26:
for A be linearly-independent Subset of TOP-REAL m st the_rank_of M = n
holds (Mx2Tran M)"A is linearly-independent
proof
let A be linearly-independent Subset of TOP-REAL m such that
A1: the_rank_of M=n;
set nV=n-VectSp_over F_Real,mV=m-VectSp_over F_Real;
reconsider Bm=MX2FinS 1.(F_Real,m) as OrdBasis of mV by MATRLIN2:45;
reconsider A1=A as Subset of mV by Lm1;
reconsider Bn=MX2FinS 1.(F_Real,n) as OrdBasis of nV by MATRLIN2:45;
A2: len Bm=m by MATRTOP1:19;
len Bn=n by MATRTOP1:19;
then reconsider M1=M as Matrix of len Bn,len Bm,F_Real by A2;
set MT=Mx2Tran(M1,Bn,Bm);
A3: Mx2Tran M=MT by MATRTOP1:20;
A4: MT is one-to-one by A1,A3,MATRTOP1:39;
reconsider R=A/\rng MT as Subset of mV;
A5:R c= A by XBOOLE_1:17;
A1 is linearly-independent by Th7;
then A6: dom MT=[#]nV & R is linearly-independent
by A5,FUNCT_2:def 1,VECTSP_7:1;
MT"R is linearly-independent
proof
assume MT"R is non linearly-independent;
then consider L be Linear_Combination of MT"R such that
A7: Carrier L<>{} and
A8: Sum L=0.nV by RANKNULL:41;
set C=Carrier L;
A9: C c=MT"R by VECTSP_6:def 4;
MT.:(MT"R)=R & MT@L is Linear_Combination of MT.:C
by FUNCT_1:77,RANKNULL:29,XBOOLE_1:17;
then A10: MT@L is Linear_Combination of R by A9,RELAT_1:123,VECTSP_6:4;
MT|C is one-to-one by A4,FUNCT_1:52;
then A11: Carrier(MT@L)=MT.:C by RANKNULL:39;
MT| (MT"R) is one-to-one by A4,FUNCT_1:52;
then Sum(MT@L)=MT.(Sum L) by Th14
.=0.mV by A8,RANKNULL:9;
hence contradiction by A6,A7,A11,A10,VECTSP_7:def 1;
end;
then MT"A is linearly-independent by RELAT_1:133;
hence thesis by A3,Th7;
end;
theorem
for A be affinely-independent Subset of TOP-REAL m st the_rank_of M = n
holds (Mx2Tran M)"A is affinely-independent
proof
set MT=Mx2Tran M;
set TRn=TOP-REAL n,TRm=TOP-REAL m;
let A be affinely-independent Subset of TRm such that
A1: the_rank_of M=n;
reconsider R=A/\rng MT as affinely-independent Subset of TRm by RLAFFIN1:43
,XBOOLE_1:17;
A2: MT"A=MT"(A/\rng MT) by RELAT_1:133;
per cases;
suppose R is empty;
then MT"A is empty by A2;
hence thesis;
end;
suppose R is non empty;
then consider v be Element of TRm such that
A3: v in R and
A4: (-v+R)\{0.TRm} is linearly-independent by RLAFFIN1:def 4;
v in rng MT by A3,XBOOLE_0:def 4;
then consider x be object such that
A5: x in dom MT and
A6: MT.x=v by FUNCT_1:def 3;
reconsider x as Element of TRn by A5;
-x=0.TRn-x by RLVECT_1:14;
then A7: MT.(-x)=(MT.(0.TRn))-(MT.x) by MATRTOP1:28
.=(0.TRm)-(MT.x) by MATRTOP1:29
.=-v by A6,RLVECT_1:14;
A8: dom MT=[#]TRn by FUNCT_2:def 1;
MT.0.TRn=0.TRm by MATRTOP1:29;
then A9: {0.TRm}=Im(MT,0.TRn) by A8,FUNCT_1:59
.=MT.:{0.TRn} by RELAT_1:def 16;
MT is one-to-one by A1,MATRTOP1:39;
then A10: MT"{0.TRm}c={0.TRn} by A9,FUNCT_1:82;
{0.TRn}c=[#]TRn by ZFMISC_1:31;
then {0.TRn}c=MT"{0.TRm} by A8,A9,FUNCT_1:76;
then MT"{0.TRm}={0.TRn} by A10;
then MT"((-v+R)\{0.TRm})=MT"(-v+R)\{0.TRn} by FUNCT_1:69
.=-x+(MT"R)\{0.TRn} by A7,MATRTOP1:31;
then A11: -x+(MT"R)\{0.TRn} is linearly-independent by A1,A4,Th26;
x in MT"R by A3,A5,A6,FUNCT_1:def 7;
hence thesis by A2,A11,RLAFFIN1:def 4;
end;
end;