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):] c= 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):] c= 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):] c= 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):] c= Indices M holds
the_rank_of M >= the_rank_of (Segm (M,nt,mt))
let M be Matrix of K; ( [:(rng nt),(rng mt):] c= Indices M implies the_rank_of M >= the_rank_of (Segm (M,nt,mt)) )
assume A1:
[:(rng nt),(rng mt):] c= Indices M
; the_rank_of M >= the_rank_of (Segm (M,nt,mt))
per cases
( n = 0 or m = 0 or ( n > 0 & m > 0 ) )
;
suppose A2:
(
n > 0 &
m > 0 )
;
the_rank_of M >= the_rank_of (Segm (M,nt,mt))A3:
dom mt = Seg m
by FINSEQ_2:124;
A4:
dom nt = Seg n
by FINSEQ_2:124;
set S =
Segm (
M,
nt,
mt);
set RS =
the_rank_of (Segm (M,nt,mt));
consider rt1,
rt2 being
Element of
(the_rank_of (Segm (M,nt,mt))) -tuples_on NAT such that A5:
[:(rng rt1),(rng rt2):] c= Indices (Segm (M,nt,mt))
and A6:
Det (Segm ((Segm (M,nt,mt)),rt1,rt2)) <> 0. K
by Th76;
set mr =
mt * rt2;
A7:
ex
R1,
R2 being
finite without_zero Subset of
NAT st
(
R1 = rng rt1 &
R2 = rng rt2 &
card R1 = card R2 &
card R1 = the_rank_of (Segm (M,nt,mt)) &
Det (EqSegm ((Segm (M,nt,mt)),R1,R2)) <> 0. K )
by A5, A6, Th75;
set nr =
nt * rt1;
A8:
rng (mt * rt2) c= rng mt
by RELAT_1:26;
len (Segm (M,nt,mt)) = n
by A2, Th1;
then A9:
rng rt1 c= dom nt
by A5, A7, A4, Th67;
then
dom (nt * rt1) = dom rt1
by RELAT_1:27;
then A10:
dom (nt * rt1) = Seg (the_rank_of (Segm (M,nt,mt)))
by FINSEQ_2:124;
width (Segm (M,nt,mt)) = m
by A2, Th1;
then A11:
rng rt2 c= dom mt
by A5, A7, A3, Th67;
then
dom (mt * rt2) = dom rt2
by RELAT_1:27;
then A12:
dom (mt * rt2) = Seg (the_rank_of (Segm (M,nt,mt)))
by FINSEQ_2:124;
rng mt c= NAT
by FINSEQ_1:def 4;
then A13:
rng (mt * rt2) c= NAT
by A8;
set SS =
Segm (
(Segm (M,nt,mt)),
rt1,
rt2);
A14:
rng (nt * rt1) c= rng nt
by RELAT_1:26;
rng nt c= NAT
by FINSEQ_1:def 4;
then A15:
rng (nt * rt1) c= NAT
by A14;
reconsider nr =
nt * rt1,
mr =
mt * rt2 as
FinSequence by A9, A11, FINSEQ_1:16;
reconsider nr =
nr,
mr =
mr as
FinSequence of
NAT by A15, A13, FINSEQ_1:def 4;
A16:
len nr = the_rank_of (Segm (M,nt,mt))
by A10, FINSEQ_1:def 3;
len mr = the_rank_of (Segm (M,nt,mt))
by A12, FINSEQ_1:def 3;
then reconsider nr =
nr,
mr =
mr as
Element of
(the_rank_of (Segm (M,nt,mt))) -tuples_on NAT by A16, FINSEQ_2:92;
set MR =
Segm (
M,
nr,
mr);
now for i, j being Nat st [i,j] in Indices (Segm ((Segm (M,nt,mt)),rt1,rt2)) holds
(Segm (M,nr,mr)) * (i,j) = (Segm ((Segm (M,nt,mt)),rt1,rt2)) * (i,j)let i,
j be
Nat;
( [i,j] in Indices (Segm ((Segm (M,nt,mt)),rt1,rt2)) implies (Segm (M,nr,mr)) * (i,j) = (Segm ((Segm (M,nt,mt)),rt1,rt2)) * (i,j) )assume A17:
[i,j] in Indices (Segm ((Segm (M,nt,mt)),rt1,rt2))
;
(Segm (M,nr,mr)) * (i,j) = (Segm ((Segm (M,nt,mt)),rt1,rt2)) * (i,j)reconsider I =
i,
J =
j,
rtI =
rt1 . i,
rtJ =
rt2 . j as
Element of
NAT by ORDINAL1:def 12;
A18:
[(rt1 . I),(rt2 . J)] in Indices (Segm (M,nt,mt))
by A5, A17, Th17;
A19:
Indices (Segm ((Segm (M,nt,mt)),rt1,rt2)) = [:(dom nr),(dom mr):]
by A10, A12, MATRIX_0:24;
then A20:
i in dom nr
by A17, ZFMISC_1:87;
A21:
j in dom mr
by A17, A19, ZFMISC_1:87;
[i,j] in Indices (Segm (M,nr,mr))
by A17, MATRIX_0:26;
hence (Segm (M,nr,mr)) * (
i,
j) =
M * (
(nr . I),
(mr . J))
by Def1
.=
M * (
(nt . rtI),
(mr . J))
by A20, FUNCT_1:12
.=
M * (
(nt . rtI),
(mt . rtJ))
by A21, FUNCT_1:12
.=
(Segm (M,nt,mt)) * (
(rt1 . I),
(rt2 . J))
by A18, Def1
.=
(Segm ((Segm (M,nt,mt)),rt1,rt2)) * (
i,
j)
by A17, Def1
;
verum end; then A22:
Segm (
(Segm (M,nt,mt)),
rt1,
rt2)
= Segm (
M,
nr,
mr)
by MATRIX_0:27;
[:(rng nr),(rng mr):] c= [:(rng nt),(rng mt):]
by A14, A8, ZFMISC_1:96;
then
[:(rng nr),(rng mr):] c= Indices M
by A1;
hence
the_rank_of M >= the_rank_of (Segm (M,nt,mt))
by A6, A22, Th76;
verum end; end;