:: Basic Properties of the Rank of Matrices over a Field
:: by Karol P\c{a}k
::
:: Received August 28, 2007
:: Copyright (c) 2007-2011 Association of Mizar Users

begin

theorem Th1: :: MATRIX13:1

for D being non empty set
for n, m being Nat
for A being Matrix of n,m,D holds
( ( n = 0 implies m = 0 ) iff ( len A = n & width A = m ) )

proof end;

theorem Th2: :: MATRIX13:2

for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is Lower_Triangular_Matrix of n,K iff M @ is Upper_Triangular_Matrix of n,K )

proof end;

theorem Th3: :: MATRIX13:3

for n being Nat
for K being Field
for M being Matrix of n,K holds diagonal_of_Matrix M = diagonal_of_Matrix (M @)

proof end;

theorem Th4: :: MATRIX13:4

for n being Nat
for perm being Element of Permutations n st perm <> idseq n holds
( ex i being Nat st
( i in Seg n & perm . i > i ) & ex j being Nat st
( j in Seg n & perm . j < j ) )

proof end;

theorem Th5: :: MATRIX13:5

for n being Nat
for K being Field
for M being Matrix of n,K
for perm being Element of Permutations n st perm <> idseq n & ( M is Lower_Triangular_Matrix of n,K or M is Upper_Triangular_Matrix of n,K ) holds
(Path_product M) . perm = 0. K

proof end;

theorem Th6: :: MATRIX13:6

for n being Nat
for K being Field
for M being Matrix of n,K
for I being Element of Permutations n st I = idseq n holds
diagonal_of_Matrix M = Path_matrix (I,M)

proof end;

theorem Th7: :: MATRIX13:7

for n being Nat
for K being Field
for M being Upper_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)

proof end;

theorem Th8: :: MATRIX13:8

for n being Nat
for K being Field
for M being Lower_Triangular_Matrix of n,K holds Det M = the multF of K $$ (diagonal_of_Matrix M)

proof end;

theorem Th9: :: MATRIX13:9

for X being finite set
for n being Nat holds card { Y where Y is Subset of X : card Y = n } = (card X) choose n

proof end;

theorem Th10: :: MATRIX13:10

for n being Nat holds card (2Set (Seg n)) = n choose 2

proof end;

theorem :: MATRIX13:11

for n being Nat
for R being Element of Permutations n st R = Rev (idseq n) holds
( R is even iff (n choose 2) mod 2 = 0 )

proof end;

theorem Th12: :: MATRIX13:12

for n being Nat
for K being Field
for M being Matrix of n,K
for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K ) holds
M * R is Upper_Triangular_Matrix of n,K

proof end;

theorem Th13: :: MATRIX13:13

for n being Nat
for K being Field
for M being Matrix of n,K
for R being Permutation of (Seg n) st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) holds
M * R is Lower_Triangular_Matrix of n,K

proof end;

theorem :: MATRIX13:14

for n being Nat
for K being Field
for M being Matrix of n,K
for R being Element of Permutations n st R = Rev (idseq n) & ( for i, j being Nat st i in Seg n & j in Seg n & i + j <= n holds
M * (i,j) = 0. K or for i, j being Nat st i in Seg n & j in Seg n & i + j > n + 1 holds
M * (i,j) = 0. K ) holds
Det M = - (( the multF of K "**" (Path_matrix (R,M))),R)

proof end;

theorem Th15: :: MATRIX13:15

for n being Nat
for K being Field
for M being Matrix of n,K
for M1, M2 being Upper_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Upper_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) )

proof end;

theorem :: MATRIX13:16

for n being Nat
for K being Field
for M being Matrix of n,K
for M1, M2 being Lower_Triangular_Matrix of n,K st M = M1 * M2 holds
( M is Lower_Triangular_Matrix of n,K & diagonal_of_Matrix M = mlt ((diagonal_of_Matrix M1),(diagonal_of_Matrix M2)) )

proof end;

begin

definition

let D be non empty set ;
let M be Matrix of D;
let n, m be Nat;
let nt be Element of n -tuples_on NAT;
let mt be Element of m -tuples_on NAT;
func Segm (M,nt,mt) -> Matrix of n,m,D means :Def1: :: MATRIX13:def 1
for i, j being Nat st [i,j] in Indices it holds
it * (i,j) = M * ((nt . i),(mt . j));
existence
ex b₁ being Matrix of n,m,D st
for i, j being Nat st [i,j] in Indices b₁ holds
b₁ * (i,j) = M * ((nt . i),(mt . j))

proof end;

