:: by Karol P\c{a}k

::

:: Received December 18, 2007

:: Copyright (c) 2007-2018 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)

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 )

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)

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)

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

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

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)

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

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

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

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

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

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

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

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

theorem Th15: :: MATRIX15:15

for k, m, n 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))

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 k, m, n 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)

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 k, m, n 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)

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 i, k, m, n 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))

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 k, m, n 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 )

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

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)

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 )

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)

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)

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;

coherence

<*b*> is Matrix of 1, len b,D ;

coherence

<*b*> @ is Matrix of len b,1,D

end;
let b be FinSequence of D;

coherence

<*b*> is Matrix of 1, len b,D ;

coherence

<*b*> @ is Matrix of len b,1,D

proof end;

:: deftheorem defines LineVec2Mx MATRIX15:def 1 :

for D being non empty set

for b being FinSequence of D holds LineVec2Mx b = <*b*>;

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*> @ ;

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

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

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)

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)

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)

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)

for a being Element of K

for f being FinSequence of K holds a * (ColVec2Mx f) = ColVec2Mx (a * f)

proof end;

definition

let K be Field;

let A, B be Matrix of K;

{ X where X is Matrix of K : ( len X = width A & width X = width B & A * X = B ) } is set ;

end;
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 ) } ;

{ X where X is Matrix of K : ( len X = width A & width X = width B & A * X = B ) } is set ;

:: 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 ) } ;

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 :: MATRIX15:34

for i being Nat

for K being Field

for A, B, X 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)

for K being Field

for A, B, X 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 A, B, X 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)) )

for a being Element of K

for A, B, X 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))

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 A, B1, B2, X1, X2 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))

for A, B1, B2, X1, X2 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 i, k, m, n 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))))))

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

proof end;

Lm4: for i, k, m, n 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))))))

proof end;

theorem Th39: :: MATRIX15:39

for i, j, k, m, n 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) & 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)))))))

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

proof end;

Lm5: for i, j, k, m, n 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 & 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)))))))

proof end;

theorem Th40: :: MATRIX15:40

for i, j, k, m, n 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 & ( 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)))))))

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

proof end;

theorem Th41: :: MATRIX15:41

for i being Nat

for K being Field

for A, B, X 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)

for K being Field

for A, B, X 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 i, n 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))))))

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

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

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

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

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

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 k, m, n 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)) ) )

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 m, n 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))) ) )

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 l, m, n 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) )

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 m, n 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) = {{}}

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 k, n 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))

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 k, m, n 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

for k, m, n 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 k, m, n 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 }

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 m, n 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

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;

scheme :: MATRIX15:sch 1

GAUSS1{ F_{1}() -> Field, F_{2}() -> Nat, F_{3}() -> Nat, F_{4}() -> Nat, F_{5}() -> Matrix of F_{2}(),F_{3}(),F_{1}(), F_{6}() -> Matrix of F_{2}(),F_{4}(),F_{1}(), F_{7}( Matrix of F_{2}(),F_{4}(),F_{1}(), Nat, Nat, Element of F_{1}()) -> Matrix of F_{2}(),F_{4}(),F_{1}(), P_{1}[ set , set ] } :

GAUSS1{ F

ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() ex N being finite without_zero Subset of NAT st

( N c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A9 & the_rank_of F_{5}() = card N & P_{1}[A9,B9] & Segm (A9,(Seg (card N)),N) is diagonal & ( for i being Nat st i in Seg (card N) holds

A9 * (i,((Sgm N) /. i)) <> 0. F_{1}() ) & ( for i being Nat st i in dom A9 & i > card N holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds

A9 * (i,j) = 0. F_{1}() ) )

provided( N c= Seg F

A9 * (i,((Sgm N) /. i)) <> 0. F

Line (A9,i) = F

A9 * (i,j) = 0. F

A1:
P_{1}[F_{5}(),F_{6}()]
and

A2: for A9 being Matrix of F_{2}(),F_{3}(),F_{1}()

for B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st P_{1}[A9,B9] holds

for i, j being Nat st i <> j & j in dom A9 holds

for a being Element of F_{1}() holds P_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),F_{7}(B9,i,j,a)]

