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