let m, n be Nat; :: thesis: for K being Field

for M being Matrix of n,m,K

for i, j being Nat

for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds

Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

let K be Field; :: thesis: for M being Matrix of n,m,K

for i, j being Nat

for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds

Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

let M be Matrix of n,m,K; :: thesis: for i, j being Nat

for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds

Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

let i, j be Nat; :: thesis: for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds

Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

let a be Element of K; :: thesis: ( M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) implies Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))))) )

assume that

A1: M is without_repeated_line and

A2: j in dom M and

A3: ( i = j implies a <> - (1_ K) ) ; :: thesis: Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

A4: len M = n by MATRIX_0:def 2;

set L = (Line (M,i)) + (a * (Line (M,j)));

A5: dom M = Seg (len M) by FINSEQ_1:def 3;

set R = RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))));

for M being Matrix of n,m,K

for i, j being Nat

for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds

Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

let K be Field; :: thesis: for M being Matrix of n,m,K

for i, j being Nat

for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds

Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

let M be Matrix of n,m,K; :: thesis: for i, j being Nat

for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds

Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

let i, j be Nat; :: thesis: for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds

Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

let a be Element of K; :: thesis: ( M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) implies Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))))) )

assume that

A1: M is without_repeated_line and

A2: j in dom M and

A3: ( i = j implies a <> - (1_ K) ) ; :: thesis: Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

A4: len M = n by MATRIX_0:def 2;

set L = (Line (M,i)) + (a * (Line (M,j)));

A5: dom M = Seg (len M) by FINSEQ_1:def 3;

set R = RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))));

per cases
( not i in dom M or i in dom M )
;

end;

suppose
not i in dom M
; :: thesis: Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

hence
Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))
by A5, MATRIX13:40; :: thesis: verum

end;suppose A6:
i in dom M
; :: thesis: Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))

then
n <> 0
by A5, A4;

then A7: width M = m by MATRIX_0:23;

then reconsider Li = Line (M,i), Lj = Line (M,j) as Vector of (m -VectSp_over K) by MATRIX13:102;

a * Lj = a * (Line (M,j)) by A7, MATRIX13:102;

then A8: (Line (M,i)) + (a * (Line (M,j))) = Li + (a * Lj) by A7, MATRIX13:102;

A9: ( not Li = Lj or a <> - (1_ K) or Li = 0. (m -VectSp_over K) )

reconsider LL = L9 as set ;

set iL = {i} --> L9;

len ((Line (M,i)) + (a * (Line (M,j)))) = width M by CARD_1:def 7;

then A11: RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) = M +* (i,LL) by MATRIX11:29

.= M +* (i .--> LL) by A6, FUNCT_7:def 3

.= M +* ({i} --> L9) by FUNCOP_1:def 9 ;

M .: ((dom M) \ (dom ({i} --> L9))) = (M .: (dom M)) \ (M .: (dom ({i} --> L9))) by A1, FUNCT_1:64

.= (rng M) \ (M .: (dom ({i} --> L9))) by RELAT_1:113

.= (rng M) \ (Im (M,i))

.= (rng M) \ {(M . i)} by A6, FUNCT_1:59

.= (rng M) \ {(Line (M,i))} by A5, A4, A6, MATRIX_0:52 ;

then A12: lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) = ((lines M) \ {(Line (M,i))}) \/ (rng ({i} --> L9)) by A11, FRECHET:12

.= ((lines M) \ {(Line (M,i))}) \/ {((Line (M,i)) + (a * (Line (M,j))))} by FUNCOP_1:8 ;

A13: Lj in lines M by A2, A5, A4, MATRIX13:103;

Li in lines M by A5, A4, A6, MATRIX13:103;

hence Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))))) by A8, A12, A13, A9, Th14; :: thesis: verum

end;then A7: width M = m by MATRIX_0:23;

then reconsider Li = Line (M,i), Lj = Line (M,j) as Vector of (m -VectSp_over K) by MATRIX13:102;

a * Lj = a * (Line (M,j)) by A7, MATRIX13:102;

then A8: (Line (M,i)) + (a * (Line (M,j))) = Li + (a * Lj) by A7, MATRIX13:102;

A9: ( not Li = Lj or a <> - (1_ K) or Li = 0. (m -VectSp_over K) )

proof

reconsider L9 = (Line (M,i)) + (a * (Line (M,j))) as Element of the carrier of K * by FINSEQ_1:def 11;
assume A10:
Li = Lj
; :: thesis: ( a <> - (1_ K) or Li = 0. (m -VectSp_over K) )

( Li = M . i & Lj = M . j ) by A2, A5, A4, A6, MATRIX_0:52;

hence ( a <> - (1_ K) or Li = 0. (m -VectSp_over K) ) by A1, A2, A3, A6, A10, FUNCT_1:def 4; :: thesis: verum

end;( Li = M . i & Lj = M . j ) by A2, A5, A4, A6, MATRIX_0:52;

hence ( a <> - (1_ K) or Li = 0. (m -VectSp_over K) ) by A1, A2, A3, A6, A10, FUNCT_1:def 4; :: thesis: verum

reconsider LL = L9 as set ;

set iL = {i} --> L9;

len ((Line (M,i)) + (a * (Line (M,j)))) = width M by CARD_1:def 7;

then A11: RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) = M +* (i,LL) by MATRIX11:29

.= M +* (i .--> LL) by A6, FUNCT_7:def 3

.= M +* ({i} --> L9) by FUNCOP_1:def 9 ;

M .: ((dom M) \ (dom ({i} --> L9))) = (M .: (dom M)) \ (M .: (dom ({i} --> L9))) by A1, FUNCT_1:64

.= (rng M) \ (M .: (dom ({i} --> L9))) by RELAT_1:113

.= (rng M) \ (Im (M,i))

.= (rng M) \ {(M . i)} by A6, FUNCT_1:59

.= (rng M) \ {(Line (M,i))} by A5, A4, A6, MATRIX_0:52 ;

then A12: lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) = ((lines M) \ {(Line (M,i))}) \/ (rng ({i} --> L9)) by A11, FRECHET:12

.= ((lines M) \ {(Line (M,i))}) \/ {((Line (M,i)) + (a * (Line (M,j))))} by FUNCOP_1:8 ;

A13: Lj in lines M by A2, A5, A4, MATRIX13:103;

Li in lines M by A5, A4, A6, MATRIX13:103;

hence Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))))) by A8, A12, A13, A9, Th14; :: thesis: verum