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

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)

proof end;

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 )

proof end;

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

proof end;

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

proof end;

theorem Th3: :: MATRIX15:3

for K being non empty addLoopStr
for f, g, h, w being FinSequence of K st len f = len g & len h = len w holds
(f ^ h) + (g ^ w) = (f + g) ^ (h + w)

proof end;

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)

proof end;

theorem Th5: :: MATRIX15:5

for f being Function
for p1, p2, f1, f2 being 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 end;

theorem Th6: :: MATRIX15:6

for f being FinSequence of NAT
for n being Nat st f is one-to-one & rng f c= Seg n & ( for i, j being Nat st i in dom f & j in dom f & i < j holds
f . i < f . j ) holds
Sgm (rng f) = f

proof end;

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 & j in dom p & i <> j & ( for k being Nat st k in dom p & k <> i & k <> j holds
p . k = 0. K ) holds
Sum p = (p /. i) + (p /. j)

proof end;

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

proof end;

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 & [: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:] & bi = ((Sgm Bx) " ) . i & bj = ((Sgm By) " ) . j & ci = ((Sgm Cx) " ) . i & 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 & Segm M,Cx,Cy = C & ( for i, j being Nat st [i,j] in (Indices M) \ ([:Bx,By:] \/ [:Cx,Cy:]) holds
M * i,j = A * i,j ) )

proof end;

theorem Th10: :: MATRIX15:10

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

proof end;

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 & ( 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)))

proof end;

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) & ( 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)

proof end;

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 & v in U holds
Lin ((U \ {u}) \/ {(u + (a * v))}) is Subspace of Lin U

proof end;

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 & v in U & ( not u = v or a <> - (1_ K) or u = 0. V ) holds
Lin ((U \ {u}) \/ {(u + (a * v))}) = Lin U

proof end;

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 func A ^^ B -> Matrix of n,(width A) + (width B),D;
coherence
A ^^ B is Matrix of n,(width A) + (width B),D

proof end;

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)

proof end;

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

proof end;

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

proof end;

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 & len pB = width B holds
ReplaceLine (A ^^ B),i,(pA ^ pB) = (ReplaceLine A,i,pA) ^^ (ReplaceLine B,i,pB)

proof end;

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 & Segm (A ^^ B),(Seg n),((Seg ((width A) + (width B))) \ (Seg (width A))) = B )

proof end;

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) & the_rank_of B <= the_rank_of (A ^^ B) )

proof end;

theorem :: MATRIX15:21

for K being Field
for A, B being 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 end;

theorem Th22: :: MATRIX15:22

for K being Field
for A, B being Matrix of K st len A = len B & width A = 0 holds
( A ^^ B = B & B ^^ A = B )

proof end;

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)

proof end;

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) & len A = len B holds
for N being finite without_zero Subset of NAT st N c= dom A & ( 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)

proof end;

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

proof end;

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 & len MD = 1 ) )

proof end;

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 & width MD = 1 ) )

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

theorem :: MATRIX15:31

for k being Nat
for K being Field holds LineVec2Mx (k |-> (0. K)) = 0. K,1,k

proof end;

theorem Th32: :: MATRIX15:32

for k being Nat
for K being Field holds ColVec2Mx (k |-> (0. K)) = 0. K,k,1

proof end;

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 & width X = width B & A * X = B ) } ;
coherence
{ X where X is Matrix of K : ( len X = width A & width X = width B & 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 & width X = width B & 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

proof end;

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 & i in Seg (width X) & Col X,i = (len X) |-> (0. K) holds
Col B,i = (len B) |-> (0. K)

proof end;

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) & X in Solutions_of (a * A),(a * B) )

proof end;

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)

proof end;

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

proof end;

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 & X2 in Solutions_of A,B2 & width B1 = width B2 holds
X1 + X2 in Solutions_of A,(B1 + B2)

proof end;

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 A' being Matrix of m,n,K
for B' being Matrix of m,k,K st X in Solutions_of A',B' holds
X in Solutions_of (RLine A',i,(a * (Line A',i))),(RLine B',i,(a * (Line B',i)))

proof end;

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

