:: 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, QC_LANG1, ROUGHS_1, GR_CY_1, FREEALG, 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, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, FINSEQOP, MATRIX13, MATRLIN, FUNCT_7, PNPROC_1, LAPLACE; constructors SETWISEO, FINSOP_1, ALGSTR_1, FVSUM_1, XXREAL_0, GROUP_4, FINSEQ_7, WELLORD2, VECTSP_6, VECTSP_7, VECTSP_9, MATRIX_6, MATRIX_7, MATRIX11, MATRIX13, PNPROC_1, REALSET1, LAPLACE, BINOP_2; registrations XBOOLE_0, FUNCT_1, FINSET_1, STRUCT_0, FVSUM_1, 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; 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; 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; 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; hence thesis by FINSEQ_3:49; 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 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; 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; 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; 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; 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; 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; 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; 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; 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; 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; 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,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) = {}; 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; 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 .= Col(C,j).i by A2,A3,Th26 .= 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) 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,CARD_2:83; 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,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; 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; 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 = {}; 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 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; 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; 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; hence thesis by TARSKI:def 1; end; len (A*A)=0 by A1,A2,MATRIX_3:def 4; then A*A={}; 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={}; 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; 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; end; hence thesis by XBOOLE_1:2; 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 RA=RLine(A',len f+1,LAf + 1_K()*LA); 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; 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 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; 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=wid