:: Solutions of Linear Equations
:: by Karol P\c{a}k
::
:: Received December 18, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem Th1: :: MATRIX15:1
for K being Field
for a being Element of K
for A, B being Matrix of K st width A = len B holds
(a * A) * B = a * (A * B)
proofend;

theorem Th2: :: MATRIX15:2
for K being Field
for a, b being Element of K
for A being Matrix of K holds
( (1_ K) * A = A & a * (b * A) = (a * b) * A )
proofend;

Lm1:  for K being Field
for A being Matrix of K holds Indices A = Indices (- A)
proofend;

Lm2:  for n being Nat
for K being Field
for a being Element of K st a <> 0. K holds
(power K) . (a,n) <> 0. K
proofend;

theorem Th3: :: MATRIX15:3
for K being non empty addLoopStr
for f, g, h, w being FinSequence of K st len f = len g &amp; len h = len w holds
(f ^ h) + (g ^ w) = (f + g) ^ (h + w)
proofend;

theorem Th4: :: MATRIX15:4
for K being non empty multMagma
for f, g being FinSequence of K
for a being Element of K holds a * (f ^ g) = (a * f) ^ (a * g)
proofend;

theorem Th5: :: MATRIX15:5
for f being Function
for p1, p2, f1, f2 being FinSequence st rng p1 c= dom f &amp; rng p2 c= dom f &amp; f1 = f * p1 &amp; f2 = f * p2 holds
f * (p1 ^ p2) = f1 ^ f2
proofend;

theorem Th6: :: MATRIX15:6
for f being FinSequence of NAT
for n being Nat st f is one-to-one &amp; rng f c= Seg n &amp; ( for i, j being Nat st i in dom f &amp; j in dom f &amp; i < j holds
f . i < f . j ) holds
Sgm (rng f) = f
proofend;

theorem Th7: :: MATRIX15:7
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of K
for i, j being Nat st i in dom p &amp; j in dom p &amp; i <> j &amp; ( for k being Nat st k in dom p &amp; k <> i &amp; k <> j holds
p . k = 0. K ) holds
Sum p = (p /. i) + (p /. j)
proofend;

theorem Th8: :: MATRIX15:8
for i, m, n being Nat st i in Seg m holds
(Sgm ((Seg (n + m)) \ (Seg n))) . i = n + i
proofend;

theorem Th9: :: MATRIX15:9
for D being non empty set
for A being Matrix of D
for Bx, By, Cx, Cy being finite without_zero Subset of NAT st [:Bx,By:] c= Indices A &amp; [:Cx,Cy:] c= Indices A holds
for B being Matrix of card Bx, card By,D
for C being Matrix of card Cx, card Cy,D st ( for i, j, bi, bj, ci, cj being Nat st [i,j] in [:Bx,By:] /\ [:Cx,Cy:] &amp; bi = ((Sgm Bx) ") . i &amp; bj = ((Sgm By) ") . j &amp; ci = ((Sgm Cx) ") . i &amp; cj = ((Sgm Cy) ") . j holds
B * (bi,bj) = C * (ci,cj) ) holds
ex M being Matrix of len A, width A,D st
( Segm (M,Bx,By) = B &amp; Segm (M,Cx,Cy) = C &amp; ( for i, j being Nat st [i,j] in (Indices M) \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * (i,j) = A * (i,j) ) )
proofend;

theorem Th10: :: MATRIX15:10
for K being Field
for A being Matrix of K
for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] c= Indices A holds
for i, j being Nat st i in (dom A) \ P &amp; j in (Seg (width A)) \ Q &amp; A * (i,j) <> 0. K &amp; Q c= Q9 &amp; (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q))
proofend;

theorem Th11: :: MATRIX15:11
for K being Field
for A being Matrix of K
for N being finite without_zero Subset of NAT st N c= dom A &amp; ( for i being Nat 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))))
proofend;

theorem Th12: :: MATRIX15:12
for K being Field
for A being Matrix of K
for N being finite without_zero Subset of NAT st N c= Seg (width A) &amp; ( for i being Nat 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))
proofend;

theorem Th13: :: MATRIX15:13
for K being Field
for V being VectSp of K
for U being finite Subset of V
for u, v being Vector of V
for a being Element of K st u in U &amp; v in U holds
Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U
proofend;

