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