proof end;

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 A' being Matrix of m,n,K
for B' being Matrix of m,k,K st X in Solutions_of A',B' & j in Seg m & i <> j holds
X in Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))

proof end;

Lm5: for n, k, j, m, i being Nat
for K being Field
for a being Element of K
for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st j in Seg m & i <> j holds
Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))

proof end;

theorem Th40: :: MATRIX15:40

for n, k, j, m, i being Nat
for K being Field
for a being Element of K
for A' being Matrix of m,n,K
for B' being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
Solutions_of A',B' = Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j)))),(RLine B',i,((Line B',i) + (a * (Line B',j))))

proof end;

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 & i in dom A & Line A,i = (width A) |-> (0. K) holds
Line B,i = (width B) |-> (0. K)

proof end;

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)

proof end;

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 & 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 end;

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 & dom A = dom B & n > 0 & ( for i being Nat 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 end;

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 & not N is empty holds
Solutions_of A,B c= Solutions_of (Segm A,N,(Seg (width A))),(Segm B,N,(Seg (width B)))

proof end;

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 & not N is empty & dom A = dom B & ( for i being Nat 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 end;

theorem Th46: :: MATRIX15:46

for i being Nat
for K being Field
for A, B being Matrix of K st i in dom A & len A > 1 holds
Solutions_of A,B c= Solutions_of (DelLine A,i),(DelLine B,i)

proof end;

theorem :: MATRIX15:47

for K being Field
for A, B being Matrix of K
for i being Nat 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 end;

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) & ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) ) )

proof end;

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 & N c= Seg m & Segm A,(Seg n),N = 1. K,n & 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) & Segm MVectors,(Seg (m -' n)),N = - ((Segm A,(Seg n),((Seg m) \ N)) @ ) & ( 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) & Col M,i = Line MVectors,j ) or Col M,i = m |-> (0. K) ) ) holds
M in Solutions_of A,(0. K,n,l) ) )

proof end;

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 & N c= Seg m & n > 0 & 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 & Segm X,N,(Seg l) = B & X in Solutions_of A,B )

proof end;

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 = {{} }

proof end;

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)

proof end;

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 & x in Solutions_of A,B holds
x is Matrix of k,m,K

proof end;

theorem Th54: :: MATRIX15:54

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

proof end;

theorem :: MATRIX15:55

for n, m being Nat
for K being Field st n > 0 & not Solutions_of (0. K,n,0 ),(0. K,n,m) is empty holds
m = 0

proof end;

theorem Th56: :: MATRIX15:56

for n being Nat
for K being Field holds Solutions_of (0. K,n,0 ),(0. K,n,0 ) = {{} }

proof end;

scheme :: MATRIX15:sch 1
GAUSS1{ F₁() -> Field, F₂() -> Nat, F₃() -> Nat, F₄() -> Nat, F₅() -> Matrix of F₂(),F₃(),F₁(), F₆() -> Matrix of F₂(),F₄(),F₁(), F₇( Matrix of F₂(),F₄(),F₁(), Nat, Nat, Element of F₁()) -> Matrix of F₂(),F₄(),F₁(), P₁[ set , set ] } :