theorem Th14: :: MATRIX15:14
for K being Field
for V being VectSp of K
for U being finite Subset of V
for u, v being Vector of V
for a being Element of K st u in U &amp; v in U &amp; ( not u = v or a <> - (1_ K) or u = 0. V ) holds
Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U
proofend;

begin

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;
:: original:^^
redefine funcA ^^ B ->  Matrix of n,(width A) + (width B),D;
coherence
 A ^^ B is Matrix of n,(width A) + (width B),D
proofend;
end;

theorem Th15: :: MATRIX15:15
for n, m, k being Nat
for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D
for i being Nat st i in Seg n holds
Line ((A ^^ B),i) = (Line (A,i)) ^ (Line (B,i))
proofend;

theorem Th16: :: MATRIX15:16
for n, m, k being Nat
for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D
for i being Nat st i in Seg (width A) holds
Col ((A ^^ B),i) = Col (A,i)
proofend;

theorem Th17: :: MATRIX15:17
for n, m, k being Nat
for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D
for i being Nat st i in Seg (width B) holds
Col ((A ^^ B),((width A) + i)) = Col (B,i)
proofend;

theorem Th18: :: MATRIX15:18
for n, m, k, i being Nat
for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D
for pA, pB being FinSequence of D st len pA = width A &amp; len pB = width B holds
ReplaceLine ((A ^^ B),i,(pA ^ pB)) = (ReplaceLine (A,i,pA)) ^^ (ReplaceLine (B,i,pB))
proofend;

theorem Th19: :: MATRIX15:19
for n, m, k being Nat
for D being non empty set
for A being Matrix of n,m,D
for B being Matrix of n,k,D holds
( Segm ((A ^^ B),(Seg n),(Seg (width A))) = A &amp; Segm ((A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A)))) = B )
proofend;

theorem Th20: :: MATRIX15:20
for K being Field
for A, B being Matrix of K st len A = len B holds
( the_rank_of A <= the_rank_of (A ^^ B) &amp; the_rank_of B <= the_rank_of (A ^^ B) )
proofend;

theorem :: MATRIX15:21
for K being Field
for A, B being Matrix of K st len A = len B &amp; len A = the_rank_of A holds
the_rank_of A = the_rank_of (A ^^ B)
proofend;

theorem Th22: :: MATRIX15:22
for K being Field
for A, B being Matrix of K st len A = len B &amp; width A = 0 holds
( A ^^ B = B &amp; B ^^ A = B )
proofend;

theorem Th23: :: MATRIX15:23
for m being Nat
for K being Field
for A, B being Matrix of K st B = 0. (K,(len A),m) holds
the_rank_of A = the_rank_of (A ^^ B)
proofend;

theorem Th24: :: MATRIX15:24
for K being Field
for A, B being Matrix of K st the_rank_of A = the_rank_of (A ^^ B) &amp; len A = len B holds
for N being finite without_zero Subset of NAT st N c= dom A &amp; ( for i being Nat st i in N holds
Line (A,i) = (width A) |-> (0. K) ) holds
for i being Nat st i in N holds
Line (B,i) = (width B) |-> (0. K)
proofend;

begin

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*>;
coherence
 <*b*> is Matrix of 1, len b,D ;
func ColVec2Mx b ->  Matrix of len b,1,D equals :: MATRIX15:def 2
<*b*> @ ;
coherence
 <*b*> @ is Matrix of len b,1,D
proofend;
end;

:: deftheorem  defines LineVec2Mx MATRIX15:def_1_:_
 for D being non empty set
for b being FinSequence of D holds LineVec2Mx b = <*b*>;

:: deftheorem  defines ColVec2Mx MATRIX15:def_2_:_
 for D being non empty set
for b being FinSequence of D holds ColVec2Mx b = <*b*> @ ;

theorem Th25: :: MATRIX15:25
for D being non empty set
for bD being FinSequence of D
for MD being Matrix of D holds
( MD = LineVec2Mx bD iff ( Line (MD,1) = bD &amp; len MD = 1 ) )
proofend;

theorem Th26: :: MATRIX15:26
for D being non empty set
for bD being FinSequence of D
for MD being Matrix of D st ( len MD <> 0 or len bD <> 0 ) holds
( MD = ColVec2Mx bD iff ( Col (MD,1) = bD &amp; width MD = 1 ) )
proofend;

