let m, n be Nat; :: thesis: for K being Field
for a being Element of K
for M being Matrix of m,n,K st lines M is linearly-independent & M is without_repeated_line holds
for i, j being Nat st j in Seg (len M) & i <> j holds
( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )
let K be Field; :: thesis: for a being Element of K
for M being Matrix of m,n,K st lines M is linearly-independent & M is without_repeated_line holds
for i, j being Nat st j in Seg (len M) & i <> j holds
( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )
let a be Element of K; :: thesis: for M being Matrix of m,n,K st lines M is linearly-independent & M is without_repeated_line holds
for i, j being Nat st j in Seg (len M) & i <> j holds
( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )
let M be Matrix of m,n,K; :: thesis: ( lines M is linearly-independent & M is without_repeated_line implies for i, j being Nat st j in Seg (len M) & i <> j holds
( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent ) )
assume that
A1: lines M is linearly-independent and
A2: M is without_repeated_line ; :: thesis: for i, j being Nat st j in Seg (len M) & i <> j holds
( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )
set V = n -VectSp_over K;
let i, j be Nat; :: thesis: ( j in Seg (len M) & i <> j implies ( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent ) )
assume that
A3: j in Seg (len M) and
A4: i <> j ; :: thesis: ( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )
set Lj = Line (M,j);
set Li = Line (M,i);
set R = RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))));

per cases ( not i in Seg (len M) or i in Seg (len M) ) ;

suppose not i in Seg (len M) ; :: thesis: ( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )

hence ( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent ) by A1, A2, Th40; :: thesis: verum

end;

suppose A5: i in Seg (len M) ; :: thesis: ( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )

reconsider N = n as Element of NAT by ORDINAL1:def 12;
A6: dom M = Seg (len M) by FINSEQ_1:def 3;
then A7: M . i <> M . j by A2, A3, A4, A5;
A8: len M = m by MATRIX_0:def 2;
then A9: Line (M,j) in lines M by A3, Th103;
A10: Line (M,i) in lines M by A5, A8, Th103;
then reconsider LI = Line (M,i), LJ = Line (M,j) as Vector of (n -VectSp_over K) by A9;
reconsider li = LI, lj = LJ as Element of N -tuples_on the carrier of K by Th102;
A11: M . i = Line (M,i) by A5, A8, MATRIX_0:52;
m <> 0 by A5, A8;
then A12: n = width M by Th1;
A13: M . j = Line (M,j) by A3, A8, MATRIX_0:52;
A14: for k being Nat st k in Seg m & k <> i holds
Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),k) <> (Line (M,i)) + (a * (Line (M,j)))

proof

a * lj = a * LJ by Th102;
then li + (a * lj) = LI + (a * LJ) by Th102
.= ((1_ K) * LI) + (a * LJ) ;
then A15: li + (a * lj) in Lin {LI,LJ} by Th116;
let k be Nat; :: thesis: ( k in Seg m & k <> i implies Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),k) <> (Line (M,i)) + (a * (Line (M,j))) )
assume that
A16: k in Seg m and
A17: k <> i ; :: thesis: Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),k) <> (Line (M,i)) + (a * (Line (M,j)))
set Lk = Line (M,k);
assume A18: Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),k) = (Line (M,i)) + (a * (Line (M,j))) ; :: thesis: contradiction
A19: Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),k) = Line (M,k) by A16, A17, MATRIX11:28;
A20: Line (M,j) <> Line (M,k)

proof

{LI,LJ} c= lines M by A10, A9, ZFMISC_1:32;
then A21: {LI,LJ} is linearly-independent by A1, VECTSP_7:1;
assume A22: Line (M,j) = Line (M,k) ; :: thesis: contradiction
A23: ((1_ K) + ((- (1_ K)) * a)) * LJ = ((1_ K) + ((- (1_ K)) * a)) * lj by Th102;
A24: (- (1_ K)) * LI = (- (1_ K)) * li by Th102;
0. (n -VectSp_over K) = n |-> (0. K) by Th102
.= lj + (- (li + (a * lj))) by A19, A18, A22, FVSUM_1:26
.= lj + ((- li) + (- (a * lj))) by FVSUM_1:31
.= lj + (((- (1_ K)) * li) + (- (a * lj))) by FVSUM_1:59
.= lj + (((- (1_ K)) * li) + ((- (1_ K)) * (a * lj))) by FVSUM_1:59
.= lj + (((- (1_ K)) * li) + (((- (1_ K)) * a) * lj)) by FVSUM_1:54
.= lj + ((((- (1_ K)) * a) * lj) + ((- (1_ K)) * li)) by FINSEQOP:33
.= (lj + (((- (1_ K)) * a) * lj)) + ((- (1_ K)) * li) by FINSEQOP:28
.= (((1_ K) * lj) + (((- (1_ K)) * a) * lj)) + ((- (1_ K)) * li) by FVSUM_1:57
.= (((1_ K) + ((- (1_ K)) * a)) * lj) + ((- (1_ K)) * li) by FVSUM_1:55
.= (((1_ K) + ((- (1_ K)) * a)) * LJ) + ((- (1_ K)) * LI) by A24, A23, Th102 ;
then - (1_ K) = 0. K by A7, A11, A13, A21, VECTSP_7:6;
hence contradiction by VECTSP_1:28; :: thesis: verum

