P;
then 0.K = Det(IP,IN)][(JP,JN) by A9,A11,A10,Th45
.= IP*JN-IN*JP by MATRIX_9:13;
hence thesis by VECTSP_1:19;
end;
suppose
I>J & NJ & N>P;
then 0.K = Det(JP,JN)][(IP,IN) by A9,A11,A10,Th45
.= JP*IN-JN*IP by MATRIX_9:13;
hence thesis by VECTSP_1:19;
end;
end;
end;
assume that
A12: ex i,j st [i,j] in Indices M & M*(i,j) <> 0.K and
A13: for i,j,n,m st [:{i,j},{n,m}:] c= Indices M holds M*(i,n)*(M*(j,m))
=M*(i,m)*(M*(j,n));
now
let i0,j0,n0,m0 such that
A14: i0<>j0 and
A15: n0<>m0 and
A16: [:{i0,j0},{n0,m0}:] c= Indices M;
A17: card {i0,j0}=2 by A14,CARD_2:57;
set JM=M*(j0,m0);
set JN=M*(j0,n0);
set IM=M*(i0,m0);
set IN=M*(i0,n0);
A18: IN*JM=IM*JN by A13,A16;
card {n0,m0}=2 by A15,CARD_2:57;
then
A19: EqSegm(M,{i0,j0},{n0,m0})=Segm(M,{i0,j0},{n0,m0}) by A17,Def3;
per cases by A14,A15,XXREAL_0:1;
suppose
i0m0;
then EqSegm(M,{i0,j0},{n0,m0} )= (IM,IN)][(JM,JN) by A19,Th45;
hence Det EqSegm(M,{i0,j0},{n0,m0}) = IM*JN-IN*JM by A17,MATRIX_9:13
.= 0.K by A18,VECTSP_1:19;
end;
suppose
i0>j0 & n0j0 & n0>m0;
then EqSegm(M,{i0,j0},{n0,m0})=(JM,JN)][(IM,IN) by A19,Th45;
hence Det EqSegm(M,{i0,j0},{n0,m0}) = JM*IN-JN*IM by A17,MATRIX_9:13
.= 0.K by A18,VECTSP_1:19;
end;
end;
hence thesis by A12,Th96;
end;
theorem
the_rank_of M = 1 iff ex i st i in Seg len M & (ex j st j in Seg width
M & M*(i,j) <> 0.K) & for k st k in Seg len M ex a st Line(M,k) =a*Line(M,i)
proof
A1: Indices M=[:Seg len M,Seg width M:] by FINSEQ_1:def 3;
thus the_rank_of M = 1 implies ex i st i in Seg len M & (ex j st j in Seg
width M & M*(i,j) <> 0.K) & for k st k in Seg len M ex a st Line(M,k) = a*Line(
M,i)
proof
assume
A2: the_rank_of M = 1;
then consider i,j such that
A3: [i,j] in Indices M and
A4: M*(i,j) <> 0.K by Th97;
take i;
A5: j in Seg width M by A3,ZFMISC_1:87;
hence
i in Seg len M & ex j st j in Seg width M & M*(i,j) <> 0.K by A1,A3,A4,
ZFMISC_1:87;
set Li=Line(M,i);
set ij=M*(i,j);
let k such that
A6: k in Seg len M;
set Lk=Line(M,k);
set kj=M*(k,j);
take a=kj * ij";
A7: i in Seg len M by A1,A3,ZFMISC_1:87;
A8: now
let n such that
A9: 1<=n and
A10: n<=width M;
A11: n in Seg width M by A9,A10;
then
A12: {j,n} c= Seg width M by A5,ZFMISC_1:32;
Li.n = M*(i,n) by A11,MATRIX_0:def 7;
then
A13: (a*Li).n=a*(M*(i,n)) by A11,FVSUM_1:51;
A14: kj = kj * 1_K
.= kj * (ij * ij") by A4,VECTSP_1:def 10
.= a * ij by GROUP_1:def 3;
{i,k} c= Seg len M by A7,A6,ZFMISC_1:32;
then [:{i,k},{j,n}:] c= Indices M by A1,A12,ZFMISC_1:96;
then
A15: ij*(M*(k,n)) = a*ij *(M*(i,n)) by A2,A14,Th97
.= ij * (a * (M*(i,n))) by GROUP_1:def 3;
Lk.n=M*(k,n) by A11,MATRIX_0:def 7;
hence Lk.n=(a*Li).n by A4,A15,A13,VECTSP_2:8;
end;
A16: len (a*Li)=width M by CARD_1:def 7;
len Lk=width M by CARD_1:def 7;
hence thesis by A16,A8;
end;
given i such that
A17: i in Seg len M and
A18: ex j st j in Seg width M & M*(i,j) <> 0.K and
A19: for k st k in Seg len M ex a st Line(M,k) = a*Line(M,i);
A20: now
set Li=Line(M,i);
let I,J,n,m be Nat such that
A21: [:{I,J},{n,m}:]c=Indices M;
A22: {n,m} c= Seg width M by A21,ZFMISC_1:114;
then
A23: n in Seg width M by ZFMISC_1:32;
then
A24: Li.n=M*(i,n) by MATRIX_0:def 7;
set LJ=Line(M,J);
set LI=Line(M,I);
A25: {I,J} c= Seg len M by A1,A21,ZFMISC_1:114;
then I in Seg len M by ZFMISC_1:32;
then consider a such that
A26: LI = a*Li by A19;
J in Seg len M by A25,ZFMISC_1:32;
then consider b such that
A27: LJ = b*Li by A19;
LJ.n=M*(J,n) by A23,MATRIX_0:def 7;
then
A28: M*(J,n)= b * (M*(i,n)) by A27,A23,A24,FVSUM_1:51;
A29: m in Seg width M by A22,ZFMISC_1:32;
then
A30: Li.m=M*(i,m) by MATRIX_0:def 7;
LJ.m=M*(J,m) by A29,MATRIX_0:def 7;
then
A31: M*(J,m)= b *(M*(i,m)) by A27,A29,A30,FVSUM_1:51;
LI.m=M*(I,m) by A29,MATRIX_0:def 7;
then
A32: M*(I,m)= a * (M*(i,m)) by A26,A29,A30,FVSUM_1:51;
LI.n=M*(I,n) by A23,MATRIX_0:def 7;
then M*(I,n)= a * (M*(i,n)) by A26,A23,A24,FVSUM_1:51;
hence M*(I,n) * (M*(J,m)) = (a * (M*(i,n)) * b) * (M*(i,m)) by A31,
GROUP_1:def 3
.= (b *(M*(i,n)) * a) * (M*(i,m)) by GROUP_1:def 3
.= M*(I,m) * (M*(J,n)) by A28,A32,GROUP_1:def 3;
end;
consider j such that
A33: j in Seg width M and
A34: M*(i,j) <> 0.K by A18;
[i,j] in Indices M by A1,A17,A33,ZFMISC_1:87;
hence thesis by A34,A20,Th97;
end;
registration
let K;
cluster diagonal for Matrix of K;
existence
proof
set E = the diagonal Matrix of 1,K;
take E;
thus thesis;
end;
end;
theorem Th99:
for M be diagonal Matrix of K for NonZero1 be set st NonZero1 = {i
where i is Element of NAT:[i,i] in Indices M & M*(i,i)<>0.K} for P,Q st [:P,Q:]
c= Indices M & card P = card Q & Det EqSegm(M,P,Q)<>0.K holds P c= NonZero1 & Q
c= NonZero1
proof
let M be diagonal Matrix of K;
let NonZero1 be set such that
A1: NonZero1={i where i is Element of NAT:[i,i] in Indices M&M*(i,i)<>0.K };
let P,Q such that
A2: [:P,Q:] c= Indices M and
A3: card P = card Q and
A4: Det EqSegm(M,P,Q)<>0.K;
set S=Segm(M,P,Q);
set SQ=Sgm Q;
set SP=Sgm P;
set ES=EqSegm(M,P,Q);
A5: Indices S=[:Seg len S,Seg width S:] by FINSEQ_1:def 3;
A6: ES=S by A3,Def3;
thus P c= NonZero1
proof
assume not P c= NonZero1;
then consider x being object such that
A7: x in P and
A8: not x in NonZero1;
A9: P c= Seg len M by A2,A3,Th67;
then
A10: rng SP=P by FINSEQ_1:def 13;
then consider y being object such that
A11: y in dom SP and
A12: SP.y=x by A7,FUNCT_1:def 3;
reconsider x,y as Element of NAT by A7,A11;
set L=Line(S,y);
A13: dom SP=Seg card P by A9,FINSEQ_3:40;
Q c= Seg width M by A2,A3,Th67;
then
A14: rng SQ=Q by FINSEQ_1:def 13;
A15: now
let i such that
A16: 1<=i and
A17: i<=width S;
A18: i in Seg width S by A16,A17;
then
A19: L.i=S*(y,i) by MATRIX_0:def 7;
y in Seg len S by A3,A13,A11,MATRIX_0:24;
then
A20: [y,i] in Indices S by A5,A18,ZFMISC_1:87;
then
A21: S*(y,i)=M*(x,SQ.i) by A12,Def1;
A22: 0.K*0.K=0.K;
A23: SQ.i<>x or SQ.i=x;
[x,SQ.i] in Indices M by A2,A10,A14,A12,A20,Th17;
then L.i=0.K by A1,A8,A21,A19,A23,MATRIX_1:def 6;
hence L.i=(0.K*L).i by A18,A22,FVSUM_1:51;
end;
A24: len L=width S by MATRIX_0:def 7;
len L=len (0.K* L) by MATRIXR1:16;
then Line(S,y) = 0.K*Line(S,y) by A24,A15;
then
A25: Det(RLine(ES,y,Line(ES,y))) = 0.K*Det(ES) by A6,A13,A11,MATRIX11:35;
RLine(ES,y,Line(ES,y))=ES by MATRIX11:30;
hence thesis by A4,A25;
end;
A26: dom S=Seg len S by FINSEQ_1:def 3;
A27: len S=card P by A3,MATRIX_0:24;
A28: width S=card P by A3,MATRIX_0:24;
thus Q c= NonZero1
proof
A29: Q c= Seg width M by A2,A3,Th67;
then
A30: dom SQ=Seg card Q by FINSEQ_3:40;
assume not Q c= NonZero1;
then consider x being object such that
A31: x in Q and
A32: not x in NonZero1;
A33: rng SQ=Q by A29,FINSEQ_1:def 13;
then consider y being object such that
A34: y in dom SQ and
A35: SQ.y=x by A31,FUNCT_1:def 3;
reconsider x,y as Element of NAT by A31,A34;
set C=Col(ES,y);
P c= Seg len M by A2,A3,Th67;
then
A36: rng SP=P by FINSEQ_1:def 13;
now
let k be Element of NAT such that
A37: k in Seg card P;
A38: S*(k,y)=C.k by A6,A27,A26,A37,MATRIX_0:def 8;
A39: [k,y] in Indices S by A3,A5,A27,A28,A30,A34,A37,ZFMISC_1:87;
then
A40: S*(k,y)=M*(SP.k,x) by A35,Def1;
A41: SP.k<>x or SP.k=x;
[SP.k,x] in Indices M by A2,A36,A33,A35,A39,Th17;
hence C.k=0.K by A1,A32,A40,A38,A41,MATRIX_1:def 6;
end;
hence thesis by A3,A4,A30,A34,MATRIX_9:53;
end;
end;
theorem Th100:
for M be diagonal Matrix of K for P st [:P,P:] c= Indices M
holds Segm(M,P,P) is diagonal
proof
let M be diagonal Matrix of K;
let P such that
A1: [:P,P:] c= Indices M;
set S=Segm(M,P,P);
set SP=Sgm P;
let i,j be Nat such that
A2: i in Seg card P and
A3: j in Seg card P and
A4: i <> j;
A5: P c= Seg len M by A1,A2,Th67;
then
A6: SP is one-to-one by FINSEQ_3:92;
[i,j] in [:Seg card P,Seg card P:] by A2,A3,ZFMISC_1:87;
then
A7: [i,j] in Indices S by MATRIX_0:24;
dom SP=Seg card P by A5,FINSEQ_3:40;
then
A8: SP.i<>SP.j by A2,A3,A4,A6;
rng SP=P by A5,FINSEQ_1:def 13;
then
A9: [SP.i,SP.j] in Indices M by A1,A7,Th17;
S*(i,j)=M*(SP.i,SP.j) by A7,Def1;
hence thesis by A9,A8,MATRIX_1:def 6;
end;
theorem
for M be diagonal Matrix of K for NonZero1 be set st NonZero1={i where i
is Element of NAT:[i,i] in Indices M & M*(i,i)<>0.K} holds the_rank_of M = card
NonZero1
proof
let M be diagonal Matrix of K;
consider P,Q such that
A1: [:P,Q:] c= Indices M and
A2: card P = card Q and
A3: card P = the_rank_of M and
A4: Det EqSegm(M,P,Q)<>0.K by Def4;
let NZ be set such that
A5: NZ={i where i is Element of NAT:[i,i] in Indices M & M*(i,i)<>0.K};
A6: NZ c= Seg width M
proof
let x be object;
assume x in NZ;
then ex i be Element of NAT st x=i & [i,i] in Indices M & M*(i,i)<>0.K by
A5;
hence thesis by ZFMISC_1:87;
end;
then not 0 in NZ;
then reconsider nz=NZ as without_zero finite Subset of NAT by A6,
MEASURE6:def 2,XBOOLE_1:1;
set S=Segm(M,nz,nz);
NZ c= dom M
proof
let x be object;
assume x in NZ;
then ex i be Element of NAT st x=i & [i,i] in Indices M & M*(i,i)<>0.K by
A5;
hence thesis by ZFMISC_1:87;
end;
then
A7: [:nz,nz:] c= Indices M by A6,ZFMISC_1:96;
then reconsider S as diagonal Matrix of card nz,K by Th100;
set d=diagonal_of_Matrix S;
now
per cases by NAT_1:14;
suppose
card nz=0;
then Det S=1_K by MATRIXR2:41;
hence Det S<>0.K;
end;
suppose
A8: card nz>=1;
set Sn=Sgm nz;
A9: now
A10: rng Sn=nz by A6,FINSEQ_1:def 13;
A11: dom d=Seg len d by FINSEQ_1:def 3;
A12: len d=card nz by MATRIX_3:def 10;
let k be Nat such that
A13: k in dom d;
A14: d.k=S*(k,k) by A13,A11,A12,MATRIX_3:def 10;
dom Sn=dom d by A6,A11,A12,FINSEQ_3:40;
then Sn.k in nz by A13,A10,FUNCT_1:def 3;
then
A15: ex i be Element of NAT st i=Sn.k & [i,i] in Indices M & M*(i,i)<>
0.K by A5;
Indices S=[:Seg card nz,Seg card nz:] by MATRIX_0:24;
then [k,k] in Indices S by A13,A11,A12,ZFMISC_1:87;
hence d.k <> 0.K by A14,A15,Def1;
end;
Det S = Product d by A8,MATRIX_7:17;
hence Det S<>0.K by A9,FVSUM_1:82;
end;
end;
then Det EqSegm(M,nz,nz)<>0.K by Def3;
then
A16: the_rank_of M >= card nz by A7,Def4;
P c= nz by A5,A1,A2,A4,Th99;
then card P <= card nz by NAT_1:43;
hence thesis by A16,A3,XXREAL_0:1;
end;
reserve v,v1,v2,u,w for Vector of n-VectSp_over K,
t,t1,t2 for Element of n -tuples_on the carrier of K,
L for Linear_Combination of n-VectSp_over K,
M,M1 for Matrix of m,n,K;
theorem Th102:
the carrier of n -VectSp_over K = n-tuples_on the carrier of K
& 0.(n -VectSp_over K) = n |-> 0.K & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 +
v2 ) & ( t = v implies a * t = a * v )
proof
A1: the addLoopStr of n -VectSp_over K=n-Group_over K by PRVECT_1:def 5;
A2: n-Group_over K=addLoopStr(# n-tuples_on the carrier of K, product(the
addF of K,n), (n |-> 0.K) qua Element of n-tuples_on the carrier of K#)
by PRVECT_1:def 3;
hence the carrier of n -VectSp_over K = n-tuples_on the carrier of K & 0.(n
-VectSp_over K) =(n |-> 0.K) by A1;
thus t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 by A2,A1,PRVECT_1:def 1;
assume
A3: t=v;
rng t c= the carrier of K by RELAT_1:def 19;
then
A4: (id (the carrier of K))*t=t by RELAT_1:53;
thus a*v = (n-Mult_over K).(a,v) by PRVECT_1:def 5
.= (the multF of K)[;](a,t) by A3,PRVECT_1:def 4
.= a*t by A4,FUNCOP_1:34;
end;
registration
let K,n;
cluster n -VectSp_over K -> right_complementable Abelian add-associative
right_zeroed;
coherence
proof
set nV = n -VectSp_over K;
A1: now
let v,u;
reconsider V=v,U=u as Element of n-tuples_on the carrier of K by Th102;
thus v + u = V + U by Th102
.= U + V by FINSEQOP:33
.= u + v by Th102;
end;
A2: now
let v;
reconsider V=v,n0=0.nV as Element of n-tuples_on the carrier of K by
Th102;
thus v + 0.nV = V + n0 by Th102
.= V + (n|->0.K) by Th102
.= v by FVSUM_1:21;
end;
A3: nV is right_complementable
proof
reconsider N=n as Element of NAT by ORDINAL1:def 12;
let v;
reconsider V=v as Element of N-tuples_on the carrier of K by Th102;
reconsider u=-V as Element of nV by Th102;
v + u = V+ -V by Th102
.= n|->0.K by FVSUM_1:26
.= 0.nV by Th102;
hence ex u st v+u=0.nV;
end;
now
let u,v,w;
reconsider V=v,U=u,W=w,UV=u+v,VW=v+w as Element of n-tuples_on the
carrier of K by Th102;
thus (u + v) + w = UV + W by Th102
.= (U + V) + W by Th102
.= U + (V + W) by FINSEQOP:28
.= U + VW by Th102
.= u + (v + w) by Th102;
end;
hence thesis by A2,A3,A1,RLVECT_1:def 2,def 3,def 4;
end;
end;
registration
let K,n;
cluster -> Function-like Relation-like for Vector of n-VectSp_over K;
correctness
proof
let v be Element of n-VectSp_over K;
v is Element of n-tuples_on the carrier of K by Th102;
hence thesis;
end;
end;
Lm7: rng M is Subset of n-VectSp_over K
proof
rng M c= the carrier of n-VectSp_over K
proof
consider m such that
A1: for x st x in rng M ex p st x = p & len p = m by MATRIX_0:9;
let x be object such that
A2: x in rng M;
consider p such that
A3: x=p and
len p =m by A2,A1;
len p=n by A2,A3,MATRIX_0:def 2;
then p is Element of n-tuples_on the carrier of K by FINSEQ_2:92;
then p in n-tuples_on the carrier of K;
hence thesis by A3,Th102;
end;
hence thesis;
end;
notation
let K,m,n;
let M be Matrix of m,n,K;
synonym lines M for rng M;
synonym M is without_repeated_line for M is one-to-one;
end;
definition
let K be Field,m,n;
let M be Matrix of m,n,K;
redefine func lines M -> Subset of n-VectSp_over K;
coherence by Lm7;
end;
theorem Th103:
x in lines M iff ex i st i in Seg m & x = Line(M,i)
proof
thus x in lines M implies ex i st i in Seg m & x = Line(M,i)
proof
assume x in lines M;
then consider i be object such that
A1: i in dom M and
A2: M.i=x by FUNCT_1:def 3;
A3: len M=m by MATRIX_0:def 2;
reconsider i as Element of NAT by A1;
A4: dom M=Seg len M by FINSEQ_1:def 3;
then M.i=Line(M,i) by A1,A3,MATRIX_0:52;
hence thesis by A1,A2,A4,A3;
end;
given i such that
A5: i in Seg m and
A6: x = Line(M,i);
A7: len M=m by MATRIX_0:def 2;
dom M=Seg len M by FINSEQ_1:def 3;
then M.i in rng M by A5,A7,FUNCT_1:def 3;
hence thesis by A5,A6,MATRIX_0:52;
end;
theorem
for V be finite Subset of n-VectSp_over K ex M be Matrix of card V,n,K
st M is without_repeated_line & lines M = V
proof
let V be finite Subset of n-VectSp_over K;
set cV=card V;
card Seg cV=cV by FINSEQ_1:57;
then Seg cV,V are_equipotent by CARD_1:5;
then consider m be Function such that
A1: m is one-to-one and
A2: dom m = Seg cV and
A3: rng m=V by WELLORD2:def 4;
reconsider M=m as FinSequence by A2,FINSEQ_1:def 2;
now
let x;
assume x in rng M;
then reconsider p=x as Element of n-tuples_on the carrier of K by A3,Th102;
len p=n by CARD_1:def 7;
hence ex p st x = p & len p = n;
end;
then reconsider M as Matrix of K by MATRIX_0:9;
A4: len M=cV by A2,FINSEQ_1:def 3;
the carrier of n -VectSp_over K = n-tuples_on the carrier of K by Th102;
then for p st p in rng M holds len p=n by A3,CARD_1:def 7;
then M is Matrix of cV,n,K by A4,MATRIX_0:def 2;
hence thesis by A1,A3;
end;
definition
let K,n;
let F be FinSequence of n-VectSp_over K;
func FinS2MX F -> Matrix of len F,n,K equals
F;
coherence
proof
A1: F is FinSequence of n-tuples_on the carrier of K by Th102;
now
A2: rng F c= n-tuples_on the carrier of K by A1,FINSEQ_1:def 4;
let x;
assume x in rng F;
then reconsider p=x as Element of n-tuples_on the carrier of K by A2;
len p=n by CARD_1:def 7;
hence ex p st x = p & len p = n;
end;
then reconsider F9=F as Matrix of K by MATRIX_0:9;
now
A3: rng F9 c= n-tuples_on the carrier of K by A1,FINSEQ_1:def 4;
let p;
assume p in rng F9;
hence len p=n by A3,CARD_1:def 7;
end;
hence thesis by MATRIX_0:def 2;
end;
end;
definition
let K,m,n;
let M be Matrix of m,n,K;
func MX2FinS M -> FinSequence of n-VectSp_over K equals
M;
coherence
proof
lines M is Subset of n-VectSp_over K;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem Th105:
the_rank_of M = m implies M is without_repeated_line
proof
assume
A1: the_rank_of M = m;
A2: len M = m by MATRIX_0:def 2;
assume not M is without_repeated_line;
then consider x1,x2 be object such that
A3: x1 in dom M and
A4: x2 in dom M and
A5: M.x1=M.x2 and
A6: x1<>x2;
reconsider x1,x2 as Element of NAT by A3,A4;
consider k such that
A7: len M = k + 1 and
A8: len Del(M,x1) = k by A3,FINSEQ_3:104;
A9: dom M=Seg len M by FINSEQ_1:def 3;
then
A10: M.x2=Line(M,x2) by A4,A2,MATRIX_0:52;
M.x1=Line(M,x1) by A3,A9,A2,MATRIX_0:52;
then M = RLine(M,x1,Line(M,x2)) by A5,A10,MATRIX11:30
.= RLine(M,x1,1_K*Line(M,x2)) by FVSUM_1:57;
then m = the_rank_of DelLine(M,x1) by A1,A4,A6,A9,Th93;
then m <= k by A8,Th74;
hence thesis by A2,A7,NAT_1:13;
end;
theorem Th106:
i in Seg len M & a = L.(M.i) implies Line(FinS2MX(L (#) MX2FinS
M),i) = a * Line(M,i)
proof
assume that
A1: i in Seg len M and
A2: a = L.(M.i);
set MX=MX2FinS M;
set LM=L (#) MX;
i in dom M by A1,FINSEQ_1:def 3;
then
A3: M.i=MX/.i by PARTFUN1:def 6;
len M=m by MATRIX_0:def 2;
then
A4: Line(M,i)=M.i by A1,MATRIX_0:52;
then reconsider
L=Line(M,i) as Element of n-tuples_on the carrier of K by A3,Th102;
set FLM = FinS2MX LM;
A5: len LM=len M by VECTSP_6:def 5;
then
A6: i in dom FLM by A1,FINSEQ_1:def 3;
Line(FLM,i)=FLM.i by A1,A5,MATRIX_0:52;
hence Line(FLM,i) = a *MX/.i by A2,A3,A6,VECTSP_6:def 5
.= a*L by A3,A4,Th102
.= a*Line(M,i);
end;
theorem Th107:
M is without_repeated_line & Carrier L c= lines M & i in Seg n
implies (Sum L).i = Sum Col(FinS2MX(L (#) MX2FinS M),i)
proof
assume that
A1: M is without_repeated_line and
A2: Carrier L c= lines M and
A3: i in Seg n;
set MX=MX2FinS M;
set V=n-VectSp_over K;
set LM=L (#) MX;
A4: len LM=len M by VECTSP_6:def 5;
set FLM = FinS2MX LM;
set C=Col(FLM,i);
len LM=len C by MATRIX_0:def 8;
then consider g be sequence of the carrier of K such that
A5: Sum C = g.(len M) and
A6: g.0 = 0.K and
A7: for j be Nat,a st j < len M & a = C.(j+1) holds g.(j+1)
= g.j+a by A4,RLVECT_1:def 12;
Sum L = Sum LM by A1,A2,VECTSP_9:3;
then consider f be sequence of the carrier of V such that
A8: Sum L = f.(len M) and
A9: f.0 = 0.V and
A10: for j be Nat,v st j < len M & v = LM.(j+1) holds f.(j+1)
= f.j+v by A4,RLVECT_1:def 12;
defpred P[Nat] means $1 <= len M implies for v be Element of V st v=f.$1
holds v.i=g.$1;
A11: len M=m by MATRIX_0:def 2;
A12: for k st P[k] holds P[k+1]
proof
reconsider N=n as Element of NAT by ORDINAL1:def 12;
let k such that
A13: P[k];
set k1=k+1;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
assume
A14: k1 <= len M;
then
A15: k0.K by Th102;
let v;
assume v=f.0;
hence v.i=g.0 by A3,A9,A6,A27,FINSEQ_2:57;
end;
for k holds P[k] from NAT_1:sch 2(A26,A12);
hence thesis by A8,A5;
end;
theorem Th108:
for M,M1 st M is without_repeated_line & for i st i in Seg m
holds ex a st Line(M1,i) = a * Line(M,i) holds ex L be Linear_Combination of
lines M st L (#) MX2FinS M = M1
proof
let M,M1 such that
A1: M is without_repeated_line and
A2: for i st i in Seg m ex a st Line(M1,i) = a * Line(M,i);
set V=n-VectSp_over K;
defpred P[set,set] means for i st $1=i ex a st a=$2 & Line(M1,i) = a * Line(
M,i);
A3: for k st k in Seg len M ex x be Element of K st P[k,x]
proof
A4: len M=m by MATRIX_0:def 2;
let k;
assume k in Seg len M;
then consider a such that
A5: Line(M1,k) = a * Line(M,k) by A2,A4;
take a;
thus thesis by A5;
end;
consider p such that
A6: dom p = Seg len M and
A7: for k st k in Seg len M holds P[k,p.k] from FINSEQ_1:sch 5(A3);
defpred Q[object,object] means
for v st $1=v holds (not v in lines M implies $2=0.
K) & (v in lines M implies for k st k in Seg m & v=Line(M,k) holds $2=p.k);
A8: for x being object st x in the carrier of V
ex y being object st y in the carrier of K & Q[x,y]
proof
let x be object;
assume x in the carrier of V;
then reconsider v=x as Element of V;
per cases;
suppose
A9: v in lines M;
A10: rng p c= the carrier of K by FINSEQ_1:def 4;
consider j such that
A11: j in Seg m and
A12: v=Line(M,j) by A9,Th103;
len M=m by MATRIX_0:def 2;
then p.j in rng p by A6,A11,FUNCT_1:def 3;
then reconsider pj=p.j as Element of the carrier of K by A10;
take pj;
thus pj in the carrier of K;
let w such that
A13: w=x;
thus not w in lines M implies pj=0.K by A9,A13;
thus w in lines M implies for k st k in Seg m & w=Line(M,k) holds pj = p
.k
proof
len M=m by MATRIX_0:def 2;
then
A14: dom M=Seg m by FINSEQ_1:def 3;
A15: M.j=Line(M,j) by A11,MATRIX_0:52;
assume w in lines M;
let k such that
A16: k in Seg m and
A17: w=Line(M,k);
M.k=Line(M,k) by A16,MATRIX_0:52;
hence thesis by A1,A11,A12,A13,A16,A17,A14,A15;
end;
end;
suppose
A18: not v in lines M;
take 0K=0.K;
thus 0K in the carrier of K;
let w such that
A19: w=x;
thus not w in lines M implies 0K=0.K;
thus thesis by A18,A19;
end;
end;
consider l be Function of the carrier of V,the carrier of K such that
A20: for x being object st x in the carrier of V holds Q[x,l.x]
from FUNCT_2:sch 1(A8
);
reconsider L=l as Element of Funcs(the carrier of V, the carrier of K) by
FUNCT_2:8;
for v st not v in lines M holds L.v = 0.K by A20;
then reconsider L as Linear_Combination of V by VECTSP_6:def 1;
A21: Carrier L c= lines M
proof
let x be object;
assume x in Carrier L;
then ex v st x = v & L.v <> 0.K by VECTSP_6:1;
hence thesis by A20;
end;
set MX=MX2FinS M;
A22: len M=m by MATRIX_0:def 2;
reconsider L as Linear_Combination of lines M by A21,VECTSP_6:def 4;
set LM=L(#)MX;
A23: len LM=len M by VECTSP_6:def 5;
A24: now
let k such that
A25: 1<=k and
A26: k<=m;
A27: k in Seg m by A25,A26;
then consider a such that
A28: p.k=a and
A29: Line(M1,k) = a * Line(M,k) by A7,A22;
dom MX = Seg m by A22,FINSEQ_1:def 3;
then
A30: MX/.k=M.k by A27,PARTFUN1:def 6;
A31: Line(M,k) in lines M by A27,Th103;
then reconsider
LMk=Line(M,k) as Element of n-tuples_on the carrier of K by Th102;
A32: LMk=M.k by A27,MATRIX_0:52;
dom LM=Seg m by A22,A23,FINSEQ_1:def 3;
then
A33: LM.k=L.(MX/.k) * MX/.k by A27,VECTSP_6:def 5;
L.LMk =p.k by A20,A27,A31;
then LM.k=a * LMk by A28,A33,A30,A32,Th102;
hence M1.k=LM.k by A27,A29,MATRIX_0:52;
end;
len M1=m by MATRIX_0:def 2;
hence thesis by A22,A23,A24,FINSEQ_1:14;
end;
theorem Th109:
for M st M is without_repeated_line holds ( for i st i in Seg m
holds Line(M,i) <> n |-> 0.K ) & ( for M1 st (for i st i in Seg m ex a st Line(
M1,i) = a * Line(M,i))& for j st j in Seg n holds Sum Col(M1,j) = 0.K holds M1
= 0.(K,m,n) ) iff lines M is linearly-independent
proof
set V=n-VectSp_over K;
set n0=n|->0.K;
A1: len n0=n by CARD_1:def 7;
let M such that
A2: M is without_repeated_line;
thus (for i st i in Seg m holds Line(M,i) <> n |-> 0.K ) & (for M1 st (for i
st i in Seg m ex a st Line(M1,i) = a * Line(M,i)) & (for j st j in Seg n holds
Sum Col(M1,j)=0.K) holds M1 = 0.(K,m,n) ) implies lines M is
linearly-independent
proof
set MX=MX2FinS M;
set V=n-VectSp_over K;
assume that
A3: for i st i in Seg m holds Line(M,i) <> n |-> 0.K and
A4: for M1 st (for i st i in Seg m ex a st Line(M1,i)=a*Line(M,i))&
for j st j in Seg n holds Sum Col(M1,j)=0.K holds M1 = 0.(K,m,n);
let L be Linear_Combination of lines M such that
A5: Sum L = 0.V;
set LM=L (#) MX;
set FLM = FinS2MX LM;
A6: len LM= len MX by VECTSP_6:def 5;
A7: len M=m by MATRIX_0:def 2;
then reconsider flm=FLM as Matrix of m,n,K by A6;
A8: for i st i in Seg m ex a st Line(flm,i)=a*Line(M,i)
proof
let i such that
A9: i in Seg m;
Line(M,i) in lines M by A9,Th103;
then reconsider LM=Line(M,i) as Element of V;
reconsider LLM=L.LM as Element of K;
Line(M,i)=M.i by A9,MATRIX_0:52;
then Line(flm,i)=LLM*Line(M,i) by A7,A9,Th106;
hence thesis;
end;
A10: len (n|->0.K)=n by CARD_1:def 7;
assume Carrier L<>{};
then consider x being object such that
A11: x in Carrier L by XBOOLE_0:def 1;
Carrier L c= lines M by VECTSP_6:def 4;
then consider i such that
A12: i in Seg m and
A13: x=Line(M,i) by A11,Th103;
consider v such that
A14: x=v and
A15: L.v<>0.K by A11,VECTSP_6:1;
reconsider LM=Line(M,i) as Element of n-tuples_on the carrier of K by A13
,A14,Th102;
Line(M,i)=M.i by A12,MATRIX_0:52;
then
A16: Line(flm,i) = (L.v) * LM by A7,A12,A13,A14,Th106;
now
let j such that
A17: j in Seg n;
A18: (n|->0.K).j=0.K by A17,FINSEQ_2:57;
Carrier L c= lines M by VECTSP_6:def 4;
then (Sum L).j = Sum Col(flm,j) by A2,A17,Th107;
hence Sum Col(flm,j) = 0.K by A5,A18,Th102;
end;
then flm=0.(K,m,n) by A4,A8;
then
A19: flm.i=n|->0.K by A12,FUNCOP_1:7;
A20: dom LM=Seg n by FINSEQ_2:124;
len LM=n by CARD_1:def 7;
then consider j such that
A21: 1<=j and
A22: j<= n and
A23: LM.j <> (n|->0.K).j by A3,A12,A10,FINSEQ_1:14;
A24: j in Seg n by A21,A22;
then
A25: LM.j<>0.K by A23,FINSEQ_2:57;
j in Seg n by A21,A22;
then
A26: LM.j in rng LM by A20,FUNCT_1:def 3;
rng LM c= the carrier of K by RELAT_1:def 19;
then reconsider LMj=LM.j as Element of K by A26;
A27: ((L.v) * LM).j=(L.v)*LMj by A24,FVSUM_1:51;
flm.i = Line(flm,i) by A12,MATRIX_0:52;
then Line(flm,i).j=0.K by A19,A24,FINSEQ_2:57;
hence thesis by A15,A25,A27,A16,VECTSP_1:12;
end;
assume
A28: lines M is linearly-independent;
hereby
let i;
assume i in Seg m;
then Line(M,i) in lines M by Th103;
then Line(M,i)<>0.V by A28,VECTSP_7:2;
hence Line(M,i) <> n |-> 0.K by Th102;
end;
let M1 such that
A29: for i st i in Seg m ex a st Line(M1,i) = a * Line(M,i) and
A30: for j st j in Seg n holds Sum Col(M1,j)=0.K;
consider L be Linear_Combination of lines M such that
A31: L (#) MX2FinS M = M1 by A2,A29,Th108;
A32: Carrier L c= lines M by VECTSP_6:def 4;
A33: now
let j such that
A34: 1<=j and
A35: j<=n;
A36: j in Seg n by A34,A35;
hence (Sum L).j = Sum Col(FinS2MX(L (#) MX2FinS M),j) by A2,A32,Th107
.= 0.K by A30,A31,A36
.= n0.j by A36,FINSEQ_2:57;
end;
reconsider SumL=Sum L as Element of n-tuples_on the carrier of K by Th102;
len SumL=n by CARD_1:def 7;
then SumL = n0 by A1,A33
.= 0.V by Th102;
then
A37: Carrier L={} by A28;
assume M1 <> 0.(K,m,n);
then consider I,J be Nat such that
A38: [I,J] in Indices M1 and
A39: M1*(I,J)<>(0.(K,m,n))*(I,J) by MATRIX_0:27;
[I,J] in Indices 0.(K,m,n) by A38,MATRIX_0:26;
then
A40: M1*(I,J)<>0.K by A39,MATRIX_3:1;
reconsider ii=I,jj=J as Element of NAT by ORDINAL1:def 12;
A41: Indices M1=Indices M by MATRIX_0:26;
then Indices M1 = [:Seg len M, Seg width M :] by FINSEQ_1:def 3;
then
A42: ii in Seg len M by A38,ZFMISC_1:87;
A43: len M=m by MATRIX_0:def 2;
then Line(M,ii) in lines M by A42,Th103;
then reconsider Mii=M.ii as Element of V by A42,A43,MATRIX_0:52;
A44: jj in Seg width M by A38,A41,ZFMISC_1:87;
then
A45: Line(M,ii).jj=M*(ii,jj) by MATRIX_0:def 7;
jj in Seg width M1 by A38,ZFMISC_1:87;
then M1*(I,J) = Line(FinS2MX(L (#) MX2FinS M),ii).jj by A31,MATRIX_0:def 7
.= ((L.Mii)* Line(M,ii)).jj by A42,Th106
.= (L.Mii) *(M*(ii,jj)) by A44,A45,FVSUM_1:51;
then L.Mii<>0.K by A40;
hence thesis by A37,VECTSP_6:1;
end;
theorem Th110:
the_rank_of M = m implies lines M is linearly-independent
proof
assume
A1: the_rank_of M = m;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
set V=n-VectSp_over K;
per cases;
suppose
m=0;
then len M=0 by MATRIX_0:def 2;
then M = {};
hence thesis;
end;
suppose
A2: m<>0;
then
A3: width M=n by Th1;
A4: M is without_repeated_line by A1,Th105;
A5: now
set n0=n|->0.K;
set NULL=0.(K,m,n);
let M1 such that
A6: for i st i in Seg m ex a st Line(M1,i) = a * Line(M,i) and
A7: for j st j in Seg n holds Sum Col(M1,j) = 0.K;
assume M1 <> 0.(K,m,n);
then consider i,j such that
A8: [i,j] in Indices M1 and
A9: M1*(i,j)<>NULL*(i,j) by MATRIX_0:27;
reconsider i,j as Element of NAT by ORDINAL1:def 12;
A10: len M=m by MATRIX_0:def 2;
Indices M1=Indices NULL by MATRIX_0:26;
then
A11: M1*(i,j)<>0.K by A8,A9,MATRIX_3:1;
A12: Indices M=[:Seg m,Seg n:] by A3,MATRIX_0:25;
Indices M1=Indices M by MATRIX_0:26;
then
A13: i in Seg m by A12,A8,ZFMISC_1:87;
then consider a such that
A14: Line(M1,i) = a * Line(M,i) by A6;
A15: width M1=n by A2,Th1;
then
A16: j in Seg n by A8,ZFMISC_1:87;
then
A17: Line(M,i).j=M*(i,j) by A3,MATRIX_0:def 7;
set R=RLine(M,i,a*Line(M,i));
consider L be Linear_Combination of lines M such that
A18: L (#) MX2FinS M = M1 by A1,A6,Th105,Th108;
set LM=L (#) MX2FinS M;
len M1=len M by A18,VECTSP_6:def 5;
then consider f be sequence of the carrier of V such that
A19: Sum LM= f.m and
A20: f.0 = 0.V and
A21: for j be Nat,v st j < m & v = LM.(j+1) holds f.(j+1)
= f.j+v by A18,A10,RLVECT_1:def 12;
set RR=RLine(R,i,n0);
A22: len RR=m by MATRIX_0:def 2;
defpred P[Nat] means $1 < i implies for t st t=f.$1 holds the_rank_of R=
the_rank_of RLine(R,i,Line(R,i)+t);
width M = len Line(M,i) by MATRIX_0:def 7
.= len (a*Line(M,i)) by MATRIXR1:16;
then
A23: width R=width M by MATRIX11:def 3;
A24: for k st P[k] holds P[k+1]
proof
let k such that
A25: P[k];
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
set k1=k+1;
A26: 1<=k1 by NAT_1:14;
A27: i<=m by A13,FINSEQ_1:1;
reconsider LR=Line(R,i),LM1=Line(M1,k1) as Element of N-tuples_on the
carrier of K by A2,Th1;
assume
A28: k1 < i;
let t such that
A29: t = f.k1;
reconsider t1=f.kk,T=t as Element of N-tuples_on the carrier of K by
Th102;
set RR=RLine(R,i,Line(R,i)+t1);
reconsider LRt=LR+t,LRt1=LR+t1 as Element of (the carrier of K)* by
FINSEQ_1:def 11;
A30: len (LR+T)=n by CARD_1:def 7;
A31: len (LR+t1)=width R by A3,A23,CARD_1:def 7;
then width RR=width R by MATRIX11:def 3;
then
A32: RLine(RR,i,LR+t) = Replace(RR,i,LRt) by A3,A23,A30,MATRIX11:29
.= Replace(Replace(R,i,LRt1),i,LRt) by A31,MATRIX11:29
.= Replace(R,i,LRt) by FUNCT_7:34
.= RLine(R,i,LR+t)by A3,A23,A30,MATRIX11:29;
i<=m by A13,FINSEQ_1:1;
then k1 0.K by A20,Th102;
then Line(R,i)+t=Line(R,i) by A3,A23,FVSUM_1:21;
hence thesis by MATRIX11:30;
end;
A40: for k holds P[k] from NAT_1:sch 2(A39,A24);
A41: for k st Q[k] holds Q[k+1]
proof
let k such that
A42: Q[k];
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
reconsider t1=f.kk as Element of N-tuples_on the carrier of K by Th102;
set k1=k+1;
reconsider LR=Line(R,i),LM1=Line(M1,k1) as Element of n-tuples_on the
carrier of K by A2,Th1;
assume that
A43: i<=k1 and
A44: k1<=m;
A45: k0.K by A11;
then
A68: m=the_rank_of R by A1,Th89;
A69: len n0=n by CARD_1:def 7;
then
A70: width RR=width R by A3,A23,MATRIX11:def 3;
A71: Line(RR,i)=n0 by A3,A13,A23,A69,MATRIX11:28;
i<=m by A13,FINSEQ_1:1;
then m=the_rank_of RLine(R,i,n0) by A68,A19,A59,A67,A69,A60,FINSEQ_1:14;
then m=the_rank_of DelLine(RR,i) by A3,A23,A71,A70,Th90;
then m<=k by A66,Th74;
hence contradiction by A65,NAT_1:13;
end;
now
A72: len M = m by MATRIX_0:def 2;
A73: dom M=Seg len M by FINSEQ_1:def 3;
let i;
assume i in Seg m;
then consider k such that
A74: m = k + 1 and
A75: len Del(M,i) = k by A73,A72,FINSEQ_3:104;
assume Line(M,i) = n |-> 0.K;
then the_rank_of DelLine(M,i) = m by A1,A3,Th90;
then m<= k by A75,Th74;
hence contradiction by A74,NAT_1:13;
end;
hence thesis by A4,A5,Th109;
end;
end;
theorem Th111:
for M be diagonal Matrix of n,K st the_rank_of M = n holds lines M is
Basis of n-VectSp_over K
proof
let M be diagonal Matrix of n,K such that
A1: the_rank_of M = n;
set lM=lines M;
set V=n-VectSp_over K;
reconsider V9=V as Subspace of V by VECTSP_4:24;
now
let v;
thus v in Lin lM implies v in V9;
thus v in V9 implies v in Lin lM
proof
reconsider t=v as Element of n-tuples_on the carrier of K by Th102;
assume v in V9;
deffunc F(Nat)=(t/.$1)*(M*($1,$1)")*Line(M,$1);
consider f be FinSequence of (width M)-tuples_on the carrier of K such
that
A2: len f = n and
A3: for j st j in dom f holds f.j = F(j) from FINSEQ_2:sch 1;
A4: dom f = Seg n by A2,FINSEQ_1:def 3;
width M=n by MATRIX_0:24;
then reconsider f as FinSequence of the carrier of V by Th102;
reconsider M1=FinS2MX f as Matrix of n,K by A2;
now
let i such that
A5: i in Seg n;
Line(M1,i) = M1.i by A5,MATRIX_0:52
.= F(i) by A3,A4,A5;
hence ex a st Line(M1,i) = a * Line(M,i);
end;
then consider L be Linear_Combination of lM such that
A6: L (#) MX2FinS M = M1 by A1,Th105,Th108;
set MX=MX2FinS M;
A7: len t=n by CARD_1:def 7;
reconsider SumL=Sum L as Element of n-tuples_on the carrier of K by Th102
;
A8: Carrier L c= lM by VECTSP_6:def 4;
A9: now
set diag=diagonal_of_Matrix M;
let i such that
A10: 1<=i and
A11: i<=n;
A12: i in Seg n by A10,A11;
then
A13: diag.i=M*(i,i) by MATRIX_3:def 10;
len diag=n by MATRIX_3:def 10;
then
A14: dom diag=Seg n by FINSEQ_1:def 3;
A15: width M=n by MATRIX_0:24;
then
A16: Line(M,i).i = M*(i,i) by A12,MATRIX_0:def 7;
set C=Col(M1,i);
A17: dom t=Seg n by FINSEQ_2:124;
len C=len M1 by MATRIX_0:def 8;
then
A18: dom C=Seg len M1 by FINSEQ_1:def 3;
len M=n by MATRIX_0:24;
then
A19: dom M=Seg n by FINSEQ_1:def 3;
A20: Det M<>0.K by A1,Th83;
A21: len M1=n by MATRIX_0:24;
then
A22: dom M1=Seg n by FINSEQ_1:def 3;
Det M=Product diag by A10,A11,MATRIX_7:17,NAT_1:14;
then
A23: diag.i<>0.K by A12,A20,A14,FVSUM_1:82;
A24: Line(M1,i) = M1.i by A12,MATRIX_0:52
.= (t/.i)*((M*(i,i))")*Line(M,i) by A3,A12,A22;
A25: width M1=n by MATRIX_0:24;
now
let k such that
A26: k in dom C and
A27: k<>i;
A28: [k,i] in Indices M by A21,A15,A12,A18,A19,A26,ZFMISC_1:87;
A29: Line(M,k).i = M*(k,i) by A15,A12,MATRIX_0:def 7
.= 0.K by A27,A28,MATRIX_1:def 6;
A30: (MX/.k) = (M.k) by A21,A18,A19,A26,PARTFUN1:def 6
.= Line(M,k) by A21,A18,A26,MATRIX_0:52;
Line(M1,k) = M1.k by A18,A26,MATRIX_0:52
.= L.(MX/.k)* MX/.k by A6,A21,A18,A22,A26,VECTSP_6:def 5
.= L.(MX/.k)* Line(M,k) by A15,A30,Th102;
then Line(M1,k).i = L.(MX/.k) * 0.K by A15,A12,A29,FVSUM_1:51
.= 0.K;
hence 0.K = M1*(k,i) by A25,A12,MATRIX_0:def 7
.= C.k by A21,A18,A22,A26,MATRIX_0:def 8;
end;
then C.i = Sum C by A21,A12,A18,MATRIX_3:12
.= SumL.i by A1,A6,A8,A12,Th105,Th107;
hence SumL.i = M1*(i,i) by A12,A22,MATRIX_0:def 8
.= Line(M1,i).i by A25,A12,MATRIX_0:def 7
.= (t/.i)*((M*(i,i))")*(M*(i,i)) by A15,A12,A24,A16,FVSUM_1:51
.= (t/.i)*((M*(i,i)")*(M*(i,i))) by GROUP_1:def 3
.= (t/.i)*1_K by A23,A13,VECTSP_1:def 10
.= t/.i
.= t.i by A12,A17,PARTFUN1:def 6;
end;
len SumL=n by CARD_1:def 7;
then SumL=t by A7,A9;
hence thesis by VECTSP_7:7;
end;
end;
then
A31: Lin lM = the ModuleStr of V by VECTSP_4:30;
lines M is linearly-independent by A1,Th110;
hence thesis by A31,VECTSP_7:def 3;
end;
Lm8: lines 1.(K,n) is Basis of n-VectSp_over K & the_rank_of 1.(K,n)=n
proof
set ONE=1.(K,n);
n=0 or n>=1 by NAT_1:14;
then
A1: Det ONE=1_K by MATRIXR2:41,MATRIX_7:16;
for i,j st [i,j] in Indices ONE & ONE*(i,j) <> 0.K holds i=j by
MATRIX_1:def 3;
then
A2: ONE is diagonal by MATRIX_1:def 6;
1_K<>0.K;
then the_rank_of ONE=n by A1,Th83;
hence thesis by A2,Th111;
end;
registration
let K,n;
cluster n -VectSp_over K -> finite-dimensional;
coherence
proof
lines 1.(K,n) is Basis of n-VectSp_over K by Lm8;
hence thesis by MATRLIN:def 1;
end;
end;
theorem
dim (n-VectSp_over K) = n
proof
set ONE=1.(K,n);
len ONE=n by MATRIX_0:24;
then
A1: dom ONE=Seg n by FINSEQ_1:def 3;
then
A2: ONE.:Seg n=lines ONE by RELAT_1:113;
the_rank_of ONE=n by Lm8;
then ONE is without_repeated_line by Th105;
then Seg n,ONE.:Seg n are_equipotent by A1,CARD_1:33;
then card Seg n=card lines ONE by A2,CARD_1:5;
then
A3: card lines ONE=n by FINSEQ_1:57;
lines ONE is Basis of n-VectSp_over K by Lm8;
hence thesis by A3,VECTSP_9:def 1;
end;
theorem Th113:
for M,i,a st for j st j in Seg m holds M*(j,i) = a holds M is
without_repeated_line iff Segm(M,Seg len M,Seg width M\{i}) is
without_repeated_line
proof
let M, i, a such that
A1: for j st j in Seg m holds M*(j,i) = a;
set Sl=Sgm Seg len M;
set SMi=Seg width M\{i};
set S=Segm(M,Seg len M,SMi);
set Si=Sgm SMi;
A2: len M=m by MATRIX_0:def 2;
A3: card Seg len M=len M by FINSEQ_1:57;
len S=card Seg len M by MATRIX_0:def 2;
then
A4: dom S=Seg m by A2,A3,FINSEQ_1:def 3;
A5: dom M=Seg m by A2,FINSEQ_1:def 3;
thus M is without_repeated_line implies S is without_repeated_line
proof
A6: SMi c= Seg width M by XBOOLE_1:36;
assume
A7: M is without_repeated_line;
let x1,x2 be object such that
A8: x1 in dom S and
A9: x2 in dom S and
A10: S.x1=S.x2;
reconsider i1=x1,i2=x2 as Element of NAT by A8,A9;
A11: Sl=idseq m by A2,FINSEQ_3:48;
then
A12: Line(M,i1) * Si = Line(M,Sl.i1) *Si by A4,A8,FINSEQ_2:49
.= Line(S,i1) by A2,A3,A4,A8,Th47,XBOOLE_1:36
.= S.i1 by A2,A3,A4,A8,MATRIX_0:52
.= Line(S,i2) by A2,A3,A4,A9,A10,MATRIX_0:52
.= Line(M,Sl.i2) * Si by A2,A3,A4,A9,Th47,XBOOLE_1:36
.= Line(M,i2) * Si by A4,A9,A11,FINSEQ_2:49;
A13: now
let k such that
A14: 1<=k and
A15: k<=width M;
A16: k in Seg width M by A14,A15;
per cases;
suppose
A17: k = i;
then
A18: M*(i2,k)=a by A1,A4,A9;
A19: M*(i1,k) =Line(M,i1).k by A16,MATRIX_0:def 7;
M*(i1,k)=a by A1,A4,A8,A17;
hence Line(M,i1).k=Line(M,i2).k by A16,A18,A19,MATRIX_0:def 7;
end;
suppose
A20: k <> i;
A21: rng Si=SMi by A6,FINSEQ_1:def 13;
k in SMi by A16,A20,ZFMISC_1:56;
then consider x being object such that
A22: x in dom Si and
A23: Si.x=k by A21,FUNCT_1:def 3;
thus Line(M,i1).k = (Line(M,i1)*Si).x by A22,A23,FUNCT_1:13
.= Line(M,i2).k by A12,A22,A23,FUNCT_1:13;
end;
end;
A24: len Line(M,i2)=width M by CARD_1:def 7;
len Line(M,i1)=width M by CARD_1:def 7;
then Line(M,i1) = Line(M,i2) by A24,A13
.= M.i2 by A4,A9,MATRIX_0:52;
then M.i1 = M.i2 by A4,A8,MATRIX_0:52;
hence thesis by A5,A4,A7,A8,A9;
end;
thus S is without_repeated_line implies M is without_repeated_line
proof
A25: Sl=idseq m by A2,FINSEQ_3:48;
assume
A26: S is without_repeated_line;
let x1,x2 be object such that
A27: x1 in dom M and
A28: x2 in dom M and
A29: M.x1=M.x2;
reconsider i1=x1,i2=x2 as Element of NAT by A27,A28;
A30: Line(M,i1)=M.i1 by A5,A27,MATRIX_0:52;
A31: Line(M,i2)=M.i2 by A5,A28,MATRIX_0:52;
S.x1 = Line(S,i1) by A2,A3,A5,A27,MATRIX_0:52
.= Line(M,Sl.i1) * Si by A2,A3,A5,A27,Th47,XBOOLE_1:36
.= Line(M,i2) * Si by A5,A27,A29,A25,A30,A31,FINSEQ_2:49
.= Line(M,Sl.i2) * Si by A5,A28,A25,FINSEQ_2:49
.= Line(S,i2) by A2,A3,A5,A28,Th47,XBOOLE_1:36
.= S.x2 by A2,A3,A5,A28,MATRIX_0:52;
hence thesis by A5,A4,A26,A27,A28;
end;
end;
theorem Th114:
for M,i st M is without_repeated_line & lines M is
linearly-independent & for j st j in Seg m holds M*(j,i) = 0.K holds lines Segm
(M,Seg len M,Seg width M\{i}) is linearly-independent
proof
let M,i;
assume that
A1: M is without_repeated_line and
A2: lines M is linearly-independent and
A3: for j st j in Seg m holds M*(j,i) = 0.K;
set SMi=Seg width M\{i};
set Sl=Seg len M;
set S=Segm(M,Sl,SMi);
A4: SMi c= Seg width M by XBOOLE_1:36;
A5: card Sl=len M by FINSEQ_1:57;
A6: len M=m by MATRIX_0:def 2;
per cases;
suppose
m=0;
then len S=0 by A6,MATRIX_0:def 2;
then S = {};
hence thesis;
end;
suppose
m<>0;
then
A7: width M=n by Th1;
A8: now
set n0=n|->0.K;
A9: len n0=n by CARD_1:def 7;
A10: dom Sgm SMi=Seg card SMi by FINSEQ_3:40,XBOOLE_1:36;
let k such that
A11: k in Seg card Sl;
Line(M,k) in lines M by A5,A6,A11,Th103;
then reconsider
LM=Line(M,k) as Element of n-tuples_on the carrier of K by Th102;
A12: len LM=n by CARD_1:def 7;
LM <> n0 by A1,A2,A5,A6,A11,Th109;
then consider n9 be Nat such that
A13: 1<=n9 and
A14: n9<=n and
A15: LM.n9 <> n0.n9 by A12,A9;
A16: n9 in Seg n by A13,A14;
then
A17: n0.n9=0.K by FINSEQ_2:57;
Sgm Sl =idseq m by A6,FINSEQ_3:48;
then
A18: Sgm Sl.k = k by A5,A6,A11,FINSEQ_2:49;
A19: rng Sgm SMi=SMi by A4,FINSEQ_1:def 13;
LM.n9=M*(k,n9) by A7,A16,MATRIX_0:def 7;
then n9<>i by A3,A5,A6,A11,A15,A17;
then n9 in SMi by A7,A16,ZFMISC_1:56;
then consider x being object such that
A20: x in dom Sgm SMi and
A21: Sgm SMi.x = n9 by A19,FUNCT_1:def 3;
assume
A22: Line(S,k) = card SMi |-> 0.K;
reconsider x as Element of NAT by A20;
Line(S,k) = Line(M,Sgm Sl.k) * Sgm SMi by A11,Th47,XBOOLE_1:36;
then Line(S,k).x=Line(M,Sgm Sl.k).n9 by A20,A21,FUNCT_1:13;
hence contradiction by A22,A15,A17,A20,A10,A18,FINSEQ_2:57;
end;
A23: now
set NULL=0.(K,card Sl,card SMi);
let M1 be Matrix of card Sl,card SMi,K such that
A24: for i st i in Seg card Sl ex a st Line(M1,i) = a * Line(S,i) and
A25: for j st j in Seg card SMi holds Sum Col(M1,j) = 0.K;
defpred P[set,set] means for i st $1=i ex a st a=$2 & Line(M1,i) = a *
Line(S,i);
A26: for k st k in Seg m ex x be Element of K st P[k,x]
proof
let k;
assume k in Seg m;
then consider a such that
A27: Line(M1,k) = a * Line(S,k) by A5,A6,A24;
take a;
thus thesis by A27;
end;
consider p such that
A28: dom p = Seg m and
A29: for k st k in Seg m holds P[k,p.k] from FINSEQ_1:sch 5(A26);
deffunc F(Nat)=p/.$1 * Line(M,$1);
consider f be FinSequence of (width M)-tuples_on the carrier of K such
that
A30: len f = m and
A31: for j st j in dom f holds f.j = F(j) from FINSEQ_2:sch 1;
reconsider f9=f as FinSequence of the carrier of n-VectSp_over K by A7
,Th102;
FinS2MX f9 is Matrix of m,n,K by A30;
then reconsider Mf=f as Matrix of m,n,K;
A32: dom f = Seg m by A30,FINSEQ_1:def 3;
len Mf = m by MATRIX_0:def 2;
then
A33: dom Mf = Seg m by FINSEQ_1:def 3;
A34: now
A35: len M1=m by A5,A6,MATRIX_0:def 2;
A36: len Mf=m by MATRIX_0:def 2;
A37: dom Mf=Seg len Mf by FINSEQ_1:def 3;
A38: dom M1=Seg len M1 by FINSEQ_1:def 3;
let j such that
A39: j in Seg n;
set C=Col(Mf,j);
A40: len C = len Mf by MATRIX_0:def 8
.= m by MATRIX_0:def 2;
per cases;
suppose
A41: j=i;
set m0=m|->0.K;
A42: now
let n9 be Nat such that
A43: 1<=n9 and
A44: n9<=m;
A45: width M = n by A43,A44,Th1;
A46: width Mf=n by A43,A44,Th1;
A47: n9 in Seg m by A43,A44;
then
A48: Mf.n9 = Mf/.n9 by A33,PARTFUN1:def 6;
0.K = M*(n9,i) by A3,A47
.= Line(M,n9).i by A39,A41,A45,MATRIX_0:def 7;
then p/.n9*0.K = (p/.n9 * Line(M,n9)).i by A39,A41,A45,FVSUM_1:51
.= (Mf/.n9).i by A31,A32,A47,A48
.= Line(Mf,n9).i by A47,A48,MATRIX_0:52
.= Mf*(n9,i) by A39,A41,A46,MATRIX_0:def 7
.= Col(Mf,i).n9 by A36,A37,A47,MATRIX_0:def 8;
hence Col(Mf,j).n9 = 0.K by A41
.= m0.n9 by A47,FINSEQ_2:57;
end;
len m0=m by CARD_1:def 7;
then C=m0 by A40,A42;
hence Sum C=0.K by A40,MATRIX_3:11;
end;
suppose
A49: j<>i;
A50: rng Sgm SMi=SMi by A4,FINSEQ_1:def 13;
j in SMi by A7,A39,A49,ZFMISC_1:56;
then consider x being object such that
A51: x in dom Sgm SMi and
A52: Sgm SMi.x=j by A50,FUNCT_1:def 3;
reconsider x as Element of NAT by A51;
set C1=Col(M1,x);
A53: dom Sgm SMi =Seg card SMi by FINSEQ_3:40,XBOOLE_1:36;
A54: now
let n9 be Nat such that
A55: 1<=n9 and
A56: n9<=m;
A57: width Mf=n by A55,A56,Th1;
A58: width S=card SMi by A6,A55,A56,Th1;
A59: Sgm Sl=idseq m by A6,FINSEQ_3:48;
A60: width M1=card SMi by A6,A55,A56,Th1;
A61: Line(M,n9).j=M*(n9,j ) by A7,A39,MATRIX_0:def 7;
A62: n9 in Seg m by A55,A56;
then consider a such that
A63: a=p.n9 and
A64: Line(M1,n9) = a * Line(S,n9) by A29;
A65: Mf.n9 = Mf/.n9 by A33,A62,PARTFUN1:def 6;
(idseq m).n9=n9 by A62,FINSEQ_2:49;
then Line(M,n9) * Sgm SMi=Line(S,n9) by A5,A6,A62,A59,Th47,
XBOOLE_1:36;
then
A66: Line(S,n9).x = Line(M,n9).j by A51,A52,FUNCT_1:13;
thus C.n9 = Mf*(n9,j) by A36,A37,A62,MATRIX_0:def 8
.= Line(Mf,n9).j by A39,A57,MATRIX_0:def 7
.= (Mf/.n9).j by A62,A65,MATRIX_0:52
.= (p/.n9 * Line(M,n9)).j by A31,A32,A62,A65
.= (a * Line(M,n9)).j by A28,A62,A63,PARTFUN1:def 6
.= a* (M*(n9,j)) by A7,A39,A61,FVSUM_1:51
.= (a*Line(S,n9)).x by A51,A53,A58,A66,A61,FVSUM_1:51
.= M1*(n9,x) by A51,A53,A60,A64,MATRIX_0:def 7
.= C1.n9 by A35,A38,A62,MATRIX_0:def 8;
end;
A67: len C=len Mf by MATRIX_0:def 8;
len C1=len M1 by MATRIX_0:def 8;
then C=C1 by A36,A35,A67,A54;
hence Sum C=0.K by A25,A51,A53;
end;
end;
now
let j such that
A68: j in Seg m;
take pj=p/.j;
thus Line(Mf,j) = Mf.j by A68,MATRIX_0:52
.= pj * Line(M,j) by A31,A32,A68;
end;
then
A69: Mf = 0.(K,m,n) by A1,A2,A34,Th109;
A70: now
let j such that
A71: 1<=j and
A72: j<=m;
A73: j in Seg m by A71,A72;
then consider a such that
A74: a=p.j and
A75: Line(M1,j) = a * Line(S,j) by A29;
A76: Line(0.(K,m,n),j) = 0.(K,m,n).j by A73,MATRIX_0:52
.= n |-> 0.K by A73,FUNCOP_1:7;
p.j=p/.j by A28,A73,PARTFUN1:def 6;
then
A77: a * Line(M,j) = Mf.j by A31,A32,A73,A74
.= Line(Mf,j) by A73,MATRIX_0:52;
A78: rng Sgm SMi =SMi by A4,FINSEQ_1:def 13;
Sgm Sl =idseq m by A6,FINSEQ_3:48;
then Sgm Sl.j = j by A73,FINSEQ_2:49;
then
A79: Line(S,j) = Line(M,j) * Sgm SMi by A5,A6,A73,Th47,XBOOLE_1:36;
Seg n /\ SMi = SMi by A7,XBOOLE_1:28,36;
then
A80: Sgm SMi " (Seg n) = Sgm SMi "(rng Sgm SMi) by A78,RELAT_1:133
.= dom Sgm SMi by RELAT_1:134
.= Seg card SMi by FINSEQ_3:40,XBOOLE_1:36;
dom Line(M,j) = Seg len Line(M,j) by FINSEQ_1:def 3
.= Seg width M by CARD_1:def 7;
then Line(M1,j) = Line(0.(K,m,n),j)*Sgm SMi by A69,A75,A77,A78,A79,Th87
,XBOOLE_1:36
.= card SMi |-> 0.K by A80,A76,FUNCOP_1:19
.= NULL.j by A5,A6,A73,FUNCOP_1:7;
hence M1.j = NULL.j by A5,A6,A73,MATRIX_0:52;
end;
A81: len NULL=m by A5,A6,MATRIX_0:def 2;
len M1=m by A5,A6,MATRIX_0:def 2;
hence M1 = NULL by A81,A70;
end;
S is without_repeated_line by A1,A3,Th113;
hence thesis by A8,A23,Th109;
end;
end;
theorem Th115:
for V be VectSp of K for U be finite Subset of V st U is
linearly-independent for u, v be Vector of V st u in U & v in U & u <> v holds
U\{u} \/ {u+a*v} is linearly-independent
proof
let V be VectSp of K;
let U be finite Subset of V such that
A1: U is linearly-independent;
let u, v be Vector of V such that
A2: u in U and
A3: v in U and
A4: u<>v;
set ua=u+a*v;
set Uu=U\{u};
set Uua=Uu\/{ua};
per cases;
suppose
u=ua;
hence thesis by A1,A2,ZFMISC_1:116;
end;
suppose
A5: u<>ua;
now
let L be Linear_Combination of Uua such that
A6: Sum(L)=0.V;
per cases;
suppose
A7: L.ua=0.K;
Carrier L c= Uu
proof
let x be object;
assume
A8: x in Carrier L;
then consider v be Vector of V such that
A9: x = v and
A10: L.v <> 0.K by VECTSP_6:1;
Carrier L c= Uua by VECTSP_6:def 4;
then v in Uu or v in {ua} & not v in {ua} by A7,A8,A9,A10,
TARSKI:def 1,XBOOLE_0:def 3;
hence thesis by A9;
end;
then reconsider L9=L as Linear_Combination of Uu by VECTSP_6:def 4;
A11: Sum L9=0.V by A6;
Uu is linearly-independent by A1,VECTSP_7:1,XBOOLE_1:36;
hence Carrier L={} by A11;
end;
suppose
A12: L.ua<>0.K;
A13: Carrier L c= Uua by VECTSP_6:def 4;
Uu c= U by XBOOLE_1:36;
then Uua c=U\/{ua} by XBOOLE_1:13;
then
A14: Carrier L c= U\/{ua} by A13;
ua in {ua} by TARSKI:def 1;
then ua in Lin{ua} by VECTSP_7:8;
then consider Lua be Linear_Combination of {ua} such that
A15: ua=Sum Lua by VECTSP_7:7;
reconsider LLua=L.ua * Lua as Linear_Combination of {ua} by VECTSP_6:31
;
A16: Carrier LLua c= {ua} by VECTSP_6:def 4;
then not u in Carrier LLua by A5,TARSKI:def 1;
then
A17: LLua.u=0.K by VECTSP_6:2;
v in {v} by TARSKI:def 1;
then v in Lin{v} by VECTSP_7:8;
then consider Lv be Linear_Combination of {v} such that
A18: v=Sum Lv by VECTSP_7:7;
reconsider LLv=(L.ua*a) * Lv as Linear_Combination of {v} by
VECTSP_6:31;
A19: Carrier LLv c= {v} by VECTSP_6:def 4;
then not u in Carrier LLv by A4,TARSKI:def 1;
then
A20: LLv.u=0.K by VECTSP_6:2;
v <> ua
proof
assume v=u+a*v;
then v-a*v = u+(a*v-a*v) by RLVECT_1:def 3
.= u+0.V by VECTSP_1:16
.= u by RLVECT_1:def 4;
then u = 1_K*v+-a*v by VECTSP_1:def 17
.= 1_K*v+(-a)*v by VECTSP_1:21
.= (1_K-a)*v by VECTSP_1:def 15;
then
A21: {v,u} is linearly-dependent by A4,VECTSP_7:5;
{v,u} c= U by A2,A3,ZFMISC_1:32;
hence thesis by A1,A21,VECTSP_7:1;
end;
then not ua in Carrier LLv by A19,TARSKI:def 1;
then
A22: LLv.ua=0.K by VECTSP_6:2;
A23: u + a * v <> 0.V
proof
{v,u} c= U by A2,A3,ZFMISC_1:32;
then
A24: {v,u} is linearly-independent by A1,VECTSP_7:1;
A25: 1_K*u = u by VECTSP_1:def 17;
assume 0.V=u + a * v;
then 1_K=0.K by A4,A24,A25,VECTSP_7:6;
hence thesis;
end;
A26: u<>0.V by A1,A2,VECTSP_7:2;
Lua.ua * ua = ua by A15,VECTSP_6:17
.= 1_K*ua by VECTSP_1:def 17;
then
A27: Lua.ua=1_K by A23,VECTSP10:4;
u in {u} by TARSKI:def 1;
then u in Lin{u} by VECTSP_7:8;
then consider Lu be Linear_Combination of {u} such that
A28: u=Sum Lu by VECTSP_7:7;
reconsider LLu=L.ua * Lu as Linear_Combination of {u} by VECTSP_6:31;
A29: Carrier LLu c= {u} by VECTSP_6:def 4;
then not ua in Carrier LLu by A5,TARSKI:def 1;
then
A30: LLu.ua=0.K by VECTSP_6:2;
{u} c= U by A2,ZFMISC_1:31;
then
A31: Carrier LLu c= U by A29;
L+ LLv+LLu-LLua = L+(LLv+LLu)-LLua by VECTSP_6:26
.= L+(LLv+LLu)+(-LLua) by VECTSP_6:def 11
.= L+(LLv+LLu+(-LLua)) by VECTSP_6:26
.= L+ (LLv+LLu-LLua) by VECTSP_6:def 11;
then
A32: Carrier (L+ LLv+LLu-LLua)c=Carrier L\/Carrier (LLv+LLu-LLua) by
VECTSP_6:23;
A33: Carrier (LLv+LLu-LLua) c= Carrier (LLv+LLu) \/Carrier LLua by
VECTSP_6:41;
A34: Carrier (LLv+ LLu) c= Carrier LLv \/ Carrier LLu by VECTSP_6:23;
{v} c= U by A3,ZFMISC_1:31;
then Carrier LLv c= U by A19;
then Carrier LLv \/ Carrier LLu c= U by A31,XBOOLE_1:8;
then Carrier (LLv+ LLu) c= U by A34;
then Carrier(LLv+LLu)\/Carrier LLua c= U\/{ua} by A16,XBOOLE_1:13;
then Carrier (LLv+LLu-LLua) c= U\/{ua} by A33;
then Carrier L\/Carrier (LLv+LLu-LLua)c=U\/{ua} by A14,XBOOLE_1:8;
then
A35: Carrier (L+ LLv+LLu-LLua) c= U\/{ua} by A32;
A36: (L+ LLv+LLu-LLua).ua=(L+ LLv+LLu+(-LLua)).ua by VECTSP_6:def 11
.= (L+ LLv+LLu).ua + (-LLua).ua by VECTSP_6:22
.= (L+ LLv).ua+ LLu.ua + (-LLua).ua by VECTSP_6:22
.= L.ua+ 0.K+ 0.K + (-LLua).ua by A22,A30,VECTSP_6:22
.= L.ua+ 0.K + (-LLua).ua by RLVECT_1:def 4
.= L.ua+(-LLua).ua by RLVECT_1:def 4
.= L.ua-LLua.ua by VECTSP_6:36
.= L.ua - L.ua*1_K by A27,VECTSP_6:def 9
.= L.ua - L.ua
.= 0.K by VECTSP_1:19;
Carrier (L+ LLv+LLu-LLua) c= U
proof
let x be object;
assume
A37: x in Carrier (L+ LLv+LLu-LLua);
assume not x in U;
then
A38: x in {ua} by A35,A37,XBOOLE_0:def 3;
ex v be Element of V st x=v & (L+ LLv+LLu-LLua).v<>0.K by A37,
VECTSP_6:1;
hence contradiction by A36,A38,TARSKI:def 1;
end;
then reconsider LLL=L+LLv+LLu-LLua as Linear_Combination of U by
VECTSP_6:def 4;
A39: not u in Uu by ZFMISC_1:56;
not u in {ua} by A5,TARSKI:def 1;
then not u in Carrier L by A13,A39,XBOOLE_0:def 3;
then
A40: L.u=0.K by VECTSP_6:2;
Lu.u * u = u by A28,VECTSP_6:17
.= 1_K*u by VECTSP_1:def 17;
then
A41: Lu.u=1_K by A26,VECTSP10:4;
LLL.u = (L+ LLv+LLu+(-LLua)).u by VECTSP_6:def 11
.= (L+ LLv+LLu).u + (-LLua).u by VECTSP_6:22
.= (L+ LLv).u+ LLu.u + (-LLua).u by VECTSP_6:22
.= L.u+ LLv.u+ LLu.u + (-LLua).u by VECTSP_6:22
.= 0.K+ 0.K + LLu.u -0.K by A20,A17,A40,VECTSP_6:36
.= 0.K+LLu.u -0.K by RLVECT_1:def 4
.= LLu.u-0.K by RLVECT_1:def 4
.= LLu.u by VECTSP_1:18
.= L.ua*1_K by A41,VECTSP_6:def 9
.= L.ua;
then
A42: u in Carrier LLL by A12,VECTSP_6:1;
Sum (L+ LLv+LLu-LLua)=Sum (L+LLv+LLu) - Sum LLua by VECTSP_6:47
.= Sum (L+LLv)+ Sum LLu - Sum LLua by VECTSP_6:44
.= Sum L+ Sum LLv+ Sum LLu - Sum LLua by VECTSP_6:44
.= Sum L+ Sum LLv+ Sum LLu - L.ua * ua by A15,VECTSP_6:45
.= Sum L+ Sum LLv+ (L.ua)*u - L.ua * ua by A28,VECTSP_6:45
.= Sum L+ (a*L.ua)*v+ (L.ua)*u-L.ua*ua by A18,VECTSP_6:45
.= Sum L+L.ua*(a*v)+L.ua*u-L.ua*ua by VECTSP_1:def 16
.= Sum L+(L.ua*(a*v) + L.ua*u)-L.ua*ua by RLVECT_1:def 3
.= Sum L+ L.ua*(a*v+ u)- L.ua*ua by VECTSP_1:def 14
.= Sum L+ (L.ua*ua- L.ua*ua) by RLVECT_1:def 3
.= 0.V+ 0.V by A6,VECTSP_1:16
.= 0.V by RLVECT_1:def 4;
hence Carrier L={} by A1,A42;
end;
end;
hence thesis;
end;
end;
theorem Th116:
for V be VectSp of K for u, v be Vector of V holds x in Lin {u,
v} iff ex a,b st x = a * u + b * v
proof
let V be VectSp of K;
let u, v be Vector of V;
per cases;
suppose
A1: u=v;
then
A2: {u,v}={u} by ENUMSET1:29;
thus x in Lin {u,v} implies ex a,b st x = a * u + b * v
proof
assume x in Lin{u,v};
then consider a such that
A3: x=a*u by A2,VECTSP10:3;
x = a*u+0.V by A3,RLVECT_1:def 4
.= a*u+0.K*v by VECTSP10:1;
hence thesis;
end;
given a,b such that
A4: x = a * u + b * v;
x=(a+b)*u by A1,A4,VECTSP_1:def 15;
hence thesis by A2,VECTSP10:3;
end;
suppose
A5: u<>v;
thus x in Lin {u,v} implies ex a,b st x = a * u + b * v
proof
assume x in Lin {u,v};
then consider L be Linear_Combination of {u,v} such that
A6: x=Sum L by VECTSP_7:7;
x=L.u*u+L.v*v by A5,A6,VECTSP_6:18;
hence thesis;
end;
deffunc F(set) = 0.K;
given a,b such that
A7: x = a * u + b * v;
consider L be Function of the carrier of V, the carrier of K such that
A8: L.u = a & L.v=b and
A9: for z be Element of V st z <> u & z<>v holds L.z = F(z) from
FUNCT_2:sch 7(A5);
reconsider L as Element of Funcs(the carrier of V,the carrier of K) by
FUNCT_2:8;
now
let z be Vector of V such that
A10: not z in {u,v};
A11: z<>u by A10,TARSKI:def 2;
z <> v by A10,TARSKI:def 2;
hence L.z = 0.K by A9,A11;
end;
then reconsider L as Linear_Combination of V by VECTSP_6:def 1;
Carrier L c= {u,v}
proof
let x be object such that
A12: x in Carrier L;
L.x <> 0.K by A12,VECTSP_6:2;
then x = v or x=u by A9,A12;
hence thesis by TARSKI:def 2;
end;
then reconsider L as Linear_Combination of {u,v} by VECTSP_6:def 4;
Sum(L) = x by A5,A7,A8,VECTSP_6:18;
hence thesis by VECTSP_7:7;
end;
end;
theorem Th117:
for M st lines M is linearly-independent & M is
without_repeated_line for i,j st j in Seg len M & i <> j holds RLine(M,i,Line(M
,i) + a*Line(M,j)) is without_repeated_line & lines RLine(M,i,Line(M,i) + a*
Line(M,j)) is linearly-independent
proof
let M such that
A1: lines M is linearly-independent and
A2: M is without_repeated_line;
set V=n-VectSp_over K;
let i,j such that
A3: j in Seg len M and
A4: i<>j;
set Lj=Line(M,j);
set Li=Line(M,i);
set R=RLine(M,i,Li+a*Lj);
per cases;
suppose
not i in Seg len M;
hence thesis by A1,A2,Th40;
end;
suppose
A5: i in Seg len M;
reconsider N=n as Element of NAT by ORDINAL1:def 12;
A6: dom M=Seg len M by FINSEQ_1:def 3;
then
A7: M.i<>M.j by A2,A3,A4,A5;
A8: len M=m by MATRIX_0:def 2;
then
A9: Lj in lines M by A3,Th103;
A10: Li in lines M by A5,A8,Th103;
then reconsider LI=Li,LJ=Lj as Vector of V by A9;
reconsider li=LI,lj=LJ as Element of N-tuples_on the carrier of K by Th102;
A11: M.i=Li by A5,A8,MATRIX_0:52;
m <> 0 by A5,A8;
then
A12: n=width M by Th1;
A13: M.j=Lj by A3,A8,MATRIX_0:52;
A14: for k st k in Seg m & k<>i holds Line(R,k)<>Li + a*Lj
proof
a*lj = a*LJ by Th102;
then li+a*lj = LI+a*LJ by Th102
.= (1_K)*LI+a*LJ by VECTSP_1:def 17;
then
A15: li+a*lj in Lin {LI,LJ} by Th116;
let k such that
A16: k in Seg m and
A17: k<>i;
set Lk=Line(M,k);
assume
A18: Line(R,k)=Li+a*Lj;
A19: Line(R,k) = Line(M,k) by A16,A17,MATRIX11:28;
A20: Lj<>Lk
proof
{LI,LJ} c= lines M by A10,A9,ZFMISC_1:32;
then
A21: {LI,LJ} is linearly-independent by A1,VECTSP_7:1;
assume
A22: Lj=Lk;
A23: (1_K+(-1_K)*a)*LJ=(1_K+(-1_K)*a)*lj by Th102;
A24: (-1_K)*LI=(-1_K)*li by Th102;
0.V = n|->0.K by Th102
.= lj+-(li+a*lj) by A19,A18,A22,FVSUM_1:26
.= lj+(-li+-a*lj) by FVSUM_1:31
.= lj+((-1_K)*li+-a*lj) by FVSUM_1:59
.= lj+((-1_K)*li+(-1_K)*(a*lj)) by FVSUM_1:59
.= lj+((-1_K)*li+((-1_K)*a)*lj) by FVSUM_1:54
.= lj+(((-1_K)*a)*lj+(-1_K)*li) by FINSEQOP:33
.= lj+((-1_K)*a)*lj+(-1_K)*li by FINSEQOP:28
.= 1_K*lj+((-1_K)*a)*lj+(-1_K)*li by FVSUM_1:57
.= (1_K+(-1_K)*a)*lj+(-1_K)*li by FVSUM_1:55
.= (1_K+(-1_K)*a)*LJ+(-1_K)*LI by A24,A23,Th102;
then -1_K=0.K by A7,A11,A13,A21,VECTSP_7:6;
hence thesis by VECTSP_1:28;
end;
A25: Lk in lines M by A16,Th103;
then reconsider LK=Lk as Vector of V;
reconsider KIJ={LK,LI,LJ} as Subset of V;
A26: KIJ is linearly-independent by A1,A10,A9,A25,VECTSP_7:1,ZFMISC_1:133;
A27: Lk in KIJ by ENUMSET1:def 1;
A28: M.k=Lk by A16,MATRIX_0:52;
M.i<>M.k by A2,A5,A8,A6,A16,A17;
then KIJ \ {LK} = {LI, LJ} by A11,A20,A28,ENUMSET1:86;
hence thesis by A19,A18,A15,A27,A26,VECTSP_9:14;
end;
reconsider LiaLj=li+a*lj as Element of (the carrier of K)* by
FINSEQ_1:def 11;
reconsider LL=LiaLj as set;
set iLL=i.-->LL;
A29: len (li+a*lj)=n by CARD_1:def 7;
then RLine(M,i,li+a*lj) = Replace(M, i, LiaLj) by A12,MATRIX11:29
.= M+*iLL by A5,A6,FUNCT_7:def 3;
then
A30: lines RLine(M,i,Li+a*Lj) = M.:(dom M\dom iLL)\/rng iLL by FRECHET:12
.= M.:(dom M\{i})\/rng iLL by FUNCOP_1:13
.= M.:(dom M\{i})\/{LL} by FUNCOP_1:8
.= (M.:dom M\M.:{i})\/{LL} by A2,FUNCT_1:64
.= (lines M\Im(M,i))\/{LL} by RELAT_1:113
.= (lines M\{LI})\/{li+a*lj} by A5,A6,A11,FUNCT_1:59;
A31: Line(R,i)=Li+a*Lj by A5,A8,A29,A12,MATRIX11:28;
now
A32: len R=m by MATRIX_0:def 2;
let x1,x2 be object such that
A33: x1 in dom R and
A34: x2 in dom R and
A35: R.x1=R.x2;
reconsider i1=x1,i2=x2 as Element of NAT by A33,A34;
A36: dom R=Seg len R by FINSEQ_1:def 3;
then
A37: R.i1=Line(R,i1) by A33,A32,MATRIX_0:52;
A38: R.i2=Line(R,i2) by A34,A36,A32,MATRIX_0:52;
per cases;
suppose
i1=i & i2=i;
hence x1=x2;
end;
suppose
i1=i & i2<>i or i1<>i & i2=i;
hence x1=x2 by A14,A31,A33,A34,A35,A36,A32,A37,A38;
end;
suppose
A39: i1<>i & i2<>i;
then
A40: R.i2=Line(M,i2) by A34,A36,A32,A38,MATRIX11:28;
A41: Line(M,i1) = M.i1 by A33,A36,A32,MATRIX_0:52;
A42: Line(M,i2) = M.i2 by A34,A36,A32,MATRIX_0:52;
R.i1=Line(M,i1) by A33,A36,A32,A37,A39,MATRIX11:28;
hence x1=x2 by A2,A8,A6,A33,A34,A35,A36,A32,A41,A40,A42;
end;
end;
hence R is without_repeated_line;
A43: a*lj = a*LJ by Th102;
lines M\{LI}\/{LI+a*LJ} is linearly-independent by A1,A7,A11,A13,A10,A9
,Th115;
hence thesis by A43,A30,Th102;
end;
end;
theorem Th118:
P c= Seg m implies lines Segm(M,P,Seg n) c= lines M
proof
set S=Segm(M,P,Seg n);
assume
A1: P c= Seg m;
then
A2: rng Sgm P = P by FINSEQ_1:def 13;
let x be object;
assume x in lines S;
then consider i such that
A3: i in Seg card P and
A4: x = Line(S,i) by Th103;
Seg m <>{} by A1,A3;
then m <> 0;
then width M=n by Th1;
then
A5: Line(S,i)=Line(M,Sgm P.i) by A3,Th48;
dom Sgm P=Seg card P by A1,FINSEQ_3:40;
then Sgm P.i in rng Sgm P by A3,FUNCT_1:def 3;
hence thesis by A1,A4,A2,A5,Th103;
end;
theorem Th119:
P c= Seg m & lines M is linearly-independent implies lines Segm
(M,P,Seg n) is linearly-independent
proof
assume that
A1: P c= Seg m and
A2: lines M is linearly-independent;
card Seg n=n by FINSEQ_1:57;
hence thesis by A1,A2,Th118,VECTSP_7:1;
end;
theorem Th120:
P c= Seg m & M is without_repeated_line implies Segm(M,P,Seg n)
is without_repeated_line
proof
assume that
A1: P c= Seg m and
A2: M is without_repeated_line;
set S=Segm(M,P,Seg n);
let x1,x2 be object such that
A3: x1 in dom S and
A4: x2 in dom S and
A5: S.x1=S.x2;
reconsider i1=x1,i2=x2 as Element of NAT by A3,A4;
len S=card P by MATRIX_0:def 2;
then
A6: dom S=Seg card P by FINSEQ_1:def 3;
then
A7: Line(S,i1)=S.i1 by A3,MATRIX_0:52;
A8: Line(S,i2)=S.i2 by A4,A6,MATRIX_0:52;
A9: Sgm P is one-to-one by A1,FINSEQ_3:92;
A10: dom Sgm P=dom S by A1,A6,FINSEQ_3:40;
Seg m<>{} by A1,A3,A6;
then m <> 0;
then
A11: width M=n by Th1;
then
A12: Line(S,i1) = Line(M,Sgm P.i1) by A3,A6,Th48;
A13: Line(S,i2) = Line(M,Sgm P.i2) by A4,A6,A11,Th48;
A14: len M=m by MATRIX_0:def 2;
A15: rng Sgm P=P by A1,FINSEQ_1:def 13;
then
A16: Sgm P.i2 in P by A4,A10,FUNCT_1:def 3;
then
A17: Line(M,Sgm P.i2)=M.(Sgm P.i2) by A1,MATRIX_0:52;
A18: Sgm P.i1 in P by A3,A10,A15,FUNCT_1:def 3;
then Sgm P.i1 in Seg m by A1;
then
A19: Sgm P.i1 in dom M by A14,FINSEQ_1:def 3;
Sgm P.i2 in Seg m by A1,A16;
then
A20: Sgm P.i2 in dom M by A14,FINSEQ_1:def 3;
Line(M,Sgm P.i1)=M.(Sgm P.i1) by A1,A18,MATRIX_0:52;
then Sgm P.i1=Sgm P.i2 by A2,A5,A12,A13,A7,A8,A17,A19,A20;
hence thesis by A3,A4,A10,A9;
end;
theorem Th121:
for M be Matrix of m,n,K holds lines M is linearly-independent
& M is without_repeated_line iff the_rank_of M = m
proof
defpred P[Nat] means for m,n st m=$1 for M be Matrix of m,n,K holds lines M
is linearly-independent & M is without_repeated_line iff the_rank_of M = m;
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
let m,n such that
A3: m=k+1;
let M be Matrix of m,n,K;
thus lines M is linearly-independent & M is without_repeated_line implies
the_rank_of M = m
proof
A4: k0.K)=n by CARD_1:def 7;
k n |-> 0.K by A9,A10,A7,Th109;
then consider i such that
A11: 1<=i and
A12: i<=n and
A13: LM.i<>(n|->0.K).i by A8,A5;
defpred Q[Nat] means $10.K by A13,FINSEQ_2:57;
len Line(M,m)=width M by MATRIX_0:def 7;
then
A16: LM.i=M*(m,i) by A8,A14,MATRIX_0:def 7;
A17: for l st Q[l] holds Q[l+1]
proof
set Mmi=M*(m,i);
let L be Nat such that
A18: Q[L];
set L1=L+1;
assume
A19: L1 0 by A26;
then
A27: width M1=n by Th1;
then
A28: LML.i=MLi by A14,MATRIX_0:def 7;
0+1<=L1 by NAT_1:13;
then
A29: L1 in Seg m by A19;
len (LML+(-(Mmi"*MLi))*LMm) = width M1 by CARD_1:def 7;
then
A30: Line(R,L1) = LML+(-(Mmi"*MLi))*LMm by A29,MATRIX11:28;
m <> 0 by A26;
then
width M=n by Th1;
then LMm.i=M*(m,i) by A14,A20,MATRIX_0:def 7;
then ((-(Mmi"*MLi))*LMm).i=(-(Mmi" * MLi)) *Mmi by A14,A27,FVSUM_1:51;
then
A31: Line(R,L1).i = MLi+(-(Mmi" * MLi)) *Mmi by A14,A27,A28,A30,FVSUM_1:18
.= MLi+(-(1_K*(Mmi" * MLi))) *Mmi
.= MLi+(-1_K)*(Mmi" * MLi) *Mmi by VECTSP_1:9
.= MLi+(-1_K)*(Mmi" * MLi *Mmi) by GROUP_1:def 3
.= MLi+(-1_K)*(Mmi" * Mmi* MLi ) by GROUP_1:def 3
.= MLi+(-1_K)*(1_K* MLi) by A15,A16,VECTSP_1:def 10
.= MLi+(-1_K)*MLi
.= MLi+(-(1_K)*MLi) by VECTSP_1:9
.= MLi+(-MLi)
.= 0.K by RLVECT_1:5;
m <> 0 by A26;
then
A32: width R=n by Th1;
per cases by A25,NAT_1:9;
suppose
j=L1;
hence thesis by A14,A32,A31,MATRIX_0:def 7;
end;
suppose
A33: j<=L;
then
A34: j0.K by Def4;
P={} iff Q={} by A52;
then consider P1,Q1 such that
A55: P1 c= Seg k and
A56: Q1 c= Seg width S\{i} and
P1 = (Sgm Seg k).:P and
Q1=Sgm (Seg width S\{i}).:Q and
A57: card P1=card P and
A58: card Q1=card Q and
A59: Segm(SSS,P,Q) = Segm(S,P1,Q1) by A51,Th57;
Seg width S\{i} c= Seg width S by XBOOLE_1:36;
then
A60: Q1 c= Seg width S by A56;
then [:P1,Q1:] c= [:Seg k,Seg width S:] by A55,ZFMISC_1:96;
then
A61: [:P1,Q1:] c= Indices S by A42,FINSEQ_1:def 3;
A62: now
per cases;
suppose
k=0;
then width S=0 by A42,MATRIX_0:def 3;
then Seg width S c= Seg n;
hence Q1 c= Seg n by A60;
end;
suppose
k>0;
hence Q1 c= Seg n by A43,A60,Th1;
end;
end;
P1={} iff Q1={} by A52,A57,A58;
then consider P2,Q2 such that
A63: P2 c= Seg k and
A64: Q2 c= Seg n and
A65: P2= Sgm (Seg k).:P1 and
A66: Q2=Sgm (Seg n).:Q1 and
A67: card P2=card P1 and
A68: card Q2=card Q1 and
A69: Segm(S,P1,Q1) = Segm(M1,P2,Q2) by A61,Th57;
A70: Q2 = (idseq n).:Q1 by A66,FINSEQ_3:48
.= Q1 by A62,FRECHET:13;
reconsider i,m as non zero Element of NAT by A3,A11,ORDINAL1:def 12;
set Q2i=Q2\/{i};
set SQ2i=Sgm Q2i;
A71: {i} c= Seg n by A14,ZFMISC_1:31;
then
A72: Q2i c= Seg n by A64,XBOOLE_1:8;
then
A73: rng SQ2i=Q2i by FINSEQ_1:def 13;
A74: P2 = (idseq k).:P1 by A65,FINSEQ_3:48
.= P1 by A55,FRECHET:13;
A75: EqSegm(SSS,P,Q) = Segm(S,P1,Q1) by A52,A59,Def3
.= EqSegm(M1,P1,Q1) by A52,A57,A58,A69,A74,A70,Def3;
A76: len EqSegm(M1,P2,Q2)=k by A53,A57,A67,MATRIX_0:def 2;
A77: len M1=m by Th1;
then
A78: the_rank_of M1 <= m by Th74;
set P2m=P2\/{m};
set ES=EqSegm(M1,P2m,Q2i);
A79: P2 c= Seg m by A6,A63;
i in {i} by TARSKI:def 1;
then
A80: i in Q2i by XBOOLE_0:def 3;
i in {i} by TARSKI:def 1;
then
A81: not i in Q2 by A56,A70,XBOOLE_0:def 5;
then
A82: card Q2i=m by A3,A52,A53,A58,A68,CARD_2:41;
then dom SQ2i=Seg m by A64,A71,FINSEQ_3:40,XBOOLE_1:8;
then consider Si be object such that
A83: Si in Seg m and
A84: SQ2i.Si=i by A80,A73,FUNCT_1:def 3;
reconsider Si as Element of NAT by A83;
km;
reconsider J=j as Element of NAT by ORDINAL1:def 12;
j<=m by A98,FINSEQ_1:1;
then j<=k by A3,A99,NAT_1:9;
then 0.K = M1*(j,i) by A40,A98
.= ES*(j,Si) by A91,A98;
hence 0.K = ES*(j,Si)*Cofactor(ES,J,Si)
.= LC.j by A97,A98,LAPLACE:def 8;
end;
then
A100: LC.m = Sum LC by A7,A97,MATRIX_3:12
.= Det ES by A86,A83,LAPLACE:27;
reconsider mSi=m+Si as Element of NAT;
-1_K<>0.K by VECTSP_1:28;
then
A101: power(K).(-1_K,mSi)<>0.K by Lm6;
Sgm P2m.m = (idseq m).m by A90,FINSEQ_3:48
.= m by A7,FINSEQ_2:49;
then Delete(ES,m,Si) = EqSegm(M1,P2m\{m},Q2i\{i}) by A7,A86,A82,A83,A84
,Th64
.= EqSegm(M1,P2,Q2i\{i}) by A85,ZFMISC_1:117
.= EqSegm(M1,P2,Q2) by A81,ZFMISC_1:117;
then power(K).(-1_K,mSi)*Minor(ES,m,Si)<>0.K by A53,A54,A74,A70,A75,A86
,A87,A76,A101,VECTSP_1:12;
then ES*(m,Si)* Cofactor(ES,m,Si)<>0.K by A15,A96,VECTSP_1:12;
then Det ES<>0.K by A7,A97,A100,LAPLACE:def 8;
then the_rank_of M1 >= m by A89,A86,A82,Def4;
hence thesis by A39,A78,XXREAL_0:1;
end;
thus thesis by Th105,Th110;
end;
A102: P[0]
proof
let m,n such that
A103: m=0;
let M be Matrix of m,n,K;
len M=0 by A103,MATRIX_0:def 2;
then M={};
hence thesis by A103,Th74;
end;
for k holds P[k] from NAT_1:sch 2(A102,A1);
hence thesis;
end;
theorem Th122:
for U be Subset of n-VectSp_over K st U c= lines M ex P st P c=
Seg m & lines Segm(M,P,Seg n) = U & Segm(M,P,Seg n) is without_repeated_line
proof
defpred P[object,object] means
ex i st i in Seg m & Line(M,i)=$1 & $2=i;
let U be Subset of n-VectSp_over K such that
A1: U c= lines M;
A2: for x being object st x in U ex y being object st y in Seg m & P[x,y]
proof
let x be object;
assume x in U;
then consider i such that
A3: i in Seg m and
A4: x=Line(M,i) by A1,Th103;
take i;
thus thesis by A3,A4;
end;
consider f be Function of U,Seg m such that
A5: for x being object st x in U holds P[x,f.x] from FUNCT_2:sch 1(A2);
A6: rng f c= Seg m by RELAT_1:def 19;
then not 0 in rng f;
then reconsider P=rng f as without_zero finite Subset of NAT by A6,
MEASURE6:def 2,XBOOLE_1:1;
set S=Segm(M,P,Seg n);
A7: rng Sgm P=P by A6,FINSEQ_1:def 13;
A8: lines S c= U
proof
A9: rng Sgm P=P by A6,FINSEQ_1:def 13;
let x be object;
A10: dom S = Seg len S by FINSEQ_1:def 3
.= Seg card P by MATRIX_0:def 2;
assume
A11: x in lines S;
then consider y being object such that
A12: y in dom S and
A13: S.y=x by FUNCT_1:def 3;
lines S c= lines M by A6,Th118;
then
A14: M<>{} by A11;
len M=m by MATRIX_0:def 2;
then
A15: width M=n by A14,Th1;
reconsider y as Element of NAT by A12;
dom Sgm P = Seg card P by A6,FINSEQ_3:40;
then Sgm P.y in rng Sgm P by A12,A10,FUNCT_1:def 3;
then consider z be object such that
A16: z in dom f and
A17: f.z=Sgm P.y by A9,FUNCT_1:def 3;
ex i st i in Seg m & Line(M,i)=z & f.z=i by A5,A16;
then z = Line(S,y) by A12,A10,A17,A15,Th48
.= x by A12,A13,A10,MATRIX_0:52;
hence thesis by A16;
end;
take P;
thus P c= Seg m by RELAT_1:def 19;
U c= lines S
proof
let x be object;
A18: dom Sgm P=Seg card P by A6,FINSEQ_3:40;
assume
A19: x in U;
then consider i such that
A20: i in Seg m and
A21: Line(M,i)=x and
A22: f.x=i by A5;
dom f=U by A20,FUNCT_2:def 1;
then i in P by A19,A22,FUNCT_1:def 3;
then i in rng Sgm P by A6,FINSEQ_1:def 13;
then consider y being object such that
A23: y in dom Sgm P and
A24: Sgm P.y=i by FUNCT_1:def 3;
reconsider y as Element of NAT by A23;
m <> 0 by A20;
then
width M=n by Th1;
then Line(S,y)=x by A21,A23,A24,A18,Th48;
hence thesis by A23,A18,Th103;
end;
hence U=lines S by A8,XBOOLE_0:def 10;
let x1,x2 be object such that
A25: x1 in dom S and
A26: x2 in dom S and
A27: S.x1=S.x2;
A28: dom S = Seg len S by FINSEQ_1:def 3
.= Seg card P by MATRIX_0:def 2;
then
A29: dom Sgm P=dom S by A6,FINSEQ_3:40;
reconsider i1=x1,i2=x2 as Element of NAT by A25,A26;
A30: dom Sgm P = Seg card P by A6,FINSEQ_3:40;
then Sgm P.i1 in rng Sgm P by A25,A28,FUNCT_1:def 3;
then consider y1 be object such that
A31: y1 in dom f and
A32: f.y1=Sgm P.i1 by A7,FUNCT_1:def 3;
A33: ex j1 be Nat st j1 in Seg m & Line(M,j1)=y1 & f.y1=j1 by A5,A31;
then m <> 0;
then
A34: width M=n by Th1;
Sgm P.i2 in rng Sgm P by A26,A28,A30,FUNCT_1:def 3;
then consider y2 be object such that
A35: y2 in dom f and
A36: f.y2=Sgm P.i2 by A7,FUNCT_1:def 3;
ex j2 be Nat st j2 in Seg m & Line(M,j2)=y2 & f.y2=j2 by A5,A35;
then
A37: Line(S,i2)=y2 by A26,A28,A36,A34,Th48;
A38: Sgm P is one-to-one by A6,FINSEQ_3:92;
A39: Line(S,i1)=S.i1 by A25,A28,MATRIX_0:52;
Line(S,i1)=y1 by A25,A28,A32,A33,A34,Th48;
then Sgm P.i1=Sgm P.i2 by A26,A27,A28,A32,A36,A37,A39,MATRIX_0:52;
hence thesis by A25,A26,A29,A38;
end;
theorem
for RANK be Element of NAT holds the_rank_of M = RANK iff (ex U be
finite Subset of n-VectSp_over K st U is linearly-independent & U c= lines M &
card U = RANK) & for W be finite Subset of n-VectSp_over K st W is
linearly-independent & W c= lines M holds card W <= RANK
proof
let R be Element of NAT;
A1: len M=m by MATRIX_0:def 2;
A2: card Seg n=n by FINSEQ_1:57;
A3: for W be finite Subset of n-VectSp_over K st W is linearly-independent
& W c= lines M holds card W <= the_rank_of M
proof
let W be finite Subset of n-VectSp_over K such that
A4: W is linearly-independent and
A5: W c= lines M;
consider P1 such that
A6: P1 c= Seg m and
A7: lines Segm(M,P1,Seg n) = W and
A8: Segm(M,P1,Seg n) is without_repeated_line by A5,Th122;
set S1=Segm(M,P1,Seg n);
A9: S1.:dom S1=lines S1 by RELAT_1:113;
dom S1,S1.:dom S1 are_equipotent by A8,CARD_1:33;
then
A10: card W = card dom S1 by A7,A9,CARD_1:5
.= card Seg len S1 by FINSEQ_1:def 3
.= card Seg card P1 by MATRIX_0:def 2
.= card P1 by FINSEQ_1:57;
per cases;
suppose
card P1=0;
hence thesis by A10;
end;
suppose
card P1>0;
then
Seg m <>{} by A6;
then
A11: m <> 0;
then
A12: len M=m by Th1;
width M=n by Th1,A11;
then [:P1,Seg n:] c= [:Seg len M,Seg width M:] by A6,A12,ZFMISC_1:96;
then [:P1,Seg n:] c= Indices M by FINSEQ_1:def 3;
then the_rank_of S1 <= the_rank_of M by Th79;
hence thesis by A2,A4,A7,A8,A10,Th121;
end;
end;
A13: now
per cases;
suppose
len M=0;
then width M=0 by MATRIX_0:def 3;
hence Seg width M c= Seg n;
end;
suppose
len M>0;
then m>0 by MATRIX_0:def 2;
hence Seg width M c= Seg n by Th1;
end;
end;
consider P,Q such that
A14: [:P,Q:] c= Indices M and
A15: card P = card Q and
A16: card P = the_rank_of M and
A17: Det EqSegm(M,P,Q)<>0.K by Def4;
Q c= Seg width M by A14,A15,Th67;
then
A18: Q c= Seg n by A13;
set S=Segm(M,P,Seg n);
A19: len S=card P by MATRIX_0:def 2;
Segm(M,P,Q)=EqSegm(M,P,Q) by A15,Def3;
then
A20: the_rank_of EqSegm(M,P,Q) <= the_rank_of S by A18,Th80;
A21: the_rank_of S<=len S by Th74;
the_rank_of EqSegm(M,P,Q) = card P by A17,Th83;
then
A22: the_rank_of S = card P by A20,A19,A21,XXREAL_0:1;
then
A23: lines S is linearly-independent by Th121;
S is without_repeated_line by A22,Th121;
then
A24: dom S,S.:dom S are_equipotent by CARD_1:33;
S.:dom S=lines S by RELAT_1:113;
then
A25: card lines S = card dom S by A24,CARD_1:5
.= card Seg len S by FINSEQ_1:def 3
.= card Seg card P by MATRIX_0:def 2
.= card P by FINSEQ_1:57;
A26: P c= Seg len M by A14,A15,Th67;
then lines S c= lines M by A1,Th118;
hence the_rank_of M = R implies (ex U be finite Subset of n-VectSp_over K st
U is linearly-independent & U c= lines M & card U = R) & for W be finite Subset
of n-VectSp_over K st W is linearly-independent & W c= lines M holds card W <=
R by A16,A23,A25,A2,A3;
assume that
A27: ex U be finite Subset of n-VectSp_over K st U is
linearly-independent & U c= lines M & card U = R and
A28: for W be finite Subset of n-VectSp_over K st W is
linearly-independent & W c= lines M holds card W <= R;
A29: R <= the_rank_of M by A3,A27;
the_rank_of M <= R by A16,A23,A25,A26,A1,A2,A28,Th118;
hence thesis by A29,XXREAL_0:1;
end;