let m, n be Nat; for K being Field
for A being Matrix of n,m,K
for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 holds
ex MVectors being Matrix of m -' n,m,K st
( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )
let K be Field; for A being Matrix of n,m,K
for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 holds
ex MVectors being Matrix of m -' n,m,K st
( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )
let A be Matrix of n,m,K; for N being finite without_zero Subset of NAT st card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 holds
ex MVectors being Matrix of m -' n,m,K st
( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )
let N be finite without_zero Subset of NAT; ( card N = n & N c= Seg m & Segm (A,(Seg n),N) = 1. (K,n) & n > 0 & m -' n > 0 implies ex MVectors being Matrix of m -' n,m,K st
( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A ) )
assume that
A1:
card N = n
and
A2:
N c= Seg m
and
A3:
Segm (A,(Seg n),N) = 1. (K,n)
and
A4:
n > 0
and
A5:
m -' n > 0
; ex MVectors being Matrix of m -' n,m,K st
( Segm (MVectors,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MVectors,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MVectors) = Space_of_Solutions_of A )
Seg m <> {}
by A1, A2, A4, CARD_1:27, XBOOLE_1:3;
then A6:
m <> 0
;
consider MV being Matrix of m -' n,m,K such that
A7:
Segm (MV,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n))
and
A8:
Segm (MV,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @)
and
A9:
for l being Nat
for M being Matrix of m,l,K st ( for i being Nat holds
( not i in Seg l or ex j being Nat st
( j in Seg (m -' n) & Col (M,i) = Line (MV,j) ) or Col (M,i) = m |-> (0. K) ) ) holds
M in Solutions_of (A,(0. (K,n,l)))
by A1, A2, A3, A4, Th49;
A10:
width MV = m
by A5, MATRIX_0:23;
A11:
( len MV = m -' n & len MV >= the_rank_of MV )
by MATRIX13:74, MATRIX_0:def 2;
A12:
Indices MV = [:(Seg (m -' n)),(Seg m):]
by A5, MATRIX_0:23;
(Seg m) \ N c= Seg m
by XBOOLE_1:36;
then A13:
[:(Seg (m -' n)),((Seg m) \ N):] c= Indices MV
by A12, ZFMISC_1:95;
A14:
width A = m
by A4, MATRIX_0:23;
A15:
len A = n
by A4, MATRIX_0:23;
lines MV c= Solutions_of (A,((len A) |-> (0. K)))
proof
let x be
object ;
TARSKI:def 3 ( not x in lines MV or x in Solutions_of (A,((len A) |-> (0. K))) )
assume
x in lines MV
;
x in Solutions_of (A,((len A) |-> (0. K)))
then consider k being
Nat such that A16:
k in Seg (m -' n)
and A17:
x = Line (
MV,
k)
by MATRIX13:103;
set C =
ColVec2Mx (Line (MV,k));
A18:
m =
width MV
by A5, MATRIX_0:23
.=
len (Line (MV,k))
by CARD_1:def 7
;
now for i being Nat holds
( not i in Seg 1 or ex j being Nat st
( j in Seg (m -' n) & Col ((ColVec2Mx (Line (MV,k))),i) = Line (MV,j) ) or Col ((ColVec2Mx (Line (MV,k))),i) = m |-> (0. K) )let i be
Nat;
( not i in Seg 1 or ex j being Nat st
( j in Seg (m -' n) & Col ((ColVec2Mx (Line (MV,k))),i) = Line (MV,j) ) or Col ((ColVec2Mx (Line (MV,k))),i) = m |-> (0. K) )assume
i in Seg 1
;
( ex j being Nat st
( j in Seg (m -' n) & Col ((ColVec2Mx (Line (MV,k))),i) = Line (MV,j) ) or Col ((ColVec2Mx (Line (MV,k))),i) = m |-> (0. K) )then A19:
i = 1
by FINSEQ_1:2, TARSKI:def 1;
Col (
(ColVec2Mx (Line (MV,k))),1)
= Line (
MV,
k)
by A6, A18, Th26;
hence
( ex
j being
Nat st
(
j in Seg (m -' n) &
Col (
(ColVec2Mx (Line (MV,k))),
i)
= Line (
MV,
j) ) or
Col (
(ColVec2Mx (Line (MV,k))),
i)
= m |-> (0. K) )
by A16, A19;
verum end;
then
ColVec2Mx (Line (MV,k)) in Solutions_of (
A,
(0. (K,n,1)))
by A9, A18;
then
ColVec2Mx (Line (MV,k)) in Solutions_of (
A,
(ColVec2Mx ((len A) |-> (0. K))))
by A15, Th32;
hence
x in Solutions_of (
A,
((len A) |-> (0. K)))
by A17;
verum
end;
then
Lin (lines MV) is Subspace of Lin (Solutions_of (A,((len A) |-> (0. K))))
by A14, VECTSP_7:13;
then A20:
the carrier of (Lin (lines MV)) c= the carrier of (Lin (Solutions_of (A,((len A) |-> (0. K)))))
by VECTSP_4:def 2;
(m -' n) + 0 > 0
by A5;
then
m -' n >= 1
by NAT_1:19;
then A21:
Det (1. (K,(m -' n))) = 1_ K
by MATRIX_7:16;
A22:
0. K <> 1_ K
;
A23:
card (Seg m) = m
by FINSEQ_1:57;
then A24:
m -' n = m - n
by A1, A2, NAT_1:43, XREAL_1:233;
A25:
card ((Seg m) \ N) = m - n
by A1, A2, A23, CARD_2:44;
then A26:
card (Seg (m -' n)) = card ((Seg m) \ N)
by A24, FINSEQ_1:57;
EqSegm (MV,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n))
by A7, A24, A25, FINSEQ_1:57, MATRIX13:def 3;
then
m -' n <= the_rank_of MV
by A24, A25, A26, A13, A21, A22, MATRIX13:def 4;
then A27:
the_rank_of MV = m -' n
by A11, XXREAL_0:1;
A28:
the carrier of (Space_of_Solutions_of A) c= the carrier of (Lin (lines MV))
proof
set SN =
(Seg m) \ N;
let y be
object ;
TARSKI:def 3 ( not y in the carrier of (Space_of_Solutions_of A) or y in the carrier of (Lin (lines MV)) )
assume
y in the
carrier of
(Space_of_Solutions_of A)
;
y in the carrier of (Lin (lines MV))
then
y in Solutions_of (
A,
((len A) |-> (0. K)))
by A6, A14, Def5;
then consider f being
FinSequence of
K such that A29:
f = y
and A30:
ColVec2Mx f in Solutions_of (
A,
(ColVec2Mx ((len A) |-> (0. K))))
;
A31:
len f = m
by A14, A30, Th59;
deffunc H1(
Nat)
-> Element of
(width MV) -tuples_on the
carrier of
K =
(f /. ((Sgm ((Seg m) \ N)) . $1)) * (Line (MV,$1));
A32:
dom f = Seg (len f)
by FINSEQ_1:def 3;
consider M being
FinSequence of
(width MV) -tuples_on the
carrier of
K such that A33:
len M = m -' n
and A34:
for
j being
Nat st
j in dom M holds
M . j = H1(
j)
from FINSEQ_2:sch 1();
A35:
dom M = Seg (m -' n)
by A33, FINSEQ_1:def 3;
reconsider M =
M as
FinSequence of the
carrier of
(m -VectSp_over K) by A10, MATRIX13:102;
reconsider M1 =
FinS2MX M as
Matrix of
m -' n,
m,
K by A33;
now for i being Nat st i in Seg (m -' n) holds
ex a being Element of the carrier of K st Line (M1,i) = a * (Line (MV,i))let i be
Nat;
( i in Seg (m -' n) implies ex a being Element of the carrier of K st Line (M1,i) = a * (Line (MV,i)) )assume A36:
i in Seg (m -' n)
;
ex a being Element of the carrier of K st Line (M1,i) = a * (Line (MV,i))take a =
f /. ((Sgm ((Seg m) \ N)) . i);
Line (M1,i) = a * (Line (MV,i))thus Line (
M1,
i) =
M1 . i
by A36, MATRIX_0:52
.=
a * (Line (MV,i))
by A34, A35, A36
;
verum end;
then consider L being
Linear_Combination of
lines MV such that A37:
L (#) (MX2FinS MV) = M1
by A27, MATRIX13:105, MATRIX13:108;
reconsider SumL =
Sum L,
f =
f as
Element of
m -tuples_on the
carrier of
K by A31, FINSEQ_2:92, MATRIX13:102;
now for i being Nat st i in Seg m holds
SumL . i = f . ilet i be
Nat;
( i in Seg m implies SumL . i = f . i )assume A38:
i in Seg m
;
SumL . i = f . iA39:
(Seg m) \ N c= Seg m
by XBOOLE_1:36;
A40:
now Sum (Col (M1,i)) = f . iper cases
( i in N or not i in N )
;
suppose A41:
i in N
;
Sum (Col (M1,i)) = f . iconsider X being
Matrix of
K such that A42:
X = ColVec2Mx f
and A43:
len X = width A
and
width X = width (ColVec2Mx ((len A) |-> (0. K)))
and A44:
A * X = ColVec2Mx ((len A) |-> (0. K))
by A30;
A45:
f = Col (
X,1)
by A6, A42, Th26;
reconsider F =
f as
Element of
(width A) -tuples_on the
carrier of
K by A4, MATRIX_0:23;
A46:
rng (Sgm (Seg (m -' n))) = Seg (m -' n)
by FINSEQ_1:def 13;
A47:
rng (Sgm N) = N
by A2, FINSEQ_1:def 13;
then consider x being
object such that A48:
x in dom (Sgm N)
and A49:
(Sgm N) . x = i
by A41, FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A48;
set L =
Line (
A,
x);
A50:
dom (mlt ((Line (A,x)),F)) = Seg m
by A14, FINSEQ_2:124;
then consider mN,
mSN being
FinSequence of
K such that A51:
mN = (mlt ((Line (A,x)),F)) * (Sgm N)
and A52:
mSN = (mlt ((Line (A,x)),F)) * (Sgm ((Seg m) \ N))
and A53:
Sum (mlt ((Line (A,x)),F)) = (Sum mN) + (Sum mSN)
by A2, Lm7;
A54:
dom (Sgm N) = Seg (card N)
by A2, FINSEQ_3:40;
then A55:
dom mN = Seg n
by A1, A2, A47, A50, A51, RELAT_1:27;
Indices (1. (K,n)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A56:
[x,x] in Indices (1. (K,n))
by A1, A54, A48, ZFMISC_1:87;
A57:
(Sgm N) . x in N
by A47, A48, FUNCT_1:def 3;
then A58:
(
F . ((Sgm N) . x) = F /. ((Sgm N) . x) &
(Line (A,x)) . ((Sgm N) . x) = A * (
x,
((Sgm N) . x)) )
by A2, A14, A31, A32, MATRIX_0:def 7, PARTFUN1:def 6;
A59:
x =
(idseq n) . x
by A1, A54, A48, FINSEQ_2:49
.=
(Sgm (Seg n)) . x
by FINSEQ_3:48
;
now for j being Nat st j in dom mN & j <> x holds
mN . j = 0. Klet j be
Nat;
( j in dom mN & j <> x implies mN . j = 0. K )assume that A60:
j in dom mN
and A61:
j <> x
;
mN . j = 0. K
Indices (1. (K,n)) = [:(Seg n),(Seg n):]
by MATRIX_0:24;
then A62:
[x,j] in Indices (1. (K,n))
by A1, A54, A48, A55, A60, ZFMISC_1:87;
A63:
(Sgm N) . j in N
by A1, A47, A54, A55, A60, FUNCT_1:def 3;
then A64:
(
F . ((Sgm N) . j) = F /. ((Sgm N) . j) &
(Line (A,x)) . ((Sgm N) . j) = A * (
x,
((Sgm N) . j)) )
by A2, A14, A31, A32, MATRIX_0:def 7, PARTFUN1:def 6;
thus mN . j =
(mlt ((Line (A,x)),F)) . ((Sgm N) . j)
by A51, A60, FUNCT_1:12
.=
(F /. ((Sgm N) . j)) * (A * (((Sgm (Seg n)) . x),((Sgm N) . j)))
by A2, A14, A59, A63, A64, FVSUM_1:61
.=
(F /. ((Sgm N) . j)) * ((1. (K,n)) * (x,j))
by A3, A62, MATRIX13:def 1
.=
(F /. ((Sgm N) . j)) * (0. K)
by A61, A62, MATRIX_1:def 3
.=
0. K
;
verum end; then
Sum mN = mN . x
by A1, A54, A48, A55, MATRIX_3:12;
then A65:
Sum mN =
(mlt ((Line (A,x)),F)) . ((Sgm N) . x)
by A1, A54, A48, A51, A55, FUNCT_1:12
.=
(F /. ((Sgm N) . x)) * (A * (((Sgm (Seg n)) . x),((Sgm N) . x)))
by A2, A14, A59, A57, A58, FVSUM_1:61
.=
(F /. ((Sgm N) . x)) * ((1. (K,n)) * (x,x))
by A3, A56, MATRIX13:def 1
.=
(F /. ((Sgm N) . x)) * (1_ K)
by A56, MATRIX_1:def 3
.=
F /. i
by A49
.=
f . i
by A31, A32, A38, PARTFUN1:def 6
;
A66:
dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N))
by FINSEQ_3:40, XBOOLE_1:36;
A67:
rng (Sgm ((Seg m) \ N)) = (Seg m) \ N
by A39, FINSEQ_1:def 13;
then
dom mSN = Seg (m -' n)
by A24, A25, A50, A52, A66, RELAT_1:27, XBOOLE_1:36;
then A68:
len mSN = m -' n
by FINSEQ_1:def 3;
A69:
ColVec2Mx ((len A) |-> (0. K)) = 0. (
K,
(len A),1)
by Th32;
(
Indices (0. (K,(len A),1)) = [:(Seg (len A)),(Seg 1):] & 1
in Seg 1 )
by A4, A15, MATRIX_0:23;
then A70:
[x,1] in Indices (0. (K,(len A),1))
by A1, A15, A54, A48, ZFMISC_1:87;
then A71:
0. K =
(ColVec2Mx ((len A) |-> (0. K))) * (
x,1)
by A69, MATRIX_3:1
.=
(Line (A,x)) "*" (Col (X,1))
by A43, A44, A69, A70, MATRIX_3:def 4
.=
Sum (mlt ((Line (A,x)),(Col (X,1))))
;
reconsider mSN =
mSN as
Element of
(m -' n) -tuples_on the
carrier of
K by A68, FINSEQ_2:92;
A72:
width M1 = m
by A5, MATRIX_0:23;
now for j being Nat st j in Seg (m -' n) holds
(Col (M1,i)) . j = (- mSN) . jlet j be
Nat;
( j in Seg (m -' n) implies (Col (M1,i)) . j = (- mSN) . j )assume A73:
j in Seg (m -' n)
;
(Col (M1,i)) . j = (- mSN) . jA74:
j =
(idseq (m -' n)) . j
by A73, FINSEQ_2:49
.=
(Sgm (Seg (m -' n))) . j
by FINSEQ_3:48
;
A75:
Line (
M1,
j) =
M1 . j
by A73, MATRIX_0:52
.=
(f /. ((Sgm ((Seg m) \ N)) . j)) * (Line (MV,j))
by A34, A35, A73
;
A76:
(Sgm ((Seg m) \ N)) . j in (Seg m) \ N
by A24, A25, A67, A66, A73, FUNCT_1:def 3;
then
(
f /. ((Sgm ((Seg m) \ N)) . j) = F . ((Sgm ((Seg m) \ N)) . j) &
A * (
x,
((Sgm ((Seg m) \ N)) . j))
= (Line (A,x)) . ((Sgm ((Seg m) \ N)) . j) )
by A14, A31, A32, A39, MATRIX_0:def 7, PARTFUN1:def 6;
then A77:
(f /. ((Sgm ((Seg m) \ N)) . j)) * (A * (x,((Sgm ((Seg m) \ N)) . j))) =
(mlt ((Line (A,x)),F)) . ((Sgm ((Seg m) \ N)) . j)
by A14, A39, A76, FVSUM_1:61
.=
mSN . j
by A24, A25, A52, A66, A73, FUNCT_1:13
;
A78:
x =
(idseq n) . x
by A1, A54, A48, FINSEQ_2:49
.=
(Sgm (Seg n)) . x
by FINSEQ_3:48
;
A79:
[:(Seg (m -' n)),N:] c= Indices MV
by A2, A12, ZFMISC_1:95;
[j,i] in Indices MV
by A2, A12, A41, A73, ZFMISC_1:87;
then A80:
[j,x] in Indices (Segm (MV,(Seg (m -' n)),N))
by A47, A49, A46, A74, A79, MATRIX13:17;
then A81:
[j,x] in Indices ((Segm (A,(Seg n),((Seg m) \ N))) @)
by A8, Lm1;
then A82:
[x,j] in Indices (Segm (A,(Seg n),((Seg m) \ N)))
by MATRIX_0:def 6;
A83:
(Line (MV,j)) . i =
MV * (
((Sgm (Seg (m -' n))) . j),
((Sgm N) . x))
by A10, A38, A49, A74, MATRIX_0:def 7
.=
(- ((Segm (A,(Seg n),((Seg m) \ N))) @)) * (
j,
x)
by A8, A80, MATRIX13:def 1
.=
- (((Segm (A,(Seg n),((Seg m) \ N))) @) * (j,x))
by A81, MATRIX_3:def 2
.=
- ((Segm (A,(Seg n),((Seg m) \ N))) * (x,j))
by A82, MATRIX_0:def 6
.=
- (A * (x,((Sgm ((Seg m) \ N)) . j)))
by A82, A78, MATRIX13:def 1
;
dom M1 = Seg (m -' n)
by A33, FINSEQ_1:def 3;
hence (Col (M1,i)) . j =
M1 * (
j,
i)
by A73, MATRIX_0:def 8
.=
(Line (M1,j)) . i
by A38, A72, MATRIX_0:def 7
.=
(f /. ((Sgm ((Seg m) \ N)) . j)) * (- (A * (x,((Sgm ((Seg m) \ N)) . j))))
by A2, A10, A41, A75, A83, FVSUM_1:51
.=
- ((f /. ((Sgm ((Seg m) \ N)) . j)) * (A * (x,((Sgm ((Seg m) \ N)) . j))))
by VECTSP_1:8
.=
(- mSN) . j
by A73, A77, FVSUM_1:23
;
verum end; then
Col (
M1,
i)
= - mSN
by A33, FINSEQ_2:119;
hence Sum (Col (M1,i)) =
- (Sum mSN)
by FVSUM_1:75
.=
(- (Sum mSN)) + ((Sum mSN) + (Sum mN))
by A71, A45, A53, RLVECT_1:def 4
.=
((- (Sum mSN)) + (Sum mSN)) + (Sum mN)
by RLVECT_1:def 3
.=
(0. K) + (Sum mN)
by VECTSP_1:19
.=
f . i
by A65, RLVECT_1:def 4
;
verum end; suppose A84:
not
i in N
;
Sum (Col (M1,i)) = f . iA85:
rng (Sgm ((Seg m) \ N)) = (Seg m) \ N
by A39, FINSEQ_1:def 13;
i in (Seg m) \ N
by A38, A84, XBOOLE_0:def 5;
then consider x being
object such that A86:
x in dom (Sgm ((Seg m) \ N))
and A87:
(Sgm ((Seg m) \ N)) . x = i
by A85, FUNCT_1:def 3;
reconsider x =
x as
Element of
NAT by A86;
A88:
dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N))
by FINSEQ_3:40, XBOOLE_1:36;
then A89:
Line (
M1,
x) =
M1 . x
by A24, A25, A86, MATRIX_0:52
.=
(f /. ((Sgm ((Seg m) \ N)) . x)) * (Line (MV,x))
by A24, A25, A34, A35, A88, A86
;
[x,x] in [:(Seg (m -' n)),(Seg (m -' n)):]
by A24, A25, A88, A86, ZFMISC_1:87;
then A90:
[x,x] in Indices (1. (K,(m -' n)))
by MATRIX_0:24;
x =
(idseq (m -' n)) . x
by A24, A25, A88, A86, FINSEQ_2:49
.=
(Sgm (Seg (m -' n))) . x
by FINSEQ_3:48
;
then A91:
(Line (MV,x)) . i =
MV * (
((Sgm (Seg (m -' n))) . x),
((Sgm ((Seg m) \ N)) . x))
by A10, A38, A87, MATRIX_0:def 7
.=
(1. (K,(m -' n))) * (
x,
x)
by A7, A90, MATRIX13:def 1
.=
1_ K
by A90, MATRIX_1:def 3
;
A92:
dom (Col (M1,i)) = Seg (len M1)
by FINSEQ_2:124;
A93:
dom M1 = Seg (len M1)
by FINSEQ_1:def 3;
A94:
len M1 = m - n
by A5, A24, MATRIX_0:23;
A95:
width M1 = m
by A5, MATRIX_0:23;
A96:
now for j being Nat st j in dom (Col (M1,i)) & x <> j holds
(Col (M1,i)) . j = 0. Klet j be
Nat;
( j in dom (Col (M1,i)) & x <> j implies (Col (M1,i)) . j = 0. K )assume that A97:
j in dom (Col (M1,i))
and A98:
x <> j
;
(Col (M1,i)) . j = 0. KA99:
Line (
M1,
j) =
M1 . j
by A92, A97, MATRIX_0:52
.=
(f /. ((Sgm ((Seg m) \ N)) . j)) * (Line (MV,j))
by A34, A92, A93, A97
;
[j,x] in [:(Seg (m -' n)),(Seg (m -' n)):]
by A24, A25, A88, A86, A92, A94, A97, ZFMISC_1:87;
then A100:
[j,x] in Indices (1. (K,(m -' n)))
by MATRIX_0:24;
j =
(idseq (m -' n)) . j
by A24, A92, A94, A97, FINSEQ_2:49
.=
(Sgm (Seg (m -' n))) . j
by FINSEQ_3:48
;
then A101:
(Line (MV,j)) . i =
MV * (
((Sgm (Seg (m -' n))) . j),
((Sgm ((Seg m) \ N)) . x))
by A10, A38, A87, MATRIX_0:def 7
.=
(1. (K,(m -' n))) * (
j,
x)
by A7, A100, MATRIX13:def 1
.=
0. K
by A98, A100, MATRIX_1:def 3
;
thus (Col (M1,i)) . j =
M1 * (
j,
i)
by A92, A93, A97, MATRIX_0:def 8
.=
((f /. ((Sgm ((Seg m) \ N)) . j)) * (Line (MV,j))) . i
by A38, A95, A99, MATRIX_0:def 7
.=
(f /. ((Sgm ((Seg m) \ N)) . j)) * (0. K)
by A10, A38, A101, FVSUM_1:51
.=
0. K
;
verum end; (Col (M1,i)) . x =
M1 * (
x,
i)
by A25, A88, A86, A94, A93, MATRIX_0:def 8
.=
(Line (M1,x)) . i
by A38, A95, MATRIX_0:def 7
.=
(f /. ((Sgm ((Seg m) \ N)) . x)) * (1_ K)
by A10, A38, A91, A89, FVSUM_1:51
.=
f /. i
by A87
.=
f . i
by A31, A32, A38, PARTFUN1:def 6
;
hence
Sum (Col (M1,i)) = f . i
by A25, A88, A86, A92, A94, A96, MATRIX_3:12;
verum end;
Carrier L c= lines MV
by VECTSP_6:def 4;
hence
SumL . i = f . i
by A27, A37, A38, A40, MATRIX13:105, MATRIX13:107;
verum end;
then A102:
SumL = f
by FINSEQ_2:119;
the
carrier of
(Lin (lines MV)) = { (Sum l) where l is Linear_Combination of lines MV : verum }
by VECTSP_7:def 2;
hence
y in the
carrier of
(Lin (lines MV))
by A29, A102;
verum
end;
take
MV
; ( Segm (MV,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MV,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MV) = Space_of_Solutions_of A )
Solutions_of (A,((len A) |-> (0. K))) = the carrier of (Space_of_Solutions_of A)
by A6, A14, Def5;
then
the carrier of (Lin (lines MV)) c= the carrier of (Space_of_Solutions_of A)
by A20, VECTSP_7:11;
then
the carrier of (Lin (lines MV)) = the carrier of (Space_of_Solutions_of A)
by A28;
hence
( Segm (MV,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) & Segm (MV,(Seg (m -' n)),N) = - ((Segm (A,(Seg n),((Seg m) \ N))) @) & Lin (lines MV) = Space_of_Solutions_of A )
by A14, A7, A8, VECTSP_4:29; verum