:: Solutions of Linear Equations :: by Karol P\c{a}k :: :: Received December 18, 2007 :: Copyright (c) 2007 Association of Mizar Users environ vocabularies TARSKI, BOOLE, ARYTM, ARYTM_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_7, TREES_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, FINSOP_1, FUNCOP_1, INCSP_1, CAT_1, CAT_3, RVSUM_1, RLSUB_1, GROUP_1, BINOP_1, SETWISEO, FINSET_1, SGRAPH1, CARD_1, CARD_3, INT_1, QC_LANG1, ROUGHS_1, GR_CY_1, FREEALG, FSM_1, XREAL_0, SEQ_1, MATRIX_1, MATRIX_2, MATRIX_3, MATRIX11, LAPLACE, MATRIX13, MATRIXR1, RLVECT_1, RLVECT_2, RLVECT_3, VECTSP_1, VECTSP_9, PRVECT_1, LMOD_7, COMPLEX1, CLASSES1, MEASURE6, RELOC, MATRIX_6, MATRIX15, ALGSTR_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, NAT_1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, SETWOP_2, FINSEQ_1, BINOP_1, STRUCT_0, FUNCOP_1, RLVECT_1, GROUP_1, VECTSP_1, SETWISEO, FINSEQ_2, MATRIX_1, MATRIX_2, FVSUM_1, FINSOP_1, BINARITH, GROUP_4, MATRIX_3, MATRIX_6, MATRIX_7, FINSEQ_7, FUNCT_4, DOMAIN_1, MATRIX11, PSCOMP_1, PRVECT_1, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, FINSEQOP, MATRIX13, MATRLIN, FUNCT_7, PNPROC_1, LAPLACE; constructors SETWISEO, FINSOP_1, ALGSTR_1, FVSUM_1, SEQM_3, XXREAL_0, GROUP_4, FINSEQ_7, WELLORD2, VECTSP_6, VECTSP_7, VECTSP_9, VALUED_0, ALGSTR_0, MATRIX_6, MATRIX_7, MATRIX11, MATRIX13, PNPROC_1, REALSET1, LAPLACE; registrations XBOOLE_0, SUBSET_1, FUNCT_1, FINSET_1, STRUCT_0, FVSUM_1, MATRIX_2, VECTSP_1, FUNCT_2, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, RELAT_1, CARD_1, FUNCOP_1, SETFAM_1, FINSEQ_2, SEQM_3, MATRLIN, MATRIX13, XREAL_0, PNPROC_1, VECTSP_9, VECTSP_7, VALUED_0, ALGSTR_0; requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET; definitions TARSKI, XBOOLE_0, RLVECT_1, FINSEQ_1, FINSEQ_2, MATRIX_1, GROUP_4, MATRIX_3, MATRIX_7, VECTSP_4, RELAT_1, LAPLACE, MATRIX13, FVSUM_1, ALGSTR_0; theorems BINARITH, CARD_1, CARD_2, CARD_FIN, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQOP, FINSOP_1, FRECHET, FUNCT_1, FUNCT_2, FUNCT_7, FUNCOP_1, FVSUM_1, GROUP_1, LAPLACE, MATRIX_1, MATRIX_2, MATRIX_3, MATRIX_4, MATRIX_5, MATRIX_6, MATRIX_7, MATRIX11, MATRIX13, MATRIXR1, MATRIXR2, MATRLIN, NAT_1, ORDINAL1, PARTFUN1, PNPROC_1, PSCOMP_1, REAL_1, RELAT_1, RELSET_1, RLVECT_1, STIRL2_1, STRUCT_0, TARSKI, WELLORD2, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ZFMISC_1; schemes FINSEQ_2, NAT_1, MATRIX_1; begin :: Preliminaries reserve x,y for set, i,j,k,l,m,n for Nat, K for Field, N for without_zero finite Subset of NAT, a,b for Element of K, A,B,B1,B2,X,X1,X2 for (Matrix of K), A' for (Matrix of m,n,K), B' for (Matrix of m,k,K), M for Matrix of n,K; theorem Th1: width A = len B implies (a*A) * B = a * (A*B) proof assume A1: width A=len B; set aA=a*A; set AB=A*B; set aAB=a*AB; A2: len aA=len A & width aA=width A & len aAB=len AB & width aAB=width AB & width AB=width B by A1,MATRIX_3:def 4,def 5; then A3: len aAB = len A & len aA=len (aA*B) & width aAB = width B & width B=width (aA*B) by A1,MATRIX_3:def 4; now let i,j such that A4: [i,j] in Indices aAB; A5: dom AB = Seg len AB by FINSEQ_1:def 3 .= dom (aA*B) by A3,A2,FINSEQ_1:def 3; A6: [i,j] in Indices AB by A4,MATRIXR1:18; then i in dom AB & j in Seg width AB by ZFMISC_1:106; then i in Seg len A & i in dom (aA*B) & j in Seg width (aA*B) by A2,A3,A5,FINSEQ_1:def 3; then A7: 1<=i & i<=len A & [i,j] in Indices (aA*B) by ZFMISC_1:106,FINSEQ_1 :3; thus aAB*(i,j) = a*(AB*(i,j)) by MATRIX_3:def 5,A6 .= a*(Line(A,i)"*"Col(B,j)) by A1,MATRIX_3:def 4,A6 .= Sum(a*mlt(Line(A,i),Col(B,j))) by FVSUM_1:92 .= Sum(mlt(a*Line(A,i),Col(B,j))) by A1,FVSUM_1:82 .= Line(aA,i)"*"Col(B,j) by A7,MATRIXR1:20 .= (aA*B)*(i,j) by A1,A2,A7,MATRIX_3:def 4; end; hence aAB=aA*B by A2,A3,MATRIX_1:21; end; theorem Th2: 1_K * A = A & a * (b * A) = (a * b) * A proof set 1A=1_K*A; set bA=b*A; set ab=a*b; set abA=ab*A; A1: len 1A=len A&width 1A=width A by MATRIX_3:def 5; A2: now let i,j such that A3: [i,j] in Indices A; thus A*(i,j) = 1_K*(A*(i,j)) by VECTSP_1:def 16 .= 1A*(i,j) by A3,MATRIX_3:def 5; end; A4: len(a*bA) = len bA by MATRIX_3:def 5 .= len A by MATRIX_3:def 5 .= len abA by MATRIX_3:def 5; A5: width(a*bA) = width bA by MATRIX_3:def 5 .= width A by MATRIX_3:def 5 .= width abA by MATRIX_3:def 5; now let i,j such that A6: [i,j] in Indices (a*bA); A7: Indices (a*bA)=Indices bA &Indices bA=Indices A &Indices A=Indices abA by MATRIXR1:18; hence (a*bA)*(i,j) = a*(bA*(i,j)) by A6,MATRIX_3:def 5 .= a*(b*(A*(i,j))) by A6,A7,MATRIX_3:def 5 .= (a*b)*(A*(i,j)) by GROUP_1:def 4 .= abA*(i,j) by A6,A7,MATRIX_3:def 5; end; hence thesis by A1,A2,A4,A5,MATRIX_1:21; end; Lm1: Indices A=Indices -A proof dom A = Seg len A by FINSEQ_1:def 3 .= Seg len (-A) by MATRIX_3:def 2 .= dom (-A) by FINSEQ_1:def 3; hence thesis by MATRIX_3:def 2; end; Lm2: a <> 0.K implies power(K).(a,n)<>0.K proof assume A1: a<>0.K; defpred P[Nat] means for n st n=$1 holds power(K).(a,n)<>0.K; A2: P[0] proof let n such that A3: n=0; 1_K<>0.K; hence thesis by A3,GROUP_1:def 8; end; A4: for k st P[k] holds P[k+1] proof let k such that A5: P[k]; let n such that A6: n=k+1; k in NAT & n in NAT by ORDINAL1:def 13; then power(K).(a,n)=power(K).(a,k) * a & power(K).(a,k) <> 0.K by A5,A6,GROUP_1:def 8; hence thesis by A1,VECTSP_1:44; end; for k holds P[k] from NAT_1:sch 2(A2,A4); hence thesis; end; theorem Th3: for K be non empty addLoopStr, f,g,h,w be FinSequence of K st len f=len g & len h = len w holds (f^h) + (g^w)= (f+g) ^ (h+w) proof let K be non empty addLoopStr, f,g,h,w be FinSequence of K such that A1: len f=len g & len h = len w; set KK=the carrier of K; reconsider F=f,G=g as Element of (len f)-tuples_on KK by A1,FINSEQ_2:110; reconsider H=h,W=w as Element of (len h)-tuples_on KK by A1,FINSEQ_2:110; reconsider FH=F^H,GW=G^W,Th36W=(F+G)^(H+W) as Element of (len f+len h)-tuples_on KK by FINSEQ_2:127; now let i such that A2: i in Seg (len f+len h); A3: i in dom FH by A2,FINSEQ_2:144; now per cases by A3,FINSEQ_1:38; suppose A4: i in dom f; A5: dom F=Seg len f & dom G=Seg len f & dom (F+G)=Seg len f by FINSEQ_2:144; then f.i in rng f & rng f c= KK & g.i in rng g & rng g c= KK by A4,FUNCT_1:def 5,RELSET_1:12; then reconsider fi=f.i,gi=g.i as Element of K; FH.i=fi & GW.i=gi by A4,A5,FINSEQ_1:def 7; hence (FH+GW).i = fi+gi by A2,FVSUM_1:22 .= (F+G).i by A4,A5,FVSUM_1:22 .= Th36W.i by A4,A5,FINSEQ_1:def 7; end; suppose ex n st n in dom h & i=len f + n; then consider n such that A6: n in dom h & i=len f + n; A7: dom H=Seg len h & dom W=Seg len h & dom (H+W)=Seg len h &len (F+G)=len f by FINSEQ_2:109,144; then h.n in rng h & rng h c= KK & w.n in rng w & rng w c= KK by A6,FUNCT_1:def 5,RELSET_1:12; then reconsider hn=h.n,wn=w.n as Element of K; FH.i=hn & GW.i=wn by A1,A6,A7,FINSEQ_1:def 7; hence (FH+GW).i = hn+wn by A2,FVSUM_1:22 .= (H+W).n by A6,A7,FVSUM_1:22 .= Th36W.i by A6,A7,FINSEQ_1:def 7; end; end; hence (FH+GW).i=Th36W.i; end; hence thesis by FINSEQ_2:139; end; theorem Th4: for K be non empty multMagma, f,g be FinSequence of K,a be Element of K holds a * (f^g) = (a*f) ^ (a*g) proof let K be non empty multMagma, f,g be FinSequence of K,a be Element of K; set KK=the carrier of K; reconsider F=f as Element of (len f)-tuples_on KK by FINSEQ_2:110; reconsider G=g as Element of (len g)-tuples_on KK by FINSEQ_2:110; reconsider FG=F^G,aFaG=(a*F)^(a*G) as Element of (len f+len g)-tuples_on KK by FINSEQ_2:127; now let i such that A1: i in Seg (len f+len g); A2: i in dom FG by A1,FINSEQ_2:144; now per cases by A2,FINSEQ_1:38; suppose A3: i in dom f; A4: dom F=Seg len f & dom (a*F)=Seg len f by FINSEQ_2:144; f.i in rng f & rng f c= KK by A3,FUNCT_1:def 5,RELSET_1:12; then reconsider fi=f.i as Element of K; FG.i=fi by A3,FINSEQ_1:def 7; hence (a*FG).i = a*fi by A1,FVSUM_1:63 .= (a*F).i by A3,A4,FVSUM_1:63 .= aFaG.i by A3,A4,FINSEQ_1:def 7; end; suppose ex n st n in dom g & i=len f + n; then consider n such that A5: n in dom g & i=len f + n; A6: dom G=Seg len g & dom (a*G)=Seg len g &len (a*F)=len f by FINSEQ_2:109,144; g.n in rng g & rng g c= KK by A5,FUNCT_1:def 5,RELSET_1:12; then reconsider gn=g.n as Element of K; FG.i=gn by A5,FINSEQ_1:def 7; hence (a*FG).i = a*gn by A1,FVSUM_1:63 .= (a*G).n by A5,A6,FVSUM_1:63 .= aFaG.i by A5,A6,FINSEQ_1:def 7; end; end; hence (a*FG).i=aFaG.i; end; hence thesis by FINSEQ_2:139; end; theorem Th5: for f be Function for p1,p2,f1,f2 be FinSequence st rng p1 c= dom f & rng p2 c= dom f & f1=f*p1 & f2=f*p2 holds f * (p1 ^ p2) = f1 ^ f2 proof let f be Function; let p1,p2,f1,f2 be FinSequence such that A1: rng p1 c= dom f & rng p2 c= dom f and A2: f1=f*p1 & f2=f*p2; rng (p1^p2) = rng p1 \/rng p2 by FINSEQ_1:44; then A3: dom f1=dom p1 & dom f2=dom p2 & dom (f*(p1^p2))=dom (p1^p2) by A1,A2,RELAT_1:46,XBOOLE_1:8; then A4: len f1=len p1 & len f2=len p2 & dom (p1^p2)=Seg (len p1+len p2) by FINSEQ_3:31,FINSEQ_1:def 7; then A5: dom (f1^f2)=dom (f*(p1^p2)) by FINSEQ_1:def 7,A3; now let x such that A6: x in dom (f1^f2); reconsider i=x as Element of NAT by A6; now per cases; suppose A7: i in dom p1; hence (f1^f2).i = f1.i by A3,FINSEQ_1:def 7 .= f.(p1.i) by A2,A3,A7,FUNCT_1:22 .= f.((p1^p2).i) by A7,FINSEQ_1:def 7 .= (f*(p1^p2)).i by A5,A6,FUNCT_1:22; end; suppose not i in dom p1; then consider n such that A8: n in dom p2 & i=len p1 + n by A3,A4,A6,FINSEQ_1:38; thus (f1^f2).i = f2.n by A3,A4,A8,FINSEQ_1:def 7 .= f.(p2.n) by A2,A3,A8,FUNCT_1:22 .= f.((p1^p2).i) by A8,FINSEQ_1:def 7 .= (f*(p1^p2)).i by A5,A6,FUNCT_1:22; end; end; hence (f1^f2).x = (f*(p1^p2)).x; end; hence thesis by A5,FUNCT_1:9; end; theorem Th6: for f be FinSequence of NAT,n st f is one-to-one & rng f c= Seg n & for i,j st i in dom f & j in dom f & i < j holds f.i < f.j holds Sgm rng f = f proof defpred P[Nat] means for f be FinSequence of NAT,n st len f=$1 & rng f c= Seg n & f is one-to-one & for i,j st i in dom f & j in dom f & i < j holds f.i < f.j holds Sgm rng f = f; A1: P[0] proof let f be FinSequence of NAT,n such that A2: len f=0 and rng f c= Seg n & f is one-to-one & for i,j st i in dom f & j in dom f & i < j holds f.i < f.j; f={} by A2,FINSEQ_1:25; hence thesis by FINSEQ_3:49,FINSEQ_1:27; end; A3: for n st P[n] holds P[n+1] proof let n such that A4: P[n]; set n1=n+1; let f be FinSequence of NAT,k such that A5: len f=n1 & rng f c= Seg k and A6: f is one-to-one and A7: for i,j st i in dom f & j in dom f & i < j holds f.i < f.j; set fn=f|n; A8: len fn =n & fn is one-to-one by A5,A6,FINSEQ_3:59,FUNCT_1:84; A9: f=fn^<*f.n1*> by A5,FINSEQ_3:61; then A10: dom fn c= dom f & rng f = rng fn\/rng<*f.n1*>& rng <*f.n1*>={f.n1} & rng fn c= rng f & rng <*f.n1*> c= rng f by FINSEQ_1:39,42,43,44,56; then A11: rng fn c= Seg k & {f.n1} c= Seg k by A5,XBOOLE_1:1; for i,j st i in dom fn & j in dom fn & i < j holds fn.i < fn.j proof let i,j such that A12: i in dom fn & j in dom fn & i < j; i in dom f & j in dom f & fn.i=f.i & fn.j=f.j by A9,A10,A12,FINSEQ_1:def 7; hence thesis by A7,A12; end; then A13: Sgm rng fn = fn by A4,A8,A11; A14: now let m',n' being Element of NAT such that A15: m' in rng fn & n' in {f.n1}; consider x such that A16: x in dom fn & fn.x=m' by A15,FUNCT_1:def 5; reconsider x as Element of NAT by A16; dom fn=Seg n by A8,FINSEQ_1:def 3; then x<=n by A16,FINSEQ_1:3; then x < n1 & n1 in Seg n1 & dom f=Seg n1 & x in dom f by A5,A10,A16,NAT_1:13,FINSEQ_1:def 3,6; then f.x < f.n1 & f.x = fn.x & f.n1=n' by A7,A9,A15,A16,FINSEQ_1:def 7,TARSKI:def 1; hence m' < n' by A16; end; not 0 in Seg k & f.n1 in {f.n1} by FINSEQ_1:3,TARSKI:def 1; then A17: f.n1<>0 by A11; thus Sgm rng f = fn ^ Sgm {f.n1} by A10,A11,A13,A14,FINSEQ_3:48 .= f by A9,A17,FINSEQ_3:50; end; A18: for n holds P[n] from NAT_1:sch 2(A1,A3); let f be FinSequence of NAT,n such that A19: f is one-to-one & rng f c= Seg n and A20: for i,j st i in dom f & j in dom f & i < j holds f.i < f.j; for g be FinSequence of NAT,n st len g=len f & rng g c= Seg n & g is one-to-one & for i,j st i in dom g & j in dom g & i < j holds g.i < g.j holds Sgm rng g = g by A18; hence thesis by A19,A20; end; theorem Th7: for K be Abelian add-associative right_zeroed right_complementable (non empty addLoopStr) for p be FinSequence of K for i,j st i in dom p & j in dom p & i<>j & for k st k in dom p & k<>i & k<>j holds p.k=0.K holds Sum p = p/.i+p/.j proof let K be Abelian add-associative right_zeroed right_complementable (non empty addLoopStr); let p be FinSequence of K; A1: now let i,j such that A2: i in dom p & j in dom p & ii & k<>j holds p.k=0.K; set pI=p|i; consider q be FinSequence such that A4: p = pI^q by FINSEQ_1:101; reconsider q as FinSequence of K by A4,FINSEQ_1:50; A5: dom p=Seg len p by FINSEQ_1:def 3; A6: i in NAT by ORDINAL1:def 13; 1 <= i & i <= len p by A5,A2,FINSEQ_1:3; then A7: i in Seg i & len pI=i & dom pI=Seg i & Seg i c= Seg len p by FINSEQ_1:7,21,A6; now let k such that A8: k in dom pI & k<>i; reconsider kk=k as Element of NAT by ORDINAL1:def 13; A9: k<>j by A2,A7,A8,FINSEQ_1:3; thus pI.k = p.kk by A4,A8,FINSEQ_1:def 7 .= 0.K by A5,A7,A3,A8,A9; end; then A10: Sum pI = pI.i by A7,MATRIX_3:14 .= p.i by A4,A7,FINSEQ_1:def 7 .= p/.i by A5,A7,PARTFUN1:def 8; not j in dom pI by A2,A7,FINSEQ_1:3; then consider ji be Nat such that A11: ji in dom q & j=i + ji by A7,A2,A4,FINSEQ_1:38; now let k such that A12: k in dom q & k<>ji; reconsider kk=k as Element of NAT by ORDINAL1:def 13; dom q = Seg len q by FINSEQ_1:def 3; then k >= 1 by A12,FINSEQ_1:3; then k+i >= i+1 by XREAL_1:9; then A13: i+kk<>i & i+kk <> i+ji by A12,NAT_1:13; thus q.k = p.(i+kk) by A4,A7,A12,FINSEQ_1:def 7 .= 0.K by A3,A11,A13,A4,A7,A12,FINSEQ_1:41; end; then Sum q = q.ji by A11,MATRIX_3:14 .= p.j by A11,A7,A4,FINSEQ_1:def 7 .= p/.j by A2,PARTFUN1:def 8; hence Sum p=p/.i+p/.j by A10,A4,RLVECT_1:58; end; let i,j such that A14: i in dom p & j in dom p & i<>j and A15: for k st k in dom p & k<>i & k<>j holds p.k=0.K; A16: for k st k in dom p & k<>j & k<>i holds p.k=0.K by A15; in) by FINSEQ_1:3; then reconsider IN=i-n as Element of NAT by NAT_1:21; n+IN=i; then IN>=1 & IN<=m by A6,NAT_1:19,XREAL_1:10; then IN in dom I by A2; then n+IN in dom (N Shift I) by A3; hence thesis; end; dom (N Shift I) c=Seg (n+m)\Seg n proof let x such that A7: x in dom (N Shift I); consider k be Element of NAT such that A8: n+k=x & k in dom I by A3,A7; 1<=k & k<=m by A2,A8,FINSEQ_1:3; then A9: n+1<=n+k & n+k<=n+m & 1<=n+1 by XREAL_1:9,NAT_1:11; then n+k >n by NAT_1:13; then A10: not k+n in Seg n by FINSEQ_1:3; 1<=n+k by A9,XXREAL_0:2; then n+k in Seg (n+m) by A9; hence thesis by A8,A10,XBOOLE_0:def 4; end; then Seg (n+m)\Seg n = dom (N Shift I) by A4,XBOOLE_0:def 10; hence thesis by A1,A2,PNPROC_1:59; end; theorem Th9: for D be non empty set, A be Matrix of D for Bx,By,Cx,Cy be without_zero finite Subset of NAT st [:Bx,By:] c= Indices A & [:Cx,Cy:] c= Indices A for B be Matrix of card Bx,card By,D, C be Matrix of card Cx,card Cy,D st for i,j,bi,bj,ci,cj be Nat st [i,j] in [:Bx,By:]/\[:Cx,Cy:] & bi = Sgm Bx".i & bj = Sgm By".j & ci = Sgm Cx".i & cj = Sgm Cy".j holds B*(bi,bj) = C*(ci,cj) ex M be Matrix of len A,width A,D st Segm(M,Bx,By) = B & Segm(M,Cx,Cy) = C & for i,j st [i,j] in Indices M\([:Bx,By:]\/[:Cx,Cy:]) holds M*(i,j) = A*(i,j) proof let D be non empty set, A be Matrix of D; let Bx,By,Cx,Cy be without_zero finite Subset of NAT such that A1: [:Bx,By:] c= Indices A & [:Cx,Cy:] c= Indices A; set bx=card Bx; set bY=card By; set cx=card Cx; set cy=card Cy; set l=len A; set w=width A; let B be Matrix of bx,bY,D,C be Matrix of cx,cy,D such that A2: for i,j,bi,bj,ci,cj be Nat st [i,j] in [:Bx,By:]/\[:Cx,Cy:] & bi = Sgm Bx".i & bj = Sgm By".j & ci = Sgm Cx".i & cj = Sgm Cy".j holds B*(bi,bj) = C*(ci,cj); consider kBx be Nat such that A3: Bx c= Seg kBx by MATRIX13:43; consider kBy be Nat such that A4: By c= Seg kBy by MATRIX13:43; consider kCx be Nat such that A5: Cx c= Seg kCx by MATRIX13:43; consider kCy be Nat such that A6: Cy c= Seg kCy by MATRIX13:43; defpred P[set,set,set] means for i,j st $1=i & $2=j holds ([i,j] in [:Bx,By:] implies (ex m,n st m in dom Sgm Bx & n in dom Sgm By & Sgm Bx.m=i & Sgm By.n=j)& for m,n st m in dom Sgm Bx & n in dom Sgm By & Sgm Bx.m=i & Sgm By.n=j holds $3=B*(m,n))& ([i,j] in [:Cx,Cy:] implies (ex m,n st m in dom Sgm Cx & n in dom Sgm Cy & Sgm Cx.m=i & Sgm Cy.n=j)&for m,n st m in dom Sgm Cx & n in dom Sgm Cy & Sgm Cx.m=i & Sgm Cy.n=j holds $3=C*(m,n))& (not [i,j] in [:Bx,By:]\/[:Cx,Cy:] implies $3=A*(i,j)); A7: for i,j st [i,j] in [:Seg l, Seg w:] for x1,x2 be Element of D st P[i,j,x1] & P[i,j,x2] holds x1 = x2 proof let i,j such that [i,j] in [:Seg l, Seg w:]; let x1,x2 be Element of D such that A8: P[i,j,x1] & P[i,j,x2]; per cases; suppose A9: [i,j] in [:Bx,By:]; then consider m,n such that A10: m in dom Sgm Bx & n in dom Sgm By and A11: Sgm Bx.m=i & Sgm By.n=j by A8; thus x1 = B*(m,n) by A8,A9,A10,A11 .= x2 by A8,A9,A10,A11; end; suppose A12: [i,j] in [:Cx,Cy:]; then consider m,n such that A13: m in dom Sgm Cx & n in dom Sgm Cy and A14: Sgm Cx.m=i & Sgm Cy.n=j by A8; thus x1 = C*(m,n) by A8,A12,A13,A14 .= x2 by A8,A12,A13,A14; end; suppose not [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:]; then A15: not [i,j] in [:Bx,By:]\/[:Cx,Cy:] by XBOOLE_0:def 2; hence x1 = A*(i,j) by A8 .= x2 by A8,A15; end; end; A16: rng Sgm Bx=Bx & rng Sgm By=By & dom Sgm Bx=Seg bx & dom Sgm By=Seg bY & rng Sgm Cx=Cx & rng Sgm Cy=Cy & dom Sgm Cx=Seg cx & dom Sgm Cy=Seg cy & Sgm Bx is one-to-one & Sgm By is one-to-one & Sgm Cx is one-to-one & Sgm Cy is one-to-one by A3,A4,A5,A6,FINSEQ_1:def 13,FINSEQ_3:45,99; A17: for i,j st [i,j] in [:Seg l, Seg w:] ex x being Element of D st P[i,j,x] proof let i,j such that [i,j] in [:Seg l, Seg w:]; per cases; suppose A18: [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:]; then i in Bx by ZFMISC_1:106; then consider x such that A19: x in dom Sgm Bx & Sgm Bx.x=i by A16,FUNCT_1:def 5; j in By by A18,ZFMISC_1:106; then consider y such that A20: y in dom Sgm By & Sgm By.y=j by A16,FUNCT_1:def 5; i in Cx by A18,ZFMISC_1:106; then consider xC be set such that A21: xC in dom Sgm Cx & Sgm Cx.xC=i by A16,FUNCT_1:def 5; j in Cy by A18,ZFMISC_1:106; then consider yC be set such that A22: yC in dom Sgm Cy & Sgm Cy.yC=j by A16,FUNCT_1:def 5; reconsider x,y,xC,yC as Element of NAT by A19,A20,A21,A22; take BB=B*(x,y); A23: now let m,n such that A24: m in dom Sgm Bx & n in dom Sgm By and A25: Sgm Bx.m=i & Sgm By.n=j; x=m & y=n by A16,A19,A20,A24,A25,FUNCT_1:def 8; hence BB=B*(m,n); end; A26: now let m,n such that A27: m in dom Sgm Cx & n in dom Sgm Cy and A28: Sgm Cx.m=i & Sgm Cy.n=j; A29: [i,j] in [:Bx,By:]/\[:Cx,Cy:] by A18,XBOOLE_0:def 3; Sgm Bx".i=x & Sgm By".j=y & Sgm Cx".i=m & Sgm Cy".j=n by A16,A19,A20,A27,A28,FUNCT_1:54; hence BB=C*(m,n) by A2,A29; end; xC in dom Sgm Cx & Sgm Cx.xC=i & yC in dom Sgm Cy & Sgm Cy.yC=j by A21,A22; hence thesis by A19,A20,A23,A26,A18,XBOOLE_0:def 2; end; suppose A30: [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:]; then i in Bx by ZFMISC_1:106; then consider x such that A31: x in dom Sgm Bx & Sgm Bx.x=i by A16,FUNCT_1:def 5; j in By by A30,ZFMISC_1:106; then consider y such that A32: y in dom Sgm By & Sgm By.y=j by A16,FUNCT_1:def 5; reconsider x,y as Element of NAT by A31,A32; take BB=B*(x,y); now let m,n such that A33: m in dom Sgm Bx & n in dom Sgm By and A34: Sgm Bx.m=i & Sgm By.n=j; x = m & y = n by A16,A31,A32,A33,A34,FUNCT_1:def 8; hence BB=B*(m,n); end; hence thesis by A31,A32,A30,XBOOLE_0:def 2; end; suppose A35: not [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:]; then i in Cx by ZFMISC_1:106; then consider x such that A36: x in dom Sgm Cx & Sgm Cx.x=i by A16,FUNCT_1:def 5; j in Cy by A35,ZFMISC_1:106; then consider y such that A37: y in dom Sgm Cy & Sgm Cy.y=j by A16,FUNCT_1:def 5; reconsider x,y as Element of NAT by A36,A37; take CC=C*(x,y); now let m,n such that A38: m in dom Sgm Cx & n in dom Sgm Cy and A39: Sgm Cx.m=i & Sgm Cy.n=j; x = m & y = n by A16,A36,A37,A38,A39,FUNCT_1:def 8; hence CC=C*(m,n); end; hence thesis by A36,A37,A35,XBOOLE_0:def 2; end; suppose A40: not [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:]; take AA=A*(i,j); thus thesis by A40; end; end; consider M be Matrix of l,w,D such that A41: for i,j st [i,j] in Indices M holds P[i,j,M*(i,j)] from MATRIX_1:sch 2(A7,A17); take M; set MB=Segm(M,Bx,By); A is Matrix of l,w,D by MATRIX_2:7; then A42: Indices A=Indices M & Indices MB=Indices B by MATRIX_1:27; now let i,j such that A43: [i,j] in Indices MB; bx<>0 by A43,MATRIX_1:23; then bx>0; then Indices MB=[:Seg bx,Seg bY:] by MATRIX_1:24; then A44: i in Seg bx & j in Seg bY by A43,ZFMISC_1:106; then Sgm Bx.i in Bx & Sgm By.j in By by A16,FUNCT_1:def 5; then [Sgm Bx.i,Sgm By.j] in [:Bx,By:] by ZFMISC_1:106; hence B*(i,j) = M*(Sgm Bx.i,Sgm By.j) by A1,A16,A41,A42,A44 .= MB*(i,j) by A43,MATRIX13:def 1; end; hence MB=B by MATRIX_1:28; set MC=Segm(M,Cx,Cy); now let i,j such that A45: [i,j] in Indices MC; cx<>0 by A45,MATRIX_1:23; then cx>0; then Indices MC=[:Seg cx,Seg cy:] by MATRIX_1:24; then A46: i in Seg cx & j in Seg cy by A45,ZFMISC_1:106; then Sgm Cx.i in Cx & Sgm Cy.j in Cy by A16,FUNCT_1:def 5; then [Sgm Cx.i,Sgm Cy.j] in [:Cx,Cy:] by ZFMISC_1:106; hence C*(i,j) = M*(Sgm Cx.i,Sgm Cy.j) by A1,A16,A41,A42,A46 .= MC*(i,j) by A45,MATRIX13:def 1; end; hence MC=C by MATRIX_1:28; let i,j such that A47: [i,j] in Indices M\([:Bx,By:]\/[:Cx,Cy:]); not [i,j] in [:Bx,By:]\/[:Cx,Cy:] by A47,XBOOLE_0:def 4; hence thesis by A41,A47; end; theorem Th10: for P,Q,Q' be without_zero finite Subset of NAT st [:P,Q':] c= Indices A for i,j st i in dom A \ P & j in Seg width A \ Q & A*(i,j) <> 0.K & Q c= Q' & Line(A,i) * Sgm Q' = card Q' |-> 0.K holds the_rank_of A > the_rank_of Segm(A,P,Q) proof let P,Q,R be without_zero finite Subset of NAT such that A1: [:P,R:] c= Indices A; let i,j such that A2: i in dom A \ P & j in Seg width A \ Q & A*(i,j)<> 0.K and A3: Q c= R & Line(A,i) * Sgm R = card R |-> 0.K; A4: [:P,Q:] c= [:P,R:] by A3,ZFMISC_1:118; then A5: [:P,Q:] c= Indices A by A1,XBOOLE_1:1; set S=Segm(A,P,Q); consider P',Q' be without_zero finite Subset of NAT such that A6: [:P',Q':] c= Indices S & card P' = card Q' and A7: card P' = the_rank_of S and A8: Det EqSegm(S,P',Q')<>0.K by MATRIX13:def 4; P'={} iff Q'={} by A6,CARD_1:47,CARD_2:59; then consider P2,Q2 be without_zero finite Subset of NAT such that A9: P2 c= P & Q2 c= Q and P2 = Sgm P.:P' & Q2=Sgm Q.:Q' and A10: card P2=card P' & card Q2=card Q' and A11: Segm(S,P',Q') = Segm(A,P2,Q2) by A6,MATRIX13:57; A12: dom A=Seg len A by FINSEQ_1:def 3; then A13: i in Seg len A & j in Seg width A by A2,XBOOLE_0:def 4; then reconsider i0=i,j0=j as non zero Element of NAT by FINSEQ_1:3; set P2i=P2\/{i0}; set Q2j=Q2\/{j0}; set ESS=EqSegm(A,P2i,Q2j); set SS=Segm(A,P2i,Q2j); per cases; suppose [:P,Q:] ={}; then card P=0 or card Q=0 by CARD_1:47,ZFMISC_1:113; then A14: the_rank_of S=0 by MATRIX13:77; [i,j] in Indices A by A12,A13,ZFMISC_1:106; hence thesis by A14,A2,MATRIX13:94; end; suppose [:P,Q:]<>{}; then P c= dom A & Q c= Seg width A & [:P,R:]<>{} by A5,A4,ZFMISC_1:138,XBOOLE_1:3; then A15: P2 c= dom A & Q2 c= Seg width A & R c= Seg width A by A9,XBOOLE_1:1,A1,ZFMISC_1:138; A16: {i0} c= dom A & {j0}c= Seg width A by A12,A13,ZFMISC_1:37; then A17: P2i c= dom A & Q2j c= Seg width A by A15,XBOOLE_1:8; A18: not i in P2 & not j in Q2 by A9,A2,XBOOLE_0:def 4; then A19: card P2i=card P2+1 & card Q2j=card Q2+1 by CARD_2:54; A20: rng Sgm P2i=P2i & dom Sgm P2i=Seg card P2i & rng Sgm Q2j=Q2j & dom Sgm Q2j=Seg card Q2j & Sgm Q2j is one-to-one & rng Sgm R=R & dom Sgm R=Seg card R by A12,A15,A17,FINSEQ_1:def 13,FINSEQ_3:45,99; i in {i} by TARSKI:def 1; then i in P2i by XBOOLE_0:def 2; then consider x such that A21: x in dom Sgm P2i & Sgm P2i.x=i by A20,FUNCT_1:def 5; j in {j} by TARSKI:def 1; then j in Q2j by XBOOLE_0:def 2; then consider y such that A22: y in dom Sgm Q2j & Sgm Q2j.y=j by A20,FUNCT_1:def 5; reconsider x,y as Element of NAT by A21,A22; set L=LaplaceExpL(ESS,x); A23: dom L = Seg len L by FINSEQ_1:def 3 .= Seg card P2i by LAPLACE:def 7; then A24: y in dom L by A6,A10,A19,A22,A16,A15,XBOOLE_1:8,FINSEQ_3:45; A25: len ESS = card P2i & dom ESS=Seg len ESS & Indices ESS = [:Seg card P2i,Seg card P2i:] by MATRIX_1:25,FINSEQ_1:def 3; A26: ESS = SS by A6,A10,A19,MATRIX13:def 3; now let k such that A27: k in dom L & k <> y; A28: [x,k] in Indices ESS by A25,A27,A20,A21,A23,ZFMISC_1:106; Sgm Q2j.k <> j by FUNCT_1:def 8,A27,A23,A20,A6,A10,A19,A22; then Sgm Q2j.k in Q2j & not Sgm Q2j.k in {j} by FUNCT_1:def 5,A27,A6,A10,A19,A20,A23,TARSKI:def 1; then Sgm Q2j.k in Q2 by XBOOLE_0:def 2; then A29: Sgm Q2j.k in Q by A9; then consider z be set such that A30: z in dom Sgm R & Sgm R.z=Sgm Q2j.k by A3,A20,FUNCT_1:def 5; A31: Sgm Q2j.k in R by A3,A29; reconsider z as Element of NAT by A30; ESS*(x,k) = A*(i,Sgm Q2j.k) by A21,A28,A26,MATRIX13:def 1 .= Line(A,i).(Sgm R.z) by MATRIX_1:def 8,A15,A31,A30 .= (card R |-> 0.K).z by A3,A30,FUNCT_1:23 .= 0.K by A20,A30,FINSEQ_1:4,FINSEQ_2:71; hence L.k = 0.K*Cofactor(ESS,x,k) by A27,LAPLACE:def 7 .= 0.K by VECTSP_1:39; end; then A32: L.y = Sum L by A24,MATRIX_3:14 .= Det ESS by A20,A21,LAPLACE:25; A33: [x,y] in Indices ESS by A6,A10,A19,A20,A21,A22,A25,ZFMISC_1:106; A34: L.y = SS*(x,y)*Cofactor(ESS,x,y) by A26,A24,LAPLACE:def 7 .= A*(i,j)*(power(K).(-1_K,x+y)*Det Delete(ESS,x,y)) by A21,A22,A33,A26,MATRIX13:def 1; A35: Delete(ESS,x,y) = EqSegm(A,P2i\{i},Q2j\{j}) by MATRIX13:64,A6,A10,A19,A20,A21,A22 .= EqSegm(A,P2,Q2j\{j}) by A18,ZFMISC_1:141 .= EqSegm(A,P2,Q2) by A18,ZFMISC_1:141 .= Segm(A,P2,Q2) by A6,A10,MATRIX13:def 3 .= EqSegm(S,P',Q') by A6,A11,MATRIX13:def 3; A36: card P2i-'1=card P' by BINARITH:39,A10,A19; -1_K<>0.K by VECTSP_1:86; then power(K).(-1_K,x+y)<>0.K by Lm2; then power(K).(-1_K,x+y) * Det Delete(ESS,x,y)<>0.K by A35,A8,A36,VECTSP_1:44; then A37: Det ESS<>0.K by A32,A2,A34,VECTSP_1:44; [:P2i,Q2j:] c= Indices A by A17,ZFMISC_1:119; then the_rank_of A >= card P2i by A6,A10,A19,A37,MATRIX13:def 4; hence thesis by A7,A10,A19,NAT_1:13; end; end; theorem Th11: for N st N c= dom A & for i st i in dom A \ N holds Line(A,i) = width A |-> 0.K holds the_rank_of A=the_rank_of Segm(A,N,Seg width A) proof let N such that A1: N c= dom A and A2: for i st i in (dom A) \ N holds Line(A,i) = width A |-> 0.K; reconsider A'=A as Matrix of len A,width A,K by MATRIX_2:7; set l=len A; set w=width A; set S=Segm(A',N,Seg width A'); consider U be finite Subset of w-VectSp_over K such that A3: U is linearly-independent & U c= lines A' & card U = the_rank_of A' by MATRIX13:123; A4: U c= lines S proof let x such that A5: x in U; consider Ni be Nat such that A6: Ni in Seg l & x = Line(A',Ni) by A3,A5,MATRIX13:103; A7: dom A=Seg l by FINSEQ_1:def 3; A8: Ni in N proof assume not Ni in N; then Ni in dom A\N by A6,A7,XBOOLE_0:def 4; then x = w |-> 0.K by A2,A6 .= 0.(w-VectSp_over K) by MATRIX13:102; hence thesis by A3,A5,VECTSP_7:3; end; rng Sgm N=N by A1,A7,FINSEQ_1:def 13; then consider i be set such that A9: i in dom Sgm N & Sgm N.i=Ni by A8,FUNCT_1:def 5; reconsider i as Element of NAT by A9; A10: dom Sgm N=Seg card N by A1,A7,FINSEQ_3:45; then Line(S,i) = x by A6,A9,MATRIX13:48; hence thesis by A9,A10,MATRIX13:103; end; A11: w=card Seg w by FINSEQ_1:78; now let W be finite Subset of w-VectSp_over K such that A12: W is linearly-independent & W c= lines S; dom A=Seg l by FINSEQ_1:def 3; then lines S c= lines A' by A1,MATRIX13:118; then W c= lines A' by A12,XBOOLE_1:1; hence card W <= the_rank_of A' by A12,MATRIX13:123; end; hence thesis by A3,A4,A11,MATRIX13:123; end; theorem Th12: for N st N c= Seg width A & for i st i in Seg width A \ N holds Col(A,i) = len A |-> 0.K holds the_rank_of A = the_rank_of Segm(A,Seg len A,N) proof let N such that A1: N c= Seg width A and A2: for i st i in Seg width A \ N holds Col(A,i) = len A |-> 0.K; A3: dom A=Seg len A by FINSEQ_1:def 3; per cases; suppose A4: card N=0; the_rank_of A = 0 proof assume the_rank_of A <>0; then the_rank_of A >0; then consider i,j such that A5: [i,j] in Indices A & A*(i,j) <> 0.K by MATRIX13:94; A6: i in dom A & j in Seg width A & N={} by A4,A5,ZFMISC_1:106,CARD_2:59; then 0.K = (len A|-> 0.K).i by A3,FINSEQ_2:71,FINSEQ_1:4 .= Col(A,j).i by A2,A6 .= A*(i,j) by A6,MATRIX_1:def 9; hence thesis by A5; end; hence thesis by A4,MATRIX13:77; end; suppose A7: card N>0; then A8: width A<>0 by FINSEQ_1:4,A1,XBOOLE_1:3,CARD_1:47; then len A<>0 by MATRIX_1:def 4; then len A in Seg len A by FINSEQ_1:5; then A9: card Seg len A=0 iff card N=0 by A7,CARD_2:59; A10: [:dom A,N:] c= Indices A by A1,ZFMISC_1:118; set AT=A@; A11: width A>0 by A8; then A12: len AT=width A by MATRIX_2:12; A13: width AT=len A by A11,MATRIX_2:12; A14: dom AT=Seg len AT by FINSEQ_1:def 3; A15: N c= dom AT by A1,A12,FINSEQ_1:def 3; A16: now let i such that A17: i in dom AT \ N; i in dom AT by A17,XBOOLE_0:def 4; hence Line(AT,i) = Col(A,i) by A12,A14,MATRIX_2:17 .= width AT |-> 0.K by A2,A12,A13,A14,A17; end; thus the_rank_of A = the_rank_of AT by MATRIX13:84 .= the_rank_of Segm(AT, N,Seg len A) by A13,A15,A16,Th11 .= the_rank_of (Segm(A,Seg len A,N)@) by A10,A9,A3,MATRIX13:61 .= the_rank_of Segm(A,Seg len A,N) by MATRIX13:84; end; end; theorem Th13: for V be VectSp of K for U be finite Subset of V for u, v be Vector of V,a st u in U & v in U holds Lin (U \ {u} \/ {u+a*v}) is Subspace of Lin U proof let V be VectSp of K; let U be finite Subset of V; let u, v be Vector of V,a such that A1: u in U & v in U; set UU=U\{u}; set ua=u+a*v; UU \/ {ua} c= the carrier of Lin U proof let x such that A2: x in UU \/ {ua}; per cases by A2,XBOOLE_0:def 2; suppose x in UU; then x in U by XBOOLE_0:def 4; then x in Lin U by VECTSP_7:13; hence thesis by STRUCT_0:def 5; end; suppose x in {ua}; then A3: x=ua by TARSKI:def 1; u in Lin U & a*v in Lin U by VECTSP_4:29,A1,VECTSP_7:13; then x in Lin U by A3,VECTSP_4:28; hence thesis by STRUCT_0:def 5; end; end; hence thesis by VECTSP_9:20; end; theorem Th14: for V be VectSp of K for U be finite Subset of V for u, v be Vector of V,a st u in U & v in U & (u = v implies (a <> -1_K or u = 0.V)) holds Lin (U \ {u} \/ {u+a*v}) = Lin U proof let V be VectSp of K; let U be finite Subset of V; let u, v be Vector of V,a such that A1: u in U & v in U and A2: u = v implies (a <> -1_K or u = 0.V); set UU=U\{u}; set ua=u+a*v; U c= the carrier of Lin (UU\/{ua}) proof let x such that A3: x in U; per cases; suppose A4: x=u; per cases; suppose u<>v; then v in UU & ua in {ua} by A1,ZFMISC_1:64,TARSKI:def 1; then A5: v in UU\/{ua} & ua in UU\/{ua} by XBOOLE_0:def 2; then A6: v in Lin(UU\/{ua}) & ua in Lin(UU\/{ua}) by VECTSP_7:13; (-a)*v in Lin(UU\/{ua}) by A5,VECTSP_4:29,VECTSP_7:13; then A7: ua+(-a)*v in Lin(UU\/{ua}) by A6,VECTSP_4:28; ua+(-a)*v = ua-a*v by VECTSP_1:68 .= u+(a*v-a*v) by RLVECT_1:def 6 .= u+0.V by VECTSP_1:63 .= u by RLVECT_1:def 7; hence thesis by A4,A7,STRUCT_0:def 5; end; suppose A8: u=v; per cases by A2,A8; suppose a<>-1_K; then 0.K<> -1_K-a by VECTSP_1:66; then 0.K<> -(-1_K-a) by VECTSP_1:86; then A9: 0.K<>a+1_K by VECTSP_1:89; ua = 1_K*u+a*u by A8,VECTSP_1:def 26 .= (1.K+a)*u by VECTSP_1:def 26; then A10: (1.K+a)" *ua =u by A9,VECTSP_1:67; ua in {ua} by TARSKI:def 1; then ua in UU\/{ua} by XBOOLE_0:def 2; then u in Lin (UU\/{ua}) by A10,VECTSP_4:29,VECTSP_7:13; hence thesis by A4,STRUCT_0:def 5; end; suppose u=0.V; then x in Lin(UU\/{ua}) by A4,VECTSP_4:25; hence thesis by STRUCT_0:def 5; end; end; end; suppose x<>u; then x in UU by A3,ZFMISC_1:64; then x in UU\/{ua} by XBOOLE_0:def 2; then x in Lin (UU\/{ua}) by VECTSP_7:13; hence thesis by STRUCT_0:def 5; end; end; then Lin (UU\/{ua}) is Subspace of Lin U & Lin U is Subspace of Lin (UU\/{ua}) by A1,VECTSP_9:20,Th13; then the carrier of Lin (UU\/{ua})c= the carrier of Lin U & the carrier of Lin U c=the carrier of Lin (UU\/{ua}) by VECTSP_4:def 2; then the carrier of Lin U =the carrier of Lin (UU\/ {ua}) by XBOOLE_0:def 10; hence thesis by VECTSP_4:37; end; begin :: Selected properties of the operator ^^ definition let D be non empty set; let n,m,k be Nat; let A be Matrix of n,m,D; let B be Matrix of n,k,D; redefine func A^^B -> Matrix of n,width A+width B,D; coherence proof set AB=A^^B; reconsider N=n as Element of NAT by ORDINAL1:def 13; A1: dom A = Seg len A by FINSEQ_1:def 3 .= Seg n by MATRIX_1:def 3; dom B = Seg len B by FINSEQ_1:def 3 .= Seg n by MATRIX_1:def 3; then A2: dom AB = Seg n/\Seg n by A1,MATRLIN:def 2 .= Seg n; then A3: len AB=N by FINSEQ_1:def 3; per cases; suppose A4: N=0; then AB={} by A3,FINSEQ_1:25; hence thesis by A4,MATRIX_1:13; end; suppose A5: N>0; then A6: N in Seg N by FINSEQ_1:5; then A.N=Line(A,N) & B.N=Line(B,N) & Line(A,N)^Line(B,N) is Element of (width A+width B)-tuples_on D by MATRIX_2:10,FINSEQ_2:127; then AB.N=Line(A,N)^Line(B,N) & AB.N in rng AB & len (Line(A,N)^Line(B,N))=width A+width B by A2,A6,MATRLIN:def 2,FUNCT_1:def 5,FINSEQ_2:109; then width AB=width A+width B by A3,A5,MATRIX_1:def 4; hence thesis by A3,MATRIX_2:7; end; end; end; theorem Th15: for D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D for i st i in Seg n holds Line(A^^B,i)=Line(A,i)^Line(B,i) proof let D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D; let i such that A1: i in Seg n; set AB=A^^B; A2: len AB=n & dom AB=Seg len AB by MATRIX_1:def 3,FINSEQ_1:def 3; Line(A,i)=A.i & Line(B,i)=B.i by A1,MATRIX_2:10; hence Line(A,i)^Line(B,i) = AB.i by A1,A2,MATRLIN:def 2 .= Line(AB,i) by A1,MATRIX_2:10; end; theorem Th16: for D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D for i st i in Seg width A holds Col(A^^B,i) = Col(A,i) proof let D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D; let i such that A1: i in Seg width A; set AB=A^^B; A2: len A=n & len AB=n by MATRIX_1:def 3; now let j such that A3: j in Seg n; A4: dom AB=Seg n & dom A=Seg n by A2,FINSEQ_1:def 3; n<>0 by A3,FINSEQ_1:4; then n>0; then width AB=width A+width B by MATRIX_1:24; then width A<=width AB by NAT_1:11; then A5: Seg width A c= Seg width AB by FINSEQ_1:7; A6: dom Line(A,j)=Seg width A by FINSEQ_2:144; thus Col(AB,i).j = AB*(j,i) by A3,A4,MATRIX_1:def 9 .= Line(AB,j).i by A1,A5,MATRIX_1:def 8 .= (Line(A,j)^Line(B,j)).i by Th15,A3 .= Line(A,j).i by A1,A6,FINSEQ_1:def 7 .= A*(j,i) by A1,MATRIX_1:def 8 .= Col(A,i).j by A3,A4,MATRIX_1:def 9; end; hence thesis by A2,FINSEQ_2:139; end; theorem Th17: for D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D for i st i in Seg width B holds Col(A^^B,width A+i) = Col(B,i) proof let D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D; let i such that A1: i in Seg width B; set AB=A^^B; A2: len B=n & len AB=n by MATRIX_1:def 3; now let j such that A3: j in Seg n; A4: dom AB=Seg n & dom B=Seg n by A2,FINSEQ_1:def 3; n<>0 by A3,FINSEQ_1:4; then n>0; then width AB=width A+width B by MATRIX_1:24; then A5: width A+i in Seg width AB by A1,FINSEQ_1:81; A6: dom Line(B,j)=Seg width B & len Line(A,j)=width A by FINSEQ_2:109,144; thus Col(AB,width A+i).j = AB*(j,width A+i) by A3,A4,MATRIX_1:def 9 .= Line(AB,j).(width A+i) by A5,MATRIX_1:def 8 .= (Line(A,j)^Line(B,j)).(width A+i) by Th15,A3 .= Line(B,j).i by A1,A6,FINSEQ_1:def 7 .= B*(j,i) by A1,MATRIX_1:def 8 .= Col(B,i).j by A3,A4,MATRIX_1:def 9; end; hence thesis by A2,FINSEQ_2:139; end; theorem Th18: for D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D for pA,pB be FinSequence of D st len pA = width A & len pB = width B holds ReplaceLine(A^^B,i,pA^pB) = ReplaceLine(A,i,pA) ^^ ReplaceLine(B,i,pB) proof let D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D; let pA,pB be FinSequence of D such that A1: len pA = width A & len pB = width B; set AB=A^^B; set RAB=RLine(AB,i,pA^pB); set RA=RLine(A,i,pA); set RB=RLine(B,i,pB); set Rab=RA^^RB; A2: len RAB=n & len Rab=n & dom RAB=Seg len RAB & dom Rab=Seg len Rab by MATRIX_1:def 3,FINSEQ_1:def 3; now let j such that A3: 1<=j & j<=n; j in NAT by ORDINAL1:def 13; then A4: j in Seg n by A3; pA is Element of (width A)-tuples_on D & pB is Element of (width B)-tuples_on D by A1,FINSEQ_2:110; then pA^pB is Element of (width A+width B)-tuples_on D by FINSEQ_2:127; then A5: len (pA^pB)=width A+width B by FINSEQ_2:109; A6: width AB=width A+width B by A3,MATRIX_1:24; A7: now per cases; suppose i=j; then Line(RAB,j)=pA^pB & Line(RA,j)=pA & Line(RB,j)=pB by A1,A4,A5,A6,MATRIX11:28; hence Line(RAB,j)=Line(Rab,j) by A4,Th15; end; suppose i<>j; then Line(RAB,j)=Line(AB,j) & Line(RA,j)=Line(A,j) & Line(RB,j)=Line(B,j) by A4,MATRIX11:28; hence Line(RAB,j) = Line(RA,j)^Line(RB,j) by A4,Th15 .= Line(Rab,j) by A4,Th15; end; end; thus RAB.j = Line(RAB,j) by A4,MATRIX_2:10 .= Rab.j by A7,A4,MATRIX_2:10; end; hence thesis by A2,FINSEQ_1:18; end; theorem Th19: for D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D holds Segm(A^^B,Seg n,Seg width A) = A & Segm(A^^B,Seg n,Seg (width A+width B)\Seg width A) = B proof let D be non empty set, A be Matrix of n,m,D, B be Matrix of n,k,D; set AB=A^^B; A1: len A=n & len AB=n & len B=n by MATRIX_1:def 3; then reconsider A'=A as Matrix of n,width A,D by MATRIX_2:7; reconsider B'=B as Matrix of n,width B,D by A1,MATRIX_2:7; A2: card Seg n=n & card Seg width A=width A & card Seg (width A+width B)=width A+width B by FINSEQ_1:78; set S1=Segm(AB,Seg n,Seg width A); now let i,j such that A3: [i,j] in Indices A'; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 13; n<>0 by A3,MATRIX_1:23; then n>0; then Indices A'=[:Seg n,Seg width A:] & Indices A'=Indices S1 by A2,MATRIX_1:24,27; then A4: I in Seg n & J in Seg width A by A3,ZFMISC_1:106; A5: dom S1 = Seg len S1 by FINSEQ_1:def 3 .= Seg n by A2,MATRIX_1:def 3; A6: J = (idseq width A).J by A4,FINSEQ_2:57,FINSEQ_1:4 .= Sgm (Seg (width A)).J by FINSEQ_3:54; A7: dom A=Seg n by A1,FINSEQ_1:def 3; thus S1*(i,j) = Col(S1,J).I by A5,A4,MATRIX_1:def 9 .= Col(AB,Sgm (Seg (width A)).J).I by A1,A2,A4,MATRIX13:50 .= Col(A,J).I by A4,Th16,A6 .= A*(i,j) by A4,A7,MATRIX_1:def 9; end; hence A=S1 by A2,MATRIX_1:28; set w=width A+width B; set SS=Seg w\Seg width A; set S2=Segm(AB,Seg n,SS); width A <= w by NAT_1:11; then Seg width A c= Seg w by FINSEQ_1:7; then A8: card SS = w-width A by A2,CARD_2:63 .= width B; now let i,j such that A9: [i,j] in Indices B'; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 13; n<>0 by A9,MATRIX_1:23; then n>0; then Indices B'=[:Seg n,Seg width B:] & Indices B'=Indices S2 by A8,A2,MATRIX_1:24,27; then A10: I in Seg n & J in Seg width B by A9,ZFMISC_1:106; A11: dom S2 = Seg len S2 by FINSEQ_1:def 3 .= Seg n by A2,MATRIX_1:def 3; A12: dom B = Seg n by A1,FINSEQ_1:def 3; thus S2*(i,j) = Col(S2,J).I by A11,A10,MATRIX_1:def 9 .= Col(AB,Sgm SS.J).I by A1,A8,A10,MATRIX13:50 .= Col(AB,width A+J).I by A10,Th8 .= Col(B,J).I by A10,Th17 .= B'*(i,j) by A10,A12,MATRIX_1:def 9; end; hence thesis by A2,A8,MATRIX_1:28; end; theorem Th20: for A,B be Matrix of K st len A = len B holds the_rank_of A <= the_rank_of (A^^B) & the_rank_of B <= the_rank_of (A^^B) proof let A,B be Matrix of K such that A1: len A = len B; set L=len A; reconsider A'=A as Matrix of L,width A,K by MATRIX_2:7; reconsider B'=B as Matrix of L,width B,K by A1,MATRIX_2:7; set AB=A'^^B'; per cases; suppose L=0; hence thesis by A1,MATRIX13:74; end; suppose L>0; then A2: width AB=width A+width B & Indices AB=[:Seg L,Seg (width A+ width B):] by MATRIX_1:24; then A3: Segm(AB,Seg L,Seg width A) = A & Segm(AB,Seg L,Seg width AB\Seg width A) = B by Th19; width A <=width AB by A2,NAT_1:11; then Seg width A c=Seg width AB& Seg width AB\Seg width A c=Seg width AB by FINSEQ_1:7,XBOOLE_1:36; then [:Seg L,Seg width A:] c= Indices AB & [:Seg L,Seg width AB\Seg width A:] c= Indices AB by A2,ZFMISC_1:118; hence thesis by A3,MATRIX13:79; end; end; theorem for A,B be Matrix of K st len A = len B & len A = the_rank_of A holds the_rank_of A = the_rank_of (A^^B) proof let A,B be Matrix of K such that A1: len A = len B & len A =the_rank_of A; set L=len A; reconsider A'=A as Matrix of L,width A,K by MATRIX_2:7; reconsider B'=B as Matrix of L,width B,K by A1,MATRIX_2:7; the_rank_of (A'^^B')<=len (A'^^B') & len (A'^^B')=L& the_rank_of (A'^^B')>=L by A1,MATRIX_1:def 3,Th20,MATRIX13:74; hence thesis by A1,XXREAL_0:1; end; theorem Th22: for A,B be Matrix of K st len A = len B & width A = 0 holds A ^^ B = B & B ^^ A = B proof let A,B be Matrix of K such that A1: len A = len B & width A =0; set L=len A; reconsider A'=A as Matrix of L,width A,K by MATRIX_2:7; reconsider B'=B as Matrix of L,width B,K by A1,MATRIX_2:7; set AB=A'^^B'; set BA=B'^^A'; per cases; suppose A2: L=0; then len AB=0 & len BA=0 by MATRIX_1:def 3; then AB={} & BA={} & A={} & B={} by A1,A2,FINSEQ_1:25; hence thesis; end; suppose L>0; then A3: width AB=width B & width BA=width B & len AB=L & len BA=L by A1,MATRIX_1:24; hence A^^B = Segm(AB,Seg L,Seg width B\Seg width A) by A1,MATRIX13:46,FINSEQ_1:4 .= B by A1,Th19; thus B^^A = Segm(BA,Seg L,Seg width B) by A3,MATRIX13:46 .=B by Th19; end; end; theorem Th23: for A,B be Matrix of K st B = 0.(K,len A,m) holds the_rank_of A = the_rank_of (A^^B) proof let A,B be Matrix of K such that A1: B = 0.(K,len A,m); set L=len A; reconsider A'=A as Matrix of L,width A,K by MATRIX_2:7; A2: len B = len A by A1,MATRIX_1:def 3; then reconsider B'=B as Matrix of L,width B,K by MATRIX_2:7; set AB=A'^^B'; per cases; suppose width B=0; hence thesis by A2,Th22; end; suppose width B>0; then L>0 by A2,MATRIX_1:def 4; then A3: width AB=width A+width B & len AB=L by MATRIX_1:24; then width A <= width AB by NAT_1:11; then A4: Seg width A c= Seg width AB by FINSEQ_1:7; now let i such that A5: i in Seg width AB \ Seg width A; A6: i in Seg width AB & not i in Seg width A by A5,XBOOLE_0:def 4; then A7: 1<=i & (i<1 or i>width A) by FINSEQ_1:3; then reconsider n=i-width A as Element of NAT by NAT_1:21; n<>0 by A7; then A8: n>0 & i=n+width A; then A9: n in Seg width B by A6,A3,FINSEQ_1:82; then A10: Col(AB,i)=Col(B',n) by Th17,A8; set L0=len AB |-> 0.K; A11: len Col(B,n)=L & len L0=L by A2,A3,FINSEQ_2:109; now let i such that A12: 1<=i & i<=L; i in NAT by ORDINAL1:def 13; then i in Seg L & Seg L=dom B by A2,A12,FINSEQ_1:def 3; then L0.i=0.K & Col(B',n).i=B'*(i,n) & [i,n] in Indices B by A3,A9,A12,MATRIX_1:def 9,FINSEQ_2:71,ZFMISC_1:106; hence Col(B',n).i=L0.i by A1,MATRIX_3:3; end; hence Col(AB,i) = len AB |-> 0.K by A10,A11,FINSEQ_1:18; end; hence the_rank_of (A^^B) = the_rank_of Segm(AB,Seg len AB,Seg width A) by A4,Th12 .= the_rank_of A by A3,Th19; end; end; theorem Th24: for A,B be Matrix of K st the_rank_of A = the_rank_of (A^^B) & len A = len B for N st N c= dom A & for i st i in N holds Line(A,i)=width A|->0.K holds for i st i in N holds Line(B,i) = width B|->0.K proof let A,B be Matrix of K such that A1: the_rank_of A = the_rank_of (A^^B) & len A=len B; reconsider A'=A as Matrix of len A,width A,K by MATRIX_2:7; reconsider B'=B as Matrix of len A,width B,K by A1,MATRIX_2:7; set AB=A'^^B'; let N such that A2: N c= dom A and A3: for i st i in N holds Line(A,i)=width A|->0.K; let i such that A4: i in N; assume Line(B,i)<>width B|->0.K; then consider j such that A5: j in Seg width B & Line(B,i).j<>(width B|->0.K).j by FINSEQ_2:139; A6: dom A=Seg len A by FINSEQ_1:def 3; len A<>0 by A2,A4,FINSEQ_1:4,def 3; then len A >0; then A7: width AB=width A+width B & dom AB=Seg len AB & len AB=len A &Indices AB= [:Seg len A,Seg (width A+width B):] by MATRIX_1:24,FINSEQ_1:def 3; then A8: j+width A in Seg width AB by A5,FINSEQ_1:81; A9: len Line(B',i)=width B' & len Line(A',i)=width A' by MATRIX_1:def 8; then A10: 1<=j & j<=len Line(B',i) by A5,FINSEQ_1:3; AB*(i,j+width A) = Line(AB,i).(j+width A) by A8,MATRIX_1:def 8 .= (Line(A',i)^Line(B',i)).(j+width A) by A2,A4,A6,Th15 .= Line(B',i).j by A9,A10,FINSEQ_1:86; then A11: AB*(i,j+width A)<> 0.K by FINSEQ_2:71,FINSEQ_1:4,A5; consider P,Q be without_zero finite Subset of NAT such that A12: [:P,Q:] c= Indices A' & card P = card Q and A13: card P = the_rank_of A' and A14: Det EqSegm(A',P,Q)<>0.K by MATRIX13:def 4; A15: Segm(AB,Seg len A,Seg width A)=A by Th19; P={} iff Q={} by A12,CARD_1:47,CARD_2:59; then consider P2,Q2 be without_zero finite Subset of NAT such that A16: P2 c= Seg len A & Q2 c= Seg width A and A17: P2 = Sgm Seg len A.:P & Q2=Sgm Seg width A.:Q and card P2=card P & card Q2=card Q and A18: Segm(A,P,Q) = Segm(AB,P2,Q2) by A12,A15,MATRIX13:57; width A <= width AB by A7,NAT_1:11; then A19: Seg width A c= Seg width AB by FINSEQ_1:7; then A20: [:P2,Seg width A:] c= Indices AB by A16,A7,ZFMISC_1:119; not i in P2 proof assume A21: i in P2; A22: Sgm Seg len A = idseq len A by FINSEQ_3:54 .= id (Seg len A); A23: P c= Seg len A & Q c= Seg width A by A12,MATRIX13:67; then A24: i in P by A21,A17,FUNCT_1:162,A22; A25: dom Sgm P=Seg card P & rng Sgm P=P & dom Sgm Q=Seg card Q & rng Sgm Q=Q by A23,FINSEQ_3:45,FINSEQ_1:def 13; then consider x such that A26: x in dom Sgm P & Sgm P.x=i by A24,FUNCT_1:def 5; reconsider x as Element of NAT by A26; A27: dom Line(A,i)=Seg width A by FINSEQ_2:144; Line(A,i) = width A|->0.K by A3,A4 .= 0.K*Line(A,i) by FVSUM_1:71; then Line(Segm(A,P,Q),x)=(0.K*Line(A,i)) * Sgm Q & Line(Segm(A,P,Q),x)=Line(A,i)* Sgm Q by A23,A25,A26,MATRIX13:47; then Line(Segm(A,P,Q),x)=0.K * Line(Segm(A,P,Q),x) & Segm(A,P,Q)=EqSegm(A,P,Q) by A12,A23,A25,A27,MATRIX13:87,def 3; then 0.K*Det EqSegm(A,P,Q) = Det RLine(EqSegm(A,P,Q),x,Line(EqSegm(A,P,Q),x)) by MATRIX11:35,A25,A26 .= Det EqSegm(A,P,Q) by MATRIX11:30; hence thesis by A14,VECTSP_1:36; end; then A28: i in dom AB\P2 by A2,A4,A6,A7,XBOOLE_0:def 4; j>=1 by A5,FINSEQ_1:3; then j+width A >=1+width A by XREAL_1:8; then j+width A >width A by NAT_1:13; then not j+width A in Q2 by A16,FINSEQ_1:3; then A29: j+width A in Seg width AB\Q2 by A8,XBOOLE_0:def 4; A30: card Seg len A=len A & card Seg width A=width A by FINSEQ_1:78; A31: Sgm (Seg len A).i = (idseq len A).i by FINSEQ_3:54 .= i by A6,A2,A4,FINSEQ_1:4,FINSEQ_2:57; card (Seg width A) |->0.K = Line(A,i) by A3,A4,A30 .= Line(AB,i) * Sgm (Seg width A) by A31,A30,A19,A15,MATRIX13:47,A2,A4,A6; then A32: card P > the_rank_of Segm(AB,P2,Q2) by A1,A16,Th10,A20,A28,A29,A11, A13; Segm(AB,P2,Q2)=EqSegm(A,P,Q) by A12,A18,MATRIX13:def 3; hence thesis by A32,A14,MATRIX13:83; end; begin ::Basic properties of two transformations which ::transform finite sequences to matrices reserve D for non empty set, bD for FinSequence of D, b,f,g for FinSequence of K, MD for Matrix of D; definition let D be non empty set; let b be FinSequence of D; func LineVec2Mx b -> Matrix of 1,len b,D equals <*b*>; coherence; func ColVec2Mx b -> Matrix of len b,1,D equals <*b*>@; coherence proof set B=<*b*>; A1: len B=1 & width B=len b & len (B@)=width B by MATRIX_1:24,def 7; per cases; suppose A2: len b=0; then B@={} by A1,FINSEQ_1:25; hence thesis by A2,MATRIX_1:13; end; suppose len b>0; then width (B@)=len B by A1,MATRIX_2:12; hence thesis by A1,MATRIX_2:7; end; end; end; theorem Th25: MD = LineVec2Mx bD iff Line(MD,1) = bD & len MD = 1 proof thus MD = LineVec2Mx bD implies Line(MD,1) = bD & len MD = 1 proof assume A1: MD = LineVec2Mx bD; 1 in Seg 1; then Line(LineVec2Mx bD,1)=(LineVec2Mx bD).1 by MATRIX_2:10; hence thesis by A1,FINSEQ_1:57; end; assume A2: Line(MD,1) = bD & len MD = 1; then reconsider md=MD as Matrix of 1,width MD,D by MATRIX_2:7; 1 in Seg 1; then md.1=bD by A2,MATRIX_2:10; hence thesis by A2,FINSEQ_1:57; end; theorem Th26: ( len MD <> 0 or len bD <> 0 ) implies ( MD = ColVec2Mx bD iff Col(MD,1) = bD & width MD = 1 ) proof assume A1: len MD <> 0 or len bD <> 0; thus MD = ColVec2Mx bD implies Col(MD,1) = bD & width MD = 1 proof assume A2: MD = ColVec2Mx bD; len (LineVec2Mx bD)=1 by Th25; then dom (LineVec2Mx bD)=Seg 1 & 1 in Seg 1 by FINSEQ_1:def 3; hence Col(MD,1) = Line(LineVec2Mx bD,1) by A2,MATRIX_2:16 .= bD by Th25; A3: len MD=len bD by A2,MATRIX_1:def 3; then len MD>0 by A1; hence width MD=1 by A2,A3,MATRIX_1:24; end; assume A4: Col(MD,1) = bD & width MD = 1; then A5: len bD=len MD & len (MD@)=1 by MATRIX_1:def 9,def 7; then A6: len MD>0 by A1; 1 in Seg 1; then Line(MD@,1)=bD by A4,MATRIX_2:17; then (LineVec2Mx bD)@ = (MD@)@ by A5,Th25 .= MD by A4,A6,MATRIX_2:15; hence thesis; end; theorem len f = len g implies (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g) proof assume A1: len f = len g; then reconsider F=f,G=g as Element of (len f)-tuples_on the carrier of K by FINSEQ_2:110; set FG=F+G; set Lf=LineVec2Mx f; set Lg=LineVec2Mx g; set Lfg=LineVec2Mx FG; A2: len FG=len f & len Lfg=1 & len Lf=1 & len Lg=1 & len (Lf+Lg)=len Lf & width (Lf+Lg)=width Lf & width Lf=len f & width Lg=len f &width Lfg=len FG by A1,MATRIX_1:24,MATRIX_3:def 3,FINSEQ_2:109; per cases; suppose len f=0; then for i,j st [i,j] in Indices (Lf+Lg) holds (Lf+Lg)*(i,j) = Lfg*(i,j) by A2,FINSEQ_1:4,ZFMISC_1:113; hence thesis by A2,MATRIX_1:21; end; suppose len f>0; then len f in Seg len f & dom Lf=Seg 1 & 1 in Seg 1 by A2,FINSEQ_1:5,def 3; then [1,len f] in Indices Lf by A2,ZFMISC_1:106; then Line(Lf+Lg,1) = Line(Lf,1)+Line(Lg,1) by A2,MATRIX_4:59 .= f+Line(Lg,1) by Th25 .= f+g by Th25; hence thesis by A2,Th25; end; end; theorem Th28: len f = len g implies (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g) proof assume A1: len f = len g; then reconsider F=f,G=g as Element of (len f)-tuples_on the carrier of K by FINSEQ_2:110; set FG=F+G; set Cf=ColVec2Mx f; set Cg=ColVec2Mx g; set Cfg=ColVec2Mx FG; A2: len FG=len f & len Cfg=len FG & len Cf=len f & len Cg=len f & len (Cf+Cg)=len Cf & width (Cf+Cg)=width Cf by A1,MATRIX_1:def 3,MATRIX_3:def 3,FINSEQ_2:109; per cases; suppose len f=0; then Cf+Cg={} & Cfg={} by A2,FINSEQ_1:25; hence thesis; end; suppose A3: len f>0; then A4: len f in Seg len f & dom Cf=Seg len f & 1 in Seg 1 & width Cf= 1& width Cg=1 by A1,A2,FINSEQ_1:5,def 3,MATRIX_1:24; then [len f,1] in Indices Cf by ZFMISC_1:106; then Col(Cf+Cg,1) = Col(Cf,1)+Col(Cg,1) by MATRIX_4:60,A2,A4 .= f+Col(Cg,1) by Th26,A3 .= f+g by Th26,A3,A1; hence thesis by Th26,A2,A3,A4; end; end; theorem a * LineVec2Mx f =LineVec2Mx (a*f) proof A1: len (LineVec2Mx f)=1 & len (a*LineVec2Mx f)=len (LineVec2Mx f) by MATRIX_1:def 3,MATRIX_3:def 5; then Line(a * LineVec2Mx f,1) = a*Line(LineVec2Mx f,1) by MATRIXR1:20 .= a*f by Th25; hence thesis by A1,Th25; end; theorem Th30: a * ColVec2Mx f = ColVec2Mx (a*f) proof A1: len f=len (a*f) by MATRIXR1:16; per cases; suppose len f=0; then len (ColVec2Mx f)= 0 & len (ColVec2Mx (a*f))= 0 & len (ColVec2Mx f)=len (a*ColVec2Mx f) by A1,MATRIX_1:def 3,MATRIX_3:def 5; then a * ColVec2Mx f = {} & ColVec2Mx (a*f) = {} by FINSEQ_1:25; hence thesis; end; suppose A2: len f>0; then A3: width ColVec2Mx f=1 & width (a*ColVec2Mx f)=width ColVec2Mx f & width ColVec2Mx (a*f)=1 by A1,MATRIX_1:24,MATRIX_3:def 5; then Col(a * ColVec2Mx f,1) = a*Col(ColVec2Mx f,1) by MATRIXR1:19 .= a*f by Th26,A2; hence thesis by A1,A2,A3,Th26; end; end; theorem LineVec2Mx (k|->0.K) = 0.(K,1,k) proof reconsider L=LineVec2Mx (k|->0.K) as Matrix of 1,k,K by FINSEQ_2:69; set Z=0.(K,1,k); now let i,j such that A1: [i,j] in Indices L; A2: j in Seg width L & i in dom L & dom L = Seg len L & len L=1 by A1,ZFMISC_1:106,MATRIX_1:def 3,FINSEQ_1:def 3; then A3: i=1 by TARSKI:def 1,FINSEQ_1:4; A4: width L=k by MATRIX_1:24; Indices Z=Indices L by MATRIX_1:27; hence Z*(i,j) = 0.K by A1,MATRIX_3:3 .= (k|->0.K).j by A2,A4,FINSEQ_2:71,FINSEQ_1:4 .= Line(L,i).j by A3,Th25 .= L*(i,j) by A2,MATRIX_1:def 8; end; hence thesis by MATRIX_1:28; end; theorem Th32: ColVec2Mx (k|->0.K) = 0.(K,k,1) proof reconsider C=ColVec2Mx (k|->0.K) as Matrix of k,1,K by FINSEQ_2:69; set Z=0.(K,k,1); now let i,j such that A1: [i,j] in Indices C; A2: i in dom C & j in Seg width C & dom C=Seg len C & len C=len (k|->0.K) & len (k|->0.K)=k by A1,ZFMISC_1:106,MATRIX_1:def 3,FINSEQ_1:def 3,FINSEQ_2:69; then width C=1 by Th26,FINSEQ_1:4; then A3: j=1 by A2,TARSKI:def 1,FINSEQ_1:4; Indices Z=Indices C by MATRIX_1:27; hence Z*(i,j) = 0.K by A1,MATRIX_3:3 .= (k|->0.K).i by A2,FINSEQ_2:71,FINSEQ_1:4 .= Col(C,j).i by A2,A3,Th26,FINSEQ_1:4 .= C*(i,j) by A2,MATRIX_1:def 9; end; hence thesis by MATRIX_1:28; end; begin :: Basis properties of the Solution of Linear Equations definition let K; let A,B; func Solutions_of(A,B) -> set equals {X : len X = width A & width X = width B & A * X = B}; coherence; end; theorem Th33: Solutions_of(A,B) is non empty implies len A = len B proof assume Solutions_of(A,B) is non empty; then consider x such that A1: x in Solutions_of(A,B) by XBOOLE_0:def 1; ex X st X=x & len X= width A & width X = width B & A * X = B by A1; hence thesis by MATRIX_3:def 4; end; theorem X in Solutions_of(A,B) & i in Seg width X & Col(X,i) = len X |-> 0.K implies Col(B,i) = len B |-> 0.K proof assume that A1: X in Solutions_of(A,B) and A2: i in Seg width X and A3: Col(X,i) = len X |-> 0.K; consider X1 such that A4: X = X1 & len X1 = width A & width X1 = width B and A5: A * X1 = B by A1; set LB0=len B |-> 0.K; A6: len Col(B,i) = len B & len LB0 = len B by FINSEQ_2:109; now let k such that A7: 1 <=k & k <= len B; k in NAT by ORDINAL1:def 13; then A8: k in Seg len B & Indices B=[:Seg len B,Seg width B:] by A7, FINSEQ_1:def 3; then [k,i] in Indices B & width A=len X1 by A2,A4,ZFMISC_1:106; then A9: B*(k,i) = Line(A,k) "*" Col(X1,i) by A5,MATRIX_3:def 4 .= Sum(0.K*Line(A,k)) by FVSUM_1:80,A3,A4 .= 0.K* Sum(Line(A,k)) by FVSUM_1:92 .= 0.K by VECTSP_1:36 .= LB0.k by A7,A8,FINSEQ_2:71; k in dom B by A8,FINSEQ_1:def 3; hence (Col(B,i)).k=LB0.k by A9,MATRIX_1:def 9; end; hence thesis by A6,FINSEQ_1:18; end; theorem Th35: X in Solutions_of(A,B) implies a*X in Solutions_of(A,a*B) & X in Solutions_of(a*A,a*B) proof assume X in Solutions_of(A,B); then consider X1 such that A1: X = X1 & len X1 = width A & width X1 = width B and A2: A * X1 = B; A3: len (a*X) = width A & width (a*X) = width X1 & width (a*B) = width B & len (a*A)=len A & width (a*A)=width A by A1,MATRIX_3:def 5; A*(a*X)=a*(A*X) & (a*A)*X=a*(A*X) by A1,Th1,MATRIXR1:22; hence thesis by A1,A2,A3; end; theorem a <> 0.K implies Solutions_of(A,B) = Solutions_of(a*A,a*B) proof assume A1: a<>0.K; thus Solutions_of(A,B) c= Solutions_of(a*A,a*B) proof let x such that A2: x in Solutions_of(A,B); ex X st x=X & len X = width A & width X = width B & A * X = B by A2; hence thesis by A2,Th35; end; let x such that A3: x in Solutions_of(a*A,a*B); consider X such that A4: x=X & len X = width (a*A) & width X = width (a*B) and (a*A) * X = (a*B) by A3; A5: a"*(a*A) = (a"*a)*A by Th2 .= 1_K *A by A1,VECTSP_1:def 22 .= A by Th2; a"*(a*B) = (a"*a)*B by Th2 .= 1_K*B by A1,VECTSP_1:def 22 .= B by Th2; hence thesis by A3,A4,A5,Th35; end; Lm3: for D be non empty set for A,B be Matrix of D st len A = len B & width A = 0 & width B = 0 holds A = B proof let D be non empty set; let A,B be Matrix of D such that A1: len A = len B & width A = 0 & width B = 0; for i,j st [i,j] in Indices A holds A*(i,j) = B*(i,j) by ZFMISC_1:113,A1,FINSEQ_1:4; hence thesis by A1,MATRIX_1:21; end; theorem Th37: X1 in Solutions_of(A,B1) & X2 in Solutions_of(A,B2) & width B1 = width B2 implies X1 + X2 in Solutions_of(A,B1 + B2) proof assume that A1: X1 in Solutions_of(A,B1) & X2 in Solutions_of(A,B2) and A2: width B1 = width B2; consider Y1 be Matrix of K such that A3: Y1 = X1 & len Y1 = width A & width Y1 = width B1 and A4: A * Y1 = B1 by A1; consider Y2 be Matrix of K such that A5: Y2 = X2 & len Y2 = width A & width Y2 = width B2 and A6: A * Y2 = B2 by A1; A7: len (X1+X2) = len X1 & width (X1+X2) = width X1 & width (B1+B2) = width B1 by MATRIX_3:def 3; now per cases; suppose len A=0; then A8: len (A*X1) = 0 & len (A*(X1+X2)) = 0 by A3,A7,MATRIX_3:def 4; then len (A*X1 + A*X2) = 0 by MATRIX_3:def 3; hence A*(X1+X2) = A*X1 + A*X2 by A8,MATRIX_1:37; end; suppose len X1=0; then width (A*X1)=0 & len (A*X1)=len A by A3,A4,MATRIX_3:def 4,MATRIX_1:def 4; then width (A*X1 + A*X2)=0 & len (A*X1+A*X2)=len A & len (A*(X1+X2))= len A & width (A*(X1+X2)) = 0 by A3,A4,A7,MATRIX_3:def 3,def 4; hence A*(X1+X2)=A*X1+A*X2 by Lm3; end; suppose len A>0 & len X1>0; hence A*(X1+X2)=A*X1 + A*X2 by A2,A3,A5,MATRIX_4:62; end; end; hence thesis by A3,A4,A6,A5,A7; end; theorem Th38: X in Solutions_of(A',B') implies X in Solutions_of(RLine(A',i,a*Line(A',i)),RLine(B',i,a*Line(B',i))) proof assume A1: X in Solutions_of(A',B'); then consider X1 be Matrix of K such that A2: X = X1 & len X1 = width A' & width X1 = width B' and A3: A' * X1 = B'; set LA=Line(A',i); set LB=Line(B',i); set RA=RLine(A',i,a*LA); set RB=RLine(B',i,a*LB); set RX=RA*X1; A4: len (a*LA)=len LA & len LA= width A' & len (a*LB)=len LB & len LB=width B' & len A'=len B' by A1,Th33,MATRIXR1:16,FINSEQ_2:109; then A5: len RA=len A' & width RA=width A' & len RB=len B' & width RB=width B' by MATRIX11:def 3; then A6: len RX=len RA & width RX=width X1 by A2,MATRIX_3:def 4; dom B'=Seg len RA by A4,A5,FINSEQ_1:def 3; then A7: Indices RX=Indices B' & Indices RB=Indices B' by A2,MATRIX_1:27,A6,FINSEQ_1:def 3; now let j,k such that A8: [j,k] in Indices RB; len B'=m by MATRIX_1:def 3; then A9: j in dom B' & dom B'=Seg m & k in Seg width B' & len LB= width B' by A7,A8,ZFMISC_1:106,FINSEQ_1:def 3,MATRIX_1:def 8; then B'*(i,k)=LB.k by MATRIX_1:def 8; then reconsider LBk=LB.k as Element of K; A10: B'*(j,k)= Line(A',j) "*" Col(X1,k) by A2,A3,A7,A8,MATRIX_3:def 4; now per cases; suppose A11: j=i; then Line(RA,i)=a*LA by A4,A9,MATRIX11:28; hence RX*(j,k) = (a*LA)"*"Col(X1,k) by A2,A5,A7,A8,A11,MATRIX_3:def 4 .= Sum(a*mlt(LA,Col(X1,k))) by FVSUM_1:82,A2 .= a*Sum(mlt(LA,Col(X1,k))) by FVSUM_1:92 .= a*LBk by A9,A10,A11,MATRIX_1:def 8 .= (a*LB).k by A9,FVSUM_1:63 .= RB*(j,k) by A11,A4,A7,A8,MATRIX11:def 3; end; suppose A12: j<>i; then Line(RA,j)=Line(A',j) by A9,MATRIX11:28; hence RX*(j,k) = Line(A',j)"*"Col(X1,k) by A2,A5,A7,A8,MATRIX_3:def 4 .= B'*(j,k) by A2,A3,A7,A8,MATRIX_3:def 4 .= RB*(j,k) by A12,A4,A7,A8,MATRIX11:def 3; end; end; hence RB*(j,k) = RX*(j,k); end; then RX=RB by A2,A4,A5,A6,MATRIX_1:21; hence thesis by A2,A5; end; Lm4: a <> 0.K implies Solutions_of(A',B') = Solutions_of(RLine(A',i,a*Line(A',i)),RLine(B',i,a*Line(B',i))) proof assume A1: a <> 0.K; set RA=RLine(A',i,a*Line(A',i)); set RB=RLine(B',i,a*Line(B',i)); thus Solutions_of(A',B') c= Solutions_of(RA,RB) proof let x such that A2: x in Solutions_of(A',B'); ex X st x=X & len X = width A' & width X = width B' & A' * X = B' by A2; hence thesis by A2,Th38; end; let x such that A3: x in Solutions_of(RA,RB); per cases; suppose A4: not i in Seg m; len A'=m & len B'=m by MATRIX_1:def 3; then RA=A' & RB=B' by A4,MATRIX13:40; hence x in Solutions_of(A',B') by A3; end; suppose A5: i in Seg m; consider X such that A6: x=X & len X = width RA & width X = width RB and RA * X = RB by A3; set RRA=RLine(RA,i,a"*Line(RA,i)); set RRB=RLine(RB,i,a"*Line(RB,i)); A7: len (a*Line(A',i))=width A' & len (a"*Line(RA,i))=width RA & len (a*Line(B',i))=width B' & len (a"*Line(RB,i))=width RB by FINSEQ_2:109; then A8: width RA=width A' & width RB=width B' by MATRIX11:def 3; reconsider aLA=a*Line(A',i),aLB=a*Line(B',i),aLAR=a"*Line(RA,i), aLBR=a"*Line(RB,i) as Element of (the carrier of K)* by FINSEQ_1:def 11; A9: a"*Line(RA,i) = a"*(a*Line(A',i)) by A5,A7,MATRIX11:28 .= (a"*a)*Line(A',i) by FVSUM_1:67 .= 1_K * Line(A',i) by A1,VECTSP_1:def 22 .= Line(A',i) by FVSUM_1:70; A10: a"*Line(RB,i) = a"*(a*Line(B',i)) by A5,A7,MATRIX11:28 .= (a"*a)*Line(B',i) by FVSUM_1:67 .= 1_K * Line(B',i) by A1,VECTSP_1:def 22 .= Line(B',i) by FVSUM_1:70; A11: RRA = Replace(RA,i,aLAR) by A7,MATRIX11:29 .= Replace(Replace(A',i,aLA),i,aLAR) by A7,MATRIX11:29 .= Replace(A',i,aLAR) by FUNCT_7:36 .= RLine(A',i,Line(A',i)) by A7,A8,A9,MATRIX11:29 .= A' by MATRIX11:30; RRB = Replace(RB,i,aLBR) by A7,MATRIX11:29 .= Replace(Replace(B',i,aLB),i,aLBR) by A7,MATRIX11:29 .= Replace(B',i,aLBR) by FUNCT_7:36 .= RLine(B',i,Line(B',i)) by A7,A8,A10,MATRIX11:29 .= B' by MATRIX11:30; hence x in Solutions_of(A',B') by A6,A11,A3,Th38; end; end; theorem Th39: X in Solutions_of(A',B') & j in Seg m & i <> j implies X in Solutions_of(RLine(A',i,Line(A',i) + a*Line(A',j)), RLine(B',i,Line(B',i) + a*Line(B',j))) proof assume that A1: X in Solutions_of(A',B') and A2: j in Seg m & i<>j; consider X1 such that A3: X = X1 & len X1 = width A' & width X1 = width B' and A4: A' * X1 = B' by A1; set LAi=Line(A',i); set LAj=Line(A',j); set LBi=Line(B',i); set LBj=Line(B',j); set RA=RLine(A',i,LAi+a*LAj); set RB=RLine(B',i,LBi+a*LBj); set RX=RA*X1; A5: len (LAi+a*LAj) = width A' & len (a*LAj) = width A' & len LAi = width A'& len (LBi+a*LBj) = width B' & len A' = len B' by A1,Th33,FINSEQ_2:109; then A6: len RA = len A' & width RA = width A' & len RB = len B' & width RB = width B' by MATRIX11:def 3; then A7: len RX = len RA & width RX=width X1 by A3,MATRIX_3:def 4; dom B'=Seg len RA by A5,A6,FINSEQ_1:def 3; then A8: Indices RX = Indices B' & Indices RB = Indices B' by A3,MATRIX_1:27,A7,FINSEQ_1:def 3; now let o,p be Nat such that A9: [o,p] in Indices RB; len B' = m by MATRIX_1:def 3; then A10: o in dom B' & dom B'=Seg m & p in Seg width B' by A8,A9,ZFMISC_1:106,FINSEQ_1:def 3; then [j,p] in Indices B' by A2,ZFMISC_1:106; then A11: B'*(o,p) = Line(A',o) "*" Col(X1,p) & B'*(j,p) = LAj"*"Col(X1,p ) & len Col(X1,p)=width A' by A3,A4,A8,A9,MATRIX_3:def 4,MATRIX_1:def 9; B'*(o,p)=Line(B',o).p & B'*(j,p)=LBj.p by A10,MATRIX_1:def 8; then reconsider LBop = Line(B',o).p,LBjp = LBj.p as Element of the carrier of K; reconsider CX=Col(X1,p) as Element of (width A')-tuples_on the carrier of K by A3; p in dom (a*LBj) by A10,FINSEQ_2:144; then (a*LBj).p in rng (a*LBj) & rng (a*LBj) c= the carrier of K by FUNCT_1:def 5,FINSEQ_1:def 4; then reconsider aLBjp=(a*Line(B',j)).p as Element of K; now per cases; suppose A12: o=i; then Line(RA,o)=LAi+a*LAj by A5,A10,MATRIX11:28; hence RX*(o,p) = (LAi+a*LAj) "*" CX by A3,A6,A8,A9,MATRIX_3:def 4 .= Sum(mlt(LAi,CX)+mlt(a*LAj,CX)) by A5,A11,MATRIX_4:56 .= Sum(mlt(LAi,CX)+a*mlt(LAj,CX)) by FVSUM_1:82 .= Sum(mlt(LAi,CX))+Sum(a*mlt(LAj,CX)) by FVSUM_1:95 .= B'*(o,p)+a*(B'*(j,p)) by A11,A12,FVSUM_1:92 .= LBop+a*(B'*(j,p)) by A10,MATRIX_1:def 8 .= LBop+a*LBjp by A10,MATRIX_1:def 8 .= LBop+aLBjp by A10,FVSUM_1:63 .= (LBi+a*LBj).p by A10,A12,FVSUM_1:22 .= RB*(o,p) by A12,A5,A8,A9,MATRIX11:def 3; end; suppose A13: o<>i; then Line(RA,o)=Line(A',o) by A10,MATRIX11:28; hence RX*(o,p) = Line(A',o)"*"Col(X1,p) by A3,A6,A8,A9,MATRIX_3:def 4 .= B'*(o,p) by A3,A4,A8,A9,MATRIX_3:def 4 .= RB*(o,p) by A13,A5,A8,A9,MATRIX11:def 3; end; end; hence RB*(o,p) = RX*(o,p); end; then RX=RB by A3,A5,A6,A7,MATRIX_1:21; hence thesis by A3,A6; end; Lm5: j in Seg m & i <> j implies Solutions_of(A',B') = Solutions_of(RLine(A',i,Line(A',i) + a*Line(A',j)), RLine(B',i,Line(B',i) + a*Line(B',j))) proof assume A1: j in Seg m & i <> j; set LA=Line(A',j); set LB=Line(B',j); set RA=RLine(A',i,Line(A',i) + a*LA); set RB=RLine(B',i,Line(B',i) + a*LB); thus Solutions_of(A',B') c= Solutions_of(RA,RB) proof let x such that A2: x in Solutions_of(A',B'); ex X st x=X & len X = width A' & width X = width B' & A' * X = B' by A2; hence thesis by A1,A2,Th39; end; let x such that A3: x in Solutions_of(RA,RB); per cases; suppose A4: not i in Seg m; len A'=m & len B'=m by MATRIX_1:def 3; then RA=A' & RB=B' by A4,MATRIX13:40; hence x in Solutions_of(A',B') by A3; end; suppose A5: i in Seg m; consider X such that A6: x=X & len X = width RA & width X = width RB and RA * X = RB by A3; set RRA=RLine(RA,i,Line(RA,i)+(-a)*Line(RA,j)); set RRB=RLine(RB,i,Line(RB,i)+(-a)*Line(RB,j)); A7: len (Line(A',i)+a*LA)=width A' & len (Line(B',i)+a*LB)=width B' & len (Line(RA,i)+(-a)*Line(RA,j))=width RA & len (Line(RB,i)+(-a)*Line(RB,j))=width RB by FINSEQ_2:109; then A8: width RA=width A' & width RB=width B' by MATRIX11:def 3; reconsider LLA=Line(A',i)+a*LA,LLB=Line(B',i)+a*LB, LLRA=Line(RA,i)+(-a)*Line(RA,j),LLRB=Line(RB,i)+(-a)*Line(RB,j) as Element of (the carrier of K)* by FINSEQ_1:def 11; A9: Line(RA,j)=LA & Line(RB,j)=LB & Line(RA,i)=Line(A',i)+a*LA & Line(RB,i)=Line(B',i)+a*LB by A1,A5,A7,MATRIX11:28; then A10: Line(RA,i)+(-a)*Line(RA,j)= Line(A',i)+a*LA+(-1_K*a)*LA by VECTSP_1:def 19 .= Line(A',i)+a*LA+((-1_K)*a)*LA by VECTSP_1:41 .= Line(A',i)+a*LA+(-1_K)*(a*LA) by FVSUM_1:67 .= Line(A',i)+a*LA+(-(a*LA)) by FVSUM_1:72 .= Line(A',i)+(a*LA+(-(a*LA))) by FINSEQOP:29 .= Line(A',i)+width A'|->0.K by FVSUM_1:35 .= Line(A',i) by FVSUM_1:28; A11: Line(RB,i)+(-a)*Line(RB,j)= Line(B',i)+a*LB+(-1_K*a)*LB by A9,VECTSP_1:def 19 .= Line(B',i)+a*LB+((-1_K)*a)*LB by VECTSP_1:41 .= Line(B',i)+a*LB+(-1_K)*(a*LB) by FVSUM_1:67 .= Line(B',i)+a*LB+(-(a*LB)) by FVSUM_1:72 .= Line(B',i)+(a*LB+(-(a*LB))) by FINSEQOP:29 .= Line(B',i)+width B'|->0.K by FVSUM_1:35 .= Line(B',i) by FVSUM_1:28; A12: RRA = Replace(RA,i,LLRA) by A7,MATRIX11:29 .= Replace(Replace(A',i,LLA),i,LLRA) by A7,MATRIX11:29 .= Replace(A',i,LLRA) by FUNCT_7:36 .= RLine(A',i,Line(RA,i)+(-a)*Line(RA,j)) by A7,A8,MATRIX11:29 .= A' by A10,MATRIX11:30; RRB = Replace(RB,i,LLRB) by A7,MATRIX11:29 .= Replace(Replace(B',i,LLB),i,LLRB) by A7,MATRIX11:29 .= Replace(B',i,LLRB) by FUNCT_7:36 .= RLine(B',i,Line(RB,i)+(-a)*Line(RB,j)) by A7,A8,MATRIX11:29 .= B' by A11,MATRIX11:30; hence x in Solutions_of(A',B') by A1,A3,A6,A12,Th39; end; end; theorem Th40: j in Seg m & (i = j implies a <> -1_K) implies Solutions_of(A',B') = Solutions_of(RLine(A',i,Line(A',i) + a*Line(A',j)), RLine(B',i,Line(B',i) + a*Line(B',j))) proof assume A1: j in Seg m & (i = j implies a <> -1_K); per cases; suppose i<>j; hence thesis by A1,Lm5; end; suppose A2: i=j; set LA=Line(A',i); set LB=Line(B',i); A3: 1_K+a <> 0.K proof assume 1_K+a=0.K; then -1.K = -1.K+(1_K+a) by RLVECT_1:def 7 .= (-1.K+1_K)+a by RLVECT_1:def 6 .= 0.K+a by VECTSP_1:66 .= a by RLVECT_1:def 7; hence thesis by A1,A2; end; A4: LA+a*LA = 1_K*LA+a*LA by FVSUM_1:70 .= (1_K+a)*LA by FVSUM_1:68; LB+a*LB = 1_K*LB+a*LB by FVSUM_1:70 .= (1_K+a)*LB by FVSUM_1:68; hence thesis by A2,A3,A4,Lm4; end; end; theorem Th41: X in Solutions_of(A,B) & i in dom A & Line(A,i) = width A |-> 0.K implies Line(B,i) = width B |-> 0.K proof assume that A1: X in Solutions_of(A,B) and A2: i in dom A & Line(A,i) = width A|->0.K; consider X1 be Matrix of K such that A3: X = X1 & len X1 = width A & width X1 = width B and A4: A * X1 = B by A1; set LB=Line(B,i); set wB0=width B |->0.K; A5: len LB=width B & len wB0=width B by FINSEQ_2:109; now let k such that A6: 1 <=k & k <= len LB; A7: k in NAT by ORDINAL1:def 13; len A=len B by Th33,A1; then dom A=Seg len B by FINSEQ_1:def 3; then A8: k in Seg width B & i in dom B by A6,A5,A2,A7,FINSEQ_1:def 3; then [i,k] in Indices B by ZFMISC_1:106; then B*(i,k) = Line(A,i) "*" Col(X,k) by A3,A4,MATRIX_3:def 4 .= Sum(0.K*Col(X,k)) by A2,A3,FVSUM_1:80 .= 0.K*Sum(Col(X,k)) by FVSUM_1:92 .= 0.K by VECTSP_1:36 .= wB0.k by A5,A6,A8,FINSEQ_2:71; hence wB0.k = LB.k by A8,MATRIX_1:def 8; end; hence thesis by A5,FINSEQ_1:18; end; Lm6: for nt be Element of n-tuples_on NAT holds i in Seg n implies Line(Segm(A,nt,Sgm Seg width A),i)=Line(A,nt.i) proof let nt be Element of n-tuples_on NAT; assume A1: i in Seg n; set S=Seg width A; len Line(A,nt.i)=width A by MATRIX_1:def 8; then dom Line(A,nt.i)=S & Sgm S = idseq width A by FINSEQ_1:def 3,FINSEQ_3:54; then Line(A,nt.i) * Sgm S = Line(A,nt.i) & rng Sgm S=S by RELAT_1:78,FINSEQ_1:def 13; hence thesis by A1,MATRIX13:24; end; theorem Th42: for nt be Element of n-tuples_on NAT st rng nt c= dom A & n>0 holds Solutions_of(A,B) c= Solutions_of(Segm(A,nt,Sgm Seg width A), Segm(B,nt,Sgm Seg width B)) proof let nt be Element of n-tuples_on NAT such that A1: rng nt c= dom A & n>0; set SA=Segm(A,nt,Sgm Seg width A); set SB=Segm(B,nt,Sgm Seg width B); let x such that A2: x in Solutions_of(A,B); consider X be Matrix of K such that A3: x = X & len X = width A & width X = width B and A4: A * X = B by A2; set SX=SA*X; A5: len A = len B by Th33,A2; A6: width SA=card Seg width A & width SB=card Seg width B & len SA=n & len SB=n by A1,MATRIX_1:24; then A7: width SA=width A & width SB=width B by FINSEQ_1:78; then A8: len SX=len SA & width SX=width X by A3,MATRIX_3:def 4; now let j,k such that A9: [j,k] in Indices SX; reconsider j'=j,k'=k as Element of NAT by ORDINAL1:def 13; j in dom SX & len SX=len SA by A9,ZFMISC_1:106,A3,A7,MATRIX_3:def 4; then A10: j in Seg n & dom nt=Seg n by A6,FINSEQ_1:def 3,FINSEQ_2:144; then A11: Line(SA,j)=Line(A,nt.j) & nt.j in rng nt by Lm6,FUNCT_1:def 5; then nt.j in dom A & dom A=Seg len B & width SX=width X by A1,A5,FINSEQ_1:def 3,A3,A7,MATRIX_3:def 4; then A12: nt.j in dom B & k in Seg width B & j in dom SB by A3,A6,A9,A10,FINSEQ_1:def 3,ZFMISC_1:106; then A13: [nt.j,k] in Indices B & [j,k] in Indices SB & width B<>0 & Sgm Seg width B=idseq width B by FINSEQ_1:4,FINSEQ_3:54,A7,ZFMISC_1:106; then A14: (Sgm Seg width B).k'=k by A12,FINSEQ_2:57; thus SX*(j,k) = Line(A,nt.j) "*" Col(X,k) by A3,A7,A9,A11,MATRIX_3:def 4 .= B*(nt.j',k) by A3,A4,A13,MATRIX_3:def 4 .= SB*(j,k) by A14,A13,MATRIX13:def 1; end; then SX=SB by A3,A6,A7,A8,MATRIX_1:21; hence thesis by A3,A7; end; theorem Th43: for nt be Element of n-tuples_on NAT st rng nt c= dom A & dom A = dom B & n > 0 & for i st i in (dom A) \ rng nt holds Line(A,i) = width A |-> 0.K & Line(B,i) = width B |-> 0.K holds Solutions_of(A,B) = Solutions_of(Segm(A,nt,Sgm Seg width A), Segm(B,nt,Sgm Seg width B)) proof let nt be Element of n-tuples_on NAT such that A1: rng nt c= dom A & dom A=dom B & n>0 and A2: for i st i in (dom A) \ rng nt holds Line(A,i) = width A |-> 0.K & Line(B,i) = width B |-> 0.K; set SA=Segm(A,nt,Sgm Seg width A); set SB=Segm(B,nt,Sgm Seg width B); A3: Solutions_of(SA,SB) c= Solutions_of(A,B) proof let x such that A4: x in Solutions_of(SA,SB); consider X be Matrix of K such that A5: x = X & len X = width SA & width X = width SB and A6: SA * X = SB by A4; set AX=A*X; A7: width SA=card Seg width A & width SB=card Seg width B by A1,MATRIX_1:24; then A8: width SA=width A & width SB=width B by FINSEQ_1:78; then A9: len AX = len A & Seg len A = dom B & dom B=Seg len B by A1,A5,MATRIX_3:def 4,FINSEQ_1:def 3; then len AX >= len B & len B >= len AX by FINSEQ_1:7; then A10: len AX = len B & width AX = width X by XXREAL_0:1,A5,A8,MATRIX_3: def 4; now let j,k such that A11: [j,k] in Indices AX; reconsider j'=j,k'=k as Element of NAT by ORDINAL1:def 13; A12: j in dom AX & dom AX=Seg len A & k in Seg width AX by A9,A11,ZFMISC_1:106,FINSEQ_1:def 3; now per cases; suppose j' in rng nt; then consider p be set such that A13: p in dom nt & nt.p=j' by FUNCT_1:def 5; reconsider p as Element of NAT by A13; A14: dom nt=Seg n by FINSEQ_2:144; Indices SB =[:Seg n,Seg card Seg width B:] by A1,MATRIX_1:24; then A15: [p,k] in Indices SB by A7,A10,A12,A13,A14,ZFMISC_1:106 ,A5; width B<>0 & Sgm Seg width B=idseq width B by A8,A5,A12,MATRIX_3:def 4,FINSEQ_1:4,FINSEQ_3:54; then A16: (Sgm Seg width B).k'=k by A5,A8,A10,A12,FINSEQ_2:57; Line(SA,p) = Line(A,j') by A13,Lm6,A14; hence AX*(j,k) = Line(SA,p)"*"Col(X,k) by A5,A8,A11,MATRIX_3:def 4 .= SB*(p,k') by A5,A6,A15,MATRIX_3:def 4 .= B*(j,k) by A13,A15,A16,MATRIX13:def 1; end; suppose not j' in rng nt; then j' in (dom A)\rng nt by A9,A12,A1,XBOOLE_0:def 4; then A17: Line(A,j) = width A|->0.K & Line(B,j) = width B|->0.K & width B<>0 by A2,A5,A8,A12,MATRIX_3:def 4,FINSEQ_1:4; hence AX*(j,k) = (width A|-> 0.K)"*"Col(X,k) by A5,A8,A11,MATRIX_3:def 4 .= Sum(0.K*Col(X,k)) by A5,A8,FVSUM_1:80 .= 0.K*Sum(Col(X,k)) by FVSUM_1:92 .= 0.K by VECTSP_1:36 .= Line(B,j).k by A5,A8,A10,A12,A17,FINSEQ_2:71 .= B*(j,k) by MATRIX_1:def 8,A5,A8,A10,A12; end; end; hence AX*(j,k)=B*(j,k); end; then AX = B by A5,A8,A10,MATRIX_1:21; hence thesis by A5,A8; end; Solutions_of(A,B) c= Solutions_of(SA,SB) by Th42,A1; hence thesis by A3,XBOOLE_0:def 10; end; theorem Th44: for N st N c= dom A & N is non empty holds Solutions_of(A,B) c= Solutions_of(Segm(A,N,Seg width A), Segm(B,N,Seg width B)) proof let N such that A1: N c= dom A & N is non empty; dom A=Seg len A & card N<>0 by A1,FINSEQ_1:def 3,CARD_2:59; then rng Sgm N = N & card N>0 by A1,FINSEQ_1:def 13; hence thesis by A1,Th42; end; theorem Th45: for N st N c= dom A & N is non empty & dom A = dom B & for i st i in (dom A) \ N holds Line(A,i) = width A |-> 0.K & Line(B,i) = width B |-> 0.K holds Solutions_of(A,B) = Solutions_of(Segm(A,N,Seg width A), Segm(B,N,Seg width B)) proof let N such that A1: N c= dom A & N is non empty & dom A=dom B and A2: for i st i in (dom A) \ N holds Line(A,i) = width A |-> 0.K & Line(B,i) = width B |-> 0.K; dom A=Seg len A & card N<>0 by A1,FINSEQ_1:def 3,CARD_2:59; then rng Sgm N = N & card N > 0 by A1,FINSEQ_1:def 13; hence thesis by A1,A2,Th43; end; theorem Th46: i in dom A & len A > 1 implies Solutions_of(A,B) c= Solutions_of(DelLine(A,i),DelLine(B,i)) proof assume A1: i in dom A & len A > 1; then reconsider l1=len A-1 as Element of NAT by NAT_1:20; A2: Seg len A=dom A & card Seg len A=l1+1 & (Seg len A)\{i}c= Seg len A by FINSEQ_1:def 3,78,XBOOLE_1:36; then Card ((Seg len A)\{i})=l1 & l1 > 1-1 by A1,STIRL2_1:65,XREAL_1:11; then A3: Solutions_of(A,B)c=Solutions_of(Segm(A,(Seg len A)\{i},Seg width A), Segm(B,(Seg len A)\{i},Seg width B)) by A2,Th44,CARD_1:47; let x such that A4: x in Solutions_of(A,B); len A=len B by A4,Th33; then Segm(A,(Seg len A)\{i},Seg width A)=Del(A,i) & Segm(B,(Seg len A)\{i},Seg width B)=Del(B,i) by MATRIX13:51; hence thesis by A3,A4; end; theorem for A,B,i st i in dom A & len A > 1 & Line(A,i) = width A |-> 0.K & i in dom B & Line(B,i) = width B |-> 0.K holds Solutions_of(A,B) = Solutions_of(DelLine(A,i),DelLine(B,i)) proof let A,B,i such that A1: i in dom A & len A > 1 and A2: Line(A,i) = width A |-> 0.K and A3: i in dom B & Line(B,i) = width B |-> 0.K; thus Solutions_of(A,B) c= Solutions_of(DelLine(A,i),DelLine(B,i)) by A1,Th46; set S=Seg len A; let x such that A4: x in Solutions_of(DelLine(A,i),DelLine(B,i)); consider mA be Nat such that A5: len A = mA + 1 & len Del(A,i) = mA by A1,FINSEQ_3:113; consider mB be Nat such that A6: len B = mB + 1 & len Del(B,i) = mB by A3,FINSEQ_3:113; A7: len B=len A & dom A=S by A4,A5,A6,Th33,FINSEQ_1:def 3; then A8: dom A=dom B by FINSEQ_1:def 3; reconsider l1=len A-1 as Element of NAT by A1,NAT_1:20; A9: card S=l1+1 & S\{i}c= Seg len A by FINSEQ_1:78,XBOOLE_1:36; then A10: Card (S\{i})=l1 & l1 > 1-1 by A1,A7,STIRL2_1:65,XREAL_1:11; now let j such that A11: j in (dom A)\(S\{i}); j in dom A /\{i} by A7,A11,XBOOLE_1:48; then j in {i} by XBOOLE_0:def 3; hence Line(A,j) = width A |-> 0.K & Line(B,j) = width B |-> 0.K by A2,A3,TARSKI:def 1; end; then Solutions_of(A,B) = Solutions_of(Segm(A,S\{i},Seg width A),Segm(B,S\{i},Seg width B)) by A7,A8,A9,A10,Th45,CARD_1:47 .= Solutions_of(DelLine(A,i),Segm(B,S\{i},Seg width B)) by MATRIX13:51 .= Solutions_of(DelLine(A,i),DelLine(B,i)) by A7,MATRIX13:51; hence thesis by A4; end; theorem for A be Matrix of n,m,K, B be Matrix of n,k,K for P be Function of Seg n,Seg n holds Solutions_of(A,B) c= Solutions_of(A*P,B*P) & (P is one-to-one implies Solutions_of(A,B) = Solutions_of(A*P,B*P)) proof let A be Matrix of n,m,K, B be Matrix of n,k,K; let P be Function of Seg n,Seg n; set IDn=idseq n; len IDn=n & IDn is FinSequence of NAT by FINSEQ_2:52,55; then reconsider IDn as Element of n-tuples_on NAT by FINSEQ_2:110; A1: dom IDn=Seg n & rng P c= Seg n & dom P=Seg n by RELSET_1:12,FUNCT_2:67; then reconsider IDnP=IDn*P as FinSequence of NAT by FINSEQ_2:51; A2: n in NAT by ORDINAL1:def 13; dom IDnP = Seg n by A1,RELAT_1:79; then len IDnP = n by FINSEQ_1:def 3,A2; then reconsider IDnP as Element of n-tuples_on NAT by FINSEQ_2:110; A3: IDn=Sgm Seg n & n=len A & len B=n & card Seg n=n & (idseq n)*P = P by A1,RELAT_1:79,FINSEQ_3:54,MATRIX_1:def 3,FINSEQ_1:78; then A4: Segm(A,IDnP,Sgm Seg width A) = Segm(A,Seg len A,Seg width A) * P by MATRIX13:33 .= A*P by MATRIX13:46; A5: Segm(B,IDnP,Sgm Seg width B) = Segm(B,Seg len B,Seg width B) * P by A3,MATRIX13:33 .= B*P by MATRIX13:46; A6: rng IDnP c=dom A by A1,A3,FINSEQ_1:def 3; per cases; suppose A7: n>0; hence Solutions_of(A,B)c=Solutions_of(A*P,B*P) by A4,A5,A6,Th42; assume A8: P is one-to-one; card Seg n = card Seg n; then P is onto by A8,STIRL2_1:70; then A9: rng P=Seg n by FUNCT_2:def 3; A10: dom A=Seg n & dom B=Seg n by A3,FINSEQ_1:def 3; then for i st i in (dom A) \ rng IDnP holds Line(A,i) = width A |-> 0.K & Line(B,i) = width B |-> 0.K by A3,A9,XBOOLE_1:37; hence Solutions_of(A,B)=Solutions_of(A*P,B*P) by A4,A5,Th43,A1,A3,A7,A10; end; suppose n=0; then len A=0 & len B=0 & len (A*P)=0 & len (B*P)=0 by MATRIX_1:23; then A={} & B={} & A*P={} & B*P = {} by FINSEQ_1:25; hence thesis; end; end; theorem Th49: for A be Matrix of n,m,K, N st card N = n & N c= Seg m & Segm(A,Seg n,N) = 1.(K,n) & n > 0 ex MVectors be Matrix of m-'n,m,K st Segm(MVectors,Seg (m-'n),Seg m \ N) = 1.(K,m-'n) & Segm(MVectors,Seg (m-'n),N) = -Segm(A,Seg n,Seg m \N)@ & for l for M be Matrix of m,l,K st for i st i in Seg l holds (ex j st j in Seg (m-'n) & Col(M,i) = Line(MVectors,j)) or Col(M,i) = m|->0.K holds M in Solutions_of(A,0.(K,n,l)) proof let A be Matrix of n,m,K,N such that A1: card N = n & N c= Seg m and A2: Segm(A,Seg n,N) = 1.(K,n) and A3: n>0; A4: len A=n & width A=m & Indices A=[:Seg n,Seg m:] by A3,MATRIX_1:24; set SN=Seg m\N; A5: SN c= Seg m by XBOOLE_1:36; then A6: [:Seg n,N:] c= Indices A & [:Seg n,SN:] c= Indices A by A1,A4, ZFMISC_1:119; set ZERO=0.(K,m-'n,m); A7: now per cases; suppose m-'n=0; then [:Seg (m-'n),N:] = {} & [:Seg (m-'n),SN:] ={} by ZFMISC_1:113,FINSEQ_1:4; hence [:Seg (m-'n),N:]c=Indices ZERO & [:Seg (m-'n),SN:]c=Indices ZERO by XBOOLE_1:2; end; suppose m-'n>0; then Indices ZERO = [:Seg (m-'n),Seg m:] by MATRIX_1:24; hence [:Seg (m-'n),N:]c=Indices ZERO & [:Seg (m-'n),SN:]c=Indices ZERO by A1,A5,ZFMISC_1:119; end; end; A8: card Seg m = m & card Seg n = n & card Seg (m-'n) = m-'n by FINSEQ_1:78; n c= card Seg m by A1,CARD_1:27; then A9: n <= m by A8,NAT_1:40; then A10: m-'n=m-n & card SN=m-n by A1,A8,BINARITH:50,CARD_2:63; set SA=Segm(A,Seg n,SN); set ONE= 1.(K,m-'n); A11: len SA=n & width SA=m-'n by A3,A8,A10,MATRIX_1:24; m-'n=0 or m-'n > 0; then (len (SA@)=0 & m-'n=0 or len (SA@)=m-'n & width (SA@)=n)& len (SA@)=len (-SA@) & width (SA@)=width (-SA@) by A11,MATRIX_2:12,MATRIX_3:def 2,MATRIX_1:def 7; then -SA@={} &m-'n=0 or -SA@ is Matrix of m-'n,n,K by FINSEQ_1:25,MATRIX_2:7; then reconsider SAT=-SA@ as Matrix of m-'n,n,K by MATRIX_1:13; A12: N misses SN by XBOOLE_1:79; [:Seg (m-'n),N:]/\[:Seg (m-'n),SN:] = [:Seg (m-'n),N/\SN:] by ZFMISC_1:122 .= [:Seg (m-'n),{}:] by A12,XBOOLE_0:def 7 .= {} by ZFMISC_1:113; then for i,j,bi,bj,ci,cj be Nat st [i,j] in [:Seg (m-'n),N:]/\[:Seg (m-'n),SN:] & bi = Sgm (Seg (m-'n))".i & bj = Sgm N".j & ci = Sgm (Seg (m-'n))".i & cj = Sgm SN".j holds SAT*(bi,bj) = ONE*(ci,cj); then consider V be Matrix of len ZERO,width ZERO,K such that A13: Segm(V,Seg(m-'n),N) = SAT & Segm(V,Seg (m-'n),SN) = ONE and for i,j st [i,j] in Indices V\([:Seg (m-'n),N:]\/[:Seg (m-'n),SN:]) holds V*(i,j) = ZERO*(i,j) by A1,A7,A8,A10,Th9; m-'n=0 or m-'n > 0; then len ZERO=0 & m-'n=0 & len V=len ZERO or len ZERO=m-'n & width ZERO=m by MATRIX_1:24,def 3; then V={} & m-'n=0 or V is Matrix of m-'n,m,K by FINSEQ_1:25; then reconsider V as Matrix of m-'n,m,K by MATRIX_1:13; take V; thus Segm(V,Seg (m-'n),SN) = ONE & Segm(V,Seg (m-'n),N)=-SA@ by A13; let l; let M be Matrix of m,l,K such that A14: for i st i in Seg l holds (ex j st j in Seg (m-'n) & Col(M,i) = Line(V,j)) or Col(M,i) = m|->0.K; set Z=0.(K,n,l); A15: len M=m & width M=l by A3,A9,MATRIX_1:24; then A16: len (A*M)=n & width (A*M)=l & width Z=l by A3,A4,MATRIX_3:def 4,MATRIX_1:24; then reconsider AM=A*M as Matrix of n,l,K by MATRIX_2:7; now let i,j such that A17: [i,j] in Indices AM; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 13; A18: Indices AM=[:Seg n,Seg l:] & Indices AM=Indices Z by A3,MATRIX_1:24,27; then A19: I in Seg n & J in Seg l by A17,ZFMISC_1:106; now per cases by A19,A14; suppose ex jj be Nat st jj in Seg (m-'n) & Col(M,J) = Line(V,jj); then consider jj be Nat such that A20: jj in Seg (m-'n) and A21: Col(M,J) = Line(V,jj); m-'n<>0 by A20,FINSEQ_1:4; then m-'n>0; then A22: len V=m-'n & width V=m & Indices V=[:Seg (m-'n),Seg m:]& Indices V=Indices ZERO by MATRIX_1:24,27; then len Line(A,I)=m & len Line(V,jj)=m by A4,MATRIX_1:def 8; then len mlt(Line(A,I),Line(V,jj))=m by MATRIX_3:8; then A23: dom mlt(Line(A,I),Line(V,jj))=Seg m by FINSEQ_1:def 3; A24: dom Sgm N=Seg n & rng Sgm N=N &dom Sgm SN=Seg(m-'n)& rng Sgm SN=SN& rng Sgm Seg n=Seg n & rng Sgm Seg(m-'n)=Seg(m-'n) & Sgm N is one-to-one & Sgm SN is one-to-one by A1,A5,A10,FINSEQ_1:def 13,FINSEQ_3:45,99; then A25: Sgm N.I in N by A19,FUNCT_1:def 5; A26: I = idseq n.I by A3,A19,FINSEQ_2:57 .= Sgm (Seg n).I by FINSEQ_3:54; then [Sgm (Seg n).I,Sgm N.I] in Indices A by A1,A4,A19,A25,ZFMISC_1:106; then A27: [I,I] in Indices Segm(A,Seg n,N) by A6,A24,MATRIX13:17; A28: Line(A,I).(Sgm N.I) = A*(I,Sgm N.I) by A1,A4,A25,MATRIX_1:def 8 .= Segm(A,Seg n,N)*(I,I) by A26,A27,MATRIX13:def 1 .= 1_K by A2,A27,MATRIX_1:def 12; A29: jj = idseq (m-'n).jj by A20,FINSEQ_1:4,FINSEQ_2:57 .= Sgm (Seg (m-'n)).jj by FINSEQ_3:54; then [Sgm (Seg (m-'n)).jj,Sgm N.I] in Indices V by A20,A1,A25,A22,ZFMISC_1:106; then A30: [jj,I] in Indices Segm(V,Seg(m-'n),N) & Indices SAT= Indices (SA@) by A7,A22,A24,MATRIX13:17,Lm1; then A31: [I,jj] in Indices SA by A13,MATRIX_1:def 7; A32: Line(V,jj).(Sgm N.I) = V*(jj,Sgm N.I) by A1,A25,A22,MATRIX_1:def 8 .= Segm(V,Seg(m-'n),N)*(jj,I) by A29,A30,MATRIX13:def 1 .= -((SA@)*(jj,I)) by A13,A30,MATRIX_3:def 2 .= -(SA*(I,jj)) by A31,MATRIX_1:def 7 .= -(A*(I,Sgm SN.jj)) by A26,A31,MATRIX13:def 1; A33: mlt(Line(A,I),Line(V,jj))/.(Sgm N.I) = mlt(Line(A,I),Line(V,jj)).(Sgm N.I) by A1,A25,A23,PARTFUN1:def 8 .= 1_K*(-(A*(I,Sgm SN.jj))) by A1,A4,A22,A25,A28,A32,FVSUM_1:74 .= -(A*(I,Sgm SN.jj)) by VECTSP_1:def 16; A34: Sgm SN.jj in SN by A20,A24,FUNCT_1:def 5; then A35: Line(A,I).(Sgm SN.jj)=A*(I,Sgm SN.jj) by A4,A5,MATRIX_1: def 8; A36: Indices ONE=[:Seg (m-'n),Seg (m-'n):] by MATRIX_1:25; then A37: [jj,jj] in Indices ONE by A20,ZFMISC_1:106; A38: Line(V,jj).(Sgm SN.jj)=V*(jj,Sgm SN.jj) by A5,A34,A22,MATRIX_1:def 8 .= ONE*(jj,jj) by A13,A29,A37,MATRIX13:def 1 .= 1_K by A37,MATRIX_1:def 12; A39: mlt(Line(A,I),Line(V,jj))/.(Sgm SN.jj) = mlt(Line(A,I),Line(V,jj)).(Sgm SN.jj) by A5,A34,A23,PARTFUN1:def 8 .= (A*(I,Sgm SN.jj))*1_K by A4,A5,A22,A35,A38,A34,FVSUM_1:74 .=A*(I,Sgm SN.jj) by VECTSP_1:def 16; A40: Sgm SN.jj <> Sgm N.I by A12,A25,A34,XBOOLE_0:3; now let kk be Nat such that A41: kk in Seg m and A42: kk<> Sgm SN.jj & kk<>Sgm N.I; now per cases by A41,XBOOLE_0:def 4; suppose kk in N; then consider x such that A43: x in dom Sgm N & Sgm N.x=kk by A24,FUNCT_1:def 5; reconsider x as Element of NAT by A43; [Sgm (Seg n).I,Sgm N.x] in Indices A by A26,A4,A19,A41,A43,ZFMISC_1:106; then A44: [I,x] in Indices Segm(A,Seg n,N) by A6,A24, MATRIX13:17; A45: Line(A,I).(Sgm N.x) = A*(I,Sgm N.x) by A4,A41,A43,MATRIX_1:def 8 .= Segm(A,Seg n,N)*(I,x) by A26,A44,MATRIX13:def 1 .= 0.K by A2,A44,A43,A42,MATRIX_1:def 12; Line(V,jj).(Sgm N.x) = V*(jj,Sgm N.x) by A41,A43,A22,MATRIX_1:def 8; hence mlt(Line(A,I),Line(V,jj)).kk = 0.K*(V*(jj,Sgm N.x)) by A4,A22,A45,A41,A43,FVSUM_1:74 .= 0.K by VECTSP_1:39; end; suppose kk in SN; then consider x such that A46: x in dom Sgm SN & Sgm SN.x=kk by A24,FUNCT_1:def 5; reconsider x as Element of NAT by A46; A47: Line(A,I).(Sgm SN.x)=A*(I,Sgm SN.x) by A4,A41,A46,MATRIX_1:def 8; A48: [jj,x] in Indices ONE by A20,A46,A24,A36,ZFMISC_1:106; Line(V,jj).(Sgm SN.x) = V*(jj,Sgm SN.x) by A22,A41,A46,MATRIX_1:def 8 .= ONE*(jj,x) by A29,A13,A48,MATRIX13:def 1 .= 0.K by A48,A46,A42,MATRIX_1:def 12; hence mlt(Line(A,I),Line(V,jj)).kk = (A*(I,Sgm SN.x))*0.K by A4,A22,A47,A41,A46,FVSUM_1:74 .= 0.K by VECTSP_1:39; end; end; hence mlt(Line(A,I),Line(V,jj)).kk=0.K; end; then Sum(mlt(Line(A,I),Line(V,jj))) = A*(I,Sgm SN.jj)+(-(A*(I,Sgm SN.jj))) by A33,A39,A23,Th7,A40,A1,A25,A5,A34 .= 0.K by VECTSP_1:63; hence Z*(i,j) = Line(A,I)"*"Line(V,jj) by A17,A18,MATRIX_3:3 .= AM*(i,j) by A4,A15,A17,A21,MATRIX_3:def 4; end; suppose Col(M,J) = m|->0.K; hence AM*(i,j) = Line(A,I)"*"(m|->0.K) by A4,A15,A17,MATRIX_3:def 4 .= Sum(0.K * Line(A,I)) by A4,FVSUM_1:80 .= 0.K*Sum(Line(A,I)) by FVSUM_1:92 .= 0.K by VECTSP_1:36 .= Z*(i,j) by A17,A18,MATRIX_3:3; end; end; hence AM*(i,j) = Z*(i,j); end; then AM = Z by MATRIX_1:28; hence thesis by A4,A15,A16; end; theorem Th50: for A be Matrix of n,m,K, B be Matrix of n,l,K, N st card N = n & N c= Seg m & n>0 & Segm(A,Seg n,N) = 1.(K,n) ex X be Matrix of m,l,K st Segm(X,Seg m \ N,Seg l) = 0.(K,m-'n,l) & Segm(X,N,Seg l) = B & X in Solutions_of(A,B) proof let A be Matrix of n,m,K, B be Matrix of n,l,K, N such that A1: card N = n & N c= Seg m & n>0 and A2: Segm(A,Seg n,N) = 1.(K,n); set SN=Seg m\N; A3: n <=card Seg m & card Seg m=m & card Seg n=n & card Seg l=l by A1,NAT_1:44,FINSEQ_1:78; then A4: m-'n=m-n & card SN=m-n & m>0 by A1,BINARITH:50,CARD_2:63; A5: SN c= Seg m by XBOOLE_1:36; set Z=0.(K,m,l); set ZERO=0.(K,m-'n,l); A6: len Z=m & width Z=l & Indices Z=[:Seg m,Seg l:] & len A=n & width A=m & Indices A=[:Seg n,Seg m:] & len B=n & width B=l & Indices B=[:Seg n,Seg l:] by A1,A3,MATRIX_1:24; then A7: [:SN,Seg l:] c= Indices Z & [:N,Seg l:] c= Indices Z by A5,A1,ZFMISC_1:118; A8: N misses SN by XBOOLE_1:79; [:N,Seg l:]/\[:SN,Seg l:] = [:N/\SN,Seg l:] by ZFMISC_1:122 .= [:{},Seg l:] by A8,XBOOLE_0:def 7 .= {} by ZFMISC_1:113; then for i,j,bi,bj,ci,cj be Nat st [i,j] in [:N,Seg l:]/\[:SN,Seg l:] & bi = Sgm N".i & bj = Sgm (Seg l)".j & ci = Sgm SN".i & cj = Sgm (Seg l)".j holds B*(bi,bj) = ZERO*(ci,cj); then consider X be Matrix of m,l,K such that A9: Segm(X,N,Seg l) = B & Segm(X,SN,Seg l) = ZERO and for i,j st [i,j] in Indices X\([:N,Seg l:]\/[:SN,Seg l:]) holds X*(i,j) = Z*(i,j) by A1,A3,A4,A6,A7,Th9; take X; thus Segm(X,SN,Seg l) = ZERO & Segm(X,N,Seg l) = B by A9; A10: len X=m & width X=l & Indices X=[:Seg m,Seg l:] by A3,MATRIX_1:24,A1; then A11: dom X=Seg m by FINSEQ_1:def 3; set AX=A*X; len AX=n & width AX=l by A6,A10,MATRIX_3:def 4; then reconsider AX as Matrix of n,l,K by MATRIX_2:7; now let i,j such that A12: [i,j] in Indices AX; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 13; A13: AX*(i,j) = Line(A,i)"*"Col(X,j) by A12,A6,A10,MATRIX_3:def 4 .= Sum(mlt(Line(A,i),Col(X,j))); Indices AX=Indices B by MATRIX_1:27; then A14: i in Seg n & j in Seg l by A6,A12,ZFMISC_1:106; A15: dom Sgm N=Seg n & rng Sgm N=N & rng Sgm (Seg n)=Seg n & rng Sgm (Seg l)=Seg l & rng Sgm SN=SN & dom Sgm SN=Seg (m-'n) & Sgm N is one-to-one by A1,A4,A5,FINSEQ_1:def 13,FINSEQ_3:45,99; then A16: Sgm N.i in N by A14,FUNCT_1:def 5; A17: [:Seg n,N:] c= Indices A & [:N,Seg l:] c= Indices X & [:SN,Seg l:] c= Indices X by A1,A5,A6,A10,ZFMISC_1:118; A18: i = (idseq n).i by A14,A1,FINSEQ_2:57 .= Sgm (Seg n).i by FINSEQ_3:54; then [Sgm (Seg n).i,Sgm N.i] in Indices A by A6,A16,A1,A14,ZFMISC_1:106; then A19: [I,I] in Indices 1.(K,n) by A2,A15,A17,MATRIX13:17; A20: Line(A,i).(Sgm N.i) = A*(I,Sgm N.I) by A1,A6,A16,MATRIX_1:def 8 .= (Segm(A,Seg n,N))*(I,I) by A2,A19,A18,MATRIX13:def 1 .= 1_K by A2,A19,MATRIX_1:def 12; A21: j = (idseq l).j by A14,FINSEQ_1:4,FINSEQ_2:57 .= Sgm (Seg l).j by FINSEQ_3:54; then [Sgm N.I,Sgm(Seg l).J] in Indices X by A10,A16,A1,A14,ZFMISC_1:106; then A22: [I,J] in Indices B by A9,A15,A17,MATRIX13:17; Col(X,j).(Sgm N.i) = X*(Sgm N.i,j) by A16,A1,A11,MATRIX_1:def 9 .= B*(I,J) by A9,A21,A22,MATRIX13:def 1; then A23: mlt(Line(A,i),Col(X,j)).(Sgm N.i) = 1_K * (B*(I,J)) by A20,A16,A1,A6,A10,FVSUM_1:74 .= B*(I,J) by VECTSP_1:def 13; len Line(A,i)=m & len Col(X,j)=m by A6,A10,FINSEQ_2:109; then len mlt(Line(A,i),Col(X,j))=m by MATRIX_3:8; then A24: dom mlt(Line(A,i),Col(X,j))=Seg m by FINSEQ_1:def 3; now let kk be Nat such that A25: kk in Seg m & kk <> Sgm N.I; per cases by A25,XBOOLE_0:def 4; suppose A26: kk in N; then consider x such that A27: x in dom Sgm N & Sgm N.x=kk by A15,FUNCT_1:def 5; reconsider x as Element of NAT by A27; [Sgm (Seg n).i,Sgm N.x] in Indices A by A1,A6,A14,A18,A26,A27,ZFMISC_1:106; then A28: [I,x] in Indices 1.(K,n) by A2,A15,A17,MATRIX13:17; A29: Line(A,i).(Sgm N.x) = A*(I,Sgm N.x) by A1,A6,A26,A27,MATRIX_1:def 8 .= (Segm(A,Seg n,N))*(I,x) by A2,A18,MATRIX13:def 1,A28 .= 0.K by MATRIX_1:def 12,A2,A25,A27,A28; Col(X,j).kk = X*(kk,j) by A26,A1,A11,MATRIX_1:def 9; hence mlt(Line(A,i),Col(X,j)).kk = 0.K*(X*(kk,j)) by A1,A27,A26,A29,A6,A10,FVSUM_1:74 .= 0.K by VECTSP_1:36; end; suppose A30: kk in SN; then consider x such that A31: x in dom Sgm SN & Sgm SN.x=kk by A15,FUNCT_1:def 5; reconsider x as Element of NAT by A31; [Sgm SN.x,Sgm (Seg l).J] in Indices X by A5,A10,A21,A14,A30,A31,ZFMISC_1:106; then A32: [x,J] in Indices ZERO by A9,A15,A17,MATRIX13:17; A33: Line(A,i).kk=A*(I,Sgm SN.x) by A6,A25,A31,MATRIX_1:def 8; Col(X,j).kk = X*(Sgm SN.x,Sgm (Seg l).j) by A21,A31,A5,A30,A11,MATRIX_1:def 9 .= ZERO*(x,J) by A9,MATRIX13:def 1,A32 .= 0.K by A32,MATRIX_3:3; hence mlt(Line(A,i),Col(X,j)).kk = (A*(I,Sgm SN.x))*0.K by A25,A33,A6,A10,FVSUM_1:74 .= 0.K by VECTSP_1:36; end; end; hence AX*(i,j)=B*(i,j) by A13,A16,A1,A23,A24,MATRIX_3:14; end; then AX=B by MATRIX_1:28; hence thesis by A6,A10; end; theorem Th51: for A be Matrix of 0,n,K, B be Matrix of 0,m,K holds Solutions_of(A,B) = {{}} proof let A be Matrix of 0,n,K, B be Matrix of 0,m,K; A1: len A=0 & len B=0 by MATRIX_1:def 3; then A2: width A=0 & B={} & width B=0 by MATRIX_1:def 4,FINSEQ_1:25; A3: Solutions_of(A,B) c= {{}} proof let x such that A4: x in Solutions_of(A,B); ex X st X=x &len X = width A & width X = width B & A * X = B by A4; then x={} by A2,FINSEQ_1:25; hence thesis by TARSKI:def 1; end; len (A*A)=0 by A1,A2,MATRIX_3:def 4; then A*A={} by FINSEQ_1:25; then A in Solutions_of(A,B) by A1,A2; hence thesis by A3,ZFMISC_1:39; end; theorem Th52: for B be Matrix of K st Solutions_of(0.(K,n,k),B) is non empty holds B = 0.(K,n,width B) proof let B be Matrix of K; set A=0.(K,n,k); assume Solutions_of(0.(K,n,k),B) is non empty; then consider x such that A1: x in Solutions_of(0.(K,n,k),B) by XBOOLE_0:def 1; consider X such that A2: X=x & len X = width A & width X = width B & A * X = B by A1; set ZERO=0.(K,n,width B); A3: len A=n & len ZERO=n by MATRIX_1:def 3; then A4: len B=len ZERO & dom A=Seg n by A1,Th33,FINSEQ_1:def 3; then reconsider B'=B as Matrix of n,width B,K by A3,MATRIX_2:7; now let i such that A5: 1<=i & i<=n; i in NAT by ORDINAL1:def 13; then A6: i in Seg n & n>0 & width A=k by A5,MATRIX_1:24; then Line(A,i) = A.i by MATRIX_2:10 .= width A|->0.K by A6,FINSEQ_2:71; then width B|-> 0.K = Line(B,i) by A1,A2,A4,A6,Th41 .= B'.i by A6,MATRIX_2:10; hence B.i=ZERO.i by A6,FINSEQ_2:71; end; hence thesis by FINSEQ_1:18,A3,A4; end; theorem Th53: for A be Matrix of n,k,K, B be Matrix of n,m,K st n > 0 holds x in Solutions_of(A,B) implies x is Matrix of k,m,K proof let A be Matrix of n,k,K, B be Matrix of n,m,K such that A1: n > 0; A2: width A=k & width B=m by A1,MATRIX_1:24; assume x in Solutions_of(A,B); then consider X such that A3: X=x & len X = k & width X = m & A * X = B by A2; thus thesis by A3,MATRIX_2:7; end; theorem Th54: n > 0 & k > 0 implies Solutions_of(0.(K,n,k),0.(K,n,m)) = {X where X is Matrix of k,m,K:not contradiction} proof assume A1: n > 0 & k > 0; set A=0.(K,n,k); set B=0.(K,n,m); set XX={X where X is Matrix of k,m,K:not contradiction}; thus Solutions_of(A,B) c= XX proof let x; assume x in Solutions_of(A,B); then x is Matrix of k,m,K by A1,Th53; hence thesis; end; let x such that A2: x in XX; consider X be Matrix of k,m,K such that A3: x=X & not contradiction by A2; A4: len A=n & width A=k & len B=n & width B=m & len X=k & width X=m by A1,MATRIX_1:24; then A*X=B by A1,MATRIX_5:38; hence thesis by A3,A4; end; theorem n>0 & Solutions_of(0.(K,n,0),0.(K,n,m)) is non empty implies m = 0 proof assume A1: n>0 & Solutions_of(0.(K,n,0),0.(K,n,m)) is non empty; then consider x such that A2: x in Solutions_of(0.(K,n,0),0.(K,n,m)) by XBOOLE_0:def 1; consider X such that A3: X=x & len X = width 0.(K,n,0) and A4: width X = width 0.(K,n,m) and 0.(K,n,0) * X = 0.(K,n,m) by A2; width 0.(K,n,0)=0 by A1,MATRIX_1:24; hence 0 = width 0.(K,n,m) by A4,A3,MATRIX_1:def 4 .= m by A1,MATRIX_1:24; end; theorem Th56: Solutions_of(0.(K,n,0),0.(K,n,0)) = {{}} proof per cases; suppose n=0; hence thesis by Th51; end; suppose A1: n>0; reconsider E={} as Matrix of 0,0,K by MATRIX_1:13; set A=0.(K,n,0); set B=0.(K,n,0); A2: len A=n & width A=0 & len B=n & width B=0 & len E=0 & width E=0 & Indices B=[:Seg n,Seg 0:] by A1,MATRIX_1:24,25; then A3: len (A*E)=n & width (A*E)=0 by MATRIX_3:def 4; for i,j st [i,j] in Indices B holds B*(i,j)=(A*E)*(i,j) by A2,FINSEQ_1:4,ZFMISC_1:113; then A*E=B by A2,A3,MATRIX_1:21; then A4: E in Solutions_of(A,B) by A2; Solutions_of(A,B) c= {{}} proof let x; assume x in Solutions_of(A,B); then reconsider X=x as Matrix of 0,0,K by A1,Th53; len X=0 by MATRIX_1:def 3; then X={} by FINSEQ_1:25; hence thesis by TARSKI:def 1; end; hence thesis by A4,ZFMISC_1:39; end; end; begin ::Gaussian eliminations scheme GAUSS1{ K() -> Field, n,m,m'() -> Nat, A() -> Matrix of n(),m(),K(), B() -> Matrix of n(),m'(),K(), F(Matrix of n(),m'(),K(),Nat,Nat,Element of K())-> Matrix of n(),m'(),K(), P[set,set]}: ex A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K(), N be without_zero finite Subset of NAT st N c= Seg m() & the_rank_of A() = the_rank_of A' & the_rank_of A() = card N & P[A',B'] & Segm(A',Seg card N,N) is diagonal & ( for i st i in Seg card N holds A'*(i,Sgm N/.i) <> 0.K() ) & ( for i st i in dom A' & i > card N holds Line(A',i)= m()|->0.K() ) & ( for i,j st i in Seg card N & j in Seg width A' & j < Sgm N.i holds A'*(i,j) = 0.K()) provided A1: P[A(),B()] and A2: for A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() st P[A',B'] for i,j st i <> j & j in dom A' for a be Element of K() holds P[RLine(A',i,Line(A',i) + a*Line(A',j)),F(B',i,j,a)] proof set r = the_rank_of A(); defpred PP[FinSequence of NAT,Nat,Nat, Matrix of n(),m(),K()] means $4*($2,$1/.$2) <> 0.K() & ( $3 in dom $1 & $2 < $3 implies $1/.$2 < $1/.$3 )& ( $3 in dom $1 \ {$2} implies $4*($3,$1/.$2) = 0.K() )& ( $3 in Seg width $4 & $3 < $1/.$2 implies $4*($2,$3) = 0.K()); ex A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() st P[A',B'] & r = the_rank_of A' & (for i st i in dom A' & i > r holds Line(A',i)=m()|->0.K())& ex f be FinSequence of NAT st len f = the_rank_of A' & f is one-to-one & rng f c= Seg width A' & for i,j st i in dom f holds PP[f,i,j,A'] proof per cases; suppose A3: n()=0; take A'=A(),B'=B(); dom A'=Seg len A' & len A'=0& Seg 0={} by A3,FINSEQ_1:4,def 3,MATRIX_1:def 3; hence P[A',B'] & r = the_rank_of A' & (for i st i in dom A' & i > r holds Line(A',i)=m()|->0.K()) by A1; take f=<*>NAT; len A'=0 by A3,MATRIX_1:23; then r<=0 by MATRIX13:74; then r=0 & len f=0 by FINSEQ_1:32; hence thesis by XBOOLE_1:2; end; suppose A4: n()>0; defpred Q[Nat] means $1 <= m() implies ex A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() st P[A',B'] & r = the_rank_of A' & ex f be FinSequence of NAT st (for i,j st [i,j] in Indices A'&i>len f&j<=$1 holds A'*(i,j)=0.K())& f is one-to-one & len f <= $1 & len f<=n() & rng f c= Seg $1 & for i,j st i in dom f holds PP[f,i,j,A']; A5: Q[0] proof assume 0<=m(); take A'=A(),B'=B(); thus P[A',B'] & r = the_rank_of A' by A1; take f=<*>NAT; now let i,j such that A6: [i,j] in Indices A' & i > len f & j<=0; j in Seg width A' by A6,ZFMISC_1:106; hence A'*(i,j)=0.K() by A6,FINSEQ_1:3; end; hence thesis by XBOOLE_1:2,FINSEQ_1:32; end; A7: for n st Q[n] holds Q[n+1] proof let n such that A8: Q[n]; set n1=n+1; assume A9: n1<=m(); then consider A' be Matrix of n(),m(),K(),B' be Matrix of n(),m'(),K() such that A10: P[A',B'] & r = the_rank_of A' and A11: ex f be FinSequence of NAT st (for i,j st [i,j] in Indices A'&i>len f&j<=n holds A'*(i,j)=0.K())& f is one-to-one & len f <= n &len f<=n()&rng f c= Seg n & for i,j st i in dom f holds PP[f,i,j,A'] by A8,NAT_1:13; consider f be FinSequence of NAT such that A12: for i,j st [i,j] in Indices A'&i>len f&j<=n holds A'*(i,j)=0.K()and A13: f is one-to-one & len f <= n & len f<=n()&rng f c=Seg n and A14: for i,j st i in dom f holds PP[f,i,j,A'] by A11; per cases; suppose A15: for i,j st [i,j] in Indices A' & i>len f & j=n1 holds A'*(i,j)=0.K(); A16: now let i,j such that A17: [i,j] in Indices A' &i>len f&j<=n1; j<=n or j=n1 by A17,NAT_1:8; hence A'*(i,j)=0.K() by A12,A15,A17; end; n<=n1 by NAT_1:13; then Seg n c= Seg n1 & Seg n1 c= Seg m() by A9,FINSEQ_1:7; then len f <=n1 & len f<=n() & rng f c= Seg n1 by A13,XBOOLE_1:1,NAT_1:12; hence thesis by A10,A13,A14,A16; end; suppose ex i,j st [i,j] in Indices A' &i>len f&j=n1&A'*(i,j)<>0.K(); then consider i0,j0 be Nat such that A18: [i0,j0] in Indices A' & i0>len f &j0=n1 & A'*(i0,j0)<>0.K(); n<=m() by A9,NAT_1:13; then A19: Indices A'=[:Seg n(),Seg m():] & width A()=m() & Seg n c= Seg m() by A4,MATRIX_1:24,FINSEQ_1:7; then A20: i0 in Seg n() & Seg n c= Seg m() by A18,ZFMISC_1:106; then A21: i0<=n() & len f+1<=i0 by A18,FINSEQ_1:3,NAT_1:13; then 0+1<=len f+1 & 0+1<=n1&len f+1<=n() by XREAL_1:9,XXREAL_0:2; then A22: len f+1 in Seg n() & j0 in Seg m() & n1 in Seg m() & Seg len f c=Seg n() & dom f = Seg len f by A13,A18,A19,ZFMISC_1:106,FINSEQ_1:def 3,7; ex A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() st P[A',B'] & r = the_rank_of A' & A'*(len f+1,n1) <> 0.K() & (for i,j st [i,j] in Indices A' & i>len f &j<=n holds A'*(i,j)=0.K())& for i,j st i in dom f holds PP[f,i,j,A'] proof per cases; suppose A'*(len f+1,n1) <> 0.K(); hence thesis by A10,A12,A14; end; suppose A23: A'*(len f+1,n1) = 0.K(); then A24: i0 <> len f+1 & i0 in dom A' & dom A'=Seg len A' by A18,ZFMISC_1:106,FINSEQ_1:def 3; set LAf=Line(A',len f+1); set LA=Line(A',i0); set LB=Line(B',i0); set RA=RLine(A',len f+1,LAf + 1_K()*LA); set LBf=Line(B',len f+1); set RB=F(B',len f+1,i0,1_K()); take RA,RB; thus P[RA,RB] & r = the_rank_of RA by A2,A10,A24,MATRIX13:92; A25: width A'=m() & len A'=n() & 1_K()*LA=LA & width A()=m()& len (LAf+LA)=width A' by A4,MATRIX_1:24,FVSUM_1:70,FINSEQ_2:109; [len f+1,j0] in Indices A' by A19,A22,ZFMISC_1:106; then RA*(len f+1,n1)=(LAf+LA).n1 & LAf.n1=0.K() & LA.n1=A'*(i0,n1) by A18,A23,A25,A22,MATRIX11:def 3,MATRIX_1:def 8; then RA*(len f+1,n1) = 0.K()+A'*(i0,n1) by A25,A22,FVSUM_1: 22 .= A'*(i0,n1) by RLVECT_1:def 7; hence RA*(len f+1,n1)<>0.K() by A18; A26: Indices RA=Indices A' by MATRIX_1:27; now let i,j such that A27: [i,j] in Indices RA & i>len f&j<=n; A28: j in Seg m()&i>=len f+1 by A25,A26,A27,ZFMISC_1:106,NAT_1:13; now per cases by A28,REAL_1:def 5; suppose i>len f+1; hence RA*(i,j) = A'*(i,j) by A25,A26,A27,MATRIX11:def 3 .= 0.K() by A27,A26,A12; end; suppose A29: i=len f+1; then A30: RA*(i,j)=(LAf+LA).j & LAf.j=A'*( len f+1,j) & LA.j=A'*(i0,j)&[i0,j] in Indices A' by A19,A20,A25,A26,A27,A28,MATRIX11:def 3, MATRIX_1:def 8,ZFMISC_1:106; hence RA*(i,j) = A'*(len f+1,j)+A'*(i0,j) by A25,A28,FVSUM_1:22 .= 0.K()+A'*(i0,j) by A12,A26,A27,A29 .= 0.K()+0.K() by A12,A18,A27,A30 .= 0.K() by RLVECT_1:def 7; end; end; hence RA*(i,j)=0.K(); end; hence for i,j st [i,j] in Indices RA & i > len f&j<=n holds RA*(i,j) = 0.K(); let i,j such that A31: i in dom f; f/.i=f.i&f.i in rng f by A31,PARTFUN1:def 8,FUNCT_1:def 5; then A32: i in Seg n() & f/.i in Seg n & i <= len f by A22,A13,A31,FINSEQ_1:3; then A33: [i,f/.i] in Indices A' & i0.K()&(j in dom f & i 0.K() and A39: for i,j st [i,j] in Indices A0& i>len f& j<=n holds A0*(i,j)=0.K() and A40: for i,j st i in dom f holds PP[f,i,j,A0]; defpred QQ[Nat] means $1<=n() implies ex A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() st P[A',B'] & r = the_rank_of A' & A'*(len f+1,n1) <> 0.K() & (for i,j st [i,j] in Indices A' & i>len f&j<=n holds A'*(i,j)=0.K())& (for i,j st i in dom f holds PP[f,i,j,A']) & for j st j in dom A'\{len f+1} & j<=$1 holds A'*(j,n1)=0.K(); A41: QQ[0] proof assume 0<=n(); take A0,B0; now let j such that A42: j in dom A0 \ {len f+1} & j<=0; dom A0=Seg len A0 & j in dom A0 by A42,FINSEQ_1:def 3,XBOOLE_0:def 4; hence A0*(j,n1) = 0.K() by A42,FINSEQ_1:3; end; hence thesis by A37,A38,A39,A40; end; A43: for k st QQ[k] holds QQ[k+1] proof let k such that A44: QQ[k]; set k1=k+1; assume k1<=n(); then consider AA be Matrix of n(),m(),K(), BB be Matrix of n(),m'( ),K() such that A45: P[AA,BB] & r = the_rank_of AA and A46: AA*(len f+1,n1) <> 0.K() and A47: for i,j st [i,j] in Indices AA & i>len f&j<=n holds AA*(i,j)=0.K()and A48: for i,j st i in dom f holds PP[f,i,j,AA] and A49: for j st j in dom AA\{len f+1} & j<=k holds AA*(j,n1)=0.K() by A44,NAT_1:13; now per cases; suppose A50: k1=len f+1; take RA=AA,RB=BB; now let j such that A51: j in dom RA \ {len f+1} & j<=k1; j <> len f+1 by A51,ZFMISC_1:64; then jlen f+1; set a=AA*(len f+1,n1); set LAf=Line(AA,len f+1); set LA=Line(AA,k1); set LB=Line(BB,k1); set LBf=Line(BB,len f+1); set RA=RLine(AA,k1,LA + (-(AA*(k1,n1))*a")*LAf); set RB=F(BB,k1,len f+1,-(AA*(k1,n1))*a"); A53: Indices A'=Indices AA & Indices A'=Indices RA&len AA=n() by MATRIX_1:27,def 3; A54: len f+1 in Seg len AA &dom AA=Seg len AA&width AA=m() & width RA=m() by A4,A22,FINSEQ_1:def 3,MATRIX_1:24; then A55: len (LA+(-(AA*(k1,n1))*a")*LAf)=m()by FINSEQ_2:109; take RA,RB; A56: P[RA,RB] & r=the_rank_of RA by A2,A45,A52,A54,MATRIX13:92; [len f+1,n1] in Indices AA by A53,A19,A22,ZFMISC_1:106; then A57: RA*(len f+1,n1)<>0.K() by A46,A52,A54,A55, MATRIX11:def 3; A58: now let i,j such that A59: [i,j] in Indices RA&i>len f&j<=n; now per cases; suppose A60: i = k1; A61: j in Seg m() by A53,A19,A59,ZFMISC_1:106; then A62: LA.j = AA*(k1,j) by A54, MATRIX_1:def 8 .= 0.K() by A60,A59,A53,A47; len f+1>len f & [len f+1,j] in Indices A' by A19,A22,A61,NAT_1:13,ZFMISC_1:106; then AA*(len f+1,j)=0.K() by A59,A53,A47; then LAf.j=0.K() by A54,A61,MATRIX_1:def 8; then ((-(AA*(k1,n1))*a")*LAf).j = (-(AA*(k1,n1))*a")*0. K() by A54,A61,FVSUM_1:63 .= 0.K() by VECTSP_1:36; then 0.K()+0.K() = (LA + (-(AA*(k1,n1))*a")*LAf).j by A54,A61,A62,FVSUM_1:22 .= RA*(i,j) by A53,A54,A59,A55,A60, MATRIX11:def 3; hence RA*(i,j) = 0.K() by RLVECT_1:def 7; end; suppose i<>k1; hence RA*(i,j) = AA*(i,j) by A53,A54,A59,A55, MATRIX11:def 3 .= 0.K() by A47,A53,A59; end; end; hence RA*(i,j)=0.K(); end; A63: now let i,j such that A64: i in dom f; set fi=f/.i; A65: fi=f.i & f.i in rng f by A64,PARTFUN1:def 8,FUNCT_1:def 5; then A66: fi in Seg n by A13; then A67: [i,fi] in Indices AA & [len f+1,fi] in Indices AA by A19,A22,A53,ZFMISC_1:106,A64; A68: LA.fi=AA*(k1,fi) & LAf.fi=AA*(len f+1,fi) & len f+1>len f & fi<=n by A54,A66,A19,MATRIX_1:def 8, NAT_1:13,FINSEQ_1:3; then LAf.fi=0.K() by A67,A47; then ((-(AA*(k1,n1))*a")*LAf).fi =(-(AA*(k1,n1))*a")*0.K() by A54,A66,A19,FVSUM_1:63 .= 0.K() by VECTSP_1:44; then A69: (LA+(-(AA*(k1,n1))*a")*LAf).fi = AA*( k1,fi)+0.K() by A54,A66,A19,A68,FVSUM_1:22 .= AA*(k1,fi) by RLVECT_1:def 7; now per cases; suppose i<>k1; then RA*(i,fi)=AA*(i,fi)by A55,A54,A67,MATRIX11:def 3; hence RA*(i,fi)<>0.K() by A64,A48; end; suppose i=k1; then RA*(i,fi)=AA*(i,fi) by A55,A54,A67,A69,MATRIX11:def 3; hence RA*(i,f/.i)<>0.K() by A48,A64; end; end; hence RA*(i,fi) <> 0.K()& (j in dom f & i < j implies fi < f/.j) by A14,A64; thus j in dom f \ {i} implies RA*(j,fi) = 0.K() proof assume A70: j in dom f \ {i}; then j in Seg len f by A22,XBOOLE_0:def 4; then A71: [j,fi] in Indices AA by A22,A53, A66,A19,ZFMISC_1:106; per cases; suppose j<>k1; hence RA*(j,fi) = AA*(j,fi) by A55,A54,A71, MATRIX11:def 3 .= 0.K() by A64,A70,A48; end; suppose A72: j = k1; hence RA*(j,fi) = (LA+(-(AA*(k1,n1))*a")*LAf).fi by A55,A54,A71,MATRIX11:def 3 .= 0.K() by A64,A70,A48,A69,A72; end; end; thus j in Seg width RA & j < f/.i implies RA*(i,j) = 0.K() proof assume A73: j in Seg width RA & j < f/.i; then A74: [i,j] in Indices AA & [len f+1,j] in Indices AA by A22,A53,A54,A64,ZFMISC_1:106; per cases; suppose i<>k1; hence RA*(i,j) = AA*(i,j) by A55,A74,A54,MATRIX11:def 3 .= 0.K() by A73,A54,A64,A48; end; suppose A75: i = k1; then A76: LA.j = AA*(i,j)by A73,A54, MATRIX_1:def 8 .= 0.K() by A73,A54,A64,A48; fi <= n by FINSEQ_1:3,A65,A13; then j <= n & len f+1 > len f by A73,XXREAL_0:2,NAT_1:13; then 0.K() = AA*(len f+1,j) by A47,A74 .= LAf.j by A73,A54,MATRIX_1:def 8; then ((-(AA*(k1,n1))*a")*LAf).j = (-(AA*(k1,n1))*a")*0.K() by A73,A54,FVSUM_1:63 .= 0.K() by VECTSP_1:36; then (LA + (-(AA*(k1,n1))*a")*LAf).j = 0.K()+0.K() by A73,A54,A76,FVSUM_1:22 .= 0.K() by RLVECT_1:def 7; hence RA*(i,j) = 0.K() by A55,A74,A54,MATRIX11:def 3,A75; end; end; end; now let j such that A77: j in dom RA \ {len f+1} & j<=k1; A78: dom RA=Seg len RA & len RA=n() & dom AA=Seg len AA by FINSEQ_1:def 3,MATRIX_1:def 3; j in dom RA by A77,XBOOLE_0:def 4; then A79: [j,n1] in Indices AA by A22,A53,A54, ZFMISC_1:106; now per cases by A77,NAT_1:8; suppose A80: j<=k; then j 0.K()and A84: for i,j st [i,j] in Indices Aa & i>len f&j<=n holds Aa*(i,j)=0.K() and A85: for i,j st i in dom f holds PP[f,i,j,Aa] and A86: for j st j in dom Aa\{len f+1}&j<=n() holds Aa*(j,n1)=0.K(); take Aa,Bb; thus P[Aa,Bb] & r = the_rank_of Aa by A83; take f'=f^<*n1*>; A87: len f'=len f+1 & len f+1>len f & len Aa=n() &dom Aa=Seg len Aa & width Aa=m() by FINSEQ_2:19,NAT_1:13,FINSEQ_1:def 3, A4,MATRIX_1:24; A88: now let i,j such that A89: [i,j] in Indices Aa & i>len f' & j<=n1; per cases by NAT_1:8,A89; suppose A90: j<=n; i>len f by A89,A87,NAT_1:13; hence Aa*(i,j)=0.K() by A84,A89,A90; end; suppose A91: j=n1; i in dom Aa by A89,ZFMISC_1:106; then i in dom Aa\{len f+1} & i<=n() by A87,A89,ZFMISC_1:64,FINSEQ_1:3; hence Aa*(i,j)=0.K() by A91,A86; end; end; Seg n misses {n1} by FINSEQ_3:15; then A92: rng f misses {n1} & <*n1*> is one-to-one & rng <*n1*>= {n1} & rng f \/{n1} c= Seg n\/{n1} & Seg n\/{n1}=Seg n1 by A13,XBOOLE_1:9,63,FINSEQ_3:102,FINSEQ_1:11,55; then A93: len f'<=n() & rng f' c= Seg n1 by A21,A87,FINSEQ_1:44, XXREAL_0:2; now let i,j such that A94: i in dom f'; A95: dom f' = Seg (len f+1) by A87,FINSEQ_1:def 3 .= dom f\/{len f+1} by A22,FINSEQ_1:11; A96: now let k such that A97: k in dom f; A98: k in dom f' by A95,A97,XBOOLE_0:def 2; thus f/.k = f.k by A97,PARTFUN1:def 8 .= f'.k by A97,FINSEQ_1:def 7 .= f'/.k by A98,PARTFUN1:def 8; end; now per cases by A94,A95,XBOOLE_0:def 2; suppose A99: i in dom f; then f/.i=f'/.i by A96; hence Aa*(i,f'/.i)<>0.K() by A99,A85; end; suppose A100: i in {len f+1}; then i=len f+1 by TARSKI:def 1; then f'.i=n1 & f'/.i=f'.i by A94,FINSEQ_1:59,PARTFUN1:def 8; hence Aa*(i,f'/.i)<>0.K() by A100,A83,TARSKI:def 1; end; end; hence Aa*(i,f'/.i) <> 0.K(); thus j in dom f' & i < j implies f'/.i < f'/.j proof assume A101: j in dom f' & i < j; per cases by A94,A95,A101,XBOOLE_0:def 2; suppose j in {len f+1} & i in {len f+1}; then i=len f+1 & j=len f+1 by TARSKI:def 1; hence thesis by A101; end; suppose A102: j in {len f+1} & i in dom f; then f/.i=f.i & f.i in rng f by PARTFUN1:def 8,FUNCT_1:def 5; then f/.i in Seg n & len f+1=j by A13,A102,TARSKI:def 1; then f/.i <= n & n < n1 & f'.j=n1 & f'.j=f'/.j by A101,NAT_1:13,FINSEQ_1:3,59,PARTFUN1:def 8; then f/.i < f'/.j & f/.i=f'/.i by A96,A102,XXREAL_0:2; hence thesis; end; suppose j in dom f & i in {len f+1}; then j<=len f & i=len f+1 by A22,FINSEQ_1:3,TARSKI:def 1; hence thesis by A101,NAT_1:13; end; suppose j in dom f & i in dom f; then f/.i=f'/.i & f/.j=f'/.j & f/.ii by A104,ZFMISC_1:64; then A106: j in dom Aa & j<>i&j<=n()&len f+1 in {len f+1} by A103,A87,FINSEQ_1:3,TARSKI:def 1; then j in dom Aa\{i} & len f+1 in dom f' by A95,ZFMISC_1:64,XBOOLE_0:def 2; then Aa*(j,n1)=0.K() & f'.(len f+1)=f'/.i by A86,A105,A106,PARTFUN1:def 8; hence thesis by FINSEQ_1:59; end; suppose A107: i<>len f+1; A108: i in dom f or i in {len f+1} by A94,A95,XBOOLE_0:def 2; then f/.i=f'/.i & f.i=f/.i & f.i in rng f by A96,PARTFUN1:def 8,FUNCT_1:def 5,A107,TARSKI:def 1; then A109: 1<=f'/.i & f'/.i<=n & n<=m() by A9, FINSEQ_1:3,A13,NAT_1:13; then f'/.i <=m() by XXREAL_0:2; then A110: f'/.i in Seg width Aa by A87,A109; j in dom f' by A104,XBOOLE_0:def 4; then A111: [j,f'/.i] in Indices Aa by A103,A110, ZFMISC_1:106; per cases; suppose j=len f+1; then j > len f by NAT_1:13; hence thesis by A84,A109,A111; end; suppose A112: j<>len f+1; j in dom f' by A104,XBOOLE_0:def 4; then j in dom f or j in {len f+1} by A95,XBOOLE_0:def 2; then j in dom f & j<>i by A104,A112,TARSKI:def 1,ZFMISC_1:64; then j in dom f\{i} by ZFMISC_1:64; then Aa*(j,f/.i)=0.K() & f/.i=f'/.i by A85,A96,A108,A107,TARSKI:def 1; hence thesis; end; end; end; thus j in Seg width Aa & j < f'/.i implies Aa*(i,j) = 0.K() proof assume A113: j in Seg width Aa & j < f'/.i; per cases; suppose A114: i in dom f; then f'/.i=f/.i by A96; hence Aa*(i,j) = 0.K() by A113,A114,A85; end; suppose A115: not i in dom f; i in dom f or i in {len f+1} by A94,A95,XBOOLE_0:def 2; then A116: i=len f+1 by A115,TARSKI:def 1; then f'.i=f'/.i & f'.i = n1 & i in dom Aa by A103,A94,FINSEQ_1:59,PARTFUN1:def 8; then j<=n & [i,j] in Indices Aa & i>len f by A113,A116,NAT_1:13,ZFMISC_1:106; hence thesis by A84; end; end; end; hence (for i,j st [i,j] in Indices Aa&i>len f'&j<=n1 holds Aa*(i,j)=0.K())& f' is one-to-one & len f' <= n1 & len f'<=n() & rng f' c= Seg n1 & for i,j st i in dom f' holds PP[f',i,j,Aa] by A88,A92,A21,A13,A87,FINSEQ_3:98,XREAL_1:8, FINSEQ_1:44,XXREAL_0:2; end; end; for n holds Q[n] from NAT_1:sch 2(A5,A7); then consider A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() such that A117: P[A',B'] & r = the_rank_of A' and A118: ex f be FinSequence of NAT st (for i,j st [i,j] in Indices A'&i>len f&j<=m() holds A'*(i,j)=0.K())& f is one-to-one & len f <= m() & len f<=n() & rng f c= Seg m() & for i,j st i in dom f holds PP[f,i,j,A']; take A',B';thus P[A',B'] & r=the_rank_of A' by A117; consider f be FinSequence of NAT such that A119: for i,j st [i,j] in Indices A'&i>len f&j<=m() holds A'*(i,j)=0.K() and A120: f is one-to-one & len f <= m() & len f<=n() & rng f c= Seg m() and A121: for i,j st i in dom f holds PP[f,i,j,A'] by A118; set L=len f; idseq L is FinSequence of NAT & len (idseq L)=L by FINSEQ_2:52,55; then reconsider idL=idseq L,F'=f as Element of L-tuples_on NAT by FINSEQ_2:110; set S=Segm(A',idL,F'); A122: rng idL=Seg L & Seg L c= Seg n() & len A'=n() & dom A'=Seg len A' & width A'=m() & dom f=Seg L by A4,A120,RELAT_1:71,FINSEQ_1:7,def 3, MATRIX_1:24; then A123: [:rng idL,rng F':] c= Indices A' & Indices S=[:Seg L,Seg L:] by A120,ZFMISC_1:119,MATRIX_1:25; now let i,j such that A124: [i,j] in Indices S; reconsider i'=i,j'=j as Element of NAT by ORDINAL1:def 13; assume A125: i>j; A126: i in Seg L & j in Seg L by A123,A124,ZFMISC_1:106; then A127: L<>0 & i in dom f \{j} by A122,A125,FINSEQ_1:4,ZFMISC_1:64; thus S*(i,j) = A'*(idL.i',f.j') by A124,MATRIX13:def 1 .= A'*(i,f.j) by A126,FINSEQ_1:4,FINSEQ_2:57 .= A'*(i,f/.j) by A122,A126,PARTFUN1:def 8 .= 0.K() by A121,A122,A126,A127; end; then A128: S is Upper_Triangular_Matrix of L,K() by MATRIX_2:def 3; set D=diagonal_of_Matrix S; set mm=the multF of K(); for k be Element of NAT st k in dom D holds D.k <> 0.K() proof let k be Element of NAT such that A129: k in dom D; len D=L by MATRIX_3:def 10; then A130: k in Seg L by A129,FINSEQ_1:def 3; then [k,k] in Indices S & L<>0 by A123,ZFMISC_1:106,FINSEQ_1:4; then S*(k,k) = A'*(idL.k,f.k) by MATRIX13:def 1 .= A'*(k,f.k) by A130,FINSEQ_2:57,FINSEQ_1:4 .= A'*(k,f/.k) by A122,A130,PARTFUN1:def 8; then S*(k,k)<>0.K() by A121,A122,A130; hence thesis by A130,MATRIX_3:def 10; end; then Product D<>0.K() by FVSUM_1:107; then Det S<>0.K() by A128,MATRIX13:7; then A131: the_rank_of A' >= L by A123,MATRIX13:76; A132: now let i such that A133: i in dom A'\(Seg L); set LA=Line(A',i); set w0=width A' |-> 0.K(); A134: len LA=width A' & len w0=width A' by FINSEQ_2:109; now let j such that A135: 1<=j & j<=width A'; j in NAT by ORDINAL1:def 13; then A136: j in Seg width A' & i in dom A' & not i in Seg L by A133,A135,XBOOLE_0:def 4; then A137: [i,j] in Indices A' & i>=1 & (i > L or i<1) & width A' <>0 by A122,ZFMISC_1:106,FINSEQ_1:3,4; thus LA.j = A'*(i,j) by A136,MATRIX_1:def 8 .= 0.K() by A122,A135,A137,A119 .= w0.j by A136,FINSEQ_2:71,FINSEQ_1:4; end; hence Line(A',i) = width A' |-> 0.K() by A134,FINSEQ_1:18; end; then the_rank_of A'=the_rank_of Segm(A',Seg L,Seg width A') & len Segm(A',Seg L,Seg width A')=card Seg L by A122,Th11,MATRIX_1:def 3; then the_rank_of A' <= card Seg L by MATRIX13:74; then A138: the_rank_of A' <= L by FINSEQ_1:78; then A139: r=L by A131,A117,XXREAL_0:1; thus for i st i in dom A' & i > r holds Line(A',i)=m()|->0.K() proof let i such that A140: i in dom A' & i > r; not i in Seg L by A139,A140,FINSEQ_1:3; then i in dom A'\(Seg L) by A140,XBOOLE_0:def 4; hence thesis by A122,A132; end; take f; thus thesis by A120,A121,A4,MATRIX_1:24,A138,A131,XXREAL_0:1; end; end; then consider A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() such that A141: P[A',B'] & r = the_rank_of A' and A142: for i st i in dom A' & i > r holds Line(A',i)=m()|->0.K() and A143: ex f be FinSequence of NAT st len f = the_rank_of A' & f is one-to-one & rng f c= Seg width A' & for i,j st i in dom f holds PP[f,i,j,A']; consider f be FinSequence of NAT such that A144: len f = the_rank_of A' and A145: f is one-to-one & rng f c= Seg width A' and A146: for i,j st i in dom f holds PP[f,i,j,A'] by A143; not 0 in rng f by A145,FINSEQ_1:3; then reconsider rngf=rng f as without_zero finite Subset of NAT by A145,PSCOMP_1:def 1,XBOOLE_1:1; take A',B',rngf; (n()=0 or n()>0)& len A' = n() by MATRIX_1:def 3; then width A' = 0 or width A' = m() by MATRIX_1:24,def 4; then Seg width A' c= Seg m() by FINSEQ_1:7; hence rngf c= Seg m() & r = the_rank_of A' by A141,A145,XBOOLE_1:1; dom f,rngf are_equipotent by A145,WELLORD2:def 4; hence A147: card rngf = card dom f by CARD_1:21 .= card Seg r by A141,A144,FINSEQ_1:def 3 .= r by FINSEQ_1:78; A148: now let i,j; assume A149: i in dom f & j in dom f & i < j; then f.i=f/.i & f.j=f/.j by PARTFUN1:def 8; hence f.i < f.j by A146,A149; end; thus P[A',B'] by A141; set S=Segm(A',Seg card rngf,rngf); A150: card Seg card rngf=card rngf & Sgm rngf = f by A145,A148,Th6,FINSEQ_1:78; then A151: Indices S = [:Seg r,Seg r:] & dom f=Seg r by A141,A144,A147,FINSEQ_1:def 3,MATRIX_1:25; now let i,j be Element of NAT such that A152: i in Seg r & j in Seg r & i <> j; A153: [i,j] in Indices S & dom f=Seg r by A151,A152,ZFMISC_1:106; A154: idseq r.i=i & i<=r by A152,FINSEQ_2:57,FINSEQ_1:3,4; A155: S*(i,j) = A'*(Sgm (Seg r).i,f.j) by A147,A150,A153,MATRIX13:def 1 .= A'*(i,f.j) by A154,FINSEQ_3:54 .= A'*(i,f/.j) by A152,A151,PARTFUN1:def 8; i in dom f\{j} by A152,A151,ZFMISC_1:64; hence S*(i,j) = 0.K() by A146,A151,A152,A155; end; hence S is diagonal by A150,MATRIX_7:def 2,A147; thus for i st i in Seg card rngf holds A'*(i,Sgm rngf/.i) <> 0.K() by A146,A147,A150,A151; thus for i st i in dom A' & i > card rngf holds Line(A',i) = m()|->0.K() by A142,A147; let i,j such that A156: i in Seg card rngf & j in Seg width A' & j < Sgm rngf.i; j Field, n,m,m'() -> Nat, A() -> Matrix of n(),m(),K(), B() -> Matrix of n(),m'(),K(), F(Matrix of n(),m'(),K(),Nat,Nat,Element of K()) -> Matrix of n(),m'(),K(), P[set,set]}: ex A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K(), N be without_zero finite Subset of NAT st N c= Seg m() & the_rank_of A() = the_rank_of A' & the_rank_of A() = card N & P[A',B'] & Segm(A',Seg card N,N) = 1.(K(),card N) & ( for i st i in dom A' & i > card N holds Line(A',i) = m()|->0.K() ) & ( for i,j st i in Seg card N & j in Seg width A' & j < Sgm N.i holds A'*(i,j) = 0.K()) provided A1: P[A(),B()] and A2: for A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() st P[A',B'] for a be Element of K() for i,j st j in dom A' & (i = j implies a <> -1_K() ) holds P[RLine(A',i,Line(A',i) + a*Line(A',j)),F(B',i,j,a)] proof A3: for A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() st P[A',B'] for i,j st i <> j & j in dom A' for a be Element of K() holds P[RLine(A',i,Line(A',i) + a*Line(A',j)),F(B',i,j,a)] by A2; set r=the_rank_of A(); consider A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K(), N be without_zero finite Subset of NAT such that A4: N c= Seg m() and A5: r = the_rank_of A' & r = card N and A6: P[A',B'] & Segm(A',Seg card N,N) is diagonal and A7: for i st i in Seg card N holds A'*(i,Sgm N/.i) <> 0.K() and A8: for i st i in dom A' & i > card N holds Line(A',i) = m()|->0.K() and A9: for i,j st i in Seg card N & j in Seg width A' & j < Sgm N.i holds A'*(i,j) = 0.K() from GAUSS1(A1,A3); defpred Q[Nat] means $1 <= card N implies ex A' be Matrix of n(),m(),K(), B' be Matrix of n(),m'(),K() st r = the_rank_of A' & ( for i st i in Seg card N & i<=$1 holds A'*(i,Sgm N/.i) = 1_K() )& P[A',B'] & Segm(A',Seg card N,N) is diagonal & ( for i st i in Seg card N holds A'*(i,Sgm N/.i) <> 0.K() )& ( for i st i in dom A' & i > card N holds Line(A',i) = m()|->0.K())& ( for i,j st i in Seg card N & j in Seg width A' & j < Sgm N.i holds A'*(i,j) = 0.K()); for i st i in Seg card N & i<=0 holds A'*(i,Sgm N/.i) = 1_K() by FINSEQ_1:3; then A10: Q[0] by A5,A6,A7,A8,A9; A11: for n st Q[n] holds Q[n+1] proof let n such that A12: Q[n]; set n1=n+1; set f=Sgm N; assume A13: n1<=card N; then consider A1 be Matrix of n(),m(),K(),A25 be Matrix of n(),m'(),K() such that A14: r = the_rank_of A1 and A15: for i st i in Seg card N & i<=n holds A1*(i,Sgm N/.i) = 1_K() and A16: P[A1,A25] & Segm(A1,Seg card N,N) is diagonal and A17: for i st i in Seg card N holds A1*(i,Sgm N/.i) <> 0.K() and A18: for i st i in dom A1 & i > card N holds Line(A1,i) = m()|->0.K()and A19: for i,j st i in Seg card N & j in Seg width A1 & j < Sgm N.i holds A1*(i,j) = 0.K() by A12,NAT_1:13; set L=Line(A1,n1); set LL=L+((A1*(n1,f/.n1))"-1_K())*L; set R=RLine(A1,n1,LL); 1<=1+n by NAT_1:11; then A20: n1 in Seg card N & dom Sgm N=Seg card N & rng Sgm N=N & len LL=width A1 by A13,A4,FINSEQ_1:def 13,FINSEQ_2:109,FINSEQ_3:45; r<=len A' & len A'=n() by A5,MATRIX13:74,MATRIX_1:def 3; then A21: Seg r c= Seg n() & dom A1=Seg len A1 & len A1=n() by FINSEQ_1:def 3,7,MATRIX_1:def 3; A22: (A1*(n1,Sgm N/.n1))"-1_K()<>-1.K() proof assume A23: (A1*(n1,Sgm N/.n1))"-1_K()=-1.K(); A24: 0.K() = 1_K()+ -1_K() by VECTSP_1:66 .= (1_K()+(-1_K()))+A1*(n1,Sgm N/.n1)" by A23,RLVECT_1:def 6 .= 0.K()+A1*(n1,Sgm N/.n1)" by VECTSP_1:66 .= A1*(n1,Sgm N/.n1)" by RLVECT_1:def 7; A1*(n1,Sgm N/.n1)<>0.K() by A17,A20; hence thesis by A24,VECTSP_1:74; end; A25: LL = 1_K()*L+((A1*(n1,f/.n1))"-1_K())*L by FVSUM_1:70 .= (1_K() +(-1_K()+(A1*(n1,f/.n1))"))*L by FVSUM_1:68 .= ((1_K() +-1_K())+(A1*(n1,f/.n1))")*L by RLVECT_1:def 6 .= (0.K()+A1*(n1,f/.n1)")*L by VECTSP_1:66 .= (A1*(n1,f/.n1))"*L by RLVECT_1:def 7; take R,FB=F(A25,n1,n1,(A1*(n1,f/.n1))"-1_K()); n()<>0 by FINSEQ_1:4,A5,A20,A21; then n()>0; then A26: width A'=m() & width A1=m() & width R=m() by MATRIX_1:24; thus the_rank_of R =r by A14,A20,A21,A22,MATRIX13:92,A5; thus A27: for i st i in Seg card N & i<=n1 holds R*(i,Sgm N/.i) = 1_K() proof let i; assume A28: i in Seg card N & i<=n1; then A29: f.i=f/.i & f.i in rng f & i in dom A1 by A20,A21,FUNCT_1:def 5,A5,PARTFUN1:def 8; then A30: [i,Sgm N/.i] in Indices A1 by A4,A20,A26,ZFMISC_1:106; per cases by A28,NAT_1:8; suppose A31: i<=n; then i0.K() by A17,A28; R*(i,f/.i) = ((A1*(i,f/.i))"*L).(f/.i)&L.(f/.i)=A1*(i,f/.i) by A4,A20,A25,A26,A29,A30,A32,MATRIX11:def 3,MATRIX_1:def 8; hence R*(i,f/.i) = (A1*(i,f/.i))"*(A1*(i,f/.i)) by A4,A20,A26,A29,FVSUM_1:63 .= 1_K() by A33,VECTSP_1:def 22; end; end; thus P[R,FB] by A2,A16,A20,A21,A5,A22; set S=Segm(R,Seg card N,N); set SA=Segm(A1,Seg card N,N); thus S is diagonal proof let i,j such that A34: [i,j] in Indices S & S*(i,j) <> 0.K(); reconsider I=i,J=j as Element of NAT by ORDINAL1:def 13; A35: rng Sgm (Seg card N)=(Seg card N) by FINSEQ_1:def 13; Indices S=[:Seg card Seg card N,Seg width S:] by MATRIX_1:26; then i in Seg card Seg card N by A34,ZFMISC_1:106; then i in Seg card card N by FINSEQ_1:76; then A36: [:Seg card N,N:] c= Indices A1 & Indices A1=Indices R & Indices S=Indices SA & Sgm (Seg card N)=idseq card N & (idseq card N).I=I by A4,A21,A26,MATRIX_1:27,ZFMISC_1:119, FINSEQ_3:54,FINSEQ_2:57,A5,FINSEQ_1:4; then A37: [I,Sgm N.J] in Indices A1 & S*(i,j)=R*(I,Sgm N.J) by A20,A34,A35,MATRIX13:def 1,17; then A38: Sgm N.J in Seg width A1 by ZFMISC_1:106; then reconsider SgmNJ=Sgm N.j as Element of NAT; per cases; suppose A39: I=n1; thus i=j proof assume A40: i<>j; R*(I,Sgm N.J)=((A1*(n1,f/.n1))"*L).SgmNJ & L.SgmNJ=A1*(I,SgmNJ) by A20,A25,A37,A38,A39,MATRIX11:def 3,MATRIX_1:def 8; then R*(I,Sgm N.J) = (A1*(n1,f/.n1))"*(A1*(I,SgmNJ)) by A38,FVSUM_1:63 .= (A1*(n1,f/.n1))"*(SA*(i,j)) by A34,A36,MATRIX13:def 1 .= (A1*(n1,f/.n1))"*(0.K()) by A16,A34,A36,A40,MATRIX_1:def 15 .= 0.K() by VECTSP_1:36; hence thesis by A34,A36,MATRIX13:def 1; end; end; suppose I<>n1; then R*(I,Sgm N.J) = A1*(Sgm (Seg card N).I,Sgm N.J) by A20,A36,A37,MATRIX11:def 3 .= SA*(i,j) by A34,A36,MATRIX13:def 1; hence i=j by A16,A34,A36,A37,MATRIX_1:def 15; end; end; thus for i st i in Seg card N holds R*(i,Sgm N/.i) <> 0.K() proof let i such that A41: i in Seg card N; f.i=f/.i & f.i in rng f & i in dom A1 by A20,A21,A41,FUNCT_1:def 5,A5,PARTFUN1:def 8; then A42: [i,Sgm N/.i] in Indices A1 by A4,A20,A26,ZFMISC_1:106; per cases; suppose i=n1; hence thesis by A27,A41; end; suppose i<>n1; then R*(i,Sgm N/.i)=A1*(i,Sgm N/.i) by A20,A42,MATRIX11:def 3; hence thesis by A17,A41; end; end; thus for i st i in dom R & i > card N holds Line(R,i) = m()|->0.K() proof let i such that A43: i in dom R & i > card N; A44: i>n1 & dom R=Seg len R & len R=n() by A13,A43,FINSEQ_1:def 3,MATRIX_1:def 3,XXREAL_0:2; hence Line(R,i) = Line(A1,i) by A43,MATRIX11:28 .= m()|->0.K() by A18,A21,A43,A44; end; let i,j such that A45: i in Seg card N & j in Seg width R & j < Sgm N.i; A46: [i,j] in Indices A1 by A21,A5,A26,A45,ZFMISC_1:106; per cases; suppose i=n1; then R*(i,j)=((A1*(n1,f/.n1))"*L).j & L.j=A1*(i,j) by A20,A25,A26,A45,A46,MATRIX11:def 3,MATRIX_1:def 8; hence R*(i,j) = (A1*(n1,f/.n1))"*(A1*(i,j)) by A26,A45,FVSUM_1:63 .= (A1*(n1,f/.n1))"*(0.K()) by A19,A26,A45 .= 0.K() by VECTSP_1:36; end; suppose i<>n1; hence R*(i,j) = A1*(i,j)by A20,A46,MATRIX11:def 3 .= 0.K() by A19,A26,A45; end; end; for n holds Q[n] from NAT_1:sch 2(A10,A11); then consider A be Matrix of n(),m(),K(),B be Matrix of n(),m'(),K()such that A47: r = the_rank_of A and A48: for i st i in Seg card N & i<=card N holds A*(i,Sgm N/.i) = 1_K() and A49: P[A,B] & Segm(A,Seg card N,N) is diagonal and for i st i in Seg card N holds A*(i,Sgm N/.i) <> 0.K() and A50: for i st i in dom A & i > card N holds Line(A,i) = m()|->0.K() and A51: for i,j st i in Seg card N & j in Seg width A & j < Sgm N.i holds A*(i,j) = 0.K(); take A,B,N; thus N c= Seg m() & r = the_rank_of A & r = card N & P[A,B] by A4,A5,A47,A49; set S=Segm(A,Seg card N,N); set ONE=1.(K(),card N); A52: card Seg card N=card N by FINSEQ_1:78; then A53: Indices ONE = [:Seg r,Seg r:] & Indices ONE = Indices S by A5,MATRIX_1:25,27; now let i,j such that A54: [i,j] in Indices ONE; reconsider i'=i,j'=j as Element of NAT by ORDINAL1:def 13; A55: i in Seg r & j in Seg r & dom Sgm N=Seg r by A4,A5,A53,A54,ZFMISC_1:106,FINSEQ_3:45; then A56: idseq r.i'=i' & i<=r by FINSEQ_2:57,FINSEQ_1:3,4; A57: S*(i,j) = A*(Sgm (Seg r).i',Sgm N.j') by A5,A53,A54,MATRIX13:def 1 .= A*(i',Sgm N.j') by A56,FINSEQ_3:54 .= A*(i',Sgm N/.j') by A55,PARTFUN1:def 8; now per cases; suppose A58: i'=j'; hence S*(i,j) = 1_K() by A5,A48,A55,A56,A57 .= ONE*(i,j) by A58,A54,MATRIX_1:def 12; end; suppose A59: i'<>j'; hence S*(i,j) = 0.K() by A49,A53,A54,MATRIX_1:def 15 .= ONE*(i,j) by A59,A54,MATRIX_1:def 12; end; end; hence S*(i,j) = ONE*(i,j); end; hence thesis by A50,A51,A52,MATRIX_1:28; end; begin :: The main theorem ::::::::::::::::::::::::::::::::::::: :: :: :: The Kronecker-Capelli theorem :: :: :: ::::::::::::::::::::::::::::::::::::: theorem Th57: for A,B be Matrix of K st len A = len B & (width A = 0 implies width B = 0) holds the_rank_of A = the_rank_of (A^^B) iff Solutions_of(A,B) is non empty proof let A,B be Matrix of K such that A1: len A = len B& (width A = 0 implies width B = 0); set L=len A; set wA=width A; set wB=width B; reconsider A'=A as Matrix of L,wA,K by MATRIX_2:7; reconsider B'=B as Matrix of L,wB,K by A1,MATRIX_2:7; deffunc F(Matrix of L,wB,K,Nat,Nat,Element of K) = RLine($1,$2,Line($1,$2) + $4*Line($1,$3)); defpred P[set,set] means for A1 be Matrix of L,wA,K, B1 be Matrix of L,wB,K st A1=$1 & B1=$2 holds the_rank_of (A'^^B')=the_rank_of (A1^^B1) & Solutions_of(A',B')=Solutions_of(A1,B1); A2: P[A',B']; A3: for A1 be Matrix of L,wA,K, B1 be Matrix of L,wB,K st P[A1,B1] for a be Element of K for i,j st j in dom A1 & (i = j implies a <> -1_K ) holds P[RLine(A1,i,Line(A1,i) + a*Line(A1,j)),F(B1,i,j,a)] proof let A1 be Matrix of L,wA,K, B1 be Matrix of L,wB,K such that A4: P[A1,B1]; let a be Element of K; let i,j such that A5: j in dom A1 & (i = j implies a <> -1_K ); set LAi=Line(A1,i); set LAj=Line(A1,j); set LBi=Line(B1,i); set LBj=Line(B1,j); set RA=RLine(A1,i,LAi + a*LAj); set RB=F(B1,i,j,a); A6: dom A1 = Seg len A1 by FINSEQ_1:def 3 .= Seg L by MATRIX_1:def 3; A7: len (A1^^B1)=L &len A1=L & len B1=L by MATRIX_1:def 3; A8: Solutions_of(A1,B1)=Solutions_of(RA,F(B1,i,j,a)) by A5,A6,Th40; per cases; suppose not i in Seg L; then RA=A1 & RB=B1 by A7,MATRIX13:40; hence thesis by A4; end; suppose A9: i in Seg L; A10: len (A1^^B1)=L by MATRIX_1:def 3; A11: len (LAi+a*LAj)=width A1 & len (LBi+a*LBj)=width B1 & len LAi=width A1 & len LBi=width B1 & len (a*LAj)=width A1 & len (a*LBj)=width B1 by FINSEQ_2:109; then RA^^RB = RLine(A1^^B1,i,(LAi+a*LAj)^(LBi+a*LBj))by Th18 .= RLine(A1^^B1,i,(LAi^LBi)+((a*LAj)^(a*LBj))) by Th3,A11 .= RLine(A1^^B1,i,(LAi^LBi)+a*(LAj^LBj)) by Th4 .= RLine(A1^^B1,i,Line(A1^^B1,i)+a*(LAj^LBj))by A9,Th15 .= RLine(A1^^B1,i,Line(A1^^B1,i)+a*Line(A1^^B1,j)) by A5,A6,Th15; then the_rank_of (RA^^RB)=the_rank_of (A1^^B1) by A5,A6,A10,MATRIX13:92; hence thesis by A8,A4; end; end; consider A1 be Matrix of L,wA,K, B1 be Matrix of L,wB,K,N such that A12: N c= Seg wA and A13: the_rank_of A' = the_rank_of A1 & the_rank_of A' = card N and A14: P[A1,B1] & Segm(A1,Seg card N,N) = 1.(K,card N) and A15: for i st i in dom A1 & i > card N holds Line(A1,i) = wA|->0.K and for i,j st i in Seg card N & j in Seg width A1 & j < Sgm N.i holds A1*(i,j) = 0.K from GAUSS2(A2,A3); per cases; suppose A16: L=0; then len (A'^^B')=0 by MATRIX_1:def 3; then the_rank_of A <=0 & the_rank_of (A^^B)<=0 by A16,MATRIX13:74; then the_rank_of A =0 & the_rank_of (A^^B)=0 & Solutions_of(A',B')={{}} by A16,Th51; hence thesis; end; suppose A17: L>0; per cases; suppose N<>{}; then card N<>0 by CARD_2:59; then A18: card N>0 & card N in Seg card N by FINSEQ_1:5; card N<=L by A13,MATRIX13:74; then A19: Seg card N c= Seg L & Seg len A1=dom A1 & len A1=L & Seg len B1=dom B1 & len B1=L & width A1=wA & width B1=wB by A17,FINSEQ_1:7,def 3,MATRIX_1:24; A20: Seg L\Seg card N c= Seg L by XBOOLE_1:36; set SN=Seg card N; set SS=Seg L\SN; A21: now let i such that A22: i in SS; i in Seg L & not i in SN by A22,XBOOLE_0:def 4; then 1<=i & (i<1 or i> card N) by FINSEQ_1:3; then i>card N & i in dom A1 by A22,A19,XBOOLE_0:def 4; hence Line(A1,i)=width A1|->0.K by A15,A19; end; A23: card SN=card N by FINSEQ_1:78; reconsider P2=Sgm SN " SN,Q2 = Sgm Seg wA " N as without_zero finite Subset of NAT by MATRIX13:53; dom Sgm SN=Seg card SN&rng Sgm SN=SN by FINSEQ_1:def 13,FINSEQ_3:45; then A24: P2 = SN by A23,RELAT_1:169; rng Sgm Seg wA=Seg wA by FINSEQ_1:def 13; then A25: Sgm Seg wA.:Q2 = N & Q2 c= dom Sgm Seg wA & dom Sgm Seg wA=Seg card Seg wA &Sgm Seg wA is one-to-one by A12,FUNCT_1:147,RELAT_1:167,FINSEQ_3:45,99; then N,Q2 are_equipotent by CARD_1:60; then A26: card N=card Q2 by CARD_1:21; thus the_rank_of A=the_rank_of(A^^B) implies Solutions_of(A,B) is non empty proof assume the_rank_of A = the_rank_of (A^^B); then the_rank_of A1 = the_rank_of (A1^^B1) by A13,A14; then for i st i in (dom A1)\Seg card N holds Line(A1,i) = width A1|-> 0.K & Line(B1,i) = width B1 |-> 0.K by A19,A20,A21,Th24; then A27: Solutions_of(A1,B1)=Solutions_of(Segm(A1,SN,Seg wA), Segm(B1,SN,Seg wB)) by A18,A19,Th45; Segm(Segm(A1,SN,Seg wA),P2,Q2)=1.(K,card N) by A14,A12,MATRIX13:56; then ex X be Matrix of card Seg wA,card Seg wB,K st Segm(X,Seg card Seg wA \ Q2,Seg card Seg wB) = 0.(K,card Seg wA-'card SN,card Seg wB) & Segm(X,Q2,Seg card Seg wB) = Segm(B1,SN,Seg wB) & X in Solutions_of(Segm(A1,SN,Seg wA),Segm(B1,SN,Seg wB)) by A25,A18,Th50,A23,A24,A26; hence thesis by A14,A27; end; thus Solutions_of(A,B) is non empty implies the_rank_of A=the_rank_of (A^^B) proof assume Solutions_of(A,B) is non empty; then Solutions_of(A1,B1) is non empty by A14; then consider x such that A28: x in Solutions_of(A1,B1) by XBOOLE_0:def 1; reconsider x as Matrix of wA,wB,K by A17,A28,Th53; set AB=A1^^B1; A29: dom AB=Seg len AB & len AB=L & width AB=width A1+width B1 & Indices AB=[:Seg L,Seg (width A1+width B1):] by A17,MATRIX_1:24,FINSEQ_1:def 3; now let i such that A30: i in SS; A31: i in dom A1&Line(A1,i)=width A1|->0.K by A19,A20,A30,A21; A32: x in Solutions_of(A1,B1) & i in dom A1 & Line(A1,i)= width A1|->0.K implies Line(B1,i)=width B1|->0.K by Th41; thus Line(AB,i)=Line(A1,i)^Line(B1,i)by A20,A30,Th15 .=width AB|->0.K by A31,A32,A29,FINSEQ_2:143,A28; end; then A33: the_rank_of Segm(AB,SN,Seg width AB)=the_rank_of AB by A19,A29,Th11; len Segm(AB,SN,Seg width AB)=card SN by MATRIX_1:def 3; then the_rank_of AB<=card SN by A33,MATRIX13:74; then A34: the_rank_of AB<=card N by FINSEQ_1:78; width A1<=width AB by A29,NAT_1:11; then Seg width A1 c= Seg width AB by FINSEQ_1:7; then A35: [:Seg L,Seg width A1:] c= Indices AB by A29,ZFMISC_1: 118; the_rank_of Segm(AB,Seg L,Seg width A1)=card N by A13,Th19; then card N <= the_rank_of AB by A35,MATRIX13:79; then the_rank_of AB=card N by A34,XXREAL_0:1; hence thesis by A13,A14; end; end; suppose A36: N={}; set ZERO=0.(K,L,wA); A37: len ZERO=L & len A1=L & width A1=wA & len B'=L & width B'=wB & Indices ZERO=[:Seg L,Seg wA:] & Indices B'=[:Seg L,Seg wB:] & wA+wB = width (A'^^B')& L = len (A'^^B') & Indices (A'^^B')=[:Seg L,Seg (wA+wB):] by A17,MATRIX_1:24; now let i such that A38: 1<=i & i<=L; i in NAT by ORDINAL1:def 13; then A39: i in Seg L & dom A1=Seg len A1 & len A1=L by A38,FINSEQ_1:def 3,MATRIX_1:def 3; hence ZERO.i = wA|->0.K by A17,FINSEQ_2:71 .= Line(A1,i) by A36,CARD_1:47,A38,A39,A15 .= A1.i by A39,MATRIX_2:10; end; then ZERO=A1 by A37,FINSEQ_1:18; then A40: the_rank_of A=0 by A13,A37,MATRIX13:95; then A41: ZERO=A by MATRIX13:95; thus the_rank_of A=the_rank_of(A^^B) implies Solutions_of(A,B) is non empty proof assume A42: the_rank_of A = the_rank_of (A^^B); A43: Segm(A'^^B',Seg L,Seg (wA+wB)\Seg wA)=B by Th19; Seg (wA+wB)\Seg wA c= Seg (wA+wB) by XBOOLE_1:36; then [:Seg L,Seg (wA+wB)\Seg wA:] c= Indices (A^^B) by A37,ZFMISC_1:118; then 0 >= the_rank_of B by A40,A43,A42,MATRIX13:79; then 0=the_rank_of B; then A44: B=0.(K,L,wB) by A1,MATRIX13:95; consider x be Matrix of wA,wB,K; wA=0 or wA>0; then wA=0 & wB=0 or Solutions_of(A',B') = {X where X is Matrix of wA,wB,K:not contradiction} by A41,A44,A1,A17,Th54; then Solutions_of(A',B')={{}} or x in Solutions_of(A',B') by Th56,A41,A44; hence thesis; end; thus Solutions_of(A,B) is non empty implies the_rank_of A=the_rank_of(A^^B) proof assume A45: Solutions_of(A,B) is non empty; assume the_rank_of A <> the_rank_of (A^^B); then the_rank_of (A'^^B')>0 by A40; then consider i,j such that A46: [i,j] in Indices (A'^^B') & (A'^^B')*(i,j)<>0.K by MATRIX13:94; A47: i in Seg L & j in Seg (wA+wB) &len Line(A',i)=wA by A37,A46,ZFMISC_1:106,FINSEQ_2:109; then A48: dom Line(A'^^B',i)=Seg (wA+wB) & dom Line(A',i)=Seg wA & dom Line(B',i)=Seg wB & Line(A'^^B',i)=Line(A',i)^Line(B',i) by A37,FINSEQ_2:144,Th15; per cases by A47,A48,FINSEQ_1:38; suppose A49: j in dom Line(A',i); then A50: [i,j] in Indices ZERO by A37,A47,A48,ZFMISC_1:106; (A'^^B')*(i,j) = Line(A'^^B',i).j by A37,A47,MATRIX_1:def 8 .= Line(A',i).j by A48,A49,FINSEQ_1:def 7 .= A'*(i,j) by A48,A49,MATRIX_1:def 8 .= 0.K by A50,A41,MATRIX_3:3; hence thesis by A46; end; suppose ex n st n in dom Line(B',i) & j=wA + n; then consider n such that A51: n in dom Line(B',i) & j=wA + n; A52: [i,n] in Indices B & B=0.(K,L,wB) by A37,A41,A45,A47,A48,A51,ZFMISC_1:106,Th52; (A'^^B')*(i,j) = Line(A'^^B',i).j by A37,A47,MATRIX_1:def 8 .= Line(B',i).n by A47,A48,A51,FINSEQ_1:def 7 .= B'*(i,n) by A48,A51,MATRIX_1:def 8 .= 0.K by A52,MATRIX_3:3; hence thesis by A46; end; end; end; end; end; begin :: Space of Solutions of Linear Equations definition let K; let A be Matrix of K; let b be FinSequence of K; func Solutions_of(A,b) equals {f : ColVec2Mx f in Solutions_of(A,ColVec2Mx b)}; coherence; end; theorem Th58: for x st x in Solutions_of(A,ColVec2Mx b) ex f st x = ColVec2Mx f & len f = width A proof let x such that A1: x in Solutions_of(A,ColVec2Mx b); consider X such that A2: X=x & len X=width A & width X = width ColVec2Mx b & A * X = ColVec2Mx b by A1; per cases; suppose A3: len X=0; take f=0|-> 0.K; len f=0 by FINSEQ_2:69; then len (ColVec2Mx f)=0 by MATRIX_1:def 3; hence thesis by A2,A3,FINSEQ_2:69,MATRIX_1:37; end; suppose A4: len X>0; then len A<>0 & len A=len (ColVec2Mx b) by A1,A2,MATRIX_1:def 4,Th33; then len b<>0 by MATRIX_1:def 3; then len b>0; then A5: width X=1 by A2,MATRIX_1:24; take f=Col(X,1); thus thesis by A2,A4,A5,Th26,MATRIX_1:def 9; end; end; theorem Th59: for f st ColVec2Mx f in Solutions_of(A,ColVec2Mx b) holds len f = width A proof let f such that A1: ColVec2Mx f in Solutions_of(A,ColVec2Mx b); consider g such that A2: ColVec2Mx f = ColVec2Mx g & len g = width A by A1,Th58; len ColVec2Mx f = len f & len ColVec2Mx g =len g by MATRIX_1:def 3; hence thesis by A2; end; definition let K; let A be Matrix of K; let b be FinSequence of K; redefine func Solutions_of(A,b) -> Subset of (width A)-VectSp_over K; coherence proof Solutions_of(A,b) c= the carrier of (width A)-VectSp_over K proof let x; assume x in Solutions_of(A,b); then consider f such that A1: x=f & ColVec2Mx f in Solutions_of(A,ColVec2Mx b); A2: (width A)-tuples_on the carrier of K= the carrier of (width A)-VectSp_over K by MATRIX13:102; len f=width A by A1,Th59; then f is Element of (width A)-tuples_on the carrier of K by FINSEQ_2:110; hence thesis by A1,A2; end; hence thesis; end; end; registration let K; let A be Matrix of K; let k be Element of NAT; cluster Solutions_of(A,k|->0.K) -> linearly-closed Subset of (width A)-VectSp_over K; coherence proof set k0=k|->0.K; set S=Solutions_of(A,k0); set V=(width A)-VectSp_over K; A1: ColVec2Mx k0=0.(K,k,1) by Th32; A2: now let v,u being Element of V such that A3: v in S & u in S; consider f such that A4: v=f & ColVec2Mx f in Solutions_of(A,ColVec2Mx k0) by A3; consider g such that A5: u=g & ColVec2Mx g in Solutions_of(A,ColVec2Mx k0) by A3; A6: len g=width A & len f =width A by A4,A5,Th59; reconsider f,g as Element of (width A)-tuples_on the carrier of K by A4,A5,MATRIX13:102; ColVec2Mx f+ColVec2Mx g in Solutions_of(A,0.(K,k,1)+0.(K,k,1)) by A4,A5,Th37,A1; then ColVec2Mx f+ColVec2Mx g in Solutions_of(A,0.(K,k,1)) by MATRIX_3:6; then ColVec2Mx (f+g) in Solutions_of(A,0.(K,k,1))by A6,Th28; then f+g in S by A1; hence v+u in S by A4,A5,MATRIX13:102; end; now let a being Element of K,v being Element of V such that A7: v in S; consider f such that A8: v=f & ColVec2Mx f in Solutions_of(A,ColVec2Mx k0) by A7; reconsider f as Element of (width A)-tuples_on the carrier of K by A8,MATRIX13:102; now per cases; suppose k=0; then len 0.(K,k,1)=0 & len (a*0.(K,k,1))=len 0.(K,k,1) by MATRIX_1:23,MATRIX_3:def 5; then 0.(K,k,1)={} & a*0.(K,k,1)={} by FINSEQ_1:25; hence 0.(K,k,1)=a*0.(K,k,1); end; suppose A9: k>0; then A10: len 0.(K,k,1)=k & width 0.(K,k,1)=1 by MATRIX_1:24; hence a*0.(K,k,1) = a*(0.K*0.(K,k,1)) by A9,MATRIX_5:40 .= (a*0.K)*0.(K,k,1) by MATRIX_5:12 .= 0.K*0.(K,k,1) by VECTSP_1:36 .= 0.(K,k,1) by A9,A10,MATRIX_5:40; end; end; then a*ColVec2Mx f in Solutions_of(A,0.(K,k,1)) by A8,A1,Th35; then ColVec2Mx (a*f) in Solutions_of(A,0.(K,k,1)) by Th30; then a*f in Solutions_of(A,k0) by A1; hence a*v in S by A8,MATRIX13:102; end; hence thesis by A2,VECTSP_4:def 1; end; end; theorem Th60: Solutions_of(A,b) is non empty & width A = 0 implies len A=0 proof set S=Solutions_of(A,b); assume A1: S is non empty & width A=0; then consider x such that A2: x in S by XBOOLE_0:def 1; consider f such that A3: x=f & ColVec2Mx f in Solutions_of(A,ColVec2Mx b) by A2; consider X such that A4: ColVec2Mx f=X & len X = width A & width X = width ColVec2Mx b and A5: A * X = ColVec2Mx b by A3; width (A * X) = width X by A4,MATRIX_3:def 4 .= 0 by A1,A4,MATRIX_1:def 4; then len b<=0 by A5,MATRIX_1:24; hence 0 = len b .= len ColVec2Mx b by MATRIX_1:def 3 .= len A by A3,Th33; end; theorem Th61: width A <> 0 or len A = 0 implies Solutions_of(A,len A|->0.K) is non empty proof assume A1: width A <> 0 or len A = 0; set L=len A|->0.K; A2: len L=len A by FINSEQ_2:69; reconsider A'=A as Matrix of len A,width A,K by MATRIX_2:7; per cases by A1; suppose len A=0; then Solutions_of(A',ColVec2Mx L) = {{}} by A2,Th51; then A3: {} in Solutions_of(A',ColVec2Mx L) by TARSKI:def 1; then consider f such that A4: {} = ColVec2Mx f & len f = width A by Th58; f in Solutions_of(A,L) by A3,A4; hence thesis; end; suppose A5: width A > 0; A6: len ColVec2Mx L=len L & ColVec2Mx L =0.(K,len A,1) by MATRIX_1:def 3,Th32; then the_rank_of A=the_rank_of (A^^(ColVec2Mx L)) by Th23; then Solutions_of(A,ColVec2Mx L) is non empty by A2,A5,A6,Th57; then consider x such that A7: x in Solutions_of(A,ColVec2Mx L) by XBOOLE_0:def 1; consider f such that A8: x = ColVec2Mx f & len f = width A by A7,Th58; f in Solutions_of(A,L) by A7,A8; hence thesis; end; end; definition let K; let A be Matrix of K; assume A1: width A = 0 implies len A = 0; func Space_of_Solutions_of(A) -> strict Subspace of (width A)-VectSp_over K means :Def5: the carrier of it = Solutions_of(A,len A|->0.K); existence proof Solutions_of(A,len A|->0.K) is non empty by A1,Th61; hence thesis by VECTSP_4:42; end; uniqueness by VECTSP_4:37; end; theorem for A be (Matrix of K), b be FinSequence of K st Solutions_of(A,b) is non empty holds Solutions_of(A,b) is Coset of Space_of_Solutions_of A proof let A be (Matrix of K),b be FinSequence of K; set V=(width A)-VectSp_over K; reconsider B=b as Element of (len b)-tuples_on the carrier of K by FINSEQ_2:110; set CB=ColVec2Mx B; assume Solutions_of(A,b) is non empty; then consider x such that A1: x in Solutions_of(A,B) by XBOOLE_0:def 1; consider f such that A2: x=f & ColVec2Mx f in Solutions_of(A,CB) by A1; set Cf=ColVec2Mx f; A3: len f =width A by A2,Th59; then reconsider f as Element of (width A)-tuples_on the carrier of K by FINSEQ_2:110; reconsider F=f as Element of V by MATRIX13:102; A4: len CB=len B & len A=len CB by A2,MATRIX_1:def 3,Th33; width A=0 implies len A=0 by A1,Th60; then A5: the carrier of Space_of_Solutions_of A=Solutions_of(A,len A|->0.K) by Def5; A6: Solutions_of(A,b) c= F+ Space_of_Solutions_of A proof let y such that A7: y in Solutions_of(A,b); consider g such that A8: y=g & ColVec2Mx g in Solutions_of(A,CB) by A7; len g =width A by A8,Th59; then reconsider g as Element of (width A)-tuples_on the carrier of K by FINSEQ_2:110; reconsider G=g,GF=g+(-1_K)*f as Element of V by MATRIX13:102; set Cg=ColVec2Mx g; A9: width CB=width((-1_K)*CB) by MATRIX_3:def 5; A10: len B=len ((-1_K)*B) & len f=len ((-1_K)*f) by A3,FINSEQ_2:109; (-1_K)*CB=ColVec2Mx ((-1_K)*B) by Th30; then A11: CB+(-1_K)*CB = ColVec2Mx (B+(-1_K)*B) by Th28,A10 .= ColVec2Mx (B+-B) by FVSUM_1:72 .= ColVec2Mx (len A|->0.K) by A4,FVSUM_1:35; A12: Cg+(-1_K)*Cf = Cg+ColVec2Mx ((-1_K)*f) by Th30 .=ColVec2Mx (g+(-1_K)*f) by A3,Th28,A10,A8,Th59; f+(g+(-1_K)*f) = f+((-1_K)*f+g) by FINSEQOP:34 .= f+(-f+g) by FVSUM_1:72 .= (f+-f)+g by FINSEQOP:29 .= (width A|->0.K)+g by FVSUM_1:35 .= g by FVSUM_1:28; then A13: F+GF=g by MATRIX13:102; (-1_K)*Cf in Solutions_of(A,(-1_K)*CB) by A2,Th35; then Cg+(-1_K)*Cf in Solutions_of(A,ColVec2Mx (len A|->0.K)) by A8,A11,A9,Th37; then g+(-1_K)*f in Solutions_of(A,len A|->0.K) by A12; then GF in Space_of_Solutions_of A by A5,STRUCT_0:def 5; hence thesis by A8,A13; end; F+ Space_of_Solutions_of A c=Solutions_of(A,b) proof let y; assume y in F+ Space_of_Solutions_of A; then consider U be Element of V such that A14: U in Space_of_Solutions_of A & y=F+U by VECTSP_4:57; reconsider u=U as Element of (width A)-tuples_on the carrier of K by MATRIX13:102; u in Solutions_of(A,len A|->0.K) by A14,A5,STRUCT_0:def 5; then consider g such that A15: u=g & ColVec2Mx g in Solutions_of(A,ColVec2Mx (len A|->0.K)); width A = len g by A15,Th59; then A16: ColVec2Mx (f+g)=Cf+ColVec2Mx g by A2,Th59,Th28; len (len A|-> 0.K) =len A & (len A=0 or len A<>0) by FINSEQ_2:69; then A17: (width CB=1 & width ColVec2Mx (len A|->0.K)=1) or (width CB=0 & width ColVec2Mx (len A|->0.K)=0) by A4,MATRIX_1:23,Th26; ColVec2Mx (len A|->0.K)=0.(K,len A,1) by Th32; then CB+ColVec2Mx (len A|->0.K)=CB by A4,MATRIX_3:6; then ColVec2Mx (f+g) in Solutions_of(A,CB) by A2,A15,A16,A17,Th37; then f+g in Solutions_of(A,b); hence thesis by A14,A15,MATRIX13:102; end; then F+ Space_of_Solutions_of A =Solutions_of(A,b) by A6,XBOOLE_0:def 10; hence thesis by VECTSP_4:def 6; end; theorem Th63: for A st ( width A = 0 implies len A = 0 ) & the_rank_of A = 0 holds Space_of_Solutions_of A = (width A)-VectSp_over K proof let A such that A1: width A = 0 implies len A = 0 and A2: the_rank_of A = 0; set L=len A|->0.K; the carrier of (width A)-VectSp_over K c= Solutions_of(A,L) proof let x such that A3: x in the carrier of (width A)-VectSp_over K; reconsider x'=x as Element of (width A)-tuples_on the carrier of K by A3,MATRIX13:102; A4: A=0.(K,len A,width A) & ColVec2Mx L=0.(K,len A,1) by A2,MATRIX13:95,Th32; per cases; suppose len A=0; then A5: Solutions_of(A,ColVec2Mx L)={{}} & width A=0 by A4,Th51, MATRIX_1:def 4; then the carrier of (width A)-VectSp_over K = 0-tuples_on the carrier of K by MATRIX13:102 .= {<*>the carrier of K} by FINSEQ_2:112; then A6: x=<*>the carrier of K by A3,TARSKI:def 1; A7: {} in Solutions_of(A,ColVec2Mx L) by A5,TARSKI:def 1; then consider f such that A8: {} = ColVec2Mx f & len f = width A by Th58; f=x by A5,A6,A8,FINSEQ_1:25; hence thesis by A7,A8; end; suppose A9: len A>0; then width A>0 by A1; then A10: Solutions_of(A,ColVec2Mx L)= {X where X is Matrix of width A,1,K:not contradiction} by A4,A9,Th54; len x'=width A by FINSEQ_2:109; then ColVec2Mx x' in Solutions_of(A,ColVec2Mx L) by A10; hence thesis; end; end; then the carrier of (width A)-VectSp_over K = Solutions_of(A,L) by XBOOLE_0:def 10 .= the carrier of Space_of_Solutions_of A by A1,Def5; hence thesis by VECTSP_4:39; end; theorem for A st Space_of_Solutions_of A = (width A)-VectSp_over K holds the_rank_of A = 0 proof let A such that A1: Space_of_Solutions_of A = (width A)-VectSp_over K; assume the_rank_of A <> 0; then the_rank_of A >0; then consider i,j such that A2: [i,j] in Indices A & A*(i,j) <> 0.K by MATRIX13:94; A3: j in Seg width A & i in dom A & dom A=Seg len A by A2,ZFMISC_1:106,FINSEQ_1:def 3; then A4: width A<>0 & len A<>0 by FINSEQ_1:4; set L=Line(1.(K,width A),j); A5: width 1.(K,width A)=width A by MATRIX_1:25; then L in (width A)-tuples_on the carrier of K; then L in the carrier of Space_of_Solutions_of A by A1,MATRIX13:102; then L in Solutions_of(A,len A|->0.K) by Def5,FINSEQ_1:4,A3; then consider f such that A6: f=L & ColVec2Mx f in Solutions_of(A,ColVec2Mx (len A|->0.K)); consider X such that A7: X=ColVec2Mx f & len X = width A and width X = width ColVec2Mx (len A|->0.K) and A8: A * X = ColVec2Mx (len A|->0.K) by A6; A9: len A>0 & ColVec2Mx (len A|->0.K)=0.(K,len A,1) by Th32,A4; then Indices ColVec2Mx (len A|->0.K)=[:Seg len A,Seg 1:] & 1 in Seg 1 by MATRIX_1:24; then A10: [i,1] in Indices ColVec2Mx (len A|->0.K) by A3,ZFMISC_1:106; then Line(A,i)"*"Col(X,1) = 0.(K,len A,1)*(i,1) by A7,A8,A9,MATRIX_3:def 4 .= 0.K by A10,A9,MATRIX_3:3; then A11: 0.K = Col(X,1)"*"Line(A,i) by FVSUM_1:115 .= Sum(mlt(f,Line(A,i))) by A3,A7,Th26,FINSEQ_1:4; A12: dom L=Seg width A & dom Line(A,i)=Seg width A by A5,FINSEQ_2:144; A13: Indices 1.(K,width A)=[:Seg width A,Seg width A:] by MATRIX_1:25; then [j,j] in Indices 1.(K,width A) by A3,ZFMISC_1:106; then A14: 1_K = 1.(K,width A)*(j,j) by MATRIX_1:def 12 .= L.j by MATRIX_1:def 8,A3,A5; now let k such that A15: k in dom L & k<>j; [j,k] in Indices 1.(K,width A) by A13,A3,A12,A15,ZFMISC_1:106; hence 0.K = 1.(K,width A)*(j,k) by A15,MATRIX_1:def 12 .= L.k by MATRIX_1:def 8,A5,A12,A15; end; then Sum(mlt(L,Line(A,i))) = Line(A,i).j by A3,A12,A14,MATRIX_3:19 .= A*(i,j) by A3,MATRIX_1:def 8; hence thesis by A11,A6,A2; end; theorem Th65: for i,j st j in Seg m & n>0 & (i = j implies a <> -1_K) holds Space_of_Solutions_of A' = Space_of_Solutions_of RLine(A',i,Line(A',i) + a*Line(A',j)) proof let i,j such that A1: j in Seg m & n>0 and A2: i = j implies a <> -1_K; set L=len A'|->0.K; len L=len A' & len A'=m by FINSEQ_2:69,MATRIX_1:def 3; then reconsider C=ColVec2Mx L as Matrix of m,1,K; set RC=RLine(C,i,Line(C,i) + a*Line(C,j)); A3: C=0.(K,len A',1) & m<>0 by Th32,A1,FINSEQ_1:4; now let i',j' be Nat such that A4: [i',j'] in Indices C; reconsider I=i',J=j' as Element of NAT by ORDINAL1:def 13; A5: len (Line(C,i) + a*Line(C,j))=width C by FINSEQ_2:109; now per cases; suppose A6: i'=i; m>0 by A3; then A7: len C=m & 1=width C & Indices C=[:Seg m,Seg 1:] by MATRIX_1:24; then A8: j' in Seg 1 & i' in Seg m by A4,ZFMISC_1:106; then A9: Line(C,i).j'=C*(i,j') & Line(C,j).j'=C*(j,j') & [i,j'] in Indices C & [j,j'] in Indices C by A1,A7,MATRIX_1:def 8,A6,ZFMISC_1:106; then (a*Line(C,j)).j'=a*(C*(j,j')) by A7,A8,FVSUM_1:63; then (Line(C,i) + a*Line(C,j)).j' = C*(i,j')+a*(C*(j,j')) by A7,A8,A9,FVSUM_1:22 .= 0.K +a*(C*(j,j')) by A3,A9,MATRIX_3:3 .= 0.K +a*0.K by A3,A9,MATRIX_3:3 .= 0.K +0.K by VECTSP_1:36 .= 0.K by RLVECT_1:def 7 .= C*(i',j') by A3,A4,MATRIX_3:3; hence C*(I,J)=RC*(I,J) by A9,A6,A5,MATRIX11:def 3; end; suppose i<>i'; hence C*(I,J)=RC*(I,J) by A4,A5,MATRIX11:def 3; end; end; hence C*(i',j')=RC*(i',j'); end; then A10: RC=C by MATRIX_1:28; set R=RLine(A',i,Line(A',i) + a*Line(A',j)); set SR=Space_of_Solutions_of R; set SA=Space_of_Solutions_of A'; m>0 by A3; then A11: len A'=m & len R=m & width A'=n & width R=n by MATRIX_1:24; then Solutions_of(A',C)=Solutions_of(R,C) & the carrier of SA = Solutions_of(A',L) & the carrier of SR = Solutions_of(R,L) by A1,A2,A10,Th40,Def5; hence thesis by A11,VECTSP_4:37; end; theorem Th66: for N st N c= dom A & N is non empty & width A > 0 & for i st i in (dom A) \ N holds Line(A,i) = width A |-> 0.K holds Space_of_Solutions_of A = Space_of_Solutions_of Segm(A,N,Seg width A) proof let N such that A1: N c= dom A & N is non empty and A2: width A>0 and A3: for i st i in (dom A) \ N holds Line(A,i) = width A |-> 0.K; set L=len A|->0.K; set C=ColVec2Mx L; A4: len L=len A & len C=len L & dom A=Seg len A by FINSEQ_1:def 3,FINSEQ_2:69,MATRIX_1:def 3; then A5: dom C=dom A & C=0.(K,len A,1) by FINSEQ_3:31,Th32; reconsider A'=A as Matrix of len A,width A,K by MATRIX_2:7; A6: Seg len A<>{} by A4,A1,XBOOLE_1:3; then A7: width C=1 & dom A is non empty by A4,Th26,FINSEQ_1:4; then A8: card Seg width C=1 by FINSEQ_1:78; now let i such that A9: i in (dom A) \ N; A10: i in dom A by A9,XBOOLE_0:def 4; then Line(C,i) = C.i by A4,MATRIX_2:10 .= (len A|->(width C|->0.K)).i by A5,A6,A4,Th26,FINSEQ_1:4 .= width C|->0.K by A4,A10,FINSEQ_2:71,FINSEQ_1:4; hence Line(A,i)=width A|->0.K & Line(C,i)=width C|->0.K by A9,A3; end; then A11: Solutions_of(A,C)=Solutions_of(Segm(A,N,Seg width A),Segm(C,N,Seg width C)) by A1,A5,Th45; now let k,l such that A12: [k,l] in Indices Segm(C,N,Seg width C); A13: Indices Segm(C,N,Seg width C)=Indices 0.(K,card N,1) by MATRIX_1:27,A8; reconsider kk=k,ll=l as Element of NAT by ORDINAL1:def 13; [:N,Seg width C:] c= Indices C & rng Sgm N=N & rng Sgm Seg 1=Seg 1 by A1,A4,A5,ZFMISC_1:118,FINSEQ_1:def 13; then A14: [Sgm N.kk,Sgm Seg width C.ll] in Indices C by A7,A12,MATRIX13 :17; thus Segm(C,N,Seg width C)*(k,l) = C*(Sgm N.kk,Sgm Seg width C.ll) by A12,MATRIX13:def 1 .= 0.K by A14,A5,MATRIX_3:3 .=0.(K,card N,1)*(k,l) by A12,A13,MATRIX_3:3; end; then A15: Segm(C,N,Seg width C) = 0.(K,card N,1) by A8,MATRIX_1:28 .= ColVec2Mx (card N|->0.K) by Th32; set S=Segm(A,N,Seg width A); set SA=Space_of_Solutions_of A; set SS=Space_of_Solutions_of S; card N<>0 by A1,CARD_2:59; then card N>0; then width S=card Seg width A by MATRIX_1:24; then A16: len S=card N & width A=width S by MATRIX_1:def 3,FINSEQ_1:78; then the carrier of SA = Solutions_of(A,L) & the carrier of SS = Solutions_of(S,card N|->0.K) by A2,Def5; hence thesis by A16,VECTSP_4:37,A11,A15; end; Lm7: for A be set st A c= dom g ex ga,gb be FinSequence of K st ga=g*Sgm A & gb=g*Sgm (dom g\A) & Sum g = Sum ga + Sum gb proof let A be set such that A1: A c= dom g; A2: dom g=Seg len g & dom g\A c= dom g by FINSEQ_1:def 3,XBOOLE_1:36; then A3: rng Sgm(A)=A & rng Sgm(dom g\A)=dom g\A by A1,FINSEQ_1:def 13; then reconsider ga=g*Sgm A,gb=g*Sgm (dom g\A) as FinSequence by A1,A2,FINSEQ_1:20; rng ga c=rng g & rng gb c=rng g & rng g c= the carrier of K by RELAT_1:45,FINSEQ_1:def 4; then rng ga c= the carrier of K & rng gb c= the carrier of K by XBOOLE_1:1; then reconsider ga,gb as FinSequence of K by FINSEQ_1:def 4; take ga,gb; (idseq len g)"A=A & (idseq len g)"(dom g\A)=dom g\A & dom g=rng idseq len g& dom g=dom idseq len g by A1,A2,FUNCT_2:171,RELAT_1:71; then A4: Sgm(A)^Sgm(dom g\A) is Permutation of dom g by FINSEQ_3:123; then reconsider gS=g*(Sgm(A)^Sgm(dom g\A)) as FinSequence of K by A2,FINSEQ_2:50; set Ad=the addF of K; A5: Ad is commutative associative & Ad has_a_unity by FVSUM_1:10; then Ad $$ g = Ad "**" gS by A4,FINSOP_1:8 .= Ad"**"(ga^gb) by A1,A2,A3,Th5 .= Sum ga+Sum gb by A5,FINSOP_1:6; hence thesis; end; theorem Th67: for A be Matrix of n,m,K, N st card N = n & N c= Seg m & Segm(A,Seg n,N) = 1.(K,n) & n > 0 & m-'n>0 ex MVectors be Matrix of m-'n,m,K st Segm(MVectors,Seg (m-'n),Seg m \ N) = 1.(K,m-'n) & Segm(MVectors,Seg (m-'n),N) = -Segm(A,Seg n,Seg m \N)@ & Lin(lines MVectors) = Space_of_Solutions_of A proof let A be Matrix of n,m,K, N such that A1: card N = n & N c= Seg m and A2: Segm(A,Seg n,N) = 1.(K,n) and A3: n > 0 & m-'n>0; A4: m<>0 by FINSEQ_1:4,A1,XBOOLE_1:3,A3,CARD_1:47; then A5: len A=n & width A=m & m>0 by A3,MATRIX_1:24; consider MV be Matrix of m-'n,m,K such that A6: Segm(MV,Seg (m-'n),Seg m \ N) = 1.(K,m-'n) and A7: Segm(MV,Seg (m-'n),N) = -Segm(A,Seg n,Seg m \N)@ and A8: for l for M be Matrix of m,l,K st for i st i in Seg l holds (ex j st j in Seg (m-'n) & Col(M,i) = Line(MV,j)) or Col(M,i) = m|->0.K holds M in Solutions_of(A,0.(K,n,l)) by A1,A2,A3,Th49; take MV; A9: len MV=m-'n & width MV=m & Indices MV=[:Seg (m-'n),Seg m:] by A3,MATRIX_1:24; A10: lines MV c= Solutions_of(A,len A|->0.K) proof let x such that A11: x in lines MV; consider k such that A12: k in Seg (m-'n) & x = Line(MV,k) by A11,MATRIX13:103; set C=ColVec2Mx Line(MV,k); A13: m = width MV by A3,MATRIX_1:24 .= len Line(MV,k) by FINSEQ_2:109; now let i; assume i in Seg 1; then i=1 & Col(C,1)=Line(MV,k) by A13,A4,Th26,TARSKI:def 1,FINSEQ_1:4; hence (ex j st j in Seg (m-'n) & Col(C,i) = Line(MV,j)) or Col(C,i) = m|->0.K by A12; end; then C in Solutions_of(A,0.(K,n,1)) by A13,A8; then C in Solutions_of(A,ColVec2Mx(len A|->0.K))by A5,Th32; hence thesis by A12; end; A14: Solutions_of(A,len A|->0.K)=the carrier of Space_of_Solutions_of A by A5,Def5; Lin (lines MV) is Subspace of Lin (Solutions_of(A,len A|->0.K)) by A10,A5,VECTSP_7:18; then the carrier of Lin (lines MV) c= the carrier of Lin (Solutions_of(A,len A|->0.K)) by VECTSP_4:def 2; then A15: the carrier of Lin (lines MV) c= the carrier of Space_of_Solutions_of(A) by VECTSP_7:16,A14; n <=card Seg m & card Seg m=m by A1,NAT_1:44,FINSEQ_1:78; then A16: m-'n=m-n & card (Seg m \ N) =m-n by A1,BINARITH:50,CARD_2:63; then A17: card Seg (m-'n)=card (Seg m \ N) by FINSEQ_1:78; A18: the_rank_of MV = m-'n proof A19: EqSegm(MV,Seg (m-'n),Seg m \ N)=1.(K,m-'n) by MATRIX13:def 3,A6,A16,FINSEQ_1:78; Seg m \ N c= Seg m by XBOOLE_1:36; then A20: [:Seg (m-'n),Seg m \ N:] c= Indices MV by ZFMISC_1:118,A9; m-'n+0>0 by A3; then m-'n>=1 by NAT_1:19; then Det 1.(K,m-'n)=1_K & 0.K<>1_K by MATRIX_7:16; then A21: m-'n <= the_rank_of MV by A16,A17,A19,A20,MATRIX13:def 4; len MV=m-'n & len MV >=the_rank_of MV by MATRIX13:74,MATRIX_1:def 3; hence thesis by A21,XXREAL_0:1; end; the carrier of Space_of_Solutions_of A c= the carrier of Lin(lines MV) proof let y; assume y in the carrier of Space_of_Solutions_of A; then y in Solutions_of(A,len A|->0.K) by A5,Def5; then consider f such that A22: f=y & ColVec2Mx f in Solutions_of(A,ColVec2Mx (len A|->0.K)); A23: len f=m & dom f=Seg len f by A5,A22,Th59,FINSEQ_1:def 3; set SN=Seg m\N; deffunc F(Nat)=f/.(Sgm SN.$1)*Line(MV,$1); consider M be FinSequence of (width MV)-tuples_on the carrier of K such that A24: len M= m-'n and A25: for j st j in Seg (m-'n) holds M.j = F(j) from FINSEQ_2:sch 1; reconsider M as FinSequence of the carrier of m-VectSp_over K by A9,MATRIX13:102; reconsider M1=FinS2MX M as Matrix of m-'n,m,K by A24; A26: MV is without_repeated_line by A18,MATRIX13:105; now let i such that A27: i in Seg (m-'n); take a=f/.(Sgm SN.i); thus Line(M1,i) = M1.i by A27,MATRIX_2:10 .= a * Line(MV,i) by A27,A25; end; then consider L be Linear_Combination of lines MV such that A28: L (#) MX2FinS MV = M1 by A26,MATRIX13:108; reconsider SumL=Sum L,f as Element of m-tuples_on the carrier of K by A23,MATRIX13:102,FINSEQ_2:110; now let i such that A29: i in Seg m; A30: SN c= Seg m by XBOOLE_1:36; A31: now per cases; suppose A32: i in N; A33: rng Sgm N=N & dom Sgm N=Seg card N by A1,FINSEQ_1:def 13,FINSEQ_3:45; then consider x such that A34: x in dom Sgm N & Sgm N.x=i by A32,FUNCT_1:def 5; reconsider x as Element of NAT by A34; consider X such that A35: X = ColVec2Mx f and A36: len X = width A & width X=width ColVec2Mx(len A|->0.K)and A37: A * X = ColVec2Mx (len A|->0.K) by A22; A38: ColVec2Mx (len A|->0.K)=0.(K,len A,1) & Indices 0.(K,len A,1)=[:Seg len A,Seg 1:] & 1 in Seg 1 by Th32,A5,A3,MATRIX_1:24; then A39: [x,1] in Indices 0.(K,len A,1)by A1,A33,A34, ZFMISC_1: 106,A5; then A40: 0.K = (ColVec2Mx (len A|->0.K))*(x,1) by A38, MATRIX_3 :3 .= Line(A,x)"*"Col(X,1) by A36,A37,MATRIX_3:def 4,A39,A38 .= Sum(mlt(Line(A,x),Col(X,1))); A41: f = Col(X,1) by A5,A36,A35,Th26; reconsider F=f as Element of (width A)-tuples_on the carrier of K by A3,MATRIX_1:24; set L=Line(A,x); A42: dom mlt(L,F)=Seg m by FINSEQ_2:144,A5; then consider mN,mSN be FinSequence of K such that A43: mN = mlt(L,F)*Sgm N and A44: mSN = mlt(L,F)*Sgm SN and A45: Sum mlt(L,F) = Sum mN + Sum mSN by A1,Lm7; A46: rng Sgm Seg (m-'n)=Seg (m-'n) & rng Sgm SN=SN & dom Sgm SN=Seg card SN by A30,FINSEQ_1:def 13,FINSEQ_3:45; then A47: dom mN=Seg n & dom mSN=Seg (m-'n) by A1,XBOOLE_1:36,A42,A43,A44,A33,A16,RELAT_1:46; then len mSN=m-'n by FINSEQ_1:def 3; then reconsider mSN as Element of (m-'n)-tuples_on the carrier of K by FINSEQ_2:110; A48: width M1=m by A3,MATRIX_1:24; A49: x = (idseq n).x by A1,A3,A34,A33,FINSEQ_2:57 .= Sgm Seg n.x by FINSEQ_3:54; now let j such that A50: j in dom mN & j<>x; A51: Sgm N.j in N by FUNCT_1:def 5,A50,A47,A1,A33; then A52: F.(Sgm N.j)=F/.(Sgm N.j) & L.(Sgm N.j)=A*(x,Sgm N. j) by A1,A23,A5,PARTFUN1:def 8,MATRIX_1:def 8; Indices 1.(K,n)=[:Seg n,Seg n:] by MATRIX_1:25; then A53: [x,j] in Indices 1.(K,n) by ZFMISC_1:106,A50,A1, A34,A47,A33; thus mN.j = mlt(L,F).(Sgm N.j) by A50,A43,FUNCT_1:22 .= F/.(Sgm N.j)*(A*(Sgm Seg n.x,Sgm N.j)) by A51,A49,A1,A5,A52,FVSUM_1:74 .= F/.(Sgm N.j)*(1.(K,n)*(x,j)) by A53,A2,MATRIX13:def 1 .= F/.(Sgm N.j)*0.K by A53,MATRIX_1:def 12,A50 .= 0.K by VECTSP_1:36; end; then A54: Sum mN=mN.x by A1,A34,A47,A33,MATRIX_3:14; A55: Sgm N.x in N by A34,FUNCT_1:def 5,A33; then A56: F.(Sgm N.x)=F/.(Sgm N.x) & L.(Sgm N.x)=A*(x,Sgm N. x) by A1,A23,A5,PARTFUN1:def 8,MATRIX_1:def 8; Indices 1.(K,n)=[:Seg n,Seg n:] by MATRIX_1:25; then A57: [x,x] in Indices 1.(K,n) by ZFMISC_1:106,A33,A34, A1; A58: Sum mN = mlt(L,F).(Sgm N.x) by A54,A43,FUNCT_1:22,A1,A34,A47,A33 .= F/.(Sgm N.x)*(A*(Sgm Seg n.x,Sgm N.x)) by A55,A49,A1,A5,A56,FVSUM_1:74 .= F/.(Sgm N.x)*(1.(K,n)*(x,x)) by A57,A2,MATRIX13:def 1 .= F/.(Sgm N.x)*1_K by A57,MATRIX_1:def 12 .= F/.i by A34,VECTSP_1:def 13 .= f.i by A29,A23,PARTFUN1:def 8; now let j such that A59: j in Seg (m-'n); A60: Line(M1,j) = M1.j by A59,MATRIX_2:10 .= f/.(Sgm SN.j)*Line(MV,j) by A25,A59; A61: j = idseq(m-'n).j by A59,FINSEQ_2:57,A3 .= Sgm Seg (m-'n).j by FINSEQ_3:54; [:Seg (m-'n),N:] c= Indices MV & [j,i] in Indices MV by A9,A1,ZFMISC_1:118,106,A59,A32; then A62: [j,x] in Indices Segm(MV,Seg (m-'n),N) by A61,A46,MATRIX13:17,A34,A33; then A63: [j,x] in Indices (Segm(A,Seg n,SN)@) by A7,Lm1; then A64: [x,j] in Indices Segm(A,Seg n,SN) by MATRIX_1: def 7; A65: x = idseq(n).x by A34,A33,A1,A3,FINSEQ_2:57 .= Sgm Seg n.x by FINSEQ_3:54; A66: Line(MV,j).i = MV*(Sgm Seg (m-'n).j,Sgm N.x) by A9,A34,A61,A29,MATRIX_1:def 8 .= (-Segm(A,Seg n,Seg m \N)@)*(j,x) by A62,A7,MATRIX13:def 1 .= -((Segm(A,Seg n,Seg m \N)@)*(j,x)) by MATRIX_3:def 2,A63 .= -(Segm(A,Seg n,SN)*(x,j)) by MATRIX_1:def 7,A64 .= -(A*(x,Sgm SN.j)) by MATRIX13:def 1,A64,A65; A67: Sgm SN.j in SN by A16,A46,A59,FUNCT_1:def 5; then f/.(Sgm SN.j) = F.(Sgm SN.j) & A*(x,Sgm SN.j) = L.(Sgm SN.j) by A23,PARTFUN1:def 8,A5,A30,MATRIX_1:def 8; then A68: f/.(Sgm SN.j) * (A*(x,Sgm SN.j)) = mlt(L,F).(Sgm SN.j) by A5,A67,FVSUM_1:74,A30 .= mSN.j by A44,A16,A46,A59,FUNCT_1:23; dom M1=Seg (m-'n) by FINSEQ_1:def 3,A24; hence Col(M1,i).j = M1*(j,i) by A59,MATRIX_1:def 9 .= Line(M1,j).i by A48,A29,MATRIX_1:def 8 .= f/.(Sgm SN.j) * (-(A*(x,Sgm SN.j))) by A60,A9,FVSUM_1:63,A32,A1,A66 .= -(f/.(Sgm SN.j) * (A*(x,Sgm SN.j))) by VECTSP_1:40 .= (-mSN).j by FVSUM_1:31,A59,A68; end; then Col(M1,i)=-mSN by A24,FINSEQ_2:139; hence Sum Col(M1,i) = - Sum mSN by FVSUM_1:94 .= -Sum mSN +(Sum mSN+Sum mN) by A45,A40,A41,RLVECT_1:def 7 .= (-Sum mSN+Sum mSN)+Sum mN by RLVECT_1:def 6 .= 0.K+Sum mN by VECTSP_1:66 .= f.i by A58,RLVECT_1:def 7; end; suppose not i in N; then A69: i in SN & rng Sgm SN=SN & dom Sgm SN=Seg card SN by A29,A30,XBOOLE_0:def 4,FINSEQ_1:def 13,FINSEQ_3:45; then consider x such that A70: x in dom Sgm SN & Sgm SN.x=i by FUNCT_1:def 5; reconsider x as Element of NAT by A70; A71: dom Col(M1,i)=Seg len M1 & len M1=m-n & width M1=m & dom M1=Seg len M1 by A3,A16,MATRIX_1:24,FINSEQ_1:def 3, FINSEQ_2:144; A72: now let j such that A73: j in dom Col(M1,i) & x<>j; [j,x] in [:Seg (m-'n),Seg (m-'n):] by ZFMISC_1:106,A69,A70,A71,A73,A16; then A74: [j,x] in Indices 1.(K,m-'n) by MATRIX_1:25; j = idseq (m-'n).j by A3,A71,A73,A16,FINSEQ_2:57 .= Sgm Seg (m-'n).j by FINSEQ_3:54; then A75: Line(MV,j).i = MV*(Sgm Seg (m-'n).j,Sgm SN.x) by A9,A70,A29,MATRIX_1:def 8 .= 1.(K,m-'n)*(j,x) by A74,A6,MATRIX13:def 1 .= 0.K by A74,A73,MATRIX_1:def 12; A76: Line(M1,j) = M1.j by A71,A73,MATRIX_2:10 .= f/.(Sgm SN.j)*Line(MV,j) by A25,A73,A71,A16; thus Col(M1,i).j = M1*(j,i) by A73,A71,MATRIX_1:def 9 .= (f/.(Sgm SN.j)*Line(MV,j)).i by A76,A29,A71,MATRIX_1:def 8 .= (f/.(Sgm SN.j))*0.K by A75,FVSUM_1:63,A29,A9 .= 0.K by VECTSP_1:36; end; [x,x] in [:Seg (m-'n),Seg (m-'n):] by ZFMISC_1:106,A69,A70,A16; then A77: [x,x] in Indices 1.(K,m-'n) by MATRIX_1:25; x = idseq (m-'n).x by A3,A69,A70,A16,FINSEQ_2:57 .= Sgm Seg (m-'n).x by FINSEQ_3:54; then A78: Line(MV,x).i = MV*(Sgm Seg (m-'n).x,Sgm SN.x) by A9,A70,A29,MATRIX_1:def 8 .= 1.(K,m-'n)*(x,x) by A77,A6,MATRIX13:def 1 .= 1_K by A77,MATRIX_1:def 12; A79: Line(M1,x) = M1.x by A69,A70,A16,MATRIX_2:10 .= f/.(Sgm SN.x)*Line(MV,x) by A25,A69,A70,A16; Col(M1,i).x = M1*(x,i) by A16,A69,A70,A71,MATRIX_1:def 9 .= Line(M1,x).i by A29,A71,MATRIX_1:def 8 .= (f/.(Sgm SN.x))*1_K by A78,FVSUM_1:63,A29,A79,A9 .= (f/.i) by A70,VECTSP_1:def 13 .= f.i by A23,A29,PARTFUN1:def 8; hence Sum Col(M1,i)=f.i by A72,MATRIX_3:14,A71,A69,A70,A16; end; end; Carrier L c= lines MV by VECTSP_6:def 7; hence SumL.i=f.i by A31,A29,A28,A18,MATRIX13:105,107; end; then A80: SumL=f by FINSEQ_2:139; the carrier of Lin(lines MV) = {Sum(l) where l is Linear_Combination of lines MV :not contradiction} by VECTSP_7:def 2; hence thesis by A80,A22; end; then the carrier of Lin (lines MV) = the carrier of Space_of_Solutions_of(A) by A15,XBOOLE_0:def 10; hence thesis by A6,A7,A5,VECTSP_4:37; end; Lm8: dim Space_of_Solutions_of 1.(K,n) = 0 proof set ONE=1.(K,n); set SS=Space_of_Solutions_of ONE; A1: the carrier of (0).SS c= the carrier of SS by VECTSP_4:def 2; the carrier of SS c= the carrier of (0).SS proof let x such that A2: x in the carrier of SS; A3: len ONE=n & width ONE=n by MATRIX_1:25; then width ONE=0 implies len ONE=0; then x in Solutions_of(ONE,n|->0.K) by A2,Def5,A3; then consider f such that A4: f=x & ColVec2Mx f in Solutions_of(ONE,ColVec2Mx (n|->0.K)); consider X such that A5: X =ColVec2Mx f & len X = width ONE and width X = width ColVec2Mx (n|->0.K) and A6: ONE * X = ColVec2Mx (n|->0.K) by A4; A7: now per cases; suppose A8: n>0; ONE*X=X by MATRIXR2:68,A3,A5; hence n|->0.K = Col(X,1) by A3,A5,A6,A8,Th26 .= f by A3,A5,A8,Th26; end; suppose n=0; then len f=0 & len (n|->0.K)=0 by A5,A3,MATRIX_1:def 3,FINSEQ_2:69; then f={} & n|->0.K={} by FINSEQ_1:25; hence f=n|->0.K; end; end; 0.SS = 0.((width ONE)-VectSp_over K ) by VECTSP_4:19 .= n|->0.K by MATRIX13:102,A3; then f in {0.SS} by TARSKI:def 1,A7; hence thesis by A4,VECTSP_4:def 3; end; then the carrier of SS = the carrier of (0).SS by A1,XBOOLE_0:def 10; then (0).SS = (Omega).SS by VECTSP_4:37; hence thesis by VECTSP_9:33; end; :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: :: :: The dimension of Space of Solutions of linear equations :: :: :: :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: theorem Th68: for A st ( width A = 0 implies len A = 0 ) holds dim Space_of_Solutions_of A = width A - the_rank_of A proof let A such that A1: width A = 0 implies len A = 0; set L=len A; set W=width A; reconsider A'=A as Matrix of L,W,K by MATRIX_2:7; per cases; suppose A2: the_rank_of A=0; dim ((width A)-VectSp_over K)=width A by MATRIX13:112; hence thesis by A1,A2,Th63; end; suppose A3: the_rank_of A>0; deffunc F(Matrix of L,W,K,Nat,Nat,Element of K) =$1; defpred P[set,set] means for A1 be Matrix of L,W,K st A1=$1 holds Space_of_Solutions_of A'=Space_of_Solutions_of A1; A4: P[A',A']; A5: W>0 by A3,MATRIX13:74; A6: for A1 be Matrix of L,W,K,B1 be Matrix of L,W,K st P[A1,B1] for a be Element of K for i,j st j in dom A1 & (i = j implies a <> -1_K ) holds P[RLine(A1,i,Line(A1,i) + a*Line(A1,j)),F(B1,i,j,a)] proof let A1 be Matrix of L,W,K,B1 be Matrix of L,W,K such that A7: P[A1,B1]; let a be Element of K; let i,j such that A8: j in dom A1 & (i = j implies a <> -1_K ); dom A1 = Seg len A1 by FINSEQ_1:def 3 .= Seg L by MATRIX_1:def 3; then Space_of_Solutions_of RLine(A1,i,Line(A1,i) + a*Line(A1,j)) = Space_of_Solutions_of A1 by A5,A8,Th65 .= Space_of_Solutions_of A' by A7; hence thesis; end; consider A1 be Matrix of L,W,K,B1 be Matrix of L,W,K,N such that A9: N c= Seg W and A10: the_rank_of A' = the_rank_of A1 & the_rank_of A' = card N and A11: P[A1,B1] & Segm(A1,Seg card N,N) = 1.(K,card N) and A12: for i st i in dom A1 & i > card N holds Line(A1,i) = W|->0.K and for i,j st i in Seg card N & j in Seg width A1 & j < Sgm N.i holds A1*(i,j) = 0.K from GAUSS2(A4,A6); card N <= len A1 by A10,MATRIX13:74; then A13: Seg card N c= Seg len A1 & Seg len A1=dom A1 by FINSEQ_1:7,def 3; A14: Seg card N is non empty & card N>0 by FINSEQ_1:5,A3,A10; A15: 00 by A5,MATRIX_1:24,A15; A18: now let i such that A19: i in (dom A1) \ Seg card N; A20: i in dom A1 & not i in Seg card N by A19,XBOOLE_0:def 4; then 1<=i & (i<1 or i > card N) by A13,FINSEQ_1:3; hence Line(A1,i) = width A1 |-> 0.K by A12,A16,A20; end; set SN=Segm(A1,Seg card N,Seg width A1); A21: Space_of_Solutions_of SN = Space_of_Solutions_of A1 by A13,A14,A17,A18,Th66 .= Space_of_Solutions_of A' by A11; A22: card Seg card N=card N & card Seg width A1=W by A16,FINSEQ_1:78; A23: Sgm (Seg card N) = idseq card N by FINSEQ_3:54 .= id Seg card N; A24: Sgm (Seg width A1) = idseq width A1 by FINSEQ_3:54 .= id Seg width A1; Seg card N c= Seg card N; then Seg card N=Sgm (Seg card N)"(Seg card N) & N=Sgm (Seg width A1)"N by FUNCT_2:171,A23,A24,A9,A16; then A25: Segm(SN,Seg card N,N)=1.(K,card N) by A11,MATRIX13:56,A9,A16; A26: card N<=W & card (Seg W\N)=W-card N by A22,A16,NAT_1:44,CARD_2:63,A9; then A27: W-'card N=W-card N by BINARITH:50; per cases; suppose A28: W-'card N=0; then SN=1.(K,card N) by A11,A16,A22,CARD_FIN:1,A9,A27; hence thesis by A28,Lm8,A21,A10,A27; end; suppose A29: W-'card N>0; then consider MVectors be Matrix of W-'card N,W,K such that A30: Segm(MVectors,Seg (W-'card N),Seg W \ N) = 1.(K,W-'card N) and Segm(MVectors,Seg (W-'card N),N)=-Segm(SN,Seg card N,Seg W \N)@ and A31: Lin(lines MVectors) = Space_of_Solutions_of A' by A9,A22,A3,A10,Th67,A25,A21; A32: dom MVectors=Seg len MVectors & len MVectors=W-'card N by MATRIX_1:def 3,FINSEQ_1:def 3; A33: card Seg (W-'card N)=W-'card N by FINSEQ_1:78; A34: Indices MVectors=[:Seg (W-'card N),Seg W:] & len MVectors=W-'card N by A29,MATRIX_1:24; A35: the_rank_of MVectors = W-'card N proof A36: EqSegm(MVectors,Seg (W-'card N),Seg W \ N)=1.(K,W-'card N) by MATRIX13:def 3,A30,A26,A27,FINSEQ_1:78; Seg W \ N c= Seg W by XBOOLE_1:36; then A37: [:Seg (W-'card N),Seg W \ N:] c= Indices MVectors by A34, ZFMISC_1:118; W-'card N+0>0 by A29; then W-'card N>=1 by NAT_1:19; then Det 1.(K,W-'card N)=1_K & 0.K<>1_K by MATRIX_7:16; then W-'card N<=the_rank_of MVectors&W-'card N>=the_rank_of MVectors by A26,A27,A36,A37,A33,A34,MATRIX13:def 4,74; hence thesis by XXREAL_0:1; end; then A38: lines MVectors is linearly-independent by MATRIX13:121; reconsider B=lines MVectors as Subset of W-VectSp_over K; MVectors is without_repeated_line by A35,MATRIX13:105; then Seg (W-'card N),B are_equipotent by A32,WELLORD2:def 4; then Card B = card Seg (W-'card N) by CARD_1:21 .= W-'card N by FINSEQ_1:78; hence thesis by VECTSP_9:30,A31,A10,A27,A38; end; end; end; theorem Th69: for M be Matrix of n,m,K, i,j,a st M is without_repeated_line & j in dom M & (i = j implies a<>-1_K) holds Lin lines M = Lin lines RLine(M,i,Line(M,i)+a*Line(M,j)) proof let M be Matrix of n,m,K, i,j,a such that A1: M is without_repeated_line & j in dom M and A2: i = j implies a<>-1_K; A3: dom M=Seg len M & len M=n by FINSEQ_1:def 3,MATRIX_1:def 3; set L=Line(M,i)+a*Line(M,j); set R=RLine(M,i,L); per cases; suppose not i in dom M; hence thesis by A3,MATRIX13:40; end; suppose A4: i in dom M; reconsider L'=L as Element of (the carrier of K)* by FINSEQ_1:def 11; reconsider LL=L' as set; n<>0 by A3,A4,FINSEQ_1:4; then n>0; then A5: width M=m by MATRIX_1:24; then reconsider Li=Line(M,i),Lj=Line(M,j) as Vector of m -VectSp_over K by MATRIX13:102; set iL={i}-->L'; len L=width M by FINSEQ_2:109; then A6: R = M+*(i,LL) by MATRIX11:29 .= M+*(i.-->LL) by A4,FUNCT_7:def 3 .= M+*iL by FUNCOP_1:def 9; a*Lj=a*Line(M,j) by A5,MATRIX13:102; then A7: L=Li+a*Lj by A5,MATRIX13:102; M.:(dom M\dom iL) = M.:(dom M)\M.:(dom iL) by A1,FUNCT_1:123 .= rng M \ M.:(dom iL) by RELAT_1:146 .= rng M \ Im(M,i) by FUNCOP_1:19 .= rng M \ {M.i} by A4,FUNCT_1:117 .= rng M \ {Line(M,i)} by A4,A3,MATRIX_2:10; then A8: lines R = lines M \ {Line(M,i)} \/rng iL by A6,FRECHET:12 .= lines M \ {Line(M,i)} \/{L} by FUNCOP_1:14; A9: Li in lines M & Lj in lines M by A1,A3,A4,MATRIX13:103; Li = Lj implies (a <> -1_K or Li = 0.(m -VectSp_over K)) proof assume A10: Li=Lj; Li=M.i & Lj=M.j by A1,A3,A4,MATRIX_2:10; hence thesis by A2,A1,A4,A10,FUNCT_1:def 8; end; hence Lin lines R=Lin lines M by A7,A8,A9,Th14; end; end; theorem Th70: for W be Subspace of m-VectSp_over K ex A be Matrix of dim W,m,K, N be without_zero finite Subset of NAT st N c= Seg m & dim W = card N & Segm(A,Seg dim W,N)=1.(K,dim W) & the_rank_of A = dim W & lines A is Basis of W proof let W be Subspace of m-VectSp_over K; consider I be finite Subset of W such that A1: I is Basis of W by VECTSP_9:def 1; A2: card I=dim W & I is linearly-independent & Lin(I) = the VectSpStr of W by A1,VECTSP_9:def 2,VECTSP_7:def 3; then reconsider U=I as linearly-independent Subset of m-VectSp_over K by VECTSP_9:15; consider M be Matrix of card I,m,K such that A3: M is without_repeated_line and A4: lines M = U by MATRIX13:104; deffunc F(Matrix of card I,m,K,Nat,Nat,Element of K) = $1; defpred P[set,set] means for A be Matrix of card I,m,K,B be Matrix of card I,m,K st $1=A holds A is without_repeated_line & lines A is linearly-independent & Lin(lines A)=(Omega).W; A5: P[M,M] by A2,VECTSP_9:21,A3,A4; A6: for A' be Matrix of card I,m,K, B' be Matrix of card I,m,K st P[A',B'] for a be Element of K for i,j st j in dom A' & (i=j implies a<>-1_K) holds P[RLine(A',i,Line(A',i) + a*Line(A',j)),F(B',i,j,a)] proof let A' be Matrix of card I,m,K, B' be Matrix of card I,m,K such that A7: P[A',B']; let a be Element of K; let i,j such that A8: j in dom A' & (i = j implies a <> -1_K ); set R=RLine(A',i,Line(A',i) + a*Line(A',j)); A9: dom A'=Seg len A' by FINSEQ_1:def 3; A10: A' is without_repeated_line&lines A' is linearly-independent by A7; then A11: Lin lines A'= Lin lines R by Th69,A8; card I = the_rank_of A' by A10,MATRIX13:121 .= the_rank_of R by A8,A9,MATRIX13:92; hence thesis by A7,A11,MATRIX13:121; end; consider A' be Matrix of card I,m,K, B' be Matrix of card I,m,K,N such that A12: N c= Seg m and A13: the_rank_of M = the_rank_of A' & the_rank_of M = card N & P[A',B'] and A14: Segm(A',Seg card N,N) = 1.(K,card N) and for i st i in dom A' & i > card N holds Line(A',i) = m|->0.K and for i,j st i in Seg card N & j in Seg width A' & j < Sgm N.i holds A'*(i,j) = 0.K from GAUSS2(A5,A6); reconsider A' as Matrix of dim W,m,K by A1,VECTSP_9:def 2; take A',N; A15: the_rank_of M = card I & lines A' is linearly-independent & Lin(lines A') = the VectSpStr of W by A13,A3,A4,MATRIX13:121; lines A' c= the carrier of Lin(lines A') proof let x such that A16: x in lines A'; x in Lin(lines A') by A16,VECTSP_7:13; hence thesis by STRUCT_0:def 5; end; then reconsider lA=lines A' as linearly-independent Subset of W by A15,VECTSP_9:16; Lin(lA) = Lin(lines A') by VECTSP_9:21; hence thesis by A2,A12,A13,A14,A15,VECTSP_7:def 3; end; theorem for W be strict Subspace of m-VectSp_over K st dim W < m ex A be Matrix of m-'dim W,m,K, N be without_zero finite Subset of NAT st card N = m-'dim W & N c= Seg m & Segm(A,Seg(m-'dim W),N) = 1.(K,m-'dim W) & W = Space_of_Solutions_of A proof let W be strict Subspace of m-VectSp_over K such that A1: dim W < m; per cases; suppose A2: dim W=0; then reconsider ONE=1.(K,m) as Matrix of m-'dim W,m,K by BINARITH:58; A3: m-'dim W=m by A2,BINARITH:58; take ONE,N=Seg m; A4: len 1.(K,m)=m & width 1.(K,m)=m & card N=m by FINSEQ_1:78,MATRIX_1:25; A5: dim Space_of_Solutions_of ONE=0 by Lm8; Space_of_Solutions_of ONE = (Omega).(Space_of_Solutions_of ONE) .= (0).(Space_of_Solutions_of ONE) by VECTSP_9:33,A5 .= (0).W by A4,VECTSP_4:48 .= (Omega).W by A2,VECTSP_9:33 .= W; hence thesis by A4,A3,MATRIX13:46; end; suppose A6: dim W > 0; consider A be Matrix of dim W,m,K, N such that A7: N c= Seg m & dim W = card N and A8: Segm(A,Seg dim W,N)=1.(K,dim W) and A9: the_rank_of A = dim W & lines A is Basis of W by Th70; set ZERO=0.(K,m-'dim W,m); A10: m-'dim W=m-dim W & m-dim W>dim W-dim W by A1,BINARITH:50,XREAL_1:11; then A11: len ZERO=m-'dim W & width ZERO=m&Indices ZERO=[:Seg (m-'dim W ), Seg m:] & card Seg (m-'dim W)=m-'dim W by MATRIX_1:24,FINSEQ_1:78; set SA = Segm(A,Seg dim W,(Seg m)\N); A12: card ((Seg m)\N) = card Seg m-card N & card Seg (m-'dim W)=m-'dim W & card Seg dim W=dim W & card Seg m = m by A7,CARD_2:63,FINSEQ_1:78; then reconsider CC=1.(K,m-'dim W) as Matrix of card Seg(m-'dim W),card((Seg m)\N),K by A1,BINARITH:50,A7; len SA=dim W & width SA =m-card N by A6,A12,MATRIX_1:24; then len (SA@)=m-dim W & width (SA@) =dim W by A7,A10,MATRIX_2:12; then len (-SA@)=m-'dim W & width (-SA@) =dim W by A10,MATRIX_3:def 2; then reconsider BB=-SA@ as Matrix of card Seg (m-'dim W),card N,K by A7,A12,MATRIX_2:7; A13: (Seg m)\N c= Seg m by XBOOLE_1:36; then A14: [:Seg (m-'dim W),N:] c= Indices ZERO & Seg m\((Seg m)\N) = Seg m /\N & [:Seg (m-'dim W),(Seg m)\N:] c= Indices ZERO & Seg m /\ N =N by A11,A7,ZFMISC_1:118,XBOOLE_1:48,28; A15: N misses (Seg m)\N by XBOOLE_1:79; [:Seg (m-'dim W),N:]/\[:Seg (m-'dim W),(Seg m)\N:]= [:Seg (m-'dim W),N/\((Seg m)\N):] by ZFMISC_1:122 .= [:Seg (m-'dim W),{}:] by A15,XBOOLE_0:def 7 .= {} by ZFMISC_1:113; then for i,j,bi,bj,ci,cj be Nat st [i,j] in [:Seg (m-'dim W),N:]/\[:Seg (m-'dim W),(Seg m)\N:] & bi=Sgm Seg(m-'dim W)".i & bj=Sgm N".j & ci=Sgm Seg(m-'dim W)".i& cj=Sgm ((Seg m)\N)".j holds BB*(bi,bj) = CC*(ci,cj); then consider M be Matrix of m-'dim W,m,K such that A16: Segm(M,Seg (m-'dim W),N)=BB & Segm(M,Seg (m-'dim W),(Seg m)\N)=CC and for i,j st [i,j] in Indices M\([:Seg (m-'dim W),N:]\/[:Seg (m-'dim W),(Seg m)\N:]) holds M*(i,j) = ZERO*(i,j) by Th9,A11,A14; m-'(m-'dim W)=m-(m-'dim W) by BINARITH:50,52; then consider MV be Matrix of dim W,m,K such that A17: Segm(MV,Seg dim W,N) = 1.(K,dim W) and A18: Segm(MV,Seg dim W,(Seg m)\N)= -Segm(M,Seg (m-'dim W),N)@ and A19: Lin(lines MV) = Space_of_Solutions_of M by A6,A7,A10,A12,A14,A16,A13,Th67; A20: now let i,j such that A21: [i,j] in Indices A; A22: Indices A=[:Seg dim W, Seg m:] & Indices A=Indices MV by A6,MATRIX_1:24,27; then A23: i in Seg dim W & rng Sgm Seg dim W=Seg dim W & dom Sgm Seg dim W=Seg dim W & j in Seg m by ZFMISC_1:106,A21,FINSEQ_1:def 13,FINSEQ_3:45,A12; then consider x such that A24: x in Seg dim W & (Sgm Seg dim W).x=i by FUNCT_1:def 5; reconsider x as Element of NAT by A24; now per cases; suppose A25: j in N; A26: rng Sgm N=N & dom Sgm N=Seg dim W by A7,FINSEQ_1:def 13,FINSEQ_3:45; then consider y such that A27: y in Seg dim W & (Sgm N).y=j by A25,FUNCT_1:def 5; reconsider y as Element of NAT by A27; [:Seg dim W,N:] c= Indices A & [i,j] in [:Seg dim W,N:] by A7,A22,A23,A25,ZFMISC_1:106,118; then A28: [x,y] in Indices Segm(A,Seg dim W,N) & [x,y] in Indices Segm(MV,Seg dim W,N) by A22,A23,A24,A26,A27,MATRIX13:17; hence A*(i,j) = Segm(MV,Seg dim W,N)*(x,y) by A8,A24,A27,A17,MATRIX13:def 1 .= MV*(i,j) by A24,A27,MATRIX13:def 1,A28; end; suppose not j in N; then A29: j in Seg m\N by A23,XBOOLE_0:def 4; A30: rng Sgm (Seg m\N)=(Seg m\N) & dom Sgm(Seg m\N)=Seg(m-'dim W) by A7,FINSEQ_1:def 13,FINSEQ_3:45,A12,A13,A10; then consider y such that A31: y in Seg (m-'dim W) & (Sgm (Seg m\N)).y=j by A29,FUNCT_1:def 5; reconsider y as Element of NAT by A31; [:Seg dim W,Seg m\N:] c= Indices A & [i,j] in [:Seg dim W,Seg m\N:] by A22,A23,A29,A13,ZFMISC_1:106,118; then A32: [x,y] in Indices Segm(A,Seg dim W,Seg m\N) & [x,y] in Indices Segm(MV,Seg dim W,Seg m\N) by A22,A23,A24,A30,A31,MATRIX13:17; then A33: [x,y] in Indices (Segm(M,Seg (m-'dim W),N)@) by A18, Lm1; then A34: [y,x] in Indices Segm(M,Seg (m-'dim W),N) by MATRIX_1: def 7; then A35: [y,x] in Indices SA@ by Lm1,A16; thus MV*(i,j) = (-Segm(M,Seg (m-'dim W),N)@)*(x,y) by A24,A31,MATRIX13:def 1,A32,A18 .= -(Segm(M,Seg (m-'dim W),N)@)*(x,y) by A33,MATRIX_3:def 2 .= -(-SA@)*(y,x) by A16,A34,MATRIX_1:def 7 .= --(SA@)*(y,x) by A35,MATRIX_3:def 2 .= (SA@)*(y,x) by RLVECT_1:30 .= SA*(x,y) by A32,MATRIX_1:def 7 .=A*(i,j) by A24,A31,MATRIX13:def 1,A32; end; end; hence A*(i,j)=MV*(i,j); end; take M,NN=Seg m\ N; reconsider lA=lines MV as Subset of W by A9,A20,MATRIX_1:28; MV = A by A20,MATRIX_1:28; then Lin(lA) = the VectSpStr of W by VECTSP_7:def 3,A9; hence thesis by XBOOLE_1:36,A16,A19,VECTSP_9:21,A7,A1,BINARITH:50,A12; end; end; theorem Th72: for A,B be Matrix of K st width A = len B & ( width A = 0 implies len A = 0 ) & ( width B = 0 implies len B = 0 ) holds Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A*B) proof let A,B be Matrix of K such that A1: width A = len B and A2: width A = 0 implies len A = 0 and A3: width B = 0 implies len B = 0; set AB=A*B; A4: len AB=len A & width AB=width B by A1,MATRIX_3:def 4; then reconsider AB as Matrix of len A,width B,K by MATRIX_2:7; the carrier of Space_of_Solutions_of B c= the carrier of Space_of_Solutions_of AB proof let x such that A5: x in the carrier of Space_of_Solutions_of B; x in Solutions_of(B,len B|->0.K) by A5,A3,Def5; then consider f such that A6: f=x & ColVec2Mx f in Solutions_of(B,ColVec2Mx (len B|->0.K)); consider X such that A7: X=ColVec2Mx f & len X = width B and A8: width X = width ColVec2Mx (len B|->0.K) and A9: B * X = ColVec2Mx (len B|->0.K) by A6; A10: ColVec2Mx (len B|->0.K)=0.(K,len B,1) & ColVec2Mx (len AB|->0.K)=0.(K,len A,1) by A4,Th32; now per cases; suppose len A=0; then A11: Solutions_of(AB,ColVec2Mx (len AB|->0.K)) ={{}} & len X=0 by Th51,A4,A7,A10,MATRIX_1:def 4; then X ={} by FINSEQ_1:25; hence X in Solutions_of(AB,ColVec2Mx (len AB|->0.K)) by TARSKI:def 1,A11; end; suppose A12: len A<>0; then len A>0 & width A>0 by A2; then A13: ColVec2Mx (len AB|->0.K) = A*(B*X) by A1,A9,A10,MATRIXR2: 18 .= AB*X by MATRIX_3:35,A1,A7; A14: len (len AB|->0.K)=len AB & len (len B|->0.K)=len B by FINSEQ_2:69; then width ColVec2Mx (len AB|->0.K)=1 by Th26,A12,A4 .= width ColVec2Mx (len B|->0.K) by Th26,A12,A2,A1,A14; hence X in Solutions_of(AB,ColVec2Mx (len AB|->0.K)) by A4,A7,A8,A13; end; end; then f in Solutions_of(AB,len AB|->0.K) by A7; hence thesis by Def5,A1,A2,A3,A4,A6; end; hence thesis by A4,VECTSP_4:35; end; theorem for A,B be Matrix of K st width A = len B holds the_rank_of (A*B) <= the_rank_of A & the_rank_of (A*B) <= the_rank_of B proof let A,B be Matrix of K such that A1: width A = len B; set AB=A*B; A2: len AB=len A & width AB=width B by A1,MATRIX_3:def 4; per cases; suppose the_rank_of AB=0; hence thesis; end; suppose the_rank_of AB>0; then A3: len AB>0 & width AB>0 by MATRIX13:74; then (width A=0 implies len A=0) & (width B=0 implies len B=0) by A1,A2,MATRIX_1:def 4; then Space_of_Solutions_of B is Subspace of Space_of_Solutions_of AB & dim Space_of_Solutions_of B = width B-the_rank_of B & dim Space_of_Solutions_of AB=width AB-the_rank_of AB by A1,A2,Th72,Th68; then A4: width B-the_rank_of B <= width B-the_rank_of AB by A2, VECTSP_9:29; set AT=A@; set BT=B@; set BA=BT*AT; width A>0 by A1,A3,A2,MATRIX_1:def 4; then A5: width AT=len A & len AT=width A & width BT=len B & len BT= width B by A2,A3,MATRIX_2:12; then A6: len BA=len BT & width BA=width AT & BA=AB@ by A1,A2,A3,MATRIX_3: def 4,24; ( width AT = 0 implies len AT = 0 ) & ( width BT = 0 implies len BT = 0 ) & width BT=len AT by A1,MATRIX_1:def 4,A5; then Space_of_Solutions_of AT is Subspace of Space_of_Solutions_of BA & dim Space_of_Solutions_of AT = width AT - the_rank_of AT & dim Space_of_Solutions_of BA = width BA - the_rank_of BA by Th72,Th68,A6; then width AT - the_rank_of AT<=width AT - the_rank_of BA by VECTSP_9:29,A6; then the_rank_of AT >= the_rank_of BA by XREAL_1:12; then the_rank_of A >= the_rank_of BA by MATRIX13:84; hence thesis by A4,XREAL_1:12,A6,MATRIX13:84; end; end; theorem Th74: for A be Matrix of n,n,K, B be Matrix of K st Det A <> 0.K & width A = len B & ( width B = 0 implies len B = 0 ) holds Space_of_Solutions_of B = Space_of_Solutions_of (A*B) proof let A be Matrix of n,n,K,B be Matrix of K such that A1: Det A <> 0.K & width A=len B and A2: width B = 0 implies len B = 0; set AB=A*B; A3: len A=n & width A=n by MATRIX_1:25; A4: len AB=len A & width AB=width B by A1,MATRIX_3:def 4; then reconsider AB as Matrix of n,width B,K by A3,MATRIX_2:7; A5: width A=0 implies len A=0 by A3; A6: the carrier of Space_of_Solutions_of AB c= the carrier of Space_of_Solutions_of B proof let x such that A7: x in the carrier of Space_of_Solutions_of AB; x in Solutions_of(AB,len AB|->0.K) by A1,A2,A7,A4,A3,Def5; then consider f such that A8: f=x & ColVec2Mx f in Solutions_of(AB,ColVec2Mx (len AB|->0.K)); consider X such that A9: X=ColVec2Mx f & len X = width AB and A10: width X = width ColVec2Mx (len AB|->0.K) and A11: AB * X = ColVec2Mx (len AB|->0.K) by A8; set BX=B*X; A is invertible by A1,LAPLACE:34; then A is_reverse_of A~ by MATRIX_6:def 4; then A12: 1.(K,n)=A~*A by MATRIX_6:def 2; A13: len (A~)=n & width (A~)=n by MATRIX_1:25; A14: len BX=len B by A4,A9,MATRIX_3:def 4; then A15: BX = 1.(K,n)* BX by A1,MATRIXR2:68,A3 .= A~ * (A*BX) by A1,A3,MATRIX_3:35,A12,A13,A14 .= A~ * ColVec2Mx(len AB|->0.K) by A1,A4,A9,A11,MATRIX_3:35 .= A~ * 0.(K,len AB,1) by Th32; now per cases; suppose A16: n = 0; len (0.(K,len AB,1))=width (A~) by A3,A4,A13,MATRIX_1:def 3; then BX={} & 0.(K,len AB,1)={} by A1,FINSEQ_1:28,A3,A13,A14,A16; hence BX=0.(K,len AB,1); end; suppose n>0; hence BX=0.(K,len AB,1) by MATRIXR2:18,A3,A4,A13,A15; end; end; then BX =ColVec2Mx(len AB|->0.K) by Th32; then ColVec2Mx f in Solutions_of(B,ColVec2Mx(len B|->0.K)) by A1,A3,A4,A9,A10; then f in Solutions_of(B,len B|->0.K); hence thesis by A2,A8,Def5; end; Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A*B) by A1,A2,A5,Th72; then the carrier of Space_of_Solutions_of B c= the carrier of Space_of_Solutions_of (A*B) by VECTSP_4:def 2; then the carrier of Space_of_Solutions_of B = the carrier of Space_of_Solutions_of (A*B) by A6,XBOOLE_0:def 10; hence thesis by A4, VECTSP_4:37; end; theorem Th75: for A be Matrix of n,n,K, B be Matrix of K st width A = len B & Det A <> 0.K holds the_rank_of (A*B) = the_rank_of B proof let A be Matrix of n,n,K, B be Matrix of K such that A1: width A = len B & Det A <>0.K; set AB=A*B; A2: len AB=len A & width AB=width B & len A=n & width A=n & len A=n by A1,MATRIX_3:def 4,MATRIX_1:25; per cases; suppose width AB=0; hence thesis by A1,A2,Lm3; end; suppose A3: width AB>0; then Space_of_Solutions_of B = Space_of_Solutions_of AB by A2,A1,Th74; then Space_of_Solutions_of B is Subspace of Space_of_Solutions_of AB & Space_of_Solutions_of AB is Subspace of Space_of_Solutions_of B & dim Space_of_Solutions_of B = width B-the_rank_of B & dim Space_of_Solutions_of AB = width AB-the_rank_of AB by A2,A3,Th68,VECTSP_4:32; then width B-the_rank_of B <= width B-the_rank_of AB & width B-the_rank_of B >= width B-the_rank_of AB by A2,VECTSP_9:29; then width B-the_rank_of B=width B-the_rank_of AB by XXREAL_0:1; hence thesis; end; end; theorem for A be Matrix of n,n,K, B be Matrix of K st len A = width B & Det A <> 0.K holds the_rank_of (B*A) = the_rank_of B proof let A be Matrix of n,n,K,B be Matrix of K such that A1: width B = len A & Det A <> 0.K; set BA=B*A; A2: len BA=len B & width BA=width A & len A=n & width A=n by A1,MATRIX_1:25,MATRIX_3:def 4; per cases; suppose width BA=0; hence thesis by A1,A2,Lm3; end; suppose A3: width BA>0; then A4: Det (A@)<>0.K & width (A@)=len A & len (B@)=width B by A1,A2,MATRIX_2:12,MATRIXR2:43; thus the_rank_of (B*A) = the_rank_of ((B*A)@) by MATRIX13:84 .= the_rank_of ((A@)*(B@)) by A1,A2,A3,MATRIX_3:24 .= the_rank_of (B@) by A1,A4,Th75 .= the_rank_of B by MATRIX13:84; end; end;