let n, m be Nat; :: thesis: for K being Field
for M being Matrix of m,n,K
for i being Nat st M is without_repeated_line & lines M is linearly-independent & ( for j being Nat st j in Seg m holds
M * j,i = 0. K ) holds
lines (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) is linearly-independent
let K be Field; :: thesis: for M being Matrix of m,n,K
for i being Nat st M is without_repeated_line & lines M is linearly-independent & ( for j being Nat st j in Seg m holds
M * j,i = 0. K ) holds
lines (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) is linearly-independent
let M be Matrix of m,n,K; :: thesis: for i being Nat st M is without_repeated_line & lines M is linearly-independent & ( for j being Nat st j in Seg m holds
M * j,i = 0. K ) holds
lines (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) is linearly-independent
let i be Nat; :: thesis: ( M is without_repeated_line & lines M is linearly-independent & ( for j being Nat st j in Seg m holds
M * j,i = 0. K ) implies lines (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) is linearly-independent )
assume that
A1: M is without_repeated_line and
A2: lines M is linearly-independent and
A3: for j being Nat st j in Seg m holds
M * j,i = 0. K ; :: thesis: lines (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) is linearly-independent
set SMi = (Seg (width M)) \ {i};
set Sl = Seg (len M);
set S = Segm M,(Seg (len M)),((Seg (width M)) \ {i});
A4: (Seg (width M)) \ {i} c= Seg (width M) by XBOOLE_1:36;
A5: card (Seg (len M)) = len M by FINSEQ_1:78;
A6: len M = m by MATRIX_1:def 3;
per cases ( m = 0 or m <> 0 ) ;
suppose m = 0 ; :: thesis: lines (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) is linearly-independent
then len (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) = 0 by A6, MATRIX_1:def 3;
then Segm M,(Seg (len M)),((Seg (width M)) \ {i}) = {} ;
hence lines (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) is linearly-independent ; :: thesis: verum
end;
suppose m <> 0 ; :: thesis: lines (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) is linearly-independent
then A7: width M = n by Th1;
A8: now
set n0 = n |-> (0. K);
A9: len (n |-> (0. K)) = n by FINSEQ_1:def 18;
A10: dom (Sgm ((Seg (width M)) \ {i})) = Seg (card ((Seg (width M)) \ {i})) by FINSEQ_3:45, XBOOLE_1:36;
let k be Nat; :: thesis: ( k in Seg (card (Seg (len M))) implies not Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),k = (card ((Seg (width M)) \ {i})) |-> (0. K) )
assume A11: k in Seg (card (Seg (len M))) ; :: thesis: not Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),k = (card ((Seg (width M)) \ {i})) |-> (0. K)
Line M,k in lines M by A5, A6, A11, Th103;
then reconsider LM = Line M,k as Element of n -tuples_on the carrier of K by Th102;
A12: len LM = n by FINSEQ_1:def 18;
LM <> n |-> (0. K) by A1, A2, A5, A6, A11, Th109;
then consider n9 being Nat such that
A13: 1 <= n9 and
A14: n9 <= n and
A15: LM . n9 <> (n |-> (0. K)) . n9 by A12, A9, FINSEQ_1:18;
n9 in NAT by ORDINAL1:def 13;
then A16: n9 in Seg n by A13, A14;
then A17: (n |-> (0. K)) . n9 = 0. K by FINSEQ_2:71;
Sgm (Seg (len M)) = idseq m by A6, FINSEQ_3:54;
then A18: (Sgm (Seg (len M))) . k = k by A5, A6, A11, FINSEQ_2:57;
A19: rng (Sgm ((Seg (width M)) \ {i})) = (Seg (width M)) \ {i} by A4, FINSEQ_1:def 13;
LM . n9 = M * k,n9 by A7, A16, MATRIX_1:def 8;
then n9 <> i by A3, A5, A6, A11, A15, A17;
then n9 in (Seg (width M)) \ {i} by A7, A16, ZFMISC_1:64;
then consider x being set such that
A20: x in dom (Sgm ((Seg (width M)) \ {i})) and
A21: (Sgm ((Seg (width M)) \ {i})) . x = n9 by A19, FUNCT_1:def 5;
assume A22: Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),k = (card ((Seg (width M)) \ {i})) |-> (0. K) ; :: thesis: contradiction
reconsider x = x as Element of NAT by A20;
Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),k = (Line M,((Sgm (Seg (len M))) . k)) * (Sgm ((Seg (width M)) \ {i})) by A11, Th47, XBOOLE_1:36;
then (Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),k) . x = (Line M,((Sgm (Seg (len M))) . k)) . n9 by A20, A21, FUNCT_1:23;
hence contradiction by A22, A15, A17, A20, A10, A18, FINSEQ_2:71; :: thesis: verum
end;
A23: now
set NULL = 0. K,(card (Seg (len M))),(card ((Seg (width M)) \ {i}));
let M1 be Matrix of card (Seg (len M)), card ((Seg (width M)) \ {i}),K; :: thesis: ( ( for i being Nat st i in Seg (card (Seg (len M))) holds
ex a being Element of K st Line M1,i = a * (Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i) ) & ( for j being Nat st j in Seg (card ((Seg (width M)) \ {i})) holds
Sum (Col M1,j) = 0. K ) implies M1 = 0. K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})) )
assume that
A24: for i being Nat st i in Seg (card (Seg (len M))) holds
ex a being Element of K st Line M1,i = a * (Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i) and
A25: for j being Nat st j in Seg (card ((Seg (width M)) \ {i})) holds
Sum (Col M1,j) = 0. K ; :: thesis: M1 = 0. K,(card (Seg (len M))),(card ((Seg (width M)) \ {i}))
defpred S1[ set , set ] means for i being Nat st $1 = i holds
ex a being Element of K st
( a = $2 & Line M1,i = a * (Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),i) );
A26: for k being Nat st k in Seg m holds
ex x being Element of K st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg m implies ex x being Element of K st S1[k,x] )
assume k in Seg m ; :: thesis: ex x being Element of K st S1[k,x]
then consider a being Element of K such that
A27: Line M1,k = a * (Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),k) by A5, A6, A24;
take a ; :: thesis: S1[k,a]
thus S1[k,a] by A27; :: thesis: verum
end;
consider p being FinSequence of K such that
A28: dom p = Seg m and
A29: for k being Nat st k in Seg m holds
S1[k,p . k] from FINSEQ_1:sch 5(A26);
deffunc H1( Nat) -> Element of (width M) -tuples_on the carrier of K = (p /. $1) * (Line M,$1);
consider f being FinSequence of (width M) -tuples_on the carrier of K such that
A30: len f = m and
A31: for j being Nat st j in dom f holds
f . j = H1(j) from FINSEQ_2:sch 1();
reconsider f9 = f as FinSequence of the carrier of (n -VectSp_over K) by A7, Th102;
FinS2MX f9 is Matrix of m,n,K by A30;
then reconsider Mf = f as Matrix of m,n,K ;
A32: dom f = Seg m by A30, FINSEQ_1:def 3;
len Mf = m by MATRIX_1:def 3;
then A33: dom Mf = Seg m by FINSEQ_1:def 3;
A34: now
A35: len M1 = m by A5, A6, MATRIX_1:def 3;
A36: len Mf = m by MATRIX_1:def 3;
A37: dom Mf = Seg (len Mf) by FINSEQ_1:def 3;
A38: dom M1 = Seg (len M1) by FINSEQ_1:def 3;
let j be Nat; :: thesis: ( j in Seg n implies Sum (Col Mf,b1) = 0. K )
assume A39: j in Seg n ; :: thesis: Sum (Col Mf,b1) = 0. K
set C = Col Mf,j;
A40: len (Col Mf,j) = len Mf by MATRIX_1:def 9
.= m by MATRIX_1:def 3 ;
per cases ( j = i or j <> i ) ;
suppose A41: j = i ; :: thesis: Sum (Col Mf,b1) = 0. K
set m0 = m |-> (0. K);
A42: now
let n9 be Nat; :: thesis: ( 1 <= n9 & n9 <= m implies (Col Mf,j) . n9 = (m |-> (0. K)) . n9 )
assume that
A43: 1 <= n9 and
A44: n9 <= m ; :: thesis: (Col Mf,j) . n9 = (m |-> (0. K)) . n9
A45: width M = n by A43, A44, Th1;
A46: width Mf = n by A43, A44, Th1;
n9 in NAT by ORDINAL1:def 13;
then A47: n9 in Seg m by A43, A44;
then A48: Mf . n9 = Mf /. n9 by A33, PARTFUN1:def 8;
0. K = M * n9,i by A3, A47
.= (Line M,n9) . i by A39, A41, A45, MATRIX_1:def 8 ;
then (p /. n9) * (0. K) = ((p /. n9) * (Line M,n9)) . i by A39, A41, A45, FVSUM_1:63
.= (Mf /. n9) . i by A31, A32, A47, A48
.= (Line Mf,n9) . i by A47, A48, MATRIX_2:10
.= Mf * n9,i by A39, A41, A46, MATRIX_1:def 8
.= (Col Mf,i) . n9 by A36, A37, A47, MATRIX_1:def 9 ;
hence (Col Mf,j) . n9 = 0. K by A41, VECTSP_1:39
.= (m |-> (0. K)) . n9 by A47, FINSEQ_2:71 ;
:: thesis: verum
end;
len (m |-> (0. K)) = m by FINSEQ_1:def 18;
then Col Mf,j = m |-> (0. K) by A40, A42, FINSEQ_1:18;
hence Sum (Col Mf,j) = 0. K by A40, MATRIX_3:13; :: thesis: verum
end;
suppose A49: j <> i ; :: thesis: Sum (Col Mf,b1) = 0. K
A50: rng (Sgm ((Seg (width M)) \ {i})) = (Seg (width M)) \ {i} by A4, FINSEQ_1:def 13;
j in (Seg (width M)) \ {i} by A7, A39, A49, ZFMISC_1:64;
then consider x being set such that
A51: x in dom (Sgm ((Seg (width M)) \ {i})) and
A52: (Sgm ((Seg (width M)) \ {i})) . x = j by A50, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A51;
set C1 = Col M1,x;
A53: dom (Sgm ((Seg (width M)) \ {i})) = Seg (card ((Seg (width M)) \ {i})) by FINSEQ_3:45, XBOOLE_1:36;
A54: now
let n9 be Nat; :: thesis: ( 1 <= n9 & n9 <= m implies (Col Mf,j) . n9 = (Col M1,x) . n9 )
assume that
A55: 1 <= n9 and
A56: n9 <= m ; :: thesis: (Col Mf,j) . n9 = (Col M1,x) . n9
A57: width Mf = n by A55, A56, Th1;
A58: width (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) = card ((Seg (width M)) \ {i}) by A6, A55, A56, Th1;
A59: Sgm (Seg (len M)) = idseq m by A6, FINSEQ_3:54;
A60: width M1 = card ((Seg (width M)) \ {i}) by A6, A55, A56, Th1;
A61: (Line M,n9) . j = M * n9,j by A7, A39, MATRIX_1:def 8;
n9 in NAT by ORDINAL1:def 13;
then A62: n9 in Seg m by A55, A56;
then consider a being Element of K such that
A63: a = p . n9 and
A64: Line M1,n9 = a * (Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),n9) by A29;
A65: Mf . n9 = Mf /. n9 by A33, A62, PARTFUN1:def 8;
(idseq m) . n9 = n9 by A62, FINSEQ_2:57;
then (Line M,n9) * (Sgm ((Seg (width M)) \ {i})) = Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),n9 by A5, A6, A62, A59, Th47, XBOOLE_1:36;
then A66: (Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),n9) . x = (Line M,n9) . j by A51, A52, FUNCT_1:23;
thus (Col Mf,j) . n9 = Mf * n9,j by A36, A37, A62, MATRIX_1:def 9
.= (Line Mf,n9) . j by A39, A57, MATRIX_1:def 8
.= (Mf /. n9) . j by A62, A65, MATRIX_2:10
.= ((p /. n9) * (Line M,n9)) . j by A31, A32, A62, A65
.= (a * (Line M,n9)) . j by A28, A62, A63, PARTFUN1:def 8
.= a * (M * n9,j) by A7, A39, A61, FVSUM_1:63
.= (a * (Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),n9)) . x by A51, A53, A58, A66, A61, FVSUM_1:63
.= M1 * n9,x by A51, A53, A60, A64, MATRIX_1:def 8
.= (Col M1,x) . n9 by A35, A38, A62, MATRIX_1:def 9 ; :: thesis: verum
end;
A67: len (Col Mf,j) = len Mf by MATRIX_1:def 9;
len (Col M1,x) = len M1 by MATRIX_1:def 9;
then Col Mf,j = Col M1,x by A36, A35, A67, A54, FINSEQ_1:18;
hence Sum (Col Mf,j) = 0. K by A25, A51, A53; :: thesis: verum
end;
end;
end;
now
let j be Nat; :: thesis: ( j in Seg m implies ex pj being Element of the carrier of K st Line Mf,j = pj * (Line M,j) )
assume A68: j in Seg m ; :: thesis: ex pj being Element of the carrier of K st Line Mf,j = pj * (Line M,j)
take pj = p /. j; :: thesis: Line Mf,j = pj * (Line M,j)
thus Line Mf,j = Mf . j by A68, MATRIX_2:10
.= pj * (Line M,j) by A31, A32, A68 ; :: thesis: verum
end;
then A69: Mf = 0. K,m,n by A1, A2, A34, Th109;
A70: now
let j be Nat; :: thesis: ( 1 <= j & j <= m implies M1 . j = (0. K,(card (Seg (len M))),(card ((Seg (width M)) \ {i}))) . j )
assume that
A71: 1 <= j and
A72: j <= m ; :: thesis: M1 . j = (0. K,(card (Seg (len M))),(card ((Seg (width M)) \ {i}))) . j
j in NAT by ORDINAL1:def 13;
then A73: j in Seg m by A71, A72;
then consider a being Element of K such that
A74: a = p . j and
A75: Line M1,j = a * (Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),j) by A29;
A76: Line (0. K,m,n),j = (0. K,m,n) . j by A73, MATRIX_2:10
.= n |-> (0. K) by A73, FUNCOP_1:13 ;
p . j = p /. j by A28, A73, PARTFUN1:def 8;
then A77: a * (Line M,j) = Mf . j by A31, A32, A73, A74
.= Line Mf,j by A73, MATRIX_2:10 ;
A78: rng (Sgm ((Seg (width M)) \ {i})) = (Seg (width M)) \ {i} by A4, FINSEQ_1:def 13;
Sgm (Seg (len M)) = idseq m by A6, FINSEQ_3:54;
then (Sgm (Seg (len M))) . j = j by A73, FINSEQ_2:57;
then A79: Line (Segm M,(Seg (len M)),((Seg (width M)) \ {i})),j = (Line M,j) * (Sgm ((Seg (width M)) \ {i})) by A5, A6, A73, Th47, XBOOLE_1:36;
(Seg n) /\ ((Seg (width M)) \ {i}) = (Seg (width M)) \ {i} by A7, XBOOLE_1:28, XBOOLE_1:36;
then A80: (Sgm ((Seg (width M)) \ {i})) " (Seg n) = (Sgm ((Seg (width M)) \ {i})) " (rng (Sgm ((Seg (width M)) \ {i}))) by A78, RELAT_1:168
.= dom (Sgm ((Seg (width M)) \ {i})) by RELAT_1:169
.= Seg (card ((Seg (width M)) \ {i})) by FINSEQ_3:45, XBOOLE_1:36 ;
dom (Line M,j) = Seg (len (Line M,j)) by FINSEQ_1:def 3
.= Seg (width M) by FINSEQ_1:def 18 ;
then Line M1,j = (Line (0. K,m,n),j) * (Sgm ((Seg (width M)) \ {i})) by A69, A75, A77, A78, A79, Th87, XBOOLE_1:36
.= (card ((Seg (width M)) \ {i})) |-> (0. K) by A80, A76, FUNCOP_1:25
.= (0. K,(card (Seg (len M))),(card ((Seg (width M)) \ {i}))) . j by A5, A6, A73, FUNCOP_1:13 ;
hence M1 . j = (0. K,(card (Seg (len M))),(card ((Seg (width M)) \ {i}))) . j by A5, A6, A73, MATRIX_2:10; :: thesis: verum
end;
A81: len (0. K,(card (Seg (len M))),(card ((Seg (width M)) \ {i}))) = m by A5, A6, MATRIX_1:def 3;
len M1 = m by A5, A6, MATRIX_1:def 3;
hence M1 = 0. K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})) by A81, A70, FINSEQ_1:18; :: thesis: verum
end;
Segm M,(Seg (len M)),((Seg (width M)) \ {i}) is without_repeated_line by A1, A3, Th113;
hence lines (Segm M,(Seg (len M)),((Seg (width M)) \ {i})) is linearly-independent by A8, A23, Th109; :: thesis: verum
end;
end;