let n, m be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K st M is without_repeated_line holds
( ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) ) iff lines M is linearly-independent )
let K be Field; :: thesis: for M being Matrix of m,n,K st M is without_repeated_line holds
( ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) ) iff lines M is linearly-independent )
set V = n -VectSp_over K;
set n0 = n |-> (0. K);
A1: len (n |-> (0. K)) = n by CARD_1:def 7;
let M be Matrix of m,n,K; :: thesis: ( M is without_repeated_line implies ( ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) ) iff lines M is linearly-independent ) )
assume A2: M is without_repeated_line ; :: thesis: ( ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) ) iff lines M is linearly-independent )
thus ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) implies lines M is linearly-independent ) :: thesis: ( lines M is linearly-independent implies ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) ) )

proof

set MX = MX2FinS M;
set V = n -VectSp_over K;
assume that
A3: for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) and
A4: for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ; :: thesis: lines M is linearly-independent
let L be Linear_Combination of lines M; :: according to VECTSP_7:def 1 :: thesis: ( not Sum L = 0. (n -VectSp_over K) or Carrier L = {} )
assume A5: Sum L = 0. (n -VectSp_over K) ; :: thesis: Carrier L = {}
set LM = L (#) (MX2FinS M);
set FLM = FinS2MX (L (#) (MX2FinS M));
A6: len M = m by MATRIX_1:def 2;
then reconsider flm = FinS2MX (L (#) (MX2FinS M)) as Matrix of m,n,K by VECTSP_6:def 5;
A7: for i being Nat st i in Seg m holds
ex a being Element of K st Line (flm,i) = a * (Line (M,i))

proof

let i be Nat; :: thesis: ( i in Seg m implies ex a being Element of K st Line (flm,i) = a * (Line (M,i)) )
assume A8: i in Seg m ; :: thesis: ex a being Element of K st Line (flm,i) = a * (Line (M,i))
Line (M,i) in lines M by A8, Th103;
then reconsider LM = Line (M,i) as Element of (n -VectSp_over K) ;
reconsider LLM = L . LM as Element of K ;
Line (M,i) = M . i by A8, MATRIX_2:8;
then Line (flm,i) = LLM * (Line (M,i)) by A6, A8, Th106;
hence ex a being Element of K st Line (flm,i) = a * (Line (M,i)) ; :: thesis: verum

end;

A9: len (n |-> (0. K)) = n by CARD_1:def 7;
assume Carrier L <> {} ; :: thesis: contradiction
then consider x being set such that
A10: x in Carrier L by XBOOLE_0:def 1;
Carrier L c= lines M by VECTSP_6:def 4;
then consider i being Nat such that
A11: i in Seg m and
A12: x = Line (M,i) by A10, Th103;
consider v being Vector of (n -VectSp_over K) such that
A13: x = v and
A14: L . v <> 0. K by A10, VECTSP_6:1;
reconsider LM = Line (M,i) as Element of n -tuples_on the carrier of K by A12, A13, Th102;
Line (M,i) = M . i by A11, MATRIX_2:8;
then A15: Line (flm,i) = (L . v) * LM by A6, A11, A12, A13, Th106;

now

let j be Nat; :: thesis: ( j in Seg n implies Sum (Col (flm,j)) = 0. K )
assume A16: j in Seg n ; :: thesis: Sum (Col (flm,j)) = 0. K
A17: (n |-> (0. K)) . j = 0. K by A16, FINSEQ_2:57;
Carrier L c= lines M by VECTSP_6:def 4;
then (Sum L) . j = Sum (Col (flm,j)) by A2, A16, Th107;
hence Sum (Col (flm,j)) = 0. K by A5, A17, Th102; :: thesis: verum

end;

then flm = 0. (K,m,n) by A4, A7;
then A18: flm . i = n |-> (0. K) by A11, FUNCOP_1:7;
A19: dom LM = Seg n by FINSEQ_2:124;
len LM = n by CARD_1:def 7;
then consider j being Nat such that
A20: 1 <= j and
A21: j <= n and
A22: LM . j <> (n |-> (0. K)) . j by A3, A11, A9, FINSEQ_1:14;
A23: j in NAT by ORDINAL1:def 12;
then A24: j in Seg n by A20, A21;
then A25: LM . j <> 0. K by A22, FINSEQ_2:57;
j in Seg n by A20, A21, A23;
then A26: LM . j in rng LM by A19, FUNCT_1:def 3;
rng LM c= the carrier of K by RELAT_1:def 19;
then reconsider LMj = LM . j as Element of K by A26;
n in NAT by ORDINAL1:def 12;
then A27: ((L . v) * LM) . j = (L . v) * LMj by A24, FVSUM_1:51;
flm . i = Line (flm,i) by A11, MATRIX_2:8;
then (Line (flm,i)) . j = 0. K by A18, A24, FINSEQ_2:57;
hence contradiction by A14, A25, A27, A15, VECTSP_1:12; :: thesis: verum

end;

assume A28: lines M is linearly-independent ; :: thesis: ( ( for i being Nat st i in Seg m holds
Line (M,i) <> n |-> (0. K) ) & ( for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n) ) )

hereby :: thesis: for M1 being Matrix of m,n,K st ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) holds
M1 = 0. (K,m,n)

let i be Nat; :: thesis: ( i in Seg m implies Line (M,i) <> n |-> (0. K) )
assume i in Seg m ; :: thesis: Line (M,i) <> n |-> (0. K)
then Line (M,i) in lines M by Th103;
then Line (M,i) <> 0. (n -VectSp_over K) by A28, VECTSP_7:2;
hence Line (M,i) <> n |-> (0. K) by Th102; :: thesis: verum

end;

let M1 be Matrix of m,n,K; :: thesis: ( ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) & ( for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ) implies M1 = 0. (K,m,n) )
assume that
A29: for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) and
A30: for j being Nat st j in Seg n holds
Sum (Col (M1,j)) = 0. K ; :: thesis: M1 = 0. (K,m,n)
consider L being Linear_Combination of lines M such that
A31: L (#) (MX2FinS M) = M1 by A2, A29, Th108;
A32: Carrier L c= lines M by VECTSP_6:def 4;

A33: now

let j be Nat; :: thesis: ( 1 <= j & j <= n implies (Sum L) . j = (n |-> (0. K)) . j )
assume that
A34: 1 <= j and
A35: j <= n ; :: thesis: (Sum L) . j = (n |-> (0. K)) . j
j in NAT by ORDINAL1:def 12;
then A36: j in Seg n by A34, A35;
hence (Sum L) . j = Sum (Col ((FinS2MX (L (#) (MX2FinS M))),j)) by A2, A32, Th107
.= 0. K by A30, A31, A36
.= (n |-> (0. K)) . j by A36, FINSEQ_2:57 ;
:: thesis: verum

end;

reconsider SumL = Sum L as Element of n -tuples_on the carrier of K by Th102;
len SumL = n by CARD_1:def 7;
then SumL = n |-> (0. K) by A1, A33, FINSEQ_1:14
.= 0. (n -VectSp_over K) by Th102 ;
then A37: Carrier L = {} by A28, VECTSP_7:def 1;
assume M1 <> 0. (K,m,n) ; :: thesis: contradiction
then consider I, J being Nat such that
A38: [I,J] in Indices M1 and
A39: M1 * (I,J) <> (0. (K,m,n)) * (I,J) by MATRIX_1:27;
[I,J] in Indices (0. (K,m,n)) by A38, MATRIX_1:26;
then A40: M1 * (I,J) <> 0. K by A39, MATRIX_3:1;
reconsider ii = I, jj = J as Element of NAT by ORDINAL1:def 12;
A41: Indices M1 = Indices M by MATRIX_1:26;
then Indices M1 = [:(Seg (len M)),(Seg (width M)):] by FINSEQ_1:def 3;
then A42: ii in Seg (len M) by A38, ZFMISC_1:87;
A43: len M = m by MATRIX_1:def 2;
then Line (M,ii) in lines M by A42, Th103;
then reconsider Mii = M . ii as Element of (n -VectSp_over K) by A42, A43, MATRIX_2:8;
A44: jj in Seg (width M) by A38, A41, ZFMISC_1:87;
then A45: (Line (M,ii)) . jj = M * (ii,jj) by MATRIX_1:def 7;
jj in Seg (width M1) by A38, ZFMISC_1:87;
then M1 * (I,J) = (Line ((FinS2MX (L (#) (MX2FinS M))),ii)) . jj by A31, MATRIX_1:def 7
.= ((L . Mii) * (Line (M,ii))) . jj by A42, Th106
.= (L . Mii) * (M * (ii,jj)) by A44, A45, FVSUM_1:51 ;
then L . Mii <> 0. K by A40, VECTSP_1:12;
hence contradiction by A37, VECTSP_6:1; :: thesis: verum