uniqueness
for b₁, b₂ being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices b₁ holds
b₁ * (i,j) = M * ((nt . i),(mt . j)) ) & ( for i, j being Nat st [i,j] in Indices b₂ holds
b₂ * (i,j) = M * ((nt . i),(mt . j)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Segm MATRIX13:def 1 :
for D being non empty set
for M being Matrix of D
for n, m being Nat
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for b₇ being Matrix of n,m,D holds
( b₇ = Segm (M,nt,mt) iff for i, j being Nat st [i,j] in Indices b₇ holds
b₇ * (i,j) = M * ((nt . i),(mt . j)) );

theorem Th17: :: MATRIX13:17

for D being non empty set
for n, m, i, j being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
( [i,j] in Indices (Segm (A,nt,mt)) iff [(nt . i),(mt . j)] in Indices A )

proof end;

theorem Th18: :: MATRIX13:18

for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT holds
not ( [:(rng nt),(rng mt):] c= Indices A & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & not (Segm (A,nt,mt)) @ = Segm ((A @),mt,nt) )

proof end;

theorem Th19: :: MATRIX13:19

for D being non empty set
for m, n being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A & ( m = 0 implies n = 0 ) holds
Segm (A,nt,mt) = (Segm ((A @),mt,nt)) @

proof end;

theorem Th20: :: MATRIX13:20

for D being non empty set
for A being Matrix of 1,D holds A = <*<*(A * (1,1))*>*>

proof end;

theorem Th21: :: MATRIX13:21

for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st n = 1 & m = 1 holds
Segm (A,nt,mt) = <*<*(A * ((nt . 1),(mt . 1)))*>*>

proof end;

theorem Th22: :: MATRIX13:22

for D being non empty set
for A being Matrix of 2,D holds A = ((A * (1,1)),(A * (1,2))) ][ ((A * (2,1)),(A * (2,2)))

proof end;

theorem Th23: :: MATRIX13:23

for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st n = 2 & m = 2 holds
Segm (A,nt,mt) = ((A * ((nt . 1),(mt . 1))),(A * ((nt . 1),(mt . 2)))) ][ ((A * ((nt . 2),(mt . 1))),(A * ((nt . 2),(mt . 2))))

proof end;

theorem Th24: :: MATRIX13:24

for D being non empty set
for m, i, n being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n & rng mt c= Seg (width A) holds
Line ((Segm (A,nt,mt)),i) = (Line (A,(nt . i))) * mt

proof end;

theorem Th25: :: MATRIX13:25

for D being non empty set
for m, i, n, j being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg n & j in Seg n & nt . i = nt . j holds
Line ((Segm (A,nt,mt)),i) = Line ((Segm (A,nt,mt)),j)

proof end;

theorem Th26: :: MATRIX13:26

for i, n, j being Nat
for K being Field
for nt, nt1 being Element of n -tuples_on NAT
for M being Matrix of K st i in Seg n & j in Seg n & nt . i = nt . j & i <> j holds
Det (Segm (M,nt,nt1)) = 0. K

proof end;

theorem Th27: :: MATRIX13:27

for n being Nat
for K being Field
for nt, nt1 being Element of n -tuples_on NAT
for M being Matrix of K st not nt is without_repeated_line holds
Det (Segm (M,nt,nt1)) = 0. K

proof end;

theorem Th28: :: MATRIX13:28

for D being non empty set
for n, j, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st j in Seg m & rng nt c= Seg (len A) holds
Col ((Segm (A,nt,mt)),j) = (Col (A,(mt . j))) * nt

proof end;

theorem Th29: :: MATRIX13:29

for D being non empty set
for n, i, m, j being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in Seg m & j in Seg m & mt . i = mt . j holds
Col ((Segm (A,nt,mt)),i) = Col ((Segm (A,nt,mt)),j)

proof end;

theorem Th30: :: MATRIX13:30

for i, m, j being Nat
for K being Field
for mt, mt1 being Element of m -tuples_on NAT
for M being Matrix of K st i in Seg m & j in Seg m & mt . i = mt . j & i <> j holds
Det (Segm (M,mt1,mt)) = 0. K

proof end;

theorem Th31: :: MATRIX13:31

for m being Nat
for K being Field
for mt, mt1 being Element of m -tuples_on NAT
for M being Matrix of K st not mt is without_repeated_line holds
Det (Segm (M,mt1,mt)) = 0. K

proof end;

theorem Th32: :: MATRIX13:32

for n being Nat
for nt, nt1 being Element of n -tuples_on NAT st nt is without_repeated_line & nt1 is without_repeated_line & rng nt = rng nt1 holds
ex perm being Permutation of (Seg n) st nt1 = nt * perm

proof end;

theorem Th33: :: MATRIX13:33

for D being non empty set
for m, n being Nat
for A being Matrix of D
for nt1, nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for f being Function of (Seg n),(Seg n) st nt1 = nt * f holds
Segm (A,nt1,mt) = (Segm (A,nt,mt)) * f

proof end;

theorem Th34: :: MATRIX13:34

for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt1, mt being Element of m -tuples_on NAT
for f being Function of (Seg m),(Seg m) st mt1 = mt * f holds
(Segm (A,nt,mt1)) @ = ((Segm (A,nt,mt)) @) * f

proof end;

theorem Th35: :: MATRIX13:35

for n being Nat
for K being Field
for nt1, nt2, nt being Element of n -tuples_on NAT
for M being Matrix of K
for perm being Element of Permutations n st nt1 = nt2 * perm holds
( Det (Segm (M,nt1,nt)) = - ((Det (Segm (M,nt2,nt))),perm) & Det (Segm (M,nt,nt1)) = - ((Det (Segm (M,nt,nt2))),perm) )

proof end;

Lm1: for n being Nat
for nt, nt1 being Element of n -tuples_on NAT st rng nt = rng nt1 & nt is without_repeated_line holds
nt1 is without_repeated_line

proof end;

theorem Th36: :: MATRIX13:36

for n being Nat
for K being Field
for M being Matrix of K
for nt, nt1, nt9, nt19 being Element of n -tuples_on NAT st rng nt = rng nt9 & rng nt1 = rng nt19 & not Det (Segm (M,nt,nt1)) = Det (Segm (M,nt9,nt19)) holds
Det (Segm (M,nt,nt1)) = - (Det (Segm (M,nt9,nt19)))

proof end;

theorem Th37: :: MATRIX13:37

for D being non empty set
for n9, m9, n, m being Nat
for A9 being Matrix of n9,m9,D
for F, Fmt being FinSequence of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)

proof end;

theorem Th38: :: MATRIX13:38

for D being non empty set
for n9, m9, m, n being Nat
for A9 being Matrix of n9,m9,D
for mt being Element of m -tuples_on NAT
for F being FinSequence of D
for i being Nat
for nt being Element of n -tuples_on NAT st not i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
Segm (A9,nt,mt) = Segm ((RLine (A9,i,F)),nt,mt)

proof end;

theorem Th39: :: MATRIX13:39

for D being non empty set
for n9, m9, m, i, n, j being Nat
for A9 being Matrix of n9,m9,D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st i in rng nt & [:(rng nt),(rng mt):] c= Indices A9 holds
ex nt1 being Element of n -tuples_on NAT st
( rng nt1 = ((rng nt) \ {i}) \/ {j} & Segm ((RLine (A9,i,(Line (A9,j)))),nt,mt) = Segm (A9,nt1,mt) )

proof end;

theorem Th40: :: MATRIX13:40

for D being non empty set
for n9, m9, i being Nat
for A9 being Matrix of n9,m9,D
for F being FinSequence of D st not i in Seg (len A9) holds
RLine (A9,i,F) = A9

proof end;

definition

let n, m be Nat;
let K be Field;
let M be Matrix of n,m,K;
let a be Element of K;
:: original: *
redefine func a * M -> Matrix of n,m,K;
coherence
a * M is Matrix of n,m,K

proof end;

end;

theorem Th41: :: MATRIX13:41

for n, m being Nat
for K being Field
for a being Element of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
a * (Segm (M,nt,mt)) = Segm ((a * M),nt,mt)

proof end;

theorem Th42: :: MATRIX13:42

for D being non empty set
for n, m being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st nt = idseq (len A) & mt = idseq (width A) holds
Segm (A,nt,mt) = A

proof end;

registration

cluster empty finite without_zero Element of bool NAT;
existence
ex b₁ being Subset of NAT st
( b₁ is empty & b₁ is without_zero & b₁ is finite )

proof end;

cluster non empty finite without_zero Element of bool NAT;
existence
ex b₁ being Subset of NAT st
( not b₁ is empty & b₁ is without_zero & b₁ is finite )

proof end;

end;

registration

let n be Nat;
cluster Seg n -> without_zero ;
coherence
Seg n is without_zero

proof end;

end;

registration

let X be without_zero set ;
let Y be set ;
cluster X \ Y -> without_zero ;
coherence
X \ Y is without_zero

proof end;

end;

definition

let i be Nat;
:: original: {
redefine func {i} -> Subset of NAT;
coherence
{i} is Subset of NAT

proof end;

let j be Nat;
:: original: {
redefine func {i,j} -> Subset of NAT;
coherence
{i,j} is Subset of NAT

proof end;

end;

theorem Th43: :: MATRIX13:43

for N being finite without_zero Subset of NAT ex k being Nat st N c= Seg k

proof end;

definition

let N be finite without_zero Subset of NAT;
:: original: Sgm
redefine func Sgm N -> Element of (card N) -tuples_on NAT;
coherence
Sgm N is Element of (card N) -tuples_on NAT

proof end;

end;

definition

let D be non empty set ;
let A be Matrix of D;
let P, Q be finite without_zero Subset of NAT;
func Segm (A,P,Q) -> Matrix of card P, card Q,D equals :: MATRIX13:def 2
Segm (A,(Sgm P),(Sgm Q));
coherence
Segm (A,(Sgm P),(Sgm Q)) is Matrix of card P, card Q,D ;

end;

:: deftheorem defines Segm MATRIX13:def 2 :
for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT holds Segm (A,P,Q) = Segm (A,(Sgm P),(Sgm Q));

theorem Th44: :: MATRIX13:44

for D being non empty set
for i0, j0 being non zero Nat
for A being Matrix of D holds Segm (A,{i0},{j0}) = <*<*(A * (i0,j0))*>*>

proof end;

theorem Th45: :: MATRIX13:45

for D being non empty set
for i0, j0, n0, m0 being non zero Nat
for A being Matrix of D st i0 < j0 & n0 < m0 holds
Segm (A,{i0,j0},{n0,m0}) = ((A * (i0,n0)),(A * (i0,m0))) ][ ((A * (j0,n0)),(A * (j0,m0)))

proof end;

theorem Th46: :: MATRIX13:46

for D being non empty set
for A being Matrix of D holds Segm (A,(Seg (len A)),(Seg (width A))) = A

proof end;

theorem Th47: :: MATRIX13:47

for D being non empty set
for i being Nat
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st i in Seg (card P) & Q c= Seg (width A) holds
Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)

proof end;

theorem Th48: :: MATRIX13:48

for D being non empty set
for i being Nat
for A being Matrix of D
for P being finite without_zero Subset of NAT st i in Seg (card P) holds
Line ((Segm (A,P,(Seg (width A)))),i) = Line (A,((Sgm P) . i))

proof end;

theorem Th49: :: MATRIX13:49

for D being non empty set
for j being Nat
for A being Matrix of D
for Q, P being finite without_zero Subset of NAT st j in Seg (card Q) & P c= Seg (len A) holds
Col ((Segm (A,P,Q)),j) = (Col (A,((Sgm Q) . j))) * (Sgm P)

proof end;

theorem Th50: :: MATRIX13:50

for D being non empty set
for j being Nat
for A being Matrix of D
for Q being finite without_zero Subset of NAT st j in Seg (card Q) holds
Col ((Segm (A,(Seg (len A)),Q)),j) = Col (A,((Sgm Q) . j))

proof end;

theorem Th51: :: MATRIX13:51

for D being non empty set
for i being Nat
for A being Matrix of D holds Segm (A,((Seg (len A)) \ {i}),(Seg (width A))) = Del (A,i)

proof end;

theorem Th52: :: MATRIX13:52

for i being Nat
for K being Field
for M being Matrix of K holds Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) = DelCol (M,i)

proof end;

theorem Th53: :: MATRIX13:53

for X being set
for P being finite without_zero Subset of NAT holds (Sgm P) " X is finite without_zero Subset of NAT

proof end;

theorem Th54: :: MATRIX13:54

for X being set
for P being finite without_zero Subset of NAT st X c= P holds
Sgm X = (Sgm P) * (Sgm ((Sgm P) " X))

proof end;

Lm2: for X being set
for P being finite without_zero Subset of NAT st X c= P holds
card X = card ((Sgm P) " X)

proof end;

theorem Th55: :: MATRIX13:55

for X, Y being set
for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT holds [:((Sgm P) " X),((Sgm Q) " Y):] c= Indices (Segm (A,P,Q))

proof end;

theorem Th56: :: MATRIX13:56

for D being non empty set
for A being Matrix of D
for P, P1, Q, Q1, P2, Q2 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 & P2 = (Sgm P1) " P & Q2 = (Sgm Q1) " Q holds
( [:(rng (Sgm P2)),(rng (Sgm Q2)):] c= Indices (Segm (A,P1,Q1)) & Segm ((Segm (A,P1,Q1)),P2,Q2) = Segm (A,P,Q) )

proof end;

theorem Th57: :: MATRIX13:57

for D being non empty set
for A being Matrix of D
for P, Q, P1, Q1 being finite without_zero Subset of NAT holds
not ( ( P = {} implies Q = {} ) & ( Q = {} implies P = {} ) & [:P,Q:] c= Indices (Segm (A,P1,Q1)) & ( for P2, Q2 being finite without_zero Subset of NAT holds
( not P2 c= P1 or not Q2 c= Q1 or not P2 = (Sgm P1) .: P or not Q2 = (Sgm Q1) .: Q or not card P2 = card P or not card Q2 = card Q or not Segm ((Segm (A,P1,Q1)),P,Q) = Segm (A,P2,Q2) ) ) )

proof end;

theorem Th58: :: MATRIX13:58

for n, i, j being Nat
for K being Field
for M being Matrix of n,K holds Segm (M,((Seg n) \ {i}),((Seg n) \ {j})) = Deleting (M,i,j)

proof end;

theorem Th59: :: MATRIX13:59

for D being non empty set
for n9, m9, i being Nat
for A9 being Matrix of n9,m9,D
for Q, P being finite without_zero Subset of NAT
for F, FQ being FinSequence of D st len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 holds
RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)

proof end;

theorem Th60: :: MATRIX13:60

for D being non empty set
for n9, m9 being Nat
for A9 being Matrix of n9,m9,D
for Q being finite without_zero Subset of NAT
for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of NAT st not i in P & [:P,Q:] c= Indices A9 holds
Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)

proof end;

theorem :: MATRIX13:61

for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT holds
not ( [:P,Q:] c= Indices A & ( card P = 0 implies card Q = 0 ) & ( card Q = 0 implies card P = 0 ) & not (Segm (A,P,Q)) @ = Segm ((A @),Q,P) )

proof end;

theorem Th62: :: MATRIX13:62

for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices A & ( card Q = 0 implies card P = 0 ) holds
Segm (A,P,Q) = (Segm ((A @),Q,P)) @

proof end;

theorem Th63: :: MATRIX13:63

for K being Field
for a being Element of K
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds
a * (Segm (M,P,Q)) = Segm ((a * M),P,Q)

proof end;

definition

let D be non empty set ;
let A be Matrix of D;
let P, Q be finite without_zero Subset of NAT;
assume A1: card P = card Q ;
func EqSegm (A,P,Q) -> Matrix of card P,D equals :Def3: :: MATRIX13:def 3
Segm (A,P,Q);
coherence
Segm (A,P,Q) is Matrix of card P,D by A1;

end;

:: deftheorem Def3 defines EqSegm MATRIX13:def 3 :
for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st card P = card Q holds
EqSegm (A,P,Q) = Segm (A,P,Q);

theorem Th64: :: MATRIX13:64

for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i, j being Nat st i in Seg (card P) & j in Seg (card P) & card P = card Q holds
( Delete ((EqSegm (M,P,Q)),i,j) = EqSegm (M,(P \ {((Sgm P) . i)}),(Q \ {((Sgm Q) . j)})) & card (P \ {((Sgm P) . i)}) = card (Q \ {((Sgm Q) . j)}) )

proof end;

Lm3: for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i being Nat st i in Seg (card P) & Det (EqSegm (M,P,Q)) <> 0. K holds
ex j being Nat st
( j in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )

proof end;

theorem Th65: :: MATRIX13:65

for K being Field
for M being Matrix of K
for P, P1, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & P c= P1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )

proof end;

Lm4: for j being Nat
for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i being Nat st j in Seg (card P) & Det (EqSegm (M,P,Q)) <> 0. K holds
ex i being Nat st
( i in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )

proof end;

theorem :: MATRIX13:66

for K being Field
for M being Matrix of K
for P1, Q, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & Q c= Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
ex P being finite without_zero Subset of NAT st
( P c= P1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )

proof end;

theorem Th67: :: MATRIX13:67

for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st card P = card Q holds
( [:P,Q:] c= Indices A iff ( P c= Seg (len A) & Q c= Seg (width A) ) )

proof end;

theorem Th68: :: MATRIX13:68

for m9, n9 being Nat
for K being Field
for M9 being Matrix of n9,m9,K
for P, Q being finite without_zero Subset of NAT
for i being Nat
for j0 being non zero Nat st j0 in Seg n9 & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M9 holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M9 & ( Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q)) or Det (EqSegm ((RLine (M9,i,(Line (M9,j0)))),P,Q)) = - (Det (EqSegm (M9,((P \ {i}) \/ {j0}),Q))) ) )

