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

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;

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, nt', nt1' being Element of n -tuples_on NAT st rng nt = rng nt' & rng nt1 = rng nt1' & not Det (Segm M,nt,nt1) = Det (Segm M,nt',nt1') holds
Det (Segm M,nt,nt1) = - (Det (Segm M,nt',nt1'))

proof end;

theorem Th37: :: MATRIX13:37

for D being non empty set
for n', m', n, m being Nat
for A' being Matrix of n',m',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 A' & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A' holds
for i, j being Nat st nt " {j} = {i} holds
RLine (Segm A',nt,mt),i,Fmt = Segm (RLine A',j,F),nt,mt

proof end;

theorem Th38: :: MATRIX13:38

for D being non empty set
for n', m', m, n being Nat
for A' being Matrix of n',m',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 A' holds
Segm A',nt,mt = Segm (RLine A',i,F),nt,mt

proof end;

theorem Th39: :: MATRIX13:39

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

proof end;

theorem Th40: :: MATRIX13:40

for D being non empty set
for n', m', i being Nat
for A' being Matrix of n',m',D
for F being FinSequence of D st not i in Seg (len A') holds
RLine A',i,F = A'

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 finSeg 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 n', m', i being Nat
for A' being Matrix of n',m',D
for Q, P being finite without_zero Subset of NAT
for F, FQ being FinSequence of D st len F = width A' & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A' holds
RLine (Segm A',P,Q),i,FQ = Segm (RLine A',((Sgm P) . i),F),P,Q

proof end;

theorem Th60: :: MATRIX13:60

for D being non empty set
for n', m' being Nat
for A' being Matrix of n',m',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 A' holds
Segm A',P,Q = Segm (RLine A',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) & card P = card Q & 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) & card P = card Q & 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 m', n' being Nat
for K being Field
for M' being Matrix of n',m',K
for P, Q being finite without_zero Subset of NAT
for i being Nat
for j0 being non zero Nat st i in Seg n' & j0 in Seg n' & i in P & not j0 in P & card P = card Q & [:P,Q:] c= Indices M' holds
( card P = card ((P \ {i}) \/ {j0}) & [:((P \ {i}) \/ {j0}),Q:] c= Indices M' & ( Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = Det (EqSegm M',((P \ {i}) \/ {j0}),Q) or Det (EqSegm (RLine M',i,(Line M',j0)),P,Q) = - (Det (EqSegm M',((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 n', m', i being Nat
for K being Field
for a being Element of K
for M' being Matrix of n',m',K st a <> 0. K holds
the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',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 n', m', i being Nat
for K being Field
for M' being Matrix of n',m',K
for p being FinSequence of K st len p = width M' holds
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,((0. K) * p))

proof end;

theorem Th92: :: MATRIX13:92

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

proof end;

theorem Th93: :: MATRIX13:93

for n', m', j, i being Nat
for K being Field
for a being Element of K
for M' being Matrix of n',m',K st j in Seg (len M') & j <> i holds
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,(a * (Line M',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 diagonal 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 NonZero being set st NonZero = { 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= NonZero & Q c= NonZero )

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 NonZero being set st NonZero = { i where i is Element of NAT : ( [i,i] in Indices M & M * i,i <> 0. K ) } holds
the_rank_of M = card NonZero

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;

definition

let K be Field;
let n be Nat;
:: original: -VectSp_over
redefine func n -VectSp_over K -> strict VectSp of K;
coherence
n -VectSp_over K is strict VectSp of K

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

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;

definition

let K be Field;
let n be Nat;
:: original: -VectSp_over
redefine func n -VectSp_over K -> strict finite-dimensional VectSp of K;
coherence
n -VectSp_over K is strict finite-dimensional VectSp of K

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;