theorem :: MATRIX15:27
for K being Field
for f, g being FinSequence of K st len f = len g holds
(LineVec2Mx f) + (LineVec2Mx g) = LineVec2Mx (f + g)
proofend;

theorem Th28: :: MATRIX15:28
for K being Field
for f, g being FinSequence of K st len f = len g holds
(ColVec2Mx f) + (ColVec2Mx g) = ColVec2Mx (f + g)
proofend;

theorem :: MATRIX15:29
for K being Field
for a being Element of K
for f being FinSequence of K holds a * (LineVec2Mx f) = LineVec2Mx (a * f)
proofend;

theorem Th30: :: MATRIX15:30
for K being Field
for a being Element of K
for f being FinSequence of K holds a * (ColVec2Mx f) = ColVec2Mx (a * f)
proofend;

theorem :: MATRIX15:31
for k being Nat
for K being Field holds LineVec2Mx (k |-> (0. K)) = 0. (K,1,k)
proofend;

theorem Th32: :: MATRIX15:32
for k being Nat
for K being Field holds ColVec2Mx (k |-> (0. K)) = 0. (K,k,1)
proofend;

begin

definition
let K be Field;
let A, B be Matrix of K;
func Solutions_of (A,B) ->  set  equals :: MATRIX15:def 3
 {  X where X is Matrix of K : ( len X = width A &amp; width X = width B &amp; A * X = B )  }  ;
coherence
  {  X where X is Matrix of K : ( len X = width A &amp; width X = width B &amp; A * X = B )  }  is set ;
end;

:: deftheorem  defines Solutions_of MATRIX15:def_3_:_
 for K being Field
for A, B being Matrix of K holds Solutions_of (A,B) =  {  X where X is Matrix of K : ( len X = width A &amp; width X = width B &amp; A * X = B )  }  ;

theorem Th33: :: MATRIX15:33
for K being Field
for A, B being Matrix of K st not Solutions_of (A,B) is empty holds
len A = len B
proofend;

theorem :: MATRIX15:34
for i being Nat
for K being Field
for X, A, B being Matrix of K st X in Solutions_of (A,B) &amp; i in Seg (width X) &amp; Col (X,i) = (len X) |-> (0. K) holds
Col (B,i) = (len B) |-> (0. K)
proofend;

theorem Th35: :: MATRIX15:35
for K being Field
for a being Element of K
for X, A, B being Matrix of K st X in Solutions_of (A,B) holds
( a * X in Solutions_of (A,(a * B)) &amp; X in Solutions_of ((a * A),(a * B)) )
proofend;

theorem :: MATRIX15:36
for K being Field
for a being Element of K
for A, B being Matrix of K st a <> 0. K holds
Solutions_of (A,B) = Solutions_of ((a * A),(a * B))
proofend;

Lm3:  for D being non empty set
for A, B being Matrix of D st len A = len B &amp; width A = 0 &amp; width B = 0 holds
A = B
proofend;

theorem Th37: :: MATRIX15:37
for K being Field
for X1, A, B1, X2, B2 being Matrix of K st X1 in Solutions_of (A,B1) &amp; X2 in Solutions_of (A,B2) &amp; width B1 = width B2 holds
X1 + X2 in Solutions_of (A,(B1 + B2))
proofend;

theorem Th38: :: MATRIX15:38
for n, m, k, i being Nat
for K being Field
for a being Element of K
for X being Matrix of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) holds
X in Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i))))))
proofend;

Lm4:  for n, m, k, i being Nat
for K being Field
for a being Element of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st a <> 0. K holds
Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,(a * (Line (A9,i))))),(RLine (B9,i,(a * (Line (B9,i))))))
proofend;

theorem Th39: :: MATRIX15:39
for n, k, j, m, i being Nat
for K being Field
for a being Element of K
for X being Matrix of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) &amp; j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
proofend;

Lm5:  for n, k, j, m, i being Nat
for K being Field
for a being Element of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m &amp; i <> j holds
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)))))))
proofend;

theorem Th40: :: MATRIX15:40
for n, k, j, m, i being Nat
for K being Field
for a being Element of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m &amp; ( i = j implies a <> - (1_ K) ) holds
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)))))))
proofend;