proof end;

theorem Th69: :: MATRIX13:69

for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st card P = card Q holds
( [:P,Q:] c= Indices A iff [:Q,P:] c= Indices (A @) )

proof end;

theorem Th70: :: MATRIX13:70

for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
Det (EqSegm (M,P,Q)) = Det (EqSegm ((M @),Q,P))

proof end;

theorem Th71: :: MATRIX13:71

for n being Nat
for K being Field
for a being Element of K
for M being Matrix of n,K holds Det (a * M) = ((power K) . (a,n)) * (Det M)

proof end;

theorem Th72: :: MATRIX13:72

for K being Field
for a being Element of K
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q)))

proof end;

definition

let K be Field;
let M be Matrix of K;
func the_rank_of M -> Element of NAT means :Def4: :: MATRIX13:def 4
( ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = it & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= it ) );
existence
ex b₁ being Element of NAT st
( ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = b₁ & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= b₁ ) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = b₁ & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= b₁ ) & ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = b₂ & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= b₂ ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines the_rank_of MATRIX13:def 4 :
for K being Field
for M being Matrix of K
for b₃ being Element of NAT holds
( b₃ = the_rank_of M iff ( ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = b₃ & Det (EqSegm (M,P,Q)) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
card P1 <= b₃ ) ) );

theorem Th73: :: MATRIX13:73

