:: Solutions of Linear Equations :: by Karol P\c{a}k :: :: Received December 18, 2007 :: Copyright (c) 2007-2021 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, 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; 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 :: MATRIX15:1 width A = len B implies (a*A) * B = a * (A*B); theorem :: MATRIX15:2 1_K * A = A & a * (b * A) = (a * b) * A; theorem :: MATRIX15:3 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); theorem :: MATRIX15:4 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); theorem :: MATRIX15:5 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; theorem :: MATRIX15:6 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; theorem :: MATRIX15:7 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; theorem :: MATRIX15:8 i in Seg m implies Sgm (Seg (n+m)\Seg n).i=n+i; theorem :: MATRIX15:9 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); theorem :: MATRIX15:10 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); theorem :: MATRIX15:11 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); theorem :: MATRIX15:12 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); theorem :: MATRIX15:13 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; theorem :: MATRIX15:14 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; 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; end; theorem :: MATRIX15:15 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); theorem :: MATRIX15:16 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); theorem :: MATRIX15:17 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); theorem :: MATRIX15:18 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); theorem :: MATRIX15:19 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; theorem :: MATRIX15:20 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); theorem :: MATRIX15:21 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); theorem :: MATRIX15:22 for A,B be Matrix of K st len A = len B & width A = 0 holds A ^^ B = B & B ^^ A = B; theorem :: MATRIX15:23 for A,B be Matrix of K st B = 0.(K,len A,m) holds the_rank_of A = the_rank_of (A^^B); theorem :: MATRIX15:24 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; 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 :: MATRIX15:def 1 <*b*>; func ColVec2Mx b -> Matrix of len b,1,D equals :: MATRIX15:def 2 <*b*>@; end; theorem :: MATRIX15:25 MD = LineVec2Mx bD iff Line(MD,1) = bD & len MD = 1; theorem :: MATRIX15:26 ( len MD <> 0 or len bD <> 0 ) implies ( MD = ColVec2Mx bD iff Col(MD,1) = bD & width MD = 1 ); theorem :: MATRIX15:27 len f = len g implies (LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g); theorem :: MATRIX15:28 len f = len g implies (ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g); theorem :: MATRIX15:29 a * LineVec2Mx f =LineVec2Mx (a*f); theorem :: MATRIX15:30 a * ColVec2Mx f = ColVec2Mx (a*f); theorem :: MATRIX15:31 LineVec2Mx (k|->0.K) = 0.(K,1,k); theorem :: MATRIX15:32 ColVec2Mx (k|->0.K) = 0.(K,k,1); begin :: Basis properties of the Solution of Linear Equations definition let K; let A,B; func Solutions_of(A,B) -> set equals :: MATRIX15:def 3 {X : len X = width A & width X = width B & A * X = B}; end; theorem :: MATRIX15:33 Solutions_of(A,B) is non empty implies len A = len B; theorem :: MATRIX15:34 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; theorem :: MATRIX15:35 X in Solutions_of(A,B) implies a*X in Solutions_of(A,a*B) & X in Solutions_of(a*A,a*B); theorem :: MATRIX15:36 a <> 0.K implies Solutions_of(A,B) = Solutions_of(a*A,a*B); theorem :: MATRIX15:37 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); theorem :: MATRIX15:38 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))); theorem :: MATRIX15:39 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))) ; theorem :: MATRIX15:40 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))); theorem :: MATRIX15:41 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; theorem :: MATRIX15:42 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)); theorem :: MATRIX15:43 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)); theorem :: MATRIX15:44 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)); theorem :: MATRIX15:45 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)); theorem :: MATRIX15:46 i in dom A & len A > 1 implies Solutions_of(A,B) c= Solutions_of (DelLine(A,i),DelLine(B,i)); theorem :: MATRIX15:47 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)); theorem :: MATRIX15:48 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)); theorem :: MATRIX15:49 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)); theorem :: MATRIX15:50 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 ); theorem :: MATRIX15:51 for A be Matrix of 0,n,K, B be Matrix of 0,m,K holds Solutions_of(A,B) = {{}} ; theorem :: MATRIX15:52 for B be Matrix of K st Solutions_of(0.(K,n,k),B) is non empty holds B = 0.(K,n,width B); theorem :: MATRIX15:53 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; theorem :: MATRIX15:54 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; theorem :: MATRIX15:55 n>0 & Solutions_of(0.(K,n,0),0.(K,n,m)) is non empty implies m = 0; theorem :: MATRIX15:56 Solutions_of(0.(K,n,0),0.(K,n,0)) = {{}}; begin ::Gaussian eliminations scheme :: MATRIX15:sch 1 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 P[A(),B()] and 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)]; scheme :: MATRIX15:sch 2 GAUSS2{ 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) = 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 P[A(),B()] and 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)]; begin :: The main theorem :: The Kronecker-Capelli theorem theorem :: MATRIX15:57 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; 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 :: MATRIX15:def 4 {f : ColVec2Mx f in Solutions_of(A,ColVec2Mx b )}; end; theorem :: MATRIX15:58 for x st x in Solutions_of(A,ColVec2Mx b) ex f st x = ColVec2Mx f & len f = width A; theorem :: MATRIX15:59 for f st ColVec2Mx f in Solutions_of(A,ColVec2Mx b) holds len f = width A; 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; 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; end; theorem :: MATRIX15:60 Solutions_of(A,b) is non empty & width A = 0 implies len A=0; theorem :: MATRIX15:61 width A <> 0 or len A = 0 implies Solutions_of(A,len A|->0.K) is non empty; definition let K; let A be Matrix of K; assume width A = 0 implies len A = 0; func Space_of_Solutions_of(A) -> strict Subspace of (width A)-VectSp_over K means :: MATRIX15:def 5 the carrier of it = Solutions_of(A,len A|->0.K); end; theorem :: MATRIX15:62 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; theorem :: MATRIX15:63 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; theorem :: MATRIX15:64 for A st Space_of_Solutions_of A = (width A)-VectSp_over K holds the_rank_of A = 0; theorem :: MATRIX15:65 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)); theorem :: MATRIX15:66 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); theorem :: MATRIX15:67 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; :: The dimension of Space of Solutions of linear equations theorem :: MATRIX15:68 for A st ( width A = 0 implies len A = 0 ) holds dim Space_of_Solutions_of A = width A - the_rank_of A; theorem :: MATRIX15:69 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)); theorem :: MATRIX15:70 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; theorem :: MATRIX15:71 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; theorem :: MATRIX15:72 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); theorem :: MATRIX15:73 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; theorem :: MATRIX15:74 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); theorem :: MATRIX15:75 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; theorem :: MATRIX15:76 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;