let m, n be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
let K be Field; :: thesis: for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
defpred S₁[ Nat] means for m, n being Nat st m = $1 holds
for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m );
A1: S₁[ 0 ]

proof

let m, n be Nat; :: thesis: ( m = 0 implies for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m ) )
assume A2: m = 0 ; :: thesis: for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
let M be Matrix of m,n,K; :: thesis: ( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
len M = 0 by A2, MATRIX_1:def 3;
then ( M = {} & the_rank_of M <= 0 ) by Th74;
then ( lines M = {} the carrier of (n -VectSp_over K) & the_rank_of M = 0 & M = {} ) ;
hence ( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m ) by A2; :: thesis: verum

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let m, n be Nat; :: thesis: ( m = k + 1 implies for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m ) )
assume A5: m = k + 1 ; :: thesis: for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
let M be Matrix of m,n,K; :: thesis: ( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m )
thus ( lines M is linearly-independent & M is without_repeated_line implies the_rank_of M = m ) :: thesis: ( the_rank_of M = m implies ( lines M is linearly-independent & M is without_repeated_line ) )

proof

assume that
A6: lines M is linearly-independent and
A7: M is without_repeated_line ; :: thesis: the_rank_of M = m
A8: ( m in Seg m & len M = m ) by A5, FINSEQ_1:6, MATRIX_1:def 3;
then Line M,m in lines M by Th103;
then reconsider LM = Line M,m as Element of n -tuples_on the carrier of K by Th102;
A9: ( LM <> n |-> (0. K) & len LM = n & len (n |-> (0. K)) = n ) by A6, A7, A8, Th109, FINSEQ_1:def 18;
then consider i being Nat such that
A10: ( 1 <= i & i <= n & LM . i <> (n |-> (0. K)) . i ) by FINSEQ_1:18;
i in NAT by ORDINAL1:def 13;
then A11: ( i in Seg n & len (Line M,m) = width M ) by A10, MATRIX_1:def 8;
then A12: ( LM . i <> 0. K & LM . i = M * m,i ) by A9, A10, FINSEQ_2:71, MATRIX_1:def 8;
defpred S₂[ Nat] means ( $1 < m implies ex M1 being Matrix of m,n,K st
( Line M1,m = Line M,m & lines M1 is linearly-independent & M1 is without_repeated_line & the_rank_of M1 = the_rank_of M & ( for j being Nat st j <= $1 & j in Seg m holds
M1 * j,i = 0. K ) ) );
A13: S₂[ 0 ]

proof

assume 0 < m ; :: thesis: ex M1 being Matrix of m,n,K st
( Line M1,m = Line M,m & lines M1 is linearly-independent & M1 is without_repeated_line & the_rank_of M1 = the_rank_of M & ( for j being Nat st j <= 0 & j in Seg m holds
M1 * j,i = 0. K ) )
take M ; :: thesis: ( Line M,m = Line M,m & lines M is linearly-independent & M is without_repeated_line & the_rank_of M = the_rank_of M & ( for j being Nat st j <= 0 & j in Seg m holds
M * j,i = 0. K ) )
thus ( Line M,m = Line M,m & lines M is linearly-independent & M is without_repeated_line & the_rank_of M = the_rank_of M & ( for j being Nat st j <= 0 & j in Seg m holds
M * j,i = 0. K ) ) by A6, A7; :: thesis: verum

end;

A14: for l being Nat st S₂[l] holds
S₂[l + 1]

proof

