:: 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
theorem Th2: :: MATRIX13:2
theorem Th3: :: MATRIX13:3
theorem Th4: :: MATRIX13:4
theorem Th5: :: MATRIX13:5
theorem Th6: :: MATRIX13:6
theorem Th7: :: MATRIX13:7
theorem Th8: :: MATRIX13:8
theorem Th9: :: MATRIX13:9
theorem Th10: :: MATRIX13:10
theorem :: MATRIX13:11
theorem Th12: :: MATRIX13:12
theorem Th13: :: MATRIX13:13
theorem :: MATRIX13:14
theorem Th15: :: MATRIX13:15
theorem :: MATRIX13:16
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)
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
end;
:: deftheorem Def1 defines Segm MATRIX13:def 1 :
theorem Th17: :: MATRIX13:17
theorem Th18: :: MATRIX13:18
theorem Th19: :: MATRIX13:19
theorem Th20: :: MATRIX13:20
theorem Th21: :: MATRIX13:21
theorem Th22: :: MATRIX13:22
theorem Th23: :: MATRIX13:23
theorem Th24: :: MATRIX13:24
theorem Th25: :: MATRIX13:25
theorem Th26: :: MATRIX13:26
theorem Th27: :: MATRIX13:27
theorem Th28: :: MATRIX13:28
theorem Th29: :: MATRIX13:29
theorem Th30: :: MATRIX13:30
theorem Th31: :: MATRIX13:31
theorem Th32: :: MATRIX13:32
theorem Th33: :: MATRIX13:33
theorem Th34: :: MATRIX13:34
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 )
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
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'))
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
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
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 )
theorem Th40: :: MATRIX13:40
theorem Th41: :: MATRIX13:41
theorem Th42: :: MATRIX13:42
theorem Th43: :: MATRIX13:43
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 :
theorem Th44: :: MATRIX13:44
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)
theorem Th46: :: MATRIX13:46
theorem Th47: :: MATRIX13:47
theorem Th48: :: MATRIX13:48
theorem Th49: :: MATRIX13:49
theorem Th50: :: MATRIX13:50
theorem Th51: :: MATRIX13:51
theorem Th52: :: MATRIX13:52
theorem Th53: :: MATRIX13:53
theorem Th54: :: MATRIX13:54
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)
theorem Th55: :: MATRIX13:55
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 )
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 ) ) )
theorem Th58: :: MATRIX13:58
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
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
theorem :: MATRIX13:61
theorem Th62: :: MATRIX13:62
theorem Th63: :: MATRIX13:63
:: deftheorem Def3 defines EqSegm MATRIX13:def 3 :
theorem Th64: :: MATRIX13:64
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 )
theorem Th65: :: MATRIX13:65
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 )
theorem :: MATRIX13:66
theorem Th67: :: MATRIX13:67
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)) ) )
theorem Th69: :: MATRIX13:69
theorem Th70: :: MATRIX13:70
theorem Th71: :: MATRIX13:71
theorem Th72: :: MATRIX13:72
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 ) )
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
end;
:: deftheorem Def4 defines the_rank_of MATRIX13:def 4 :
theorem Th73: :: MATRIX13:73
theorem Th74: :: MATRIX13:74
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 ) ) )
theorem Th75: :: MATRIX13:75
theorem Th76: :: MATRIX13:76
theorem Th77: :: MATRIX13:77
theorem Th78: :: MATRIX13:78
theorem Th79: :: MATRIX13:79
theorem Th80: :: MATRIX13:80
theorem Th81: :: MATRIX13:81
theorem Th82: :: MATRIX13:82
theorem Th83: :: MATRIX13:83
theorem :: MATRIX13:84
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
theorem :: MATRIX13:85
theorem :: MATRIX13:86
theorem Th87: :: MATRIX13:87
theorem Th88: :: MATRIX13:88
theorem Th89: :: MATRIX13:89
theorem Th90: :: MATRIX13:90
theorem Th91: :: MATRIX13:91
theorem Th92: :: MATRIX13:92
theorem Th93: :: MATRIX13:93
theorem Th94: :: MATRIX13:94
theorem :: MATRIX13:95
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 ) ) )
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) ) ) )
theorem :: MATRIX13:98
theorem Th99: :: MATRIX13:99
theorem Th100: :: MATRIX13:100
theorem :: MATRIX13:101
theorem Th102: :: MATRIX13:102
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)
theorem Th103: :: MATRIX13:103
theorem :: MATRIX13:104
:: deftheorem defines FinS2MX MATRIX13:def 5 :
:: deftheorem defines MX2FinS MATRIX13:def 6 :
theorem Th105: :: MATRIX13:105
theorem Th106: :: MATRIX13:106
theorem Th107: :: MATRIX13:107
theorem Th108: :: MATRIX13:108
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 )
theorem Th110: :: MATRIX13:110
theorem Th111: :: MATRIX13:111
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 )
theorem :: MATRIX13:112
theorem Th113: :: MATRIX13:113
theorem Th114: :: MATRIX13:114
theorem Th115: :: MATRIX13:115
theorem Th116: :: MATRIX13:116
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 )
theorem Th118: :: MATRIX13:118
theorem Th119: :: MATRIX13:119
theorem Th120: :: MATRIX13:120
theorem Th121: :: MATRIX13:121
theorem Th122: :: MATRIX13:122
theorem :: MATRIX13:123