let m, n be Nat; 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; 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; ( 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
; ( ( ( 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 )
( 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)
;
lines M is linearly-independent
let L be
Linear_Combination of
lines M;
VECTSP_7:def 1 ( not Sum L = 0. (n -VectSp_over K) or Carrier L = {} )
assume A5:
Sum L = 0. (n -VectSp_over K)
;
Carrier L = {}
set LM =
L (#) (MX2FinS M);
set FLM =
FinS2MX (L (#) (MX2FinS M));
A6:
len (L (#) (MX2FinS M)) = len (MX2FinS M)
by VECTSP_6:def 5;
A7:
len M = m
by MATRIX_0:def 2;
then reconsider flm =
FinS2MX (L (#) (MX2FinS M)) as
Matrix of
m,
n,
K by A6;
A8:
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;
( i in Seg m implies ex a being Element of K st Line (flm,i) = a * (Line (M,i)) )
assume A9:
i in Seg m
;
ex a being Element of K st Line (flm,i) = a * (Line (M,i))
Line (
M,
i)
in lines M
by A9, 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 A9, MATRIX_0:52;
then
Line (
flm,
i)
= LLM * (Line (M,i))
by A7, A9, Th106;
hence
ex
a being
Element of
K st
Line (
flm,
i)
= a * (Line (M,i))
;
verum
end;
A10:
len (n |-> (0. K)) = n
by CARD_1:def 7;
assume
Carrier L <> {}
;
contradiction
then consider x being
object such that A11:
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 A12:
i in Seg m
and A13:
x = Line (
M,
i)
by A11, Th103;
consider v being
Vector of
(n -VectSp_over K) such that A14:
x = v
and A15:
L . v <> 0. K
by A11, VECTSP_6:1;
reconsider LM =
Line (
M,
i) as
Element of
n -tuples_on the
carrier of
K by A13, A14, Th102;
Line (
M,
i)
= M . i
by A12, MATRIX_0:52;
then A16:
Line (
flm,
i)
= (L . v) * LM
by A7, A12, A13, A14, Th106;
then
flm = 0. (
K,
m,
n)
by A4, A8;
then A19:
flm . i = n |-> (0. K)
by A12, FUNCOP_1:7;
A20:
dom LM = Seg n
by FINSEQ_2:124;
len LM = n
by CARD_1:def 7;
then consider j being
Nat such that A21:
1
<= j
and A22:
j <= n
and A23:
LM . j <> (n |-> (0. K)) . j
by A3, A12, A10, FINSEQ_1:14;
A24:
j in Seg n
by A21, A22;
then A25:
LM . j <> 0. K
by A23, FINSEQ_2:57;
j in Seg n
by A21, A22;
then A26:
LM . j in rng LM
by A20, 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;
A27:
((L . v) * LM) . j = (L . v) * LMj
by A24, FVSUM_1:51;
flm . i = Line (
flm,
i)
by A12, MATRIX_0:52;
then
(Line (flm,i)) . j = 0. K
by A19, A24, FINSEQ_2:57;
hence
contradiction
by A15, A25, A27, A16, VECTSP_1:12;
verum
end;
assume A28:
lines M is linearly-independent
; ( ( 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) ) )
let M1 be Matrix of m,n,K; ( ( 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
; 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;
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
.=
0. (n -VectSp_over K)
by Th102
;
then A37:
Carrier L = {}
by A28;
assume
M1 <> 0. (K,m,n)
; 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_0:27;
[I,J] in Indices (0. (K,m,n))
by A38, MATRIX_0: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_0: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_0: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_0:52;
A44:
jj in Seg (width M)
by A38, A41, ZFMISC_1:87;
then A45:
(Line (M,ii)) . jj = M * (ii,jj)
by MATRIX_0: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_0: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;
hence
contradiction
by A37, VECTSP_6:1; verum