:: Solutions of Linear Equations :: by Karol P\c{a}k :: :: Received December 18, 2007 :: Copyright (c) 2007-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, VECTSP_1, FREEALG, FINSET_1, SUBSET_1, MATRIX_1, TREES_1, FINSEQ_1, RELAT_1, XXREAL_0, INCSP_1, FVSUM_1, CARD_3, RVSUM_1, GROUP_1, ARYTM_1, SUPINF_2, FUNCT_1, ARYTM_3, CARD_1, XBOOLE_0, ALGSTR_0, ORDINAL4, STRUCT_0, FINSEQ_2, TARSKI, RLVECT_1, PARTFUN1, VALUED_1, ZFMISC_1, CLASSES1, XCMPLX_0, MATRIX_3, MATRIX13, LAPLACE, PRVECT_1, RLVECT_3, LMOD_7, QC_LANG1, RLSUB_1, MESFUNC1, PRE_POLY, MATRIX11, MATRIXR1, AFINSQ_1, FINSEQ_3, FUNCT_2, SETWISEO, FINSOP_1, RLVECT_2, RLVECT_5, FUNCOP_1, FUNCT_4, MATRIX_6, MATRIX15; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, NAT_1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, SETWOP_2, FINSEQ_1, STRUCT_0, FUNCOP_1, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_2, MATRIX_0, MATRIX_1, FVSUM_1, FINSOP_1, NAT_D, GROUP_4, MATRIX_3, MATRIX_6, MATRIX_7, FINSEQ_7, FUNCT_4, DOMAIN_1, MATRIX11, MEASURE6, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, PRVECT_1, MATRIX13, PRE_POLY, MATRLIN, FUNCT_7, PNPROC_1, LAPLACE; constructors SETWISEO, FINSOP_1, ALGSTR_1, FVSUM_1, GROUP_4, FINSEQ_7, WELLORD2, VECTSP_6, VECTSP_7, VECTSP_9, MATRIX_6, MATRIX_7, MATRIX11, MATRIX13, PNPROC_1, REALSET1, LAPLACE, BINARITH, RELSET_1; registrations 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, MATRLIN, MATRIX13, XREAL_0, VECTSP_9, VALUED_0, RELSET_1, PRVECT_1, MATRIX_0, MATRIX_1; requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET; definitions TARSKI, XBOOLE_0, MATRIX_1; equalities XBOOLE_0, FINSEQ_1, FINSEQ_2, MATRIX_0, GROUP_4, MATRIX_3, VECTSP_4, RELAT_1, LAPLACE, MATRIX13, FVSUM_1, ALGSTR_0, CARD_1, ORDINAL1; expansions TARSKI, XBOOLE_0, FINSEQ_1, MATRIX_1; theorems CARD_1, CARD_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQOP, FINSOP_1, FRECHET, FUNCT_1, FUNCT_2, FUNCT_7, FUNCOP_1, FVSUM_1, GROUP_1, LAPLACE, MATRIX_0, MATRIX_3, MATRIX_4, MATRIX_5, MATRIX_6, MATRIX_7, MATRIX11, MATRIX13, MATRIXR1, MATRIXR2, MATRLIN, NAT_1, ORDINAL1, PARTFUN1, RELAT_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, NAT_D, PRE_POLY, MEASURE6, MATRIX_1, VALUED_1; schemes FINSEQ_2, NAT_1, MATRIX_0; 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), A9 for (Matrix of m,n,K), B9 for (Matrix of m,k,K); theorem Th1: width A = len B implies (a*A) * B = a * (A*B) proof set aA=a*A; set AB=A*B; set aAB=a*AB; assume A1: width A=len B; then A2: width AB=width B by MATRIX_3:def 4; A3: len aAB=len AB by MATRIX_3:def 5; then A4: len aAB = len A by A1,MATRIX_3:def 4; A5: width aA=width A by MATRIX_3:def 5; then A6: len aA=len A & len aA=len (aA*B) by A1,MATRIX_3:def 4,def 5; A7: now let i,j; assume [i,j] in Indices aAB; then A8: [i,j] in Indices AB by MATRIXR1:18; then i in dom AB by ZFMISC_1:87; then i in Seg len A by A3,A4,FINSEQ_1:def 3; then A9: 1<=i & i<=len A by FINSEQ_1:1; dom AB = Seg len AB by FINSEQ_1:def 3 .= dom (aA*B) by A3,A4,A6,FINSEQ_1:def 3; then A10: [i,j] in Indices (aA*B) by A1,A5,A2,A8,MATRIX_3:def 4; thus aAB*(i,j) = a*(AB*(i,j)) by A8,MATRIX_3:def 5 .= a*(Line(A,i)"*"Col(B,j)) by A1,A8,MATRIX_3:def 4 .= Sum(a*mlt(Line(A,i),Col(B,j))) by FVSUM_1:73 .= Sum(mlt(a*Line(A,i),Col(B,j))) by A1,FVSUM_1:68 .= Line(aA,i)"*"Col(B,j) by A9,MATRIXR1:20 .= (aA*B)*(i,j) by A1,A5,A10,MATRIX_3:def 4; end; width aAB=width AB & width B=width (aA*B) by A1,A5,MATRIX_3:def 4,def 5; hence thesis by A2,A4,A6,A7,MATRIX_0: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: now let i,j such that A2: [i,j] in Indices A; thus A*(i,j) = 1_K*(A*(i,j)) .= 1A*(i,j) by A2,MATRIX_3:def 5; end; A3: len(a*bA) = len bA by MATRIX_3:def 5 .= len A by MATRIX_3:def 5 .= len abA by MATRIX_3:def 5; A4: now A5: Indices bA=Indices A by MATRIXR1:18; A6: Indices (a*bA)=Indices bA by MATRIXR1:18; let i,j such that A7: [i,j] in Indices (a*bA); thus (a*bA)*(i,j) = a*(bA*(i,j)) by A7,A6,MATRIX_3:def 5 .= a*(b*(A*(i,j))) by A7,A6,A5,MATRIX_3:def 5 .= (a*b)*(A*(i,j)) by GROUP_1:def 3 .= abA*(i,j) by A7,A6,A5,MATRIX_3:def 5; end; A8: width(a*bA) = width bA by MATRIX_3:def 5 .= width A by MATRIX_3:def 5 .= width abA by MATRIX_3:def 5; len 1A=len A & width 1A=width A by MATRIX_3:def 5; hence thesis by A1,A3,A8,A4,MATRIX_0: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 defpred P[Nat] means for n st n=$1 holds power(K).(a,n)<>0.K; assume A1: a<>0.K; A2: for k st P[k] holds P[k+1] proof let k; assume P[k]; then A3: power(K).(a,k) <> 0.K; let n; assume n=k+1; then power(K).(a,n)=power(K).(a,k) * a by GROUP_1:def 7; hence thesis by A1,A3,VECTSP_1:12; end; A4: P[0] proof A5: 1_K<>0.K; let n; assume n=0; hence thesis by A5,GROUP_1:def 7; end; for k holds P[k] from NAT_1:sch 2(A4,A2); 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 and A2: len h = len w; set KK=the carrier of K; reconsider H=h,W=w as Element of (len h)-tuples_on KK by A2,FINSEQ_2:92; reconsider F=f,G=g as Element of (len f)-tuples_on KK by A1,FINSEQ_2:92; reconsider FH=F^H,GW=G^W,Th36W=(F+G)^(H+W) as Tuple of len f+len h, KK; reconsider FH,GW,Th36W as Element of (len f+len h) -tuples_on KK by FINSEQ_2:131; now let i such that A3: i in Seg (len f+len h); A4: i in dom FH by A3,FINSEQ_2:124; now per cases by A4,FINSEQ_1:25; suppose A5: i in dom f; A6: rng f c= KK & rng g c= KK by RELAT_1:def 19; A7: dom (F+G)=Seg len f by FINSEQ_2:124; A8: f.i in rng f by A5,FUNCT_1:def 3; A9: dom F=Seg len f by FINSEQ_2:124; A10: dom G=Seg len f by FINSEQ_2:124; then g.i in rng g by A5,A9,FUNCT_1:def 3; then reconsider fi=f.i,gi=g.i as Element of K by A8,A6; A11: FH.i=fi by A5,FINSEQ_1:def 7; GW.i=gi by A5,A9,A10,FINSEQ_1:def 7; hence (FH+GW).i = fi+gi by A3,A11,FVSUM_1:18 .= (F+G).i by A5,A9,FVSUM_1:18 .= Th36W.i by A5,A9,A7,FINSEQ_1:def 7; end; suppose ex n st n in dom h & i=len f + n; then consider n such that A12: n in dom h and A13: i=len f + n; A14: h.n in rng h by A12,FUNCT_1:def 3; A15: rng h c= KK & rng w c= KK by RELAT_1:def 19; A16: dom H=Seg len h by FINSEQ_2:124; A17: dom W=Seg len h by FINSEQ_2:124; then w.n in rng w by A12,A16,FUNCT_1:def 3; then reconsider hn=h.n,wn=w.n as Element of K by A14,A15; A18: FH.i=hn by A12,A13,FINSEQ_1:def 7; A19: dom (H+W)=Seg len h & len (F+G)=len f by CARD_1:def 7,FINSEQ_2:124; GW.i=wn by A1,A12,A13,A16,A17,FINSEQ_1:def 7; hence (FH+GW).i = hn+wn by A3,A18,FVSUM_1:18 .= (H+W).n by A12,A16,FVSUM_1:18 .= Th36W.i by A12,A13,A16,A19,FINSEQ_1:def 7; end; end; hence (FH+GW).i=Th36W.i; end; hence thesis by FINSEQ_2:119; 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:92; reconsider G=g as Element of (len g)-tuples_on KK by FINSEQ_2:92; reconsider FG=F^G,aFaG=(a*F)^(a*G) as Element of (len f+len g)-tuples_on KK by FINSEQ_2:131; now let i such that A1: i in Seg (len f+len g); A2: i in dom FG by A1,FINSEQ_2:124; now per cases by A2,FINSEQ_1:25; suppose A3: i in dom f; A4: rng f c= KK by RELAT_1:def 19; f.i in rng f by A3,FUNCT_1:def 3; then reconsider fi=f.i as Element of K by A4; A5: dom F=Seg len f by FINSEQ_2:124; A6: dom (a*F)=Seg len f by FINSEQ_2:124; FG.i=fi by A3,FINSEQ_1:def 7; hence (a*FG).i = a*fi by A1,FVSUM_1:51 .= (a*F).i by A3,A5,FVSUM_1:51 .= aFaG.i by A3,A5,A6,FINSEQ_1:def 7; end; suppose A7: ex n st n in dom g & i=len f + n; A8: rng g c= KK by RELAT_1:def 19; A9: dom (a*G)=Seg len g & len (a*F)=len f by CARD_1:def 7,FINSEQ_2:124; consider n such that A10: n in dom g and A11: i=len f + n by A7; g.n in rng g by A10,FUNCT_1:def 3; then reconsider gn=g.n as Element of K by A8; A12: dom G=Seg len g by FINSEQ_2:124; FG.i=gn by A10,A11,FINSEQ_1:def 7; hence (a*FG).i = a*gn by A1,FVSUM_1:51 .= (a*G).n by A10,A12,FVSUM_1:51 .= aFaG.i by A10,A11,A12,A9,FINSEQ_1:def 7; end; end; hence (a*FG).i=aFaG.i; end; hence thesis by FINSEQ_2:119; 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 and A2: rng p2 c= dom f and A3: f1=f*p1 and A4: f2=f*p2; A5: dom (p1^p2)=Seg (len p1+len p2) by FINSEQ_1:def 7; rng (p1^p2) = rng p1 \/rng p2 by FINSEQ_1:31; then A6: dom (f*(p1^p2))=dom (p1^p2) by A1,A2,RELAT_1:27,XBOOLE_1:8; A7: dom f1=dom p1 by A1,A3,RELAT_1:27; then A8: len f1=len p1 by FINSEQ_3:29; A9: dom f2=dom p2 by A2,A4,RELAT_1:27; then len f2=len p2 by FINSEQ_3:29; then A10: dom (f1^f2)=dom (f*(p1^p2)) by A6,A8,A5,FINSEQ_1:def 7; now let x be object such that A11: x in dom (f1^f2); reconsider i=x as Element of NAT by A11; now per cases; suppose A12: i in dom p1; hence (f1^f2).i = f1.i by A7,FINSEQ_1:def 7 .= f.(p1.i) by A3,A7,A12,FUNCT_1:12 .= f.((p1^p2).i) by A12,FINSEQ_1:def 7 .= (f*(p1^p2)).i by A10,A11,FUNCT_1:12; end; suppose not i in dom p1; then consider n such that A13: n in dom p2 and A14: i=len p1 + n by A7,A9,A8,A11,FINSEQ_1:25; thus (f1^f2).i = f2.n by A9,A8,A13,A14,FINSEQ_1:def 7 .= f.(p2.n) by A4,A9,A13,FUNCT_1:12 .= f.((p1^p2).i) by A13,A14,FINSEQ_1:def 7 .= (f*(p1^p2)).i by A10,A11,FUNCT_1:12; end; end; hence (f1^f2).x = (f*(p1^p2)).x; end; hence thesis by A10,FUNCT_1:2; 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 and f is one-to-one and 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:43; 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 and A6: rng f c= Seg k and A7: f is one-to-one and A8: for i,j st i in dom f & j in dom f & i < j holds f.i < f.j; set fn=f|n; A9: f=fn^<*f.n1*> by A5,FINSEQ_3:55; then A10: rng fn c= rng f by FINSEQ_1:29; A11: dom fn c= dom f by A9,FINSEQ_1:26; A12: 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 A13: i in dom fn & j in dom fn and A14: i < j; fn.i=f.i & fn.j=f.j by A9,A13,FINSEQ_1:def 7; hence thesis by A8,A11,A13,A14; end; A15: len fn =n by A5,FINSEQ_3:53; A16: now A17: n1 in Seg n1 & dom f=Seg n1 by A5,FINSEQ_1:4,def 3; let m9,n9 being Nat such that A18: m9 in rng fn and A19: n9 in {f.n1}; consider x being object such that A20: x in dom fn and A21: fn.x=m9 by A18,FUNCT_1:def 3; reconsider x as Element of NAT by A20; A22: f.x = fn.x by A9,A20,FINSEQ_1:def 7; dom fn=Seg n by A15,FINSEQ_1:def 3; then x<=n by A20,FINSEQ_1:1; then x < n1 by NAT_1:13; then f.x < f.n1 by A8,A11,A20,A17; hence m9 < n9 by A19,A21,A22,TARSKI:def 1; end; fn is one-to-one by A7,FUNCT_1:52; then A23: Sgm rng fn = fn by A4,A6,A15,A10,A12,XBOOLE_1:1; A24: rng <*f.n1*>={f.n1} by FINSEQ_1:39; rng <*f.n1*> c= rng f by A9,FINSEQ_1:30; then A25: {f.n1} c= Seg k by A6,A24; A26: rng f = rng fn\/rng<*f.n1*> by A9,FINSEQ_1:31; A27: f.n1 in {f.n1} by TARSKI:def 1; rng fn c= Seg k by A6,A10; hence Sgm rng f = fn ^ Sgm {f.n1} by A26,A24,A25,A23,A16,FINSEQ_3:42 .= f by A9,A25,A27,FINSEQ_3:44; end; let f be FinSequence of NAT,n such that A28: 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; for n holds P[n] from NAT_1:sch 2(A1,A3); then 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; hence thesis by A28; 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 and A3: j in dom p and A4: ii & k<>j holds p.k=0.K; A6: dom p=Seg len p by FINSEQ_1:def 3; then i in NAT & 1 <= i by A2,FINSEQ_1:1; then A7: i in Seg i; set pI=p|i; consider q be FinSequence such that A8: p = pI^q by FINSEQ_1:80; reconsider q as FinSequence of K by A8,FINSEQ_1:36; A9: i <= len p by A2,A6,FINSEQ_1:1; then A10: len pI=i by FINSEQ_1:17; A11: dom pI=Seg i by A9,FINSEQ_1:17; then not j in dom pI by A4,FINSEQ_1:1; then consider ji be Nat such that A12: ji in dom q and A13: j=i + ji by A3,A8,A10,FINSEQ_1:25; now let k such that A14: k in dom q and A15: k<>ji; reconsider kk=k as Element of NAT by ORDINAL1:def 12; A16: i+kk <> i+ji by A15; dom q = Seg len q by FINSEQ_1:def 3; then k >= 1 by A14,FINSEQ_1:1; then k+i >= i+1 by XREAL_1:7; then A17: i+kk<>i by NAT_1:13; thus q.k = p.(i+kk) by A8,A10,A14,FINSEQ_1:def 7 .= 0.K by A5,A8,A10,A13,A14,A17,A16,FINSEQ_1:28; end; then A18: Sum q = q.ji by A12,MATRIX_3:12 .= p.j by A8,A10,A12,A13,FINSEQ_1:def 7 .= p/.j by A3,PARTFUN1:def 6; A19: Seg i c= Seg len p by A9,FINSEQ_1:5; now let k such that A20: k in dom pI and A21: k<>i; reconsider kk=k as Element of NAT by ORDINAL1:def 12; A22: k<>j by A4,A11,A20,FINSEQ_1:1; thus pI.k = p.kk by A8,A20,FINSEQ_1:def 7 .= 0.K by A5,A6,A11,A19,A20,A21,A22; end; then Sum pI = pI.i by A7,A11,MATRIX_3:12 .= p.i by A8,A7,A11,FINSEQ_1:def 7 .= p/.i by A6,A7,A19,PARTFUN1:def 6; hence Sum p=p/.i+p/.j by A8,A18,RLVECT_1:41; end; let i,j such that A23: i in dom p & j in dom p and A24: i<>j and A25: for k st k in dom p & k<>i & k<>j holds p.k=0.K; A26: ij & k<>i holds p.k=0.K by A25; hence thesis by A1,A23,A25,A26; end; theorem Th8: i in Seg m implies Sgm (Seg (n+m)\Seg n).i=n+i proof assume A1: i in Seg m; reconsider N=n as Element of NAT by ORDINAL1:def 12; set I=idseq m; A2: dom I=Seg len I by FINSEQ_1:def 3; A3: dom (N Shift I) = {k+N where k is Nat: k in dom I} by VALUED_1:def 12; A4: Seg (n+m)\Seg n c= dom (N Shift I) proof let x be object such that A5: x in Seg (n+m)\Seg n; reconsider i=x as Element of NAT by A5; A6: i in Seg (n+m) by A5,XBOOLE_0:def 5; not i in Seg n by A5,XBOOLE_0:def 5; then A7: i<1 or i>n; then reconsider IN=i-n as Element of NAT by A6,FINSEQ_1:1,NAT_1:21; A8: n+IN=i; i<=n+m by A6,FINSEQ_1:1; then A9: IN<=m by A8,XREAL_1:8; IN>=1 by A6,A7,A8,FINSEQ_1:1,NAT_1:19; then IN in dom I by A9; 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 be object; assume x in dom (N Shift I); then consider k be Nat such that A10: k+n=x and A11: k in dom I by A3; k<=m by A11,FINSEQ_1:1; then A12: n+k<=n+m by XREAL_1:7; 1<=k by A11,FINSEQ_1:1; then A13: n+1<=n+k by XREAL_1:7; then n+k >n by NAT_1:13; then A14: not k+n in Seg n by FINSEQ_1:1; 1<=n+1 by NAT_1:11; then 1<=n+k by A13,XXREAL_0:2; then n+k in Seg (n+m) by A12; hence thesis by A10,A14,XBOOLE_0:def 5; end; then Seg (n+m)\Seg n = dom (N Shift I) by A4; hence thesis by A1,A2,VALUED_1:44; 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 and A2: [:Cx,Cy:] c= Indices A; set w=width A; set l=len A; set cy=card Cy; set cx=card Cx; set bY=card By; set bx=card Bx; let B be Matrix of bx,bY,D,C be Matrix of cx,cy,D such that A3: 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); A4: ex kBy be Nat st By c= Seg kBy by MATRIX13:43; then A5: rng Sgm By=By by FINSEQ_1:def 13; 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)); A6: ex kBx be Nat st Bx c= Seg kBx by MATRIX13:43; then A7: rng Sgm Bx=Bx by FINSEQ_1:def 13; A8: dom Sgm By=Seg bY by A4,FINSEQ_3:40; A9: Sgm By is one-to-one by A4,FINSEQ_3:92; A10: Sgm Bx is one-to-one by A6,FINSEQ_3:92; A11: ex kCy be Nat st Cy c= Seg kCy by MATRIX13:43; then A12: rng Sgm Cy=Cy by FINSEQ_1:def 13; A13: Sgm Cy is one-to-one by A11,FINSEQ_3:92; A14: ex kCx be Nat st Cx c= Seg kCx by MATRIX13:43; then A15: rng Sgm Cx=Cx by FINSEQ_1:def 13; A16: Sgm Cx is one-to-one by A14,FINSEQ_3:92; 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 j in Cy by ZFMISC_1:87; then consider yC be object such that A19: yC in dom Sgm Cy and A20: Sgm Cy.yC=j by A12,FUNCT_1:def 3; j in By by A18,ZFMISC_1:87; then consider y being object such that A21: y in dom Sgm By and A22: Sgm By.y=j by A5,FUNCT_1:def 3; i in Cx by A18,ZFMISC_1:87; then consider xC be object such that A23: xC in dom Sgm Cx and A24: Sgm Cx.xC=i by A15,FUNCT_1:def 3; i in Bx by A18,ZFMISC_1:87; then consider x being object such that A25: x in dom Sgm Bx and A26: Sgm Bx.x=i by A7,FUNCT_1:def 3; reconsider x,y as Element of NAT by A25,A21; take BB=B*(x,y); A27: now let m,n; assume m in dom Sgm Cx & n in dom Sgm Cy & Sgm Cx.m=i & Sgm Cy.n=j; then A28: Sgm Cx".i=m & Sgm Cy".j=n by A16,A13,FUNCT_1:32; A29: Sgm By".j=y by A9,A21,A22,FUNCT_1:32; [i,j] in [:Bx,By:]/\[:Cx,Cy:] & Sgm Bx".i=x by A10,A18,A25,A26, FUNCT_1:32,XBOOLE_0:def 4; hence BB=C*(m,n) by A3,A29,A28; end; now let m,n such that A30: m in dom Sgm Bx and A31: n in dom Sgm By and A32: Sgm Bx.m=i and A33: Sgm By.n=j; x=m by A10,A25,A26,A30,A32,FUNCT_1:def 4; hence BB=B*(m,n) by A9,A21,A22,A31,A33,FUNCT_1:def 4; end; hence thesis by A18,A25,A26,A21,A22,A23,A24,A19,A20,A27,XBOOLE_0:def 3; end; suppose A34: [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:]; then j in By by ZFMISC_1:87; then consider y being object such that A35: y in dom Sgm By and A36: Sgm By.y=j by A5,FUNCT_1:def 3; i in Bx by A34,ZFMISC_1:87; then consider x being object such that A37: x in dom Sgm Bx and A38: Sgm Bx.x=i by A7,FUNCT_1:def 3; reconsider x,y as Element of NAT by A37,A35; take BB=B*(x,y); now let m,n such that A39: m in dom Sgm Bx and A40: n in dom Sgm By and A41: Sgm Bx.m=i and A42: Sgm By.n=j; x = m by A10,A37,A38,A39,A41,FUNCT_1:def 4; hence BB=B*(m,n) by A9,A35,A36,A40,A42,FUNCT_1:def 4; end; hence thesis by A34,A37,A38,A35,A36,XBOOLE_0:def 3; end; suppose A43: not [i,j] in [:Bx,By:] & [i,j] in [:Cx,Cy:]; then j in Cy by ZFMISC_1:87; then consider y being object such that A44: y in dom Sgm Cy and A45: Sgm Cy.y=j by A12,FUNCT_1:def 3; i in Cx by A43,ZFMISC_1:87; then consider x being object such that A46: x in dom Sgm Cx and A47: Sgm Cx.x=i by A15,FUNCT_1:def 3; reconsider x,y as Element of NAT by A46,A44; take CC=C*(x,y); now let m,n such that A48: m in dom Sgm Cx and A49: n in dom Sgm Cy and A50: Sgm Cx.m=i and A51: Sgm Cy.n=j; x = m by A16,A46,A47,A48,A50,FUNCT_1:def 4; hence CC=C*(m,n) by A13,A44,A45,A49,A51,FUNCT_1:def 4; end; hence thesis by A43,A46,A47,A44,A45,XBOOLE_0:def 3; end; suppose A52: not [i,j] in [:Bx,By:] & not [i,j] in [:Cx,Cy:]; take A*(i,j); thus thesis by A52; end; end; consider M be Matrix of l,w,D such that A53: for i,j st [i,j] in Indices M holds P[i,j,M*(i,j)] from MATRIX_0: sch 2(A17); set MB=Segm(M,Bx,By); take M; A is Matrix of l,w,D by MATRIX_0:51; then A54: Indices A=Indices M by MATRIX_0:26; A55: dom Sgm Bx=Seg bx by A6,FINSEQ_3:40; now let i,j such that A56: [i,j] in Indices MB; bx<>0 by A56,MATRIX_0:22; then A57: Indices MB=[:Seg bx,Seg bY:] by MATRIX_0:23; then A58: j in Seg bY by A56,ZFMISC_1:87; then A59: Sgm By.j in By by A5,A8,FUNCT_1:def 3; A60: i in Seg bx by A56,A57,ZFMISC_1:87; then Sgm Bx.i in Bx by A7,A55,FUNCT_1:def 3; then [Sgm Bx.i,Sgm By.j] in [:Bx,By:] by A59,ZFMISC_1:87; hence B*(i,j) = M*(Sgm Bx.i,Sgm By.j) by A1,A55,A8,A53,A54,A60,A58 .= MB*(i,j) by A56,MATRIX13:def 1; end; hence MB=B by MATRIX_0:27; set MC=Segm(M,Cx,Cy); A61: dom Sgm Cy=Seg cy by A11,FINSEQ_3:40; A62: dom Sgm Cx=Seg cx by A14,FINSEQ_3:40; now let i,j such that A63: [i,j] in Indices MC; cx<>0 by A63,MATRIX_0:22; then A64: Indices MC=[:Seg cx,Seg cy:] by MATRIX_0:23; then A65: j in Seg cy by A63,ZFMISC_1:87; then A66: Sgm Cy.j in Cy by A12,A61,FUNCT_1:def 3; A67: i in Seg cx by A63,A64,ZFMISC_1:87; then Sgm Cx.i in Cx by A15,A62,FUNCT_1:def 3; then [Sgm Cx.i,Sgm Cy.j] in [:Cx,Cy:] by A66,ZFMISC_1:87; hence C*(i,j) = M*(Sgm Cx.i,Sgm Cy.j) by A2,A62,A61,A53,A54,A67,A65 .= MC*(i,j) by A63,MATRIX13:def 1; end; hence MC=C by MATRIX_0:27; let i,j such that A68: [i,j] in Indices M\([:Bx,By:]\/[:Cx,Cy:]); not [i,j] in [:Bx,By:]\/[:Cx,Cy:] by A68,XBOOLE_0:def 5; hence thesis by A53,A68; end; theorem Th10: for P,Q,Q9 be without_zero finite Subset of NAT st [:P,Q9:] 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= Q9 & Line(A,i) * Sgm Q9 = card Q9 |-> 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 and A3: j in Seg width A \ Q and A4: A*(i,j)<> 0.K and A5: Q c= R and A6: Line(A,i) * Sgm R = card R |-> 0.K; A7: dom A=Seg len A by FINSEQ_1:def 3; then A8: i in Seg len A by A2,XBOOLE_0:def 5; A9: [:P,Q:] c= [:P,R:] by A5,ZFMISC_1:95; then A10: [:P,Q:] c= Indices A by A1; reconsider i0=i,j0=j as non zero Element of NAT by A2,A3,A7; A11: j in Seg width A by A3,XBOOLE_0:def 5; set S=Segm(A,P,Q); consider P9,Q9 be without_zero finite Subset of NAT such that A12: [:P9,Q9:] c= Indices S and A13: card P9 = card Q9 and A14: card P9 = the_rank_of S and A15: Det EqSegm(S,P9,Q9)<>0.K by MATRIX13:def 4; P9={} iff Q9={} by A13; then consider P2,Q2 be without_zero finite Subset of NAT such that A16: P2 c= P and A17: Q2 c= Q and P2 = Sgm P.:P9 and Q2=Sgm Q.:Q9 and A18: card P2=card P9 and A19: card Q2=card Q9 and A20: Segm(S,P9,Q9) = Segm(A,P2,Q2) by A12,MATRIX13:57; set Q2j=Q2\/{j0}; set P2i=P2\/{i0}; 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:27,ZFMISC_1:90; then A21: the_rank_of S=0 by MATRIX13:77; [i,j] in Indices A by A7,A8,A11,ZFMISC_1:87; hence thesis by A4,A21,MATRIX13:94; end; suppose A22: [:P,Q:]<>{}; then P c= dom A by A10,ZFMISC_1:114; then A23: P2 c= dom A by A16; [:P,R:]<>{} by A9,A22,XBOOLE_1:3; then A24: R c= Seg width A by A1,ZFMISC_1:114; then A25: dom Sgm R=Seg card R by FINSEQ_3:40; Q c= Seg width A by A10,A22,ZFMISC_1:114; then A26: Q2 c= Seg width A by A17; A27: {j0}c= Seg width A by A11,ZFMISC_1:31; then A28: Sgm Q2j is one-to-one by A26,FINSEQ_3:92,XBOOLE_1:8; A29: Q2j c= Seg width A by A26,A27,XBOOLE_1:8; then A30: rng Sgm Q2j=Q2j by FINSEQ_1:def 13; A31: {i0} c= dom A by A7,A8,ZFMISC_1:31; then A32: P2i c= dom A by A23,XBOOLE_1:8; then A33: [:P2i,Q2j:] c= Indices A by A29,ZFMISC_1:96; A34: dom Sgm P2i=Seg card P2i by A7,A23,A31,FINSEQ_3:40,XBOOLE_1:8; i in {i} by TARSKI:def 1; then A35: i in P2i by XBOOLE_0:def 3; A36: not i in P2 by A2,A16,XBOOLE_0:def 5; then A37: card P2i=card P2+1 by CARD_2:41; then A38: card P2i-'1=card P9 by A18,NAT_D:34; A39: not j in Q2 by A3,A17,XBOOLE_0:def 5; then A40: card Q2j=card Q2+1 by CARD_2:41; then A41: ESS = SS by A13,A18,A19,A36,CARD_2:41,MATRIX13:def 3; j in {j} by TARSKI:def 1; then j in Q2j by XBOOLE_0:def 3; then consider y being object such that A42: y in dom Sgm Q2j and A43: Sgm Q2j.y=j by A30,FUNCT_1:def 3; rng Sgm P2i=P2i by A7,A32,FINSEQ_1:def 13; then consider x being object such that A44: x in dom Sgm P2i and A45: Sgm P2i.x=i by A35,FUNCT_1:def 3; reconsider x,y as Element of NAT by A44,A42; -1_K<>0.K by VECTSP_1:28; then A46: power(K).(-1_K,x+y)<>0.K by Lm2; set L=LaplaceExpL(ESS,x); A47: dom L = Seg len L by FINSEQ_1:def 3 .= Seg card P2i by LAPLACE:def 7; then A48: y in dom L by A13,A18,A19,A26,A27,A37,A40,A42,FINSEQ_3:40,XBOOLE_1:8; A49: dom Sgm Q2j=Seg card Q2j by A26,A27,FINSEQ_3:40,XBOOLE_1:8; then Delete(ESS,x,y) = EqSegm(A,P2i\{i},Q2j\{j}) by A13,A18,A19,A37,A40,A34 ,A44,A45,A42,A43,MATRIX13:64 .= EqSegm(A,P2,Q2j\{j}) by A36,ZFMISC_1:117 .= EqSegm(A,P2,Q2) by A39,ZFMISC_1:117 .= Segm(A,P2,Q2) by A13,A18,A19,MATRIX13:def 3 .= EqSegm(S,P9,Q9) by A13,A20,MATRIX13:def 3; then A50: power(K).(-1_K,x+y) * Det Delete(ESS,x,y)<>0.K by A15,A38,A46,VECTSP_1:12; A51: Indices ESS = [:Seg card P2i,Seg card P2i:] by MATRIX_0:24; then A52: [x,y] in Indices ESS by A13,A18,A19,A37,A40,A34,A49,A44,A42,ZFMISC_1:87; A53: rng Sgm R=R by A24,FINSEQ_1:def 13; now let k such that A54: k in dom L and A55: k <> y; Sgm Q2j.k <> j by A13,A18,A19,A37,A40,A49,A28,A42,A43,A47,A54,A55, FUNCT_1:def 4; then A56: not Sgm Q2j.k in {j} by TARSKI:def 1; Sgm Q2j.k in Q2j by A13,A18,A19,A37,A40,A30,A49,A47,A54,FUNCT_1:def 3; then Sgm Q2j.k in Q2 by A56,XBOOLE_0:def 3; then A57: Sgm Q2j.k in Q by A17; then A58: Sgm Q2j.k in R by A5; consider z being object such that A59: z in dom Sgm R and A60: Sgm R.z=Sgm Q2j.k by A5,A53,A57,FUNCT_1:def 3; reconsider z as Element of NAT by A59; [x,k] in Indices ESS by A34,A44,A47,A51,A54,ZFMISC_1:87; then ESS*(x,k) = A*(i,Sgm Q2j.k) by A45,A41,MATRIX13:def 1 .= Line(A,i).(Sgm R.z) by A24,A60,A58,MATRIX_0:def 7 .= (card R |-> 0.K).z by A6,A59,FUNCT_1:13 .= 0.K by A25,A59,FINSEQ_2:57; hence L.k = 0.K*Cofactor(ESS,x,k) by A54,LAPLACE:def 7 .= 0.K; end; then A61: L.y = Sum L by A48,MATRIX_3:12 .= Det ESS by A34,A44,LAPLACE:25; L.y = SS*(x,y)*Cofactor(ESS,x,y) by A48,A41,LAPLACE:def 7 .= A*(i,j)*(power(K).(-1_K,x+y)*Det Delete(ESS,x,y)) by A45,A43,A41,A52, MATRIX13:def 1; then Det ESS<>0.K by A4,A61,A50,VECTSP_1:12; then the_rank_of A >= card P2i by A13,A18,A19,A37,A40,A33,MATRIX13:def 4; hence thesis by A14,A18,A37,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; set w=width A; set l=len A; reconsider A9=A as Matrix of len A,width A,K by MATRIX_0:51; set S=Segm(A9,N,Seg width A9); consider U be finite Subset of w-VectSp_over K such that A3: U is linearly-independent and A4: U c= lines A9 and A5: card U = the_rank_of A9 by MATRIX13:123; A6: U c= lines S proof let x be object such that A7: x in U; consider Ni be Nat such that A8: Ni in Seg l and A9: x = Line(A9,Ni) by A4,A7,MATRIX13:103; A10: dom A=Seg l by FINSEQ_1:def 3; A11: Ni in N proof assume not Ni in N; then Ni in dom A\N by A8,A10,XBOOLE_0:def 5; then x = w |-> 0.K by A2,A9 .= 0.(w-VectSp_over K) by MATRIX13:102; hence thesis by A3,A7,VECTSP_7:2; end; rng Sgm N=N by A1,A10,FINSEQ_1:def 13; then consider i be object such that A12: i in dom Sgm N and A13: Sgm N.i=Ni by A11,FUNCT_1:def 3; reconsider i as Element of NAT by A12; A14: dom Sgm N=Seg card N by A1,A10,FINSEQ_3:40; then Line(S,i) = x by A9,A12,A13,MATRIX13:48; hence thesis by A12,A14,MATRIX13:103; end; A15: now let W be finite Subset of w-VectSp_over K such that A16: W is linearly-independent and A17: W c= lines S; dom A=Seg l by FINSEQ_1:def 3; then lines S c= lines A9 by A1,MATRIX13:118; then W c= lines A9 by A17; hence card W <= the_rank_of A9 by A16,MATRIX13:123; end; w=card Seg w by FINSEQ_1:57; hence thesis by A3,A5,A6,A15,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 A5: N={} by A4; assume the_rank_of A <>0; then consider i,j such that A6: [i,j] in Indices A and A7: A*(i,j) <> 0.K by MATRIX13:94; A8: j in Seg width A by A6,ZFMISC_1:87; A9: i in dom A by A6,ZFMISC_1:87; then 0.K = (len A|-> 0.K).i by A3,FINSEQ_2:57 .= Col(A,j).i by A2,A8,A5 .= A*(i,j) by A9,MATRIX_0:def 8; hence thesis by A7; end; hence thesis by A4,MATRIX13:77; end; suppose A10: card N>0; then N <> {}; then Seg width A <> {} by A1,XBOOLE_1:3; then A11: width A<>0; then A12: len A<>0 by MATRIX_0:def 3; set AT=A@; A13: [:dom A,N:] c= Indices A by A1,ZFMISC_1:95; A14: width AT=len A by A11,MATRIX_0:54; A15: len AT=width A by A11,MATRIX_0:54; then A16: N c= dom AT by A1,FINSEQ_1:def 3; A17: dom AT=Seg len AT by FINSEQ_1:def 3; A18: now let i such that A19: i in dom AT \ N; i in dom AT by A19,XBOOLE_0:def 5; hence Line(AT,i) = Col(A,i) by A15,A17,MATRIX_0:59 .= width AT |-> 0.K by A2,A15,A14,A17,A19; end; thus the_rank_of A = the_rank_of AT by MATRIX13:84 .= the_rank_of Segm(AT, N,Seg len A) by A14,A16,A18,Th11 .= the_rank_of (Segm(A,Seg len A,N)@) by A3,A10,A12,A13,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 ua=u+a*v; set UU=U\{u}; UU \/ {ua} c= the carrier of Lin U proof let x be object such that A2: x in UU \/ {ua}; per cases by A2,XBOOLE_0:def 3; suppose x in UU; then x in U by XBOOLE_0:def 5; then x in Lin U by VECTSP_7:8; hence thesis by STRUCT_0:def 5; end; suppose A3: x in {ua}; A4: u in Lin U & a*v in Lin U by A1,VECTSP_4:21,VECTSP_7:8; x=ua by A3,TARSKI:def 1; then x in Lin U by A4,VECTSP_4:20; hence thesis by STRUCT_0:def 5; end; end; hence thesis by VECTSP_9:16; 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 and A2: v in U and A3: u = v implies (a <> -1_K or u = 0.V); set ua=u+a*v; set UU=U\{u}; U c= the carrier of Lin (UU\/{ua}) proof let x be object such that A4: x in U; per cases; suppose A5: x=u; per cases; suppose A6: u<>v; A7: ua+(-a)*v = ua-a*v by VECTSP_1:21 .= u+(a*v-a*v) by RLVECT_1:def 3 .= u+0.V by VECTSP_1:16 .= u by RLVECT_1:def 4; ua in {ua} by TARSKI:def 1; then ua in UU\/{ua} by XBOOLE_0:def 3; then A8: ua in Lin(UU\/{ua}) by VECTSP_7:8; v in UU by A2,A6,ZFMISC_1:56; then v in UU\/{ua} by XBOOLE_0:def 3; then (-a)*v in Lin(UU\/{ua}) by VECTSP_4:21,VECTSP_7:8; then ua+(-a)*v in Lin(UU\/{ua}) by A8,VECTSP_4:20; hence thesis by A5,A7,STRUCT_0:def 5; end; suppose A9: u=v; per cases by A3,A9; suppose a<>-1_K; then 0.K<> -1_K-a by VECTSP_1:19; then 0.K<> -(-1_K-a) by VECTSP_1:28; then A10: 0.K<>a+1_K by VECTSP_1:31; ua in {ua} by TARSKI:def 1; then A11: ua in UU\/{ua} by XBOOLE_0:def 3; ua = 1_K*u+a*u by A9,VECTSP_1:def 17 .= (1.K+a)*u by VECTSP_1:def 15; then (1.K+a)" *ua =u by A10,VECTSP_1:20; then u in Lin (UU\/{ua}) by A11,VECTSP_4:21,VECTSP_7:8; hence thesis by A5,STRUCT_0:def 5; end; suppose u=0.V; then x in Lin(UU\/{ua}) by A5,VECTSP_4:17; hence thesis by STRUCT_0:def 5; end; end; end; suppose x<>u; then x in UU by A4,ZFMISC_1:56; then x in UU\/{ua} by XBOOLE_0:def 3; then x in Lin (UU\/{ua}) by VECTSP_7:8; hence thesis by STRUCT_0:def 5; end; end; then Lin U is Subspace of Lin (UU\/{ua}) by VECTSP_9:16; then A12: the carrier of Lin U c=the carrier of Lin (UU\/{ua}) by VECTSP_4:def 2; Lin (UU\/{ua}) is Subspace of Lin U by A1,A2,Th13; then the carrier of Lin (UU\/{ua})c= the carrier of Lin U by VECTSP_4:def 2; then the carrier of Lin U =the carrier of Lin (UU\/ {ua}) by A12; hence thesis by VECTSP_4:29; 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 reconsider N=n as Element of NAT by ORDINAL1:def 12; set AB=A^^B; A1: dom B = Seg len B by FINSEQ_1:def 3 .= Seg n by MATRIX_0:def 2; dom A = Seg len A by FINSEQ_1:def 3 .= Seg n by MATRIX_0:def 2; then A2: dom AB = Seg n/\Seg n by A1,PRE_POLY:def 4 .= Seg n; then A3: len AB=N by FINSEQ_1:def 3; per cases; suppose A4: N=0; then AB={} by A2; hence thesis by A4,MATRIX_0:13; end; suppose A5: N>0; then A6: N in Seg N by FINSEQ_1:3; then A.N=Line(A,N) & B.N=Line(B,N) by MATRIX_0:52; then A7: AB.N=Line(A,N)^Line(B,N) by A2,A6,PRE_POLY:def 4; A8: len (Line(A,N)^Line(B,N))=width A+width B by CARD_1:def 7; AB.N in rng AB by A2,A6,FUNCT_1:def 3; then width AB=width A+width B by A3,A5,A7,A8,MATRIX_0:def 3; hence thesis by A3,MATRIX_0:51; 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; set AB=A^^B; A1: len AB=n & dom AB=Seg len AB by FINSEQ_1:def 3,MATRIX_0:def 2; let i such that A2: i in Seg n; Line(A,i)=A.i & Line(B,i)=B.i by A2,MATRIX_0:52; hence Line(A,i)^Line(B,i) = AB.i by A2,A1,PRE_POLY:def 4 .= Line(AB,i) by A2,MATRIX_0:52; 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 AB=n by MATRIX_0:def 2; A3: len A=n by MATRIX_0:def 2; now let j such that A4: j in Seg n; n<>0 by A4; then width AB=width A+width B by MATRIX_0:23; then width A<=width AB by NAT_1:11; then A5: Seg width A c= Seg width AB by FINSEQ_1:5; A6: dom A=Seg n by A3,FINSEQ_1:def 3; A7: dom Line(A,j)=Seg width A by FINSEQ_2:124; dom AB=Seg n by A2,FINSEQ_1:def 3; hence Col(AB,i).j = AB*(j,i) by A4,MATRIX_0:def 8 .= Line(AB,j).i by A1,A5,MATRIX_0:def 7 .= (Line(A,j)^Line(B,j)).i by A4,Th15 .= Line(A,j).i by A1,A7,FINSEQ_1:def 7 .= A*(j,i) by A1,MATRIX_0:def 7 .= Col(A,i).j by A4,A6,MATRIX_0:def 8; end; hence thesis by A3,A2,FINSEQ_2:119; 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 AB=n by MATRIX_0:def 2; A3: len B=n by MATRIX_0:def 2; now A4: dom B=Seg n by A3,FINSEQ_1:def 3; let j such that A5: j in Seg n; n<>0 by A5; then width AB=width A+width B by MATRIX_0:23; then A6: width A+i in Seg width AB by A1,FINSEQ_1:60; A7: dom Line(B,j)=Seg width B & len Line(A,j)=width A by CARD_1:def 7 ,FINSEQ_2:124; dom AB=Seg n by A2,FINSEQ_1:def 3; hence Col(AB,width A+i).j = AB*(j,width A+i) by A5,MATRIX_0:def 8 .= Line(AB,j).(width A+i) by A6,MATRIX_0:def 7 .= (Line(A,j)^Line(B,j)).(width A+i) by A5,Th15 .= Line(B,j).i by A1,A7,FINSEQ_1:def 7 .= B*(j,i) by A1,MATRIX_0:def 7 .= Col(B,i).j by A5,A4,MATRIX_0:def 8; end; hence thesis by A3,A2,FINSEQ_2:119; 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 and A2: len pB = width B; set RB=RLine(B,i,pB); set RA=RLine(A,i,pA); set AB=A^^B; set RAB=RLine(AB,i,pA^pB); set Rab=RA^^RB; A3: now pA is Element of (width A)-tuples_on D & pB is Element of (width B) -tuples_on D by A1,A2,FINSEQ_2:92; then pA^pB is Tuple of width A+width B, D; then pA^pB is Element of (width A+width B)-tuples_on D by FINSEQ_2:131; then A4: len (pA^pB)=width A+width B by CARD_1:def 7; let j such that A5: 1<=j & j<=n; A6: j in Seg n by A5; A7: width AB=width A+width B by A5,MATRIX_0:23; A8: now per cases; suppose A9: i=j; then A10: Line(RB,j)=pB by A2,A6,MATRIX11:28; Line(RAB,j)=pA^pB & Line(RA,j)=pA by A1,A6,A4,A7,A9,MATRIX11:28; hence Line(RAB,j)=Line(Rab,j) by A6,A10,Th15; end; suppose A11: i<>j; then A12: Line(RB,j)=Line(B,j) by A6,MATRIX11:28; Line(RAB,j)=Line(AB,j) & Line(RA,j)=Line(A,j) by A6,A11,MATRIX11:28; hence Line(RAB,j) = Line(RA,j)^Line(RB,j) by A6,A12,Th15 .= Line(Rab,j) by A6,Th15; end; end; thus RAB.j = Line(RAB,j) by A6,MATRIX_0:52 .= Rab.j by A6,A8,MATRIX_0:52; end; len RAB=n & len Rab=n by MATRIX_0:def 2; hence thesis by A3; 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: card Seg n=n by FINSEQ_1:57; A2: len A=n by MATRIX_0:def 2; then reconsider A9=A as Matrix of n,width A,D by MATRIX_0:51; set S1=Segm(AB,Seg n,Seg width A); A3: card Seg width A=width A by FINSEQ_1:57; A4: len AB=n by MATRIX_0:def 2; now let i,j such that A5: [i,j] in Indices A9; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12; A6: dom A=Seg n by A2,FINSEQ_1:def 3; n<>0 by A5,MATRIX_0:22; then Indices A9=[:Seg n,Seg width A:] by MATRIX_0:23; then A7: I in Seg n by A5,ZFMISC_1:87; A8: J in Seg width A by A5,ZFMISC_1:87; then A9: J = (idseq width A).J by FINSEQ_2:49 .= Sgm (Seg (width A)).J by FINSEQ_3:48; dom S1 = Seg len S1 by FINSEQ_1:def 3 .= Seg n by A1,MATRIX_0:def 2; hence S1*(i,j) = Col(S1,J).I by A7,MATRIX_0:def 8 .= Col(AB,Sgm (Seg (width A)).J).I by A4,A3,A8,MATRIX13:50 .= Col(A,J).I by A8,A9,Th16 .= A*(i,j) by A7,A6,MATRIX_0:def 8; end; hence A=S1 by A1,A3,MATRIX_0:27; set w=width A+width B; set SS=Seg w\Seg width A; set S2=Segm(AB,Seg n,SS); A10: len B=n by MATRIX_0:def 2; then reconsider B9=B as Matrix of n,width B,D by MATRIX_0:51; width A <= w by NAT_1:11; then card Seg (width A+width B)=width A+width B & Seg width A c= Seg w by FINSEQ_1:5,57; then A11: card SS = w-width A by A3,CARD_2:44 .= width B; now A12: dom B = Seg n by A10,FINSEQ_1:def 3; let i,j such that A13: [i,j] in Indices B9; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12; A14: J in Seg width B by A13,ZFMISC_1:87; n<>0 by A13,MATRIX_0:22; then Indices B9=[:Seg n,Seg width B:] by MATRIX_0:23; then A15: I in Seg n by A13,ZFMISC_1:87; dom S2 = Seg len S2 by FINSEQ_1:def 3 .= Seg n by A1,MATRIX_0:def 2; hence S2*(i,j) = Col(S2,J).I by A15,MATRIX_0:def 8 .= Col(AB,Sgm SS.J).I by A4,A11,A14,MATRIX13:50 .= Col(AB,width A+J).I by A14,Th8 .= Col(B,J).I by A14,Th17 .= B9*(i,j) by A15,A12,MATRIX_0:def 8; end; hence thesis by A1,A11,MATRIX_0:27; 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 B9=B as Matrix of L,width B,K by A1,MATRIX_0:51; reconsider A9=A as Matrix of L,width A,K by MATRIX_0:51; set AB=A9^^B9; per cases; suppose L=0; hence thesis by A1,MATRIX13:74; end; suppose A2: L>0; A3: Segm(AB,Seg L,Seg width A) = A by Th19; A4: Indices AB=[:Seg L,Seg (width A+ width B):] by A2,MATRIX_0:23; A5: width AB=width A+width B by A2,MATRIX_0:23; then width A <=width AB by NAT_1:11; then Seg width A c=Seg width AB by FINSEQ_1:5; then A6: [:Seg L,Seg width A:] c= Indices AB by A5,A4,ZFMISC_1:95; Seg width AB\Seg width A c=Seg width AB by XBOOLE_1:36; then A7: [:Seg L,Seg width AB\Seg width A:] c= Indices AB by A5,A4,ZFMISC_1:95; Segm(AB,Seg L,Seg width AB\Seg width A) = B by A5,Th19; hence thesis by A3,A6,A7,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 and A2: len A =the_rank_of A; set L=len A; reconsider B9=B as Matrix of L,width B,K by A1,MATRIX_0:51; reconsider A9=A as Matrix of L,width A,K by MATRIX_0:51; A3: the_rank_of (A9^^B9)<=len (A9^^B9) & len (A9^^B9)=L by MATRIX13:74 ,MATRIX_0:def 2; the_rank_of (A9^^B9)>=L by A1,A2,Th20; hence thesis by A2,A3,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 and A2: width A =0; A3: Seg width A = {} by A2; set L=len A; reconsider B9=B as Matrix of L,width B,K by A1,MATRIX_0:51; reconsider A9=A as Matrix of L,width A,K by MATRIX_0:51; set AB=A9^^B9; set BA=B9^^A9; per cases; suppose A4: L=0; then len BA=0 by MATRIX_0:def 2; then A5: BA={}; len AB=0 by A4,MATRIX_0:def 2; then AB={}; hence thesis by A1,A4,A5; end; suppose A6: L>0; then width AB=width B & len AB=L by A2,MATRIX_0:23; hence A^^B = Segm(AB,Seg L,Seg width B\Seg width A) by A3,MATRIX13:46 .= B by A2,Th19; width BA=width B & len BA=L by A2,A6,MATRIX_0:23; hence B^^A = Segm(BA,Seg L,Seg width B) by 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); A2: len B = len A by A1,MATRIX_0:def 2; set L=len A; reconsider B9=B as Matrix of L,width B,K by A2,MATRIX_0:51; reconsider A9=A as Matrix of L,width A,K by MATRIX_0:51; set AB=A9^^B9; per cases; suppose width B=0; hence thesis by A2,Th22; end; suppose width B>0; then A3: L>0 by A2,MATRIX_0:def 3; then A4: width AB=width A+width B by MATRIX_0:23; A5: len AB=L by A3,MATRIX_0:23; A6: now set L0=len AB |-> 0.K; let i such that A7: i in Seg width AB \ Seg width A; A8: i in Seg width AB by A7,XBOOLE_0:def 5; not i in Seg width A by A7,XBOOLE_0:def 5; then A9: i<1 or i>width A; then reconsider n=i-width A as Element of NAT by A8,FINSEQ_1:1,NAT_1:21; A10: i=n+width A; n<>0 by A8,A9,FINSEQ_1:1; then A11: n in Seg width B by A4,A8,A10,FINSEQ_1:61; A12: now let i such that A13: 1<=i & i<=L; A14: i in Seg L by A13; then A15: L0.i=0.K by A5,FINSEQ_2:57; Seg L=dom B by A2,FINSEQ_1:def 3; then Col(B9,n).i=B9*(i,n) & [i,n] in Indices B by A11,A14, MATRIX_0:def 8,ZFMISC_1:87; hence Col(B9,n).i=L0.i by A1,A15,MATRIX_3:1; end; A16: len Col(B,n)=L & len L0=L by A2,A5,CARD_1:def 7; Col(AB,i)=Col(B9,n) by A10,A11,Th17; hence Col(AB,i) = len AB |-> 0.K by A16,A12; end; width A <= width AB by A4,NAT_1:11; then Seg width A c= Seg width AB by FINSEQ_1:5; hence the_rank_of (A^^B) = the_rank_of Segm(AB,Seg len AB,Seg width A) by A6,Th12 .= the_rank_of A by A5,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) and A2: len A=len B; reconsider B9=B as Matrix of len A,width B,K by A2,MATRIX_0:51; reconsider A9=A as Matrix of len A,width A,K by MATRIX_0:51; set AB=A9^^B9; let N such that A3: N c= dom A and A4: for i st i in N holds Line(A,i)=width A|->0.K; let i such that A5: i in N; dom A <> {} by A3,A5; then Seg len A <> {} by FINSEQ_1:def 3; then A6: len A<>0; then A7: width AB=width A+width B by MATRIX_0:23; then width A <= width AB by NAT_1:11; then A8: Seg width A c= Seg width AB by FINSEQ_1:5; A9: card Seg len A=len A by FINSEQ_1:57; A10: Segm(AB,Seg len A,Seg width A)=A by Th19; A11: dom A=Seg len A by FINSEQ_1:def 3; A12: Sgm (Seg len A).i = (idseq len A).i by FINSEQ_3:48 .= i by A3,A5,A11,FINSEQ_2:49; card Seg width A=width A by FINSEQ_1:57; then A13: card (Seg width A) |->0.K = Line(A,i) by A4,A5 .= Line(AB,i) * Sgm (Seg width A) by A3,A5,A11,A10,A8,A9,A12,MATRIX13:47; assume Line(B,i)<>width B|->0.K; then consider j such that A14: j in Seg width B and A15: Line(B,i).j<>(width B|->0.K).j by FINSEQ_2:119; A16: len Line(A9,i)=width A9 & 1<=j by A14,FINSEQ_1:1,MATRIX_0:def 7; len Line(B9,i)=width B9 by MATRIX_0:def 7; then A17: j<=len Line(B9,i) by A14,FINSEQ_1:1; A18: j+width A in Seg width AB by A14,A7,FINSEQ_1:60; then AB*(i,j+width A) = Line(AB,i).(j+width A) by MATRIX_0:def 7 .= (Line(A9,i)^Line(B9,i)).(j+width A) by A3,A5,A11,Th15 .= Line(B9,i).j by A16,A17,FINSEQ_1:65; then A19: AB*(i,j+width A)<> 0.K by A14,A15,FINSEQ_2:57; consider P,Q be without_zero finite Subset of NAT such that A20: [:P,Q:] c= Indices A9 and A21: card P = card Q and A22: card P = the_rank_of A9 and A23: Det EqSegm(A9,P,Q)<>0.K by MATRIX13:def 4; P={} iff Q={} by A21; then consider P2,Q2 be without_zero finite Subset of NAT such that A24: P2 c= Seg len A and A25: Q2 c= Seg width A and A26: P2 = Sgm Seg len A.:P and Q2=Sgm Seg width A.:Q and card P2=card P and card Q2=card Q and A27: Segm(A,P,Q) = Segm(AB,P2,Q2) by A20,A10,MATRIX13:57; A28: Segm(AB,P2,Q2)=EqSegm(A,P,Q) by A21,A27,MATRIX13:def 3; A29: dom AB=Seg len AB & len AB=len A by A6,FINSEQ_1:def 3,MATRIX_0:23; then A30: [:P2,Seg width A:] c= Indices AB by A24,A8,ZFMISC_1:96; j>=1 by A14,FINSEQ_1:1; then j+width A >=1+width A by XREAL_1:6; then j+width A >width A by NAT_1:13; then not j+width A in Q2 by A25,FINSEQ_1:1; then A31: j+width A in Seg width AB\Q2 by A18,XBOOLE_0:def 5; not i in P2 proof A32: Line(A,i) = width A|->0.K by A4,A5 .= 0.K*Line(A,i) by FVSUM_1:58; A33: Sgm Seg len A = idseq len A by FINSEQ_3:48 .= id (Seg len A); A34: P c= Seg len A by A20,A21,MATRIX13:67; then A35: rng Sgm P=P by FINSEQ_1:def 13; assume i in P2; then i in P by A26,A33,A34,FUNCT_1:92; then consider x being object such that A36: x in dom Sgm P and A37: Sgm P.x=i by A35,FUNCT_1:def 3; reconsider x as Element of NAT by A36; A38: Segm(A,P,Q)=EqSegm(A,P,Q) by A21,MATRIX13:def 3; A39: Q c= Seg width A by A20,A21,MATRIX13:67; then A40: rng Sgm Q=Q by FINSEQ_1:def 13; A41: dom Sgm P=Seg card P by A34,FINSEQ_3:40; then dom Line(A,i)=Seg width A & Line(Segm(A,P,Q),x)=Line(A,i)* Sgm Q by A39,A36,A37,FINSEQ_2:124,MATRIX13:47; then Line(Segm(A,P,Q),x)=0.K * Line(Segm(A,P,Q),x) by A39,A40,A32, MATRIX13:87; then 0.K*Det EqSegm(A,P,Q) = Det RLine(EqSegm(A,P,Q),x,Line(EqSegm(A,P,Q), x)) by A41,A36,A38,MATRIX11:35 .= Det EqSegm(A,P,Q) by MATRIX11:30; hence thesis by A23; end; then i in dom AB\P2 by A3,A5,A11,A29,XBOOLE_0:def 5; then card P > the_rank_of Segm(AB,P2,Q2) by A1,A19,A22,A25,A30,A31,A13,Th10; hence thesis by A23,A28,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 by MATRIX_0:23; A2: width B=len b by MATRIX_0:23; A3: len (B@)=width B by MATRIX_0:def 6; per cases; suppose A4: len b=0; then B@={} by A3,MATRIX_0:23; hence thesis by A4,MATRIX_0:13; end; suppose len b>0; then width (B@)=len B by A2,MATRIX_0:54; hence thesis by A1,A2,A3,MATRIX_0:51; 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 1 in Seg 1; then A1: Line(LineVec2Mx bD,1)=(LineVec2Mx bD).1 by MATRIX_0:52; assume MD = LineVec2Mx bD; hence thesis by A1,FINSEQ_1:40; end; assume that A2: Line(MD,1) = bD and A3: len MD = 1; reconsider md=MD as Matrix of 1,width MD,D by A3,MATRIX_0:51; 1 in Seg 1; then md.1=bD by A2,MATRIX_0:52; hence thesis by A3,FINSEQ_1:40; 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 len (LineVec2Mx bD)=1 by Th25; then A2: dom (LineVec2Mx bD)=Seg 1 by FINSEQ_1:def 3; assume A3: MD = ColVec2Mx bD; 1 in Seg 1; hence Col(MD,1) = Line(LineVec2Mx bD,1) by A3,A2,MATRIX_0:58 .= bD by Th25; len MD=len bD by A3,MATRIX_0:def 2; hence thesis by A1,A3,MATRIX_0:23; end; assume that A4: Col(MD,1) = bD and A5: width MD = 1; A6: len MD>0 by A1,A4,MATRIX_0:def 8; A7: len (MD@)=1 by A5,MATRIX_0:def 6; 1 in Seg 1; then Line(MD@,1)=bD by A4,A5,MATRIX_0:59; then (LineVec2Mx bD)@ = (MD@)@ by A7,Th25 .= MD by A5,A6,MATRIX_0:57; hence thesis; end; theorem len f = len g implies (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g) proof set Lf=LineVec2Mx f; set Lg=LineVec2Mx g; A1: len Lf=1 by CARD_1:def 7; assume A2: len f = len g; then reconsider F=f,G=g as Element of (len f)-tuples_on the carrier of K by FINSEQ_2:92; A3: width Lg=len f by A2,MATRIX_0:23; set FG=F+G; set Lfg=LineVec2Mx FG; A4: len FG=len f & len Lfg=1 by CARD_1:def 7; A5: width Lfg=len FG by MATRIX_0:23; A6: len (Lf+Lg)=len Lf by MATRIX_3:def 3; A7: width (Lf+Lg)=width Lf by MATRIX_3:def 3; A8: width Lf=len f by MATRIX_0:23; per cases; suppose len f=0; then Seg len f = {}; then for i,j st [i,j] in Indices (Lf+Lg) holds (Lf+Lg)*(i,j) = Lfg*(i,j) by A7,A8,ZFMISC_1:90; hence thesis by A4,A1,A6,A7,A8,A5,MATRIX_0:21; end; suppose A9: len f>0; A10: dom Lf=Seg 1 & 1 in Seg 1 by A1,FINSEQ_1:def 3; len f in Seg len f by A9,FINSEQ_1:3; then [1,len f] in Indices Lf by A8,A10,ZFMISC_1:87; then Line(Lf+Lg,1) = Line(Lf,1)+Line(Lg,1) by A3,MATRIX_0:23,MATRIX_4:59 .= f+Line(Lg,1) by Th25 .= f+g by Th25; hence thesis by A1,A6,Th25; end; end; theorem Th28: len f = len g implies (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g) proof set Cf=ColVec2Mx f; set Cg=ColVec2Mx g; A1: len Cf=len f by MATRIX_0:def 2; assume A2: len f = len g; then reconsider F=f,G=g as Element of (len f)-tuples_on the carrier of K by FINSEQ_2:92; A3: len Cg=len f by A2,MATRIX_0:def 2; set FG=F+G; set Cfg=ColVec2Mx FG; A4: len Cfg=len FG by MATRIX_0:def 2; A5: len FG=len f & width (Cf+Cg)=width Cf by CARD_1:def 7,MATRIX_3:def 3; A6: len (Cf+Cg)=len Cf by MATRIX_3:def 3; per cases; suppose A7: len f=0; then Cf+Cg={} by A6,MATRIX_0:def 2; hence thesis by A4,A7; end; suppose A8: len f>0; A9: dom Cf=Seg len f & 1 in Seg 1 by A1,FINSEQ_1:def 3; A10: width Cf= 1 by A8,MATRIX_0:23; len f in Seg len f by A8,FINSEQ_1:3; then [len f,1] in Indices Cf by A9,A10,ZFMISC_1:87; then Col(Cf+Cg,1) = Col(Cf,1)+Col(Cg,1) by A1,A3,MATRIX_4:60 .= f+Col(Cg,1) by A8,Th26 .= f+g by A2,A8,Th26; hence thesis by A5,A8,A10,Th26; end; end; theorem a * LineVec2Mx f =LineVec2Mx (a*f) proof A1: len (a*LineVec2Mx f)=len (LineVec2Mx f) by MATRIX_3:def 5; A2: len (LineVec2Mx f)=1 by MATRIX_0:def 2; then Line(a * LineVec2Mx f,1) = a*Line(LineVec2Mx f,1) by MATRIXR1:20 .= a*f by Th25; hence thesis by A2,A1,Th25; end; theorem Th30: a * ColVec2Mx f = ColVec2Mx (a*f) proof A1: len f=len (a*f) by MATRIXR1:16; per cases; suppose A2: len f=0; len (ColVec2Mx f)=len (a*ColVec2Mx f) by MATRIX_3:def 5; then A3: a * ColVec2Mx f = {} by A2,MATRIX_0:def 2; len (ColVec2Mx (a*f))= 0 by A1,A2,MATRIX_0:def 2; hence thesis by A3; end; suppose A4: len f>0; A5: width (a*ColVec2Mx f)=width ColVec2Mx f by MATRIX_3:def 5; A6: width ColVec2Mx f=1 by A4,MATRIX_0:23; then Col(a * ColVec2Mx f,1) = a*Col(ColVec2Mx f,1) by MATRIXR1:19 .= a*f by A4,Th26; hence thesis by A1,A4,A6,A5,Th26; end; end; theorem LineVec2Mx (k|->0.K) = 0.(K,1,k) proof card(k|->0.K) = k by CARD_1:def 7; then reconsider L=LineVec2Mx (k|->0.K) as Matrix of 1,k,K; set Z=0.(K,1,k); now A1: width L=k by MATRIX_0:23; A2: dom L = Seg len L & len L=1 by FINSEQ_1:def 3,MATRIX_0:def 2; let i,j such that A3: [i,j] in Indices L; A4: j in Seg width L by A3,ZFMISC_1:87; i in dom L by A3,ZFMISC_1:87; then A5: i=1 by A2,FINSEQ_1:2,TARSKI:def 1; Indices Z=Indices L by MATRIX_0:26; hence Z*(i,j) = 0.K by A3,MATRIX_3:1 .= (k|->0.K).j by A4,A1,FINSEQ_2:57 .= Line(L,i).j by A5,Th25 .= L*(i,j) by A4,MATRIX_0:def 7; end; hence thesis by MATRIX_0:27; end; theorem Th32: ColVec2Mx (k|->0.K) = 0.(K,k,1) proof card(k|->0.K) = k by CARD_1:def 7; then reconsider C=ColVec2Mx (k|->0.K) as Matrix of k,1,K; set Z=0.(K,k,1); now A1: len (k|->0.K)=k by CARD_1:def 7; let i,j such that A2: [i,j] in Indices C; A3: i in dom C by A2,ZFMISC_1:87; A4: j in Seg width C by A2,ZFMISC_1:87; A5: dom C=Seg len C & len C=len (k|->0.K) by FINSEQ_1:def 3,MATRIX_0:def 2; then width C=1 by A3,A1,Th26; then A6: j=1 by A4,FINSEQ_1:2,TARSKI:def 1; Indices Z=Indices C by MATRIX_0:26; hence Z*(i,j) = 0.K by A2,MATRIX_3:1 .= (k|->0.K).i by A3,A5,A1,FINSEQ_2:57 .= Col(C,j).i by A3,A5,A1,A6,Th26 .= C*(i,j) by A3,MATRIX_0:def 8; end; hence thesis by MATRIX_0:27; end; begin :: Basis properties of the Solution of Linear Equations definition let K; let A,B; func Solutions_of(A,B) -> set equals {X : len X = width A & width X = width B & A * X = B}; coherence; end; theorem Th33: Solutions_of(A,B) is non empty implies len A = len B proof assume Solutions_of(A,B) is non empty; then consider x being object such that A1: x in Solutions_of(A,B); 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; set LB0=len B |-> 0.K; consider X1 such that A4: X = X1 and A5: len X1 = width A and A6: width X1 = width B and A7: A * X1 = B by A1; A8: now let k such that A9: 1 <=k & k <= len B; A10: k in Seg len B by A9; Indices B=[:Seg len B,Seg width B:] by FINSEQ_1:def 3; then [k,i] in Indices B by A2,A4,A6,A10,ZFMISC_1:87; then A11: B*(k,i) = Line(A,k) "*" Col(X1,i) by A5,A7,MATRIX_3:def 4 .= Sum(0.K*Line(A,k)) by A3,A4,A5,FVSUM_1:66 .= 0.K* Sum(Line(A,k)) by FVSUM_1:73 .= 0.K .= LB0.k by A10,FINSEQ_2:57; k in dom B by A10,FINSEQ_1:def 3; hence (Col(B,i)).k=LB0.k by A11,MATRIX_0:def 8; end; len Col(B,i) = len B & len LB0 = len B by CARD_1:def 7; hence thesis by A8; 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 A1: width (a*B) = width B & width (a*A)=width A by MATRIX_3:def 5; assume X in Solutions_of(A,B); then consider X1 such that A2: X = X1 & len X1 = width A and A3: width X1 = width B & A * X1 = B; A4: len (a*X) = width A & width (a*X) = width X1 by A2,MATRIX_3:def 5; A*(a*X)=a*(A*X) & (a*A)*X=a*(A*X) by A2,Th1,MATRIXR1:22; hence thesis by A2,A3,A4,A1; 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 be object 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; A3: a"*(a*A) = (a"*a)*A by Th2 .= 1_K *A by A1,VECTSP_1:def 10 .= A by Th2; A4: a"*(a*B) = (a"*a)*B by Th2 .= 1_K*B by A1,VECTSP_1:def 10 .= B by Th2; let x be object such that A5: x in Solutions_of(a*A,a*B); ex X st x=X & len X = width (a*A) & width X = width (a* B) & (a*A) * X = (a*B) by A5; hence thesis by A5,A3,A4,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 and A2: width A = 0 and A3: width B = 0; Seg width A = {} by A2; then Indices A = {} by ZFMISC_1:90; then for i,j st [i,j] in Indices A holds A*(i,j) = B*(i,j); hence thesis by A1,A2,A3,MATRIX_0: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) and A2: X2 in Solutions_of(A,B2) and A3: width B1 = width B2; A4: ex Y1 be Matrix of K st Y1 = X1 & len Y1 = width A & width Y1 = width B1 & A * Y1 = B1 by A1; A5: width (X1+X2) = width X1 by MATRIX_3:def 3; A6: len (X1+X2) = len X1 by MATRIX_3:def 3; A7: ex Y2 be Matrix of K st Y2 = X2 & len Y2 = width A & width Y2 = width B2 & A * Y2 = B2 by A2; A8: now per cases; suppose A9: len A=0; then len (A*X1) = 0 by A4,MATRIX_3:def 4; then A10: len (A*X1 + A*X2) = 0 by MATRIX_3:def 3; len (A*(X1+X2)) = 0 by A4,A6,A9,MATRIX_3:def 4; hence A*(X1+X2) = A*X1 + A*X2 by A10; end; suppose len X1=0; then width (A*X1)=0 by A4,MATRIX_0:def 3; then A11: width (A*X1 + A*X2)=0 & width (A*(X1+X2)) = 0 by A4,A6,A5,MATRIX_3:def 3 ,def 4; len (A*X1)=len A by A4,MATRIX_3:def 4; then A12: len (A*X1+A*X2)=len A by MATRIX_3:def 3; len (A*(X1+X2))= len A by A4,A6,MATRIX_3:def 4; hence A*(X1+X2)=A*X1+A*X2 by A12,A11,Lm3; end; suppose len A>0 & len X1>0; hence A*(X1+X2)=A*X1 + A*X2 by A3,A4,A7,MATRIX_4:62; end; end; width (B1+B2) = width B1 by MATRIX_3:def 3; hence thesis by A4,A7,A6,A5,A8; end; theorem Th38: X in Solutions_of(A9,B9) implies X in Solutions_of(RLine(A9,i,a* Line(A9,i)),RLine(B9,i,a*Line(B9,i))) proof set LA=Line(A9,i); set LB=Line(B9,i); set RA=RLine(A9,i,a*LA); set RB=RLine(B9,i,a*LB); A1: Indices RB=Indices B9 by MATRIX_0:26; A2: len (a*LB)=len LB & len LB=width B9 by CARD_1:def 7,MATRIXR1:16; then A3: width RB=width B9 by MATRIX11:def 3; A4: len (a*LA)=len LA & len LA= width A9 by CARD_1:def 7,MATRIXR1:16; then A5: len RA=len A9 by MATRIX11:def 3; assume A6: X in Solutions_of(A9,B9); then consider X1 be Matrix of K such that A7: X = X1 and A8: len X1 = width A9 and A9: width X1 = width B9 and A10: A9 * X1 = B9; set RX=RA*X1; A11: width RA=width A9 by A4,MATRIX11:def 3; then A12: len RX=len RA & width RX=width X1 by A8,MATRIX_3:def 4; A13: len A9=len B9 by A6,Th33; then dom B9=Seg len RA by A5,FINSEQ_1:def 3; then A14: Indices RX=Indices B9 by A9,A12,FINSEQ_1:def 3; A15: now len B9=m by MATRIX_0:def 2; then A16: dom B9=Seg m by FINSEQ_1:def 3; let j,k such that A17: [j,k] in Indices RB; A18: j in dom B9 by A1,A17,ZFMISC_1:87; A19: k in Seg width B9 by A1,A17,ZFMISC_1:87; then B9*(i,k)=LB.k by MATRIX_0:def 7; then reconsider LBk=LB.k as Element of K; A20: B9*(j,k)= Line(A9,j) "*" Col(X1,k) by A8,A10,A1,A17,MATRIX_3:def 4; now per cases; suppose A21: j=i; then Line(RA,i)=a*LA by A4,A18,A16,MATRIX11:28; hence RX*(j,k) = (a*LA)"*"Col(X1,k) by A8,A11,A14,A1,A17,A21, MATRIX_3:def 4 .= Sum(a*mlt(LA,Col(X1,k))) by A8,FVSUM_1:68 .= a*Sum(mlt(LA,Col(X1,k))) by FVSUM_1:73 .= a*LBk by A19,A20,A21,MATRIX_0:def 7 .= (a*LB).k by A19,FVSUM_1:51 .= RB*(j,k) by A2,A1,A17,A21,MATRIX11:def 3; end; suppose A22: j<>i; then Line(RA,j)=Line(A9,j) by A18,A16,MATRIX11:28; hence RX*(j,k) = Line(A9,j)"*"Col(X1,k) by A8,A11,A14,A1,A17, MATRIX_3:def 4 .= B9*(j,k) by A8,A10,A1,A17,MATRIX_3:def 4 .= RB*(j,k) by A2,A1,A17,A22,MATRIX11:def 3; end; end; hence RB*(j,k) = RX*(j,k); end; len RB=len B9 by A2,MATRIX11:def 3; then RX=RB by A9,A13,A5,A3,A12,A15,MATRIX_0:21; hence thesis by A7,A8,A9,A11,A3; end; Lm4: a <> 0.K implies Solutions_of(A9,B9) = Solutions_of(RLine(A9,i,a*Line(A9, i)),RLine(B9,i,a*Line(B9,i))) proof assume A1: a <> 0.K; set RB=RLine(B9,i,a*Line(B9,i)); set RA=RLine(A9,i,a*Line(A9,i)); thus Solutions_of(A9,B9) c= Solutions_of(RA,RB) proof let x be object such that A2: x in Solutions_of(A9,B9); ex X st x=X & len X = width A9 & width X = width B9 & A9 * X = B9 by A2; hence thesis by A2,Th38; end; let x be object such that A3: x in Solutions_of(RA,RB); per cases; suppose A4: not i in Seg m; len A9=m by MATRIX_0:def 2; then len B9=m & RA=A9 by A4,MATRIX13:40,MATRIX_0:def 2; hence thesis by A3,A4,MATRIX13:40; end; suppose A5: i in Seg m; reconsider aLA=a*Line(A9,i),aLB=a*Line(B9,i),aLAR=a"*Line(RA,i), aLBR=a"* Line(RB,i) as Element of (the carrier of K)* by FINSEQ_1:def 11; set RRB=RLine(RB,i,a"*Line(RB,i)); set RRA=RLine(RA,i,a"*Line(RA,i)); A6: ex X st x=X & len X = width RA & width X = width RB & RA * X = RB by A3; A7: len (a*Line(A9,i))=width A9 by CARD_1:def 7; then A8: a"*Line(RA,i) = a"*(a*Line(A9,i)) by A5,MATRIX11:28 .= (a"*a)*Line(A9,i) by FVSUM_1:54 .= 1_K * Line(A9,i) by A1,VECTSP_1:def 10 .= Line(A9,i) by FVSUM_1:57; A9: len (a*Line(B9,i))=width B9 by CARD_1:def 7; then A10: a"*Line(RB,i) = a"*(a*Line(B9,i)) by A5,MATRIX11:28 .= (a"*a)*Line(B9,i) by FVSUM_1:54 .= 1_K * Line(B9,i) by A1,VECTSP_1:def 10 .= Line(B9,i) by FVSUM_1:57; A11: width RB=width B9 by A9,MATRIX11:def 3; A12: len (a"*Line(RB,i))=width RB by CARD_1:def 7; then A13: RRB = Replace(RB,i,aLBR) by MATRIX11:29 .= Replace(Replace(B9,i,aLB),i,aLBR) by A9,MATRIX11:29 .= Replace(B9,i,aLBR) by FUNCT_7:34 .= RLine(B9,i,Line(B9,i)) by A12,A11,A10,MATRIX11:29 .= B9 by MATRIX11:30; A14: width RA=width A9 by A7,MATRIX11:def 3; A15: len (a"*Line(RA,i))=width RA by CARD_1:def 7; then RRA = Replace(RA,i,aLAR) by MATRIX11:29 .= Replace(Replace(A9,i,aLA),i,aLAR) by A7,MATRIX11:29 .= Replace(A9,i,aLAR) by FUNCT_7:34 .= RLine(A9,i,Line(A9,i)) by A15,A14,A8,MATRIX11:29 .= A9 by MATRIX11:30; hence thesis by A3,A6,A13,Th38; end; end; theorem Th39: X in Solutions_of(A9,B9) & j in Seg m implies X in Solutions_of( RLine(A9,i,Line(A9,i) + a*Line(A9,j)), RLine(B9,i,Line(B9,i) + a*Line(B9,j))) proof assume that A1: X in Solutions_of(A9,B9) and A2: j in Seg m; consider X1 such that A3: X = X1 and A4: len X1 = width A9 and A5: width X1 = width B9 and A6: A9 * X1 = B9 by A1; set LAj=Line(A9,j); set LAi=Line(A9,i); set RA=RLine(A9,i,LAi+a*LAj); A7: len (LAi+a*LAj) = width A9 by CARD_1:def 7; then A8: len RA = len A9 by MATRIX11:def 3; set RX=RA*X1; A9: width RA = width A9 by A7,MATRIX11:def 3; then A10: len RX = len RA & width RX=width X1 by A4,MATRIX_3:def 4; A11: len A9 = len B9 by A1,Th33; then dom B9=Seg len RA by A8,FINSEQ_1:def 3; then A12: Indices RX = Indices B9 by A5,A10,FINSEQ_1:def 3; set LBj=Line(B9,j); set LBi=Line(B9,i); set RB=RLine(B9,i,LBi+a*LBj); A13: Indices RB = Indices B9 by MATRIX_0:26; A14: len (LBi+a*LBj) = width B9 by CARD_1:def 7; then A15: width RB = width B9 by MATRIX11:def 3; A16: len (a*LAj) = width A9 & len LAi = width A9 by CARD_1:def 7; A17: now A18: rng (a*LBj) c= the carrier of K by FINSEQ_1:def 4; let o,p be Nat such that A19: [o,p] in Indices RB; A20: o in dom B9 by A13,A19,ZFMISC_1:87; A21: B9*(o,p) = Line(A9,o) "*" Col(X1,p) by A4,A6,A13,A19,MATRIX_3:def 4; reconsider CX=Col(X1,p) as Element of (width A9)-tuples_on the carrier of K by A4; A22: len Col(X1,p)=width A9 by A4,MATRIX_0:def 8; A23: p in Seg width B9 by A13,A19,ZFMISC_1:87; then B9*(o,p)=Line(B9,o).p & B9*(j,p)=LBj.p by MATRIX_0:def 7; then reconsider LBop = Line(B9,o).p,LBjp = LBj.p as Element of the carrier of K; p in dom (a*LBj) by A23,FINSEQ_2:124; then (a*LBj).p in rng (a*LBj) by FUNCT_1:def 3; then reconsider aLBjp=(a*Line(B9,j)).p as Element of K by A18; len B9 = m by MATRIX_0:def 2; then A24: dom B9=Seg m by FINSEQ_1:def 3; then [j,p] in Indices B9 by A2,A23,ZFMISC_1:87; then A25: B9*(j,p) = LAj"*"Col(X1,p ) by A4,A6,MATRIX_3:def 4; now per cases; suppose A26: o=i; then Line(RA,o)=LAi+a*LAj by A7,A20,A24,MATRIX11:28; hence RX*(o,p) = (LAi+a*LAj) "*" CX by A4,A9,A12,A13,A19,MATRIX_3:def 4 .= Sum(mlt(LAi,CX)+mlt(a*LAj,CX)) by A16,A22,MATRIX_4:56 .= Sum(mlt(LAi,CX)+a*mlt(LAj,CX)) by FVSUM_1:68 .= Sum(mlt(LAi,CX))+Sum(a*mlt(LAj,CX)) by FVSUM_1:76 .= B9*(o,p)+a*(B9*(j,p)) by A21,A25,A26,FVSUM_1:73 .= LBop+a*(B9*(j,p)) by A23,MATRIX_0:def 7 .= LBop+a*LBjp by A23,MATRIX_0:def 7 .= LBop+aLBjp by A23,FVSUM_1:51 .= (LBi+a*LBj).p by A23,A26,FVSUM_1:18 .= RB*(o,p) by A14,A13,A19,A26,MATRIX11:def 3; end; suppose A27: o<>i; then Line(RA,o)=Line(A9,o) by A20,A24,MATRIX11:28; hence RX*(o,p) = Line(A9,o)"*"Col(X1,p) by A4,A9,A12,A13,A19, MATRIX_3:def 4 .= B9*(o,p) by A4,A6,A13,A19,MATRIX_3:def 4 .= RB*(o,p) by A14,A13,A19,A27,MATRIX11:def 3; end; end; hence RB*(o,p) = RX*(o,p); end; len RB = len B9 by A14,MATRIX11:def 3; then RX=RB by A5,A11,A8,A15,A10,A17,MATRIX_0:21; hence thesis by A3,A4,A5,A9,A15; end; Lm5: j in Seg m & i <> j implies Solutions_of(A9,B9) = Solutions_of(RLine(A9,i ,Line(A9,i) + a*Line(A9,j)), RLine(B9,i,Line(B9,i) + a*Line(B9,j))) proof assume that A1: j in Seg m and A2: i <> j; set LB=Line(B9,j); set LA=Line(A9,j); set RA=RLine(A9,i,Line(A9,i) + a*LA); set RB=RLine(B9,i,Line(B9,i) + a*LB); thus Solutions_of(A9,B9) c= Solutions_of(RA,RB) proof let x be object such that A3: x in Solutions_of(A9,B9); ex X st x=X & len X = width A9 & width X = width B9 & A9 * X = B9 by A3; hence thesis by A1,A3,Th39; end; let x be object such that A4: x in Solutions_of(RA,RB); per cases; suppose A5: not i in Seg m; len A9=m by MATRIX_0:def 2; then len B9=m & RA=A9 by A5,MATRIX13:40,MATRIX_0:def 2; hence thesis by A4,A5,MATRIX13:40; end; suppose A6: i in Seg m; reconsider LLA=Line(A9,i)+a*LA,LLB=Line(B9,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; set RRB=RLine(RB,i,Line(RB,i)+(-a)*Line(RB,j)); set RRA=RLine(RA,i,Line(RA,i)+(-a)*Line(RA,j)); A7: ex X st x=X & len X = width RA & width X = width RB & RA * X = RB by A4; A8: Line(RB,j)=LB by A1,A2,MATRIX11:28; A9: len (Line(B9,i)+a*LB)=width B9 by CARD_1:def 7; then A10: width RB=width B9 by MATRIX11:def 3; Line(RB,i)=Line(B9,i)+a*LB by A6,A9,MATRIX11:28; then A11: Line(RB,i)+(-a)*Line(RB,j)= Line(B9,i)+a*LB+(-1_K*a)*LB by A8 .= Line(B9,i)+a*LB+((-1_K)*a)*LB by VECTSP_1:9 .= Line(B9,i)+a*LB+(-1_K)*(a*LB) by FVSUM_1:54 .= Line(B9,i)+a*LB+(-(a*LB)) by FVSUM_1:59 .= Line(B9,i)+(a*LB+(-(a*LB))) by FINSEQOP:28 .= Line(B9,i)+width B9|->0.K by FVSUM_1:26 .= Line(B9,i) by FVSUM_1:21; A12: len (Line(RB,i)+(-a)*Line(RB,j))=width RB by CARD_1:def 7; then A13: RRB = Replace(RB,i,LLRB) by MATRIX11:29 .= Replace(Replace(B9,i,LLB),i,LLRB) by A9,MATRIX11:29 .= Replace(B9,i,LLRB) by FUNCT_7:34 .= RLine(B9,i,Line(RB,i)+(-a)*Line(RB,j)) by A12,A10,MATRIX11:29 .= B9 by A11,MATRIX11:30; A14: Line(RA,j)=LA by A1,A2,MATRIX11:28; A15: len (Line(A9,i)+a*LA)=width A9 by CARD_1:def 7; then A16: width RA=width A9 by MATRIX11:def 3; Line(RA,i)=Line(A9,i)+a*LA by A6,A15,MATRIX11:28; then A17: Line(RA,i)+(-a)*Line(RA,j)= Line(A9,i)+a*LA+(-1_K*a)*LA by A14 .= Line(A9,i)+a*LA+((-1_K)*a)*LA by VECTSP_1:9 .= Line(A9,i)+a*LA+(-1_K)*(a*LA) by FVSUM_1:54 .= Line(A9,i)+a*LA+(-(a*LA)) by FVSUM_1:59 .= Line(A9,i)+(a*LA+(-(a*LA))) by FINSEQOP:28 .= Line(A9,i)+width A9|->0.K by FVSUM_1:26 .= Line(A9,i) by FVSUM_1:21; A18: len (Line(RA,i)+(-a)*Line(RA,j))=width RA by CARD_1:def 7; then RRA = Replace(RA,i,LLRA) by MATRIX11:29 .= Replace(Replace(A9,i,LLA),i,LLRA) by A15,MATRIX11:29 .= Replace(A9,i,LLRA) by FUNCT_7:34 .= RLine(A9,i,Line(RA,i)+(-a)*Line(RA,j)) by A18,A16,MATRIX11:29 .= A9 by A17,MATRIX11:30; hence thesis by A1,A4,A7,A13,Th39; end; end; theorem Th40: j in Seg m & (i = j implies a <> -1_K) implies Solutions_of(A9, B9) = Solutions_of(RLine(A9,i,Line(A9,i) + a*Line(A9,j)), RLine(B9,i,Line(B9,i) + a*Line(B9,j))) proof assume that A1: j in Seg m and A2: i = j implies a <> -1_K; per cases; suppose i<>j; hence thesis by A1,Lm5; end; suppose A3: i=j; A4: 1_K+a <> 0.K proof assume 1_K+a=0.K; then -1.K = -1.K+(1_K+a) by RLVECT_1:def 4 .= (-1.K+1_K)+a by RLVECT_1:def 3 .= 0.K+a by VECTSP_1:19 .= a by RLVECT_1:def 4; hence thesis by A2,A3; end; set LB=Line(B9,i); set LA=Line(A9,i); A5: LB+a*LB = 1_K*LB+a*LB by FVSUM_1:57 .= (1_K+a)*LB by FVSUM_1:55; LA+a*LA = 1_K*LA+a*LA by FVSUM_1:57 .= (1_K+a)*LA by FVSUM_1:55; hence thesis by A3,A4,A5,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 and A3: Line(A,i) = width A|->0.K; set wB0=width B |->0.K; set LB=Line(B,i); A4: len LB=width B by CARD_1:def 7; A5: ex X1 be Matrix of K st X = X1 & len X1 = width A & width X1 = width B & A * X1 = B by A1; A6: now let k such that A7: 1 <=k & k <= len LB; A8: k in Seg width B by A4,A7; len A=len B by A1,Th33; then dom A=Seg len B by FINSEQ_1:def 3; then i in dom B by A2,FINSEQ_1:def 3; then [i,k] in Indices B by A8,ZFMISC_1:87; then B*(i,k) = Line(A,i) "*" Col(X,k) by A5,MATRIX_3:def 4 .= Sum(0.K*Col(X,k)) by A3,A5,FVSUM_1:66 .= 0.K*Sum(Col(X,k)) by FVSUM_1:73 .= 0.K .= wB0.k by A8,FINSEQ_2:57; hence wB0.k = LB.k by A8,MATRIX_0:def 7; end; len wB0=width B by CARD_1:def 7; hence thesis by A4,A6; 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; set S=Seg width A; A1: rng Sgm S=S by FINSEQ_1:def 13; len Line(A,nt.i)=width A by MATRIX_0:def 7; then A2: dom Line(A,nt.i)=S by FINSEQ_1:def 3; Sgm S = idseq width A by FINSEQ_3:48; then A3: Line(A,nt.i) * Sgm S = Line(A,nt.i) by A2,RELAT_1:52; assume i in Seg n; hence thesis by A3,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 and A2: n>0; set SA=Segm(A,nt,Sgm Seg width A); A3: len SA=n by A2,MATRIX_0:23; width SA=card Seg width A by A2,MATRIX_0:23; then A4: width SA=width A by FINSEQ_1:57; set SB=Segm(B,nt,Sgm Seg width B); A5: len SB=n by A2,MATRIX_0:23; width SB=card Seg width B by A2,MATRIX_0:23; then A6: width SB=width B by FINSEQ_1:57; let x be object such that A7: x in Solutions_of(A,B); consider X be Matrix of K such that A8: x = X and A9: len X = width A and A10: width X = width B and A11: A * X = B by A7; set SX=SA*X; A12: len A = len B by A7,Th33; A13: now A14: len SX=len SA by A9,A4,MATRIX_3:def 4; let j,k such that A15: [j,k] in Indices SX; j in dom SX by A15,ZFMISC_1:87; then A16: j in Seg n by A3,A14,FINSEQ_1:def 3; width SX=width X by A9,A4,MATRIX_3:def 4; then A17: k in Seg width B by A10,A15,ZFMISC_1:87; dom nt=Seg n by FINSEQ_2:124; then nt.j in rng nt by A16,FUNCT_1:def 3; then A18: nt.j in dom A by A1; dom A=Seg len B by A12,FINSEQ_1:def 3; then nt.j in dom B by A18,FINSEQ_1:def 3; then A19: [nt.j,k] in Indices B by A17,ZFMISC_1:87; reconsider j9=j,k9=k as Element of NAT by ORDINAL1:def 12; Sgm Seg width B=idseq width B by FINSEQ_3:48; then A20: (Sgm Seg width B).k9=k by A17,FINSEQ_2:49; j in dom SB by A5,A16,FINSEQ_1:def 3; then A21: [j,k] in Indices SB by A6,A17,ZFMISC_1:87; Line(SA,j)=Line(A,nt.j) by A16,Lm6; hence SX*(j,k) = Line(A,nt.j) "*" Col(X,k) by A9,A4,A15,MATRIX_3:def 4 .= B*(nt.j9,k) by A9,A11,A19,MATRIX_3:def 4 .= SB*(j,k) by A21,A20,MATRIX13:def 1; end; len SX=len SA & width SX=width X by A9,A4,MATRIX_3:def 4; then SX=SB by A10,A3,A5,A6,A13,MATRIX_0:21; hence thesis by A8,A9,A10,A4,A6; 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 and A2: dom A=dom B and A3: n>0 and A4: 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 SB=Segm(B,nt,Sgm Seg width B); set SA=Segm(A,nt,Sgm Seg width A); A5: Solutions_of(SA,SB) c= Solutions_of(A,B) proof A6: Seg len A = dom B by A2,FINSEQ_1:def 3; A7: width SB=card Seg width B by A3,MATRIX_0:23; then A8: width SB=width B by FINSEQ_1:57; let x be object; assume x in Solutions_of(SA,SB); then consider X be Matrix of K such that A9: x = X and A10: len X = width SA and A11: width X = width SB and A12: SA * X = SB; set AX=A*X; width SA=card Seg width A by A3,MATRIX_0:23; then A13: width SA=width A by FINSEQ_1:57; then A14: width AX = width X by A10,MATRIX_3:def 4; A15: len AX = len A by A10,A13,MATRIX_3:def 4; A16: now A17: dom AX=Seg len A by A15,FINSEQ_1:def 3; let j,k such that A18: [j,k] in Indices AX; A19: k in Seg width AX by A18,ZFMISC_1:87; reconsider j9=j,k9=k as Element of NAT by ORDINAL1:def 12; A20: j in dom AX by A18,ZFMISC_1:87; now per cases; suppose A21: j9 in rng nt; A22: dom nt=Seg n by FINSEQ_2:124; Sgm Seg width B=idseq width B by FINSEQ_3:48; then A23: (Sgm Seg width B).k9=k by A11,A8,A14,A19,FINSEQ_2:49; consider p be object such that A24: p in dom nt and A25: nt.p=j9 by A21,FUNCT_1:def 3; reconsider p as Element of NAT by A24; Indices SB =[:Seg n,Seg card Seg width B:] by A3,MATRIX_0:23; then A26: [p,k] in Indices SB by A11,A7,A14,A19,A24,A22,ZFMISC_1:87; Line(SA,p) = Line(A,j9) by A24,A25,A22,Lm6; hence AX*(j,k) = Line(SA,p)"*"Col(X,k) by A10,A13,A18,MATRIX_3:def 4 .= SB*(p,k9) by A10,A12,A26,MATRIX_3:def 4 .= B*(j,k) by A25,A26,A23,MATRIX13:def 1; end; suppose not j9 in rng nt; then A27: j9 in (dom A)\rng nt by A2,A6,A20,A17,XBOOLE_0:def 5; then A28: Line(B,j) = width B|->0.K by A4; Line(A,j) = width A|->0.K by A4,A27; hence AX*(j,k) = (width A|-> 0.K)"*"Col(X,k) by A10,A13,A18, MATRIX_3:def 4 .= Sum(0.K*Col(X,k)) by A10,A13,FVSUM_1:66 .= 0.K*Sum(Col(X,k)) by FVSUM_1:73 .= 0.K .= Line(B,j).k by A11,A8,A14,A19,A28,FINSEQ_2:57 .= B*(j,k) by A11,A8,A14,A19,MATRIX_0:def 7; end; end; hence AX*(j,k)=B*(j,k); end; len AX = len B by A15,A6,FINSEQ_1:def 3; then AX = B by A11,A7,A14,A16,FINSEQ_1:57,MATRIX_0:21; hence thesis by A9,A10,A11,A13,A8; end; Solutions_of(A,B) c= Solutions_of(SA,SB) by A1,A3,Th42; hence thesis by A5; 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 and A2: N is non empty; dom A=Seg len A by FINSEQ_1:def 3; then rng Sgm N = N by A1,FINSEQ_1:def 13; hence thesis by A1,A2,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 and A2: 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; dom A=Seg len A by FINSEQ_1:def 3; then rng Sgm N = N 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 that A1: i in dom A and A2: len A > 1; reconsider l1=len A-1 as Element of NAT by A2,NAT_1:20; A3: l1 > 1-1 by A2,XREAL_1:9; A4: Seg len A=dom A by FINSEQ_1:def 3; card Seg len A=l1+1 by FINSEQ_1:57; then card ((Seg len A)\{i})=l1 by A1,A4,STIRL2_1:55; then A5: 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 A4,A3,Th44,CARD_1:27,XBOOLE_1:36; let x be object such that A6: x in Solutions_of(A,B); len A=len B by A6,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 A5,A6; 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 and A2: len A > 1 and A3: Line(A,i) = width A |-> 0.K and A4: i in dom B and A5: Line(B,i) = width B |-> 0.K; reconsider l1=len A-1 as Element of NAT by A2,NAT_1:20; A6: l1 > 1-1 by A2,XREAL_1:9; thus Solutions_of(A,B) c= Solutions_of(DelLine(A,i),DelLine(B,i)) by A1,A2 ,Th46; let x be object such that A7: x in Solutions_of(DelLine(A,i),DelLine(B,i)); set S=Seg len A; A8: dom A=S by FINSEQ_1:def 3; A9: now let j; assume j in (dom A)\(S\{i}); then j in dom A /\{i} by A8,XBOOLE_1:48; then j in {i} by XBOOLE_0:def 4; hence Line(A,j) = width A |-> 0.K & Line(B,j) = width B |-> 0.K by A3,A5, TARSKI:def 1; end; card S=l1+1 by FINSEQ_1:57; then A10: card (S\{i})=l1 by A1,A8,STIRL2_1:55; (ex mA be Nat st len A = mA + 1 & len Del(A,i) = mA )& ex mB be Nat st len B = mB + 1 & len Del(B,i) = mB by A1,A4,FINSEQ_3:104; then A11: len B=len A by A7,Th33; then dom A=dom B by A8,FINSEQ_1:def 3; then Solutions_of(A,B) = Solutions_of(Segm(A,S\{i},Seg width A),Segm(B,S\{i} ,Seg width B)) by A8,A10,A6,A9,Th45,CARD_1:27,XBOOLE_1:36 .= Solutions_of(DelLine(A,i),Segm(B,S\{i},Seg width B)) by MATRIX13:51 .= Solutions_of(DelLine(A,i),DelLine(B,i)) by A11,MATRIX13:51; hence thesis by A7; 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 set IDn=idseq n; len IDn=n & IDn is FinSequence of NAT by CARD_1:def 7,FINSEQ_2:48; then reconsider IDn as Element of n-tuples_on NAT by FINSEQ_2:92; let A be Matrix of n,m,K, B be Matrix of n,k,K; let P be Function of Seg n,Seg n; A1: rng P c= Seg n by RELAT_1:def 19; dom IDn=Seg n; then reconsider IDnP=IDn*P as FinSequence of NAT by FINSEQ_2:47; dom P=Seg n by FUNCT_2:52; then n in NAT & dom IDnP = Seg n by A1,ORDINAL1:def 12,RELAT_1:53; then len IDnP = n by FINSEQ_1:def 3; then reconsider IDnP as Element of n-tuples_on NAT by FINSEQ_2:92; A2: n=len A by MATRIX_0:def 2; A3: (idseq n)*P = P by A1,RELAT_1:53; then A4: rng IDnP c=dom A by A1,A2,FINSEQ_1:def 3; A5: IDn=Sgm Seg n & card Seg n=n by FINSEQ_1:57,FINSEQ_3:48; then A6: Segm(A,IDnP,Sgm Seg width A) = Segm(A,Seg len A,Seg width A) * P by A2, MATRIX13:33 .= A*P by MATRIX13:46; A7: len B=n by MATRIX_0:def 2; then A8: Segm(B,IDnP,Sgm Seg width B) = Segm(B,Seg len B,Seg width B) * P by A5, MATRIX13:33 .= B*P by MATRIX13:46; per cases; suppose A9: n>0; hence Solutions_of(A,B)c=Solutions_of(A*P,B*P) by A6,A8,A4,Th42; A10: card Seg n = card Seg n; A11: dom A=Seg n by A2,FINSEQ_1:def 3; A12: dom B=Seg n by A7,FINSEQ_1:def 3; assume P is one-to-one; then P is onto by A10,STIRL2_1:60; then rng P=Seg n by FUNCT_2: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,A11,XBOOLE_1:37; hence thesis by A1,A3,A6,A8,A9,A11,A12,Th43; end; suppose A13: n=0; then len B=0 by MATRIX_0:22; then A14: B={}; len A=0 by A13,MATRIX_0:22; then A15: A={}; A*P={} by A13; hence thesis by A15,A14; 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 and A2: N c= Seg m and A3: Segm(A,Seg n,N) = 1.(K,n) and A4: n>0; set SN=Seg m\N; A5: m-'n=0 or m-'n > 0; A6: card Seg m = m by FINSEQ_1:57; then A7: card SN=m-n by A1,A2,CARD_2:44; set ZERO=0.(K,m-'n,m); A8: SN c= Seg m by XBOOLE_1:36; A9: now per cases; suppose m-'n=0; then Seg (m-'n) = {}; then [:Seg (m-'n),N:] = {} & [:Seg (m-'n),SN:] ={} by ZFMISC_1:90; hence [:Seg (m-'n),N:]c=Indices ZERO & [:Seg (m-'n),SN:]c=Indices ZERO; end; suppose m-'n>0; then Indices ZERO = [:Seg (m-'n),Seg m:] by MATRIX_0:23; hence [:Seg (m-'n),N:]c=Indices ZERO & [:Seg (m-'n),SN:]c=Indices ZERO by A2,A8 ,ZFMISC_1:96; end; end; set SA=Segm(A,Seg n,SN); card Seg n = n by FINSEQ_1:57; then A10: len SA=n by A4,MATRIX_0:23; A11: len (SA@)=len (-SA@) & width (SA@)=width (-SA@) by MATRIX_3:def 2; A12: width A=m by A4,MATRIX_0:23; Segm n c= Segm card Seg m by A1,A2,CARD_1:11; then A13: n <= m by A6,NAT_1:39; then A14: m-'n=m-n by XREAL_1:233; then width SA=m-'n by A4,A7,MATRIX_0:23; then len (SA@)=0 & m-'n=0 or len (SA@)=m-'n & width (SA@)=n by A10,A5, MATRIX_0:54,def 6; then -SA@={} &m-'n=0 or -SA@ is Matrix of m-'n,n,K by A11,MATRIX_0:51; then reconsider SAT=-SA@ as Matrix of m-'n,n,K by MATRIX_0:13; set ONE= 1.(K,m-'n); A15: N misses SN by XBOOLE_1:79; [:Seg (m-'n),N:]/\[:Seg (m-'n),SN:] = [:Seg (m-'n),N/\SN:] by ZFMISC_1:99 .= [:Seg (m-'n),{}:] by A15 .= {} by ZFMISC_1:90; then card Seg (m-'n) = m-'n & 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) by FINSEQ_1:57; then consider V be Matrix of len ZERO,width ZERO,K such that A16: Segm(V,Seg(m-'n),N) = SAT and A17: 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,A9,A14,A7,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_0:23,def 2; then V={} & m-'n=0 or V is Matrix of m-'n,m,K; then reconsider V as Matrix of m-'n,m,K; take V; thus Segm(V,Seg (m-'n),SN) = ONE & Segm(V,Seg (m-'n),N)=-SA@ by A16,A17; let l; let M be Matrix of m,l,K such that A18: 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); A19: len M=m by A4,A13,MATRIX_0:23; A20: width M=l by A4,A13,MATRIX_0:23; then A21: width (A*M)=l by A12,A19,MATRIX_3:def 4; len A=n by A4,MATRIX_0:23; then len (A*M)=n by A12,A19,MATRIX_3:def 4; then reconsider AM=A*M as Matrix of n,l,K by A21,MATRIX_0:51; A22: Indices A=[:Seg n,Seg m:] by A4,MATRIX_0:23; then A23: [:Seg n,N:] c= Indices A by A2,ZFMISC_1:96; now A24: Indices AM=Indices Z by MATRIX_0:26; let i,j such that A25: [i,j] in Indices AM; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12; A26: Indices AM=[:Seg n,Seg l:] by A4,MATRIX_0:23; then A27: I in Seg n by A25,ZFMISC_1:87; A28: J in Seg l by A25,A26,ZFMISC_1:87; now per cases by A18,A28; suppose ex jj be Nat st jj in Seg (m-'n) & Col(M,J) = Line(V,jj); then consider jj be Nat such that A29: jj in Seg (m-'n) and A30: Col(M,J) = Line(V,jj); A31: jj = idseq (m-'n).jj by A29,FINSEQ_2:49 .= Sgm (Seg (m-'n)).jj by FINSEQ_3:48; A32: Indices ONE=[:Seg (m-'n),Seg (m-'n):] by MATRIX_0:24; then A33: [jj,jj] in Indices ONE by A29,ZFMISC_1:87; A34: rng Sgm SN=SN by A8,FINSEQ_1:def 13; A35: dom Sgm SN=Seg(m-'n) by A14,A7,FINSEQ_3:40,XBOOLE_1:36; then A36: Sgm SN.jj in SN by A29,A34,FUNCT_1:def 3; then A37: Line(A,I).(Sgm SN.jj)=A*(I,Sgm SN.jj) by A12,A8,MATRIX_0:def 7; A38: m-'n<>0 by A29; then A39: width V=m by MATRIX_0:23; then A40: Line(V,jj).(Sgm SN.jj)=V*(jj,Sgm SN.jj) by A8,A36,MATRIX_0:def 7 .= ONE*(jj,jj) by A17,A31,A33,MATRIX13:def 1 .= 1_K by A33,MATRIX_1:def 3; A41: len Line(A,I)=m by A12,MATRIX_0:def 7; A42: I = idseq n.I by A27,FINSEQ_2:49 .= Sgm (Seg n).I by FINSEQ_3:48; len Line(V,jj)=m by A39,MATRIX_0:def 7; then len mlt(Line(A,I),Line(V,jj))=m by A41,MATRIX_3:6; then A43: dom mlt(Line(A,I),Line(V,jj))=Seg m by FINSEQ_1:def 3; then A44: mlt(Line(A,I),Line(V,jj))/.(Sgm SN.jj) = mlt(Line(A,I),Line(V,jj) ).(Sgm SN.jj) by A8,A36,PARTFUN1:def 6 .= (A*(I,Sgm SN.jj))*1_K by A12,A8,A39,A36,A37,A40,FVSUM_1:61 .=A*(I,Sgm SN.jj); A45: Indices V=Indices ZERO & rng Sgm Seg(m-'n)=Seg(m-'n) by FINSEQ_1:def 13 ,MATRIX_0:26; A46: rng Sgm N=N by A2,FINSEQ_1:def 13; A47: rng Sgm Seg n=Seg n by FINSEQ_1:def 13; A48: now let kk be Nat such that A49: kk in Seg m and A50: kk<> Sgm SN.jj and A51: kk<>Sgm N.I; now per cases by A49,XBOOLE_0:def 5; suppose kk in N; then consider x being object such that A52: x in dom Sgm N and A53: Sgm N.x=kk by A46,FUNCT_1:def 3; reconsider x as Element of NAT by A52; A54: Line(V,jj).(Sgm N.x) = V*(jj,Sgm N.x) by A39,A49,A53, MATRIX_0:def 7; [Sgm (Seg n).I,Sgm N.x] in Indices A by A22,A27,A42,A49,A53, ZFMISC_1:87; then A55: [I,x] in Indices Segm(A,Seg n,N) by A23,A46,A47,MATRIX13:17; Line(A,I).(Sgm N.x) = A*(I,Sgm N.x) by A12,A49,A53,MATRIX_0:def 7 .= Segm(A,Seg n,N)*(I,x) by A42,A55,MATRIX13:def 1 .= 0.K by A3,A51,A53,A55,MATRIX_1:def 3; hence mlt(Line(A,I),Line(V,jj)).kk = 0.K*(V*(jj,Sgm N.x)) by A12 ,A39,A49,A53,A54,FVSUM_1:61 .= 0.K; end; suppose kk in SN; then consider x being object such that A56: x in dom Sgm SN and A57: Sgm SN.x=kk by A34,FUNCT_1:def 3; reconsider x as Element of NAT by A56; A58: Line(A,I).(Sgm SN.x)=A*(I,Sgm SN.x) by A12,A49,A57,MATRIX_0:def 7 ; A59: [jj,x] in Indices ONE by A29,A35,A32,A56,ZFMISC_1:87; Line(V,jj).(Sgm SN.x) = V*(jj,Sgm SN.x) by A39,A49,A57, MATRIX_0:def 7 .= ONE*(jj,x) by A17,A31,A59,MATRIX13:def 1 .= 0.K by A50,A57,A59,MATRIX_1:def 3; hence mlt(Line(A,I),Line(V,jj)).kk = (A*(I,Sgm SN.x))*0.K by A12 ,A39,A49,A57,A58,FVSUM_1:61 .= 0.K; end; end; hence mlt(Line(A,I),Line(V,jj)).kk=0.K; end; dom Sgm N=Seg n by A1,A2,FINSEQ_3:40; then A60: Sgm N.I in N by A27,A46,FUNCT_1:def 3; then A61: Sgm SN.jj <> Sgm N.I by A15,A36,XBOOLE_0:3; [Sgm (Seg n).I,Sgm N.I] in Indices A by A2,A22,A27,A60,A42,ZFMISC_1:87; then A62: [I,I] in Indices Segm(A,Seg n,N) by A23,A46,A47,MATRIX13:17; Indices V=[:Seg (m-'n),Seg m:] by A38,MATRIX_0:23; then [Sgm (Seg (m-'n)).jj,Sgm N.I] in Indices V by A2,A29,A60,A31, ZFMISC_1:87; then A63: [jj,I] in Indices Segm(V,Seg(m-'n),N) by A9,A46,A45,MATRIX13:17; A64: Indices SAT= Indices (SA@) by Lm1; then A65: [I,jj] in Indices SA by A16,A63,MATRIX_0:def 6; A66: Line(V,jj).(Sgm N.I) = V*(jj,Sgm N.I) by A2,A39,A60,MATRIX_0:def 7 .= Segm(V,Seg(m-'n),N)*(jj,I) by A31,A63,MATRIX13:def 1 .= -((SA@)*(jj,I)) by A16,A63,A64,MATRIX_3:def 2 .= -(SA*(I,jj)) by A65,MATRIX_0:def 6 .= -(A*(I,Sgm SN.jj)) by A42,A65,MATRIX13:def 1; A67: Line(A,I).(Sgm N.I) = A*(I,Sgm N.I) by A2,A12,A60,MATRIX_0:def 7 .= Segm(A,Seg n,N)*(I,I) by A42,A62,MATRIX13:def 1 .= 1_K by A3,A62,MATRIX_1:def 3; mlt(Line(A,I),Line(V,jj))/.(Sgm N.I) = mlt(Line(A,I),Line(V,jj)). (Sgm N.I) by A2,A43,A60,PARTFUN1:def 6 .= 1_K*(-(A*(I,Sgm SN.jj))) by A2,A12,A39,A60,A67,A66,FVSUM_1:61 .= -(A*(I,Sgm SN.jj)); then Sum(mlt(Line(A,I),Line(V,jj))) = A*(I,Sgm SN.jj)+(-(A*(I,Sgm SN. jj))) by A2,A8,A43,A60,A36,A44,A61,A48,Th7 .= 0.K by VECTSP_1:16; hence Z*(i,j) = Line(A,I)"*"Line(V,jj) by A25,A24,MATRIX_3:1 .= AM*(i,j) by A12,A19,A25,A30,MATRIX_3:def 4; end; suppose Col(M,J) = m|->0.K; hence AM*(i,j) = Line(A,I)"*"(m|->0.K) by A12,A19,A25,MATRIX_3:def 4 .= Sum(0.K * Line(A,I)) by A12,FVSUM_1:66 .= 0.K*Sum(Line(A,I)) by FVSUM_1:73 .= 0.K .= Z*(i,j) by A25,A24,MATRIX_3:1; end; end; hence AM*(i,j) = Z*(i,j); end; then AM = Z by MATRIX_0:27; hence thesis by A12,A19,A20,A21; 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 and A2: N c= Seg m and A3: n>0 and A4: Segm(A,Seg n,N) = 1.(K,n); A5: width A=m by A3,MATRIX_0:23; set Z=0.(K,m,l); set SN=Seg m\N; A6: card Seg m=m by FINSEQ_1:57; then A7: m-'n=m-n & card SN=m-n by A1,A2,CARD_2:44,NAT_1:43,XREAL_1:233; set ZERO=0.(K,m-'n,l); A8: N misses SN by XBOOLE_1:79; [:N,Seg l:]/\[:SN,Seg l:] = [:N/\SN,Seg l:] by ZFMISC_1:99 .= [:{},Seg l:] by A8 .= {} by ZFMISC_1:90; then A9: 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); A10: Indices A=[:Seg n,Seg m:] by A3,MATRIX_0:23; A11: n <=card Seg m by A1,A2,NAT_1:43; then A12: len Z=m & width Z=l by A3,A6,MATRIX_0:23; A13: Indices Z=[:Seg m,Seg l:] by A3,A11,A6,MATRIX_0:23; then A14: [:N,Seg l:] c= Indices Z by A2,ZFMISC_1:95; A15: SN c= Seg m by XBOOLE_1:36; then card Seg l=l & [:SN,Seg l:] c= Indices Z by A13,FINSEQ_1:57,ZFMISC_1:95; then consider X be Matrix of m,l,K such that A16: Segm(X,N,Seg l) = B and A17: 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,A7,A12,A14,A9,Th9; set AX=A*X; A18: len X=m by A3,A11,A6,MATRIX_0:23; then A19: dom X=Seg m by FINSEQ_1:def 3; len A=n by A3,MATRIX_0:23; then A20: len AX=n by A5,A18,MATRIX_3:def 4; take X; thus Segm(X,SN,Seg l) = ZERO & Segm(X,N,Seg l) = B by A16,A17; A21: Indices X=[:Seg m,Seg l:] by A3,A11,A6,MATRIX_0:23; A22: width B=l by A3,MATRIX_0:23; A23: width X=l by A3,A11,A6,MATRIX_0:23; then width AX=l by A5,A18,MATRIX_3:def 4; then reconsider AX as Matrix of n,l,K by A20,MATRIX_0:51; A24: Indices B=[:Seg n,Seg l:] by A3,MATRIX_0:23; now A25: [:N,Seg l:] c= Indices X by A2,A21,ZFMISC_1:95; let i,j such that A26: [i,j] in Indices AX; reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12; A27: Indices AX=Indices B by MATRIX_0:26; then A28: i in Seg n by A24,A26,ZFMISC_1:87; len Line(A,i)=m & len Col(X,j)=m by A5,A18,CARD_1:def 7; then len mlt(Line(A,i),Col(X,j))=m by MATRIX_3:6; then A29: dom mlt(Line(A,i),Col(X,j))=Seg m by FINSEQ_1:def 3; A30: rng Sgm (Seg l)=Seg l by FINSEQ_1:def 13; A31: rng Sgm (Seg n)=Seg n & [:Seg n,N:] c= Indices A by A2,A10,FINSEQ_1:def 13 ,ZFMISC_1:95; A32: rng Sgm N=N by A2,FINSEQ_1:def 13; dom Sgm N=Seg n by A1,A2,FINSEQ_3:40; then A33: Sgm N.i in N by A28,A32,FUNCT_1:def 3; A34: j in Seg l by A22,A26,A27,ZFMISC_1:87; then A35: j = (idseq l).j by FINSEQ_2:49 .= Sgm (Seg l).j by FINSEQ_3:48; then [Sgm N.I,Sgm(Seg l).J] in Indices X by A2,A21,A34,A33,ZFMISC_1:87; then A36: [I,J] in Indices B by A16,A32,A30,A25,MATRIX13:17; A37: rng Sgm SN=SN by A15,FINSEQ_1:def 13; A38: i = (idseq n).i by A28,FINSEQ_2:49 .= Sgm (Seg n).i by FINSEQ_3:48; then [Sgm (Seg n).i,Sgm N.i] in Indices A by A2,A10,A28,A33,ZFMISC_1:87; then A39: [I,I] in Indices 1.(K,n) by A4,A32,A31,MATRIX13:17; A40: [:SN,Seg l:] c= Indices X by A15,A21,ZFMISC_1:95; A41: now let kk be Nat such that A42: kk in Seg m and A43: kk <> Sgm N.I; per cases by A42,XBOOLE_0:def 5; suppose A44: kk in N; then consider x being object such that A45: x in dom Sgm N and A46: Sgm N.x=kk by A32,FUNCT_1:def 3; reconsider x as Element of NAT by A45; [Sgm (Seg n).i,Sgm N.x] in Indices A by A2,A10,A28,A38,A44,A46, ZFMISC_1:87; then A47: [I,x] in Indices 1.(K,n) by A4,A32,A31,MATRIX13:17; A48: Col(X,j).kk = X*(kk,j) by A2,A19,A44,MATRIX_0:def 8; Line(A,i).(Sgm N.x) = A*(I,Sgm N.x) by A2,A5,A44,A46,MATRIX_0:def 7 .= (Segm(A,Seg n,N))*(I,x) by A4,A38,A47,MATRIX13:def 1 .= 0.K by A4,A43,A46,A47,MATRIX_1:def 3; hence mlt(Line(A,i),Col(X,j)).kk = 0.K*(X*(kk,j)) by A2,A5,A18,A44,A46,A48, FVSUM_1:61 .= 0.K; end; suppose A49: kk in SN; then consider x being object such that A50: x in dom Sgm SN and A51: Sgm SN.x=kk by A37,FUNCT_1:def 3; reconsider x as Element of NAT by A50; A52: Line(A,i).kk=A*(I,Sgm SN.x) by A5,A42,A51,MATRIX_0:def 7; [Sgm SN.x,Sgm (Seg l).J] in Indices X by A15,A21,A34,A35,A49,A51, ZFMISC_1:87; then A53: [x,J] in Indices ZERO by A17,A30,A37,A40,MATRIX13:17; Col(X,j).kk = X*(Sgm SN.x,Sgm (Seg l).j) by A15,A19,A35,A49,A51, MATRIX_0:def 8 .= ZERO*(x,J) by A17,A53,MATRIX13:def 1 .= 0.K by A53,MATRIX_3:1; hence mlt(Line(A,i),Col(X,j)).kk = (A*(I,Sgm SN.x))*0.K by A5,A18,A42,A52, FVSUM_1:61 .= 0.K; end; end; A54: Col(X,j).(Sgm N.i) = X*(Sgm N.i,j) by A2,A19,A33,MATRIX_0:def 8 .= B*(I,J) by A16,A35,A36,MATRIX13:def 1; Line(A,i).(Sgm N.i) = A*(I,Sgm N.I) by A2,A5,A33,MATRIX_0:def 7 .= (Segm(A,Seg n,N))*(I,I) by A4,A38,A39,MATRIX13:def 1 .= 1_K by A4,A39,MATRIX_1:def 3; then A55: mlt(Line(A,i),Col(X,j)).(Sgm N.i) = 1_K * (B*(I,J)) by A2,A5,A18,A33,A54, FVSUM_1:61 .= B*(I,J); AX*(i,j) = Line(A,i)"*"Col(X,j) by A5,A18,A26,MATRIX_3:def 4 .= Sum(mlt(Line(A,i),Col(X,j))); hence AX*(i,j)=B*(i,j) by A2,A33,A55,A29,A41,MATRIX_3:12; end; then AX=B by MATRIX_0:27; hence thesis by A5,A22,A18,A23; 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 by MATRIX_0:def 2; A2: Solutions_of(A,B) c= {{}} proof let x be object; assume x in Solutions_of(A,B); then ex X st X=x &len X = width A & width X = width B & A * X = B; then x={} by A1,MATRIX_0:def 3; hence thesis by TARSKI:def 1; end; len B=0 by MATRIX_0:def 2; then A3: B={} & width B=0 by MATRIX_0:def 3; A4: width A=0 by A1,MATRIX_0:def 3; then len (A*A)=0 by A1,MATRIX_3:def 4; then A*A={}; then A in Solutions_of(A,B) by A1,A4,A3; hence thesis by A2,ZFMISC_1:33; 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); set ZERO=0.(K,n,width B); assume Solutions_of(0.(K,n,k),B) is non empty; then consider x being object such that A1: x in Solutions_of(0.(K,n,k),B); A2: len A=n by MATRIX_0:def 2; A3: dom A=Seg n; A4: len ZERO=n by MATRIX_0:def 2; then A5: len B=len ZERO by A1,A2,Th33; then reconsider B9=B as Matrix of n,width B,K by A4,MATRIX_0:51; A6: ex X st X=x & len X = width A & width X = width B & A * X = B by A1; now let i such that A7: 1<=i & i<=n; A8: width A=k by A7,MATRIX_0:23; A9: i in Seg n by A7; then Line(A,i) = A.i by MATRIX_0:52 .= width A|->0.K by A9,A8,FINSEQ_2:57; then width B|-> 0.K = Line(B,i) by A1,A6,A3,A9,Th41 .= B9.i by A9,MATRIX_0:52; hence B.i=ZERO.i by A9,FINSEQ_2:57; end; hence thesis by A4,A5; 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; assume n > 0; then A1: width A=k & width B=m by MATRIX_0:23; assume x in Solutions_of(A,B); then ex X st X=x & len X = k & width X = m & A * X = B by A1; hence thesis by MATRIX_0:51; end; theorem Th54: n > 0 & k > 0 implies Solutions_of(0.(K,n,k),0.(K,n,m)) = the set of all X where X is Matrix of k,m,K proof assume that A1: n > 0 and A2: k > 0; set B=0.(K,n,m); A3: width B=m by A1,MATRIX_0:23; set XX=the set of all X where X is Matrix of k,m,K; set A=0.(K,n,k); thus Solutions_of(A,B) c= XX proof let x be object; assume x in Solutions_of(A,B); then x is Matrix of k,m,K by A1,Th53; hence thesis; end; let x be object; assume x in XX; then consider X be Matrix of k,m,K such that A4: x=X and not contradiction; A5: width A=k & len X=k by A1,A2,MATRIX_0:23; A6: width X=m by A2,MATRIX_0:23; len A=n by A1,MATRIX_0:23; then A*X=B by A1,A2,A5,A6,MATRIX_5:22; hence thesis by A4,A3,A5,A6; end; theorem n>0 & Solutions_of(0.(K,n,0),0.(K,n,m)) is non empty implies m = 0 proof assume that A1: n>0 and A2: Solutions_of(0.(K,n,0),0.(K,n,m)) is non empty; consider x being object such that A3: x in Solutions_of(0.(K,n,0),0.(K,n,m)) by A2; A4: width 0.(K,n,0)=0 by A1,MATRIX_0:23; ex X st X=x & len X = width 0.(K,n,0) & width X = width 0.(K,n,m) & 0.(K, n,0) * X = 0.(K,n,m) by A3; hence 0 = width 0.(K,n,m) by A4,MATRIX_0:def 3 .= m by A1,MATRIX_0:23; 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; set B=0.(K,n,0); set A=0.(K,n,0); reconsider E={} as Matrix of 0,0,K by MATRIX_0:13; A2: width A=0 by A1,MATRIX_0:23; then A3: for i,j st [i,j] in Indices B holds B*(i,j)=(A*E)*(i,j) by ZFMISC_1:90; A4: Solutions_of(A,B) c= {{}} proof let x be object; 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_0:def 2; then X={}; hence thesis by TARSKI:def 1; end; A5: len E=0; A6: width E=0 by MATRIX_0:24; then A7: width (A*E)=0 by A2,A5,MATRIX_3:def 4; A8: len A=n by A1,MATRIX_0:23; then len (A*E)=n by A2,A5,MATRIX_3:def 4; then A*E=B by A8,A2,A7,A3,MATRIX_0:21; then E in Solutions_of(A,B) by A2,A5,A6; hence thesis by A4,ZFMISC_1:33; end; end; begin ::Gaussian eliminations scheme GAUSS1{ K() -> Field, n,m,m9() -> Nat, A() -> Matrix of n(),m(),K(), B() -> Matrix of n(),m9(),K(), F(Matrix of n(),m9(),K(),Nat,Nat,Element of K())-> Matrix of n(),m9(),K(), P[set,set]}: ex A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K(), N be without_zero finite Subset of NAT st N c= Seg m() & the_rank_of A() = the_rank_of A9 & the_rank_of A() = card N & P[A9,B9] & Segm (A9,Seg card N,N) is diagonal & ( for i st i in Seg card N holds A9*(i,Sgm N/.i ) <> 0.K() ) & ( for i st i in dom A9 & i > card N holds Line(A9,i)= m() |-> 0.K( ) ) & for i,j st i in Seg card N & j in Seg width A9 & j < Sgm N.i holds A9*(i, j) = 0.K() provided A1: P[A(),B()] and A2: for A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K() st P[ A9,B9] for i,j st i <> j & j in dom A9 for a be Element of K() holds P[RLine(A9 ,i,Line(A9,i) + a*Line(A9,j)),F(B9,i,j,a)] proof 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()); set r = the_rank_of A(); ex A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K() st P[A9,B9] & r = the_rank_of A9 & (for i st i in dom A9 & i > r holds Line(A9,i)=m() |-> 0.K ())& ex f be FinSequence of NAT st len f = the_rank_of A9 & f is one-to-one & rng f c= Seg width A9 & for i,j st i in dom f holds PP[f,i,j,A9] proof per cases; suppose A3: n()=0; take A9=A(),B9=B(); dom A9=Seg len A9 & len A9=0 by A3,FINSEQ_1:def 3,MATRIX_0:def 2; hence P[A9,B9] & r = the_rank_of A9 & for i st i in dom A9 & i > r holds Line(A9,i)=m() |->0.K() by A1; take <*>NAT; len A9=0 by A3,MATRIX_0:22; hence thesis by MATRIX13:74; end; suppose A4: n()>0; defpred Q[Nat] means $1 <= m() implies ex A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K() st P[A9,B9] & r = the_rank_of A9 & ex f be FinSequence of NAT st (for i,j st [i,j] in Indices A9&i>len f&j<=$1 holds A9*(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,A9]; A5: for n st Q[n] holds Q[n+1] proof let n such that A6: Q[n]; set n1=n+1; assume A7: n1<=m(); then consider A9 be Matrix of n(),m(),K(),B9 be Matrix of n(),m9(),K() such that A8: ( P[A9,B9])& r = the_rank_of A9 and A9: ex f be FinSequence of NAT st (for i,j st [i,j] in Indices A9 &i>len f&j<=n holds A9*(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,A9] by A6,NAT_1:13; consider f be FinSequence of NAT such that A10: for i,j st [i,j] in Indices A9&i>len f&j<=n holds A9*(i,j)=0. K() and A11: f is one-to-one and A12: len f <= n and A13: len f<=n() and A14: rng f c=Seg n and A15: for i,j st i in dom f holds PP[f,i,j,A9] by A9; per cases; suppose A16: for i,j st [i,j] in Indices A9 & i>len f & j=n1 holds A9*(i ,j)=0.K(); A17: now let i,j such that A18: [i,j] in Indices A9 & i>len f and A19: j<=n1; j<=n or j=n1 by A19,NAT_1:8; hence A9*(i,j)=0.K() by A10,A16,A18; end; n<=n1 by NAT_1:13; then Seg n c= Seg n1 by FINSEQ_1:5; then A20: rng f c= Seg n1 by A14; len f <=n1 by A12,NAT_1:12; hence thesis by A8,A11,A13,A15,A17,A20; end; suppose ex i,j st [i,j] in Indices A9 &i>len f&j=n1&A9*(i,j)<>0.K(); then consider i0,j0 be Nat such that A21: [i0,j0] in Indices A9 and A22: i0>len f and A23: j0=n1 and A24: A9*(i0,j0)<>0.K(); A25: Indices A9=[:Seg n(),Seg m():] by A4,MATRIX_0:23; then A26: n1 in Seg m() by A21,A23,ZFMISC_1:87; A27: i0 in Seg n() by A21,A25,ZFMISC_1:87; then A28: i0<=n() by FINSEQ_1:1; A29: len f+1<=i0 by A22,NAT_1:13; then 0+1<=len f+1 & len f+1<=n() by A28,XREAL_1:7,XXREAL_0:2; then A30: len f+1 in Seg n(); defpred QQ[Nat] means $1<=n() implies ex A9 be Matrix of n(),m(),K() , B9 be Matrix of n(),m9(),K() st P[A9,B9] & r = the_rank_of A9 & A9*(len f+1, n1) <> 0.K() & (for i,j st [i,j] in Indices A9 & i>len f&j<=n holds A9*(i,j)=0. K())& (for i,j st i in dom f holds PP[f,i,j,A9]) & for j st j in dom A9\{len f+ 1} & j<=$1 holds A9*(j,n1)=0.K(); A31: dom f = Seg len f by FINSEQ_1:def 3; n<=m() by A7,NAT_1:13; then A32: Seg n c= Seg m() by FINSEQ_1:5; A33: Seg len f c=Seg n() by A13,FINSEQ_1:5; A34: for k st QQ[k] holds QQ[k+1] proof let k such that A35: QQ[k]; set k1=k+1; assume k1<=n(); then consider AA be Matrix of n(),m(),K(), BB be Matrix of n(),m9( ),K( ) such that A36: P[AA,BB] and A37: r = the_rank_of AA and A38: AA*(len f+1,n1) <> 0.K() and A39: for i,j st [i,j] in Indices AA & i>len f&j<=n holds AA*( i,j)=0.K() and A40: for i,j st i in dom f holds PP[f,i,j,AA] and A41: for j st j in dom AA\{len f+1} & j<=k holds AA*(j,n1)=0. K() by A35,NAT_1:13; now per cases; suppose A42: k1=len f+1; take RA=AA,RB=BB; now let j such that A43: j in dom RA \ {len f+1} and A44: j<=k1; j <> len f+1 by A43,ZFMISC_1:56; then jlen f+1; set LA=Line(AA,k1); set LAf=Line(AA,len f+1); set a=AA*(len f+1,n1); set RA=RLine(AA,k1,LA + (-(AA*(k1,n1))*a")*LAf); A46: width AA=m() by A4,MATRIX_0:23; then A47: len (LA+(-(AA*(k1,n1))*a")*LAf)=m()by CARD_1:def 7; A48: Indices A9=Indices AA by MATRIX_0:26; then [len f+1,n1] in Indices AA by A25,A30,A26,ZFMISC_1:87; then A49: RA*(len f+1,n1)<>0.K() by A38,A45,A46,A47,MATRIX11:def 3; A50: Indices A9=Indices RA by MATRIX_0:26; A51: now let i,j such that A52: [i,j] in Indices RA and A53: i>len f and A54: j<=n; now per cases; suppose A55: i = k1; A56: j in Seg m() by A25,A50,A52,ZFMISC_1:87; then len f+1>len f & [len f+1,j] in Indices A9 by A25,A30 ,NAT_1:13,ZFMISC_1:87; then AA*(len f+1,j)=0.K() by A39,A48,A54; then LAf.j=0.K() by A46,A56,MATRIX_0:def 7; then A57: ((-(AA*(k1,n1))*a")*LAf).j = (-(AA*(k1,n1))*a")*0. K() by A46,A56,FVSUM_1:51 .= 0.K(); LA.j = AA*(k1,j) by A46,A56,MATRIX_0:def 7 .= 0.K() by A39,A48,A50,A52,A53,A54,A55; then 0.K()+0.K() = (LA + (-(AA*(k1,n1))*a")*LAf).j by A46 ,A56,A57,FVSUM_1:18 .= RA*(i,j) by A48,A50,A46,A47,A52,A55,MATRIX11:def 3; hence RA*(i,j) = 0.K() by RLVECT_1:def 4; end; suppose i<>k1; hence RA*(i,j) = AA*(i,j) by A48,A50,A46,A47,A52, MATRIX11:def 3 .= 0.K() by A39,A48,A50,A52,A53,A54; end; end; hence RA*(i,j)=0.K(); end; set RB=F(BB,k1,len f+1,-(AA*(k1,n1))*a"); take RA,RB; A58: width RA=m() by A4,MATRIX_0:23; A59: len AA=n() by MATRIX_0:def 2; A60: now A61: dom AA=Seg len AA by FINSEQ_1:def 3; let j such that A62: j in dom RA \ {len f+1} and A63: j<=k1; j in dom RA by A62,XBOOLE_0:def 5; then A64: [j,n1] in Indices AA by A26,A48,A50,A58,ZFMISC_1:87; A65: dom RA=Seg len RA & len RA=n() by FINSEQ_1:def 3 ,MATRIX_0:def 2; now per cases by A63,NAT_1:8; suppose A66: j<=k; then jlen f & fi<=n by A14,A72,FINSEQ_1:1,NAT_1:13; [len f+1,fi] in Indices AA & LAf.fi=AA*(len f+1,fi) by A25 ,A32,A30,A48,A46,A73,MATRIX_0:def 7,ZFMISC_1:87; then LAf.fi=0.K() by A39,A74; then A75: ((-(AA*(k1,n1))*a")*LAf).fi =(-(AA*(k1,n1))*a")*0.K() by A32,A46,A73,FVSUM_1:51 .= 0.K(); LA.fi=AA*(k1,fi) by A32,A46,A73,MATRIX_0:def 7; then A76: (LA+(-(AA*(k1,n1))*a")*LAf).fi = AA*( k1,fi)+0.K() by A32,A46 ,A73,A75,FVSUM_1:18 .= AA*(k1,fi) by RLVECT_1:def 4; A77: [i,fi] in Indices AA by A25,A32,A33,A31,A48,A71,A73, ZFMISC_1:87; now per cases; suppose i<>k1; then RA*(i,fi)=AA*(i,fi)by A46,A47,A77,MATRIX11:def 3; hence RA*(i,fi)<>0.K() by A40,A71; end; suppose i=k1; then RA*(i,fi)=AA*(i,fi) by A46,A47,A77,A76, MATRIX11:def 3; hence RA*(i,f/.i)<>0.K() by A40,A71; end; end; hence RA*(i,fi) <> 0.K()& (j in dom f & i < j implies fi < f /.j) by A15,A71; thus j in dom f \ {i} implies RA*(j,fi) = 0.K() proof assume A78: j in dom f \ {i}; then j in Seg len f by A31,XBOOLE_0:def 5; then A79: [j,fi] in Indices AA by A25,A32,A33,A48,A73,ZFMISC_1:87; per cases; suppose j<>k1; hence RA*(j,fi) = AA*(j,fi) by A46,A47,A79,MATRIX11:def 3 .= 0.K() by A40,A71,A78; end; suppose A80: j = k1; hence RA*(j,fi) = (LA+(-(AA*(k1,n1))*a")*LAf).fi by A46,A47,A79 ,MATRIX11:def 3 .= 0.K() by A40,A71,A76,A78,A80; end; end; thus j in Seg width RA & j < f/.i implies RA*(i,j) = 0.K() proof assume that A81: j in Seg width RA and A82: j < f/.i; A83: [len f+1,j] in Indices AA by A30,A59,A69,A46,A58,A81, ZFMISC_1:87; A84: [i,j] in Indices AA by A33,A31,A59,A69,A46,A58,A71,A81, ZFMISC_1:87; per cases; suppose i<>k1; hence RA*(i,j) = AA*(i,j) by A46,A47,A84,MATRIX11:def 3 .= 0.K() by A40,A46,A58,A71,A81,A82; end; suppose A85: i = k1; fi <= n by A14,A72,FINSEQ_1:1; then A86: j <= n by A82,XXREAL_0:2; len f+1 > len f by NAT_1:13; then 0.K() = AA*(len f+1,j) by A39,A83,A86 .= LAf.j by A46,A58,A81,MATRIX_0:def 7; then A87: ((-(AA*(k1,n1))*a")*LAf).j = (-(AA*(k1,n1))*a")*0. K() by A46,A58,A81,FVSUM_1:51 .= 0.K(); LA.j = AA*(i,j)by A46,A58,A81,A85,MATRIX_0:def 7 .= 0.K() by A40,A46,A58,A71,A81,A82; then (LA + (-(AA*(k1,n1))*a")*LAf).j = 0.K()+0.K() by A46 ,A58,A81,A87,FVSUM_1:18 .= 0.K() by RLVECT_1:def 4; hence thesis by A46,A47,A84,A85,MATRIX11:def 3; end; end; end; A88: len f+1 in Seg len AA by A4,A30,MATRIX_0:23; then A89: r=the_rank_of RA by A37,A45,MATRIX13:92; P[RA,RB] by A2,A36,A45,A88,A69; hence thesis by A89,A49,A51,A70,A60; end; end; hence thesis; end; A90: j0 in Seg m() by A21,A25,ZFMISC_1:87; ex A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K() st P[A9,B9] & r = the_rank_of A9 & A9*(len f+1,n1) <> 0.K() & (for i,j st [i,j] in Indices A9 & i>len f &j<=n holds A9*(i,j)=0.K())& for i,j st i in dom f holds PP[f,i,j,A9] proof per cases; suppose A9*(len f+1,n1) <> 0.K(); hence thesis by A8,A10,A15; end; suppose A91: A9*(len f+1,n1) = 0.K(); set RB=F(B9,len f+1,i0,1_K()); set LA=Line(A9,i0); set LAf=Line(A9,len f+1); set RA=RLine(A9,len f+1,LAf + 1_K()*LA); take RA,RB; i0 in dom A9 & dom A9=Seg len A9 by A21,FINSEQ_1:def 3 ,ZFMISC_1:87; hence P[RA,RB] & r = the_rank_of RA by A2,A8,A23,A24,A91, MATRIX13:92; A92: 1_K()*LA=LA & len (LAf+LA)=width A9 by CARD_1:def 7,FVSUM_1:57; [len f+1,j0] in Indices A9 by A25,A30,A90,ZFMISC_1:87; then A93: RA*(len f+1,n1)=(LAf+LA).n1 by A23,A92,MATRIX11:def 3; A94: width A9=m() by A4,MATRIX_0:23; then A95: LA.n1=A9*(i0,n1) by A23,A90,MATRIX_0:def 7; LAf.n1=0.K() by A23,A90,A91,A94,MATRIX_0:def 7; then RA*(len f+1,n1) = 0.K()+A9*(i0,n1) by A26,A94,A93,A95, FVSUM_1:18 .= A9*(i0,n1) by RLVECT_1:def 4; hence RA*(len f+1,n1)<>0.K() by A23,A24; A96: Indices RA=Indices A9 by MATRIX_0:26; now let i,j such that A97: [i,j] in Indices RA and A98: i>len f and A99: j<=n; A100: j in Seg m() by A94,A96,A97,ZFMISC_1:87; A101: i>=len f+1 by A98,NAT_1:13; now per cases by A101,XXREAL_0:1; suppose i>len f+1; hence RA*(i,j) = A9*(i,j) by A92,A96,A97,MATRIX11:def 3 .= 0.K() by A10,A96,A97,A98,A99; end; suppose A102: i=len f+1; A103: [i0,j] in Indices A9 by A25,A27,A100,ZFMISC_1:87; A104: LAf.j=A9*( len f+1,j) & LA.j=A9*(i0,j) by A94,A100, MATRIX_0:def 7; RA*(i,j)=(LAf+LA).j by A92,A96,A97,A102,MATRIX11:def 3; hence RA*(i,j) = A9*(len f+1,j)+A9*(i0,j) by A94,A100,A104, FVSUM_1:18 .= 0.K()+A9*(i0,j) by A10,A96,A97,A98,A99,A102 .= 0.K()+0.K() by A10,A22,A99,A103 .= 0.K() by RLVECT_1:def 4; 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 A105: i in dom f; i <= len f by A31,A105,FINSEQ_1:1; then A106: i0.K()&(j in dom f & i 0.K() & for i,j st [ i,j] in Indices A0& i>len f& j<=n holds A0*(i,j)=0.K() ) & for i ,j st i in dom f holds PP[f,i,j,A0]; A115: QQ[0] proof assume 0<=n(); take A0,B0; now A116: dom A0=Seg len A0 by FINSEQ_1:def 3; let j; assume j in dom A0 \ {len f+1} & j<=0; hence A0*(j,n1) = 0.K() by A116; end; hence thesis by A114; end; for k holds QQ[k] from NAT_1:sch 2(A115,A34); then consider Aa be Matrix of n(),m(),K(),Bb be Matrix of n(),m9(),K() such that A117: ( P[Aa,Bb])& r = the_rank_of Aa and A118: Aa*(len f+1,n1) <> 0.K() and A119: for i,j st [i,j] in Indices Aa & i>len f&j<=n holds Aa*(i, j)=0.K() and A120: for i,j st i in dom f holds PP[f,i,j,Aa] and A121: 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 A117; take f9=f^<*n1*>; A122: len f9=len f+1 by FINSEQ_2:16; A123: len Aa=n() & dom Aa=Seg len Aa by A4,FINSEQ_1:def 3,MATRIX_0:23; A124: now let i,j such that A125: [i,j] in Indices Aa and A126: i>len f9 and A127: j<=n1; per cases by A127,NAT_1:8; suppose A128: j<=n; i>len f by A122,A126,NAT_1:13; hence Aa*(i,j)=0.K() by A119,A125,A128; end; suppose A129: j=n1; i in dom Aa by A125,ZFMISC_1:87; then i in dom Aa\{len f+1} & i<=n() by A122,A123,A126,FINSEQ_1:1 ,ZFMISC_1:56; hence Aa*(i,j)=0.K() by A121,A129; end; end; A130: width Aa=m() by A4,MATRIX_0:23; A131: len f9<=n() by A28,A29,A122,XXREAL_0:2; A132: now let i,j such that A133: i in dom f9; A134: dom f9 = Seg (len f+1) by A122,FINSEQ_1:def 3 .= dom f\/{len f+1} by A31,FINSEQ_1:9; A135: now let k such that A136: k in dom f; A137: k in dom f9 by A134,A136,XBOOLE_0:def 3; thus f/.k = f.k by A136,PARTFUN1:def 6 .= f9.k by A136,FINSEQ_1:def 7 .= f9/.k by A137,PARTFUN1:def 6; end; now per cases by A133,A134,XBOOLE_0:def 3; suppose A138: i in dom f; then f/.i=f9/.i by A135; hence Aa*(i,f9/.i)<>0.K() by A120,A138; end; suppose A139: i in {len f+1}; A140: f9/.i=f9.i by A133,PARTFUN1:def 6; i=len f+1 by A139,TARSKI:def 1; hence Aa*(i,f9/.i)<>0.K() by A118,A140,FINSEQ_1:42; end; end; hence Aa*(i,f9/.i) <> 0.K(); thus j in dom f9 & i < j implies f9/.i < f9/.j proof assume that A141: j in dom f9 and A142: i < j; per cases by A133,A134,A141,XBOOLE_0:def 3; suppose A143: j in {len f+1} & i in {len f+1}; then i=len f+1 by TARSKI:def 1; hence thesis by A142,A143,TARSKI:def 1; end; suppose A144: j in {len f+1} & i in dom f; then len f+1=j by TARSKI:def 1; then A145: f9.j=n1 by FINSEQ_1:42; f/.i=f.i & f.i in rng f by A144,FUNCT_1:def 3,PARTFUN1:def 6; then A146: f/.i <= n by A14,FINSEQ_1:1; f9.j=f9/.j by A141,PARTFUN1:def 6; then f/.i < f9/.j by A146,A145,NAT_1:13; hence thesis by A135,A144; end; suppose j in dom f & i in {len f+1}; then j<=len f & i=len f+1 by A31,FINSEQ_1:1,TARSKI:def 1; hence thesis by A142,NAT_1:13; end; suppose A147: j in dom f & i in dom f; then f/.i=f9/.i & f/.j=f9/.j by A135; hence thesis by A15,A142,A147; end; end; dom f9=Seg len f9 by FINSEQ_1:def 3; then A148: dom f9 c= dom Aa by A123,A131,FINSEQ_1:5; thus j in dom f9 \ {i} implies Aa*(j,f9/.i) = 0.K() proof assume A149: j in dom f9 \ {i}; per cases; suppose A150: i=len f+1; len f+1 in {len f+1} by TARSKI:def 1; then len f+1 in dom f9 by A134,XBOOLE_0:def 3; then A151: f9.(len f+1)=f9/.i by A150,PARTFUN1:def 6; A152: j in dom f9 by A149,ZFMISC_1:56; j<>i by A149,ZFMISC_1:56; then A153: j in dom Aa\{i} by A148,A152,ZFMISC_1:56; j<=n() by A123,A148,A152,FINSEQ_1:1; then Aa*(j,n1)=0.K() by A121,A150,A153; hence thesis by A151,FINSEQ_1:42; end; suppose A154: i<>len f+1; A155: j in dom f9 by A149,XBOOLE_0:def 5; A156: i in dom f or i in {len f+1} by A133,A134,XBOOLE_0:def 3; then A157: f.i in rng f by A154,FUNCT_1:def 3,TARSKI:def 1; A158: f/.i=f9/.i & f.i=f/.i by A135,A154,A156,PARTFUN1:def 6 ,TARSKI:def 1; then A159: 1<=f9/.i by A14,A157,FINSEQ_1:1; A160: f9/.i<=n by A14,A158,A157,FINSEQ_1:1; n<=m() by A7,NAT_1:13; then f9/.i <=m() by A160,XXREAL_0:2; then f9/.i in Seg width Aa by A130,A159; then A161: [j,f9/.i] in Indices Aa by A148,A155,ZFMISC_1:87; per cases; suppose j=len f+1; then j > len f by NAT_1:13; hence thesis by A119,A160,A161; end; suppose A162: j<>len f+1; j in dom f9 by A149,XBOOLE_0:def 5; then A163: j in dom f or j in {len f+1} by A134,XBOOLE_0:def 3; j<>i by A149,ZFMISC_1:56; then j in dom f\{i} by A162,A163,TARSKI:def 1,ZFMISC_1:56; then Aa*(j,f/.i)=0.K() by A120,A154,A156,TARSKI:def 1; hence thesis by A135,A154,A156,TARSKI:def 1; end; end; end; thus j in Seg width Aa & j < f9/.i implies Aa*(i,j) = 0.K() proof assume that A164: j in Seg width Aa and A165: j < f9/.i; per cases; suppose A166: i in dom f; then f9/.i=f/.i by A135; hence thesis by A120,A164,A165,A166; end; suppose A167: not i in dom f; i in dom f or i in {len f+1} by A133,A134,XBOOLE_0:def 3; then A168: i=len f+1 by A167,TARSKI:def 1; then A169: f9.i = n1 by FINSEQ_1:42; f9.i=f9/.i by A133,PARTFUN1:def 6; then A170: j<=n by A165,A169,NAT_1:13; A171: i>len f by A168,NAT_1:13; [i,j] in Indices Aa by A133,A148,A164,ZFMISC_1:87; hence thesis by A119,A170,A171; end; end; end; A172: rng <*n1*>= {n1} & rng f \/{n1} c= Seg n\/{n1} by A14,FINSEQ_1:38 ,XBOOLE_1:9; A173: Seg n\/{n1}=Seg n1 by FINSEQ_1:9; rng f misses {n1} & <*n1*> is one-to-one by A14,FINSEQ_3:14 ,XBOOLE_1:63; hence thesis by A11,A12,A28,A29,A122,A124,A172,A173,A132,FINSEQ_1:31 ,FINSEQ_3:91,XREAL_1:6,XXREAL_0:2; end; end; A174: Q[0] proof assume 0<=m(); take A9=A(),B9=B(); thus P[A9,B9] & r = the_rank_of A9 by A1; take f=<*>NAT; now let i,j such that A175: [i,j] in Indices A9 and i > len f and A176: j<=0; j in Seg width A9 by A175,ZFMISC_1:87; hence A9*(i,j)=0.K() by A176; end; hence thesis; end; for n holds Q[n] from NAT_1:sch 2(A174,A5); then consider A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K() such that A177: P[A9,B9] and A178: r = the_rank_of A9 and A179: ex f be FinSequence of NAT st (for i,j st [i,j] in Indices A9& i>len f&j<=m() holds A9*(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,A9]; consider f be FinSequence of NAT such that A180: for i,j st [i,j] in Indices A9&i>len f&j<=m() holds A9*(i,j)= 0.K() and A181: f is one-to-one and len f <= m() and A182: len f<=n() and A183: rng f c= Seg m() and A184: for i,j st i in dom f holds PP[f,i,j,A9] by A179; A185: len A9=n() by A4,MATRIX_0:23; take A9,B9; thus P[A9,B9] & r=the_rank_of A9 by A177,A178; A186: dom A9=Seg len A9 by FINSEQ_1:def 3; set L=len f; A187: Seg L c= Seg n() by A182,FINSEQ_1:5; idseq L is FinSequence of NAT & len (idseq L)=L by CARD_1:def 7 ,FINSEQ_2:48; then reconsider idL=idseq L,F9=f as Element of L-tuples_on NAT by FINSEQ_2:92; set S=Segm(A9,idL,F9); A188: dom f=Seg L by FINSEQ_1:def 3; set D=diagonal_of_Matrix S; A189: Indices S=[:Seg L,Seg L:] by MATRIX_0:24; for k be Nat st k in dom D holds D.k <> 0.K() proof A190: len D=L by MATRIX_3:def 10; let k be Nat; assume k in dom D; then A191: k in Seg L by A190,FINSEQ_1:def 3; then [k,k] in Indices S by A189,ZFMISC_1:87; then S*(k,k) = A9*(idL.k,f.k) by MATRIX13:def 1 .= A9*(k,f.k) by A191,FINSEQ_2:49 .= A9*(k,f/.k) by A188,A191,PARTFUN1:def 6; then S*(k,k)<>0.K() by A184,A188,A191; hence thesis by A191,MATRIX_3:def 10; end; then A192: Product D<>0.K() by FVSUM_1:82; now let i,j such that A193: [i,j] in Indices S; A194: i in Seg L by A189,A193,ZFMISC_1:87; assume i>j; then A195: i in dom f \{j} by A188,A194,ZFMISC_1:56; reconsider i9=i,j9=j as Element of NAT by ORDINAL1:def 12; A196: j in Seg L by A189,A193,ZFMISC_1:87; thus S*(i,j) = A9*(idL.i9,f.j9) by A193,MATRIX13:def 1 .= A9*(i,f.j) by A194,FINSEQ_2:49 .= A9*(i,f/.j) by A188,A196,PARTFUN1:def 6 .= 0.K() by A184,A188,A196,A195; end; then S is upper_triangular Matrix of L,K() by MATRIX_1:def 8; then A197: Det S<>0.K() by A192,MATRIX13:7; A198: len Segm(A9,Seg L,Seg width A9)=card Seg L by MATRIX_0:def 2; A199: width A9=m() by A4,MATRIX_0:23; [:rng idL,rng F9:] c= Indices A9 by A183,A187,A185,A186,A199, ZFMISC_1:96; then A200: the_rank_of A9 >= L by A197,MATRIX13:76; A201: now set w0=width A9 |-> 0.K(); let i such that A202: i in dom A9\(Seg L); set LA=Line(A9,i); A203: now not i in Seg L by A202,XBOOLE_0:def 5; then A204: i > L or i<1; let j such that A205: 1<=j and A206: j<=width A9; A207: j in Seg width A9 by A205,A206; A208: i in dom A9 by A202,XBOOLE_0:def 5; then A209: [i,j] in Indices A9 by A207,ZFMISC_1:87; thus LA.j = A9*(i,j) by A207,MATRIX_0:def 7 .= 0.K() by A180,A186,A199,A206,A208,A209,A204,FINSEQ_1:1 .= w0.j by A207,FINSEQ_2:57; end; len LA=width A9 & len w0=width A9 by CARD_1:def 7; hence Line(A9,i) = width A9 |-> 0.K() by A203; end; then the_rank_of A9=the_rank_of Segm(A9,Seg L,Seg width A9) by A187,A185 ,A186,Th11; then the_rank_of A9 <= card Seg L by A198,MATRIX13:74; then A210: the_rank_of A9 <= L by FINSEQ_1:57; then A211: r=L by A178,A200,XXREAL_0:1; thus for i st i in dom A9 & i > r holds Line(A9,i)=m() |->0.K() proof let i such that A212: i in dom A9 and A213: i > r; not i in Seg L by A211,A213,FINSEQ_1:1; then i in dom A9\(Seg L) by A212,XBOOLE_0:def 5; hence thesis by A199,A201; end; take f; thus thesis by A4,A181,A183,A184,A200,A210,MATRIX_0:23,XXREAL_0:1; end; end; then consider A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K() such that A214: P[A9,B9] and A215: r = the_rank_of A9 and A216: for i st i in dom A9 & i > r holds Line(A9,i)=m() |->0.K() and A217: ex f be FinSequence of NAT st len f = the_rank_of A9 & f is one-to-one & rng f c= Seg width A9 & for i,j st i in dom f holds PP[f,i,j,A9] ; consider f be FinSequence of NAT such that A218: len f = the_rank_of A9 and A219: f is one-to-one and A220: rng f c= Seg width A9 and A221: for i,j st i in dom f holds PP[f,i,j,A9] by A217; not 0 in rng f by A220; then reconsider rngf=rng f as without_zero finite Subset of NAT by A220, MEASURE6:def 2,XBOOLE_1:1; A222: n()=0 or n()>0; set S=Segm(A9,Seg card rngf,rngf); A223: dom f=Seg r by A215,A218,FINSEQ_1:def 3; take A9,B9,rngf; len A9 = n() by MATRIX_0:def 2; then width A9 = 0 or width A9 = m() by A222,MATRIX_0:23,def 3; then Seg width A9 c= Seg m(); hence rngf c= Seg m() & r = the_rank_of A9 by A215,A220; dom f,rngf are_equipotent by A219,WELLORD2:def 4; hence A224: card rngf = card dom f by CARD_1:5 .= card Seg r by A215,A218,FINSEQ_1:def 3 .= r by FINSEQ_1:57; now let i,j; assume that A225: i in dom f & j in dom f and A226: i < j; f.i=f/.i & f.j=f/.j by A225,PARTFUN1:def 6; hence f.i < f.j by A221,A225,A226; end; then A227: Sgm rngf = f by A219,A220,Th6; thus P[A9,B9] by A214; A228: card Seg card rngf=card rngf by FINSEQ_1:57; then A229: Indices S = [:Seg r,Seg r:] by A224,MATRIX_0:24; now let i,j be Nat such that A230: i in Seg r and A231: j in Seg r and A232: i <> j; A233: i in dom f\{j} by A223,A230,A232,ZFMISC_1:56; A234: idseq r.i=i by A230,FINSEQ_2:49; [i,j] in Indices S by A229,A230,A231,ZFMISC_1:87; then S*(i,j) = A9*(Sgm (Seg r).i,f.j) by A224,A227,MATRIX13:def 1 .= A9*(i,f.j) by A234,FINSEQ_3:48 .= A9*(i,f/.j) by A223,A231,PARTFUN1:def 6; hence S*(i,j) = 0.K() by A221,A223,A231,A233; end; hence S is diagonal by A224,A228,MATRIX_7:def 2; thus for i st i in Seg card rngf holds A9*(i,Sgm rngf/.i) <> 0.K() by A221 ,A224,A227,A223; thus for i st i in dom A9 & i > card rngf holds Line(A9,i) = m() |->0.K() by A216,A224; let i,j such that A235: i in Seg card rngf and A236: j in Seg width A9 and A237: j < Sgm rngf.i; j Field, n,m,m9() -> Nat, A() -> Matrix of n(),m(),K(), B() -> Matrix of n(),m9(),K(), F(Matrix of n(),m9(),K(),Nat,Nat,Element of K()) -> Matrix of n(),m9(),K(), P[set,set]}: ex A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K(), N be without_zero finite Subset of NAT st N c= Seg m() & the_rank_of A() = the_rank_of A9 & the_rank_of A() = card N & P[A9,B9] & Segm (A9,Seg card N,N) = 1.(K(),card N) & ( for i st i in dom A9 & i > card N holds Line(A9,i) = m() |->0.K() ) & for i,j st i in Seg card N & j in Seg width A9 & j < Sgm N.i holds A9*(i,j) = 0.K() provided A1: P[A(),B()] and A2: for A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K() st P[ A9,B9] for a be Element of K() for i,j st j in dom A9 & (i = j implies a <> - 1_K() ) holds P[RLine(A9,i,Line(A9,i) + a*Line(A9,j)),F(B9,i,j,a)] proof set r=the_rank_of A(); A3: for A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K() st P[A9,B9 ] for i,j st i <> j & j in dom A9 for a be Element of K() holds P[RLine(A9,i, Line(A9,i) + a*Line(A9,j)),F(B9,i,j,a)] by A2; consider A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K(), N be without_zero finite Subset of NAT such that A4: N c= Seg m() and A5: r = the_rank_of A9 & r = card N and A6: ( P[A9,B9] & Segm(A9,Seg card N,N) is diagonal & for i st i in Seg card N holds A9*(i,Sgm N/.i) <> 0.K() )&( ( for i st i in dom A9 & i > card N holds Line(A9,i) = m() |->0.K())& for i,j st i in Seg card N & j in Seg width A9 & j < Sgm N.i holds A9*(i,j) = 0.K() ) from GAUSS1(A1,A3); set ONE=1.(K(),card N); A7: Indices ONE = [:Seg r,Seg r:] by A5,MATRIX_0:24; defpred Q[Nat] means $1 <= card N implies ex A9 be Matrix of n(),m(),K(), B9 be Matrix of n(),m9(),K() st r = the_rank_of A9 & ( for i st i in Seg card N & i<=$1 holds A9*(i,Sgm N/.i) = 1_K() )& P[A9,B9] & Segm(A9,Seg card N,N) is diagonal & ( for i st i in Seg card N holds A9*(i,Sgm N/.i) <> 0.K() )& ( for i st i in dom A9 & i > card N holds Line(A9,i) = m() |->0.K())& ( for i,j st i in Seg card N & j in Seg width A9 & j < Sgm N.i holds A9*(i,j) = 0.K()); A8: for n st Q[n] holds Q[n+1] proof set f=Sgm N; let n such that A9: Q[n]; set n1=n+1; assume A10: n1<=card N; then consider A1 be Matrix of n(),m(),K(),A25 be Matrix of n(),m9(),K() such that A11: r = the_rank_of A1 and A12: for i st i in Seg card N & i<=n holds A1*(i,Sgm N/.i) = 1_K() and A13: P[A1,A25] and A14: Segm(A1,Seg card N,N) is diagonal and A15: for i st i in Seg card N holds A1*(i,Sgm N/.i) <> 0.K() and A16: for i st i in dom A1 & i > card N holds Line(A1,i) = m() |->0.K() and A17: for i,j st i in Seg card N & j in Seg width A1 & j < Sgm N.i holds A1*(i,j) = 0.K() by A9,NAT_1:13; set L=Line(A1,n1); set LL=L+((A1*(n1,f/.n1))"-1_K())*L; set R=RLine(A1,n1,LL); take R,FB=F(A25,n1,n1,(A1*(n1,f/.n1))"-1_K()); A18: len A1=n() by MATRIX_0:def 2; set SA=Segm(A1,Seg card N,N); set S=Segm(R,Seg card N,N); A19: len LL=width A1 by CARD_1:def 7; r<=len A9 & len A9=n() by A5,MATRIX13:74,MATRIX_0:def 2; then A20: Seg r c= Seg n() by FINSEQ_1:5; 1<=1+n by NAT_1:11; then A21: n1 in Seg card N by A10; then A22: n()<>0 by A5,A20; then A23: width R=m() by MATRIX_0:23; A24: (A1*(n1,Sgm N/.n1))"-1_K()<>-1.K() proof assume A25: (A1*(n1,Sgm N/.n1))"-1_K()=-1.K(); A26: 0.K() = 1_K()+ -1_K() by VECTSP_1:19 .= (1_K()+(-1_K()))+A1*(n1,Sgm N/.n1)" by A25,RLVECT_1:def 3 .= 0.K()+A1*(n1,Sgm N/.n1)" by VECTSP_1:19 .= A1*(n1,Sgm N/.n1)" by RLVECT_1:def 4; A1*(n1,Sgm N/.n1)<>0.K() by A15,A21; hence thesis by A26,VECTSP_1:25; end; hence the_rank_of R =r by A5,A11,A21,A20,A18,MATRIX13:92; A27: width A1=m() by A22,MATRIX_0:23; A28: LL = 1_K()*L+((A1*(n1,f/.n1))"-1_K())*L by FVSUM_1:57 .= (1_K() +(-1_K()+(A1*(n1,f/.n1))"))*L by FVSUM_1:55 .= ((1_K() +-1_K())+(A1*(n1,f/.n1))")*L by RLVECT_1:def 3 .= (0.K()+A1*(n1,f/.n1)")*L by VECTSP_1:19 .= (A1*(n1,f/.n1))"*L by RLVECT_1:def 4; A29: dom A1=Seg len A1 by FINSEQ_1:def 3; A30: rng Sgm N=N by A4,FINSEQ_1:def 13; A31: dom Sgm N=Seg card N by A4,FINSEQ_3:40; thus A32: for i st i in Seg card N & i<=n1 holds R*(i,Sgm N/.i) = 1_K() proof let i; assume that A33: i in Seg card N and A34: i<=n1; A35: f.i=f/.i & f.i in rng f by A31,A33,FUNCT_1:def 3,PARTFUN1:def 6; then A36: [i,Sgm N/.i] in Indices A1 by A4,A5,A30,A20,A29,A18,A27,A33,ZFMISC_1:87; per cases by A34,NAT_1:8; suppose A37: i<=n; then i0.K() by A15,A33; R*(i,f/.i) = ((A1*(i,f/.i))"*L).(f/.i) & L.(f/.i)=A1*(i,f/.i) by A4,A30 ,A19,A28,A27,A35,A36,A38,MATRIX11:def 3,MATRIX_0:def 7; hence R*(i,f/.i) = (A1*(i,f/.i))"*(A1*(i,f/.i)) by A4,A30,A27,A35, FVSUM_1:51 .= 1_K() by A39,VECTSP_1:def 10; end; end; thus P[R,FB] by A2,A5,A13,A21,A20,A29,A18,A24; thus S is diagonal proof A40: Indices A1=Indices R by MATRIX_0:26; let i,j such that A41: [i,j] in Indices S and A42: S*(i,j) <> 0.K(); reconsider I=i,J=j as Element of NAT by ORDINAL1:def 12; Indices S=[:Seg card Seg card N,Seg width S:] by MATRIX_0:25; then i in Seg card Seg card N by A41,ZFMISC_1:87; then i in Seg card card N by FINSEQ_1:55; then A43: Sgm (Seg card N)=idseq card N & (idseq card N).I=I by FINSEQ_2:49 ,FINSEQ_3:48; then A44: S*(i,j)=R*(I,Sgm N.J) by A41,MATRIX13:def 1; rng Sgm (Seg card N)=(Seg card N) & [:Seg card N,N:] c= Indices A1 by A4,A5,A20,A29,A18,A27,FINSEQ_1:def 13,ZFMISC_1:96; then A45: [I,Sgm N.J] in Indices A1 by A30,A41,A40,A43,MATRIX13:17; then A46: Sgm N.J in Seg width A1 by ZFMISC_1:87; then reconsider SgmNJ=Sgm N.j as Element of NAT; A47: Indices S=Indices SA by MATRIX_0:26; per cases; suppose A48: I=n1; thus i=j proof assume A49: i<>j; R*(I,Sgm N.J)=((A1*(n1,f/.n1))"*L).SgmNJ & L.SgmNJ=A1*(I,SgmNJ) by A19,A28,A45,A46,A48,MATRIX11:def 3,MATRIX_0:def 7; then R*(I,Sgm N.J) = (A1*(n1,f/.n1))"*(A1*(I,SgmNJ)) by A46, FVSUM_1:51 .= (A1*(n1,f/.n1))"*(SA*(i,j)) by A41,A47,A43,MATRIX13:def 1 .= (A1*(n1,f/.n1))"*(0.K()) by A14,A41,A47,A49 .= 0.K(); hence thesis by A41,A42,A43,MATRIX13:def 1; end; end; suppose I<>n1; then R*(I,Sgm N.J) = A1*(Sgm (Seg card N).I,Sgm N.J) by A19,A43,A45, MATRIX11:def 3 .= SA*(i,j) by A41,A47,MATRIX13:def 1; hence thesis by A14,A41,A42,A47,A44; end; end; thus for i st i in Seg card N holds R*(i,Sgm N/.i) <> 0.K() proof let i such that A50: i in Seg card N; f.i=f/.i & f.i in rng f by A31,A50,FUNCT_1:def 3,PARTFUN1:def 6; then A51: [i,Sgm N/.i] in Indices A1 by A4,A5,A30,A20,A29,A18,A27,A50,ZFMISC_1:87; per cases; suppose i=n1; hence thesis by A32,A50; end; suppose i<>n1; then R*(i,Sgm N/.i)=A1*(i,Sgm N/.i) by A19,A51,MATRIX11:def 3; hence thesis by A15,A50; end; end; thus for i st i in dom R & i > card N holds Line(R,i) = m() |->0.K() proof A52: dom R=Seg len R & len R=n() by FINSEQ_1:def 3,MATRIX_0:def 2; let i such that A53: i in dom R & i > card N; thus Line(R,i) = Line(A1,i) by A10,A53,A52,MATRIX11:28 .= m() |->0.K() by A16,A29,A18,A53,A52; end; let i,j such that A54: i in Seg card N and A55: j in Seg width R and A56: j < Sgm N.i; A57: [i,j] in Indices A1 by A5,A20,A29,A18,A27,A23,A54,A55,ZFMISC_1:87; per cases; suppose i=n1; then R*(i,j)=((A1*(n1,f/.n1))"*L).j & L.j=A1*(i,j) by A19,A28,A27,A23,A55 ,A57,MATRIX11:def 3,MATRIX_0:def 7; hence R*(i,j) = (A1*(n1,f/.n1))"*(A1*(i,j)) by A27,A23,A55,FVSUM_1:51 .= (A1*(n1,f/.n1))"*(0.K()) by A17,A27,A23,A54,A55,A56 .= 0.K(); end; suppose i<>n1; hence R*(i,j) = A1*(i,j)by A19,A57,MATRIX11:def 3 .= 0.K() by A17,A27,A23,A54,A55,A56; end; end; for i st i in Seg card N & i<=0 holds A9*(i,Sgm N/.i) = 1_K(); then A58: Q[0] by A5,A6; for n holds Q[n] from NAT_1:sch 2(A58,A8); then consider A be Matrix of n(),m(),K(),B be Matrix of n(),m9(),K()such that A59: r = the_rank_of A and A60: for i st i in Seg card N & i<=card N holds A*(i,Sgm N/.i) = 1_K() and A61: P[A,B] and A62: Segm(A,Seg card N,N) is diagonal and for i st i in Seg card N holds A*(i,Sgm N/.i) <> 0.K() and A63: ( 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 (); take A,B,N; thus N c= Seg m() & r = the_rank_of A & r = card N & P[A,B] by A4,A5,A59,A61; set S=Segm(A,Seg card N,N); A64: card Seg card N=card N by FINSEQ_1:57; then A65: Indices ONE = Indices S by MATRIX_0:26; now A66: dom Sgm N=Seg r by A4,A5,FINSEQ_3:40; let i,j such that A67: [i,j] in Indices ONE; A68: j in Seg r by A7,A67,ZFMISC_1:87; reconsider i9=i,j9=j as Element of NAT by ORDINAL1:def 12; A69: i in Seg r by A7,A67,ZFMISC_1:87; then A70: idseq r.i9=i9 by FINSEQ_2:49; A71: i<=r by A69,FINSEQ_1:1; A72: S*(i,j) = A*(Sgm (Seg r).i9,Sgm N.j9) by A5,A65,A67,MATRIX13:def 1 .= A*(i9,Sgm N.j9) by A70,FINSEQ_3:48 .= A*(i9,Sgm N/.j9) by A68,A66,PARTFUN1:def 6; now per cases; suppose A73: i9=j9; hence S*(i,j) = 1_K() by A5,A60,A69,A71,A72 .= ONE*(i,j) by A67,A73,MATRIX_1:def 3; end; suppose A74: i9<>j9; hence S*(i,j) = 0.K() by A62,A65,A67 .= ONE*(i,j) by A67,A74,MATRIX_1:def 3; end; end; hence S*(i,j) = ONE*(i,j); end; hence thesis by A63,A64,MATRIX_0:27; end; begin :: The main theorem :: The Kronecker-Capelli theorem theorem Th57: for A,B be Matrix of K st len A = len B & (width A = 0 implies width B = 0) holds the_rank_of A = the_rank_of (A^^B) iff Solutions_of(A,B) is non empty proof let A,B be Matrix of K such that A1: len A = len B and A2: width A = 0 implies width B = 0; set wB=width B; set L=len A; reconsider B9=B as Matrix of L,wB,K by A1,MATRIX_0:51; set wA=width A; reconsider A9=A as Matrix of L,wA,K by MATRIX_0:51; deffunc F(Matrix of L,wB,K,Nat,Nat,Element of K) = RLine($1,$2,Line($1,$2) + $4*Line($1,$3)); defpred P[set,set] means for A1 be Matrix of L,wA,K, B1 be Matrix of L,wB,K st A1=$1 & B1=$2 holds the_rank_of (A9^^B9)=the_rank_of (A1^^B1) & Solutions_of (A9,B9)=Solutions_of(A1,B1); A3: for A1 be Matrix of L,wA,K, B1 be Matrix of L,wB,K st P[A1,B1] for a be Element of K for i,j st j in dom A1 & (i = j implies a <> -1_K ) holds P[RLine( A1,i,Line(A1,i) + a*Line(A1,j)),F(B1,i,j,a)] proof let A1 be Matrix of L,wA,K, B1 be Matrix of L,wB,K such that A4: P[A1,B1]; let a be Element of K; let i,j such that A5: j in dom A1 and A6: i = j implies a <> -1_K; set LAj=Line(A1,j); set LAi=Line(A1,i); set RA=RLine(A1,i,LAi + a*LAj); A7: dom A1 = Seg len A1 by FINSEQ_1:def 3 .= Seg L by MATRIX_0:def 2; then A8: Solutions_of(A1,B1)=Solutions_of(RA,F(B1,i,j,a)) by A5,A6,Th40; set RB=F(B1,i,j,a); set LBj=Line(B1,j); set LBi=Line(B1,i); A9: len A1=L & len B1=L by MATRIX_0:def 2; per cases; suppose not i in Seg L; then RA=A1 & RB=B1 by A9,MATRIX13:40; hence thesis by A4; end; suppose A10: i in Seg L; A11: len (A1^^B1)=L by MATRIX_0:def 2; A12: len (a*LAj)=width A1 & len (a*LBj)=width B1 by CARD_1:def 7; A13: len LAi=width A1 & len LBi=width B1 by CARD_1:def 7; len (LAi+a*LAj)=width A1 & len (LBi+a*LBj)=width B1 by CARD_1:def 7; then RA^^RB = RLine(A1^^B1,i,(LAi+a*LAj)^(LBi+a*LBj))by Th18 .= RLine(A1^^B1,i,(LAi^LBi)+((a*LAj)^(a*LBj))) by A13,A12,Th3 .= RLine(A1^^B1,i,(LAi^LBi)+a*(LAj^LBj)) by Th4 .= RLine(A1^^B1,i,Line(A1^^B1,i)+a*(LAj^LBj))by A10,Th15 .= RLine(A1^^B1,i,Line(A1^^B1,i)+a*Line(A1^^B1,j)) by A5,A7,Th15; then the_rank_of (RA^^RB)=the_rank_of (A1^^B1) by A5,A6,A7,A11, MATRIX13:92; hence thesis by A4,A8; end; end; A14: P[A9,B9]; consider A1 be Matrix of L,wA,K, B1 be Matrix of L,wB,K,N such that A15: N c= Seg wA and A16: the_rank_of A9 = the_rank_of A1 & the_rank_of A9 = card N and A17: P[A1,B1] & Segm(A1,Seg card N,N) = 1.(K,card N) and A18: for i st i in dom A1 & i > card N holds Line(A1,i) = wA|->0.K and for i,j st i in Seg card N & j in Seg width A1 & j < Sgm N.i holds A1*(i ,j) = 0.K from GAUSS2(A14,A3); per cases; suppose A19: L=0; then len (A9^^B9)=0 & the_rank_of A =0 by MATRIX13:74,MATRIX_0:def 2; hence thesis by A19,Th51,MATRIX13:74; end; suppose A20: L>0; per cases; suppose A21: N<>{}; set SN=Seg card N; set SS=Seg L\SN; A22: card SN=card N by FINSEQ_1:57; reconsider P2=Sgm SN " SN,Q2 = Sgm Seg wA " N as without_zero finite Subset of NAT by MATRIX13:53; dom Sgm SN=Seg card SN & rng Sgm SN=SN by FINSEQ_1:def 13,FINSEQ_3:40; then A23: P2 = SN by A22,RELAT_1:134; rng Sgm Seg wA=Seg wA by FINSEQ_1:def 13; then A24: Sgm Seg wA.:Q2 = N by A15,FUNCT_1:77; Q2 c= dom Sgm Seg wA & Sgm Seg wA is one-to-one by FINSEQ_3:92 ,RELAT_1:132; then N,Q2 are_equipotent by A24,CARD_1:33; then A25: dom Sgm Seg wA=Seg card Seg wA & card N=card Q2 by CARD_1:5,FINSEQ_3:40; A26: Seg len A1=dom A1 & len A1=L by A20,FINSEQ_1:def 3,MATRIX_0:23; A27: width A1=wA by A20,MATRIX_0:23; A28: now let i such that A29: i in SS; not i in SN by A29,XBOOLE_0:def 5; then A30: i<1 or i> card N; i in Seg L by A29,XBOOLE_0:def 5; hence Line(A1,i)=width A1|->0.K by A18,A26,A27,A30,FINSEQ_1:1; end; card N<=L by A16,MATRIX13:74; then A31: Seg card N c= Seg L by FINSEQ_1:5; A32: len B1=L by A20,MATRIX_0:23; A33: Seg len B1=dom B1 & width B1=wB by A20,FINSEQ_1:def 3,MATRIX_0:23; thus the_rank_of A=the_rank_of(A^^B) implies Solutions_of(A,B) is non empty proof assume the_rank_of A = the_rank_of (A^^B); then the_rank_of A1 = the_rank_of (A1^^B1) by A16,A17; then for i st i in (dom A1)\Seg card N holds Line(A1,i) = width A1|-> 0.K & Line(B1,i) = width B1 |-> 0.K by A26,A32,A28,Th24,XBOOLE_1:36; then A34: Solutions_of(A1,B1)=Solutions_of(Segm(A1,SN,Seg wA), Segm(B1,SN, Seg wB)) by A21,A31,A26,A32,A27,A33,Th45; Segm(Segm(A1,SN,Seg wA),P2,Q2)=1.(K,card N) by A15,A17,MATRIX13:56; then ex X be Matrix of card Seg wA,card Seg wB,K st Segm(X,Seg card Seg wA \ Q2,Seg card Seg wB) = 0.(K,card Seg wA-'card SN,card Seg wB) & Segm(X, Q2,Seg card Seg wB) = Segm(B1,SN,Seg wB) & X in Solutions_of(Segm(A1,SN,Seg wA) ,Segm(B1,SN,Seg wB)) by A21,A22,A23,A25,Th50,RELAT_1:132; hence thesis by A17,A34; end; A35: Seg L\Seg card N c= Seg L by XBOOLE_1:36; thus Solutions_of(A,B) is non empty implies the_rank_of A=the_rank_of (A ^^B) proof assume Solutions_of(A,B) is non empty; then Solutions_of(A1,B1) is non empty by A17; then consider x being object such that A36: x in Solutions_of(A1,B1); set AB=A1^^B1; A37: len Segm(AB,SN,Seg width AB)=card SN by MATRIX_0:def 2; A38: dom AB=Seg len AB & len AB=L by A20,FINSEQ_1:def 3,MATRIX_0:23; reconsider x as Matrix of wA,wB,K by A20,A36,Th53; A39: the_rank_of Segm(AB,Seg L,Seg width A1)=card N by A16,Th19; A40: width AB=width A1+width B1 by A20,MATRIX_0:23; now let i such that A41: i in SS; A42: Line(A1,i)=width A1|->0.K by A28,A41; A43: x in Solutions_of(A1,B1) & i in dom A1 & Line(A1,i)= width A1 |->0.K implies Line(B1,i)=width B1|->0.K by Th41; thus Line(AB,i)=Line(A1,i)^Line(B1,i)by A35,A41,Th15 .=width AB|->0.K by A26,A35,A36,A40,A41,A42,A43,FINSEQ_2:123; end; then the_rank_of Segm(AB,SN,Seg width AB)=the_rank_of AB by A31,A38 ,Th11; then the_rank_of AB<=card SN by A37,MATRIX13:74; then A44: the_rank_of AB<=card N by FINSEQ_1:57; width A1<=width AB by A40,NAT_1:11; then Seg width A1 c= Seg width AB by FINSEQ_1:5; then [:Seg L,Seg width A1:] c= Indices AB by A38,ZFMISC_1:95; then card N <= the_rank_of AB by A39,MATRIX13:79; then the_rank_of AB=card N by A44,XXREAL_0:1; hence thesis by A16,A17; end; end; suppose A45: N={}; set ZERO=0.(K,L,wA); A46: now let i such that A47: 1<=i & i<=L; A48: dom A1=Seg len A1 & len A1=L by FINSEQ_1:def 3,MATRIX_0:def 2; A49: i in Seg L by A47; hence ZERO.i = wA|->0.K by FINSEQ_2:57 .= Line(A1,i) by A18,A45,A49,A48 .= A1.i by A49,MATRIX_0:52; end; A50: len ZERO=L by A20,MATRIX_0:23; A51: width A1=wA by A20,MATRIX_0:23; len A1=L by A20,MATRIX_0:23; then ZERO=A1 by A50,A46; then A52: the_rank_of A=0 by A16,A50,A51,MATRIX13:95; then A53: ZERO=A by MATRIX13:95; A54: Indices (A9^^B9)=[:Seg L,Seg (wA+wB):] by A20,MATRIX_0:23; thus the_rank_of A=the_rank_of(A^^B) implies Solutions_of(A,B) is non empty proof set x = the Matrix of wA,wB,K; assume A55: the_rank_of A = the_rank_of (A^^B); Seg (wA+wB)\Seg wA c= Seg (wA+wB) by XBOOLE_1:36; then A56: [:Seg L,Seg (wA+wB)\Seg wA:] c= Indices (A^^B) by A54,ZFMISC_1:95; Segm(A9^^B9,Seg L,Seg (wA+wB)\Seg wA)=B by Th19; then 0=the_rank_of B by A52,A55,A56,MATRIX13:79; then A57: B=0.(K,L,wB) by A1,MATRIX13:95; then wA=0 & wB=0 or Solutions_of(A9,B9) = the set of all X where X is Matrix of wA, wB,K by A2,A20,A53,Th54; then Solutions_of(A9,B9)={{}} or x in Solutions_of(A9,B9) by A53,A57 ,Th56; hence thesis; end; A58: Indices B9=[:Seg L,Seg wB:] by A20,MATRIX_0:23; A59: wA+wB = width (A9^^B9) by A20,MATRIX_0:23; A60: Indices ZERO=[:Seg L,Seg wA:] by A20,MATRIX_0:23; thus Solutions_of(A,B) is non empty implies the_rank_of A=the_rank_of(A ^^B) proof assume A61: Solutions_of(A,B) is non empty; assume the_rank_of A <> the_rank_of (A^^B); then consider i,j such that A62: [i,j] in Indices (A9^^B9) and A63: (A9^^B9)*(i,j)<>0.K by A52,MATRIX13:94; A64: j in Seg (wA+wB) by A59,A62,ZFMISC_1:87; A65: dom Line(A9^^B9,i)=Seg (wA+wB) by A59,FINSEQ_2:124; A66: len Line(A9,i)=wA by CARD_1:def 7; A67: dom Line(B9,i)=Seg wB by FINSEQ_2:124; A68: dom Line(A9,i)=Seg wA by FINSEQ_2:124; A69: i in Seg L by A54,A62,ZFMISC_1:87; then A70: Line(A9^^B9,i)=Line(A9,i)^Line(B9,i) by Th15; per cases by A64,A66,A65,A70,FINSEQ_1:25; suppose A71: j in dom Line(A9,i); then A72: [i,j] in Indices ZERO by A60,A69,A68,ZFMISC_1:87; (A9^^B9)*(i,j) = Line(A9^^B9,i).j by A59,A64,MATRIX_0:def 7 .= Line(A9,i).j by A70,A71,FINSEQ_1:def 7 .= A9*(i,j) by A68,A71,MATRIX_0:def 7 .= 0.K by A53,A72,MATRIX_3:1; hence thesis by A63; end; suppose ex n st n in dom Line(B9,i) & j=wA + n; then consider n such that A73: n in dom Line(B9,i) and A74: j=wA + n; A75: [i,n] in Indices B by A58,A69,A67,A73,ZFMISC_1:87; A76: B=0.(K,L,wB) by A53,A61,Th52; (A9^^B9)*(i,j) = Line(A9^^B9,i).j by A59,A64,MATRIX_0:def 7 .= Line(B9,i).n by A66,A70,A73,A74,FINSEQ_1:def 7 .= B9*(i,n) by A67,A73,MATRIX_0:def 7 .= 0.K by A75,A76,MATRIX_3:1; hence thesis by A63; end; end; end; end; end; begin :: Space of Solutions of Linear Equations definition let K; let A be Matrix of K; let b be FinSequence of K; func Solutions_of(A,b) -> set equals {f : ColVec2Mx f in Solutions_of(A,ColVec2Mx b )}; coherence; end; theorem Th58: for x st x in Solutions_of(A,ColVec2Mx b) ex f st x = ColVec2Mx f & len f = width A proof let x such that A1: x in Solutions_of(A,ColVec2Mx b); consider X such that A2: X=x and A3: len X=width A and A4: width X = width ColVec2Mx b and A * X = ColVec2Mx b by A1; per cases; suppose A5: len X=0; take f=0|-> 0.K; len (ColVec2Mx f)=0 by MATRIX_0:def 2; hence thesis by A2,A3,A5,CARD_2:64; end; suppose A6: len X>0; take Col(X,1); A7: len A=len (ColVec2Mx b) by A1,Th33; len A<>0 by A3,A6,MATRIX_0:def 3; then len b>0 by A7,MATRIX_0:def 2; then width X=1 by A4,MATRIX_0:23; hence thesis by A2,A3,A6,Th26,MATRIX_0:def 8; end; end; theorem Th59: for f st ColVec2Mx f in Solutions_of(A,ColVec2Mx b) holds len f = width A proof let f; assume ColVec2Mx f in Solutions_of(A,ColVec2Mx b); then A1: ex g st ColVec2Mx f = ColVec2Mx g & len g = width A by Th58; len ColVec2Mx f = len f by MATRIX_0:def 2; hence thesis by A1,MATRIX_0:def 2; end; definition let K; let A be Matrix of K; let b be FinSequence of K; redefine func Solutions_of(A,b) -> Subset of (width A)-VectSp_over K; coherence proof Solutions_of(A,b) c= the carrier of (width A)-VectSp_over K proof let x be object; assume x in Solutions_of(A,b); then consider f such that A1: x=f and A2: ColVec2Mx f in Solutions_of(A,ColVec2Mx b); len f=width A by A2,Th59; then (width A)-tuples_on the carrier of K= the carrier of (width A) -VectSp_over K & f is Element of (width A)-tuples_on the carrier of K by FINSEQ_2:92,MATRIX13:102; hence thesis by A1; end; hence thesis; end; end; registration let K; let A be Matrix of K; let k be Element of NAT; cluster Solutions_of(A,k|->0.K) -> linearly-closed for Subset of (width A) -VectSp_over K; coherence proof set V=(width A)-VectSp_over K; set k0=k|->0.K; set S=Solutions_of(A,k0); A1: ColVec2Mx k0=0.(K,k,1) by Th32; A2: now let a being Element of K,v being Element of V; assume v in S; then consider f such that A3: v=f and A4: ColVec2Mx f in Solutions_of(A,ColVec2Mx k0); reconsider f as Element of (width A)-tuples_on the carrier of K by A3, MATRIX13:102; now per cases; suppose k=0; then len (a*0.(K,k,1))=len 0.(K,k,1) & 0.(K,k,1)={} by MATRIX_3:def 5 ; hence 0.(K,k,1)=a*0.(K,k,1); end; suppose A5: k>0; then A6: len 0.(K,k,1)=k & width 0.(K,k,1)=1 by MATRIX_0:23; hence a*0.(K,k,1) = a*(0.K*0.(K,k,1)) by A5,MATRIX_5:24 .= (a*0.K)*0.(K,k,1) by MATRIX_5:11 .= 0.K*0.(K,k,1) .= 0.(K,k,1) by A5,A6,MATRIX_5:24; end; end; then a*ColVec2Mx f in Solutions_of(A,0.(K,k,1)) by A1,A4,Th35; then ColVec2Mx (a*f) in Solutions_of(A,0.(K,k,1)) by Th30; then a*f in Solutions_of(A,k0) by A1; hence a*v in S by A3,MATRIX13:102; end; now let v,u being Element of V such that A7: v in S and A8: u in S; consider f such that A9: v=f and A10: ColVec2Mx f in Solutions_of(A,ColVec2Mx k0) by A7; consider g such that A11: u=g and A12: ColVec2Mx g in Solutions_of(A,ColVec2Mx k0) by A8; A13: len g=width A by A12,Th59; reconsider f,g as Element of (width A)-tuples_on the carrier of K by A9 ,A11,MATRIX13:102; ColVec2Mx f+ColVec2Mx g in Solutions_of(A,0.(K,k,1)+0.(K,k,1)) by A1,A10 ,A12,Th37; then ColVec2Mx f+ColVec2Mx g in Solutions_of(A,0.(K,k,1)) by MATRIX_3:4; then ColVec2Mx (f+g) in Solutions_of(A,0.(K,k,1))by A10,A13,Th28,Th59; then f+g in S by A1; hence v+u in S by A9,A11,MATRIX13:102; end; hence thesis by A2,VECTSP_4:def 1; end; end; theorem Th60: Solutions_of(A,b) is non empty & width A = 0 implies len A=0 proof set S=Solutions_of(A,b); assume that A1: S is non empty and A2: width A=0; consider x being object such that A3: x in S by A1; consider f such that x=f and A4: ColVec2Mx f in Solutions_of(A,ColVec2Mx b) by A3; consider X such that ColVec2Mx f=X and A5: len X = width A and width X = width ColVec2Mx b and A6: A * X = ColVec2Mx b by A4; width (A * X) = width X by A5,MATRIX_3:def 4 .= 0 by A2,A5,MATRIX_0:def 3; hence 0 = len b by A6,MATRIX_0:23 .= len ColVec2Mx b by MATRIX_0:def 2 .= len A by A4,Th33; end; theorem Th61: width A <> 0 or len A = 0 implies Solutions_of(A,len A|->0.K) is non empty proof set L=len A|->0.K; A1: len L=len A by CARD_1:def 7; reconsider A9=A as Matrix of len A,width A,K by MATRIX_0:51; assume A2: width A <> 0 or len A = 0; per cases by A2; suppose len A=0; then Solutions_of(A9,ColVec2Mx L) = {{}} by A1,Th51; then A3: {} in Solutions_of(A9,ColVec2Mx L) by TARSKI:def 1; then consider f such that A4: {} = ColVec2Mx f and len f = width A by Th58; f in Solutions_of(A,L) by A3,A4; hence thesis; end; suppose A5: width A > 0; ColVec2Mx L =0.(K,len A,1) by Th32; then len ColVec2Mx L=len L & the_rank_of A=the_rank_of (A^^(ColVec2Mx L)) by Th23,MATRIX_0:def 2; then Solutions_of(A,ColVec2Mx L) is non empty by A1,A5,Th57; then consider x being object such that A6: x in Solutions_of(A,ColVec2Mx L); consider f such that A7: x = ColVec2Mx f and len f = width A by A6,Th58; f in Solutions_of(A,L) by A6,A7; hence thesis; end; end; definition let K; let A be Matrix of K; assume A1: width A = 0 implies len A = 0; func Space_of_Solutions_of(A) -> strict Subspace of (width A)-VectSp_over K means :Def5: the carrier of it = Solutions_of(A,len A|->0.K); existence proof Solutions_of(A,len A|->0.K) is non empty by A1,Th61; hence thesis by VECTSP_4:34; end; uniqueness by VECTSP_4:29; end; theorem for A be (Matrix of K), b be FinSequence of K st Solutions_of(A,b) is non empty holds Solutions_of(A,b) is Coset of Space_of_Solutions_of A proof let A be (Matrix of K),b be FinSequence of K; set V=(width A)-VectSp_over K; reconsider B=b as Element of (len b)-tuples_on the carrier of K by FINSEQ_2:92; set CB=ColVec2Mx B; assume Solutions_of(A,b) is non empty; then consider x being object such that A1: x in Solutions_of(A,B); consider f such that x=f and A2: ColVec2Mx f in Solutions_of(A,CB) by A1; set Cf=ColVec2Mx f; A3: len f =width A by A2,Th59; then reconsider f as Element of (width A)-tuples_on the carrier of K by FINSEQ_2:92; reconsider F=f as Element of V by MATRIX13:102; A4: len CB=len B & len A=len CB by A2,Th33,MATRIX_0:def 2; width A=0 implies len A=0 by A1,Th60; then A5: the carrier of Space_of_Solutions_of A=Solutions_of(A,len A|->0.K) by Def5; A6: Solutions_of(A,b) c= F+ Space_of_Solutions_of A proof len B=len ((-1_K)*B) & (-1_K)*CB=ColVec2Mx ((-1_K)*B) by Th30,CARD_1:def 7; then A7: CB+(-1_K)*CB = ColVec2Mx (B+(-1_K)*B) by Th28 .= ColVec2Mx (B+-B) by FVSUM_1:59 .= ColVec2Mx (len A|->0.K) by A4,FVSUM_1:26; let y be object; assume y in Solutions_of(A,b); then consider g such that A8: y=g and A9: ColVec2Mx g in Solutions_of(A,CB); len g =width A by A9,Th59; then reconsider g as Element of (width A)-tuples_on the carrier of K by FINSEQ_2:92; set Cg=ColVec2Mx g; reconsider GF=g+(-1_K)*f as Element of V by MATRIX13:102; A10: len f=len ((-1_K)*f) by A3,CARD_1:def 7; width CB=width((-1_K)*CB) & (-1_K)*Cf in Solutions_of(A,(-1_K)*CB) by A2 ,Th35,MATRIX_3:def 5; then A11: Cg+(-1_K)*Cf in Solutions_of(A,ColVec2Mx (len A|->0.K)) by A9,A7,Th37; Cg+(-1_K)*Cf = Cg+ColVec2Mx ((-1_K)*f) by Th30 .=ColVec2Mx (g+(-1_K)*f) by A3,A9,A10,Th28,Th59; then g+(-1_K)*f in Solutions_of(A,len A|->0.K) by A11; then A12: GF in Space_of_Solutions_of A by A5,STRUCT_0:def 5; f+(g+(-1_K)*f) = f+((-1_K)*f+g) by FINSEQOP:33 .= f+(-f+g) by FVSUM_1:59 .= (f+-f)+g by FINSEQOP:28 .= (width A|->0.K)+g by FVSUM_1:26 .= g by FVSUM_1:21; then F+GF=g by MATRIX13:102; hence thesis by A8,A12; end; F+ Space_of_Solutions_of A c=Solutions_of(A,b) proof let y be object; A13: len A=0 or len A<>0; len (len A|-> 0.K) =len A by CARD_1:def 7; then A14: width CB=1 & width ColVec2Mx (len A|->0.K)=1 or width CB=0 & width ColVec2Mx (len A|->0.K)=0 by A4,A13,Th26,MATRIX_0:22; ColVec2Mx (len A|->0.K)=0.(K,len A,1) by Th32; then A15: CB+ColVec2Mx (len A|->0.K)=CB by A4,MATRIX_3:4; assume y in F+ Space_of_Solutions_of A; then consider U be Element of V such that A16: U in Space_of_Solutions_of A and A17: y=F+U by VECTSP_4:42; reconsider u=U as Element of (width A)-tuples_on the carrier of K by MATRIX13:102; u in Solutions_of(A,len A|->0.K) by A5,A16,STRUCT_0:def 5; then consider g such that A18: u=g and A19: ColVec2Mx g in Solutions_of(A,ColVec2Mx (len A|->0.K)); width A = len g by A19,Th59; then ColVec2Mx (f+g)=Cf+ColVec2Mx g by A2,Th28,Th59; then ColVec2Mx (f+g) in Solutions_of(A,CB) by A2,A19,A14,A15,Th37; then f+g in Solutions_of(A,b); hence thesis by A17,A18,MATRIX13:102; end; then F+ Space_of_Solutions_of A =Solutions_of(A,b) by A6; hence thesis by VECTSP_4:def 6; end; theorem Th63: for A st ( width A = 0 implies len A = 0 ) & the_rank_of A = 0 holds Space_of_Solutions_of A = (width A)-VectSp_over K proof let A such that A1: width A = 0 implies len A = 0 and A2: the_rank_of A = 0; set L=len A|->0.K; the carrier of (width A)-VectSp_over K c= Solutions_of(A,L) proof let x be object such that A3: x in the carrier of (width A)-VectSp_over K; reconsider x9=x as Element of (width A)-tuples_on the carrier of K by A3, MATRIX13:102; A4: A=0.(K,len A,width A) & ColVec2Mx L=0.(K,len A,1) by A2,Th32,MATRIX13:95; per cases; suppose A5: len A=0; then Solutions_of(A,ColVec2Mx L)={{}} by A4,Th51; then A6: {} in Solutions_of(A,ColVec2Mx L) by TARSKI:def 1; then consider f such that A7: {} = ColVec2Mx f and A8: len f = width A by Th58; width A=0 by A5,MATRIX_0:def 3; then the carrier of (width A)-VectSp_over K = 0-tuples_on the carrier of K by MATRIX13:102 .= {<*>the carrier of K} by FINSEQ_2:94; then x=<*>the carrier of K by A3,TARSKI:def 1; then f=x by A5,A8,MATRIX_0:def 3; hence thesis by A6,A7; end; suppose A9: len A>0; A10: len x9=width A by CARD_1:def 7; Solutions_of(A,ColVec2Mx L)= the set of all X where X is Matrix of width A,1,K by A1,A4,A9,Th54; then ColVec2Mx x9 in Solutions_of(A,ColVec2Mx L) by A10; hence thesis; end; end; then the carrier of (width A)-VectSp_over K = Solutions_of(A,L) .= the carrier of Space_of_Solutions_of A by A1,Def5; hence thesis by VECTSP_4:31; end; theorem for A st Space_of_Solutions_of A = (width A)-VectSp_over K holds the_rank_of A = 0 proof let A such that A1: Space_of_Solutions_of A = (width A)-VectSp_over K; assume the_rank_of A <> 0; then consider i,j such that A2: [i,j] in Indices A and A3: A*(i,j) <> 0.K by MATRIX13:94; A4: j in Seg width A by A2,ZFMISC_1:87; then A5: width A <> 0; set L=Line(1.(K,width A),j); A6: width 1.(K,width A)=width A by MATRIX_0:24; then A7: dom L=Seg width A by FINSEQ_2:124; A8: Indices 1.(K,width A)=[:Seg width A,Seg width A:] by MATRIX_0:24; A9: now let k such that A10: k in dom L and A11: k<>j; [j,k] in Indices 1.(K,width A) by A4,A7,A8,A10,ZFMISC_1:87; hence 0.K = 1.(K,width A)*(j,k) by A11,MATRIX_1:def 3 .= L.k by A6,A7,A10,MATRIX_0:def 7; end; A12: dom Line(A,i)=Seg width A by FINSEQ_2:124; [j,j] in Indices 1.(K,width A) by A4,A8,ZFMISC_1:87; then 1_K = 1.(K,width A)*(j,j) by MATRIX_1:def 3 .= L.j by A4,A6,MATRIX_0:def 7; then A13: Sum(mlt(L,Line(A,i))) = Line(A,i).j by A4,A7,A12,A9,MATRIX_3:17 .= A*(i,j) by A4,MATRIX_0:def 7; A14: ColVec2Mx (len A|->0.K)=0.(K,len A,1) by Th32; A15: i in dom A by A2,ZFMISC_1:87; L in (width A)-tuples_on the carrier of K by A6; then L in the carrier of Space_of_Solutions_of A by A1,MATRIX13:102; then L in Solutions_of(A,len A|->0.K) by Def5,A5; then consider f such that A16: f=L and A17: ColVec2Mx f in Solutions_of(A,ColVec2Mx (len A|->0.K)); consider X such that A18: X=ColVec2Mx f and A19: len X = width A and width X = width ColVec2Mx (len A|->0.K) and A20: A * X = ColVec2Mx (len A|->0.K) by A17; A21: 1 in Seg 1; A22: dom A=Seg len A by FINSEQ_1:def 3; then len A<>0 by A2,ZFMISC_1:87; then Indices ColVec2Mx (len A|->0.K)=[:Seg len A,Seg 1:] by A14,MATRIX_0:23; then A23: [i,1] in Indices ColVec2Mx (len A|->0.K) by A15,A22,A21,ZFMISC_1:87; then Line(A,i)"*"Col(X,1) = 0.(K,len A,1)*(i,1) by A19,A20,A14,MATRIX_3:def 4 .= 0.K by A14,A23,MATRIX_3:1; then 0.K = Col(X,1)"*"Line(A,i) by FVSUM_1:90 .= Sum(mlt(f,Line(A,i))) by A18,A19,Th26,A5; hence thesis by A3,A16,A13; end; theorem Th65: for i,j st j in Seg m & n>0 & (i = j implies a <> -1_K) holds Space_of_Solutions_of A9 = Space_of_Solutions_of RLine(A9,i,Line(A9,i) + a*Line (A9,j)) proof let i,j such that A1: j in Seg m and A2: n>0 and A3: i = j implies a <> -1_K; set L=len A9|->0.K; set R=RLine(A9,i,Line(A9,i) + a*Line(A9,j)); A4: m<>0 by A1; then A5: width R=n by MATRIX_0:23; len L=len A9 by CARD_1:def 7; then len L = m by MATRIX_0:def 2; then reconsider C=ColVec2Mx L as Matrix of m,1,K; set RC=RLine(C,i,Line(C,i) + a*Line(C,j)); A6: C=0.(K,len A9,1) by Th32; now let i9,j9 be Nat such that A7: [i9,j9] in Indices C; reconsider I=i9,J=j9 as Element of NAT by ORDINAL1:def 12; A8: len (Line(C,i) + a*Line(C,j))=width C by CARD_1:def 7; now per cases; suppose A9: i9=i; A10: 1=width C by A4,MATRIX_0:23; then A11: j9 in Seg 1 by A7,ZFMISC_1:87; then Line(C,j).j9=C*(j,j9) by A10,MATRIX_0:def 7; then A12: (a*Line(C,j)).j9=a*(C*(j,j9)) by A10,A11,FVSUM_1:51; Indices C=[:Seg m,Seg 1:] by A4,MATRIX_0:23; then A13: [j,j9] in Indices C by A1,A11,ZFMISC_1:87; Line(C,i).j9=C*(i,j9) by A10,A11,MATRIX_0:def 7; then (Line(C,i) + a*Line(C,j)).j9 = C*(i,j9)+a*(C*(j,j9)) by A10,A11 ,A12,FVSUM_1:18 .= 0.K +a*(C*(j,j9)) by A6,A7,A9,MATRIX_3:1 .= 0.K +a*0.K by A6,A13,MATRIX_3:1 .= 0.K +0.K .= 0.K by RLVECT_1:def 4 .= C*(i9,j9) by A6,A7,MATRIX_3:1; hence C*(I,J)=RC*(I,J) by A7,A8,A9,MATRIX11:def 3; end; suppose i<>i9; hence C*(I,J)=RC*(I,J) by A7,A8,MATRIX11:def 3; end; end; hence C*(i9,j9)=RC*(i9,j9); end; then RC=C by MATRIX_0:27; then A14: Solutions_of(A9,C)=Solutions_of(R,C) by A1,A3,Th40; set SR=Space_of_Solutions_of R; len A9=m & len R=m by A4,MATRIX_0:23; then A15: the carrier of SR = Solutions_of(R,L) by A2,A5,Def5; set SA=Space_of_Solutions_of A9; A16: width A9=n by A4,MATRIX_0:23; then the carrier of SA = Solutions_of(A9,L) by A2,Def5; hence thesis by A16,A5,A14,A15,VECTSP_4:29; end; theorem Th66: for N st N c= dom A & N is non empty & width A > 0 & for i st i in (dom A) \ N holds Line(A,i) = width A |-> 0.K holds Space_of_Solutions_of A = Space_of_Solutions_of Segm(A,N,Seg width A) proof let N such that A1: N c= dom A and A2: N is non empty and A3: width A>0 and A4: for i st i in (dom A) \ N holds Line(A,i) = width A |-> 0.K; set L=len A|->0.K; set C=ColVec2Mx L; A5: len L=len A by CARD_1:def 7; set S=Segm(A,N,Seg width A); A6: width S=card Seg width A by A2,MATRIX_0:23; then A7: width A=width S by FINSEQ_1:57; set SS=Space_of_Solutions_of S; len S=card N by MATRIX_0:def 2; then A8: the carrier of SS = Solutions_of(S,card N|->0.K) by A3,A6,Def5; set SA=Space_of_Solutions_of A; A9: the carrier of SA = Solutions_of(A,L) by A3,Def5; A10: C=0.(K,len A,1) by Th32; len C=len L by MATRIX_0:def 2; then A11: dom C=dom A by A5,FINSEQ_3:29; A12: dom A=Seg len A by FINSEQ_1:def 3; then A13: Seg len A<>{} by A1,A2; then A14: width C=1 by Th26; then A15: card Seg width C=1 by FINSEQ_1:57; now A16: rng Sgm Seg 1=Seg 1 by FINSEQ_1:def 13; A17: Indices Segm(C,N,Seg width C)=Indices 0.(K,card N,1) by A15,MATRIX_0:26; let k,l such that A18: [k,l] in Indices Segm(C,N,Seg width C); reconsider kk=k,ll=l as Element of NAT by ORDINAL1:def 12; [:N,Seg width C:] c= Indices C & rng Sgm N=N by A1,A12,A11,FINSEQ_1:def 13 ,ZFMISC_1:95; then A19: [Sgm N.kk,Sgm Seg width C.ll] in Indices C by A14,A18,A16,MATRIX13:17; thus Segm(C,N,Seg width C)*(k,l) = C*(Sgm N.kk,Sgm Seg width C.ll) by A18, MATRIX13:def 1 .= 0.K by A10,A19,MATRIX_3:1 .=0.(K,card N,1)*(k,l) by A18,A17,MATRIX_3:1; end; then A20: Segm(C,N,Seg width C) = 0.(K,card N,1) by A15,MATRIX_0:27 .= ColVec2Mx (card N|->0.K) by Th32; now let i such that A21: i in (dom A) \ N; A22: i in dom A by A21,XBOOLE_0:def 5; then Line(C,i) = C.i by A5,A12,MATRIX_0:52 .= (len A|->(width C|->0.K)).i by A10,A13,Th26 .= width C|->0.K by A12,A22,FINSEQ_2:57; hence Line(A,i)=width A|->0.K & Line(C,i)=width C|->0.K by A4,A21; end; then Solutions_of(A,C)=Solutions_of(Segm(A,N,Seg width A),Segm(C,N,Seg width C)) by A1,A2,A11,Th45; hence thesis by A20,A7,A9,A8,VECTSP_4:29; end; Lm7: for A be set st A c= dom g ex ga,gb be FinSequence of K st ga=g*Sgm A & gb=g*Sgm (dom g\A) & Sum g = Sum ga + Sum gb proof A1: rng g c= the carrier of K by FINSEQ_1:def 4; set Ad=the addF of K; A2: dom g=Seg len g by FINSEQ_1:def 3; then A3: dom g=rng idseq len g & dom g=dom idseq len g; let A be set such that A4: A c= dom g; A5: rng Sgm(A)=A by A4,A2,FINSEQ_1:def 13; A6: (idseq len g)"A=A by A4,A2,FUNCT_2:94; A7: dom g\A c= dom g by XBOOLE_1:36; then A8: rng Sgm(dom g\A)=dom g\A by A2,FINSEQ_1:def 13; then reconsider ga=g*Sgm A,gb=g*Sgm (dom g\A) as FinSequence by A4,A5, FINSEQ_1:16,XBOOLE_1:36; (idseq len g)"(dom g\A)=dom g\A by A2,A7,FUNCT_2:94; then A9: Sgm(A)^Sgm(dom g\A) is Permutation of dom g by A6,A3,FINSEQ_3:114; then reconsider gS=g*(Sgm(A)^Sgm(dom g\A)) as FinSequence of K by A2, FINSEQ_2:46; rng ga c=rng g by RELAT_1:26; then A10: rng ga c= the carrier of K by A1; rng gb c=rng g by RELAT_1:26; then rng gb c= the carrier of K by A1; then reconsider ga,gb as FinSequence of K by A10,FINSEQ_1:def 4; take ga,gb; Ad $$ g = Ad "**" gS by A9,FINSOP_1:7,FVSUM_1:8 .= Ad"**"(ga^gb) by A4,A7,A5,A8,Th5 .= Sum ga+Sum gb by FINSOP_1:5,FVSUM_1:8; hence thesis; end; theorem Th67: for A be Matrix of n,m,K, N st card N = n & N c= Seg m & Segm(A, Seg n,N) = 1.(K,n) & n > 0 & m-'n>0 ex MVectors be Matrix of m-'n,m,K st Segm( MVectors,Seg (m-'n),Seg m \ N) = 1.(K,m-'n) & Segm(MVectors,Seg (m-'n),N) = - Segm(A,Seg n,Seg m \N)@ & Lin(lines MVectors) = Space_of_Solutions_of A proof let A be Matrix of n,m,K, N such that A1: card N = n and A2: N c= Seg m and A3: Segm(A,Seg n,N) = 1.(K,n) and A4: n > 0 and A5: m-'n>0; Seg m <>{} by A1,A2,A4,CARD_1:27,XBOOLE_1:3; then A6: m<>0; consider MV be Matrix of m-'n,m,K such that A7: Segm(MV,Seg (m-'n),Seg m \ N) = 1.(K,m-'n) and A8: Segm(MV,Seg (m-'n),N) = -Segm(A,Seg n,Seg m \N)@ and A9: for l for M be Matrix of m,l,K st for i st i in Seg l holds (ex j st j in Seg (m-'n) & Col(M,i) = Line(MV,j)) or Col(M,i) = m|->0.K holds M in Solutions_of(A,0.(K,n,l)) by A1,A2,A3,A4,Th49; A10: width MV=m by A5,MATRIX_0:23; A11: len MV=m-'n & len MV >=the_rank_of MV by MATRIX13:74,MATRIX_0:def 2; A12: Indices MV=[:Seg (m-'n),Seg m:] by A5,MATRIX_0:23; Seg m \ N c= Seg m by XBOOLE_1:36; then A13: [:Seg (m-'n),Seg m \ N:] c= Indices MV by A12,ZFMISC_1:95; A14: width A=m by A4,MATRIX_0:23; A15: len A=n by A4,MATRIX_0:23; lines MV c= Solutions_of(A,len A|->0.K) proof let x be object; assume x in lines MV; then consider k such that A16: k in Seg (m-'n) and A17: x = Line(MV,k) by MATRIX13:103; set C=ColVec2Mx Line(MV,k); A18: m = width MV by A5,MATRIX_0:23 .= len Line(MV,k) by CARD_1:def 7; now let i; assume i in Seg 1; then A19: i=1 by FINSEQ_1:2,TARSKI:def 1; Col(C,1)=Line(MV,k) by A6,A18,Th26; hence (ex j st j in Seg (m-'n) & Col(C,i) = Line(MV,j)) or Col(C,i) = m |->0.K by A16,A19; end; then C in Solutions_of(A,0.(K,n,1)) by A9,A18; then C in Solutions_of(A,ColVec2Mx(len A|->0.K))by A15,Th32; hence thesis by A17; end; then Lin (lines MV) is Subspace of Lin (Solutions_of(A,len A|->0.K)) by A14, VECTSP_7:13; then A20: the carrier of Lin (lines MV) c= the carrier of Lin (Solutions_of(A,len A|->0.K)) by VECTSP_4:def 2; m-'n+0>0 by A5; then m-'n>=1 by NAT_1:19; then A21: Det 1.(K,m-'n)=1_K by MATRIX_7:16; A22: 0.K<>1_K; A23: card Seg m=m by FINSEQ_1:57; then A24: m-'n=m-n by A1,A2,NAT_1:43,XREAL_1:233; A25: card (Seg m \ N) =m-n by A1,A2,A23,CARD_2:44; then A26: card Seg (m-'n)=card (Seg m \ N) by A24,FINSEQ_1:57; EqSegm(MV,Seg (m-'n),Seg m \ N)=1.(K,m-'n) by A7,A24,A25,FINSEQ_1:57 ,MATRIX13:def 3; then m-'n <= the_rank_of MV by A24,A25,A26,A13,A21,A22,MATRIX13:def 4; then A27: the_rank_of MV = m-'n by A11,XXREAL_0:1; A28: the carrier of Space_of_Solutions_of A c= the carrier of Lin(lines MV) proof set SN=Seg m\N; let y be object; assume y in the carrier of Space_of_Solutions_of A; then y in Solutions_of(A,len A|->0.K) by A6,A14,Def5; then consider f such that A29: f=y and A30: ColVec2Mx f in Solutions_of(A,ColVec2Mx (len A|->0.K)); A31: len f=m by A14,A30,Th59; deffunc F(Nat)=f/.(Sgm SN.$1)*Line(MV,$1); A32: dom f=Seg len f by FINSEQ_1:def 3; consider M be FinSequence of (width MV)-tuples_on the carrier of K such that A33: len M= m-'n and A34: for j st j in dom M holds M.j = F(j) from FINSEQ_2:sch 1; A35: dom M = Seg(m-'n) by A33,FINSEQ_1:def 3; reconsider M as FinSequence of the carrier of m-VectSp_over K by A10, MATRIX13:102; reconsider M1=FinS2MX M as Matrix of m-'n,m,K by A33; now let i such that A36: i in Seg (m-'n); take a=f/.(Sgm SN.i); thus Line(M1,i) = M1.i by A36,MATRIX_0:52 .= a * Line(MV,i) by A34,A35,A36; end; then consider L be Linear_Combination of lines MV such that A37: L (#) MX2FinS MV = M1 by A27,MATRIX13:105,108; reconsider SumL=Sum L,f as Element of m-tuples_on the carrier of K by A31, FINSEQ_2:92,MATRIX13:102; now let i such that A38: i in Seg m; A39: SN c= Seg m by XBOOLE_1:36; A40: now per cases; suppose A41: i in N; consider X such that A42: X = ColVec2Mx f and A43: len X = width A and width X=width ColVec2Mx(len A|->0.K) and A44: A * X = ColVec2Mx (len A|->0.K) by A30; A45: f = Col(X,1) by A6,A42,Th26; reconsider F=f as Element of (width A)-tuples_on the carrier of K by A4,MATRIX_0:23; A46: rng Sgm Seg (m-'n)=Seg (m-'n) by FINSEQ_1:def 13; A47: rng Sgm N=N by A2,FINSEQ_1:def 13; then consider x being object such that A48: x in dom Sgm N and A49: Sgm N.x=i by A41,FUNCT_1:def 3; reconsider x as Element of NAT by A48; set L=Line(A,x); A50: dom mlt(L,F)=Seg m by A14,FINSEQ_2:124; then consider mN,mSN be FinSequence of K such that A51: mN = mlt(L,F)*Sgm N and A52: mSN = mlt(L,F)*Sgm SN and A53: Sum mlt(L,F) = Sum mN + Sum mSN by A2,Lm7; A54: dom Sgm N=Seg card N by A2,FINSEQ_3:40; then A55: dom mN=Seg n by A1,A2,A47,A50,A51,RELAT_1:27; Indices 1.(K,n)=[:Seg n,Seg n:] by MATRIX_0:24; then A56: [x,x] in Indices 1.(K,n) by A1,A54,A48,ZFMISC_1:87; A57: Sgm N.x in N by A47,A48,FUNCT_1:def 3; then A58: F.(Sgm N.x)=F/.(Sgm N.x) & L.(Sgm N.x)=A*(x,Sgm N. x) by A2,A14,A31 ,A32,MATRIX_0:def 7,PARTFUN1:def 6; A59: x = (idseq n).x by A1,A54,A48,FINSEQ_2:49 .= Sgm Seg n.x by FINSEQ_3:48; now let j such that A60: j in dom mN and A61: j<>x; Indices 1.(K,n)=[:Seg n,Seg n:] by MATRIX_0:24; then A62: [x,j] in Indices 1.(K,n) by A1,A54,A48,A55,A60,ZFMISC_1:87; A63: Sgm N.j in N by A1,A47,A54,A55,A60,FUNCT_1:def 3; then A64: F.(Sgm N.j)=F/.(Sgm N.j) & L.(Sgm N.j)=A*(x,Sgm N. j) by A2,A14,A31 ,A32,MATRIX_0:def 7,PARTFUN1:def 6; thus mN.j = mlt(L,F).(Sgm N.j) by A51,A60,FUNCT_1:12 .= F/.(Sgm N.j)*(A*(Sgm Seg n.x,Sgm N.j)) by A2,A14,A59,A63,A64, FVSUM_1:61 .= F/.(Sgm N.j)*(1.(K,n)*(x,j)) by A3,A62,MATRIX13:def 1 .= F/.(Sgm N.j)*0.K by A61,A62,MATRIX_1:def 3 .= 0.K; end; then Sum mN=mN.x by A1,A54,A48,A55,MATRIX_3:12; then A65: Sum mN = mlt(L,F).(Sgm N.x) by A1,A54,A48,A51,A55,FUNCT_1:12 .= F/.(Sgm N.x)*(A*(Sgm Seg n.x,Sgm N.x)) by A2,A14,A59,A57,A58, FVSUM_1:61 .= F/.(Sgm N.x)*(1.(K,n)*(x,x)) by A3,A56,MATRIX13:def 1 .= F/.(Sgm N.x)*1_K by A56,MATRIX_1:def 3 .= F/.i by A49 .= f.i by A31,A32,A38,PARTFUN1:def 6; A66: dom Sgm SN=Seg card SN by FINSEQ_3:40,XBOOLE_1:36; A67: rng Sgm SN=SN by A39,FINSEQ_1:def 13; then dom mSN=Seg (m-'n) by A24,A25,A50,A52,A66,RELAT_1:27,XBOOLE_1:36 ; then A68: len mSN=m-'n by FINSEQ_1:def 3; A69: ColVec2Mx (len A|->0.K)=0.(K,len A,1) by Th32; Indices 0.(K,len A,1)=[:Seg len A,Seg 1:] & 1 in Seg 1 by A4,A15, MATRIX_0:23; then A70: [x,1] in Indices 0.(K,len A,1)by A1,A15,A54,A48,ZFMISC_1:87; then A71: 0.K = (ColVec2Mx (len A|->0.K))*(x,1) by A69,MATRIX_3:1 .= Line(A,x)"*"Col(X,1) by A43,A44,A69,A70,MATRIX_3:def 4 .= Sum(mlt(Line(A,x),Col(X,1))); reconsider mSN as Element of (m-'n)-tuples_on the carrier of K by A68 ,FINSEQ_2:92; A72: width M1=m by A5,MATRIX_0:23; now let j such that A73: j in Seg (m-'n); A74: j = idseq(m-'n).j by A73,FINSEQ_2:49 .= Sgm Seg (m-'n).j by FINSEQ_3:48; A75: Line(M1,j) = M1.j by A73,MATRIX_0:52 .= f/.(Sgm SN.j)*Line(MV,j) by A34,A35,A73; A76: Sgm SN.j in SN by A24,A25,A67,A66,A73,FUNCT_1:def 3; then f/.(Sgm SN.j) = F.(Sgm SN.j) & A*(x,Sgm SN.j) = L.(Sgm SN.j) by A14,A31,A32,A39,MATRIX_0:def 7,PARTFUN1:def 6; then A77: f/.(Sgm SN.j) * (A*(x,Sgm SN.j)) = mlt(L,F).(Sgm SN.j) by A14,A39 ,A76,FVSUM_1:61 .= mSN.j by A24,A25,A52,A66,A73,FUNCT_1:13; A78: x = idseq(n).x by A1,A54,A48,FINSEQ_2:49 .= Sgm Seg n.x by FINSEQ_3:48; A79: [:Seg (m-'n),N:] c= Indices MV by A2,A12,ZFMISC_1:95; [j,i] in Indices MV by A2,A12,A41,A73,ZFMISC_1:87; then A80: [j,x] in Indices Segm(MV,Seg (m-'n),N) by A47,A49,A46,A74,A79, MATRIX13:17; then A81: [j,x] in Indices (Segm(A,Seg n,SN)@) by A8,Lm1; then A82: [x,j] in Indices Segm(A,Seg n,SN) by MATRIX_0:def 6; A83: Line(MV,j).i = MV*(Sgm Seg (m-'n).j,Sgm N.x) by A10,A38,A49,A74, MATRIX_0:def 7 .= (-Segm(A,Seg n,Seg m \N)@)*(j,x) by A8,A80,MATRIX13:def 1 .= -((Segm(A,Seg n,Seg m \N)@)*(j,x)) by A81,MATRIX_3:def 2 .= -(Segm(A,Seg n,SN)*(x,j)) by A82,MATRIX_0:def 6 .= -(A*(x,Sgm SN.j)) by A82,A78,MATRIX13:def 1; dom M1=Seg (m-'n) by A33,FINSEQ_1:def 3; hence Col(M1,i).j = M1*(j,i) by A73,MATRIX_0:def 8 .= Line(M1,j).i by A38,A72,MATRIX_0:def 7 .= f/.(Sgm SN.j) * (-(A*(x,Sgm SN.j))) by A2,A10,A41,A75,A83, FVSUM_1:51 .= -(f/.(Sgm SN.j) * (A*(x,Sgm SN.j))) by VECTSP_1:8 .= (-mSN).j by A73,A77,FVSUM_1:23; end; then Col(M1,i)=-mSN by A33,FINSEQ_2:119; hence Sum Col(M1,i) = - Sum mSN by FVSUM_1:75 .= -Sum mSN +(Sum mSN+Sum mN) by A71,A45,A53,RLVECT_1:def 4 .= (-Sum mSN+Sum mSN)+Sum mN by RLVECT_1:def 3 .= 0.K+Sum mN by VECTSP_1:19 .= f.i by A65,RLVECT_1:def 4; end; suppose A84: not i in N; A85: rng Sgm SN=SN by A39,FINSEQ_1:def 13; i in SN by A38,A84,XBOOLE_0:def 5; then consider x being object such that A86: x in dom Sgm SN and A87: Sgm SN.x=i by A85,FUNCT_1:def 3; reconsider x as Element of NAT by A86; A88: dom Sgm SN=Seg card SN by FINSEQ_3:40,XBOOLE_1:36; then A89: Line(M1,x) = M1.x by A24,A25,A86,MATRIX_0:52 .= f/.(Sgm SN.x)*Line(MV,x) by A24,A25,A34,A35,A88,A86; [x,x] in [:Seg (m-'n),Seg (m-'n):] by A24,A25,A88,A86,ZFMISC_1:87; then A90: [x,x] in Indices 1.(K,m-'n) by MATRIX_0:24; x = idseq (m-'n).x by A24,A25,A88,A86,FINSEQ_2:49 .= Sgm Seg (m-'n).x by FINSEQ_3:48; then A91: Line(MV,x).i = MV*(Sgm Seg (m-'n).x,Sgm SN.x) by A10,A38,A87, MATRIX_0:def 7 .= 1.(K,m-'n)*(x,x) by A7,A90,MATRIX13:def 1 .= 1_K by A90,MATRIX_1:def 3; A92: dom Col(M1,i)=Seg len M1 by FINSEQ_2:124; A93: dom M1=Seg len M1 by FINSEQ_1:def 3; A94: len M1=m-n by A5,A24,MATRIX_0:23; A95: width M1=m by A5,MATRIX_0:23; A96: now let j such that A97: j in dom Col(M1,i) and A98: x<>j; A99: Line(M1,j) = M1.j by A92,A97,MATRIX_0:52 .= f/.(Sgm SN.j)*Line(MV,j) by A34,A92,A93,A97; [j,x] in [:Seg (m-'n),Seg (m-'n):] by A24,A25,A88,A86,A92,A94,A97, ZFMISC_1:87; then A100: [j,x] in Indices 1.(K,m-'n) by MATRIX_0:24; j = idseq (m-'n).j by A24,A92,A94,A97,FINSEQ_2:49 .= Sgm Seg (m-'n).j by FINSEQ_3:48; then A101: Line(MV,j).i = MV*(Sgm Seg (m-'n).j,Sgm SN.x) by A10,A38,A87, MATRIX_0:def 7 .= 1.(K,m-'n)*(j,x) by A7,A100,MATRIX13:def 1 .= 0.K by A98,A100,MATRIX_1:def 3; thus Col(M1,i).j = M1*(j,i) by A92,A93,A97,MATRIX_0:def 8 .= (f/.(Sgm SN.j)*Line(MV,j)).i by A38,A95,A99,MATRIX_0:def 7 .= (f/.(Sgm SN.j))*0.K by A10,A38,A101,FVSUM_1:51 .= 0.K; end; Col(M1,i).x = M1*(x,i) by A25,A88,A86,A94,A93,MATRIX_0:def 8 .= Line(M1,x).i by A38,A95,MATRIX_0:def 7 .= (f/.(Sgm SN.x))*1_K by A10,A38,A91,A89,FVSUM_1:51 .= (f/.i) by A87 .= f.i by A31,A32,A38,PARTFUN1:def 6; hence Sum Col(M1,i)=f.i by A25,A88,A86,A92,A94,A96,MATRIX_3:12; end; end; Carrier L c= lines MV by VECTSP_6:def 4; hence SumL.i=f.i by A27,A37,A38,A40,MATRIX13:105,107; end; then A102: SumL=f by FINSEQ_2:119; the carrier of Lin(lines MV) = the set of all Sum(l) where l is Linear_Combination of lines MV by VECTSP_7:def 2; hence thesis by A29,A102; end; take MV; Solutions_of(A,len A|->0.K)=the carrier of Space_of_Solutions_of A by A6,A14 ,Def5; then the carrier of Lin (lines MV) c= the carrier of Space_of_Solutions_of(A ) by A20,VECTSP_7:11; then the carrier of Lin (lines MV) = the carrier of Space_of_Solutions_of(A ) by A28; hence thesis by A14,A7,A8,VECTSP_4:29; end; Lm8: dim Space_of_Solutions_of 1.(K,n) = 0 proof set ONE=1.(K,n); set SS=Space_of_Solutions_of ONE; A1: the carrier of SS c= the carrier of (0).SS proof let x be object such that A2: x in the carrier of SS; A3: len ONE=n by MATRIX_0:24; A4: width ONE=n by MATRIX_0:24; then width ONE=0 implies len ONE=0 by MATRIX_0:24; then x in Solutions_of(ONE,n|->0.K) by A2,A3,Def5; then consider f such that A5: f=x and A6: ColVec2Mx f in Solutions_of(ONE,ColVec2Mx (n|->0.K)); consider X such that A7: X =ColVec2Mx f and A8: len X = width ONE and width X = width ColVec2Mx (n|->0.K) and A9: ONE * X = ColVec2Mx (n|->0.K) by A6; A10: now per cases; suppose A11: n>0; ONE*X=X by A4,A8,MATRIXR2:68; hence n|->0.K = Col(X,1) by A9,A11,Th26 .= f by A4,A7,A8,A11,Th26; end; suppose A12: n=0; then f={} by A4,A7,A8,MATRIX_0:def 2; hence f=n|->0.K by A12; end; end; 0.SS = 0.((width ONE)-VectSp_over K ) by VECTSP_4:11 .= n|->0.K by A4,MATRIX13:102; then f in {0.SS} by A10,TARSKI:def 1; hence thesis by A5,VECTSP_4:def 3; end; the carrier of (0).SS c= the carrier of SS by VECTSP_4:def 2; then the carrier of SS = the carrier of (0).SS by A1; then (0).SS = (Omega).SS by VECTSP_4:29; hence thesis by VECTSP_9:29; end; :: The dimension of Space of Solutions of linear equations theorem Th68: for A st ( width A = 0 implies len A = 0 ) holds dim Space_of_Solutions_of A = width A - the_rank_of A proof let A such that A1: width A = 0 implies len A = 0; set W=width A; set L=len A; reconsider A9=A as Matrix of L,W,K by MATRIX_0:51; per cases; suppose A2: the_rank_of A=0; dim ((width A)-VectSp_over K)=width A by MATRIX13:112; hence thesis by A1,A2,Th63; end; suppose A3: the_rank_of A>0; defpred P[set,set] means for A1 be Matrix of L,W,K st A1=$1 holds Space_of_Solutions_of A9=Space_of_Solutions_of A1; deffunc F(Matrix of L,W,K,Nat,Nat,Element of K) =$1; A4: W>0 by A3,MATRIX13:74; A5: for A1 be Matrix of L,W,K,B1 be Matrix of L,W,K st P[A1,B1] for a be Element of K for i,j st j in dom A1 & (i = j implies a <> -1_K ) holds P[RLine( A1,i,Line(A1,i) + a*Line(A1,j)),F(B1,i,j,a)] proof let A1 be Matrix of L,W,K,B1 be Matrix of L,W,K such that A6: P[A1,B1]; let a be Element of K; A7: dom A1 = Seg len A1 by FINSEQ_1:def 3 .= Seg L by MATRIX_0:def 2; let i,j; assume j in dom A1 &( i = j implies a <> -1_K); then Space_of_Solutions_of RLine(A1,i,Line(A1,i) + a*Line(A1,j)) = Space_of_Solutions_of A1 by A4,A7,Th65 .= Space_of_Solutions_of A9 by A6; hence thesis; end; A8: P[A9,A9]; consider A1 be Matrix of L,W,K,B1 be Matrix of L,W,K,N such that A9: N c= Seg W and A10: the_rank_of A9 = the_rank_of A1 & the_rank_of A9 = card N and A11: P[A1,B1] & Segm(A1,Seg card N,N) = 1.(K,card N) and A12: for i st i in dom A1 & i > card N holds Line(A1,i) = W|->0.K and for i,j st i in Seg card N & j in Seg width A1 & j < Sgm N.i holds A1* (i,j) = 0.K from GAUSS2(A8,A5); A13: 0 card N; i in dom A1 by A24,XBOOLE_0:def 5; hence Line(A1,i) = width A1 |-> 0.K by A12,A22,A14,A25,FINSEQ_1:1; end; card N <= len A1 by A10,MATRIX13:74; then A26: Seg card N c= Seg len A1 by FINSEQ_1:5; width A1>0 by A4,A13,MATRIX_0:23; then A27: Space_of_Solutions_of SN = Space_of_Solutions_of A1 by A3,A10,A26,A22,A23 ,Th66 .= Space_of_Solutions_of A9 by A11; per cases; suppose A28: W-'card N=0; then SN=1.(K,card N) by A9,A11,A14,A21,A18,CARD_2:102; hence thesis by A10,A27,A18,A28,Lm8; end; suppose A29: W-'card N>0; then W-'card N+0>0; then W-'card N>=1 by NAT_1:19; then A30: Det 1.(K,W-'card N)=1_K by MATRIX_7:16; A31: card Seg (W-'card N)=W-'card N & 0.K<>1_K by FINSEQ_1:57; consider MVectors be Matrix of W-'card N,W,K such that A32: Segm(MVectors,Seg (W-'card N),Seg W \ N) = 1.(K,W-'card N) and Segm(MVectors,Seg (W-'card N),N)=-Segm(SN,Seg card N,Seg W \N)@ and A33: Lin(lines MVectors) = Space_of_Solutions_of A9 by A3,A9,A10,A27,A21,A15 ,A20,A29,Th67; len MVectors=W-'card N by A29,MATRIX_0:23; then A34: W-'card N>=the_rank_of MVectors by MATRIX13:74; A35: Seg W \ N c= Seg W by XBOOLE_1:36; Indices MVectors=[:Seg (W-'card N),Seg W:] by A29,MATRIX_0:23; then A36: [:Seg (W-'card N),Seg W \ N:] c= Indices MVectors by A35,ZFMISC_1:95; reconsider B=lines MVectors as Subset of W-VectSp_over K; A37: dom MVectors=Seg len MVectors & len MVectors=W-'card N by FINSEQ_1:def 3 ,MATRIX_0:def 2; EqSegm(MVectors,Seg (W-'card N),Seg W \ N)=1.(K,W-'card N) by A16,A18,A32 ,FINSEQ_1:57,MATRIX13:def 3; then A38: W-'card N<=the_rank_of MVectors by A16,A18,A36,A30,A31,MATRIX13:def 4; then MVectors is without_repeated_line by A34,MATRIX13:105,XXREAL_0:1; then Seg (W-'card N),B are_equipotent by A37,WELLORD2:def 4; then A39: card B = card Seg (W-'card N) by CARD_1:5 .= W-'card N by FINSEQ_1:57; the_rank_of MVectors = W-'card N by A38,A34,XXREAL_0:1; then lines MVectors is linearly-independent by MATRIX13:121; hence thesis by A10,A18,A33,A39,VECTSP_9:26; end; end; end; theorem Th69: for M be Matrix of n,m,K, i,j,a st M is without_repeated_line & j in dom M & (i = j implies a<>-1_K) holds Lin lines M = Lin lines RLine(M,i, Line(M,i)+a*Line(M,j)) proof let M be Matrix of n,m,K, i,j,a such that A1: M is without_repeated_line and A2: j in dom M and A3: i = j implies a<>-1_K; A4: len M=n by MATRIX_0:def 2; set L=Line(M,i)+a*Line(M,j); A5: dom M=Seg len M by FINSEQ_1:def 3; set R=RLine(M,i,L); per cases; suppose not i in dom M; hence thesis by A5,MATRIX13:40; end; suppose A6: i in dom M; then n<>0 by A5,A4; then A7: width M=m by MATRIX_0:23; then reconsider Li=Line(M,i),Lj=Line(M,j) as Vector of m -VectSp_over K by MATRIX13:102; a*Lj=a*Line(M,j) by A7,MATRIX13:102; then A8: L=Li+a*Lj by A7,MATRIX13:102; A9: Li = Lj implies (a <> -1_K or Li = 0.(m -VectSp_over K)) proof assume A10: Li=Lj; Li=M.i & Lj=M.j by A2,A5,A4,A6,MATRIX_0:52; hence thesis by A1,A2,A3,A6,A10,FUNCT_1:def 4; end; reconsider L9=L as Element of (the carrier of K)* by FINSEQ_1:def 11; reconsider LL=L9 as set; set iL={i}-->L9; len L=width M by CARD_1:def 7; then A11: R = M+*(i,LL) by MATRIX11:29 .= M+*(i.-->LL) by A6,FUNCT_7:def 3 .= M+*iL by FUNCOP_1:def 9; M.:(dom M\dom iL) = M.:(dom M)\M.:(dom iL) by A1,FUNCT_1:64 .= rng M \ M.:(dom iL) by RELAT_1:113 .= rng M \ Im(M,i) .= rng M \ {M.i} by A6,FUNCT_1:59 .= rng M \ {Line(M,i)} by A5,A4,A6,MATRIX_0:52; then A12: lines R = lines M \ {Line(M,i)} \/rng iL by A11,FRECHET:12 .= lines M \ {Line(M,i)} \/{L} by FUNCOP_1:8; A13: Lj in lines M by A2,A5,A4,MATRIX13:103; Li in lines M by A5,A4,A6,MATRIX13:103; hence thesis by A8,A12,A13,A9,Th14; end; end; theorem Th70: for W be Subspace of m-VectSp_over K ex A be Matrix of dim W,m,K , N be without_zero finite Subset of NAT st N c= Seg m & dim W = card N & Segm( A,Seg dim W,N)=1.(K,dim W) & the_rank_of A = dim W & lines A is Basis of W proof let W be Subspace of m-VectSp_over K; consider I be finite Subset of W such that A1: I is Basis of W by MATRLIN:def 1; I is linearly-independent by A1,VECTSP_7:def 3; then reconsider U=I as linearly-independent Subset of m-VectSp_over K by VECTSP_9:11; defpred P[set,set] means for A be Matrix of card I,m,K,B be Matrix of card I ,m,K st $1=A holds A is without_repeated_line & lines A is linearly-independent & Lin(lines A)=(Omega).W; deffunc F(Matrix of card I,m,K,Nat,Nat,Element of K) = $1; consider M be Matrix of card I,m,K such that A2: M is without_repeated_line & lines M = U by MATRIX13:104; A3: for A9 be Matrix of card I,m,K, B9 be Matrix of card I,m,K st P[A9,B9] for a be Element of K for i,j st j in dom A9 & (i=j implies a<>-1_K) holds P[ RLine(A9,i,Line(A9,i) + a*Line(A9,j)),F(B9,i,j,a)] proof let A9 be Matrix of card I,m,K, B9 be Matrix of card I,m,K such that A4: P[A9,B9]; A5: dom A9=Seg len A9 by FINSEQ_1:def 3; let a be Element of K; let i,j such that A6: j in dom A9 &( i = j implies a <> -1_K); set R=RLine(A9,i,Line(A9,i) + a*Line(A9,j)); A7: A9 is without_repeated_line by A4; then A8: Lin lines A9= Lin lines R by A6,Th69; lines A9 is linearly-independent by A4; then card I = the_rank_of A9 by A7,MATRIX13:121 .= the_rank_of R by A6,A5,MATRIX13:92; hence thesis by A4,A8,MATRIX13:121; end; Lin(I) = the ModuleStr of W by A1,VECTSP_7:def 3; then A9: P[M,M] by A2,VECTSP_9:17; consider A9 be Matrix of card I,m,K, B9 be Matrix of card I,m,K,N such that A10: N c= Seg m and A11: the_rank_of M = the_rank_of A9 & the_rank_of M = card N & P[A9,B9] and A12: Segm(A9,Seg card N,N) = 1.(K,card N) and for i st i in dom A9 & i > card N holds Line(A9,i) = m|->0.K and for i,j st i in Seg card N & j in Seg width A9 & j < Sgm N.i holds A9*(i ,j) = 0.K from GAUSS2(A9,A3); dim W = card I by A1,VECTSP_9:def 1; then reconsider A9 as Matrix of dim W,m,K; lines A9 c= the carrier of Lin(lines A9) by VECTSP_7:8,STRUCT_0:def 5; then reconsider lA=lines A9 as linearly-independent Subset of W by A11, VECTSP_9:12; take A9,N; A13: Lin(lA) = Lin(lines A9) by VECTSP_9:17; A14: the_rank_of M = card I by A2,MATRIX13:121; A15: card I=dim W by A1,VECTSP_9:def 1; Lin(lines A9) = the ModuleStr of W by A11; hence thesis by A15,A10,A11,A12,A14,A13,VECTSP_7:def 3; end; theorem for W be strict Subspace of m-VectSp_over K st dim W < m ex A be Matrix of m-'dim W,m,K, N be without_zero finite Subset of NAT st card N = m-' dim W & N c= Seg m & Segm(A,Seg(m-'dim W),N) = 1.(K,m-'dim W) & W = Space_of_Solutions_of A proof let W be strict Subspace of m-VectSp_over K such that A1: dim W < m; per cases; suppose A2: dim W=0; then m-'dim W = m by NAT_D:40; then reconsider ONE=1.(K,m) as Matrix of m-'dim W,m,K; take ONE,Seg m; A3: len 1.(K,m)=m by MATRIX_0:24; A4: dim Space_of_Solutions_of ONE=0 by Lm8; A5: m-'dim W=m by A2,NAT_D:40; A6: width 1.(K,m)=m by MATRIX_0:24; Space_of_Solutions_of ONE = (Omega).(Space_of_Solutions_of ONE) .= (0).(Space_of_Solutions_of ONE) by A4,VECTSP_9:29 .= (0).W by A6,VECTSP_4:37 .= (Omega).W by A2,VECTSP_9:29 .= W; hence thesis by A5,A3,A6,FINSEQ_1:57,MATRIX13:46; end; suppose A7: dim W > 0; set ZERO=0.(K,m-'dim W,m); A8: m-dim W>dim W-dim W by A1,XREAL_1:9; A9: m-'dim W=m-dim W by A1,XREAL_1:233; then A10: len ZERO=m-'dim W & width ZERO=m by A8,MATRIX_0:23; A11: card Seg m = m by FINSEQ_1:57; consider A be Matrix of dim W,m,K, N such that A12: N c= Seg m and A13: dim W = card N and A14: Segm(A,Seg dim W,N)=1.(K,dim W) and the_rank_of A = dim W and A15: lines A is Basis of W by Th70; set SA = Segm(A,Seg dim W,(Seg m)\N); A16: card ((Seg m)\N) = card Seg m-card N by A12,CARD_2:44; then A17: width SA =m-card N by A7,A11,MATRIX_0:23; A18: card Seg dim W=dim W by FINSEQ_1:57; then len SA=dim W by A7,MATRIX_0:23; then width (SA@) =dim W by A13,A8,A17,MATRIX_0:54; then A19: width (-SA@) =dim W by MATRIX_3:def 2; A20: card Seg (m-'dim W)=m-'dim W by FINSEQ_1:57; m-'dim W = m-dim W by A1,XREAL_1:233; then reconsider CC=1.(K,m-'dim W) as Matrix of card Seg(m-'dim W),card((Seg m)\ N),K by A13,A16,A11,A20; A21: Seg m\((Seg m)\N) = Seg m /\N & m-'(m-'dim W)=m-(m-'dim W) by NAT_D:35 ,XBOOLE_1:48,XREAL_1:233; A22: Indices ZERO=[:Seg (m-'dim W ), Seg m:] by A9,A8,MATRIX_0:23; then A23: [:Seg (m-'dim W),N:] c= Indices ZERO by A12,ZFMISC_1:95; len (SA@)=m-dim W by A13,A8,A17,MATRIX_0:54; then len (-SA@)=m-'dim W by A9,MATRIX_3:def 2; then reconsider BB=-SA@ as Matrix of card Seg (m-'dim W),card N,K by A13,A20,A19, MATRIX_0:51; A24: N misses (Seg m)\N by XBOOLE_1:79; A25: (Seg m)\N c= Seg m by XBOOLE_1:36; then A26: [:Seg (m-'dim W),(Seg m)\N:] c= Indices ZERO by A22,ZFMISC_1:95; [:Seg (m-'dim W),N:]/\[:Seg (m-'dim W),(Seg m)\N:]= [:Seg (m-'dim W), N/\((Seg m)\N):] by ZFMISC_1:99 .= [:Seg (m-'dim W),{}:] by A24 .= {} by ZFMISC_1:90; then for i,j,bi,bj,ci,cj be Nat st [i,j] in [:Seg (m-'dim W),N:]/\[:Seg (m -'dim W),(Seg m)\N:] & bi=Sgm Seg(m-'dim W)".i & bj=Sgm N".j & ci=Sgm Seg(m-' dim W)".i& cj=Sgm ((Seg m)\N)".j holds BB*(bi,bj) = CC*(ci,cj); then consider M be Matrix of m-'dim W,m,K such that A27: Segm(M,Seg (m-'dim W),N)=BB and A28: Segm(M,Seg (m-'dim W),(Seg m)\N)=CC and for i,j st [i,j] in Indices M\([:Seg (m-'dim W),N:]\/[:Seg (m-'dim W), (Seg m)\N:]) holds M*(i,j) = ZERO*(i,j) by A10,A23,A26,Th9; Seg m /\ N =N by A12,XBOOLE_1:28; then consider MV be Matrix of dim W,m,K such that A29: Segm(MV,Seg dim W,N) = 1.(K,dim W) and A30: Segm(MV,Seg dim W,(Seg m)\N)= -Segm(M,Seg (m-'dim W),N)@ and A31: Lin(lines MV) = Space_of_Solutions_of M by A7,A13,A9,A8,A16,A11,A28,A21 ,Th67,XBOOLE_1:36; A32: now A33: Indices A=[:Seg dim W, Seg m:] by A7,MATRIX_0:23; let i,j such that A34: [i,j] in Indices A; A35: i in Seg dim W by A34,A33,ZFMISC_1:87; A36: Indices A=Indices MV by MATRIX_0:26; A37: rng Sgm Seg dim W=Seg dim W by FINSEQ_1:def 13; dom Sgm Seg dim W=Seg dim W by A18,FINSEQ_3:40; then consider x being object such that A38: x in Seg dim W and A39: (Sgm Seg dim W).x=i by A35,A37,FUNCT_1:def 3; reconsider x as Element of NAT by A38; A40: j in Seg m by A34,A33,ZFMISC_1:87; now per cases; suppose A41: j in N; then A42: [i,j] in [:Seg dim W,N:] by A35,ZFMISC_1:87; A43: rng Sgm N=N by A12,FINSEQ_1:def 13; dom Sgm N=Seg dim W by A12,A13,FINSEQ_3:40; then consider y being object such that A44: y in Seg dim W and A45: (Sgm N).y=j by A41,A43,FUNCT_1:def 3; reconsider y as Element of NAT by A44; A46: [:Seg dim W,N:] c= Indices A by A12,A33,ZFMISC_1:95; then A47: [x,y] in Indices Segm(MV,Seg dim W,N) by A36,A37,A39,A43,A45,A42, MATRIX13:17; [x,y] in Indices Segm(A,Seg dim W,N) by A37,A39,A43,A45,A46,A42, MATRIX13:17; hence A*(i,j) = Segm(MV,Seg dim W,N)*(x,y) by A14,A29,A39,A45, MATRIX13:def 1 .= MV*(i,j) by A39,A45,A47,MATRIX13:def 1; end; suppose not j in N; then A48: j in Seg m\N by A40,XBOOLE_0:def 5; then A49: [i,j] in [:Seg dim W,Seg m\N:] by A35,ZFMISC_1:87; A50: rng Sgm (Seg m\N)=(Seg m\N) by A25,FINSEQ_1:def 13; dom Sgm(Seg m\N)=Seg(m-'dim W) by A13,A9,A16,A11,FINSEQ_3:40 ,XBOOLE_1:36; then consider y being object such that A51: y in Seg (m-'dim W) and A52: (Sgm (Seg m\N)).y=j by A48,A50,FUNCT_1:def 3; reconsider y as Element of NAT by A51; A53: [:Seg dim W,Seg m\N:] c= Indices A by A25,A33,ZFMISC_1:95; then A54: [x,y] in Indices Segm(A,Seg dim W,Seg m\N) by A37,A39,A50,A52,A49, MATRIX13:17; A55: [x,y] in Indices Segm(MV,Seg dim W,Seg m\N) by A36,A37,A39,A50,A52 ,A53,A49,MATRIX13:17; then A56: [x,y] in Indices (Segm(M,Seg (m-'dim W),N)@) by A30,Lm1; then A57: [y,x] in Indices Segm(M,Seg (m-'dim W),N) by MATRIX_0:def 6; then A58: [y,x] in Indices SA@ by A27,Lm1; thus MV*(i,j) = (-Segm(M,Seg (m-'dim W),N)@)*(x,y) by A30,A39,A52,A55 ,MATRIX13:def 1 .= -(Segm(M,Seg (m-'dim W),N)@)*(x,y) by A56,MATRIX_3:def 2 .= -(-SA@)*(y,x) by A27,A57,MATRIX_0:def 6 .= --(SA@)*(y,x) by A58,MATRIX_3:def 2 .= (SA@)*(y,x) by RLVECT_1:17 .= SA*(x,y) by A54,MATRIX_0:def 6 .=A*(i,j) by A39,A52,A54,MATRIX13:def 1; end; end; hence A*(i,j)=MV*(i,j); end; then reconsider lA=lines MV as Subset of W by A15,MATRIX_0:27; take M,Seg m\ N; MV = A by A32,MATRIX_0:27; then Lin(lA) = the ModuleStr of W by A15,VECTSP_7:def 3; hence thesis by A1,A13,A16,A11,A28,A31,VECTSP_9:17,XBOOLE_1:36,XREAL_1:233; end; end; theorem Th72: for A,B be Matrix of K st width A = len B & ( width A = 0 implies len A = 0 ) & ( width B = 0 implies len B = 0 ) holds Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A*B) proof let A,B be Matrix of K such that A1: width A = len B and A2: width A = 0 implies len A = 0 and A3: width B = 0 implies len B = 0; set AB=A*B; A4: len AB=len A by A1,MATRIX_3:def 4; A5: width AB=width B by A1,MATRIX_3:def 4; then reconsider AB as Matrix of len A,width B,K by A4,MATRIX_0:51; the carrier of Space_of_Solutions_of B c= the carrier of Space_of_Solutions_of AB proof let x be object; assume x in the carrier of Space_of_Solutions_of B; then x in Solutions_of(B,len B|->0.K) by A3,Def5; then consider f such that A6: f=x and A7: ColVec2Mx f in Solutions_of(B,ColVec2Mx (len B|->0.K)); consider X such that A8: X=ColVec2Mx f and A9: len X = width B and A10: width X = width ColVec2Mx (len B|->0.K) and A11: B * X = ColVec2Mx (len B|->0.K) by A7; A12: ColVec2Mx (len AB|->0.K)=0.(K,len A,1) by A4,Th32; A13: ColVec2Mx (len B|->0.K)=0.(K,len B,1) by Th32; now per cases; suppose len A=0; then Solutions_of(AB,ColVec2Mx (len AB|->0.K)) ={{}} & X ={} by A4,A5,A9,A12 ,Th51,MATRIX_0:def 3; hence X in Solutions_of(AB,ColVec2Mx (len AB|->0.K)) by TARSKI:def 1; end; suppose A14: len A<>0; then A15: width ColVec2Mx (len AB|->0.K)=1 by A4,Th26 .= width ColVec2Mx (len B|->0.K) by A1,A2,A14,Th26; ColVec2Mx (len AB|->0.K) = A*(B*X) by A1,A2,A11,A13,A12,A14,MATRIXR2:18 .= AB*X by A1,A9,MATRIX_3:33; hence X in Solutions_of(AB,ColVec2Mx (len AB|->0.K)) by A5,A9,A10,A15; end; end; then f in Solutions_of(AB,len AB|->0.K) by A8; hence thesis by A1,A2,A3,A4,A5,A6,Def5; end; hence thesis by A5,VECTSP_4:27; end; theorem for A,B be Matrix of K st width A = len B holds the_rank_of (A*B) <= the_rank_of A & the_rank_of (A*B) <= the_rank_of B proof let A,B be Matrix of K such that A1: width A = len B; set AB=A*B; A2: width AB=width B by A1,MATRIX_3:def 4; per cases; suppose the_rank_of AB=0; hence thesis; end; suppose A3: the_rank_of AB>0; set AT=A@; A4: width AB>0 by A3,MATRIX13:74; then A5: width A>0 by A1,A2,MATRIX_0:def 3; then A6: len AT=width A by MATRIX_0:54; set BT=B@; set BA=BT*AT; width AT=len A by A5,MATRIX_0:54; then A7: width AT = 0 implies len AT = 0 by A5,MATRIX_0:def 3; then A8: dim Space_of_Solutions_of AT = width AT - the_rank_of AT by Th68; A9: width BT=len B by A2,A4,MATRIX_0:54; then width BT = 0 implies len BT = 0 by A2,A4,MATRIX_0:def 3; then A10: Space_of_Solutions_of AT is Subspace of Space_of_Solutions_of BA by A1,A6 ,A9,A7,Th72; A11: width BA=width AT by A1,A6,A9,MATRIX_3:def 4; then dim Space_of_Solutions_of BA = width BA - the_rank_of BA by A5,A7,Th68 ,MATRIX_0:54; then width AT - the_rank_of AT<=width AT - the_rank_of BA by A11,A10,A8, VECTSP_9:25; then the_rank_of AT >= the_rank_of BA by XREAL_1:10; then A12: the_rank_of A >= the_rank_of BA by MATRIX13:84; width A=0 implies len A=0 by A1,A2,A4,MATRIX_0:def 3; then A13: Space_of_Solutions_of B is Subspace of Space_of_Solutions_of AB by A1,A2 ,A4,Th72; dim Space_of_Solutions_of B = width B-the_rank_of B & dim Space_of_Solutions_of AB=width AB-the_rank_of AB by A2,A4,Th68; then A14: width B-the_rank_of B <= width B-the_rank_of AB by A2,A13,VECTSP_9:25; BA=AB@ by A1,A2,A4,MATRIX_3:22; hence thesis by A14,A12,MATRIX13:84,XREAL_1:10; end; end; theorem Th74: for A be Matrix of n,n,K, B be Matrix of K st Det A <> 0.K & width A = len B & ( width B = 0 implies len B = 0 ) holds Space_of_Solutions_of B = Space_of_Solutions_of (A*B) proof let A be Matrix of n,n,K,B be Matrix of K such that A1: Det A <> 0.K and A2: width A=len B and A3: width B = 0 implies len B = 0; set AB=A*B; A4: len AB=len A by A2,MATRIX_3:def 4; A5: width AB=width B by A2,MATRIX_3:def 4; A6: len A=n by MATRIX_0:24; reconsider AB as Matrix of n,width B,K by A4,A5,MATRIX_0:24,51; A7: width A=n by MATRIX_0:24; A8: the carrier of Space_of_Solutions_of AB c= the carrier of Space_of_Solutions_of B proof A is invertible by A1,LAPLACE:34; then A is_reverse_of A~ by MATRIX_6:def 4; then A9: 1.(K,n)=A~*A by MATRIX_6:def 2; A10: len (A~)=n by MATRIX_0:24; let x be object; assume x in the carrier of Space_of_Solutions_of AB; then x in Solutions_of(AB,len AB|->0.K) by A2,A3,A6,A7,A4,A5,Def5; then consider f such that A11: f=x and A12: ColVec2Mx f in Solutions_of(AB,ColVec2Mx (len AB|->0.K)); consider X such that A13: X=ColVec2Mx f and A14: len X = width AB and A15: width X = width ColVec2Mx (len AB|->0.K) and A16: AB * X = ColVec2Mx (len AB|->0.K) by A12; A17: width (A~)=n by MATRIX_0:24; set BX=B*X; A18: len BX=len B by A5,A14,MATRIX_3:def 4; then A19: BX = 1.(K,n)* BX by A2,A7,MATRIXR2:68 .= A~ * (A*BX) by A2,A6,A9,A17,A18,MATRIX_3:33 .= A~ * ColVec2Mx(len AB|->0.K) by A2,A5,A14,A16,MATRIX_3:33 .= A~ * 0.(K,len AB,1) by Th32; now per cases; suppose A20: n = 0; then 0.(K,len AB,1)={} by A6,A4; hence BX=0.(K,len AB,1) by A2,A18,A20,MATRIX_0:24; end; suppose n>0; hence BX=0.(K,len AB,1) by A6,A4,A10,A17,A19,MATRIXR2:18; end; end; then BX =ColVec2Mx(len AB|->0.K) by Th32; then ColVec2Mx f in Solutions_of(B,ColVec2Mx(len B|->0.K)) by A2,A6,A7,A4,A5,A13 ,A14,A15; then f in Solutions_of(B,len B|->0.K); hence thesis by A3,A11,Def5; end; width A=0 implies len A=0 by A6,MATRIX_0:24; then Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A*B) by A2 ,A3,Th72; then the carrier of Space_of_Solutions_of B c= the carrier of Space_of_Solutions_of (A*B) by VECTSP_4:def 2; then the carrier of Space_of_Solutions_of B = the carrier of Space_of_Solutions_of (A*B) by A8; hence thesis by A5,VECTSP_4:29; end; theorem Th75: for A be Matrix of n,n,K, B be Matrix of K st width A = len B & Det A <> 0.K holds the_rank_of (A*B) = the_rank_of B proof let A be Matrix of n,n,K, B be Matrix of K such that A1: width A = len B and A2: Det A <>0.K; set AB=A*B; A3: len AB=len A by A1,MATRIX_3:def 4; A4: len A=n & width A=n by MATRIX_0:24; A5: width AB=width B by A1,MATRIX_3:def 4; per cases; suppose width AB=0; hence thesis by A1,A3,A5,A4,Lm3; end; suppose A6: width AB>0; then Space_of_Solutions_of B = Space_of_Solutions_of AB & dim Space_of_Solutions_of B = width B-the_rank_of B by A1,A2,A5,Th68,Th74; then width B-the_rank_of B=width B-the_rank_of AB by A5,A6,Th68; hence thesis; end; end; theorem for A be Matrix of n,n,K, B be Matrix of K st len A = width B & Det A <> 0.K holds the_rank_of (B*A) = the_rank_of B proof let A be Matrix of n,n,K,B be Matrix of K such that A1: width B = len A and A2: Det A <> 0.K; set BA=B*A; A3: len BA=len B by A1,MATRIX_3:def 4; A4: width BA=width A by A1,MATRIX_3:def 4; A5: len A=n & width A=n by MATRIX_0:24; per cases; suppose width BA=0; hence thesis by A1,A3,A4,A5,Lm3; end; suppose A6: width BA>0; then A7: width (A@)=len A & len (B@)=width B by A1,A4,A5,MATRIX_0:54; A8: Det (A@)<>0.K by A2,MATRIXR2:43; thus the_rank_of (B*A) = the_rank_of ((B*A)@) by MATRIX13:84 .= the_rank_of ((A@)*(B@)) by A1,A4,A6,MATRIX_3:22 .= the_rank_of (B@) by A1,A8,A7,Th75 .= the_rank_of B by MATRIX13:84; end; end;