let i, m9, n9 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_0:def 2;
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 A6:
n9 <> 0
by A2, A3;
set KK = the
carrier of
K;
A7:
p is
Element of
(len p) -tuples_on the
carrier of
K
by FINSEQ_2:92;
A8:
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 A9:
Line (
(RLine (M9,i,((0. K) * p))),
i)
= (len p) |-> (0. K)
by A7, FVSUM_1:58;
reconsider 0p =
(0. K) * p as
Element of the
carrier of
K * by FINSEQ_1:def 11;
A10:
i in NAT
by ORDINAL1:def 12;
RLine (
M9,
i,
((0. K) * p))
= Replace (
M9,
i,
0p)
by A1, A8, MATRIX11:29;
then A11:
Replace (
(RLine (M9,i,((0. K) * p))),
i,
0p)
= Replace (
M9,
i,
0p)
by FUNCT_7:34;
A12:
width (RLine (M9,i,((0. K) * p))) = m9
by Th1, A6;
width M9 = m9
by Th1, A6;
then
the_rank_of (RLine (M9,i,((0. K) * p))) = the_rank_of (DelLine ((RLine (M9,i,((0. K) * p))),i))
by A1, A12, A9, Th90;
hence
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * p)))
by A11, A10, COMPUT_1:4;
verum end;