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

theorem Th1: :: MATRIX13:1
for D being non empty set
for m, n 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
() . 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 $$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$$
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 () 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 () & ( 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 () & ( 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 () & ( 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 ((),()) )
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 ((),()) )
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 b1 being Matrix of n,m,D st
for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = M * ((nt . i),(mt . j))
proof end;
uniqueness
for b1, b2 being Matrix of n,m,D st ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * (i,j) = M * ((nt . i),(mt . j)) ) & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * (i,j) = M * ((nt . i),(mt . j)) ) holds
b1 = b2
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 b7 being Matrix of n,m,D holds
( b7 = Segm (M,nt,mt) iff for i, j being Nat st [i,j] in Indices b7 holds
b7 * (i,j) = M * ((nt . i),(mt . j)) );

theorem Th17: :: MATRIX13:17
for D being non empty set
for i, j, 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 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 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 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 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 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 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 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 i, 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 i in Seg n & rng mt c= Seg () 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 i, j, 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 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, j, n 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 one-to-one holds
Det (Segm (M,nt,nt1)) = 0. K
proof end;

theorem Th28: :: MATRIX13:28
for D being non empty set
for j, 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 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 i, j, 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 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, j, m 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 one-to-one 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 one-to-one & nt1 is one-to-one & 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 nt, nt1 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 m, n being Nat
for A being Matrix of D
for nt being Element of n -tuples_on NAT
for mt, mt1 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 nt, nt1, nt2 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 one-to-one holds
nt1 is one-to-one

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 m, n, m9, n9 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 m, n, m9, n9 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 i, j, m, n, m9, n9 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 i, m9, n9 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 m, n 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 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 nt = idseq (len A) & mt = idseq () holds
Segm (A,nt,mt) = A
proof end;

registration
existence
ex b1 being Subset of NAT st
( b1 is empty & b1 is without_zero & b1 is finite )
proof end;
existence
ex b1 being Subset of NAT st
( not b1 is empty & b1 is without_zero & b1 is finite )
proof end;
end;

registration
let n be Nat;
coherence by FINSEQ_1:1;
end;

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

definition
let i be Nat;
:: original: {
redefine func {i} -> Subset of NAT;
coherence
{i} is Subset of NAT
by ;
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 ())) = 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 () 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 ()))),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 P, Q 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 ())) = 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 ()) \ {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, P2, Q, Q1, 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, P1, Q, 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 i, j, n 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 i, m9, n9 being Nat
for A9 being Matrix of n9,m9,D
for P, Q 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 m9, n9 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 () ) )
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) = (() . (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)) = (() . (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 b1 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 = b1 & 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 <= b1 ) )
proof end;
uniqueness
for b1, b2 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 = b1 & 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 <= b1 ) & ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = b2 & 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 <= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines the_rank_of MATRIX13:def 4 :
for K being Field
for M being Matrix of K
for b3 being Element of NAT holds
( b3 = 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 = b3 & 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 <= b3 ) ) );

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 m, n 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 m, n 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 m, n 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 m, n 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
() . (a,n) <> 0. K

proof end;

theorem :: MATRIX13:85
for m, n 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 i, m9, n9 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) = () |-> (0. K) holds
the_rank_of (DelLine (M,i)) = the_rank_of M
proof end;

theorem Th91: :: MATRIX13:91
for i, m9, n9 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 i, j, m9, n9 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 i, j, m9, n9 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),()) )
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 () & 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;
existence
ex b1 being Matrix of K st b1 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 V185(b1)
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 v, v1, v2 being Vector of ()
for t, t1, t2 being Element of n -tuples_on the carrier of K holds
( the carrier of () = n -tuples_on the carrier of K & 0. () = 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;
coherence
proof end;
end;

registration
let K be Field;
let n be Nat;
cluster -> Relation-like Function-like for Element of the carrier of ();
correctness
coherence
for b1 being Vector of () holds
( b1 is Function-like & b1 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 ()

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 ();
coherence
lines is Subset of ()
by Lm7;
end;

theorem Th103: :: MATRIX13:103
for x being object
for m, n 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 () 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 ();
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 () 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 () equals :: MATRIX13:def 6
M;
coherence
M is FinSequence of ()
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 m, n 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 i, m, n 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 (#) ())),i) = a * (Line (M,i))
proof end;

theorem Th107: :: MATRIX13:107
for i, m, 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 (#) ())),i))
proof end;

theorem Th108: :: MATRIX13:108
for m, n 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 (#) () = M1
proof end;

theorem Th109: :: MATRIX13:109
for m, n 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 m, n 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 V185(b2) Matrix of n,K st the_rank_of M = n holds
lines M is Basis of ()
proof end;

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

proof end;

registration
let K be Field;
let n be Nat;
coherence
proof end;
end;

theorem :: MATRIX13:112
for n being Nat
for K being Field holds dim () = n
proof end;

theorem Th113: :: MATRIX13:113
for m, n 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 ()) \ {i})) is without_repeated_line )
proof end;

theorem Th114: :: MATRIX13:114
for m, n 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 ()) \ {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 object
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 m, n 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 m, n being Nat
for K being Field
for M being Matrix of m,n,K
for U being Subset of () 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 () st
( U is linearly-independent & U c= lines M & card U = RANK ) & ( for W being finite Subset of () st W is linearly-independent & W c= lines M holds
card W <= RANK ) ) )
proof end;