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