let n, m 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 13;
A6: dom M = Seg (len M) by FINSEQ_1:def 3;
then A7: M . i <> M . j by A2, A3, A4, A5, FUNCT_1:def 8;
A8: len M = m by MATRIX_1:def 3;
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_2:10;
m <> 0 by A5, A8;
then A12: n = width M by Th1;
A13: M . j = Line M,j by A3, A8, MATRIX_2:10;
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) by VECTSP_1:def 29 ;
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:38;
then A21: {LI,LJ} is linearly-independent by A1, VECTSP_7:2;
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:35
.= lj + ((- li) + (- (a * lj))) by FVSUM_1:40
.= lj + (((- (1_ K)) * li) + (- (a * lj))) by FVSUM_1:72
.= lj + (((- (1_ K)) * li) + ((- (1_ K)) * (a * lj))) by FVSUM_1:72
.= lj + (((- (1_ K)) * li) + (((- (1_ K)) * a) * lj)) by FVSUM_1:67
.= lj + ((((- (1_ K)) * a) * lj) + ((- (1_ K)) * li)) by FINSEQOP:34
.= (lj + (((- (1_ K)) * a) * lj)) + ((- (1_ K)) * li) by FINSEQOP:29
.= (((1_ K) * lj) + (((- (1_ K)) * a) * lj)) + ((- (1_ K)) * li) by FVSUM_1:70
.= (((1_ K) + ((- (1_ K)) * a)) * lj) + ((- (1_ K)) * li) by FVSUM_1:68
.= (((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:9;
hence contradiction by VECTSP_1:86; :: 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, JORDAN16:2, VECTSP_7:2;
A27: Line M,k in KIJ by ENUMSET1:def 1;
A28: M . k = Line M,k by A16, MATRIX_2:10;
M . i <> M . k by A2, A5, A8, A6, A16, A17, FUNCT_1:def 8;
then KIJ \ {LK} = {LI,LJ} by A11, A20, A28, ENUMSET1:136;
hence contradiction by A19, A18, A15, A27, A26, VECTSP_9:18; :: 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 FINSEQ_1:def 18;
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)) by FUNCOP_1:19
.= (M .: ((dom M) \ {i})) \/ {LL} by FUNCOP_1:14
.= ((M .: (dom M)) \ (M .: {i})) \/ {LL} by A2, FUNCT_1:123
.= ((lines M) \ (Im M,i)) \/ {LL} by RELAT_1:146
.= ((lines M) \ {LI}) \/ {(li + (a * lj))} by A5, A6, A11, FUNCT_1:117 ;
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

A32: len (RLine M,i,((Line M,i) + (a * (Line M,j)))) = m by MATRIX_1:def 3;
let x1, x2 be set ; :: 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_2:10;
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_2:10;

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_2:10;
A42: Line M,i2 = M . i2 by A34, A36, A32, MATRIX_2:10;
(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, FUNCT_1:def 8; :: thesis: verum

end;

end;

end;

hence RLine M,i,((Line M,i) + (a * (Line M,j))) is without_repeated_line by FUNCT_1:def 8; :: 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;