let m, n be Nat; 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; 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; 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; ( 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
; 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:57;
A6:
len M = m
by MATRIX_0:def 2;
per cases
( m = 0 or m <> 0 )
;
suppose
m <> 0
;
lines (Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))) is linearly-independent then A7:
width M = n
by Th1;
A8:
now for k being Nat st k in Seg (card (Seg (len M))) holds
not Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),k) = (card ((Seg (width M)) \ {i})) |-> (0. K)set n0 =
n |-> (0. K);
A9:
len (n |-> (0. K)) = n
by CARD_1:def 7;
A10:
dom (Sgm ((Seg (width M)) \ {i})) = Seg (card ((Seg (width M)) \ {i}))
by FINSEQ_3:40, XBOOLE_1:36;
let k be
Nat;
( 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)))
;
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 CARD_1:def 7;
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;
A16:
n9 in Seg n
by A13, A14;
then A17:
(n |-> (0. K)) . n9 = 0. K
by FINSEQ_2:57;
Sgm (Seg (len M)) = idseq m
by A6, FINSEQ_3:48;
then A18:
(Sgm (Seg (len M))) . k = k
by A5, A6, A11, FINSEQ_2:49;
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_0:def 7;
then
n9 <> i
by A3, A5, A6, A11, A15, A17;
then
n9 in (Seg (width M)) \ {i}
by A7, A16, ZFMISC_1:56;
then consider x being
object 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 3;
assume A22:
Line (
(Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),
k)
= (card ((Seg (width M)) \ {i})) |-> (0. K)
;
contradictionreconsider 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:13;
hence
contradiction
by A22, A15, A17, A20, A10, A18, FINSEQ_2:57;
verum end; A23:
now for M1 being Matrix of card (Seg (len M)), card ((Seg (width M)) \ {i}),K st ( 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 ) holds
M1 = 0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})))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;
( ( 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
;
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;
( k in Seg m implies ex x being Element of K st S1[k,x] )
assume
k in Seg m
;
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
;
S1[k,a]
thus
S1[
k,
a]
by A27;
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_0:def 2;
then A33:
dom Mf = Seg m
by FINSEQ_1:def 3;
A34:
now for j being Nat st j in Seg n holds
Sum (Col (Mf,j)) = 0. KA35:
len M1 = m
by A5, A6, MATRIX_0:def 2;
A36:
len Mf = m
by MATRIX_0:def 2;
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;
( j in Seg n implies Sum (Col (Mf,b1)) = 0. K )assume A39:
j in Seg n
;
Sum (Col (Mf,b1)) = 0. Kset C =
Col (
Mf,
j);
A40:
len (Col (Mf,j)) =
len Mf
by MATRIX_0:def 8
.=
m
by MATRIX_0:def 2
;
per cases
( j = i or j <> i )
;
suppose A41:
j = i
;
Sum (Col (Mf,b1)) = 0. Kset m0 =
m |-> (0. K);
A42:
now for n9 being Nat st 1 <= n9 & n9 <= m holds
(Col (Mf,j)) . n9 = (m |-> (0. K)) . n9let n9 be
Nat;
( 1 <= n9 & n9 <= m implies (Col (Mf,j)) . n9 = (m |-> (0. K)) . n9 )assume that A43:
1
<= n9
and A44:
n9 <= m
;
(Col (Mf,j)) . n9 = (m |-> (0. K)) . n9A45:
width M = n
by A43, A44, Th1;
A46:
width Mf = n
by A43, A44, Th1;
A47:
n9 in Seg m
by A43, A44;
then A48:
Mf . n9 = Mf /. n9
by A33, PARTFUN1:def 6;
0. K =
M * (
n9,
i)
by A3, A47
.=
(Line (M,n9)) . i
by A39, A41, A45, MATRIX_0:def 7
;
then (p /. n9) * (0. K) =
((p /. n9) * (Line (M,n9))) . i
by A39, A41, A45, FVSUM_1:51
.=
(Mf /. n9) . i
by A31, A32, A47, A48
.=
(Line (Mf,n9)) . i
by A47, A48, MATRIX_0:52
.=
Mf * (
n9,
i)
by A39, A41, A46, MATRIX_0:def 7
.=
(Col (Mf,i)) . n9
by A36, A37, A47, MATRIX_0:def 8
;
hence (Col (Mf,j)) . n9 =
0. K
by A41
.=
(m |-> (0. K)) . n9
by A47, FINSEQ_2:57
;
verum end;
len (m |-> (0. K)) = m
by CARD_1:def 7;
then
Col (
Mf,
j)
= m |-> (0. K)
by A40, A42;
hence
Sum (Col (Mf,j)) = 0. K
by A40, MATRIX_3:11;
verum end; suppose A49:
j <> i
;
Sum (Col (Mf,b1)) = 0. KA50:
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:56;
then consider x being
object 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 3;
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:40, XBOOLE_1:36;
A54:
now for n9 being Nat st 1 <= n9 & n9 <= m holds
(Col (Mf,j)) . n9 = (Col (M1,x)) . n9let n9 be
Nat;
( 1 <= n9 & n9 <= m implies (Col (Mf,j)) . n9 = (Col (M1,x)) . n9 )assume that A55:
1
<= n9
and A56:
n9 <= m
;
(Col (Mf,j)) . n9 = (Col (M1,x)) . n9A57:
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:48;
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_0:def 7;
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 6;
(idseq m) . n9 = n9
by A62, FINSEQ_2:49;
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:13;
thus (Col (Mf,j)) . n9 =
Mf * (
n9,
j)
by A36, A37, A62, MATRIX_0:def 8
.=
(Line (Mf,n9)) . j
by A39, A57, MATRIX_0:def 7
.=
(Mf /. n9) . j
by A62, A65, MATRIX_0:52
.=
((p /. n9) * (Line (M,n9))) . j
by A31, A32, A62, A65
.=
(a * (Line (M,n9))) . j
by A28, A62, A63, PARTFUN1:def 6
.=
a * (M * (n9,j))
by A7, A39, A61, FVSUM_1:51
.=
(a * (Line ((Segm (M,(Seg (len M)),((Seg (width M)) \ {i}))),n9))) . x
by A51, A53, A58, A66, A61, FVSUM_1:51
.=
M1 * (
n9,
x)
by A51, A53, A60, A64, MATRIX_0:def 7
.=
(Col (M1,x)) . n9
by A35, A38, A62, MATRIX_0:def 8
;
verum end; A67:
len (Col (Mf,j)) = len Mf
by MATRIX_0:def 8;
len (Col (M1,x)) = len M1
by MATRIX_0:def 8;
then
Col (
Mf,
j)
= Col (
M1,
x)
by A36, A35, A67, A54;
hence
Sum (Col (Mf,j)) = 0. K
by A25, A51, A53;
verum end; end; end; now for j being Nat st j in Seg m holds
ex pj being Element of the carrier of K st Line (Mf,j) = pj * (Line (M,j))let j be
Nat;
( 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
;
ex pj being Element of the carrier of K st Line (Mf,j) = pj * (Line (M,j))take pj =
p /. j;
Line (Mf,j) = pj * (Line (M,j))thus Line (
Mf,
j) =
Mf . j
by A68, MATRIX_0:52
.=
pj * (Line (M,j))
by A31, A32, A68
;
verum end; then A69:
Mf = 0. (
K,
m,
n)
by A1, A2, A34, Th109;
A70:
now for j being Nat st 1 <= j & j <= m holds
M1 . j = (0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})))) . jlet j be
Nat;
( 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
;
M1 . j = (0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})))) . jA73:
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_0:52
.=
n |-> (0. K)
by A73, FUNCOP_1:7
;
p . j = p /. j
by A28, A73, PARTFUN1:def 6;
then A77:
a * (Line (M,j)) =
Mf . j
by A31, A32, A73, A74
.=
Line (
Mf,
j)
by A73, MATRIX_0:52
;
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:48;
then
(Sgm (Seg (len M))) . j = j
by A73, FINSEQ_2:49;
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:133
.=
dom (Sgm ((Seg (width M)) \ {i}))
by RELAT_1:134
.=
Seg (card ((Seg (width M)) \ {i}))
by FINSEQ_3:40, XBOOLE_1:36
;
dom (Line (M,j)) =
Seg (len (Line (M,j)))
by FINSEQ_1:def 3
.=
Seg (width M)
by CARD_1:def 7
;
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:19
.=
(0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})))) . j
by A5, A6, A73, FUNCOP_1:7
;
hence
M1 . j = (0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})))) . j
by A5, A6, A73, MATRIX_0:52;
verum end; A81:
len (0. (K,(card (Seg (len M))),(card ((Seg (width M)) \ {i})))) = m
by A5, A6, MATRIX_0:def 2;
len M1 = m
by A5, A6, MATRIX_0:def 2;
hence
M1 = 0. (
K,
(card (Seg (len M))),
(card ((Seg (width M)) \ {i})))
by A81, A70;
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;
verum end; end;