for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q holds
( card P <= len M & card Q <= width M )

proof end;

theorem Th74: :: MATRIX13:74

for K being Field
for M being Matrix of K holds
( the_rank_of M <= len M & the_rank_of M <= width M )

proof end;

Lm5: for n, m being Nat
for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K holds
not ( [:(rng nt),(rng mt):] c= Indices M & ( n = 0 implies m = 0 ) & ( m = 0 implies n = 0 ) & ( for P1, P2 being finite without_zero Subset of NAT holds
( not P1 = rng nt or not P2 = rng mt ) ) )

proof end;

theorem Th75: :: MATRIX13:75

for n being Nat
for K being Field
for nt1, nt2 being Element of n -tuples_on NAT
for M being Matrix of K st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds
ex P1, P2 being finite without_zero Subset of NAT st
( P1 = rng nt1 & P2 = rng nt2 & card P1 = card P2 & card P1 = n & Det (EqSegm (M,P1,P2)) <> 0. K )

proof end;

theorem Th76: :: MATRIX13:76

for K being Field
for M being Matrix of K
for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex rt1, rt2 being Element of RANK -tuples_on NAT st
( [:(rng rt1),(rng rt2):] c= Indices M & Det (Segm (M,rt1,rt2)) <> 0. K ) & ( for n being Nat
for nt1, nt2 being Element of n -tuples_on NAT st [:(rng nt1),(rng nt2):] c= Indices M & Det (Segm (M,nt1,nt2)) <> 0. K holds
n <= RANK ) ) )

