begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem
begin
definition
let D be non
empty set ;
let M be
Matrix of ;
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:
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:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
for
n being
Nat for
K being
Field for
nt1,
nt2,
nt being
Element of
n -tuples_on NAT for
M being
Matrix of
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:
for
n being
Nat for
K being
Field for
M being
Matrix of
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:
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:
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:
for
D being non
empty set for
n',
m',
m,
i,
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 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:
theorem Th41:
theorem Th42:
theorem Th43:
definition
let D be non
empty set ;
let A be
Matrix of ;
let P,
Q be
finite without_zero Subset of ;
func Segm A,
P,
Q -> Matrix of
card P,
card Q,
D equals
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:
theorem Th45:
for
D being non
empty set for
i0,
j0,
n0,
m0 being non
zero Nat for
A being
Matrix of 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:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
Lm2:
for X being set
for P being finite without_zero Subset of st X c= P holds
card X = card ((Sgm P) " X)
theorem Th55:
theorem Th56:
for
D being non
empty set for
A being
Matrix of
for
P,
P1,
Q,
Q1,
P2,
Q2 being
finite without_zero Subset of 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:
for
D being non
empty set for
A being
Matrix of
for
P,
Q,
P1,
Q1 being
finite without_zero Subset of 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 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:
theorem Th59:
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
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:
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
for
F being
FinSequence of
D for
i being
Nat for
P being
finite without_zero Subset of st not
i in P &
[:P,Q:] c= Indices A' holds
Segm A',
P,
Q = Segm (RLine A',i,F),
P,
Q
theorem
theorem Th62:
theorem Th63:
:: deftheorem Def3 defines EqSegm MATRIX13:def 3 :
theorem Th64:
Lm3:
for K being Field
for M being Matrix of
for P, Q being finite without_zero Subset of
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 )
theorem Th65:
Lm4:
for j being Nat
for K being Field
for M being Matrix of
for P, Q being finite without_zero Subset of
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 )
theorem
theorem Th67:
theorem Th68:
for
m',
n' being
Nat for
K being
Field for
M' being
Matrix of the
carrier of
K,
n',
for
P,
Q being
finite without_zero Subset of
for
i being
Nat for
j0 being non
zero Nat st
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:
theorem Th70:
theorem Th71:
theorem Th72:
definition
let K be
Field;
let M be
Matrix of ;
func the_rank_of M -> Element of
NAT means :
Def4:
( ex
P,
Q being
finite without_zero Subset of 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 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 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 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 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 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 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 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:
theorem Th74:
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 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 holds
( not P1 = rng nt or not P2 = rng mt ) ) )
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
theorem Th83:
theorem
Lm6:
for n being Nat
for K being Field
for a being Element of st a <> 0. K holds
(power K) . a,n <> 0. K
theorem
theorem
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
theorem Th94:
theorem
theorem Th96:
for
K being
Field for
M being
Matrix of 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:
for
K being
Field for
M being
Matrix of 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
theorem Th99:
theorem Th100:
theorem
theorem Th102:
Lm7:
for m, n being Nat
for K being Field
for M being Matrix of the carrier of K,m, holds rng M is Subset of
theorem Th103:
theorem
:: deftheorem defines FinS2MX MATRIX13:def 5 :
:: deftheorem defines MX2FinS MATRIX13:def 6 :
theorem Th105:
theorem Th106:
theorem Th107:
theorem Th108:
theorem Th109:
for
n,
m being
Nat for
K being
Field for
M being
Matrix of the
carrier of
K,
m, 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 the
carrier of
K,
m, st ( for
i being
Nat st
i in Seg m holds
ex
a being
Element of 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:
theorem Th111:
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
theorem Th113:
theorem Th114:
theorem Th115:
theorem Th116:
theorem Th117:
for
n,
m being
Nat for
K being
Field for
a being
Element of
for
M being
Matrix of the
carrier of
K,
m, 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:
theorem Th119:
theorem Th120:
theorem Th121:
theorem Th122:
theorem