let n, m be Nat; for K being Field
for M being Matrix of m,n,K st the_rank_of M = m holds
lines M is linearly-independent
let K be Field; for M being Matrix of m,n,K st the_rank_of M = m holds
lines M is linearly-independent
let M be Matrix of m,n,K; ( the_rank_of M = m implies lines M is linearly-independent )
assume A1:
the_rank_of M = m
; lines M is linearly-independent
reconsider N = n as Element of NAT by ORDINAL1:def 13;
set V = n -VectSp_over K;
per cases
( m = 0 or m <> 0 )
;
suppose A2:
m <> 0
;
lines M is linearly-independent then A3:
width M = n
by Th1;
A4:
M is
without_repeated_line
by A1, Th105;
A5:
now set n0 =
n |-> (0. K);
set NULL =
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 not M1 <> 0. K,m,n )assume that A6:
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 A7:
for
j being
Nat st
j in Seg n holds
Sum (Col M1,j) = 0. K
;
not M1 <> 0. K,m,nassume
M1 <> 0. K,
m,
n
;
contradictionthen consider i,
j being
Nat such that A8:
[i,j] in Indices M1
and A9:
M1 * i,
j <> (0. K,m,n) * i,
j
by MATRIX_1:28;
reconsider i =
i,
j =
j as
Element of
NAT by ORDINAL1:def 13;
A10:
len M = m
by MATRIX_1:def 3;
Indices M1 = Indices (0. K,m,n)
by MATRIX_1:27;
then A11:
M1 * i,
j <> 0. K
by A8, A9, MATRIX_3:3;
A12:
Indices M = [:(Seg m),(Seg n):]
by A3, MATRIX_1:26;
Indices M1 = Indices M
by MATRIX_1:27;
then A13:
i in Seg m
by A12, A8, ZFMISC_1:106;
then consider a being
Element of
K such that A14:
Line M1,
i = a * (Line M,i)
by A6;
A15:
width M1 = n
by A2, Th1;
then A16:
j in Seg n
by A8, ZFMISC_1:106;
then A17:
(Line M,i) . j = M * i,
j
by A3, MATRIX_1:def 8;
set R =
RLine M,
i,
(a * (Line M,i));
consider L being
Linear_Combination of
lines M such that A18:
L (#) (MX2FinS M) = M1
by A1, A6, Th105, Th108;
set LM =
L (#) (MX2FinS M);
len M1 = len M
by A18, VECTSP_6:def 8;
then consider f being
Function of
NAT ,the
carrier of
(n -VectSp_over K) such that A19:
Sum (L (#) (MX2FinS M)) = f . m
and A20:
f . 0 = 0. (n -VectSp_over K)
and A21:
for
j being
Element of
NAT for
v being
Vector of
(n -VectSp_over K) st
j < m &
v = (L (#) (MX2FinS M)) . (j + 1) holds
f . (j + 1) = (f . j) + v
by A18, A10, RLVECT_1:def 13;
set RR =
RLine (RLine M,i,(a * (Line M,i))),
i,
(n |-> (0. K));
A22:
len (RLine (RLine M,i,(a * (Line M,i))),i,(n |-> (0. K))) = m
by MATRIX_1:def 3;
defpred S1[
Nat]
means ( $1
< i implies for
t being
Element of
n -tuples_on the
carrier of
K st
t = f . $1 holds
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t)) );
width M =
len (Line M,i)
by MATRIX_1:def 8
.=
len (a * (Line M,i))
by MATRIXR1:16
;
then A23:
width (RLine M,i,(a * (Line M,i))) = width M
by MATRIX11:def 3;
A24:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A25:
S1[
k]
;
S1[k + 1]
reconsider kk =
k as
Element of
NAT by ORDINAL1:def 13;
set k1 =
k + 1;
A26:
1
<= k + 1
by NAT_1:14;
A27:
i <= m
by A13, FINSEQ_1:3;
reconsider LR =
Line (RLine M,i,(a * (Line M,i))),
i,
LM1 =
Line M1,
(k + 1) as
Element of
N -tuples_on the
carrier of
K by A2, Th1;
assume A28:
k + 1
< i
;
for t being Element of n -tuples_on the carrier of K st t = f . (k + 1) holds
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t))
let t be
Element of
n -tuples_on the
carrier of
K;
( t = f . (k + 1) implies the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t)) )
assume A29:
t = f . (k + 1)
;
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t))
reconsider t1 =
f . kk,
T =
t as
Element of
N -tuples_on the
carrier of
K by Th102;
set RR =
RLine (RLine M,i,(a * (Line M,i))),
i,
((Line (RLine M,i,(a * (Line M,i))),i) + t1);
reconsider LRt =
LR + t,
LRt1 =
LR + t1 as
Element of the
carrier of
K * by FINSEQ_1:def 11;
A30:
len (LR + T) = n
by FINSEQ_1:def 18;
A31:
len (LR + t1) = width (RLine M,i,(a * (Line M,i)))
by A3, A23, FINSEQ_1:def 18;
then
width (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t1)) = width (RLine M,i,(a * (Line M,i)))
by MATRIX11:def 3;
then A32:
RLine (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t1)),
i,
(LR + t) =
Replace (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t1)),
i,
LRt
by A3, A23, A30, MATRIX11:29
.=
Replace (Replace (RLine M,i,(a * (Line M,i))),i,LRt1),
i,
LRt
by A31, MATRIX11:29
.=
Replace (RLine M,i,(a * (Line M,i))),
i,
LRt
by FUNCT_7:36
.=
RLine (RLine M,i,(a * (Line M,i))),
i,
(LR + t)
by A3, A23, A30, MATRIX11:29
;
i <= m
by A13, FINSEQ_1:3;
then
k + 1
< m
by A28, XXREAL_0:2;
then A33:
k + 1
in Seg m
by A26;
then A34:
Line M1,
(k + 1) = M1 . (k + 1)
by MATRIX_2:10;
Line M1,
(k + 1) in lines M1
by A33, Th103;
then reconsider LMk1 =
(L (#) (MX2FinS M)) . (k + 1) as
Element of
(n -VectSp_over K) by A18, A33, MATRIX_2:10;
consider a being
Element of
K such that A35:
Line M1,
(k + 1) = a * (Line M,(k + 1))
by A6, A33;
A36:
Line M,
(k + 1) =
Line (RLine M,i,(a * (Line M,i))),
(k + 1)
by A28, A33, MATRIX11:28
.=
Line (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t1)),
(k + 1)
by A28, A33, MATRIX11:28
;
k < i
by A28, NAT_1:13;
then
k < m
by A27, XXREAL_0:2;
then t =
(f . kk) + LMk1
by A21, A29
.=
t1 + (Line M1,(k + 1))
by A15, A18, A34, Th102
;
then A37:
LR + t =
(LR + t1) + LM1
by FINSEQOP:29
.=
(Line (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t1)),i) + (a * (Line (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t1)),(k + 1)))
by A13, A35, A31, A36, MATRIX11:28
;
A38:
len (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t1)) = m
by MATRIX_1:def 3;
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t1))
by A25, A28, NAT_1:13;
hence
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t))
by A28, A33, A38, A32, A37, Th92;
verum
end; defpred S2[
Nat]
means (
i <= $1 & $1
<= m implies for
t being
Element of
n -tuples_on the
carrier of
K st
t = f . $1 holds
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,t) );
A39:
S1[
0 ]
proof
assume
0 < i
;
for t being Element of n -tuples_on the carrier of K st t = f . 0 holds
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t))
let t be
Element of
n -tuples_on the
carrier of
K;
( t = f . 0 implies the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t)) )
assume
t = f . 0
;
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t))
then
t = n |-> (0. K)
by A20, Th102;
then
(Line (RLine M,i,(a * (Line M,i))),i) + t = Line (RLine M,i,(a * (Line M,i))),
i
by A3, A23, FVSUM_1:28;
hence
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,((Line (RLine M,i,(a * (Line M,i))),i) + t))
by MATRIX11:30;
verum
end; A40:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A39, A24);
A41:
for
k being
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A42:
S2[
k]
;
S2[k + 1]
reconsider kk =
k as
Element of
NAT by ORDINAL1:def 13;
reconsider t1 =
f . kk as
Element of
N -tuples_on the
carrier of
K by Th102;
set k1 =
k + 1;
reconsider LR =
Line (RLine M,i,(a * (Line M,i))),
i,
LM1 =
Line M1,
(k + 1) as
Element of
n -tuples_on the
carrier of
K by A2, Th1;
assume that A43:
i <= k + 1
and A44:
k + 1
<= m
;
for t being Element of n -tuples_on the carrier of K st t = f . (k + 1) holds
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,t)
A45:
k < m
by A44, NAT_1:13;
1
<= k + 1
by NAT_1:14;
then A46:
k + 1
in Seg m
by A44;
then A47:
Line M1,
(k + 1) = M1 . (k + 1)
by MATRIX_2:10;
Line M1,
(k + 1) in lines M1
by A46, Th103;
then reconsider LMk1 =
(L (#) (MX2FinS M)) . (k + 1) as
Element of
(n -VectSp_over K) by A18, A46, MATRIX_2:10;
let t be
Element of
n -tuples_on the
carrier of
K;
( t = f . (k + 1) implies the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,t) )
assume
t = f . (k + 1)
;
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,t)
then A48:
t =
(f . kk) + LMk1
by A21, A45
.=
t1 + LM1
by A18, A47, Th102
;
consider b being
Element of
K such that A49:
Line M1,
(k + 1) = b * (Line M,(k + 1))
by A6, A46;
reconsider T =
t,
T1 =
t1 as
Element of the
carrier of
K * by FINSEQ_1:def 11;
per cases
( i = k + 1 or i < k + 1 )
by A43, XXREAL_0:1;
suppose A50:
i = k + 1
;
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,t)
len LM1 = n
by FINSEQ_1:def 18;
then
LR = LM1
by A3, A14, A46, A50, MATRIX11:28;
then A51:
LR + t1 = t
by A48, FINSEQOP:34;
k < i
by A50, NAT_1:13;
hence
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,t)
by A40, A51;
verum end; suppose A52:
i < k + 1
;
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,t)set RR =
RLine (RLine M,i,(a * (Line M,i))),
i,
t1;
A53:
len t1 = width (RLine M,i,(a * (Line M,i)))
by A3, A23, FINSEQ_1:def 18;
then
Line (RLine (RLine M,i,(a * (Line M,i))),i,t1),
i = t1
by A13, MATRIX11:28;
then A54:
t =
(Line (RLine (RLine M,i,(a * (Line M,i))),i,t1),i) + (b * (Line (RLine M,i,(a * (Line M,i))),(k + 1)))
by A46, A49, A48, A52, MATRIX11:28
.=
(Line (RLine (RLine M,i,(a * (Line M,i))),i,t1),i) + (b * (Line (RLine (RLine M,i,(a * (Line M,i))),i,t1),(k + 1)))
by A46, A52, MATRIX11:28
;
A55:
len t = n
by FINSEQ_1:def 18;
width (RLine (RLine M,i,(a * (Line M,i))),i,t1) = width (RLine M,i,(a * (Line M,i)))
by A53, MATRIX11:def 3;
then A56:
RLine (RLine (RLine M,i,(a * (Line M,i))),i,t1),
i,
t =
Replace (RLine (RLine M,i,(a * (Line M,i))),i,t1),
i,
T
by A3, A23, A55, MATRIX11:29
.=
Replace (Replace (RLine M,i,(a * (Line M,i))),i,T1),
i,
T
by A53, MATRIX11:29
.=
Replace (RLine M,i,(a * (Line M,i))),
i,
T
by FUNCT_7:36
.=
RLine (RLine M,i,(a * (Line M,i))),
i,
t
by A3, A23, A55, MATRIX11:29
;
A57:
len (RLine (RLine M,i,(a * (Line M,i))),i,t1) = m
by MATRIX_1:def 3;
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,t1)
by A42, A44, A52, NAT_1:13;
hence
the_rank_of (RLine M,i,(a * (Line M,i))) = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,t)
by A46, A52, A54, A56, A57, Th92;
verum end;
end; A58:
S2[
0 ]
by A13;
A59:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A58, A41);
reconsider SumLM =
Sum (L (#) (MX2FinS M)) as
Element of
n -tuples_on the
carrier of
K by Th102;
A60:
now let j be
Nat;
( 1 <= j & j <= n implies SumLM . j = (n |-> (0. K)) . j )assume that A61:
1
<= j
and A62:
j <= n
;
SumLM . j = (n |-> (0. K)) . j
j in NAT
by ORDINAL1:def 13;
then A63:
j in Seg n
by A61, A62;
A64:
Carrier L c= lines M
by VECTSP_6:def 7;
M1 = FinS2MX (L (#) (MX2FinS M))
by A18;
then Sum (Col M1,j) =
(Sum L) . j
by A1, A63, A64, Th105, Th107
.=
SumLM . j
by A4, A64, VECTSP_9:7
;
hence SumLM . j =
0. K
by A7, A63
.=
(n |-> (0. K)) . j
by A63, FINSEQ_2:71
;
verum end;
dom (RLine (RLine M,i,(a * (Line M,i))),i,(n |-> (0. K))) = Seg (len (RLine (RLine M,i,(a * (Line M,i))),i,(n |-> (0. K))))
by FINSEQ_1:def 3;
then consider k being
Nat such that A65:
m = k + 1
and A66:
len (Del (RLine (RLine M,i,(a * (Line M,i))),i,(n |-> (0. K))),i) = k
by A13, A22, FINSEQ_3:113;
A67:
len SumLM = n
by FINSEQ_1:def 18;
M1 * i,
j =
(Line M1,i) . j
by A15, A16, MATRIX_1:def 8
.=
a * (M * i,j)
by A3, A16, A14, A17, FVSUM_1:63
;
then
a <> 0. K
by A11, VECTSP_1:44;
then A68:
m = the_rank_of (RLine M,i,(a * (Line M,i)))
by A1, Th89;
A69:
len (n |-> (0. K)) = n
by FINSEQ_1:def 18;
then A70:
width (RLine (RLine M,i,(a * (Line M,i))),i,(n |-> (0. K))) = width (RLine M,i,(a * (Line M,i)))
by A3, A23, MATRIX11:def 3;
A71:
Line (RLine (RLine M,i,(a * (Line M,i))),i,(n |-> (0. K))),
i = n |-> (0. K)
by A3, A13, A23, A69, MATRIX11:28;
i <= m
by A13, FINSEQ_1:3;
then
m = the_rank_of (RLine (RLine M,i,(a * (Line M,i))),i,(n |-> (0. K)))
by A68, A19, A59, A67, A69, A60, FINSEQ_1:18;
then
m = the_rank_of (DelLine (RLine (RLine M,i,(a * (Line M,i))),i,(n |-> (0. K))),i)
by A3, A23, A71, A70, Th90;
then
m <= k
by A66, Th74;
hence
contradiction
by A65, NAT_1:13;
verum end; now A72:
len M = m
by MATRIX_1:def 3;
A73:
dom M = Seg (len M)
by FINSEQ_1:def 3;
let i be
Nat;
( i in Seg m implies not Line M,i = n |-> (0. K) )assume
i in Seg m
;
not Line M,i = n |-> (0. K)then consider k being
Nat such that A74:
m = k + 1
and A75:
len (Del M,i) = k
by A73, A72, FINSEQ_3:113;
assume
Line M,
i = n |-> (0. K)
;
contradictionthen
the_rank_of (DelLine M,i) = m
by A1, A3, Th90;
then
m <= k
by A75, Th74;
hence
contradiction
by A74, NAT_1:13;
verum end; hence
lines M is
linearly-independent
by A4, A5, Th109;
verum end;