proof end;

theorem Th77: :: MATRIX13:77

for n, m being Nat
for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st ( n = 0 or m = 0 ) holds
the_rank_of (Segm (M,nt,mt)) = 0

proof end;

theorem Th78: :: MATRIX13:78

for n, m being Nat
for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] c= Indices M holds
the_rank_of M >= the_rank_of (Segm (M,nt,mt))

proof end;

theorem Th79: :: MATRIX13:79

for K being Field
for M being Matrix of K
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M holds
the_rank_of M >= the_rank_of (Segm (M,P,Q))

proof end;

theorem Th80: :: MATRIX13:80

for K being Field
for M being Matrix of K
for P, P1, Q, Q1 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 holds
the_rank_of (Segm (M,P,Q)) <= the_rank_of (Segm (M,P1,Q1))

proof end;

theorem Th81: :: MATRIX13:81

for f, g being Function st rng f c= rng g holds
ex h being Function st
( dom h = dom f & rng h c= dom g & f = g * h )

proof end;

theorem Th82: :: MATRIX13:82

for n, m being Nat
for K being Field
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT
for M being Matrix of K st [:(rng nt),(rng mt):] = Indices M holds
the_rank_of M = the_rank_of (Segm (M,nt,mt))

proof end;

theorem Th83: :: MATRIX13:83

