let m, n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: ( the_rank_of M = m implies lines M is linearly-independent )
assume A1: the_rank_of M = m ; :: thesis: lines M is linearly-independent
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set V = n -VectSp_over K;
per cases ( m = 0 or m <> 0 ) ;
suppose m = 0 ; :: thesis: lines M is linearly-independent
then len M = 0 by MATRIX_0:def 2;
then M = {} ;
hence lines M is linearly-independent ; :: thesis: verum
end;
suppose A2: m <> 0 ; :: thesis: lines M is linearly-independent
then A3: width M = n by Th1;
A4: M is without_repeated_line by A1, Th105;
A5: now :: 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
not M1 <> 0. (K,m,n)
set n0 = n |-> (0. K);
set NULL = 0. (K,m,n);
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 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 ; :: thesis: not M1 <> 0. (K,m,n)
assume M1 <> 0. (K,m,n) ; :: thesis: contradiction
then 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_0:27;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 12;
A10: len M = m by MATRIX_0:def 2;
Indices M1 = Indices (0. (K,m,n)) by MATRIX_0:26;
then A11: M1 * (i,j) <> 0. K by A8, A9, MATRIX_3:1;
A12: Indices M = [:(Seg m),(Seg n):] by A3, MATRIX_0:25;
Indices M1 = Indices M by MATRIX_0:26;
then A13: i in Seg m by A12, A8, ZFMISC_1:87;
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:87;
then A17: (Line (M,i)) . j = M * (i,j) by A3, MATRIX_0:def 7;
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 5;
then consider f being sequence of 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 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 12;
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_0:def 2;
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_0:def 7
.= 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; :: thesis: ( S1[k] implies S1[k + 1] )
assume A25: S1[k] ; :: thesis: S1[k + 1]
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
set k1 = k + 1;
A26: 1 <= k + 1 by NAT_1:14;
A27: i <= m by A13, FINSEQ_1: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 A28: k + 1 < i ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 CARD_1:def 7;
A31: len (LR + t1) = width (RLine (M,i,(a * (Line (M,i))))) by A3, A23, CARD_1:def 7;
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:34
.= RLine ((RLine (M,i,(a * (Line (M,i))))),i,(LR + t)) by A3, A23, A30, MATRIX11:29 ;
i <= m by A13, FINSEQ_1:1;
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_0:52;
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_0:52;
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:28
.= (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_0:def 2;
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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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:21;
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; :: thesis: 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; :: thesis: ( S2[k] implies S2[k + 1] )
assume A42: S2[k] ; :: thesis: S2[k + 1]
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
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 ; :: thesis: 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_0:52;
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_0:52;
let t be Element of n -tuples_on the carrier of K; :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: 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 CARD_1:def 7;
then LR = LM1 by A3, A14, A46, A50, MATRIX11:28;
then A51: LR + t1 = t by A48, FINSEQOP:33;
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; :: thesis: verum
end;
suppose A52: i < k + 1 ; :: thesis: 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, CARD_1:def 7;
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 CARD_1:def 7;
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:34
.= 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_0:def 2;
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; :: thesis: verum
end;
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 :: thesis: for j being Nat st 1 <= j & j <= n holds
SumLM . j = (n |-> (0. K)) . j
let j be Nat; :: thesis: ( 1 <= j & j <= n implies SumLM . j = (n |-> (0. K)) . j )
assume that
A61: 1 <= j and
A62: j <= n ; :: thesis: SumLM . j = (n |-> (0. K)) . j
A63: j in Seg n by A61, A62;
A64: Carrier L c= lines M by VECTSP_6:def 4;
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:3 ;
hence SumLM . j = 0. K by A7, A63
.= (n |-> (0. K)) . j by A63, FINSEQ_2:57 ;
:: thesis: 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:104;
A67: len SumLM = n by CARD_1:def 7;
M1 * (i,j) = (Line (M1,i)) . j by A15, A16, MATRIX_0:def 7
.= a * (M * (i,j)) by A3, A16, A14, A17, FVSUM_1:51 ;
then a <> 0. K by A11;
then A68: m = the_rank_of (RLine (M,i,(a * (Line (M,i))))) by A1, Th89;
A69: len (n |-> (0. K)) = n by CARD_1:def 7;
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:1;
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:14;
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; :: thesis: verum
end;
now :: thesis: for i being Nat st i in Seg m holds
not Line (M,i) = n |-> (0. K)
A72: len M = m by MATRIX_0:def 2;
A73: dom M = Seg (len M) by FINSEQ_1:def 3;
let i be Nat; :: thesis: ( i in Seg m implies not Line (M,i) = n |-> (0. K) )
assume i in Seg m ; :: thesis: 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:104;
assume Line (M,i) = n |-> (0. K) ; :: thesis: contradiction
then the_rank_of (DelLine (M,i)) = m by A1, A3, Th90;
then m <= k by A75, Th74;
hence contradiction by A74, NAT_1:13; :: thesis: verum
end;
hence lines M is linearly-independent by A4, A5, Th109; :: thesis: verum
end;
end;