let n, m be Nat; for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
let f be n -element real-valued FinSequence; for M being Matrix of n,m,F_Real
for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
let M be Matrix of n,m,F_Real; for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )
defpred S1[ Nat] means for n, m being Nat
for M being Matrix of n,m,F_Real
for f being b1 -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = $1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) );
A1:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A2:
S1[
i]
;
S1[i + 1]
let n,
m be
Nat;
for M being Matrix of n,m,F_Real
for f being n -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = i + 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )let M be
Matrix of
n,
m,
F_Real;
for f being n -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = i + 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )let f be
n -element real-valued FinSequence;
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = i + 1 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )let S be
Subset of
(Seg n);
( ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = i + 1 implies ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) ) )
assume that A3:
(
n = 0 implies
m = 0 )
and A4:
M | S is
one-to-one
and A5:
rng (M | S) = lines M
and A6:
card (lines M) = i + 1
;
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
A7:
len M = n
by A3, MATRIX13:1;
A8:
width M = m
by A3, MATRIX13:1;
per cases
( i = 0 or i > 0 )
;
suppose
i = 0
;
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )then consider L being
Linear_Combination of
lines M such that A9:
Sum L = (Mx2Tran M) . f
and A10:
for
i being
Nat st
i in Seg n holds
(
L . (Line (M,i)) = Sum f &
M " {(Line (M,i))} = dom f )
by A6, Lm5;
take
L
;
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )thus
Sum L = (Mx2Tran M) . f
by A9;
for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))})))let w be
Nat;
( w in S implies L . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) )assume A11:
w in S
;
L . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))
M " {(Line (M,w))} = dom f
by A10, A11;
then A12:
f | (M " {(Line (M,w))}) = f
;
L . (Line (M,w)) = Sum f
by A10, A11;
hence
Sum (Seq (f | (M " {(Line (M,w))}))) = L . (Line (M,w))
by A12, FINSEQ_3:116;
verum end; suppose A13:
i > 0
;
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
lines M <> {}
by A6;
then consider x being
object such that A14:
x in lines M
by XBOOLE_0:def 1;
reconsider LM =
{x} as
Subset of
(lines M) by A14, ZFMISC_1:31;
set n1 =
n -' (card (M " LM));
reconsider ML1 =
M - LM as
Matrix of
n -' (card (M " LM)),
m,
F_Real by MATRTOP1:14;
A15:
LM ` = (lines M) \ LM
by SUBSET_1:def 4;
then A16:
LM misses LM `
by XBOOLE_1:79;
LM \/ (LM `) =
[#] (lines M)
by SUBSET_1:10
.=
lines M
by SUBSET_1:def 3
;
then A17:
(M " LM) \/ (M " (LM `)) =
M " (rng M)
by RELAT_1:140
.=
dom M
by RELAT_1:134
;
A18:
len ML1 = (len M) - (card (M " LM))
by FINSEQ_3:59;
then A19:
n - (card (M " LM)) = n -' (card (M " LM))
by A7, XREAL_1:49, XREAL_1:233;
LM misses LM `
by A15, XBOOLE_1:79;
then A20:
(card (M " LM)) + (card (M " (LM `))) =
card (dom M)
by A17, CARD_2:40, FUNCT_1:71
.=
n
by A7, CARD_1:62
;
A21:
n -' (card (M " LM)) <> 0
set n2 =
n -' (card (M " (LM `)));
reconsider ML2 =
M - (LM `) as
Matrix of
n -' (card (M " (LM `))),
m,
F_Real by MATRTOP1:14;
rng ML2 = (rng M) \ (LM `)
by FINSEQ_3:65;
then A22:
rng ML2 = (LM `) `
by SUBSET_1:def 4;
reconsider FR =
F_Real as
Field ;
set Mf =
(Mx2Tran M) . f;
set V =
m -VectSp_over F_Real;
len f = n
by CARD_1:def 7;
then A23:
dom f = Seg n
by FINSEQ_1:def 3;
consider j being
object such that A24:
j in dom (M | S)
and A25:
(M | S) . j = x
by A5, A14, FUNCT_1:def 3;
A26:
x = M . j
by A24, A25, FUNCT_1:47;
A27:
j in dom M
by A24, RELAT_1:57;
A28:
j in S
by A24;
reconsider j =
j as
Nat by A24;
A29:
x = Line (
M,
j)
by A27, A26, MATRIX_0:60;
A30:
len ML2 = (len M) - (card (M " (LM `)))
by FINSEQ_3:59;
then A31:
n - (card (M " (LM `))) = n -' (card (M " (LM `)))
by A7, XREAL_1:49, XREAL_1:233;
A32:
rng ML1 = (rng M) \ LM
by FINSEQ_3:65;
then A33:
rng ML1 = LM `
by SUBSET_1:def 4;
reconsider LMj =
Line (
M,
j) as
Element of
(m -VectSp_over F_Real) by A8, MATRIX13:102;
A34:
card (rng ML1) =
(card (rng M)) - (card LM)
by A32, CARD_2:44
.=
(i + 1) - 1
by A6, CARD_2:42
;
(LM `) ` = LM
;
then consider P being
Permutation of
(dom M) such that A35:
(M - LM) ^ (M - (LM `)) = M * P
by FINSEQ_3:115;
dom M = Seg n
by A7, FINSEQ_1:def 3;
then reconsider p =
P as
Permutation of
(Seg n) ;
A36:
(M | S) * P =
(M | S) * (p | (dom p))
.=
(M * p) | ((dom p) /\ (p " S))
by FUNCT_1:100
.=
(M * p) | (p " S)
by RELAT_1:132, XBOOLE_1:28
;
reconsider pp =
P as
one-to-one Function ;
len (M * p) = n
by MATRIX_0:def 2;
then A37:
dom (M * p) = Seg n
by FINSEQ_1:def 3;
set ppj =
(pp ") . j;
A38:
rng p = Seg n
by FUNCT_2:def 3;
then A39:
(
p " S = (pp ") .: S &
dom (pp ") = Seg n )
by FUNCT_1:33, FUNCT_1:85;
then A40:
(pp ") . j in p " S
by A28, FUNCT_1:def 6;
A41:
p . ((pp ") . j) = j
by A28, A38, FUNCT_1:35;
A42:
not
(pp ") . j in dom ML1
proof
assume A43:
(pp ") . j in dom ML1
;
contradiction
(M * P) . ((pp ") . j) = M . j
by A40, A41, A37, FUNCT_1:12;
then
(M * P) . ((pp ") . j) = LMj
by A27, MATRIX_0:60;
then
ML1 . ((pp ") . j) = LMj
by A35, A43, FINSEQ_1:def 7;
then A44:
ML1 . ((pp ") . j) in LM
by A29, TARSKI:def 1;
ML1 . ((pp ") . j) in LM `
by A33, A43, FUNCT_1:def 3;
hence
contradiction
by A16, A44, XBOOLE_0:3;
verum
end; set pSj =
(p " S) \ {((pp ") . j)};
dom M = Seg n
by A7, FINSEQ_1:def 3;
then A45:
dom (M | S) = S
by RELAT_1:62;
A46:
(p " S) \ {((pp ") . j)} c= dom ML1
proof
let y be
object ;
TARSKI:def 3 ( not y in (p " S) \ {((pp ") . j)} or y in dom ML1 )
assume A47:
y in (p " S) \ {((pp ") . j)}
;
y in dom ML1
then reconsider Y =
y as
Nat ;
A48:
(M * p) . y = M . (p . y)
by A37, A47, FUNCT_1:12;
not
y in {((pp ") . j)}
by A47, XBOOLE_0:def 5;
then A49:
y <> (pp ") . j
by TARSKI:def 1;
A50:
(pp ") . j in dom P
by A40, FUNCT_1:def 7;
A51:
y in p " S
by A47, XBOOLE_0:def 5;
then A52:
p . y in dom (M | S)
by A45, FUNCT_1:def 7;
y in dom P
by A51, FUNCT_1:def 7;
then
p . y <> j
by A41, A49, A50, FUNCT_1:def 4;
then
(M | S) . (p . y) <> (M | S) . j
by A4, A24, A52, FUNCT_1:def 4;
then
(M * p) . y <> LMj
by A25, A29, A48, A52, FUNCT_1:47;
then A53:
not
(M * p) . y in LM
by A29, TARSKI:def 1;
assume
not
y in dom ML1
;
contradiction
then consider w being
Nat such that A54:
w in dom ML2
and A55:
Y = (len ML1) + w
by A35, A37, A47, FINSEQ_1:25;
(M * p) . Y = ML2 . w
by A35, A54, A55, FINSEQ_1:def 7;
hence
contradiction
by A22, A53, A54, FUNCT_1:def 3;
verum
end; then
(
(M * p) | ((p " S) \ {((pp ") . j)}) = ((M * p) | (p " S)) | ((p " S) \ {((pp ") . j)}) &
(M * p) | ((p " S) \ {((pp ") . j)}) = ML1 | ((p " S) \ {((pp ") . j)}) )
by A35, FINSEQ_6:11, RELAT_1:74, XBOOLE_1:36;
then A56:
ML1 | ((p " S) \ {((pp ") . j)}) is
one-to-one
by A4, A36, FUNCT_1:52;
(
dom p = Seg n &
p . ((pp ") . j) = j )
by A28, A38, FUNCT_1:35, FUNCT_2:52;
then A57:
(pp ") . j in dom ((M | S) * p)
by A24, A40, FUNCT_1:11;
then
((M | S) * p) . ((pp ") . j) = LMj
by A25, A29, A41, FUNCT_1:12;
then A58:
LM =
Im (
((M | S) * p),
((pp ") . j))
by A29, A57, FUNCT_1:59
.=
((M * p) | (p " S)) .: {((pp ") . j)}
by A36, RELAT_1:def 16
;
rng M =
rng ((M * p) | (p " S))
by A5, A36, A38, A45, RELAT_1:28
.=
(M * p) .: (p " S)
by RELAT_1:115
.=
((M * p) | (p " S)) .: (p " S)
by RELAT_1:129
;
then A59:
rng ML1 =
((M * p) | (p " S)) .: ((p " S) \ {((pp ") . j)})
by A4, A36, A32, A58, FUNCT_1:64
.=
rng (((M * p) | (p " S)) | ((p " S) \ {((pp ") . j)}))
by RELAT_1:115
.=
rng ((M * p) | ((p " S) \ {((pp ") . j)}))
by RELAT_1:74, XBOOLE_1:36
.=
rng (ML1 | ((p " S) \ {((pp ") . j)}))
by A35, A46, FINSEQ_6:11
;
reconsider fp =
f * p as
n -element FinSequence of
REAL by MATRTOP1:21;
A60:
(n -' (card (M " LM))) + (n -' (card (M " (LM `)))) =
len (ML1 ^ ML2)
by MATRIX_0:def 2
.=
len (M * p)
by A35
.=
n
by MATRIX_0:def 2
;
len fp = n
by CARD_1:def 7;
then consider fp1,
fp2 being
FinSequence of
REAL such that A61:
len fp1 = n -' (card (M " LM))
and A62:
len fp2 = n -' (card (M " (LM `)))
and A63:
fp = fp1 ^ fp2
by A60, FINSEQ_2:23;
A64:
fp2 is
n -' (card (M " (LM `))) -element
by A62, CARD_1:def 7;
then A65:
len ((Mx2Tran ML2) . fp2) = m
by CARD_1:def 7;
card LM = 1
by CARD_2:42;
then consider L2 being
Linear_Combination of
lines ML2 such that A66:
Sum L2 = (Mx2Tran ML2) . fp2
and A67:
for
i being
Nat st
i in Seg (n -' (card (M " (LM `)))) holds
(
L2 . (Line (ML2,i)) = Sum fp2 &
ML2 " {(Line (ML2,i))} = dom fp2 )
by A64, A22, Lm5;
A68:
fp1 is
n -' (card (M " LM)) -element
by A61, CARD_1:def 7;
then
len ((Mx2Tran ML1) . fp1) = m
by CARD_1:def 7;
then reconsider Mf1 =
@ ((Mx2Tran ML1) . fp1),
Mf2 =
@ ((Mx2Tran ML2) . fp2) as
Element of
m -tuples_on the
carrier of
F_Real by A65, FINSEQ_2:92;
A69:
Carrier L2 c= lines ML2
by VECTSP_6:def 4;
len ML1 = n -' (card (M " LM))
by A7, A18, XREAL_1:49, XREAL_1:233;
then
(p " S) \ {((pp ") . j)} is
Subset of
(Seg (n -' (card (M " LM))))
by A46, FINSEQ_1:def 3;
then consider L1 being
Linear_Combination of
lines ML1 such that A70:
Sum L1 = (Mx2Tran ML1) . fp1
and A71:
for
i being
Nat st
i in (p " S) \ {((pp ") . j)} holds
L1 . (Line (ML1,i)) = Sum (Seq (fp1 | (ML1 " {(Line (ML1,i))})))
by A2, A68, A21, A56, A59, A34;
A72:
Carrier L1 c= lines ML1
by VECTSP_6:def 4;
(rng ML1) \/ (rng ML2) =
[#] (lines M)
by A22, A33, SUBSET_1:10
.=
lines M
by SUBSET_1:def 3
;
then
(
L1 is
Linear_Combination of
lines M &
L2 is
Linear_Combination of
lines M )
by VECTSP_6:4, XBOOLE_1:7;
then reconsider L12 =
L1 + L2 as
Linear_Combination of
lines M by VECTSP_6:24;
take
L12
;
( Sum L12 = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L12 . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )thus (Mx2Tran M) . f =
(Mx2Tran (ML1 ^ ML2)) . (fp1 ^ fp2)
by A35, A60, A63, MATRTOP1:21
.=
((Mx2Tran ML1) . fp1) + ((Mx2Tran ML2) . fp2)
by A68, A64, MATRTOP1:36
.=
Mf1 + Mf2
by MATRTOP1:1
.=
(Sum L1) + (Sum L2)
by A70, A66, MATRIX13:102
.=
Sum L12
by VECTSP_6:44
;
for i being Nat st i in S holds
L12 . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))})))let w be
Nat;
( w in S implies L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))}))) )assume A73:
w in S
;
L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))
Line (
M,
w)
in lines M
by A73, MATRIX13:103;
then reconsider LMw =
Line (
M,
w) as
Element of
(m -VectSp_over F_Real) ;
p " (M " {LMw}) = (M * p) " {LMw}
by RELAT_1:146;
then A74:
Sum (Seq (f | (M " {LMw}))) =
Sum (Seq (fp | ((M * p) " {LMw})))
by A23, MATRTOP1:10
.=
Sum ((Seq (fp1 | (ML1 " {LMw}))) ^ (Seq (fp2 | (ML2 " {LMw}))))
by A7, A35, A61, A62, A63, A18, A30, A19, A31, MATRTOP1:13
.=
(Sum (Seq (fp1 | (ML1 " {LMw})))) + (Sum (Seq (fp2 | (ML2 " {LMw}))))
by RVSUM_1:75
;
set ppw =
(pp ") . w;
A75:
(pp ") . w in p " S
by A39, A73, FUNCT_1:def 6;
p . ((pp ") . w) = w
by A38, A73, FUNCT_1:35;
then A76:
(M * P) . ((pp ") . w) = M . w
by A37, A75, FUNCT_1:12;
reconsider ppw =
(pp ") . w as
Nat by A75;
A77:
M . w = LMw
by A73, MATRIX_0:52;
reconsider L1w =
L1 . LMw,
L2w =
L2 . LMw as
Element of
FR ;
A78:
L12 . LMw = L1w + L2w
by VECTSP_6:22;
per cases
( ppw in dom ML1 or ex z being Nat st
( z in dom ML2 & ppw = (len ML1) + z ) )
by A35, A37, A75, FINSEQ_1:25;
suppose A79:
ppw in dom ML1
;
L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))then A80:
ML1 . ppw = LMw
by A35, A76, A77, FINSEQ_1:def 7;
then A81:
LMw in rng ML1
by A79, FUNCT_1:def 3;
then
not
LMw in Carrier L2
by A22, A33, A69, A16, XBOOLE_0:3;
then A82:
L2 . LMw = 0. F_Real
by VECTSP_6:2;
not
LMw in rng ML2
by A22, A33, A16, A81, XBOOLE_0:3;
then
{LMw} misses rng ML2
by ZFMISC_1:50;
then
ML2 " {LMw} = {}
by RELAT_1:138;
then A83:
Sum (Seq (fp2 | (ML2 " {LMw}))) = 0
by RVSUM_1:72;
(
Line (
ML1,
ppw)
= ML1 . ppw &
ppw in (p " S) \ {((pp ") . j)} )
by A75, A42, A79, MATRIX_0:60, ZFMISC_1:56;
then
L1 . LMw = Sum (Seq (fp1 | (ML1 " {LMw})))
by A71, A80;
hence
L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))
by A74, A78, A82, A83, RLVECT_1:def 4;
verum end; suppose
ex
z being
Nat st
(
z in dom ML2 &
ppw = (len ML1) + z )
;
L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))then consider z being
Nat such that A84:
z in dom ML2
and A85:
ppw = (len ML1) + z
;
A86:
ML2 . z = LMw
by A35, A76, A77, A84, A85, FINSEQ_1:def 7;
then A87:
LMw in rng ML2
by A84, FUNCT_1:def 3;
then
not
LMw in Carrier L1
by A22, A33, A72, A16, XBOOLE_0:3;
then A88:
L1 . LMw = 0. F_Real
by VECTSP_6:2;
not
LMw in LM `
by A22, A16, A87, XBOOLE_0:3;
then
{LMw} misses rng ML1
by A33, ZFMISC_1:50;
then
ML1 " {LMw} = {}
by RELAT_1:138;
then A89:
Seq (fp1 | (ML1 " {LMw})) = <*> REAL
;
L1w + L2w = L2w + L1w
by RLVECT_1:def 2;
then A90:
L12 . LMw = L2 . LMw
by A78, A88, RLVECT_1:def 4;
A91:
dom ML2 = Seg (n -' (card (M " (LM `))))
by A7, A30, A31, FINSEQ_1:def 3;
A92:
ML2 . z = Line (
ML2,
z)
by A84, MATRIX_0:60;
then
ML2 " {LMw} = dom fp2
by A67, A84, A86, A91;
then A93:
fp2 | (ML2 " {LMw}) = fp2
;
L2 . LMw = Sum fp2
by A67, A84, A86, A92, A91;
hence
L12 . (Line (M,w)) = Sum (Seq (f | (M " {(Line (M,w))})))
by A74, A90, A89, A93, FINSEQ_3:116, RVSUM_1:72;
verum end; end;
end;
A94:
S1[ 0 ]
proof
let n,
m be
Nat;
for M being Matrix of n,m,F_Real
for f being n -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = 0 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )let M be
Matrix of
n,
m,
F_Real;
for f being n -element real-valued FinSequence
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = 0 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )let f be
n -element real-valued FinSequence;
for S being Subset of (Seg n) st ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = 0 holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )let S be
Subset of
(Seg n);
( ( n = 0 implies m = 0 ) & M | S is one-to-one & rng (M | S) = lines M & card (lines M) = 0 implies ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) ) )
assume that A95:
(
n = 0 implies
m = 0 )
and
M | S is
one-to-one
and
rng (M | S) = lines M
and A96:
card (lines M) = 0
;
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
reconsider L =
ZeroLC (m -VectSp_over F_Real) as
Linear_Combination of
lines M by VECTSP_6:5;
take
L
;
( Sum L = (Mx2Tran M) . f & ( for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) ) )
A97:
Sum L =
0. (m -VectSp_over F_Real)
by VECTSP_6:15
.=
0. (TOP-REAL m)
by Lm2
;
A98:
(
len M = n &
M = {} )
by A95, A96, MATRIX13:1;
thus
Sum L = (Mx2Tran M) . f
by A95, A98, A97;
for i being Nat st i in S holds
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))})))
let i be
Nat;
( i in S implies L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) )
thus
(
i in S implies
L . (Line (M,i)) = Sum (Seq (f | (M " {(Line (M,i))}))) )
by A98;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A94, A1);
then A99:
S1[ card (lines M)]
;
per cases
( n <> 0 or n = 0 )
;
suppose A100:
n = 0
;
for S being Subset of (Seg n) st M | S is one-to-one & rng (M | S) = lines M holds
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )let S be
Subset of
(Seg n);
( M | S is one-to-one & rng (M | S) = lines M implies ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) ) )assume
(
M | S is
one-to-one &
rng (M | S) = lines M )
;
ex L being Linear_Combination of lines M st
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )reconsider L =
ZeroLC (m -VectSp_over F_Real) as
Linear_Combination of
lines M by VECTSP_6:5;
take
L
;
( Sum L = (Mx2Tran M) . f & ( for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))}))) ) )thus Sum L =
0. (m -VectSp_over F_Real)
by VECTSP_6:15
.=
0. (TOP-REAL m)
by Lm2
.=
(Mx2Tran M) . f
by A100, MATRTOP1:def 3
;
for k being Nat st k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))})))thus
for
k being
Nat st
k in S holds
L . (Line (M,k)) = Sum (Seq (f | (M " {(Line (M,k))})))
by A100;
verum end;