let L be Nat; :: thesis: ( S₂[L] implies S₂[L + 1] )
assume A15: S₂[L] ; :: thesis: S₂[L + 1]
set L1 = L + 1;
assume A16: L + 1 < m ; :: thesis: ex M1 being Matrix of m,n,K st
( Line M1,m = Line M,m & lines M1 is linearly-independent & M1 is without_repeated_line & the_rank_of M1 = the_rank_of M & ( for j being Nat st j <= L + 1 & j in Seg m holds
M1 * j,i = 0. K ) )
then consider M1 being Matrix of m,n,K such that
A17: ( Line M1,m = Line M,m & lines M1 is linearly-independent ) and
A18: ( M1 is without_repeated_line & the_rank_of M1 = the_rank_of M ) and
A19: for j being Nat st j <= L & j in Seg m holds
M1 * j,i = 0. K by A15, NAT_1:13;
set Mmi = M * m,i;
set MLi = M1 * (L + 1),i;
0 + 1 <= L + 1 by NAT_1:13;
then A20: L + 1 in Seg m by A16;
take R = RLine M1,(L + 1),((Line M1,(L + 1)) + ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (Line M1,m))); :: thesis: ( Line R,m = Line M,m & lines R is linearly-independent & R is without_repeated_line & the_rank_of R = the_rank_of M & ( for j being Nat st j <= L + 1 & j in Seg m holds
R * j,i = 0. K ) )
len M1 = m by MATRIX_1:def 3;
hence ( Line R,m = Line M,m & lines R is linearly-independent & R is without_repeated_line & the_rank_of R = the_rank_of M ) by A8, A16, A17, A18, Th92, Th117, MATRIX11:28; :: thesis: for j being Nat st j <= L + 1 & j in Seg m holds
R * j,i = 0. K
let j be Nat; :: thesis: ( j <= L + 1 & j in Seg m implies R * j,i = 0. K )
assume A21: ( j <= L + 1 & j in Seg m ) ; :: thesis: R * j,i = 0. K
set LML = Line M1,(L + 1);
set LMm = Line M1,m;
A22: ( width R = n & width M1 = n & width M = n ) by A21, Th1, FINSEQ_1:4;
then A23: ( (Line M1,(L + 1)) . i = M1 * (L + 1),i & (Line M1,m) . i = M * m,i ) by A11, A17, MATRIX_1:def 8;
then A24: ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (Line M1,m)) . i = (- (((M * m,i) " ) * (M1 * (L + 1),i))) * (M * m,i) by A11, A22, FVSUM_1:63;
len ((Line M1,(L + 1)) + ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (Line M1,m))) = width M1 by FINSEQ_1:def 18;
then Line R,(L + 1) = (Line M1,(L + 1)) + ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (Line M1,m)) by A20, MATRIX11:28;
then A25: (Line R,(L + 1)) . i = (M1 * (L + 1),i) + ((- (((M * m,i) " ) * (M1 * (L + 1),i))) * (M * m,i)) by A11, A22, A23, A24, FVSUM_1:22
.= (M1 * (L + 1),i) + ((- ((1_ K) * (((M * m,i) " ) * (M1 * (L + 1),i)))) * (M * m,i)) by VECTSP_1:def 13
.= (M1 * (L + 1),i) + (((- (1_ K)) * (((M * m,i) " ) * (M1 * (L + 1),i))) * (M * m,i)) by VECTSP_1:41
.= (M1 * (L + 1),i) + ((- (1_ K)) * ((((M * m,i) " ) * (M1 * (L + 1),i)) * (M * m,i))) by GROUP_1:def 4
.= (M1 * (L + 1),i) + ((- (1_ K)) * ((((M * m,i) " ) * (M * m,i)) * (M1 * (L + 1),i))) by GROUP_1:def 4
.= (M1 * (L + 1),i) + ((- (1_ K)) * ((1_ K) * (M1 * (L + 1),i))) by A12, VECTSP_1:def 22
.= (M1 * (L + 1),i) + ((- (1_ K)) * (M1 * (L + 1),i)) by VECTSP_1:def 13
.= (M1 * (L + 1),i) + (- ((1_ K) * (M1 * (L + 1),i))) by VECTSP_1:41
.= (M1 * (L + 1),i) + (- (M1 * (L + 1),i)) by VECTSP_1:def 13
.= 0. K by RLVECT_1:16 ;

per cases ( j = L + 1 or j <= L ) by A21, NAT_1:9;

suppose j = L + 1 ; :: thesis: R * j,i = 0. K

hence R * j,i = 0. K by A11, A22, A25, MATRIX_1:def 8; :: thesis: verum

end;

suppose A26: j <= L ; :: thesis: R * j,i = 0. K

then A27: j < L + 1 by NAT_1:13;
thus 0. K = M1 * j,i by A19, A21, A26
.= (Line M1,j) . i by A11, A22, MATRIX_1:def 8
.= (Line R,j) . i by A21, A27, MATRIX11:28
.= R * j,i by A11, A22, MATRIX_1:def 8 ; :: thesis: verum

end;

end;

end;

A28: for l being Nat holds S₂[l] from NAT_1:sch 2(A13, A14);
k < m by A5, NAT_1:13;
then consider M1 being Matrix of m,n,K such that
A29: ( Line M1,m = Line M,m & lines M1 is linearly-independent ) and
A30: ( M1 is without_repeated_line & the_rank_of M1 = the_rank_of M ) and
A31: for j being Nat st j <= k & j in Seg m holds
M1 * j,i = 0. K by A28;
set S = Segm M1,(Seg k),(Seg n);
k < m by A5, NAT_1:13;
then A32: Seg k c= Seg m by FINSEQ_1:7;
then A33: ( lines (Segm M1,(Seg k),(Seg n)) is linearly-independent & Segm M1,(Seg k),(Seg n) is without_repeated_line ) by A29, A30, Th119, Th120;
A34: ( card (Seg k) = k & card (Seg n) = n ) by FINSEQ_1:78;
then A35: len (Segm M1,(Seg k),(Seg n)) = k by MATRIX_1:def 3;
set SwS = Seg (width (Segm M1,(Seg k),(Seg n)));
set SSS = Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i});

now

let j be Nat; :: thesis: ( j in Seg k implies (Segm M1,(Seg k),(Seg n)) * j,i = 0. K )
assume A36: j in Seg k ; :: thesis: (Segm M1,(Seg k),(Seg n)) * j,i = 0. K
A37: (Sgm (Seg k)) . j = (idseq k) . j by FINSEQ_3:54
.= j by A36, FINSEQ_2:57 ;
A38: (Sgm (Seg n)) . i = (idseq n) . i by FINSEQ_3:54
.= i by A11, FINSEQ_2:57 ;
A39: ( j <= k & j in Seg m ) by A32, A36, FINSEQ_1:3;
width (Segm M1,(Seg k),(Seg n)) = n by A34, A36, Th1;
then [j,i] in [:(Seg k),(Seg (width (Segm M1,(Seg k),(Seg n)))):] by A11, A36, ZFMISC_1:106;
then [j,i] in Indices (Segm M1,(Seg k),(Seg n)) by A35, FINSEQ_1:def 3;
hence (Segm M1,(Seg k),(Seg n)) * j,i = M1 * ((Sgm (Seg k)) . j),((Sgm (Seg n)) . i) by Def1
.= 0. K by A31, A37, A38, A39 ;
:: thesis: verum

end;

then ( lines (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})) is linearly-independent & Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i}) is without_repeated_line ) by A33, A34, A35, Th113, Th114;
then the_rank_of (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})) = k by A4, A34;
then consider P, Q being finite without_zero Subset of NAT such that
A40: ( [:P,Q:] c= Indices (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})) & card P = card Q ) and
A41: ( card P = k & Det (EqSegm (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})),P,Q) <> 0. K ) by Def4;
( P = {} iff Q = {} ) by A40;
then consider P1, Q1 being finite without_zero Subset of NAT such that
A42: ( P1 c= Seg k & Q1 c= (Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i} ) and
( P1 = (Sgm (Seg k)) .: P & Q1 = (Sgm ((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})) .: Q ) and
A43: ( card P1 = card P & card Q1 = card Q ) and
A44: Segm (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})),P,Q = Segm (Segm M1,(Seg k),(Seg n)),P1,Q1 by A40, Th57;
(Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i} c= Seg (width (Segm M1,(Seg k),(Seg n))) by XBOOLE_1:36;
then A45: Q1 c= Seg (width (Segm M1,(Seg k),(Seg n))) by A42, XBOOLE_1:1;
then [:P1,Q1:] c= [:(Seg k),(Seg (width (Segm M1,(Seg k),(Seg n)))):] by A42, ZFMISC_1:119;
then A46: [:P1,Q1:] c= Indices (Segm M1,(Seg k),(Seg n)) by A35, FINSEQ_1:def 3;
( P1 = {} iff Q1 = {} ) by A40, A43;
then consider P2, Q2 being finite without_zero Subset of NAT such that
A47: ( P2 c= Seg k & Q2 c= Seg n ) and
A48: ( P2 = (Sgm (Seg k)) .: P1 & Q2 = (Sgm (Seg n)) .: Q1 ) and
A49: ( card P2 = card P1 & card Q2 = card Q1 ) and
A50: Segm (Segm M1,(Seg k),(Seg n)),P1,Q1 = Segm M1,P2,Q2 by A46, Th57;
A51: P2 = (idseq k) .: P1 by A48, FINSEQ_3:54
.= P1 by A42, FRECHET:13 ;

A52: now

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: Q1 c= Seg n

then width (Segm M1,(Seg k),(Seg n)) = 0 by A35, MATRIX_1:def 4;
then Seg (width (Segm M1,(Seg k),(Seg n))) c= Seg n by FINSEQ_1:7;
hence Q1 c= Seg n by A45, XBOOLE_1:1; :: thesis: verum

end;

suppose k > 0 ; :: thesis: Q1 c= Seg n

hence Q1 c= Seg n by A34, A45, Th1; :: thesis: verum

end;

end;

end;

A53: Q2 = (idseq n) .: Q1 by A48, FINSEQ_3:54
.= Q1 by A52, FRECHET:13 ;
A54: EqSegm (Segm (Segm M1,(Seg k),(Seg n)),(Seg k),((Seg (width (Segm M1,(Seg k),(Seg n)))) \ {i})),P,Q = Segm (Segm M1,(Seg k),(Seg n)),P1,Q1 by A40, A44, Def3
.= EqSegm M1,P1,Q1 by A40, A43, A50, A51, A53, Def3 ;
reconsider i = i, m = m as non zero Element of NAT by A5, A10, ORDINAL1:def 13;
set P2m = P2 \/ {m};
set Q2i = Q2 \/ {i};
A55: ( {m} c= Seg m & P2 c= Seg m & {i} c= Seg n & m <> 0 ) by A8, A11, A32, A47, XBOOLE_1:1, ZFMISC_1:37;
then A56: ( P2 \/ {m} c= Seg m & Q2 \/ {i} c= Seg n ) by A47, XBOOLE_1:8;
then A57: ( [:(P2 \/ {m}),(Q2 \/ {i}):] c= [:(Seg m),(Seg n):] & len M1 = m & width M1 = n ) by Th1, ZFMISC_1:119;
then A58: [:(P2 \/ {m}),(Q2 \/ {i}):] c= Indices M1 by FINSEQ_1:def 3;
( k < m & i in {i} ) by A5, NAT_1:13, TARSKI:def 1;
then A59: ( not m in P2 & not i in Q2 ) by A42, A51, A53, FINSEQ_1:3, XBOOLE_0:def 5;
then A60: ( card (P2 \/ {m}) = m & card (Q2 \/ {i}) = m ) by A5, A40, A41, A43, A49, CARD_2:54;
set SQ2i = Sgm (Q2 \/ {i});
i in {i} by TARSKI:def 1;
then ( i in Q2 \/ {i} & rng (Sgm (Q2 \/ {i})) = Q2 \/ {i} & dom (Sgm (Q2 \/ {i})) = Seg m ) by A56, A60, FINSEQ_1:def 13, FINSEQ_3:45, XBOOLE_0:def 3;
then consider Si being set such that
A61: ( Si in Seg m & (Sgm (Q2 \/ {i})) . Si = i ) by FUNCT_1:def 5;
reconsider Si = Si as Element of NAT by A61;
set ES = EqSegm M1,(P2 \/ {m}),(Q2 \/ {i});
set LC = LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si;
card (Seg m) = m by FINSEQ_1:78;
then A62: P2 \/ {m} = Seg m by A55, A60, CARD_FIN:1, XBOOLE_1:8;

A63: now

let j be Nat; :: thesis: ( j in Seg m implies (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si = M1 * j,i )
assume A64: j in Seg m ; :: thesis: (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si = M1 * j,i
A65: Col M1,i = Col (Segm M1,(P2 \/ {m}),(Q2 \/ {i})),Si by A57, A60, A61, A62, Th50
.= Col (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si by A60, Def3 ;
A66: ( dom M1 = Seg (len M1) & m = len (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) & dom (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) = Seg (len (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i}))) ) by A60, FINSEQ_1:def 3, MATRIX_1:def 3;
hence (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si = (Col M1,i) . j by A64, A65, MATRIX_1:def 9
.= M1 * j,i by A57, A64, A66, MATRIX_1:def 9 ;
:: thesis: verum

end;

len (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) = m by A60, LAPLACE:def 8;
then A67: dom (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) = Seg m by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in Seg m & j <> m implies 0. K = (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) . j )
assume A68: ( j in Seg m & j <> m ) ; :: thesis: 0. K = (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) . j
reconsider J = j as Element of NAT by ORDINAL1:def 13;
j <= m by A68, FINSEQ_1:3;
then j <= k by A5, A68, NAT_1:9;
then 0. K = M1 * j,i by A31, A68
.= (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si by A63, A68 ;
hence 0. K = ((EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * j,Si) * (Cofactor (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),J,Si) by VECTSP_1:39
.= (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) . j by A67, A68, LAPLACE:def 8 ;
:: thesis: verum

end;

then A69: (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) . m = Sum (LaplaceExpC (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),Si) by A8, A67, MATRIX_3:14
.= Det (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) by A60, A61, LAPLACE:27 ;
(Sgm (P2 \/ {m})) . m = (idseq m) . m by A62, FINSEQ_3:54
.= m by A8, FINSEQ_2:57 ;
then A70: Delete (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),m,Si = EqSegm M1,((P2 \/ {m}) \ {m}),((Q2 \/ {i}) \ {i}) by A8, A60, A61, Th64
.= EqSegm M1,P2,((Q2 \/ {i}) \ {i}) by A59, ZFMISC_1:141
.= EqSegm M1,P2,Q2 by A59, ZFMISC_1:141 ;
A71: ( len (Delete (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),m,Si) = m -' 1 & len (EqSegm M1,P2,Q2) = k ) by A41, A43, A49, A60, MATRIX_1:def 3;
reconsider mSi = m + Si as Element of NAT ;
A72: (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * m,Si = M1 * m,i by A8, A63
.= (Line M,m) . i by A11, A29, A57, MATRIX_1:def 8 ;
- (1_ K) <> 0. K by VECTSP_1:86;
then (power K) . (- (1_ K)),mSi <> 0. K by Lm6;
then ((power K) . (- (1_ K)),mSi) * (Minor (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),m,Si) <> 0. K by A41, A51, A53, A54, A60, A70, A71, VECTSP_1:44;
then ((EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) * m,Si) * (Cofactor (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})),m,Si) <> 0. K by A12, A72, VECTSP_1:44;
then Det (EqSegm M1,(P2 \/ {m}),(Q2 \/ {i})) <> 0. K by A8, A67, A69, LAPLACE:def 8;
then ( the_rank_of M1 >= m & the_rank_of M1 <= m ) by A57, A58, A60, Def4, Th74;
hence the_rank_of M = m by A30, XXREAL_0:1; :: thesis: verum

end;

thus ( the_rank_of M = m implies ( lines M is linearly-independent & M is without_repeated_line ) ) by Th105, Th110; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
hence for M being Matrix of m,n,K holds
( ( lines M is linearly-independent & M is without_repeated_line ) iff the_rank_of M = m ) ; :: thesis: verum