let m, n be Nat; for K being Field
for M, M1 being Matrix of m,n,K st M is without_repeated_line & ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) holds
ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1
let K be Field; for M, M1 being Matrix of m,n,K st M is without_repeated_line & ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) holds
ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1
let M, M1 be Matrix of m,n,K; ( M is without_repeated_line & ( for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i)) ) implies ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1 )
assume that
A1:
M is without_repeated_line
and
A2:
for i being Nat st i in Seg m holds
ex a being Element of K st Line (M1,i) = a * (Line (M,i))
; ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1
set V = n -VectSp_over K;
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 (M,i)) );
A3:
for k being Nat st k in Seg (len M) holds
ex x being Element of K st S1[k,x]
consider p being FinSequence of K such that
A6:
dom p = Seg (len M)
and
A7:
for k being Nat st k in Seg (len M) holds
S1[k,p . k]
from FINSEQ_1:sch 5(A3);
defpred S2[ object , object ] means for v being Vector of (n -VectSp_over K) st $1 = v holds
( ( not v in lines M implies $2 = 0. K ) & ( v in lines M implies for k being Nat st k in Seg m & v = Line (M,k) holds
$2 = p . k ) );
A8:
for x being object st x in the carrier of (n -VectSp_over K) holds
ex y being object st
( y in the carrier of K & S2[x,y] )
proof
let x be
object ;
( x in the carrier of (n -VectSp_over K) implies ex y being object st
( y in the carrier of K & S2[x,y] ) )
assume
x in the
carrier of
(n -VectSp_over K)
;
ex y being object st
( y in the carrier of K & S2[x,y] )
then reconsider v =
x as
Element of
(n -VectSp_over K) ;
per cases
( v in lines M or not v in lines M )
;
suppose A9:
v in lines M
;
ex y being object st
( y in the carrier of K & S2[x,y] )A10:
rng p c= the
carrier of
K
by FINSEQ_1:def 4;
consider j being
Nat such that A11:
j in Seg m
and A12:
v = Line (
M,
j)
by A9, Th103;
len M = m
by MATRIX_0:def 2;
then
p . j in rng p
by A6, A11, FUNCT_1:def 3;
then reconsider pj =
p . j as
Element of the
carrier of
K by A10;
take
pj
;
( pj in the carrier of K & S2[x,pj] )thus
pj in the
carrier of
K
;
S2[x,pj]let w be
Vector of
(n -VectSp_over K);
( x = w implies ( ( not w in lines M implies pj = 0. K ) & ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
pj = p . k ) ) )assume A13:
w = x
;
( ( not w in lines M implies pj = 0. K ) & ( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
pj = p . k ) )thus
( not
w in lines M implies
pj = 0. K )
by A9, A13;
( w in lines M implies for k being Nat st k in Seg m & w = Line (M,k) holds
pj = p . k )thus
(
w in lines M implies for
k being
Nat st
k in Seg m &
w = Line (
M,
k) holds
pj = p . k )
verumproof
len M = m
by MATRIX_0:def 2;
then A14:
dom M = Seg m
by FINSEQ_1:def 3;
A15:
M . j = Line (
M,
j)
by A11, MATRIX_0:52;
assume
w in lines M
;
for k being Nat st k in Seg m & w = Line (M,k) holds
pj = p . k
let k be
Nat;
( k in Seg m & w = Line (M,k) implies pj = p . k )
assume that A16:
k in Seg m
and A17:
w = Line (
M,
k)
;
pj = p . k
M . k = Line (
M,
k)
by A16, MATRIX_0:52;
hence
pj = p . k
by A1, A11, A12, A13, A16, A17, A14, A15;
verum
end; end;
end;
consider l being Function of the carrier of (n -VectSp_over K), the carrier of K such that
A20:
for x being object st x in the carrier of (n -VectSp_over K) holds
S2[x,l . x]
from FUNCT_2:sch 1(A8);
reconsider L = l as Element of Funcs ( the carrier of (n -VectSp_over K), the carrier of K) by FUNCT_2:8;
for v being Vector of (n -VectSp_over K) st not v in lines M holds
L . v = 0. K
by A20;
then reconsider L = L as Linear_Combination of n -VectSp_over K by VECTSP_6:def 1;
A21:
Carrier L c= lines M
set MX = MX2FinS M;
A22:
len M = m
by MATRIX_0:def 2;
reconsider L = L as Linear_Combination of lines M by A21, VECTSP_6:def 4;
set LM = L (#) (MX2FinS M);
A23:
len (L (#) (MX2FinS M)) = len M
by VECTSP_6:def 5;
A24:
now for k being Nat st 1 <= k & k <= m holds
M1 . k = (L (#) (MX2FinS M)) . klet k be
Nat;
( 1 <= k & k <= m implies M1 . k = (L (#) (MX2FinS M)) . k )assume that A25:
1
<= k
and A26:
k <= m
;
M1 . k = (L (#) (MX2FinS M)) . kA27:
k in Seg m
by A25, A26;
then consider a being
Element of
K such that A28:
p . k = a
and A29:
Line (
M1,
k)
= a * (Line (M,k))
by A7, A22;
dom (MX2FinS M) = Seg m
by A22, FINSEQ_1:def 3;
then A30:
(MX2FinS M) /. k = M . k
by A27, PARTFUN1:def 6;
A31:
Line (
M,
k)
in lines M
by A27, Th103;
then reconsider LMk =
Line (
M,
k) as
Element of
n -tuples_on the
carrier of
K by Th102;
A32:
LMk = M . k
by A27, MATRIX_0:52;
dom (L (#) (MX2FinS M)) = Seg m
by A22, A23, FINSEQ_1:def 3;
then A33:
(L (#) (MX2FinS M)) . k = (L . ((MX2FinS M) /. k)) * ((MX2FinS M) /. k)
by A27, VECTSP_6:def 5;
L . LMk = p . k
by A20, A27, A31;
then
(L (#) (MX2FinS M)) . k = a * LMk
by A28, A33, A30, A32, Th102;
hence
M1 . k = (L (#) (MX2FinS M)) . k
by A27, A29, MATRIX_0:52;
verum end;
len M1 = m
by MATRIX_0:def 2;
hence
ex L being Linear_Combination of lines M st L (#) (MX2FinS M) = M1
by A22, A23, A24, FINSEQ_1:14; verum