:: Linear Transformations of Euclidean Topological Spaces
:: 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, BINOP_2, CARD_1, CARD_3, CLASSES1,
COMPLEX1, CONNSP_2, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1,
FINSOP_1, FUNCT_1, FUNCT_2, FVSUM_1, INCSP_1, LMOD_7, MATRIX_1, MATRIX_3,
MATRIX_6, MATRIX13, MATRIX15, MATRIXR1, MATRLIN, MATRLIN2, MESFUNC1,
METRIC_1, NAT_1, NUMBERS, ORDINAL2, ORDINAL4, PARTFUN1, PARTFUN3,
PRE_POLY, PRE_TOPC, PRVECT_1, QC_LANG1, RANKNULL, REAL_1, RELAT_1,
RLSUB_1, RLVECT_3, RLVECT_5, RVSUM_1, SQUARE_1, STRUCT_0, SUBSET_1,
SUPINF_2, TARSKI, TOPS_1, TOPS_2, TREES_1, VALUED_0, VALUED_1, VECTSP_1,
VECTSP10, XBOOLE_0, XXREAL_0, ZFMISC_1, FUNCOP_1, FUNCT_7, MOD_3,
NUMBER09, GROUP_1, XCMPLX_0;
notations GROUP_1, VECTSP_2, GCD_1, TARSKI, XBOOLE_0, ZFMISC_1,
SUBSET_1, RELAT_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
FINSET_1, TOPS_1, TOPS_2, FUNCT_1, PARTFUN1, VALUED_0, VALUED_1,
FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, BINOP_1, STRUCT_0,
VECTSP_1, MATRIX_0, MATRIX_1, MATRIX_3, VECTSP_4, VECTSP_7,
VECTSP_9, MATRIX13, XREAL_0, RVSUM_1, ALGSTR_0, FVSUM_1, RANKNULL,
MATRIX11, COMPLEX1, BINOP_2, FUNCOP_1, SQUARE_1, PRE_TOPC,
PARTFUN3, MATRIX_6, MATRLIN, MATRLIN2, NAT_D, MATRIX15, CONNSP_2,
METRIC_1, EUCLID, FINSOP_1, PNPROC_1, RUSUB_4, PRVECT_1;
constructors GROUP_1, VECTSP_2, GCD_1, BINARITH, CONNSP_2, FINSOP_1,
FVSUM_1, LAPLACE, MATRIX_6, MATRIX11, MATRIX13, MATRIX15,
MATRLIN2, MONOID_0, PARTFUN3, PNPROC_1, RANKNULL, RELSET_1,
RUSUB_5, SETWISEO, SQUARE_1, TOPS_1, TOPS_2, VECTSP_9, VECTSP10,
WELLORD2, EUCLID, MATRIX_1, REAL_1, BINOP_2, VALUED_2, MATRIX_3;
registrations BINOP_2, CARD_1, EUCLID, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSET_1,
FUNCT_1, FUNCT_2, GRCAT_1, MATRIX13, MATRLIN2, MEMBERED, MOD_2, MONOID_0,
NAT_1, NUMBERS, PARTFUN3, PRVECT_1, RELAT_1, RELSET_1, RVSUM_1, STRUCT_0,
VALUED_0, VALUED_1, VECTSP_1, VECTSP_9, XREAL_0, XXREAL_0, MATRIX_6,
ORDINAL1, MATRIX_1, MATRIX_3, GCD_1, LAPLACE;
requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
definitions BORSUK_1, PARTFUN3, TARSKI, XBOOLE_0;
equalities EUCLID, FINSEQ_1, MATRIX13, RANKNULL, SQUARE_1, STRUCT_0, VECTSP_1,
VECTSP_4, XBOOLE_0, FVSUM_1, RLVECT_1;
expansions FINSEQ_1, PARTFUN3, STRUCT_0, TARSKI, XBOOLE_0;
theorems ABSVALUE, BINOP_2, CARD_1, CARD_2, CONNSP_2, EUCLID, EUCLID_2,
FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQOP, FINSOP_1,
FUNCOP_1, FUNCT_1, FUNCT_2, FVSUM_1, GOBOARD6, LAPLACE, MATRIX_0,
MATRIX_3, MATRIX_4, MATRIX_6, MATRIX11, MATRIX13, MATRIX14,
MATRIX15, MATRIXR1, MATRLIN, MATRLIN2, MATRPROB, METRIC_1, NAT_1,
ORDINAL1, PARTFUN3, RANKNULL, RELAT_1, RLVECT_1, RUSUB_4, RVSUM_1,
SPPOL_1, SQUARE_1, TARSKI, TOPREAL3, TOPS_2, VALUED_0, VALUED_1,
VECTSP_4, VECTSP_7, VECTSP_9, XBOOLE_0, XBOOLE_1, XCMPLX_1,
XREAL_0, XREAL_1, XXREAL_0, ZFMISC_1, MATRIX_7, MATRIXR2;
schemes FINSEQ_1, FUNCT_2, NAT_1;
begin :: Preliminaries
reserve X,Y for set,
n,m,k,i for Nat,
r for Real,
R for Element of F_Real,
K for Field,
f,f1,f2,g1,g2 for FinSequence,
rf,rf1,rf2 for real-valued FinSequence,
cf,cf1,cf2 for complex-valued FinSequence,
F for Function;
registration
let X,Y;
let F be positive-yielding PartFunc of X,REAL;
cluster F|Y -> positive-yielding;
coherence
proof
let r be Real;
assume
A1: r in rng(F|Y);
rng(F|Y)c=rng F by RELAT_1:70;
hence thesis by A1,PARTFUN3:def 1;
end;
end;
registration
let X,Y;
let F be negative-yielding PartFunc of X,REAL;
cluster F|Y -> negative-yielding;
coherence
proof
let r be Real;
assume
A1: r in rng(F|Y);
rng(F|Y)c=rng F by RELAT_1:70;
hence thesis by A1,PARTFUN3:def 2;
end;
end;
registration
let X,Y;
let F be nonpositive-yielding PartFunc of X,REAL;
cluster F|Y -> nonpositive-yielding;
coherence
proof
let r be Real;
assume
A1: r in rng(F|Y);
rng(F|Y)c=rng F by RELAT_1:70;
hence thesis by A1,PARTFUN3:def 3;
end;
end;
registration
let X,Y;
let F be nonnegative-yielding PartFunc of X,REAL;
cluster F|Y -> nonnegative-yielding;
coherence
proof
let r be Real;
assume
A1: r in rng(F|Y);
rng(F|Y)c=rng F by RELAT_1:70;
hence thesis by A1,PARTFUN3:def 4;
end;
end;
registration
let rf;
cluster sqrt rf -> FinSequence-like;
coherence
proof
dom rf=dom sqrt rf & ex n st dom rf=Seg n
by FINSEQ_1:def 2,PARTFUN3:def 5;
hence thesis;
end;
end;
definition
let rf;
func @rf -> FinSequence of F_Real equals
rf;
coherence
proof
rng rf c=REAL;
hence thesis by FINSEQ_1:def 4;
end;
end;
definition
let p be FinSequence of F_Real;
func @p -> FinSequence of REAL equals
p;
coherence;
end;
theorem
@rf1 + @rf2 = rf1 + rf2 by RVSUM_1:def 4;
theorem Th2:
sqrt (rf1^rf2) = (sqrt rf1) ^ (sqrt rf2)
proof
set rf12=rf1^rf2;
set s12=sqrt rf12,s1=sqrt rf1,s2=sqrt rf2;
A1: dom s12=dom rf12 by PARTFUN3:def 5;
A2: dom s2=dom rf2 by PARTFUN3:def 5;
then
A3: len s2=len rf2 by FINSEQ_3:29;
A4: dom s1=dom rf1 by PARTFUN3:def 5;
then
A5: len s1=len rf1 by FINSEQ_3:29;
A6: 1<=n & n<=len s12 implies s12.n=(s1^s2).n
proof
assume 1<=n & n<=len s12;
then
A7: n in dom s12 by FINSEQ_3:25;
then
A8: s12.n=sqrt(rf12.n) by PARTFUN3:def 5;
per cases by A1,A7,FINSEQ_1:25;
suppose
A9: n in dom rf1;
then rf12.n=rf1.n & s1.n=sqrt(rf1.n)
by A4,FINSEQ_1:def 7,PARTFUN3:def 5;
hence thesis by A4,A8,A9,FINSEQ_1:def 7;
end;
suppose ex m st m in dom rf2 & n=len rf1+m;
then consider m such that
A10: m in dom rf2 & n=len rf1+m;
rf12.n=rf2.m & s2.m=sqrt(rf2.m)
by A2,A10,FINSEQ_1:def 7,PARTFUN3:def 5;
hence thesis by A2,A5,A8,A10,FINSEQ_1:def 7;
end;
end;
len s12=len rf12 by A1,FINSEQ_3:29;
then len s12=len s1+len s2 by A5,A3,FINSEQ_1:22;
then len s12=len(s1^s2) by FINSEQ_1:22;
hence thesis by A6;
end;
theorem Th3:
sqrt <*r*> = <*sqrt r*>
proof
set R=<*r*>;
A1: R.1=r;
A2: dom R=dom sqrt R by PARTFUN3:def 5;
then
A3: len R=len sqrt R by FINSEQ_3:29;
1 in Seg 1 & dom R=Seg 1 by FINSEQ_1:38;
then len R=1 & (sqrt R).1=sqrt r by A2,A1,FINSEQ_1:40,PARTFUN3:def 5;
hence thesis by A3,FINSEQ_1:40;
end;
theorem Th4:
sqrt(rf^2)=abs rf
proof
set F=rf^2;
set S=sqrt F;
A1: dom S=dom F by PARTFUN3:def 5;
A2: dom abs rf=dom rf & dom F=dom rf by VALUED_1:11,def 11;
now let x be object;
reconsider fx=rf.x as Real;
A3: fx>=0 or fx<0;
assume
A4: x in dom abs rf;
then F.x=fx^2 & S.x=sqrt(F.x) by A2,A1,PARTFUN3:def 5,VALUED_1:11;
then
A5: S.x=fx & fx>=0 or S.x=-fx & fx<0 by A3,SQUARE_1:22,23;
(abs rf).x=|.fx.| by A4,VALUED_1:def 11;
hence (abs rf).x=S.x by A5,ABSVALUE:def 1;
end;
hence thesis by A2,A1,FUNCT_1:2;
end;
theorem Th5:
rf is nonnegative-yielding implies sqrt Sum rf <= Sum sqrt rf
proof
defpred P[Nat] means
for f be real-valued FinSequence st len f=$1 & f is nonnegative-yielding
holds sqrt Sum f<=Sum sqrt f & 0<=Sum f;
A1: P[n] implies P[n+1]
proof
assume
A2: P[n];
set n1=n+1;
let f be real-valued FinSequence such that
A3: len f=n1 and
A4: f is nonnegative-yielding;
rng f c=REAL;
then reconsider F=f as FinSequence of REAL by FINSEQ_1:def 4;
reconsider fn=F|n as FinSequence of REAL;
A5: F=fn^<*F.n1*> by A3,FINSEQ_3:55;
then sqrt F = (sqrt fn)^sqrt<*F.n1*> by Th2
.= (sqrt fn)^<*sqrt(F.n1)*> by Th3;
then
A6: Sum sqrt F=Sum(sqrt fn)+sqrt(F.n1) by RVSUM_1:74;
A7: len fn=n by A3,FINSEQ_3:53;
then sqrt(Sum fn)<=Sum sqrt fn by A2,A4;
then
A8: sqrt(Sum fn)+sqrt(f.n1)<=Sum sqrt F by A6,XREAL_1:6;
A9: Sum f=(Sum fn)+(f.n1) by A5,RVSUM_1:74;
n1>=1 by NAT_1:11;
then n1 in dom f by A3,FINSEQ_3:25;
then f.n1 in rng f by FUNCT_1:def 3;
then
A10: f.n1>=0 by A4;
A11: (Sum fn)>=0 by A2,A4,A7;
then sqrt Sum f<=sqrt(Sum fn)+sqrt(f.n1) by A9,A10,SQUARE_1:59;
hence thesis by A9,A11,A10,A8,XXREAL_0:2;
end;
A12: P[0 qua Nat]
proof
let f be real-valued FinSequence such that
A13: len f=0 and
f is nonnegative-yielding;
dom f=dom sqrt f by PARTFUN3:def 5;
then len f=len sqrt f by FINSEQ_3:29;
then
A14: sqrt f=<*>REAL by A13;
f=<*>REAL by A13;
hence thesis by A14,RVSUM_1:72,SQUARE_1:17;
end;
P[n] from NAT_1:sch 2(A12,A1);
then P[len rf];
hence thesis;
end;
theorem
ex X st X c= dom F & rng F = rng(F|X) & (F|X) is one-to-one
proof
defpred P[object,object] means
F.$2=$1;
A1: for x be object st x in rng F ex y being object st y in dom F & P[x,y]
by FUNCT_1:def 3;
consider g being Function of rng F,dom F such that
A2: for x be object st x in rng F holds P[x,g.x] from FUNCT_2:sch 1(A1);
take X=rng g;
set FX=F|X;
dom F={} iff rng F={} by RELAT_1:42;
then
A3: dom g=rng F by FUNCT_2:def 1;
thus
A4: X c=dom F by RELAT_1:def 19;
A5: rng F c=rng FX
proof
let y be object;
assume y in rng F;
then g.y in X & F.(g.y)=y by A2,A3,FUNCT_1:def 3;
hence thesis by A4,FUNCT_1:50;
end;
rng FX c=rng F by RELAT_1:70;
hence rng F=rng FX by A5;
now let x1,x2 be object;
assume that
A6: x1 in dom FX and
A7: x2 in dom FX and
A8: FX.x1=FX.x2;
A9: FX.x1=F.x1 & FX.x2=F.x2 by A6,A7,FUNCT_1:47;
A10: dom FX c=X by RELAT_1:58;
then consider y1 be object such that
A11: y1 in dom g and
A12: g.y1=x1 by A6,FUNCT_1:def 3;
consider y2 be object such that
A13: y2 in dom g & g.y2=x2 by A7,A10,FUNCT_1:def 3;
F.x1=y1 by A2,A3,A11,A12;
hence x1=x2 by A2,A3,A8,A9,A12,A13;
end;
hence thesis by FUNCT_1:def 4;
end;
registration
let cf,X;
cluster cf-X -> complex-valued;
coherence
proof
rng cf c=COMPLEX & rng(cf-X)c=rng cf by FINSEQ_3:66,VALUED_0:def 1;
then rng(cf-X)c=COMPLEX;
hence thesis by VALUED_0:def 1;
end;
end;
registration
let rf,X;
cluster rf-X -> real-valued;
coherence
proof
rng(rf-X)c=rng rf by FINSEQ_3:66;
then rng(rf-X)c=REAL by XBOOLE_1:1;
hence thesis by VALUED_0:def 3;
end;
end;
registration
let cf be complex-valued FinSubsequence;
cluster Seq cf -> complex-valued;
coherence;
end;
registration
let rf be real-valued FinSubsequence;
cluster Seq rf -> real-valued;
coherence;
end;
theorem Th7:
for P be Permutation of dom f st f1 = f*P
ex Q be Permutation of dom(f-X) st f1-X = (f-X)*Q
proof
let P be Permutation of dom f such that
A1: f1=f*P;
reconsider p=P as one-to-one Function;
A2: rng P=dom f by FUNCT_2:def 3;
then A3: dom(p")=dom f by FUNCT_1:33;
A4: P.:(f1"X)=P.:(P"(f"X)) by A1,RELAT_1:146
.=f"X by A2,FUNCT_1:77,RELAT_1:132;
A5: dom P=dom f by FUNCT_2:52;
then A6: dom f1=dom f by A1,A2,RELAT_1:27;
set DfX=(dom f1)\f1"X;
set DX=(dom f)\f"X;
A7: card DX=card(dom f)-card(f"X) by CARD_2:44,RELAT_1:132;
A9: dom Sgm DX=Seg card DX by FINSEQ_3:40;
A10: p"(f"X)=(p").:(f"X) by FUNCT_1:85;
f1"X=P"(f"X) by A1,RELAT_1:146;
then A11: f"X,f1"X are_equipotent by A3,A10,CARD_1:33,RELAT_1:132;
A13: rng(P*Sgm DfX)=P.:(rng Sgm DfX) by RELAT_1:127
.=P.:DfX by FINSEQ_1:def 14
.=(P.:(dom P))\P.:(f1"X) by A5,A6,FUNCT_1:64
.=DX by A4,A2,RELAT_1:113;
reconsider SDX=Sgm DX as one-to-one Function by FINSEQ_3:92;
A14: dom(SDX")=rng SDX by FUNCT_1:33;
card(dom f)=len f by CARD_1:62;
then A15: dom(f-X)=dom SDX by A7,A9,FINSEQ_3:62;
card DfX=card(dom f1)-card(f1"X) by CARD_2:44,RELAT_1:132;
then card DX=card DfX by A11,A6,A7,CARD_1:5;
then A16: dom SDX=dom Sgm DfX by A9,FINSEQ_3:40;
A17: rng Sgm DX=DX by FINSEQ_1:def 14;
rng(SDX")=dom SDX by FUNCT_1:33;
then A18: rng((SDX")*(P*Sgm DfX))=dom SDX by A17,A14,A13,RELAT_1:28;
rng Sgm DfX=DfX by FINSEQ_1:def 14;
then dom(P*Sgm DfX)=dom Sgm DfX by A5,A6,RELAT_1:27,XBOOLE_1:36;
then dom((SDX")*(P*Sgm DfX))=dom Sgm DfX by A17,A14,A13,RELAT_1:27;
then reconsider Q=(SDX")*(P*Sgm DfX) as Function of dom(f-X),dom(f-X)
by A18,A15,A16,FUNCT_2:1;
A19: Q is onto by A18,A15,FUNCT_2:def 3;
Sgm DfX is one-to-one by FINSEQ_3:92;
then reconsider Q as Permutation of dom(f-X) by A19;
SDX*(SDX")=id DX by A17,FUNCT_1:39;
then A20: SDX*Q=(id DX)*(P*Sgm DfX) by RELAT_1:36
.=P*Sgm DfX by A13,RELAT_1:53;
(f-X)*Q=f*SDX*Q by FINSEQ_3:def 1
.=f*(P*Sgm DfX) by A20,RELAT_1:36
.=f1*Sgm DfX by A1,RELAT_1:36
.=f1-X by FINSEQ_3:def 1;
hence thesis;
end;
theorem
for P be Permutation of dom cf st cf1 = cf*P holds Sum (cf1-X) = Sum(cf-X)
proof
rng(cf1-X)c=COMPLEX by VALUED_0:def 1;
then reconsider fPX=cf1-X as FinSequence of COMPLEX by FINSEQ_1:def 4;
rng(cf-X)c=COMPLEX by VALUED_0:def 1;
then reconsider fX=cf-X as FinSequence of COMPLEX by FINSEQ_1:def 4;
let P be Permutation of dom cf such that
A1: cf1=cf*P;
consider Q be Permutation of dom(cf-X) such that
A2: cf1-X=(cf-X)*Q by A1,Th7;
thus Sum(cf1-X)=addcomplex"**"fPX by RVSUM_1:def 11
.=addcomplex"**"fX by A2,FINSOP_1:7
.=Sum(cf-X) by RVSUM_1:def 11;
end;
theorem Th9:
for f,f1 be FinSubsequence for P be Permutation of dom f st f1 = f*P
ex Q be Permutation of dom Seq(f1|P"X) st Seq(f|X) = Seq(f1|P"X) * Q
proof
let f,f1 be FinSubsequence;
consider n be Nat such that
A1: dom f c=Seg n by FINSEQ_1:def 12;
let P be Permutation of dom f such that
A2: f1=f*P;
set SPX=Sgm(P"X);
A3: P"X c=dom P by RELAT_1:132;
then A4: dom(P|P"X)=P"X by RELAT_1:62;
A5: dom P=dom f by FUNCT_2:52;
then P"X c= Seg n by A1,A3;
then
a1: P"X is included_in_Seg;
then
A6: SPX is one-to-one by FINSEQ_3:92;
set dfX=dom f/\X;
set SdX=Sgm dfX;
A8: rng SdX=dfX by FINSEQ_1:def 14;
A9: rng P=dom f by FUNCT_2:def 3;
then A10: P"X=P"dfX by RELAT_1:133;
then A11: P"X=(P").:dfX by FUNCT_1:85;
set PS=(P|P"X)*SPX;
A12: P|P"X is one-to-one by FUNCT_1:52;
P"X c=Seg n by A1,A5,A3;
then P"X is included_in_Seg;
then A13: rng SPX=P"X by FINSEQ_1:def 14;
rng(P|P"X)=P.:(P"dfX) by A10,RELAT_1:115
.=dfX by A9,FUNCT_1:77,XBOOLE_1:17;
then A14: rng PS=dfX by A4,A13,RELAT_1:28;
A15: dom((PS qua Function)")=dfX by A6,A12,A14,FUNCT_1:33;
dom(P")=rng P by FUNCT_1:33;
then dfX,(P").:dfX are_equipotent by A9,CARD_1:33,XBOOLE_1:17;
then card dfX=card(P"X) by A11,CARD_1:5;
then A16: dom SPX=Seg card dfX by a1,FINSEQ_3:40;
then dom PS=Seg card dfX by A4,A13,RELAT_1:27;
then rng((PS qua Function)")=Seg card dfX by A6,A12,FUNCT_1:33;
then A17: rng(((PS qua Function)")*SdX)=Seg card dfX by A15,A8,RELAT_1:28;
dom f1=dom P by A2,A9,RELAT_1:27;
then A18: dom(f1|P"X)=P"X by RELAT_1:62,132;
then A19: dom Seq(f1|P"X)=Seg card dfX by A16,A13,RELAT_1:27;
dom SdX=Seg card dfX by FINSEQ_3:40;
then dom(((PS qua Function)")*SdX)=Seg card dfX by A15,A8,RELAT_1:27;
then reconsider PSS=((PS qua Function)")*SdX
as Function of dom Seq(f1|P"X),dom Seq(f1|P"X)
by A19,A17,FUNCT_2:1;
A20: PSS is onto by A19,A17,FUNCT_2:def 3;
SdX is one-to-one by FINSEQ_3:92;
then reconsider PSS as Permutation of dom Seq(f1|P"X) by A6,A12,A20;
A21: PS*PSS=(PS*(PS qua Function)")*SdX by RELAT_1:36
.=(id dfX)*SdX by A6,A12,A14,FUNCT_1:39;
set fX=f|X;
A22: fX=f|dfX by RELAT_1:157;
take PSS;
f1|P"X=f*(P|P"X) by A2,RELAT_1:83;
hence Seq(f1|P"X)*PSS=f*PS*PSS by A18,RELAT_1:36
.=f*((id dfX)*SdX) by A21,RELAT_1:36
.=(f*(id dfX))*SdX by RELAT_1:36
.=fX*SdX by A22,RELAT_1:65
.=Seq fX by RELAT_1:61;
end;
theorem
for cf,cf1 be complex-valued FinSubsequence
for P be Permutation of dom cf st cf1 = cf * P
holds Sum Seq(cf|X) = Sum Seq(cf1|P"X)
proof
let cf,cf1 be complex-valued FinSubsequence;
rng Seq(cf|X)c=COMPLEX by VALUED_0:def 1;
then reconsider SfX=Seq(cf|X) as FinSequence of COMPLEX by FINSEQ_1:def 4;
let P be Permutation of dom cf such that
A1: cf1=cf*P;
consider Q be Permutation of dom Seq(cf1|P"X) such that
A2: Seq(cf|X)=Seq(cf1|P"X)*Q by A1,Th9;
rng Seq(cf1|P"X)c=COMPLEX by VALUED_0:def 1;
then reconsider SfPX=Seq(cf1|P"X) as FinSequence of COMPLEX
by FINSEQ_1:def 4;
thus Sum Seq(cf1|P"X)=addcomplex"**"SfPX by RVSUM_1:def 11
.=addcomplex"**"SfX by A2,FINSOP_1:7
.=Sum Seq(cf|X) by RVSUM_1:def 11;
end;
theorem Th11:
for f be FinSubsequence for n be Element of NAT st
for i holds i+n in X iff i in Y
holds (n Shift f) |X = n Shift(f|Y)
proof
let f be FinSubsequence;
let n be Element of NAT such that
A1: i+n in X iff i in Y;
set fY=f|Y;
set nf=n Shift f;
set nfX=nf|X;
set nfY=n Shift fY;
A2: dom nfY={k+n where k is Nat:k in dom fY} by VALUED_1:def 12;
A3: now let x be object;
assume x in dom nfY;
then consider k be Nat such that
A4: x=k+n and
A5: k in dom fY by A2;
A6: k in dom f by A5,RELAT_1:57;
A7: k in Y by A5,RELAT_1:57;
then x in X by A1,A4;
hence nfX.x=nf.x by FUNCT_1:49
.=f.k by A4,A6,VALUED_1:def 12
.=fY.k by A7,FUNCT_1:49
.=nfY.x by A4,A5,VALUED_1:def 12;
end;
A8: dom nf={k+n where k is Nat:k in dom f} by VALUED_1:def 12;
A9: dom nfY c=dom nfX
proof
let x be object;
assume x in dom nfY;
then consider k be Nat such that
A10: x=k+n and
A11: k in dom fY by A2;
k in Y by A11,RELAT_1:57;
then A12: x in X by A1,A10;
k in dom f by A11,RELAT_1:57;
then x in dom nf by A8,A10;
hence thesis by A12,RELAT_1:57;
end;
dom nfX c=dom nfY
proof
let x be object;
assume A13: x in dom nfX;
then x in dom nf by RELAT_1:57;
then consider k be Nat such that
A14: x=k+n and
A15: k in dom f by A8;
x in X by A13,RELAT_1:57;
then k in Y by A1,A14;
then k in dom fY by A15,RELAT_1:57;
hence thesis by A2,A14;
end;
then dom nfY=dom nfX by A9;
hence thesis by A3,FUNCT_1:2;
end;
theorem Th12:
ex Y be Subset of NAT st
Seq((f1^f2) |X) = Seq(f1|X)^Seq(f2|Y) &
for n st n>0 holds n in Y iff n+len f1 in X/\dom(f1^f2)
proof
set f12=f1^f2;
set n1=len f1,n2=len f2;
set X12=X/\dom f12;
set X1=X12/\Seg n1,X2=X12\(Seg n1);
set Y2={i where i is Element of NAT:i+n1 in X2};
Y2 c=NAT
proof
let x be object;
assume x in Y2;
then ex i be Element of NAT st i=x & i+n1 in X2;
hence thesis;
end;
then reconsider Y2 as Subset of NAT;
set Sf2=n1 Shift f2;
A1: f12=f1\/Sf2 by VALUED_1:49;
take Y2;
A2: X12/\dom Sf2 c=X2
proof
let x be object;
assume A3: x in X12/\dom Sf2;
then x in dom Sf2 by XBOOLE_0:def 4;
then x in {k+n1 where k is Nat:k in dom f2} by VALUED_1:def 12;
then consider k be Nat such that
A4: x=k+n1 and
A5: k in dom f2;
1<=k by A5,FINSEQ_3:25;
then 1+n1<=k+n1 by XREAL_1:6;
then n1<k+n1 by NAT_1:13;
then A6: not x in Seg n1 by A4,FINSEQ_1:1;
x in X12 by A3,XBOOLE_0:def 4;
hence thesis by A6,XBOOLE_0:def 5;
end;
A7: now let i;
thus i+n1 in X2 implies i in Y2
proof
assume A8: i+n1 in X2;
i in NAT by ORDINAL1:def 12;
hence thesis by A8;
end;
assume i in Y2;
then ex j be Element of NAT st i=j & j+n1 in X2;
hence i+n1 in X2;
end;
f1|X1 c=f1 & f2|Y2 c=f2 by RELAT_1:59;
then consider ss be FinSubsequence such that
A9: ss=(f1|X1)\/(n1 Shift(f2|Y2)) & (Seq(f1|X1))^(Seq(f2|Y2))=Seq ss
by VALUED_1:64;
A10: dom f1=Seg n1 by FINSEQ_1:def 3;
then (dom f12)/\Seg n1=Seg n1 by FINSEQ_1:26,XBOOLE_1:28;
then A11: f1|X=f1| (X/\((dom f12)/\Seg n1)) by A10,RELAT_1:157
.=f1|X1 by XBOOLE_1:16;
X2 c=X12/\dom Sf2
proof
let x be object;
assume A12: x in X2;
then A13: not x in Seg n1 by XBOOLE_0:def 5;
A14: x in X12 by A12,XBOOLE_0:def 5;
then x in dom f12 by XBOOLE_0:def 4;
then consider k be Nat such that
A15: k in dom f2 & x=n1+k by A10,A13,FINSEQ_1:25;
x in {i+n1 where i is Nat:i in dom f2} by A15;
then x in dom Sf2 by VALUED_1:def 12;
hence thesis by A14,XBOOLE_0:def 4;
end;
then A16: X2=X12/\dom Sf2 by A2;
f12|X=f12|X12 by RELAT_1:157;
then f12|X=f12*(id X12) by RELAT_1:65
.=(f1*(id X12))\/(Sf2*(id X12)) by A1,RELAT_1:32
.=(f1|X12)\/(Sf2*(id X12)) by RELAT_1:65
.=(f1|X12)\/(Sf2|X12) by RELAT_1:65
.=(f1|X12)\/(Sf2|X2) by A16,RELAT_1:157
.=(f1|X1)\/(Sf2|X2) by A10,RELAT_1:157;
hence Seq((f1^f2) |X)=Seq(f1|X)^Seq(f2|Y2) by A7,A11,A9,Th11;
let n;
assume n>0;
then n+n1> (0 qua Nat)+n1 by XREAL_1:6;
then A17: not n+n1 in Seg n1 by FINSEQ_1:1;
hereby assume n in Y2;
then n+n1 in X2 by A7;
hence n+n1 in X12 by XBOOLE_0:def 5;
end;
assume n+n1 in X12;
then n+n1 in X2 by A17,XBOOLE_0:def 5;
hence n in Y2 by A7;
end;
theorem
len g1 = len f1 & len g2 <= len f2 implies
Seq((f1^f2) | (g1^g2)"X) = Seq(f1|g1"X) ^ Seq(f2|g2"X)
proof
assume that
A1: len f1=len g1 and
A2: len g2<=len f2;
set f12=f1^f2,g12=g1^g2;
A3: dom f12=Seg len f12 & dom g12=Seg len g12 by FINSEQ_1:def 3;
set g12X=g12"X;
consider Y be Subset of NAT such that
A4: Seq(f12|g12X)=Seq(f1|g12X)^Seq(f2|Y) and
A5: for n st n>0 holds n in Y iff n+len f1 in g12X/\dom f12 by Th12;
A6: Y/\dom f2 c=g2"X
proof
let x be object;
assume A7: x in Y/\dom f2;
then reconsider i=x as Nat;
x in dom f2 by A7,XBOOLE_0:def 4;
then A8: i>0 by FINSEQ_3:25;
then i+len f1>len f1+(0 qua Nat) by XREAL_1:6;
then A9: not i+len f1 in dom g1 by A1,FINSEQ_3:25;
x in Y by A7,XBOOLE_0:def 4;
then i+len f1 in g12X/\dom f12 by A5,A8;
then A10: i+len f1 in g12X by XBOOLE_0:def 4;
then A11: g12.(i+len f1) in X by FUNCT_1:def 7;
i+len f1 in dom g12 by A10,FUNCT_1:def 7;
then A12: ex j be Nat st j in dom g2 & i+len f1=len g1+j by A9,FINSEQ_1:25;
then g12.(i+len f1)=g2.i by A1,FINSEQ_1:def 7;
hence thesis by A1,A11,A12,FUNCT_1:def 7;
end;
A13: dom f1=dom g1 by A1,FINSEQ_3:29;
A14: g1"X c=g12X/\dom f1
proof
let x be object;
assume A15: x in g1"X;
then A16: x in dom g1 by FUNCT_1:def 7;
A17: g1.x in X by A15,FUNCT_1:def 7;
dom g1 c=dom g12 & g12.x=g1.x by A16,FINSEQ_1:26,def 7;
then x in g12X by A16,A17,FUNCT_1:def 7;
hence thesis by A13,A16,XBOOLE_0:def 4;
end;
len f12=len f1+len f2 & len g12=len g1+len g2 by FINSEQ_1:22;
then len g12<=len f12 by A1,A2,XREAL_1:6;
then A18: dom g12 c=dom f12 by A3,FINSEQ_1:5;
g12X/\dom f1 c=g1"X
proof
let x be object;
assume A19: x in g12X/\dom f1;
then x in g12X by XBOOLE_0:def 4;
then A20: g12.x in X by FUNCT_1:def 7;
A21: x in dom f1 by A19,XBOOLE_0:def 4;
then g12.x=g1.x by A13,FINSEQ_1:def 7;
hence thesis by A13,A21,A20,FUNCT_1:def 7;
end;
then g12X/\dom f1=g1"X by A14;
then A22: f1|g1"X=f1|g12X by RELAT_1:157;
dom f2=Seg len f2 & dom g2=Seg len g2 by FINSEQ_1:def 3;
then A23: dom g2 c=dom f2 by A2,FINSEQ_1:5;
g2"X c=Y/\dom f2
proof
let x be object;
assume A24: x in g2"X;
then A25: x in dom g2 by FUNCT_1:def 7;
then reconsider i=x as Nat;
A26: g2.x in X by A24,FUNCT_1:def 7;
A27: i+len g1 in dom g12 by A25,FINSEQ_1:28;
g12.(i+len g1)=g2.i by A25,FINSEQ_1:def 7;
then i+len g1 in g12X by A26,A27,FUNCT_1:def 7;
then A28: i+len g1 in g12X/\dom f12 by A18,A27,XBOOLE_0:def 4;
i>0 by A25,FINSEQ_3:25;
then i in Y by A1,A5,A28;
hence thesis by A23,A25,XBOOLE_0:def 4;
end;
then Y/\dom f2=g2"X by A6;
hence thesis by A4,A22,RELAT_1:157;
end;
theorem
for D be non empty set for M be Matrix of n,m,D holds
M-X is Matrix of n-'card(M"X),m,D
proof
let D be non empty set;
let M be Matrix of n,m,D;
A1: rng(M-X)c=rng M by FINSEQ_3:66;
rng M c=D* by FINSEQ_1:def 4;
then rng(M-X)c=D* by A1;
then reconsider MX=M-X as FinSequence of D* by FINSEQ_1:def 4;
A2: len MX=len M-card(M"X) by FINSEQ_3:59;
then len M >= card(M"X) by XREAL_1:49;
then
A3: len M=n & len MX=len M-' card(M"X) by A2,MATRIX_0:def 2,XREAL_1:233;
per cases;
suppose len MX=0;
then MX={};
hence thesis by A3,MATRIX_0:13;
end;
suppose len MX>0;
A4: for x be object st x in rng MX ex s be FinSequence st s=x & len s=m
proof
let x be object;
consider nn be Nat such that
A5: for x be object st x in rng M ex p be FinSequence of D st
x=p & len p=nn by MATRIX_0:9;
assume A6: x in rng MX;
then ex p be FinSequence of D st x=p & len p=nn by A1,A5;
then reconsider p=x as FinSequence of D;
len p=m by A1,A6,MATRIX_0:def 2;
hence thesis;
end;
then reconsider MX as Matrix of D by MATRIX_0:def 1;
now let p be FinSequence of D;
assume p in rng MX;
then ex s be FinSequence st s=p & len s=m by A4;
hence len p=m;
end;
hence thesis by A3,MATRIX_0:def 2;
end;
end;
theorem Th15:
for F be Function of Seg n,Seg n,D be non empty set
for M be Matrix of n,m,D for i st i in Seg width M
holds Col(M*F,i) = Col(M,i)*F
proof
let F be Function of Seg n,Seg n,D be non empty set;
let M be Matrix of n,m,D;
let i;
assume A1: i in Seg width M;
A2: len M=n by MATRIX_0:def 2;
then A3: dom M=Seg n by FINSEQ_1:def 3;
len Col(M,i)=n by A2,CARD_1:def 7;
then A4: dom Col(M,i)=Seg n by FINSEQ_1:def 3;
dom F=Seg n & rng F c=Seg n by FUNCT_2:52,RELAT_1:def 19;
then A5: dom(Col(M,i)*F)=Seg n by A4,RELAT_1:27;
A6: len(M*F)=n by MATRIX_0:def 2;
then A7: dom(M*F)=Seg n by FINSEQ_1:def 3;
A8: now let x be object;
assume A9: x in Seg n;
then reconsider j=x as Element of NAT;
Indices M=[:dom M,Seg width M:] by MATRIX_0:def 4;
then A10: [j,i] in Indices M by A1,A3,A9,ZFMISC_1:87;
A11: F.x in Seg n by A4,A5,A9,FUNCT_1:11;
then reconsider Fj=F.x as Element of NAT;
thus (Col(M,i)*F).x=Col(M,i).Fj by A5,A9,FUNCT_1:12
.=M*(Fj,i) by A3,A11,MATRIX_0:def 8
.=(M*F)*(j,i) by A10,MATRIX11:def 4
.=Col(M*F,i).x by A7,A9,MATRIX_0:def 8;
end;
len Col(M*F,i)=n by A6,CARD_1:def 7;
then dom Col(M*F,i)=Seg n by FINSEQ_1:def 3;
hence thesis by A5,A8,FUNCT_1:2;
end;
Lm1: for A be Matrix of n,m,K st(n=0 implies m=0) & the_rank_of A=n
ex B be Matrix of m-' n,m,K st the_rank_of(A^B)=m
proof
let A be Matrix of n,m,K;
set V=m-VectSp_over K,L=lines A;
assume that
A1: n=0 implies m=0 and
A2: the_rank_of A=n;
A3: len A=n by A1,MATRIX13:1;
L is linearly-independent by A2,MATRIX13:121;
then consider B be Subset of V such that
A4: L c= B and
a5: B is base by VECTSP_7:17;
A5: B is linearly-independent by a5,VECTSP_7:def 3;
A6: Lin(B)=the ModuleStr of V by a5,VECTSP_7:def 3;
reconsider B as finite Subset of V by A5,VECTSP_9:21;
B is Basis of V by A5,A6,VECTSP_7:def 3;
then A7: card B=dim V by VECTSP_9:def 1
.=m by MATRIX13:112;
width A=m by A1,MATRIX13:1;
then A8: m-n>=0 by A2,MATRIX13:74,XREAL_1:48;
then A9: m-n=m-' n by XREAL_0:def 2;
A10: A is without_repeated_line by A2,MATRIX13:121;
then A11: len A=card L by FINSEQ_4:62;
set BL=B\L;
consider p be FinSequence such that
A12: rng p=BL and
A13: p is one-to-one by FINSEQ_4:58;
reconsider p as FinSequence of V by A12,FINSEQ_1:def 4;
len p=card BL by A12,A13,FINSEQ_4:62
.=card B-card L by A4,CARD_2:44
.=m-' n by A3,A11,A7,A8,XREAL_0:def 2;
then reconsider P=FinS2MX p as Matrix of m-' n,m,K;
rng A misses rng P by A12,XBOOLE_1:79;
then A14: A^P is without_repeated_line by A10,A13,FINSEQ_3:91;
take P;
lines(A^P)=L\/rng P by FINSEQ_1:31
.=L\/B by A12,XBOOLE_1:39
.=B by A4,XBOOLE_1:12;
hence thesis by A5,A9,A14,MATRIX13:121;
end;
:: This will be a theorem in MATGRP_1
LmDet:
Det 1.(K, m) = 1_K
proof
per cases;
suppose m >= 1;
hence thesis by MATRIX_7:16;
end;
suppose m < 1;
then m = 0 by NAT_1:14;
then Det 1.(K, m) = 1.K by MATRIXR2:41;
hence thesis;
end;
end;
theorem Th16:
for A be Matrix of n,m,K st the_rank_of A = n
ex B be Matrix of m-' n,m,K st the_rank_of(A^B) = m
proof
let A be Matrix of n,m,K such that
A1: the_rank_of A=n;
per cases;
suppose A2: n=0;
then m-' n=m-n by XREAL_0:def 2;
then reconsider ONE=1.(K,m) as Matrix of m-' n,m,K by A2;
Det 1.(K,m) is non zero by LAPLACE:43;
then A3: the_rank_of ONE=m by MATRIX13:83;
len A=0 by A2,MATRIX_0:def 2;
then A is empty;
then A^ONE=ONE by FINSEQ_1:34;
hence thesis by A3;
end;
suppose n>0;
hence thesis by A1,Lm1;
end;
end;
theorem
for A be Matrix of n,m,K st the_rank_of A = m
ex B be Matrix of n,n-' m,K st the_rank_of(A^^B) = n
proof
let A be Matrix of n,m,K such that
A1: the_rank_of A=m;
A2: len A=n by MATRIX_0:def 2;
per cases;
suppose A3: m=0;
then n-' m=n-m by XREAL_0:def 2;
then reconsider ONE=1.(K,n) as Matrix of n,n-' m,K by A3;
A4: len 1.(K,n)=n by MATRIX_0:24;
Det 1.(K,n) is non zero by LAPLACE:43;
then A5: the_rank_of ONE=n by MATRIX13:83;
width A=m by A3,MATRIX13:1;
then A^^ONE=ONE by A2,A3,A4,MATRIX15:22;
hence thesis by A5;
end;
suppose A6: m>0;
n-m>=0 by A1,A2,MATRIX13:74,XREAL_1:48;
then A7: n-' m=n-m by XREAL_0:def 2;
A8: n>0 by A1,A2,A6,MATRIX13:74;
then A9: width A=m by MATRIX13:1;
per cases;
suppose A10: n=m;
take B=the Matrix of n,n-' m,K;
len B=n & width B=0 by A6,A7,A10,MATRIX_0:23;
hence thesis by A1,A2,A10,MATRIX15:22;
end;
suppose A11: n<>m;
A12: width(A@)=n by A2,A6,A9,MATRIX_0:54;
len(A@)=m by A6,A9,MATRIX_0:54;
then reconsider A1=A@ as Matrix of m,n,K by A12,MATRIX_0:51;
the_rank_of A1=m by A1,MATRIX13:84;
then consider B be Matrix of n-' m,n,K such that
A13: the_rank_of(A1^B)=n by Th16;
A14: n-' m<>0 by A7,A11;
then A15: width B=n by MATRIX13:1;
then A16: len(B@)=n by A8,MATRIX_0:54;
len B=n-' m by A14,MATRIX13:1;
then width(B@)=n-' m by A8,A15,MATRIX_0:54;
then reconsider B1=B@ as Matrix of n,n-' m,K by A16,MATRIX_0:51;
A1@=A by A2,A6,A8,A9,MATRIX_0:57;
then A17: (A1^B)@=A^^B1 by A12,A15,MATRLIN:28;
the_rank_of((A1^B)@)=n by A13,MATRIX13:84;
hence thesis by A17;
end;
end;
end;
reserve f,f1,f2 for n-element real-valued FinSequence,
p,p1,p2 for Point of TOP-REAL n,
M,M1,M2 for Matrix of n,m,F_Real,
A,B for Matrix of n,F_Real;
Lm2: f is Point of TOP-REAL n
proof
len f=n & @@f=f by CARD_1:def 7;
hence thesis by TOPREAL3:46;
end;
begin :: Linear Transformations of Euclidean Topological Spaces
:: given by a Transformation Matrix
definition
let n,m,M;
func Mx2Tran M -> Function of TOP-REAL n,TOP-REAL m means
:Def3:
it.f = Line(LineVec2Mx(@f)*M,1) if n <> 0 otherwise it.f = 0.TOP-REAL m;
existence
proof
set Tm=TOP-REAL m;
set Tn=TOP-REAL n;
A1: now
assume A2: n <> 0;
defpred P[Element of Tn,Element of Tm] means
$2=Line(LineVec2Mx(@$1)*M,1);
A3: for x being Element of Tn ex y being Element of Tm st P[x,y]
proof
let x be Element of Tn;
set L=LineVec2Mx(@x);
set LL=Line(L*M,1);
len x=n by CARD_1:def 7;
then A4: width L=n by MATRIX13:1;
len M=n & width M=m by A2,MATRIX13:1;
then width(L*M)=m by A4,MATRIX_3:def 4;
then LL in REAL m;
then reconsider LL as Element of Tm by EUCLID:22;
P[x,LL];
hence thesis;
end;
consider F being Function of Tn,Tm such that
A5: for x being Element of Tn holds P[x,F.x] from FUNCT_2:sch 3(A3);
take F;
let f;
(@f is FinSequence of REAL) & len f=n by CARD_1:def 7;
then f is Element of n-tuples_on REAL by FINSEQ_2:92;
then f in REAL n;
then f is Element of Tn by EUCLID:22;
hence F.f = Line(LineVec2Mx(@f)*M,1) by A5;
end;
now
assume n = 0;
defpred P[Element of Tn,Element of Tm] means $2=0.Tm;
A6: for x being Element of Tn ex y being Element of Tm st P[x,y];
consider F being Function of Tn,Tm such that
A7: for x being Element of Tn holds P[x,F.x] from FUNCT_2:sch 3(A6);
take F;
let f;
(@f is FinSequence of REAL) & len f=n by CARD_1:def 7;
then f is Element of n-tuples_on REAL by FINSEQ_2:92;
then f in REAL n;
then f is Element of Tn by EUCLID:22;
hence F.f = 0.Tm by A7;
end;
hence thesis by A1;
end;
uniqueness
proof
let F1,F2 be Function of TOP-REAL n,TOP-REAL m;
A8: now
assume n <> 0;
assume
A9: F1.f=Line(LineVec2Mx(@f)*M,1);
assume
A10: F2.f=Line(LineVec2Mx(@f)*M,1);
now let x be Element of TOP-REAL n;
thus F1.x=Line(LineVec2Mx(@x)*M,1) by A9
.=F2.x by A10;
end;
hence F1 = F2 by FUNCT_2:63;
end;
now assume n = 0;
assume
A11: F1.f = 0.TOP-REAL m;
assume
A12: F2.f = 0.TOP-REAL m;
now let x be Element of TOP-REAL n;
thus F1.x = 0.TOP-REAL m by A11 .= F2.x by A12;
end;
hence F1 = F2 by FUNCT_2:63;
end;
hence thesis by A8;
end;
correctness;
end;
Lm3: now let n,m,M;let x be object;
set T=Mx2Tran M;
per cases;
suppose A1: x in dom T;
A2: rng T c=the carrier of TOP-REAL m by RELAT_1:def 19;
T.x in rng T by A1,FUNCT_1:def 3;
hence T.x is real-valued FinSequence by A2;
end;
suppose not x in dom T;
hence T.x is real-valued FinSequence by FUNCT_1:def 2;
end;
end;
registration
let n,m,M;
let x be object;
cluster (Mx2Tran M).x -> Function-like Relation-like;
coherence by Lm3;
end;
registration
let n,m,M;
let x be object;
cluster (Mx2Tran M).x -> real-valued FinSequence-like;
coherence by Lm3;
end;
registration
let n,m,M,f;
cluster (Mx2Tran M).f -> m-element;
coherence
proof
set T=Mx2Tran M;
(@f is FinSequence of REAL) & len f=n by CARD_1:def 7;
then f is Element of n-tuples_on REAL by FINSEQ_2:92;
then f in REAL n;
then f in the carrier of TOP-REAL n by EUCLID:22;
then f in dom T by FUNCT_2:def 1;
then A1: T.f in rng T by FUNCT_1:def 3;
rng T c=the carrier of TOP-REAL m by RELAT_1:def 19;
hence thesis by A1;
end;
end;
theorem Th18:
1 <= i & i <= m & n <> 0 implies (Mx2Tran M).f.i = @f"*"Col(M,i)
proof
assume that
A1: 1<=i & i<=m and
A2: n<>0;
A3: len M=n by A2,MATRIX13:1;
set Lf=LineVec2Mx(@f);
set LfM=Lf*M;
len f=n by CARD_1:def 7;
then A4: width Lf=n by MATRIX13:1;
width M=m by A2,MATRIX13:1;
then A5: width LfM=m by A4,A3,MATRIX_3:def 4;
len Lf=1 by MATRIX13:1;
then len LfM=1 by A4,A3,MATRIX_3:def 4;
then A6: [1,i] in Indices LfM by A1,A5,MATRIX_0:30;
set LM=Line(LfM,1);
i in Seg m & (Mx2Tran M).f=LM by A1,A2,Def3;
hence (Mx2Tran M).f.i=LfM*(1,i) by A5,MATRIX_0:def 7
.=Line(Lf,1)"*"Col(M,i) by A4,A3,A6,MATRIX_3:def 4
.=@f"*"Col(M,i) by MATRIX15:25;
end;
theorem Th19:
len MX2FinS 1.(K,n) = n
proof
MX2FinS 1.(K,n) is OrdBasis of n-VectSp_over K by MATRLIN2:45;
hence len MX2FinS 1.(K,n)=dim(n-VectSp_over K) by MATRLIN2:21
.=n by MATRIX13:112;
end;
theorem Th20:
for Bn be OrdBasis of n-VectSp_over F_Real,
Bm be OrdBasis of m-VectSp_over F_Real st
Bn = MX2FinS 1.(F_Real,n) & Bm = MX2FinS 1.(F_Real,m)
for M1 be Matrix of len Bn,len Bm,F_Real st M1 = M
holds Mx2Tran M = Mx2Tran(M1,Bn,Bm)
proof
let Bn be OrdBasis of n-VectSp_over F_Real,
Bm be OrdBasis of m-VectSp_over F_Real such that
A1: Bn=MX2FinS 1.(F_Real,n) and
A2: Bm=MX2FinS 1.(F_Real,m);
set T=Mx2Tran M;
let M1 be Matrix of len Bn,len Bm,F_Real such that
A3: M1=M;
set Tb=Mx2Tran(M1,Bn,Bm);
dom Tb=the carrier of n-VectSp_over F_Real by FUNCT_2:def 1;
then A4: dom Tb =REAL n by MATRIX13:102
.=the carrier of TOP-REAL n by EUCLID:22;
A5: for x be object st x in dom T holds T.x=Tb.x
proof
let x be object;
assume x in dom T;
then reconsider v=x as Element of TOP-REAL n by FUNCT_2:def 1;
reconsider g=v as Vector of n-VectSp_over F_Real by A4,FUNCT_2:def 1;
set L=LineVec2Mx(@v);
len v=n by CARD_1:def 7;
then A6: len L=1 & width L=n by MATRIX13:1;
A7: len Bn=n by A1,Th19;
A8: len Bm=m by A2,Th19;
per cases;
suppose A9: n=0;
then Tb.g = 0.(m-VectSp_over F_Real) by A1,Th19,MATRLIN2:33
.= m |-> 0.F_Real by MATRIX13:102
.= 0* m
.= 0.TOP-REAL m by EUCLID:70
.= T.v by A9,Def3;
hence thesis;
end;
suppose A10: n>0;
A11: (Tb.g) |--Bm=Tb.g by A2,A8,MATRLIN2:46;
A12: g|--Bn=g & AutMt(Tb,Bn,Bm)=M by A1,A3,A7,MATRLIN2:36,46;
1 in dom L & len M=width L by A10,A6,FINSEQ_3:25,MATRIX13:1;
then LineVec2Mx(Line(L*M,1))=LineVec2Mx(Line(L,1))*M by MATRLIN2:35
.=L*M by MATRIX15:25
.=LineVec2Mx(Tb.g|--Bm) by A7,A10,A12,MATRLIN2:31;
hence Tb.x=Line(LineVec2Mx(Line(L*M,1)),1) by A11,MATRIX15:25
.=Line(L*M,1) by MATRIX15:25
.=T.x by A10,Def3;
end;
end;
dom T=the carrier of TOP-REAL n by FUNCT_2:def 1;
hence thesis by A4,A5,FUNCT_1:2;
end;
theorem
for P be Permutation of Seg n holds
(Mx2Tran M).f = (Mx2Tran(M*P)).(f*P) & f*P is n-element FinSequence of REAL
proof
let P be Permutation of Seg n;
A1: len f=n by CARD_1:def 7;
then A2: rng P=Seg n & dom f=Seg n by FINSEQ_1:def 3,FUNCT_2:def 3;
dom P=Seg n by FUNCT_2:52;
then A3: dom(f*P)=Seg n by A2,RELAT_1:27;
then reconsider fP=f*P as FinSequence by FINSEQ_1:def 2;
rng(f*P)=rng f by A2,RELAT_1:28;
then reconsider fP as FinSequence of REAL by FINSEQ_1:def 4;
A4: len fP=n by A1,A3,FINSEQ_1:def 3;
then A5: fP is n-element by CARD_1:def 7;
(Mx2Tran M).f = (Mx2Tran(M*P)).(f*P)
proof
per cases;
suppose A6: n<>0;
then A7: width M=m by MATRIX13:1;
set MP=M*P;
A8: len M=n by A6,MATRIX13:1;
A9: now let i be Nat;
assume A10: 1<=i & i<=m;
then i in Seg m;
then A11: mlt(@fP,Col(MP,i))=(the multF of F_Real).:(fP,Col(M,i)*P)
by A7,Th15
.=mlt(@f,Col(M,i))*P by FUNCOP_1:25;
len Col(M,i)=n by A8,CARD_1:def 7;
then len mlt(@f,Col(M,i))=n by A1,MATRIX_3:6;
then A12: dom mlt(@f,Col(M,i))=Seg n by FINSEQ_1:def 3;
(Mx2Tran MP).fP.i=@fP"*"Col(MP,i) by A6,A5,A10,Th18
.=(the addF of F_Real)"**"mlt(@fP,Col(MP,i));
hence (Mx2Tran MP).fP.i = @f"*"Col(M,i) by A12,A11,FINSOP_1:7
.=(Mx2Tran M).f.i by A6,A10,Th18;
end;
len((Mx2Tran M).f)=m & len((Mx2Tran MP).fP)=m by A5,CARD_1:def 7;
hence thesis by A9;
end;
suppose
A13: n = 0;
len fP = n by A4;
then card fP = n;
then
A14: fP is n-element FinSequence by CARD_1:def 7;
thus (Mx2Tran M).f = 0.TOP-REAL m by Def3,A13
.= (Mx2Tran(M*P)).fP by A13,Def3,A14
.= (Mx2Tran(M*P)).(f*P);
end;
end;
hence thesis by A4,CARD_1:def 7;
end;
theorem Th22:
(Mx2Tran M).(f1+f2) = (Mx2Tran M).f1 + (Mx2Tran M).f2
proof
set f12=f1+f2;
set T=Mx2Tran M;
per cases;
suppose A1: n<>0;
A4: len M=n by A1,MATRIX13:1;
set L2=LineVec2Mx@f2;
set L1=LineVec2Mx@f1;
A5: len L2=1 by MATRIX13:1;
A6: len f2=n by CARD_1:def 7;
then A7: width L2=n by MATRIX13:1;
A8: width M=m by A1,MATRIX13:1;
then A9: width(L2*M)=m by A7,A4,MATRIX_3:def 4;
A10: len f1=n by CARD_1:def 7;
then A11: width L1=n by MATRIX13:1;
then A12: width(L1*M)=m by A4,A8,MATRIX_3:def 4;
A13: len L1=1 by MATRIX13:1;
then a13: len(L1*M)=1 by A11,A4,MATRIX_3:def 4;
A15: @(T.f1)=Line(L1*M,1) & @(T.f2)=Line(L2*M,1) by A1,Def3;
B1: 1 in dom (L1*M) by a13,FINSEQ_3:25;
@f12=@f1+@f2 by RVSUM_1:def 4;
then (LineVec2Mx@f12)*M=(L1+L2)*M by A10,A6,MATRIX15:27
.=L1*M+L2*M by A13,A5,A11,A7,A4,MATRIX_4:63;
hence T.f12=Line(L1*M+L2*M,1) by A1,Def3
.=Line(L1*M,1)+Line(L2*M,1) by B1,A12,A9,MATRIX_4:59
.=T.f1+T.f2 by A15,RVSUM_1:def 4;
end;
suppose A16: n=0;
reconsider zz=0 as Real;
A17: 0.TOP-REAL m = 0* m by EUCLID:70 .= m |-> 0;
then A18: T.f2 = m |-> 0 by A16,Def3;
thus T.(f1+f2) = m |-> (zz+zz) by A16,A17,Def3
.= m |-> zz + m |-> zz by RVSUM_1:14
.= T.f1 + T.f2 by A16,A18;
end;
end;
reconsider zz=0 as Real;
theorem Th23:
(Mx2Tran M).(r*f) = r * ((Mx2Tran M).f)
proof
set rf=r*f;
set T=Mx2Tran M;
per cases;
suppose A1: n<>0;
per cases;
suppose A2: m=0;
then T.rf=0.REAL 0;
hence thesis by A2;
end;
suppose m>0;
reconsider R=r as Element of F_Real by XREAL_0:def 1;
set Lr=LineVec2Mx@rf;
set L=LineVec2Mx@f;
A3: R*@f=@rf by MATRIXR1:17;
len f=n by CARD_1:def 7;
then A4: width L=n by MATRIX13:1;
A5: len M=n by A1,MATRIX13:1;
len L=1 by MATRIX13:1;
then A6: len(L*M)=1 by A4,A5,MATRIX_3:def 4;
T.@f=Line(L*M,1) by A1,Def3;
hence r*(T.f)=R*Line(L*M,1) by MATRIXR1:17
.=Line(R*(L*M),1) by A6,MATRIXR1:20
.=Line((R*L)*M,1) by A4,A5,MATRIX15:1
.=Line(Lr*M,1) by A3,MATRIX15:29
.=T.(r*f) by A1,Def3;
end;
end;
suppose A7: n = 0;
A8: 0.TOP-REAL m = 0* m by EUCLID:70 .= m |-> 0;
hence T.rf = m |-> (r*zz) by A7,Def3
.= r * (m |-> zz) by RVSUM_1:48
.= r * T.f by A7,A8,Def3;
end;
end;
theorem Th24:
(Mx2Tran M).(f1-f2) = (Mx2Tran M).f1 - (Mx2Tran M).f2
proof
f1-f2=f1+-f2 by RVSUM_1:31
.=f1+(-1)*f2 by RVSUM_1:54;
hence (Mx2Tran M).(f1-f2)=(Mx2Tran M).f1+(Mx2Tran M).((-1)*f2) by Th22
.=(Mx2Tran M).f1+(-1)*(Mx2Tran M).f2 by Th23
.=(Mx2Tran M).f1+-(Mx2Tran M).f2 by RVSUM_1:54
.=(Mx2Tran M).f1-(Mx2Tran M).f2 by RVSUM_1:31;
end;
theorem
(Mx2Tran(M1+M2)).f = (Mx2Tran M1).f + (Mx2Tran M2).f
proof
set T12=Mx2Tran(M1+M2);
set T2=Mx2Tran M2;
set T1=Mx2Tran M1;
per cases;
suppose A1: n<>0;
set L=LineVec2Mx@f;
len f=n by CARD_1:def 7;
then A4: width L=n by MATRIX13:1;
A5: len M2=n & width M2=m by A1,MATRIX13:1;
then A6: width(L*M2)=m by A4,MATRIX_3:def 4;
A8: len M1=n by A1,MATRIX13:1;
A9: width M1=m by A1,MATRIX13:1;
then A10: width(L*M1)=m by A4,A8,MATRIX_3:def 4;
len L=1 by MATRIX13:1;
then len(L*M1)=1 by A4,A8,MATRIX_3:def 4; then
B1: 1 in dom (L*M1) by FINSEQ_3:25;
@(T1.f)=Line(L*M1,1) & @(T2.f)=Line(L*M2,1) by A1,Def3;
hence T1.f+T2.f=Line(L*M1,1)+Line(L*M2,1) by RVSUM_1:def 4
.=Line(L*M1+L*M2,1) by B1,A10,A6,MATRIX_4:59
.=Line(L*(M1+M2),1) by A4,A8,A9,A5,MATRIX_4:62
.=T12.f by A1,Def3;
end;
suppose A13: n=0;
A14: 0.TOP-REAL m = 0* m by EUCLID:70 .= m |-> 0;
then A15: T2.f = m |-> 0 by A13,Def3;
thus T12.f = m |-> (zz+zz) by A13,A14,Def3
.= m |-> zz + m |-> zz by RVSUM_1:14
.= T1.f + T2.f by A13,A14,A15,Def3;
end;
end;
theorem
r = R implies r * (Mx2Tran M).f = (Mx2Tran(R*M)).f
proof
set L=LineVec2Mx@f;
set RM=R*M;
set T=Mx2Tran M;
set TR=Mx2Tran RM;
assume
A1: r=R;
per cases;
suppose A2: n<>0;
A3: len M=n by A2,MATRIX13:1;
len f=n by CARD_1:def 7;
then A4: width L=n by MATRIX13:1;
len L=1 by MATRIX13:1;
then A5: len(L*M)=1 by A4,A3,MATRIX_3:def 4;
T.f=Line(L*M,1) by A2,Def3;
hence r*(T.f)=R*Line(L*M,1) by A1,MATRIXR1:17
.=Line(R*(L*M),1) by A5,MATRIXR1:20
.=Line(L*RM,1) by A4,A3,MATRIXR1:22
.=TR.f by A2,Def3;
end;
suppose A6: n=0;
A7: 0.TOP-REAL m = 0* m by EUCLID:70 .= m |-> 0;
hence r * T.f = r * (m |-> zz) by A6,Def3
.= m |-> (r*zz) by RVSUM_1:48
.= TR.f by A6,A7,Def3;
end;
end;
theorem Th27:
(Mx2Tran M).(p1+p2) = (Mx2Tran M).p1 + (Mx2Tran M).p2 by Th22;
theorem Th28:
(Mx2Tran M).(p1-p2) = (Mx2Tran M).p1-(Mx2Tran M).p2 by Th24;
theorem Th29:
(Mx2Tran M).0.TOP-REAL n = 0.TOP-REAL m
proof
set TRn=the Element of TOP-REAL n;
set MT=Mx2Tran M;
0.TOP-REAL n =TRn-TRn by RLVECT_1:5;
hence MT.0.TOP-REAL n=(MT.TRn)-(MT.TRn) by Th28
.=0.TOP-REAL m by RLVECT_1:5;
end;
theorem
for A be Subset of TOP-REAL n holds
(Mx2Tran M).:(p+A) = (Mx2Tran M).p + (Mx2Tran M).:A
proof
set TRn=TOP-REAL n;
set TRm=TOP-REAL m;
set MT=Mx2Tran M;
let A be Subset of TRn;
A1: dom MT=[#]TRn by FUNCT_2:def 1;
thus MT.:(p+A)c=MT.p+MT.:A
proof
let y be object;
assume y in MT.:(p+A);
then consider x be object such that
x in dom MT and
A2: x in p+A and
A3: MT.x=y by FUNCT_1:def 6;
x in {p+w where w is Element of TRn:w in A} by A2,RUSUB_4:def 8;
then consider w be Element of TRn such that
A4: x=p+w & w in A;
MT.w in MT.:A & MT.x=MT.p+MT.w by A1,A4,Th27,FUNCT_1:def 6;
then MT.x in {MT.p+u where u is Element of TRm:u in MT.:A};
hence thesis by A3,RUSUB_4:def 8;
end;
let y be object;
assume y in MT.p+MT.:A;
then y in {MT.p+u where u is Element of TRm:u in MT.:A} by RUSUB_4:def 8;
then consider u be Element of TRm such that
A5: y=MT.p+u and
A6: u in MT.:A;
consider w be object such that
w in dom MT and
A7: w in A and
A8: MT.w=u by A6,FUNCT_1:def 6;
reconsider w as Element of TRn by A7;
p+w in {p+L where L is Element of TRn:L in A} by A7;
then A9: p+w in p+A by RUSUB_4:def 8;
y =MT.(p+w) by A5,A8,Th27;
hence thesis by A1,A9,FUNCT_1:def 6;
end;
theorem
for A be Subset of TOP-REAL m holds
(Mx2Tran M)"(((Mx2Tran M).p)+A) = p + (Mx2Tran M)"A
proof
set MT=Mx2Tran M;
set TRn=TOP-REAL n;
set TRm=TOP-REAL m;
let A be Subset of TRm;
set w=p;
set MTw=MT.w;
A1: w+MT"A={w+v where v is Element of TRn:v in MT"A} by RUSUB_4:def 8;
A2: MTw+A={MTw+v where v is Element of TRm:v in A} by RUSUB_4:def 8;
A3: dom MT=[#]TRn by FUNCT_2:def 1;
hereby let x be object;
assume A4: x in MT"(MTw+A);
then reconsider f=x as Element of TRn;
MT.x in MTw+A by A4,FUNCT_1:def 7;
then consider v be Element of TRm such that
A5: MT.x=MTw+v and
A6: v in A by A2;
MT.f-MTw =(v+MTw)-MTw by A5
.=v+(MTw-MTw) by RLVECT_1:28
.=v+0.TRm by RLVECT_1:15
.=v by RLVECT_1:4;
then v=MT.(f-w) by Th28;
then A7: f-w in MT"A by A3,A6,FUNCT_1:def 7;
w+(f-w)=(f-w)+w
.=f-(w-w) by RLVECT_1:29
.=f-0.TRn by RLVECT_1:15
.=f by RLVECT_1:13;
hence x in w+MT"A by A1,A7;
end;
let x be object;
assume x in w+MT"A;
then consider v be Element of TRn such that
A8: x=w+v and
A9: v in MT"A by A1;
A10: MT.v in A by A9,FUNCT_1:def 7;
MT.(w+v)=MTw+MT.v by Th27;
then MT.x in MTw+A by A2,A8,A10;
hence thesis by A3,A8,FUNCT_1:def 7;
end;
theorem Th32:
for A be Matrix of n,m,F_Real,
B be Matrix of width A,k,F_Real st
(n = 0 implies m = 0) & (m = 0 implies k = 0)
holds (Mx2Tran B) * (Mx2Tran A) = Mx2Tran(A*B)
proof
let A be Matrix of n,m,F_Real,B be Matrix of width A,k,F_Real such that
A1: n=0 implies m=0 and
A2: m=0 implies k=0;
reconsider Bk=MX2FinS 1.(F_Real,k) as OrdBasis of k-VectSp_over F_Real
by MATRLIN2:45;
reconsider Bm=MX2FinS 1.(F_Real,m) as OrdBasis of m-VectSp_over F_Real
by MATRLIN2:45;
reconsider Bn=MX2FinS 1.(F_Real,n) as OrdBasis of n-VectSp_over F_Real
by MATRLIN2:45;
A3: len A=n by A1,MATRIX13:1;
A4: len Bk=k by Th19;
A5: len Bm=m by Th19;
A6: len Bn=n by Th19;
then reconsider A1=A as Matrix of len Bn,len Bm,F_Real by A5;
A7: Mx2Tran A=Mx2Tran(A1,Bn,Bm) by Th20;
A8: width A=m by A1,MATRIX13:1;
then A9: width B=k by A2,MATRIX13:1;
then reconsider AB=A*B as Matrix of len Bn,len Bk,F_Real by A3,A6,A4;
len Bm=m by Th19;
then reconsider B1=B as Matrix of len Bm,len Bk,F_Real by A8,A4;
A10: len B1=m by A2,A8,MATRIX13:1;
Mx2Tran(A*B)=Mx2Tran(AB,Bn,Bk) by A3,A9,Th20;
then Mx2Tran(A*B)=Mx2Tran(B1,Bm,Bk)*Mx2Tran(A1,Bn,Bm) by A8,A10,MATRLIN2:40;
hence thesis by A8,A7,Th20;
end;
theorem Th33:
Mx2Tran 1.(F_Real,n) = id TOP-REAL n
proof
set V=n-VectSp_over F_Real;
reconsider Bn=MX2FinS 1.(F_Real,n) as OrdBasis of V by MATRLIN2:45;
A1: len Bn=n by Th19;
then reconsider ONE=1.(F_Real,n) as Matrix of len Bn,len Bn,F_Real;
A2: Mx2Tran 1.(F_Real,n)=Mx2Tran(ONE,Bn,Bn) by Th20;
A3: [#]TOP-REAL n=dom Mx2Tran 1.(F_Real,n) by FUNCT_2:def 1
.=[#]V by A2,FUNCT_2:def 1;
thus Mx2Tran 1.(F_Real,n)
=Mx2Tran(AutMt(id V,Bn,Bn),Bn,Bn) by A1,Th20,MATRLIN2:28
.=id TOP-REAL n by A3,MATRLIN2:34;
end;
theorem Th34:
Mx2Tran M1 = Mx2Tran M2 implies M1 = M2
proof
assume that
A1: Mx2Tran M1=Mx2Tran M2;
set Vn=n-VectSp_over F_Real,Vm=m-VectSp_over F_Real;
reconsider Bn=MX2FinS 1.(F_Real,n) as OrdBasis of Vn by MATRLIN2:45;
reconsider Bm=MX2FinS 1.(F_Real,m) as OrdBasis of Vm by MATRLIN2:45;
A2: len Bm=m by Th19;
len Bn=n by Th19;
then reconsider A1=M1,B1=M2 as Matrix of len Bn,len Bm,F_Real by A2;
A3: Mx2Tran(A1,Bn,Bm)=Mx2Tran M1 by Th20
.=Mx2Tran(B1,Bn,Bm) by A1,Th20;
thus M1=AutMt(Mx2Tran(A1,Bn,Bm),Bn,Bm) by MATRLIN2:36
.=M2 by A3,MATRLIN2:36;
end;
theorem Th35:
for A be Matrix of n,m,F_Real,
B be Matrix of k,m,F_Real
holds
(Mx2Tran(A^B)).(f^(k|->0)) = (Mx2Tran A).f &
(Mx2Tran(B^A)).((k|->0)^f) = (Mx2Tran A).f
proof
let A be Matrix of n,m,F_Real,B be Matrix of k,m,F_Real;
reconsider k0=k|->In(0,REAL) as k-element FinSequence of REAL;
A1: len B=k by MATRIX_0:def 2;
set kf=k0^f;
per cases;
suppose A2: n<>0;
then A3: width A=m by MATRIX13:1;
A4: len f=n & len k0=k by CARD_1:def 7;
A5: len A=n by A2,MATRIX13:1;
thus(Mx2Tran(A^B)).(f^(k|->0))=(Mx2Tran A).f
proof
set fk=f^k0;
per cases;
suppose A6: k=0;
then B is empty by A1;
then A7: Mx2Tran(A^B)=Mx2Tran A by A6,FINSEQ_1:34;
k0 is empty by A6;
hence thesis by A7,FINSEQ_1:34;
end;
suppose A8: k<>0;
set Mab=Mx2Tran(A^B),Ma=Mx2Tran A;
A9: width B=m by A8,MATRIX_0:23;
A10: now let i;
reconsider S1=Sum mlt(@k0,Col(B,i)),S2=Sum mlt(@f,Col(A,i))
as Element of F_Real;
assume A11: 1<=i & i<=m;
then A12: i in Seg m;
mlt(@k0,Col(B,i))=(0.F_Real)*Col(B,i) by A1,FVSUM_1:66
.=k|->0.F_Real by A1,FVSUM_1:58;
then A13: Sum mlt(@k0,Col(B,i))=Sum(k|->0) by MATRPROB:36
.=0.(F_Real qua Field) by RVSUM_1:81;
A14: len Col(A,i)=n & len Col(B,i)=k by A5,A1,MATRIX_0:def 8;
mlt(@fk,Col(A^B,i))=mlt((@f)^(@k0),Col(A,i)^Col(B,i))
by A3,A9,A12,MATRLIN:26
.=mlt(@f,Col(A,i))^mlt(@k0,Col(B,i)) by A4,A14,MATRIX14:7;
then Sum(mlt(@fk,Col(A^B,i)))
=addreal.(Sum mlt(@f,Col(A,i)),Sum mlt(@k0,Col(B,i))) by FINSOP_1:5
.=Sum mlt(@f,Col(A,i))+Sum mlt(@k0,Col(B,i)) by BINOP_2:def 9
.=@f"*"Col(A,i) by A13;
hence Ma.f.i=@fk"*"Col(A^B,i) by A2,A11,Th18
.=Mab.fk.i by A2,A11,Th18;
end;
len(Mab.fk)=m & len(Ma.f)=m by CARD_1:def 7;
hence thesis by A10;
end;
end;
per cases;
suppose A15: k=0;
then B is empty by A1;
then A16: Mx2Tran(B^A)=Mx2Tran A by A15,FINSEQ_1:34;
k0 is empty by A15;
hence thesis by A16,FINSEQ_1:34;
end;
suppose A17: k<>0;
set Mba=Mx2Tran(B^A),Ma=Mx2Tran A;
A18: width B=m by A17,MATRIX_0:23;
A19: now let i;
reconsider S1=Sum mlt(@k0,Col(B,i)),S2=Sum mlt(@f,Col(A,i)) as
Element of F_Real;
assume A20: 1<=i & i<=m;
then A21: i in Seg m;
mlt(@k0,Col(B,i))=(0.F_Real)*Col(B,i) by A1,FVSUM_1:66
.=k|->0.F_Real by A1,FVSUM_1:58;
then A22: Sum mlt(@k0,Col(B,i))=Sum(k|->0) by MATRPROB:36
.=0.(F_Real qua Field) by RVSUM_1:81;
A23: len Col(A,i)=n & len Col(B,i)=k by A5,A1,MATRIX_0:def 8;
mlt(@kf,Col(B^A,i)) =mlt((@k0)^(@f),Col(B,i)^Col(A,i))
by A3,A18,A21,MATRLIN:26
.=mlt(@k0,Col(B,i))^mlt(@f,Col(A,i)) by A4,A23,MATRIX14:7;
then Sum(mlt(@kf,Col(B^A,i)))
=addreal.(Sum mlt(@k0,Col(B,i)),Sum mlt(@f,Col(A,i))) by FINSOP_1:5
.=Sum mlt(@f,Col(A,i))+0.F_Real by A22,BINOP_2:def 9
.=@f"*"Col(A,i);
hence Ma.f.i=@kf"*"Col(B^A,i) by A2,A20,Th18
.=Mba.kf.i by A2,A20,Th18;
end;
len(Mba.kf)=m & len(Ma.f)=m by CARD_1:def 7;
hence thesis by A19;
end;
end;
suppose A24: n=0;
A25: 0.TOP-REAL k = 0* k by EUCLID:70 .= k |-> 0;
f = {} by A24;
then A26: f^(k|->0) = k|->0 & (k|->0)^f = k|->0 by FINSEQ_1:34;
thus (Mx2Tran(A^B)).(f^(k|->0))
= 0.TOP-REAL m by A25,A26,Th29,A24
.= (Mx2Tran A).f by A24,Def3;
thus (Mx2Tran(B^A)).((k|->0)^f)
= 0.TOP-REAL m by A25,A26,Th29,A24
.= (Mx2Tran A).f by A24,Def3;
end;
end;
theorem
for A be Matrix of n,m,F_Real,
B be Matrix of k,m,F_Real
for g be k-element real-valued FinSequence holds
(Mx2Tran(A^B)).(f^g) = (Mx2Tran A).f+(Mx2Tran B).g
proof
A1: len f=n by CARD_1:def 7;
rng f c=REAL;
then f is FinSequence of REAL by FINSEQ_1:def 4;
then reconsider F=f,n0=n|->In(0,REAL)
as Element of n-tuples_on REAL by A1,FINSEQ_2:92;
let A be Matrix of n,m,F_Real,B be Matrix of k,m,F_Real;
let g be k-element real-valued FinSequence;
A2: len g=k by CARD_1:def 7;
rng g c=REAL;
then g is FinSequence of REAL by FINSEQ_1:def 4;
then reconsider G=g,k0=k|->In(0,REAL) as Element of k-tuples_on REAL
by A2,FINSEQ_2:92;
f=F+n0 by RVSUM_1:16;
then g=G+k0 & f=addreal.:(f,n0) by RVSUM_1:16,def 4;
then f^g=(addreal.:(F,n0))^(addreal.:(k0,G)) by RVSUM_1:def 4
.=addreal.:(F^k0,n0^G) by FINSEQOP:11
.=(F^k0)+(n0^G) by RVSUM_1:def 4;
hence (Mx2Tran(A^B)).(f^g)=(Mx2Tran(A^B)).(F^k0)+(Mx2Tran(A^B)).(n0^G)
by Th22
.=(Mx2Tran A).f+(Mx2Tran(A^B)).(n0^G) by Th35
.=(Mx2Tran A).f+(Mx2Tran B).g by Th35;
end;
theorem
for A be Matrix of n,k,F_Real,
B be Matrix of n,m,F_Real
st n = 0 implies k+m = 0
holds (Mx2Tran(A^^B)).f = (Mx2Tran A).f^(Mx2Tran B).f
proof
let A be Matrix of n,k,F_Real,B be Matrix of n,m,F_Real;
set L=LineVec2Mx(@f);
set MAB=(Mx2Tran(A^^B)).f,MA=(Mx2Tran A).f,MB=(Mx2Tran B).f;
A1: len MA=k by CARD_1:def 7;
assume A2: n=0 implies k+m=0;
then n=0 implies k=0;
then A3: width A=k by MATRIX13:1;
n=0 implies m=0 by A2;
then A4: width B=m by MATRIX13:1;
A5: len MB=m by CARD_1:def 7;
then A6: len(MA^MB)=k+m by A1,FINSEQ_1:22;
A7: for i st 1<=i & i<=k+m holds(MA^MB).i=MAB.i
proof
let i;
assume that
A8: 1<=i and
A9: i<=k+m;
A10: i in dom(MA^MB) by A6,A8,A9,FINSEQ_3:25;
A11: MAB.i=@f"*"Col(A^^B,i) by A2,A3,A4,A8,A9,Th18;
per cases by A10,FINSEQ_1:25;
suppose A12: i in dom MA;
then i<=k by A1,FINSEQ_3:25;
then A13: MA.i=@f"*"Col(A,i) by A2,A8,Th18;
i in Seg width A & (MA^MB).i=MA.i by A3,A1,A12,FINSEQ_1:def 3,def 7;
hence (MA^MB).i=MAB.i by A11,A13,MATRIX15:16;
end;
suppose ex j be Nat st j in dom MB & i=len MA+j;
then consider j be Nat such that
A14: j in dom MB and
A15: i=len MA+j;
1<=j & j<=m by A5,A14,FINSEQ_3:25;
then A16: MB.j=@f"*"Col(B,j) by A2,Th18;
j in Seg width B & (MA^MB).i=MB.j by A4,A5,A14,A15,FINSEQ_1:def 3,def 7;
hence (MA^MB).i=MAB.i by A3,A1,A11,A15,A16,MATRIX15:17;
end;
end;
len MAB=k+m by A3,A4,CARD_1:def 7;
hence thesis by A6,A7;
end;
theorem
M = 1.(F_Real,m) |n implies ((Mx2Tran M).f) |n = f
proof
set ONE=1.(F_Real,m);
assume A1: M=ONE|n;
per cases;
suppose A2: n=0;
then ((Mx2Tran M).f) |n is empty;
hence thesis by A2;
end;
suppose A3: n>0;
set TRm=TOP-REAL m;
set V=m-VectSp_over F_Real;
A4: len ONE=m by MATRIX_0:24;
A5: len f=n by CARD_1:def 7;
consider A be FinSequence such that
A6: ONE=M^A by A1,FINSEQ_1:80;
ONE=MX2FinS ONE;
then reconsider A as FinSequence of V by A6,FINSEQ_1:36;
set L=len A;
len M=n by A3,MATRIX13:1;
then n+L=m by A4,A6,FINSEQ_1:22;
then A7: f^(L|->0) is Element of TRm by Lm2;
set A1=FinS2MX A;
A8: (f^(L|->0)) |n=(f^(L|->0)) |dom f by A5,FINSEQ_1:def 3
.=f by FINSEQ_1:21;
(Mx2Tran(M^A1)).(f^(L|->0))=(Mx2Tran ONE).(f^(L|->0))
by A3,A4,A6,MATRIX13:1
.=(id TRm).(f^(L|->0)) by Th33
.=f^(L|->0) by A7;
hence thesis by A8,Th35;
end;
end;
begin :: Selected Properties of the Mx2Tran Operator
theorem Th39:
Mx2Tran M is one-to-one iff the_rank_of M = n
proof
set MM=Mx2Tran M;
per cases;
suppose A1: n=0 iff m=0;
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 Th19;
A3: len Bn=n by Th19;
then reconsider M1=M as Matrix of len Bn,len Bm,F_Real by A2;
A4: len M1=n by A1,MATRIX13:1;
A5: len Bm=m by Th19;
set T=Mx2Tran(M1,Bn,Bm);
A6: T is one-to-one iff ker T=(0).nV by MATRLIN2:43;
A7: width M1=m by A1,MATRIX13:1;
per cases;
suppose A8: m=0;
A9: the carrier of TOP-REAL 0 ={0.TOP-REAL 0} by EUCLID:22,77;
then rng MM c={0.TOP-REAL 0} by A8,RELAT_1:def 19;
then rng MM={0.TOP-REAL 0} by ZFMISC_1:33;
then card{0.TOP-REAL 0}=card{0.TOP-REAL 0} & MM is onto
by A8,A9,FUNCT_2:def 3;
hence thesis by A1,A4,A8,A9,MATRIX13:74,FINSEQ_4:63;
end;
suppose A10: m>0;
then reconsider SS=Space_of_Solutions_of(M1@) as Subspace of nV
by A4,A7,MATRIX_0:54;
A11: width(M1@)=n by A4,A7,A10,MATRIX_0:54;
hereby assume A12: Mx2Tran M is one-to-one;
[#]SS c={0.nV}
proof
let x be object;
assume A13: x in [#]SS;
then reconsider v=x as Vector of nV by VECTSP_4:10;
v=v|--Bn by A3,MATRLIN2:46;
then v|--Bn in SS by A13;
then v in ker T by A1,A3,A5,A10,MATRLIN2:41;
then v=0.nV by A6,A12,Th20,VECTSP_4:35;
hence thesis by TARSKI:def 1;
end;
then [#]SS={0.nV} by ZFMISC_1:33;
then SS=(0).nV by VECTSP_4:def 3;
then dim SS=0 by RANKNULL:16;
then 0=n-the_rank_of(M1@) by A1,A10,A11,MATRIX15:68;
hence the_rank_of M=n by MATRIX13:84;
end;
A14: the_rank_of(M1@)=the_rank_of M by MATRIX13:84;
assume the_rank_of M=n;
then dim SS=n-n by A1,A10,A11,A14,MATRIX15:68;
then A15: SS is trivial by MATRLIN2:42;
[#]ker T c={0.nV}
proof
let x be object;
assume A16: x in [#]ker T;
then reconsider v=x as Vector of nV by VECTSP_4:10;
v in ker T by A16;
then v|--Bn in SS by A1,A3,A5,A10,MATRLIN2:41;
then v in SS by A3,MATRLIN2:46;
then v in the carrier of SS;
then v=0.SS by A15;
then v=0.nV by VECTSP_4:11;
hence thesis by TARSKI:def 1;
end;
then [#]ker T={0.nV} by ZFMISC_1:33;
hence thesis by A6,Th20,VECTSP_4:def 3;
end;
end;
suppose A17: n=0 & m<>0;
A18: now
let x1,x2 be object such that
A19: x1 in dom MM & x2 in dom MM & MM.x1 = MM.x2;
A20: dom MM = [#]TOP-REAL 0 by A17,FUNCT_2:def 1
.= {0.TOP-REAL 0} by EUCLID:22,77;
hence x1 = 0.TOP-REAL 0 by A19,TARSKI:def 1
.= x2 by A19,A20,TARSKI:def 1;
end;
len M = n by MATRIX_0:def 2;
hence thesis by A18,A17,FUNCT_1:def 4,MATRIX13:74;
end;
suppose A21: n<>0 & m=0;
reconsider x1 = n |-> 1 as Point of TOP-REAL n by Lm2;
reconsider x2 = n |-> 2 as Point of TOP-REAL n by Lm2;
A22: dom MM = [#]TOP-REAL n by FUNCT_2:def 1;
A23: MM.x1 = 0.TOP-REAL 0 by A21 .=MM.x2 by A21;
A24: x1 <> x2
proof
assume A25: x1 = x2;
A26: x1 = (Seg n) --> 1 by FINSEQ_2:def 2
.= [:Seg n,{1}:] by FUNCOP_1:def 2;
x2 = (Seg n) --> 2 by FINSEQ_2:def 2
.= [:Seg n,{2}:] by FUNCOP_1:def 2;
then {1} = {2} by A25,A26,A21,ZFMISC_1:110;
then 2 in {1} by TARSKI:def 1;
hence contradiction by TARSKI:def 1;
end;
width M = m by A21,MATRIX13:1;
hence thesis by A24,A21,A23,A22,FUNCT_1:def 4,MATRIX13:74;
end;
end;
theorem Th40:
Mx2Tran A is one-to-one iff Det A <> 0.F_Real
proof
Mx2Tran A is one-to-one iff the_rank_of A=n by Th39;
hence thesis by MATRIX13:83;
end;
theorem Th41:
Mx2Tran M is onto iff the_rank_of M = m
proof
set MM=Mx2Tran M;
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;
A1: [#]mV =REAL m by MATRIX13:102
.=[#]TOP-REAL m by EUCLID:22;
A2: len Bm=m by Th19;
len Bn=n by Th19;
then reconsider M1=M as Matrix of len Bn,len Bm,F_Real by A2;
set T=Mx2Tran(M1,Bn,Bm);
A3: dom T=[#]nV by FUNCT_2:def 1;
A4: [#]im T=T.:[#]nV by RANKNULL:def 2
.=rng T by A3,RELAT_1:113;
A5: MM=T by Th20;
hereby assume MM is onto;
then [#]im T=[#](Omega).mV by A5,A1,A4,FUNCT_2:def 3;
then rank T=dim(Omega).mV by VECTSP_4:29
.=m by MATRIX13:112;
hence the_rank_of M=m by MATRLIN2:49;
end;
A6: dim mV=m by MATRIX13:112;
assume the_rank_of M=m;
then m=rank T by MATRLIN2:49
.=dim im T;
then (Omega).(im T)=(Omega).mV by A6,VECTSP_9:28;
hence thesis by A5,A1,A4,FUNCT_2:def 3;
end;
theorem Th42:
Mx2Tran A is onto iff Det A <> 0.F_Real
proof
Mx2Tran A is onto iff the_rank_of A=n by Th41;
hence thesis by MATRIX13:83;
end;
theorem Th43:
for A,B st Det A <> 0.F_Real holds (Mx2Tran A)" = Mx2Tran B iff A~ = B
proof
A1: n=0 implies n=0;
let A,B such that
A2: Det A<>0.F_Real;
Det A is non zero by A2;
then Det A is unital; then
A3: A is invertible by LAPLACE:34;
set MA=Mx2Tran A,MB=Mx2Tran B;
A4: width B=n by MATRIX_0:24;
reconsider ma=MA,mb=MB as Function;
A5: width A=n & len A=n by MATRIX_0:24;
A6: MA is one-to-one by A2,Th40;
hereby assume MA"=MB;
then A7: mb*ma=id dom ma by A6,FUNCT_1:39
.=id TOP-REAL n by FUNCT_2:def 1
.=Mx2Tran 1.(F_Real,n) by Th33;
MB*MA=Mx2Tran(A*B) by A5,A4,A1,Th32;
then B is_reverse_of A by A3,A7,Th34,MATRIX_6:38;
hence A~=B by A3,MATRIX_6:def 4;
end;
assume A8: A~=B;
MA is onto by A2,Th42;
then A9: dom MB=[#]TOP-REAL n & rng MA=[#]TOP-REAL n by FUNCT_2:def 1,def 3;
A10: n in NAT by ORDINAL1:def 12;
MB*MA=Mx2Tran(A*B) by A5,A4,A1,Th32
.=Mx2Tran 1.(F_Real,n) by A3,A10,A8,MATRIX14:18
.=id TOP-REAL n by Th33
.=id dom MA by FUNCT_2:def 1;
hence thesis by A6,A9,FUNCT_1:41;
end;
Lm4: for f be n-element real-valued FinSequence
ex L be m-element FinSequence of REAL st |.(Mx2Tran M).f.|<=Sum L*|.f.| &
for i be Nat st i in dom L holds L.i=|.@Col(M,i).|
proof
let f be n-element real-valued FinSequence;
set Lf=LineVec2Mx(@f);
set LfM=Lf*M;
set LM=Line(LfM,1);
deffunc L(Nat)=|.@Col(M,$1).|;
consider L be FinSequence such that
A1: len L=m & for k be Nat st k in dom L holds L.k=L(k) from FINSEQ_1:sch 2;
rng L c=REAL
proof
let y be object;
assume y in rng L;
then consider x be object such that
A2: x in dom L and
A3: L.x=y by FUNCT_1:def 3;
reconsider x as Nat by A2;
L.x=L(x) by A1,A2;
hence thesis by A3,XREAL_0:def 1;
end;
then L is FinSequence of REAL by FINSEQ_1:def 4;
then reconsider L1=L as Element of m-tuples_on REAL by A1,FINSEQ_2:92;
take L1;
per cases;
suppose A4: n<>0; then
A5: len M=n by MATRIX13:1;
(Mx2Tran M).f=LM by A4,Def3;
then A6: len LM=m by CARD_1:def 7;
A7: |.(Mx2Tran M).f.|=sqrt Sum sqr@LM by A4,Def3;
reconsider LM as Element of m-tuples_on REAL by A6,FINSEQ_2:92;
len(abs LM)=m by CARD_1:def 7;
then reconsider aLM=abs LM as Element of m-tuples_on REAL by FINSEQ_2:92;
A8: len f=n by CARD_1:def 7;
then A9: width Lf=n by MATRIX13:1;
width M=m by A4,MATRIX13:1;
then A10: width LfM=m by A5,A9,MATRIX_3:def 4;
len Lf=1 by MATRIX13:1;
then A11: len LfM=1 by A5,A9,MATRIX_3:def 4;
now let i be Nat;
A12: len Col(M,i)=n by A5,MATRIX_0:def 8;
then A13: |.|(f,@Col(M,i))|.|<=|.f.|*L(i) by A8,EUCLID_2:15;
assume A14: i in Seg m;
then A15: 1<=i & i<=m by FINSEQ_1:1;
then A16: [1,i] in Indices LfM by A11,A10,MATRIX_0:30;
i in dom L by A1,A15,FINSEQ_3:25;
then A17: L.i=L(i) by A1;
LM.i=LfM*(1,i) by A10,A14,MATRIX_0:def 7
.=Line(Lf,1)"*"Col(M,i) by A5,A9,A16,MATRIX_3:def 4
.=Sum(mlt(@f,Col(M,i))) by MATRIX15:25
.=Sum mlt(f,@Col(M,i)) by A8,A12,MATRPROB:35,36
.=|(f,@Col(M,i))| by RVSUM_1:def 16;
then aLM.i<=|.f.|*L(i) by A13,VALUED_1:18;
hence (aLM).i<=(|.f.|*L1).i by A17,RVSUM_1:44;
end;
then A18: Sum aLM<=Sum(|.f.|*L1) by RVSUM_1:82;
sqr LM=LM(#)LM by VALUED_1:def 8;
then sqrt Sum(sqr LM)<=Sum sqrt(sqr LM) by Th5;
then Sum(|.f.|*L1)=|.f.|*Sum L1 & sqrt Sum(sqr LM)<=Sum aLM by Th4,
RVSUM_1:87;
hence thesis by A7,A1,A18,XXREAL_0:2;
end;
suppose A19: n=0;
now let i be Nat;
assume i in dom L1;
then L1.i = |.@Col(M,i).| by A1;
hence 0 <= L1.i;
end;
then A20: Sum L1 >= 0 by RVSUM_1:84;
|.(Mx2Tran M).f.| = |.0.TOP-REAL m.| by A19,Def3
.= 0 by EUCLID_2:39;
hence thesis by A1,A20;
end;
end;
theorem Th44:
ex L be m-element FinSequence of REAL st
(for i st i in dom L holds L.i=|.@Col(M,i).|) &
for f holds|.(Mx2Tran M).f.|<=Sum L*|.f.|
proof
set F=the n-element real-valued FinSequence;
consider L be m-element FinSequence of REAL such that
|.(Mx2Tran M).F.|<=Sum L*|.F.| and
A1: for i be Nat st i in dom L holds L.i=|.@Col(M,i).| by Lm4;
take L;
thus for i st i in dom L holds L.i=|.@Col(M,i).| by A1;
let f be n-element real-valued FinSequence;
consider L1 be m-element FinSequence of REAL such that
A2: |.(Mx2Tran M).f.|<=Sum L1*|.f.| and
A3: for i be Nat st i in dom L1 holds L1.i=|.@Col(M,i).| by Lm4;
len L1=m & len L=m by CARD_1:def 7;
then A4: dom L=dom L1 by FINSEQ_3:29;
now let i be Nat;
assume A5: i in dom L;
hence L.i=|.@Col(M,i).| by A1
.=L1.i by A3,A4,A5;
end;
hence thesis by A2,A4,FINSEQ_1:13;
end;
theorem Th45:
ex L be Real st L>0 & for f holds |.(Mx2Tran M).f.| <= L*|.f.|
proof
consider L be m-element FinSequence of REAL such that
A1: for i st i in dom L holds L.i=|.@Col(M,i).| and
A2: for f be n-element real-valued FinSequence
holds|.(Mx2Tran M).f.|<=Sum L*|.f.| by Th44;
reconsider S1 = 1+Sum L as Real;
take S1;
now let i;
assume i in dom L;
then L.i=|.@Col(M,i).| by A1;
hence 0<=L.i;
end;
then Sum L>=0 by RVSUM_1:84;
hence S1>0;
let f;
Sum L<=S1 by XREAL_1:29;
then A3: Sum L*|.f.|<=S1*|.f.| by XREAL_1:64;
|.(Mx2Tran M).f.|<=Sum L*|.f.| by A2;
hence thesis by A3,XXREAL_0:2;
end;
reconsider jj=1 as Real;
theorem
the_rank_of M = n implies
ex L be Real st L > 0 & for f holds |.f.| <= L*|.(Mx2Tran M).f.|
proof
assume that
A1: the_rank_of M=n;
per cases;
suppose A2: n<>0;
consider N be Matrix of m-' n,m,F_Real such that
A3: the_rank_of(M^N)=m by A1,Th16;
width M=m by A2,MATRIX13:1;
then m-n>=0 by A1,MATRIX13:74,XREAL_1:48;
then A4: m-n=m-' n by XREAL_0:def 2;
then reconsider MN=M^N as Matrix of m,F_Real;
A5: dom id TOP-REAL m=[#]TOP-REAL m;
set mn=(m-' n) |->0;
A6: m=0 iff m=0;
sqr mn=(m-' n) |->((0 qua Real)^2) by RVSUM_1:56
.=(m-' n) |->(0*0);
then A7: Sum sqr mn=(m-' n)*(0 qua Nat) by RVSUM_1:80;
set MN1=MN~;
consider L be Real such that
A8: L>0 and
A9: for f be m-element real-valued FinSequence holds
|.(Mx2Tran MN1).f.|<=L*|.f.| by Th45;
take L;
thus L>0 by A8;
let f be n-element real-valued FinSequence;
set fm=f^mn;
set Mfm=(Mx2Tran MN).fm;
A10: Mfm =(Mx2Tran M).f by A4,Th35;
Det MN<>0.F_Real by A3,MATRIX13:83;
then Det MN is non zero;
then Det MN is unital;
then A11: MN is invertible by LAPLACE:34;
A12: width MN = m by MATRIX_0:24;
reconsider MN2=MN1 as Matrix of width MN,m,F_Real
by A12;
A13: width MN1=m & len MN=m by MATRIX_0:24;
A14: (Mx2Tran MN1)*(Mx2Tran MN)=(Mx2Tran MN2)*(Mx2Tran MN) by MATRIX_0:24
.=Mx2Tran(MN*MN2) by A6,Th32
.=Mx2Tran 1.(F_Real,m) by A11,A13,MATRIX14:18
.=id TOP-REAL m by Th33;
sqr fm=sqr f^sqr mn by RVSUM_1:144;
then Sum sqr fm=Sum sqr f+Sum sqr mn by RVSUM_1:75
.=Sum sqr f by A7;
then A15: |.fm.| =|.f.|;
A16: fm is Point of TOP-REAL m by A4,Lm2;
then fm=(id TOP-REAL m).fm
.=(Mx2Tran MN1).Mfm by A16,A14,A5,FUNCT_1:12;
hence thesis by A9,A10,A15;
end;
suppose A17: n=0;
A18: |. 0*n .| = 0 by EUCLID:7;
take L=jj;
thus thesis by A17,A18;
end;
end;
theorem Th47:
Mx2Tran M is continuous
proof
set Tn=TOP-REAL n;
set Tm=TOP-REAL m;
set TM=Mx2Tran M;
consider L be Real such that
A1: L>0 and
A2: for f be n-element real-valued FinSequence holds|.TM.f.|<=L*|.f.|
by Th45;
let x being Point of Tn,U being a_neighborhood of TM.x;
reconsider TMx=TM.x as Point of Tm;
reconsider tmx=TMx as Point of Euclid m by EUCLID:67;
reconsider X=x as Point of Euclid n by EUCLID:67;
tmx in Int(U) by CONNSP_2:def 1;
then consider r be Real such that
A3: r>0 and
A4: Ball(tmx,r)c=U by GOBOARD6:5;
reconsider B=Ball(X,r/L) as Subset of Tn by EUCLID:67;
r/L>0 by A3,A1,XREAL_1:139;
then x in Int B by GOBOARD6:5;
then reconsider Bx=B as a_neighborhood of x by CONNSP_2:def 1;
take Bx;
let y be object;
assume y in TM.:Bx;
then consider p be object such that
p in dom TM and
A5: p in Bx and
A6: TM.p=y by FUNCT_1:def 6;
reconsider p as Point of Tn by A5;
A7: r/L*L=r by A1,XCMPLX_1:87;
reconsider TMp=TM.p as Point of Tm;
reconsider tmp=TMp as Point of Euclid m by EUCLID:67;
dist(tmx,tmp)=|.TM.x-TM.p.| by SPPOL_1:39
.=|.TM.(x-p).| by Th28;
then A8: dist(tmx,tmp)<=L*|.x-p.| by A2;
reconsider P=p as Point of Euclid n by EUCLID:67;
dist(X,P)<r/L by A5,METRIC_1:11;
then A9: dist(X,P)*L<r/L*L by A1,XREAL_1:68;
dist(X,P)=|.x-p.| by SPPOL_1:39;
then dist(tmx,tmp)<r by A9,A7,A8,XXREAL_0:2;
then tmp in Ball(tmx,r) by METRIC_1:11;
hence thesis by A4,A6;
end;
registration
let n,K;
cluster invertible for Matrix of n,K;
existence
proof
1.(K,n) is invertible;
hence thesis;
end;
end;
registration
let n;
let A be invertible Matrix of n,F_Real;
cluster Mx2Tran A -> being_homeomorphism;
coherence
proof
set T=Mx2Tran A;
A1: (T is continuous) & Mx2Tran(A~) is continuous by Th47;
A2: Det A<>0.F_Real by LAPLACE:43;
then A3: T"=Mx2Tran(A~) by Th43;
A4: T is onto one-to-one by A2,Th40,Th42;
then A5: rng T=[#]TOP-REAL n by FUNCT_2:def 3;
dom T=[#]TOP-REAL n & T/"=T" by A4,FUNCT_2:def 1,TOPS_2:def 4;
hence thesis by A4,A3,A1,A5,TOPS_2:def 5;
end;
end;