let n9, m9, i be Nat; for K being Field
for M9 being Matrix of n9,m9,K
for p being FinSequence of K st len p = width M9 holds
the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,((0. K) * p))
let K be Field; for M9 being Matrix of n9,m9,K
for p being FinSequence of K st len p = width M9 holds
the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,((0. K) * p))
let M9 be Matrix of n9,m9,K; for p being FinSequence of K st len p = width M9 holds
the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,((0. K) * p))
let p be FinSequence of K; ( len p = width M9 implies the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,((0. K) * p)) )
assume A1:
len p = width M9
; the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,((0. K) * p))
set R = RLine M9,i,((0. K) * p);
A2:
Seg (len M9) = dom M9
by FINSEQ_1:def 3;
A3:
len M9 = n9
by MATRIX_1:def 3;
per cases
( not i in dom M9 or i in dom M9 )
;
suppose A5:
i in dom M9
;
the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,((0. K) * p))then B5:
n9 <> 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 M9,i,((0. K) * p)),
i = (0. K) * p
by A1, A2, A3, A5, MATRIX11:28;
then A8:
Line (RLine M9,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 M9,
i,
((0. K) * p) = Replace M9,
i,
0p
by A1, A7, MATRIX11:29;
then A10:
Replace (RLine M9,i,((0. K) * p)),
i,
0p = Replace M9,
i,
0p
by FUNCT_7:36;
A11:
width (RLine M9,i,((0. K) * p)) = m9
by Th1, B5;
width M9 = m9
by Th1, B5;
then
the_rank_of (RLine M9,i,((0. K) * p)) = the_rank_of (DelLine (RLine M9,i,((0. K) * p)),i)
by A1, A11, A8, Th90;
hence
the_rank_of (DelLine M9,i) = the_rank_of (RLine M9,i,((0. K) * p))
by A10, A9, COMPUT_1:7;
verum end;