for n being Nat
for K being Field
for M being Matrix of n,K holds
( the_rank_of M = n iff Det M <> 0. K )

proof end;

theorem :: MATRIX13:84

for K being Field
for M being Matrix of K holds the_rank_of M = the_rank_of (M @)

proof end;

Lm6: 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 :: MATRIX13:85

for n, m being Nat
for K being Field
for M being Matrix of n,m,K
for F being Permutation of (Seg n) holds the_rank_of M = the_rank_of (M * F)

proof end;

theorem :: MATRIX13:86

for K being Field
for a being Element of K
for M being Matrix of K st a <> 0. K holds
the_rank_of M = the_rank_of (a * M)

proof end;

theorem Th87: :: MATRIX13:87

for K being Field
for a being Element of K
for p, pf being FinSequence of K
for f being Function st pf = p * f & rng f c= dom p holds
(a * p) * f = a * pf

proof end;

theorem Th88: :: MATRIX13:88

for K being Field
for p, pf, q, qf being FinSequence of K
for f being Function st pf = p * f & rng f c= dom p & qf = q * f & rng f c= dom q holds
(p + q) * f = pf + qf

proof end;

theorem Th89: :: MATRIX13:89

for n9, m9, i being Nat
for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st a <> 0. K holds
the_rank_of M9 = the_rank_of (RLine (M9,i,(a * (Line (M9,i)))))

proof end;

theorem Th90: :: MATRIX13:90

for i being Nat
for K being Field
for M being Matrix of K st Line (M,i) = (width M) |-> (0. K) holds
the_rank_of (DelLine (M,i)) = the_rank_of M

proof end;

theorem Th91: :: MATRIX13:91

for n9, m9, i being Nat
for K being Field
for M9 being Matrix of n9,m9,K
for p being FinSequence of K st len p = width M9 holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))

proof end;

theorem Th92: :: MATRIX13:92

for n9, m9, j, i being Nat
for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) & ( i = j implies a <> - (1_ K) ) holds
the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))

proof end;

theorem Th93: :: MATRIX13:93

for n9, m9, j, i being Nat
for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) & j <> i holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))

proof end;

theorem Th94: :: MATRIX13:94

for K being Field
for M being Matrix of K holds
( the_rank_of M > 0 iff ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) )

proof end;

theorem :: MATRIX13:95

for K being Field
for M being Matrix of K holds
( the_rank_of M = 0 iff M = 0. (K,(len M),(width M)) )

proof end;

theorem Th96: :: MATRIX13:96

for K being Field
for M being Matrix of K holds
( the_rank_of M = 1 iff ( ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i0, j0, n0, m0 being non zero Nat st i0 <> j0 & n0 <> m0 & [:{i0,j0},{n0,m0}:] c= Indices M holds
Det (EqSegm (M,{i0,j0},{n0,m0})) = 0. K ) ) )

proof end;

theorem Th97: :: MATRIX13:97