A2: for A9 being Matrix of F

for B9 being Matrix of F

for i, j being Nat st i <> j & j in dom A9 holds

for a being Element of F

proof end;

scheme :: MATRIX15:sch 2

GAUSS2{ F_{1}() -> Field, F_{2}() -> Nat, F_{3}() -> Nat, F_{4}() -> Nat, F_{5}() -> Matrix of F_{2}(),F_{3}(),F_{1}(), F_{6}() -> Matrix of F_{2}(),F_{4}(),F_{1}(), F_{7}( Matrix of F_{2}(),F_{4}(),F_{1}(), Nat, Nat, Element of F_{1}()) -> Matrix of F_{2}(),F_{4}(),F_{1}(), P_{1}[ set , set ] } :

GAUSS2{ F

ex A9 being Matrix of F_{2}(),F_{3}(),F_{1}() ex B9 being Matrix of F_{2}(),F_{4}(),F_{1}() ex N being finite without_zero Subset of NAT st

( N c= Seg F_{3}() & the_rank_of F_{5}() = the_rank_of A9 & the_rank_of F_{5}() = card N & P_{1}[A9,B9] & Segm (A9,(Seg (card N)),N) = 1. (F_{1}(),(card N)) & ( for i being Nat st i in dom A9 & i > card N holds

Line (A9,i) = F_{3}() |-> (0. F_{1}()) ) & ( for i, j being Nat st i in Seg (card N) & j in Seg (width A9) & j < (Sgm N) . i holds

A9 * (i,j) = 0. F_{1}() ) )

provided( N c= Seg F

Line (A9,i) = F

A9 * (i,j) = 0. F

A1:
P_{1}[F_{5}(),F_{6}()]
and

A2: for A9 being Matrix of F_{2}(),F_{3}(),F_{1}()

for B9 being Matrix of F_{2}(),F_{4}(),F_{1}() st P_{1}[A9,B9] holds

for a being Element of F_{1}()

for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ F_{1}()) ) holds

P_{1}[ RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))),F_{7}(B9,i,j,a)]

A2: for A9 being Matrix of F

for B9 being Matrix of F

for a being Element of F

for i, j being Nat st j in dom A9 & ( i = j implies a <> - (1_ F

P

proof end;

:: The Kronecker-Capelli theorem

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 )

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;

{ f where f is FinSequence of K : ColVec2Mx f in Solutions_of (A,(ColVec2Mx b)) } is set ;

end;
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)) } ;

{ f where f is FinSequence of K : ColVec2Mx f in Solutions_of (A,(ColVec2Mx b)) } is set ;

:: 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)) } ;

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 )

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

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)

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

registration

let K be Field;

let A be Matrix of K;

let k be Element of NAT ;

coherence

for b_{1} being Subset of ((width A) -VectSp_over K) st b_{1} = Solutions_of (A,(k |-> (0. K))) holds

b_{1} is linearly-closed

end;
let A be Matrix of K;

let k be Element of NAT ;

coherence

for b

b

proof 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

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

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 ) ;

ex b_{1} being strict Subspace of (width A) -VectSp_over K st the carrier of b_{1} = Solutions_of (A,((len A) |-> (0. K)))

for b_{1}, b_{2} being strict Subspace of (width A) -VectSp_over K st the carrier of b_{1} = Solutions_of (A,((len A) |-> (0. K))) & the carrier of b_{2} = Solutions_of (A,((len A) |-> (0. K))) holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
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 the carrier of it = Solutions_of (A,((len A) |-> (0. K)));

ex b

proof end;

uniqueness for b

b

:: 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_{3} being strict Subspace of (width A) -VectSp_over K holds

( b_{3} = Space_of_Solutions_of A iff the carrier of b_{3} = Solutions_of (A,((len A) |-> (0. K))) );

for K being Field

for A being Matrix of K st ( width A = 0 implies len A = 0 ) holds

for b

( b

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

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

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

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 A9 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 A9 = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))

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

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 m, n 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 )

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;

:: 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)

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 m, n 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 & 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)))))))

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

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 )

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)

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 )

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)

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

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

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;