ex A' being Matrix of F₂(),F₃(),F₁() ex B' being Matrix of F₂(),F₄(),F₁() ex N being finite without_zero Subset of NAT st
( N c= Seg F₃() & the_rank_of F₅() = the_rank_of A' & the_rank_of F₅() = card N & P₁[A',B'] & Segm A',(Seg (card N)),N is diagonal & ( for i being Nat st i in Seg (card N) holds
A' * i,((Sgm N) /. i) <> 0. F₁() ) & ( for i being Nat st i in dom A' & i > card N holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A') & j < (Sgm N) . i holds
A' * i,j = 0. F₁() ) )

provided

A1: P₁[F₅(),F₆()] and
A2: for A' being Matrix of F₂(),F₃(),F₁()
for B' being Matrix of F₂(),F₄(),F₁() st P₁[A',B'] holds
for i, j being Nat st i <> j & j in dom A' holds
for a being Element of F₁() holds P₁[ RLine A',i,((Line A',i) + (a * (Line A',j))),F₇(B',i,j,a)]

proof end;

scheme :: MATRIX15:sch 2
GAUSS2{ F₁() -> Field, F₂() -> Nat, F₃() -> Nat, F₄() -> Nat, F₅() -> Matrix of F₂(),F₃(),F₁(), F₆() -> Matrix of F₂(),F₄(),F₁(), F₇( Matrix of F₂(),F₄(),F₁(), Nat, Nat, Element of F₁()) -> Matrix of F₂(),F₄(),F₁(), P₁[ set , set ] } :

ex A' being Matrix of F₂(),F₃(),F₁() ex B' being Matrix of F₂(),F₄(),F₁() ex N being finite without_zero Subset of NAT st
( N c= Seg F₃() & the_rank_of F₅() = the_rank_of A' & the_rank_of F₅() = card N & P₁[A',B'] & Segm A',(Seg (card N)),N = 1. F₁(),(card N) & ( for i being Nat st i in dom A' & i > card N holds
Line A',i = F₃() |-> (0. F₁()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A') & j < (Sgm N) . i holds
A' * i,j = 0. F₁() ) )

provided

A1: P₁[F₅(),F₆()] and
A2: for A' being Matrix of F₂(),F₃(),F₁()
for B' being Matrix of F₂(),F₄(),F₁() st P₁[A',B'] holds
for a being Element of F₁()
for i, j being Nat st j in dom A' & ( i = j implies a <> - (1_ F₁()) ) holds
P₁[ RLine A',i,((Line A',i) + (a * (Line A',j))),F₇(B',i,j,a)]

proof end;

theorem Th57: :: MATRIX15:57

for K being Field
for A, B being 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 not Solutions_of A,B is empty )

proof end;

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 & len f = width A )

proof end;

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

proof end;

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)

proof end;

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 Subset of ((width A) -VectSp_over K);
coherence
Solutions_of A,(k |-> (0. K)) is linearly-closed Subset of ((width A) -VectSp_over K)

proof end;

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 & width A = 0 holds
len A = 0

proof end;

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

proof end;

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 b₁ being strict Subspace of (width A) -VectSp_over K st the carrier of b₁ = Solutions_of A,((len A) |-> (0. K))

proof end;

uniqueness
for b₁, b₂ being strict Subspace of (width A) -VectSp_over K st the carrier of b₁ = Solutions_of A,((len A) |-> (0. K)) & the carrier of b₂ = Solutions_of A,((len A) |-> (0. K)) holds
b₁ = b₂ by VECTSP_4:37;

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 b₃ being strict Subspace of (width A) -VectSp_over K holds
( b₃ = Space_of_Solutions_of A iff the carrier of b₃ = 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

proof end;

theorem Th63: :: MATRIX15:63

for K being Field
for A being Matrix of K 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 end;

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

proof end;

theorem Th65: :: MATRIX15:65

for m, n being Nat
for K being Field
for a being Element of K
for A' being Matrix of m,n,K
for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A' = Space_of_Solutions_of (RLine A',i,((Line A',i) + (a * (Line A',j))))

proof end;

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 & not N is empty & width A > 0 & ( 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)))

proof end;

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) & gb = g * (Sgm ((dom g) \ A)) & Sum g = (Sum ga) + (Sum gb) )

proof end;

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 & N c= Seg m & Segm A,(Seg n),N = 1. K,n & n > 0 & 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) & Segm MVectors,(Seg (m -' n)),N = - ((Segm A,(Seg n),((Seg m) \ N)) @ ) & Lin (lines MVectors) = Space_of_Solutions_of A )

proof end;

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

proof end;

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)

proof end;

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 one-to-one & 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 end;

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 & 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 end;

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) & N c= Seg m & Segm A,(Seg (m -' (dim W))),N = 1. K,(m -' (dim W)) & W = Space_of_Solutions_of A )

proof end;

theorem Th72: :: MATRIX15:72

for K being Field
for A, B being 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 end;

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 & the_rank_of (A * B) <= the_rank_of B )

proof end;

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 & width A = len B & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B = Space_of_Solutions_of (A * B)

proof end;

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 & Det A <> 0. K holds
the_rank_of (A * B) = the_rank_of B

proof end;

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 & Det A <> 0. K holds
the_rank_of (B * A) = the_rank_of B

proof end;