begin
begin
definition
let D be non
empty set ;
let M be
Matrix of
D;
let n,
m be
Nat;
let nt be
Element of
n -tuples_on NAT;
let mt be
Element of
m -tuples_on NAT;
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;
theorem Th22:
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)))
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
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 one-to-one holds
nt1 is one-to-one
theorem Th36:
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)))
theorem Th37:
for
D being non
empty set for
n9,
m9,
n,
m being
Nat for
A9 being
Matrix of
n9,
m9,
D for
F,
Fmt being
FinSequence of
D for
nt being
Element of
n -tuples_on NAT for
mt being
Element of
m -tuples_on NAT st
len F = width A9 &
Fmt = F * mt &
[:(rng nt),(rng mt):] c= Indices A9 holds
for
i,
j being
Nat st
nt " {j} = {i} holds
RLine (
(Segm (A9,nt,mt)),
i,
Fmt)
= Segm (
(RLine (A9,j,F)),
nt,
mt)
theorem Th38:
for
D being non
empty set for
n9,
m9,
m,
n being
Nat for
A9 being
Matrix of
n9,
m9,
D for
mt being
Element of
m -tuples_on NAT for
F being
FinSequence of
D for
i being
Nat for
nt being
Element of
n -tuples_on NAT st not
i in rng nt &
[:(rng nt),(rng mt):] c= Indices A9 holds
Segm (
A9,
nt,
mt)
= Segm (
(RLine (A9,i,F)),
nt,
mt)
theorem Th39:
for
D being non
empty set for
n9,
m9,
m,
i,
n,
j being
Nat for
A9 being
Matrix of
n9,
m9,
D for
nt being
Element of
n -tuples_on NAT for
mt being
Element of
m -tuples_on NAT st
i in rng nt &
[:(rng nt),(rng mt):] c= Indices A9 holds
ex
nt1 being
Element of
n -tuples_on NAT st
(
rng nt1 = ((rng nt) \ {i}) \/ {j} &
Segm (
(RLine (A9,i,(Line (A9,j)))),
nt,
mt)
= Segm (
A9,
nt1,
mt) )
theorem Th45:
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)))
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 Th56:
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:
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 Th59:
for
D being non
empty set for
n9,
m9,
i being
Nat for
A9 being
Matrix of
n9,
m9,
D for
Q,
P being
finite without_zero Subset of
NAT for
F,
FQ being
FinSequence of
D st
len F = width A9 &
FQ = F * (Sgm Q) &
[:P,Q:] c= Indices A9 holds
RLine (
(Segm (A9,P,Q)),
i,
FQ)
= Segm (
(RLine (A9,((Sgm P) . i),F)),
P,
Q)
theorem Th60:
for
D being non
empty set for
n9,
m9 being
Nat for
A9 being
Matrix of
n9,
m9,
D for
Q being
finite without_zero Subset of
NAT for
F being
FinSequence of
D for
i being
Nat for
P being
finite without_zero Subset of
NAT st not
i in P &
[:P,Q:] c= Indices A9 holds
Segm (
A9,
P,
Q)
= Segm (
(RLine (A9,i,F)),
P,
Q)
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 )
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 )
theorem Th68:
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))) ) )
definition
let K be
Field;
let M be
Matrix of
K;
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;
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 ) ) )
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 Th96:
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:
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)) ) ) )
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 Th109:
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 )
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 Th117:
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 )