let i, j, m9, n9 be Nat; :: thesis: for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) & j <> i holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))
let K be Field; :: thesis: for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) & j <> i holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))
let a be Element of K; :: thesis: for M9 being Matrix of n9,m9,K st j in Seg (len M9) & j <> i holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))
let M9 be Matrix of n9,m9,K; :: thesis: ( j in Seg (len M9) & j <> i implies the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j))))) )
assume that
A1: j in Seg (len M9) and
A2: i <> j ; :: thesis: the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))
per cases ( i in Seg (len M9) or not i in Seg (len M9) ) ;
suppose A3: i in Seg (len M9) ; :: thesis: the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))
set Li = Line (M9,i);
set W = width M9;
set R = RLine (M9,i,((0. K) * (Line (M9,i))));
A4: width M9 = len ((0. K) * (Line (M9,i))) by CARD_1:def 7;
then A5: len (RLine (M9,i,((0. K) * (Line (M9,i))))) = len M9 by MATRIX11:def 3;
set Lj = Line (M9,j);
A6: width M9 = len (a * (Line (M9,j))) by CARD_1:def 7;
reconsider 0Li = (0. K) * (Line (M9,i)), aLj = a * (Line (M9,j)) as Element of the carrier of K * by FINSEQ_1:def 11;
width (RLine (M9,i,((0. K) * (Line (M9,i))))) = width M9 by A4, MATRIX11:def 3;
then A7: RLine ((RLine (M9,i,((0. K) * (Line (M9,i))))),i,aLj) = Replace ((RLine (M9,i,((0. K) * (Line (M9,i))))),i,aLj) by A6, MATRIX11:29
.= Replace ((Replace (M9,i,0Li)),i,aLj) by A4, MATRIX11:29
.= Replace (M9,i,aLj) by FUNCT_7:34
.= RLine (M9,i,aLj) by A6, MATRIX11:29 ;
A8: len M9 = n9 by MATRIX_0:def 2;
then A9: Line ((RLine (M9,i,((0. K) * (Line (M9,i))))),j) = Line (M9,j) by A1, A2, MATRIX11:28;
Line ((RLine (M9,i,((0. K) * (Line (M9,i))))),i) = (0. K) * (Line (M9,i)) by A3, A4, A8, MATRIX11:28;
then A10: (Line ((RLine (M9,i,((0. K) * (Line (M9,i))))),i)) + (a * (Line ((RLine (M9,i,((0. K) * (Line (M9,i))))),j))) = ((width M9) |-> (0. K)) + (a * (Line (M9,j))) by A9, FVSUM_1:58
.= a * (Line (M9,j)) by FVSUM_1:21 ;
width M9 = len (Line (M9,i)) by CARD_1:def 7;
hence the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,((0. K) * (Line (M9,i))))) by Th91
.= the_rank_of (RLine (M9,i,(a * (Line (M9,j))))) by A1, A2, A5, A10, A7, Th92 ;
:: thesis: verum
end;
suppose A11: not i in Seg (len M9) ; :: thesis: the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))
then not i in dom M9 by FINSEQ_1:def 3;
then DelLine (M9,i) = M9 by FINSEQ_3:104;
hence the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j))))) by A11, Th40; :: thesis: verum
end;
end;