for K being Field
for M being Matrix of K holds
( the_rank_of M = 1 iff ( ex i, j being Nat st
( [i,j] in Indices M & M * (i,j) <> 0. K ) & ( for i, j, n, m being Nat st [:{i,j},{n,m}:] c= Indices M holds
(M * (i,n)) * (M * (j,m)) = (M * (i,m)) * (M * (j,n)) ) ) )

proof end;

theorem :: MATRIX13:98

for K being Field
for M being Matrix of K holds
( the_rank_of M = 1 iff ex i being Nat st
( i in Seg (len M) & ex j being Nat st
( j in Seg (width M) & M * (i,j) <> 0. K ) & ( for k being Nat st k in Seg (len M) holds
ex a being Element of K st Line (M,k) = a * (Line (M,i)) ) ) )

proof end;

registration

let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding tabular diagonal V221() FinSequence of the carrier of K * ;
existence
ex b₁ being Matrix of K st b₁ is diagonal

proof end;

end;

theorem Th99: :: MATRIX13:99

for K being Field
for M being diagonal Matrix of K
for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds
for P, Q being finite without_zero Subset of NAT st [:P,Q:] c= Indices M & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K holds
( P c= NonZero1 & Q c= NonZero1 )

proof end;

theorem Th100: :: MATRIX13:100

for K being Field
for M being diagonal Matrix of K
for P being finite without_zero Subset of NAT st [:P,P:] c= Indices M holds
Segm (M,P,P) is diagonal

proof end;

theorem :: MATRIX13:101

for K being Field
for M being diagonal Matrix of K
for NonZero1 being set st NonZero1 = { i where i is Element of NAT : ( [i,i] in Indices M & M * (i,i) <> 0. K ) } holds
the_rank_of M = card NonZero1

proof end;

theorem Th102: :: MATRIX13:102

for n being Nat
for K being Field
for a being Element of K
for v1, v2, v being Vector of (n -VectSp_over K)
for t1, t2, t being Element of n -tuples_on the carrier of K holds
( the carrier of (n -VectSp_over K) = n -tuples_on the carrier of K & 0. (n -VectSp_over K) = n |-> (0. K) & ( t1 = v1 & t2 = v2 implies t1 + t2 = v1 + v2 ) & ( t = v implies a * t = a * v ) )

proof end;

registration

let K be Field;
let n be Nat;
cluster n -VectSp_over K -> right_complementable Abelian add-associative right_zeroed ;
coherence
( n -VectSp_over K is right_complementable & n -VectSp_over K is Abelian & n -VectSp_over K is add-associative & n -VectSp_over K is right_zeroed )

proof end;

end;

registration

let K be Field;
let n be Nat;
cluster -> Relation-like Function-like Element of the carrier of (n -VectSp_over K);
correctness
coherence
for b₁ being Vector of (n -VectSp_over K) holds
( b₁ is Function-like & b₁ is Relation-like );

proof end;

end;

Lm7: for m, n being Nat
for K being Field
for M being Matrix of m,n,K holds rng M is Subset of (n -VectSp_over K)

proof end;

notation

let K be Field;
let m, n be Nat;
let M be Matrix of m,n,K;
synonym lines M for rng K;
synonym without_repeated_line M for one-to-one ;

end;

definition

let K be Field;
let m, n be Nat;
let M be Matrix of m,n,K;
:: original: lines
redefine func lines M -> Subset of (n -VectSp_over K);
coherence
lines is Subset of (n -VectSp_over K) by Lm7;

end;

theorem Th103: :: MATRIX13:103

for x being set
for n, m being Nat
for K being Field
for M being Matrix of m,n,K holds
( x in lines M iff ex i being Nat st
( i in Seg m & x = Line (M,i) ) )

proof end;

theorem :: MATRIX13:104

for n being Nat
for K being Field
for V being finite Subset of (n -VectSp_over K) ex M being Matrix of card V,n,K st
( M is without_repeated_line & lines M = V )

proof end;

definition

let K be Field;
let n be Nat;
let F be FinSequence of (n -VectSp_over K);
func FinS2MX F -> Matrix of len F,n,K equals :: MATRIX13:def 5
F;
coherence
F is Matrix of len F,n,K

proof end;

end;

:: deftheorem defines FinS2MX MATRIX13:def 5 :
for K being Field
for n being Nat
for F being FinSequence of (n -VectSp_over K) holds FinS2MX F = F;

definition

let K be Field;
let m, n be Nat;
let M be Matrix of m,n,K;
func MX2FinS M -> FinSequence of (n -VectSp_over K) equals :: MATRIX13:def 6
M;
coherence
M is FinSequence of (n -VectSp_over K)

proof end;

end;

:: deftheorem defines MX2FinS MATRIX13:def 6 :
for K being Field
for m, n being Nat
for M being Matrix of m,n,K holds MX2FinS M = M;

theorem Th105: :: MATRIX13:105

for n, m being Nat
for K being Field
for M being Matrix of m,n,K st the_rank_of M = m holds
M is without_repeated_line