end;

A25: Line (M,k) in lines M by A16, Th103;
then reconsider LK = Line (M,k) as Vector of (n -VectSp_over K) ;
reconsider KIJ = {LK,LI,LJ} as Subset of (n -VectSp_over K) ;
A26: KIJ is linearly-independent by A1, A10, A9, A25, VECTSP_7:1, ZFMISC_1:133;
A27: Line (M,k) in KIJ by ENUMSET1:def 1;
A28: M . k = Line (M,k) by A16, MATRIX_0:52;
M . i <> M . k by A2, A5, A8, A6, A16, A17;
then KIJ \ {LK} = {LI,LJ} by A11, A20, A28, ENUMSET1:86;
hence contradiction by A19, A18, A15, A27, A26, VECTSP_9:14; :: thesis: verum

end;

reconsider LiaLj = li + (a * lj) as Element of the carrier of K * by FINSEQ_1:def 11;
reconsider LL = LiaLj as set ;
set iLL = i .--> LL;
A29: len (li + (a * lj)) = n by CARD_1:def 7;
then RLine (M,i,(li + (a * lj))) = Replace (M,i,LiaLj) by A12, MATRIX11:29
.= M +* (i .--> LL) by A5, A6, FUNCT_7:def 3 ;
then A30: lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) = (M .: ((dom M) \ (dom (i .--> LL)))) \/ (rng (i .--> LL)) by FRECHET:12
.= (M .: ((dom M) \ {i})) \/ (rng (i .--> LL))
.= (M .: ((dom M) \ {i})) \/ {LL} by FUNCOP_1:8
.= ((M .: (dom M)) \ (M .: {i})) \/ {LL} by A2, FUNCT_1:64
.= ((lines M) \ (Im (M,i))) \/ {LL} by RELAT_1:113
.= ((lines M) \ {LI}) \/ {(li + (a * lj))} by A5, A6, A11, FUNCT_1:59 ;
A31: Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),i) = (Line (M,i)) + (a * (Line (M,j))) by A5, A8, A29, A12, MATRIX11:28;

now :: thesis: for x1, x2 being object st x1 in dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) & x2 in dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) & (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . x1 = (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . x2 holds
x1 = x2

A32: len (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) = m by MATRIX_0:def 2;
let x1, x2 be object ; :: thesis: ( x1 in dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) & x2 in dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) & (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . x1 = (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . x2 implies b₁ = b₂ )
assume that
A33: x1 in dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) and
A34: x2 in dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) and
A35: (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . x1 = (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . x2 ; :: thesis: b₁ = b₂
reconsider i1 = x1, i2 = x2 as Element of NAT by A33, A34;
A36: dom (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) = Seg (len (RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))))) by FINSEQ_1:def 3;
then A37: (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . i1 = Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),i1) by A33, A32, MATRIX_0:52;
A38: (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . i2 = Line ((RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))),i2) by A34, A36, A32, MATRIX_0:52;

per cases ( ( i1 = i & i2 = i ) or ( i1 = i & i2 <> i ) or ( i1 <> i & i2 = i ) or ( i1 <> i & i2 <> i ) ) ;

suppose ( i1 = i & i2 = i ) ; :: thesis: b₁ = b₂

hence x1 = x2 ; :: thesis: verum

end;

suppose ( ( i1 = i & i2 <> i ) or ( i1 <> i & i2 = i ) ) ; :: thesis: b₁ = b₂

hence x1 = x2 by A14, A31, A33, A34, A35, A36, A32, A37, A38; :: thesis: verum

end;

suppose A39: ( i1 <> i & i2 <> i ) ; :: thesis: b₁ = b₂

then A40: (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . i2 = Line (M,i2) by A34, A36, A32, A38, MATRIX11:28;
A41: Line (M,i1) = M . i1 by A33, A36, A32, MATRIX_0:52;
A42: Line (M,i2) = M . i2 by A34, A36, A32, MATRIX_0:52;
(RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) . i1 = Line (M,i1) by A33, A36, A32, A37, A39, MATRIX11:28;
hence x1 = x2 by A2, A8, A6, A33, A34, A35, A36, A32, A41, A40, A42; :: thesis: verum

end;

end;

end;

hence RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line ; :: thesis: lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent
A43: a * lj = a * LJ by Th102;
((lines M) \ {LI}) \/ {(LI + (a * LJ))} is linearly-independent by A1, A7, A11, A13, A10, A9, Th115;
hence lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent by A43, A30, Th102; :: thesis: verum

end;

end;