theorem Th41: :: MATRIX15:41
for i being Nat
for K being Field
for X, A, B being Matrix of K st X in Solutions_of (A,B) &amp; i in dom A &amp; Line (A,i) = (width A) |-> (0. K) holds
Line (B,i) = (width B) |-> (0. K)
proofend;

Lm6:  for n, i being Nat
for K being Field
for A being Matrix of K
for nt being Element of n -tuples_on NAT st i in Seg n holds
Line ((Segm (A,nt,(Sgm (Seg (width A))))),i) = Line (A,(nt . i))
proofend;

theorem Th42: :: MATRIX15:42
for n being Nat
for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT st rng nt c= dom A &amp; n > 0 holds
Solutions_of (A,B) c= Solutions_of ((Segm (A,nt,(Sgm (Seg (width A))))),(Segm (B,nt,(Sgm (Seg (width B))))))
proofend;

theorem Th43: :: MATRIX15:43
for n being Nat
for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT st rng nt c= dom A &amp; dom A = dom B &amp; n > 0 &amp; ( for i being Nat st i in (dom A) \ (rng nt) holds
( Line (A,i) = (width A) |-> (0. K) &amp; 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))))))
proofend;

theorem Th44: :: MATRIX15:44
for K being Field
for A, B being Matrix of K
for N being finite without_zero Subset of NAT st N c= dom A &amp; not N is empty holds
Solutions_of (A,B) c= Solutions_of ((Segm (A,N,(Seg (width A)))),(Segm (B,N,(Seg (width B)))))
proofend;

theorem Th45: :: MATRIX15:45
for K being Field
for A, B being Matrix of K
for N being finite without_zero Subset of NAT st N c= dom A &amp; not N is empty &amp; dom A = dom B &amp; ( for i being Nat st i in (dom A) \ N holds
( Line (A,i) = (width A) |-> (0. K) &amp; 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)))))
proofend;

theorem Th46: :: MATRIX15:46
for i being Nat
for K being Field
for A, B being Matrix of K st i in dom A &amp; len A > 1 holds
Solutions_of (A,B) c= Solutions_of ((DelLine (A,i)),(DelLine (B,i)))
proofend;

theorem :: MATRIX15:47
for K being Field
for A, B being Matrix of K
for i being Nat st i in dom A &amp; len A > 1 &amp; Line (A,i) = (width A) |-> (0. K) &amp; i in dom B &amp; Line (B,i) = (width B) |-> (0. K) holds
Solutions_of (A,B) = Solutions_of ((DelLine (A,i)),(DelLine (B,i)))
proofend;

theorem :: MATRIX15:48
for n, m, k being Nat
for K being Field
for A being Matrix of n,m,K
for B being Matrix of n,k,K
for P being Function of (Seg n),(Seg n) holds
( Solutions_of (A,B) c= Solutions_of ((A * P),(B * P)) &amp; ( P is one-to-one implies Solutions_of (A,B) = Solutions_of ((A * P),(B * P)) ) )
proofend;