proof end;

theorem Th106: :: MATRIX13:106

for m, n, i being Nat
for K being Field
for a being Element of K
for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st i in Seg (len M) & a = L . (M . i) holds
Line ((FinS2MX (L (#) (MX2FinS M))),i) = a * (Line (M,i))

proof end;

theorem Th107: :: MATRIX13:107

for m, i, n being Nat
for K being Field
for L being Linear_Combination of n -VectSp_over K
for M being Matrix of m,n,K st M is without_repeated_line & Carrier L c= lines M & i in Seg n holds
(Sum L) . i = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),i))

proof end;

theorem Th108: :: MATRIX13:108

for n, m being Nat
for K being Field
for M, M1 being Matrix of m,n,K st M is without_repeated_line & ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) holds
ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1

proof end;

theorem Th109: :: MATRIX13:109

for n, m being Nat
for K being Field
for M being Matrix of m,n,K st M is without_repeated_line holds
( ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) ) iff lines M is linearly-independent )

proof end;

theorem Th110: :: MATRIX13:110

for n, m being Nat
for K being Field
for M being Matrix of m,n,K st the_rank_of M = m holds
lines M is linearly-independent

proof end;

theorem Th111: :: MATRIX13:111

for n being Nat
for K being Field
for M being Diagonal of n,K st the_rank_of M = n holds
lines M is Basis of n -VectSp_over K

proof end;

Lm8: for n being Nat
for K being Field holds
( lines (1. (K,n)) is Basis of n -VectSp_over K & the_rank_of (1. (K,n)) = n )

proof end;

registration

let K be Field;
let n be Nat;
cluster n -VectSp_over K -> finite-dimensional ;
coherence
n -VectSp_over K is finite-dimensional

proof end;

end;

theorem :: MATRIX13:112

for n being Nat
for K being Field holds dim (n -VectSp_over K) = n

proof end;

theorem Th113: :: MATRIX13:113

for n, m being Nat
for K being Field
for M being Matrix of m,n,K
for i being Nat
for a being Element of K st ( for j being Nat st j in Seg m holds
M * (j,i) = a ) holds
( M is without_repeated_line iff Segm (M,(Seg (len M)),((Seg (width M)) \ {i})) is without_repeated_line )

proof end;

theorem Th114: :: MATRIX13:114

for n, m being Nat
for K being Field
for M being Matrix of m,n,K
for i being Nat st M is without_repeated_line & lines M is linearly-independent & ( for j being Nat st j in Seg m holds
M * (j,i) = 0. K ) holds
lines (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) is linearly-independent

proof end;

theorem Th115: :: MATRIX13:115

for K being Field
for a being Element of K
for V being VectSp of K
for U being finite Subset of V st U is linearly-independent holds
for u, v being Vector of V st u in U & v in U & u <> v holds
(U \ {u}) \/ {(u + (a * v))} is linearly-independent

proof end;

theorem Th116: :: MATRIX13:116

for x being set
for K being Field
for V being VectSp of K
for u, v being Vector of V holds
( x in Lin {u,v} iff ex a, b being Element of K st x = (a * u) + (b * v) )

proof end;

theorem Th117: :: MATRIX13:117

for n, m being Nat
for K being Field
for a being Element of K
for M being Matrix of m,n,K st lines M is linearly-independent & M is without_repeated_line holds
for i, j being Nat st j in Seg (len M) & i <> j holds
( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )

proof end;

theorem Th118: :: MATRIX13:118

for m, n being Nat
for K being Field
for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m holds
lines (Segm (M,P,(Seg n))) c= lines M

proof end;

theorem Th119: :: MATRIX13:119

for m, n being Nat
for K being Field
for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m & lines M is linearly-independent holds
lines (Segm (M,P,(Seg n))) is linearly-independent

proof end;

theorem Th120: :: MATRIX13:120

for m, n being Nat
for K being Field
for P being finite without_zero Subset of NAT
for M being Matrix of m,n,K st P c= Seg m & M is without_repeated_line holds
Segm (M,P,(Seg n)) is without_repeated_line

proof end;

theorem Th121: :: MATRIX13:121

for m, n being Nat
for K being Field
for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )

proof end;

theorem Th122: :: MATRIX13:122

for n, m being Nat
for K being Field
for M being Matrix of m,n,K
for U being Subset of (n -VectSp_over K) st U c= lines M holds
ex P being finite without_zero Subset of NAT st
( P c= Seg m & lines (Segm (M,P,(Seg n))) = U & Segm (M,P,(Seg n)) is without_repeated_line )

proof end;

theorem :: MATRIX13:123

for m, n being Nat
for K being Field
for M being Matrix of m,n,K
for RANK being Element of NAT holds
( the_rank_of M = RANK iff ( ex U being finite Subset of (n -VectSp_over K) st
( U is linearly-independent & U c= lines M & card U = RANK ) & ( for W being finite Subset of (n -VectSp_over K) st W is linearly-independent & W c= lines M holds
card W <= RANK ) ) )

proof end;