let n', m', i be Nat; for K being Field
for M' being Matrix of the carrier of K,n',
for p being FinSequence of st len p = width M' holds
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,((0. K) * p))
let K be Field; for M' being Matrix of the carrier of K,n',
for p being FinSequence of st len p = width M' holds
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,((0. K) * p))
let M' be Matrix of the carrier of K,n',; for p being FinSequence of st len p = width M' holds
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,((0. K) * p))
let p be FinSequence of ; ( len p = width M' implies the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,((0. K) * p)) )
assume A1:
len p = width M'
; the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,((0. K) * p))
set R = RLine M',i,((0. K) * p);
A2:
Seg (len M') = dom M'
by FINSEQ_1:def 3;
A3:
len M' = n'
by MATRIX_1:def 3;
per cases
( not i in dom M' or i in dom M' )
;
suppose A5:
i in dom M'
;
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,((0. K) * p))then B5:
n' <> 0
by A2, A3;
set KK = the
carrier of
K;
A6:
p is
Element of
(len p) -tuples_on the
carrier of
K
by FINSEQ_2:110;
A7:
len ((0. K) * p) = len p
by MATRIXR1:16;
then
Line (RLine M',i,((0. K) * p)),
i = (0. K) * p
by A1, A2, A3, A5, MATRIX11:28;
then A8:
Line (RLine M',i,((0. K) * p)),
i = (len p) |-> (0. K)
by A6, FVSUM_1:71;
reconsider 0p =
(0. K) * p as
Element of the
carrier of
K * by FINSEQ_1:def 11;
A9:
i in NAT
by ORDINAL1:def 13;
RLine M',
i,
((0. K) * p) = Replace M',
i,
0p
by A1, A7, MATRIX11:29;
then A10:
Replace (RLine M',i,((0. K) * p)),
i,
0p = Replace M',
i,
0p
by FUNCT_7:36;
A11:
width (RLine M',i,((0. K) * p)) = m'
by A2, A3, A5, Th1, FINSEQ_1:4, B5;
width M' = m'
by A2, A3, A5, Th1, FINSEQ_1:4, B5;
then
the_rank_of (RLine M',i,((0. K) * p)) = the_rank_of (DelLine (RLine M',i,((0. K) * p)),i)
by A1, A11, A8, Th90;
hence
the_rank_of (DelLine M',i) = the_rank_of (RLine M',i,((0. K) * p))
by A10, A9, COMPUT_1:7;
verum end;