theorem Th49: :: MATRIX15:49
for n, m being Nat
for K being Field
for A being Matrix of n,m,K
for N being finite without_zero Subset of NAT st card N = n &amp; N c= Seg m &amp; Segm (A,(Seg n),N) = 1. (K,n) &amp; n > 0 holds
ex MVectors being Matrix of m -' n,m,K st
( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) &amp; Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) &amp; ( for l being Nat
for M being Matrix of m,l,K st ( for i being Nat holds
( not i in Seg l or ex j being Nat st
( j in Seg (m -' n) &amp; Col (M,i) = Line (MVectors,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l))) ) )
proofend;

theorem Th50: :: MATRIX15:50
for n, m, l being Nat
for K being Field
for A being Matrix of n,m,K
for B being Matrix of n,l,K
for N being finite without_zero Subset of NAT st card N = n &amp; N c= Seg m &amp; n > 0 &amp; Segm (A,(Seg n),N) = 1. (K,n) holds
ex X being Matrix of m,l,K st
( Segm (X,((Seg m) \ N),(Seg l)) = 0. (K,(m -' n),l) &amp; Segm (X,N,(Seg l)) = B &amp; X in Solutions_of (A,B) )
proofend;

theorem Th51: :: MATRIX15:51
for n, m being Nat
for K being Field
for A being Matrix of 0 ,n,K
for B being Matrix of 0 ,m,K holds Solutions_of (A,B) = {{}}
proofend;

theorem Th52: :: MATRIX15:52
for n, k being Nat
for K being Field
for B being Matrix of K st not Solutions_of ((0. (K,n,k)),B) is empty holds
B = 0. (K,n,(width B))
proofend;

theorem Th53: :: MATRIX15:53
for x being set
for n, k, m being Nat
for K being Field
for A being Matrix of n,k,K
for B being Matrix of n,m,K st n > 0 &amp; x in Solutions_of (A,B) holds
x is Matrix of k,m,K
proofend;

theorem Th54: :: MATRIX15:54
for n, k, m being Nat
for K being Field st n > 0 &amp; k > 0 holds
Solutions_of ((0. (K,n,k)),(0. (K,n,m))) =  {  X where X is Matrix of k,m,K : verum  }
proofend;

theorem :: MATRIX15:55
for n, m being Nat
for K being Field st n > 0 &amp; not Solutions_of ((0. (K,n,0)),(0. (K,n,m))) is empty holds
m = 0
proofend;

theorem Th56: :: MATRIX15:56
for n being Nat
for K being Field holds Solutions_of ((0. (K,n,0)),(0. (K,n,0))) = {{}}
proofend;

begin

scheme :: MATRIX15:sch 1
GAUSS1{ F1() ->  Field, F2() ->  Nat, F3() ->  Nat, F4() ->  Nat, F5() ->  Matrix of F2(),F3(),F1(), F6() ->  Matrix of F2(),F4(),F1(), F7( Matrix of F2(),F4(),F1(), Nat, Nat, Element of F1()) ->  Matrix of F2(),F4(),F1(), P1[ set , set ] } :
 ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() ex N being finite without_zero Subset of NAT st
( N c= Seg F3() &amp; the_rank_of F5() = the_rank_of A9 &amp; the_rank_of F5() = card N &amp; P1[A9,B9] &amp; Segm (A9,(Seg (card N)),N) is diagonal &amp; ( for i being Nat st i in Seg (card N) holds
A9 * (i,((Sgm N) /. i)) <> 0. F1() ) &amp; ( for i being Nat st i in dom A9 &amp; i > card N holds
Line (A9,i) = F3() |-> (0. F1()) ) &amp; ( for i, j being Nat st i in Seg (card N) &amp; j in Seg (width A9) &amp; j < (Sgm N) . i holds
A9 * (i,j) = 0. F1() ) )
provided
A1: P1[F5(),F6()] and
A2: for A9 being Matrix of F2(),F3(),F1()
for B9 being Matrix of F2(),F4(),F1() st P1[A9,B9] holds
for i, j being Nat st i <> j &amp; j in dom A9 holds
for a being Element of F1() holds P1[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),F7(B9,i,j,a)]
proofend;

scheme :: MATRIX15:sch 2
GAUSS2{ F1() ->  Field, F2() ->  Nat, F3() ->  Nat, F4() ->  Nat, F5() ->  Matrix of F2(),F3(),F1(), F6() ->  Matrix of F2(),F4(),F1(), F7( Matrix of F2(),F4(),F1(), Nat, Nat, Element of F1()) ->  Matrix of F2(),F4(),F1(), P1[ set , set ] } :
 ex A9 being Matrix of F2(),F3(),F1() ex B9 being Matrix of F2(),F4(),F1() ex N being finite without_zero Subset of NAT st
( N c= Seg F3() &amp; the_rank_of F5() = the_rank_of A9 &amp; the_rank_of F5() = card N &amp; P1[A9,B9] &amp; Segm (A9,(Seg (card N)),N) = 1. (F1(),(card N)) &amp; ( for i being Nat st i in dom A9 &amp; i > card N holds
Line (A9,i) = F3() |-> (0. F1()) ) &amp; ( for i, j being Nat st i in Seg (card N) &amp; j in Seg (width A9) &amp; j < (Sgm N) . i holds
A9 * (i,j) = 0. F1() ) )
provided
A1: P1[F5(),F6()] and
A2: for A9 being Matrix of F2(),F3(),F1()
for B9 being Matrix of F2(),F4(),F1() st P1[A9,B9] holds
for a being Element of F1()
for i, j being Nat st j in dom A9 &amp; ( i = j implies a <> - (1_ F1()) ) holds
P1[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),F7(B9,i,j,a)]
proofend;

begin

:: The Kronecker-Capelli theorem
theorem Th57: :: MATRIX15:57
for K being Field
for A, B being Matrix of K st len A = len B &amp; ( width A = 0 implies width B = 0 ) holds
( the_rank_of A = the_rank_of (A ^^ B) iff not Solutions_of (A,B) is empty )
proofend;

begin

definition
let K be Field;
let A be Matrix of K;
let b be FinSequence of K;
func Solutions_of (A,b) ->  set  equals :: MATRIX15:def 4
 {  f where f is FinSequence of K : ColVec2Mx f in Solutions_of (A,(ColVec2Mx b))  }  ;
coherence
  {  f where f is FinSequence of K : ColVec2Mx f in Solutions_of (A,(ColVec2Mx b))  }  is set ;
end;

:: deftheorem  defines Solutions_of MATRIX15:def_4_:_
 for K being Field
for A being Matrix of K
for b being FinSequence of K holds Solutions_of (A,b) =  {  f where f is FinSequence of K : ColVec2Mx f in Solutions_of (A,(ColVec2Mx b))  }  ;

theorem Th58: :: MATRIX15:58
for K being Field
for A being Matrix of K
for b being FinSequence of K
for x being set st x in Solutions_of (A,(ColVec2Mx b)) holds
ex f being FinSequence of K st
( x = ColVec2Mx f &amp; len f = width A )
proofend;

theorem Th59: :: MATRIX15:59
for K being Field
for A being Matrix of K
for b, f being FinSequence of K st ColVec2Mx f in Solutions_of (A,(ColVec2Mx b)) holds
len f = width A
proofend;

definition
let K be Field;
let A be Matrix of K;
let b be FinSequence of K;
:: original:Solutions_of
redefine func Solutions_of (A,b) ->  Subset of ((width A) -VectSp_over K);
coherence
 Solutions_of (A,b) is Subset of ((width A) -VectSp_over K)
proofend;
end;

registration
let K be Field;
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
 for b1 being Subset of ((width A) -VectSp_over K) st b1 = Solutions_of (A,(k |-> (0. K))) holds
b1 is linearly-closed
proofend;
end;

theorem Th60: :: MATRIX15:60
for K being Field
for A being Matrix of K
for b being FinSequence of K st not Solutions_of (A,b) is empty &amp; width A = 0 holds
len A = 0
proofend;

theorem Th61: :: MATRIX15:61
for K being Field
for A being Matrix of K st ( width A <> 0 or len A = 0 ) holds
not Solutions_of (A,((len A) |-> (0. K))) is empty
proofend;

definition
let K be Field;
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: :: MATRIX15:def 5
 the carrier of it = Solutions_of (A,((len A) |-> (0. K)));
existence
 ex b1 being strict Subspace of (width A) -VectSp_over K st the carrier of b1 = Solutions_of (A,((len A) |-> (0. K)))
proofend;
uniqueness
 for b1, b2 being strict Subspace of (width A) -VectSp_over K st the carrier of b1 = Solutions_of (A,((len A) |-> (0. K))) &amp; the carrier of b2 = Solutions_of (A,((len A) |-> (0. K))) holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def5 defines Space_of_Solutions_of MATRIX15:def_5_:_
 for K being Field
for A being Matrix of K st ( width A = 0 implies len A = 0 ) holds
for b3 being strict Subspace of (width A) -VectSp_over K holds
( b3 = Space_of_Solutions_of A iff the carrier of b3 = Solutions_of (A,((len A) |-> (0. K))) );

theorem :: MATRIX15:62
for K being Field
for A being Matrix of K
for b being FinSequence of K st not Solutions_of (A,b) is empty holds
Solutions_of (A,b) is Coset of Space_of_Solutions_of A
proofend;

theorem Th63: :: MATRIX15:63
for K being Field
for A being Matrix of K st ( width A = 0 implies len A = 0 ) &amp; the_rank_of A = 0 holds
Space_of_Solutions_of A = (width A) -VectSp_over K
proofend;

theorem :: MATRIX15:64
for K being Field
for A being Matrix of K st Space_of_Solutions_of A = (width A) -VectSp_over K holds
the_rank_of A = 0
proofend;

theorem Th65: :: MATRIX15:65
for m, n being Nat
for K being Field
for a being Element of K
for A9 being Matrix of m,n,K
for i, j being Nat st j in Seg m &amp; n > 0 &amp; ( 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))))))
proofend;

theorem Th66: :: MATRIX15:66
for K being Field
for A being Matrix of K
for N being finite without_zero Subset of NAT st N c= dom A &amp; not N is empty &amp; width A > 0 &amp; ( for i being Nat 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))))
proofend;

