let m, n be 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))
let K be 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))
let nt be 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))
let mt be 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))
let M be Matrix of K; ( [:(rng nt),(rng mt):] = Indices M implies the_rank_of M = the_rank_of (Segm (M,nt,mt)) )
set RM = the_rank_of M;
set S = Segm (M,nt,mt);
consider rt1, rt2 being Element of (the_rank_of M) -tuples_on NAT such that
A1:
[:(rng rt1),(rng rt2):] c= Indices M
and
A2:
Det (Segm (M,rt1,rt2)) <> 0. K
by Th76;
assume A3:
[:(rng nt),(rng mt):] = Indices M
; the_rank_of M = the_rank_of (Segm (M,nt,mt))
A4:
now the_rank_of M <= the_rank_of (Segm (M,nt,mt))per cases
( the_rank_of M = 0 or the_rank_of M > 0 )
;
suppose A5:
the_rank_of M > 0
;
the_rank_of M <= the_rank_of (Segm (M,nt,mt))then
len rt2 > 0
;
then A6:
rt2 <> {}
;
len rt1 > 0
by A5;
then A7:
rt1 <> {}
;
then
rng nt <> {}
by A3, A1, A6;
then
dom nt <> {}
by RELAT_1:42;
then A8:
n <> 0
;
then A9:
width (Segm (M,nt,mt)) = m
by Th1;
A10:
dom mt = Seg m
by FINSEQ_2:124;
set MR =
Segm (
M,
rt1,
rt2);
A11:
dom rt2 = Seg (the_rank_of M)
by FINSEQ_2:124;
rng rt1 c= rng nt
by A3, A1, A6, ZFMISC_1:114;
then consider R1 being
Function such that A12:
dom R1 = dom rt1
and A13:
rng R1 c= dom nt
and A14:
rt1 = nt * R1
by Th81;
rng rt2 c= rng mt
by A3, A1, A7, ZFMISC_1:114;
then consider R2 being
Function such that A15:
dom R2 = dom rt2
and A16:
rng R2 c= dom mt
and A17:
rt2 = mt * R2
by Th81;
A18:
dom rt1 = Seg (the_rank_of M)
by FINSEQ_2:124;
then reconsider R1 =
R1,
R2 =
R2 as
FinSequence by A12, A15, A11, FINSEQ_1:def 2;
A19:
rng R1 c= NAT
by A13, XBOOLE_1:1;
rng R2 c= NAT
by A16, XBOOLE_1:1;
then reconsider R1 =
R1,
R2 =
R2 as
FinSequence of
NAT by A19, FINSEQ_1:def 4;
A20:
len R1 = the_rank_of M
by A12, A18, FINSEQ_1:def 3;
len R2 = the_rank_of M
by A15, A11, FINSEQ_1:def 3;
then reconsider R1 =
R1,
R2 =
R2 as
Element of
(the_rank_of M) -tuples_on NAT by A20, FINSEQ_2:92;
set SR =
Segm (
(Segm (M,nt,mt)),
R1,
R2);
len (Segm (M,nt,mt)) = n
by Th1, A8;
then A21:
Indices (Segm (M,nt,mt)) = [:(Seg n),(Seg m):]
by A9, FINSEQ_1:def 3;
now for i, j being Nat st [i,j] in Indices (Segm ((Segm (M,nt,mt)),R1,R2)) holds
(Segm (M,rt1,rt2)) * (i,j) = (Segm ((Segm (M,nt,mt)),R1,R2)) * (i,j)A22:
dom mt = Seg m
by FINSEQ_2:124;
let i,
j be
Nat;
( [i,j] in Indices (Segm ((Segm (M,nt,mt)),R1,R2)) implies (Segm (M,rt1,rt2)) * (i,j) = (Segm ((Segm (M,nt,mt)),R1,R2)) * (i,j) )assume A23:
[i,j] in Indices (Segm ((Segm (M,nt,mt)),R1,R2))
;
(Segm (M,rt1,rt2)) * (i,j) = (Segm ((Segm (M,nt,mt)),R1,R2)) * (i,j)reconsider I =
i,
J =
j,
RI =
R1 . i,
RJ =
R2 . j as
Element of
NAT by ORDINAL1:def 12;
A24:
dom nt = Seg n
by FINSEQ_2:124;
A25:
Indices (Segm ((Segm (M,nt,mt)),R1,R2)) = [:(dom R1),(dom R2):]
by A12, A15, A18, A11, MATRIX_0:24;
then A26:
i in dom R1
by A23, ZFMISC_1:87;
A27:
j in dom R2
by A23, A25, ZFMISC_1:87;
then A28:
R2 . j in rng R2
by FUNCT_1:def 3;
R1 . i in rng R1
by A26, FUNCT_1:def 3;
then A29:
[(R1 . I),(R2 . J)] in Indices (Segm (M,nt,mt))
by A13, A16, A21, A28, A24, A22, ZFMISC_1:87;
[i,j] in Indices (Segm (M,rt1,rt2))
by A23, MATRIX_0:26;
hence (Segm (M,rt1,rt2)) * (
i,
j) =
M * (
(rt1 . I),
(rt2 . J))
by Def1
.=
M * (
(nt . RI),
(rt2 . J))
by A12, A14, A26, FUNCT_1:12
.=
M * (
(nt . RI),
(mt . RJ))
by A15, A17, A27, FUNCT_1:12
.=
(Segm (M,nt,mt)) * (
(R1 . I),
(R2 . J))
by A29, Def1
.=
(Segm ((Segm (M,nt,mt)),R1,R2)) * (
i,
j)
by A23, Def1
;
verum end; then A30:
Det (Segm ((Segm (M,nt,mt)),R1,R2)) <> 0. K
by A2, MATRIX_0:27;
dom nt = Seg n
by FINSEQ_2:124;
then
[:(rng R1),(rng R2):] c= Indices (Segm (M,nt,mt))
by A13, A16, A10, A21, ZFMISC_1:96;
hence
the_rank_of M <= the_rank_of (Segm (M,nt,mt))
by A30, Th76;
verum end; end; end;
the_rank_of M >= the_rank_of (Segm (M,nt,mt))
by A3, Th78;
hence
the_rank_of M = the_rank_of (Segm (M,nt,mt))
by A4, XXREAL_0:1; verum