Lm7:  for K being Field
for g being FinSequence of K
for A being set st A c= dom g holds
ex ga, gb being FinSequence of K st
( ga = g * (Sgm A) &amp; gb = g * (Sgm ((dom g) \ A)) &amp; Sum g = (Sum ga) + (Sum gb) )
proofend;

theorem Th67: :: MATRIX15:67
for n, m being Nat
for K being Field
for A being Matrix of n,m,K
for N being finite without_zero Subset of NAT st card N = n &amp; N c= Seg m &amp; Segm (A,(Seg n),N) = 1. (K,n) &amp; n > 0 &amp; m -' n > 0 holds
ex MVectors being Matrix of m -' n,m,K st
( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) &amp; Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) &amp; Lin (lines MVectors) = Space_of_Solutions_of A )
proofend;

Lm8:  for n being Nat
for K being Field holds dim (Space_of_Solutions_of (1. (K,n))) = 0
proofend;

:: The dimension of Space of Solutions of linear equations
theorem Th68: :: MATRIX15:68
for K being Field
for A being Matrix of K st ( width A = 0 implies len A = 0 ) holds
dim (Space_of_Solutions_of A) = (width A) - (the_rank_of A)
proofend;

theorem Th69: :: MATRIX15:69
for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for i, j being Nat
for a being Element of K st M is without_repeated_line &amp; j in dom M &amp; ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))
proofend;

theorem Th70: :: MATRIX15:70
for m being Nat
for K being Field
for W being Subspace of m -VectSp_over K ex A being Matrix of dim W,m,K ex N being finite without_zero Subset of NAT st
( N c= Seg m &amp; dim W = card N &amp; Segm (A,(Seg (dim W)),N) = 1. (K,(dim W)) &amp; the_rank_of A = dim W &amp; lines A is Basis of W )
proofend;

theorem :: MATRIX15:71
for m being Nat
for K being Field
for W being strict Subspace of m -VectSp_over K st dim W < m holds
ex A being Matrix of m -' (dim W),m,K ex N being finite without_zero Subset of NAT st
( card N = m -' (dim W) &amp; N c= Seg m &amp; Segm (A,(Seg (m -' (dim W))),N) = 1. (K,(m -' (dim W))) &amp; W = Space_of_Solutions_of A )
proofend;

theorem Th72: :: MATRIX15:72
for K being Field
for A, B being Matrix of K st width A = len B &amp; ( width A = 0 implies len A = 0 ) &amp; ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B)
proofend;

theorem :: MATRIX15:73
for K being Field
for A, B being Matrix of K st width A = len B holds
( the_rank_of (A * B) <= the_rank_of A &amp; the_rank_of (A * B) <= the_rank_of B )
proofend;

theorem Th74: :: MATRIX15:74
for n being Nat
for K being Field
for A being Matrix of n,n,K
for B being Matrix of K st Det A <> 0. K &amp; width A = len B &amp; ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B = Space_of_Solutions_of (A * B)
proofend;

theorem Th75: :: MATRIX15:75
for n being Nat
for K being Field
for A being Matrix of n,n,K
for B being Matrix of K st width A = len B &amp; Det A <> 0. K holds
the_rank_of (A * B) = the_rank_of B
proofend;

theorem :: MATRIX15:76
for n being Nat
for K being Field
for A being Matrix of n,n,K
for B being Matrix of K st len A = width B &amp; Det A <> 0. K holds
the_rank_of (B * A) = the_rank_of B
proofend;