let m, n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ;
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 ;
A11: ( len MV = m -' n & len MV >= the_rank_of MV ) by ;
A12: Indices MV = [:(Seg (m -' n)),(Seg m):] by ;
(Seg m) \ N c= Seg m by XBOOLE_1:36;
then A13: [:(Seg (m -' n)),((Seg m) \ N):] c= Indices MV by ;
A14: width A = m by ;
A15: len A = n by ;
lines MV c= Solutions_of (A,((len A) |-> (0. K)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lines MV or x in Solutions_of (A,((len A) |-> (0. K))) )
assume x in lines MV ; :: thesis: 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
.= len (Line (MV,k)) by CARD_1:def 7 ;
now :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ;
Col ((ColVec2Mx (Line (MV,k))),1) = Line (MV,k) by ;
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 ; :: thesis: verum
end;
then ColVec2Mx (Line (MV,k)) in Solutions_of (A,(0. (K,n,1))) by ;
then ColVec2Mx (Line (MV,k)) in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) by ;
hence x in Solutions_of (A,((len A) |-> (0. K))) by A17; :: thesis: verum
end;
then Lin (lines MV) is Subspace of Lin (Solutions_of (A,((len A) |-> (0. K)))) by ;
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 ;
A25: card ((Seg m) \ N) = m - n by ;
then A26: card (Seg (m -' n)) = card ((Seg m) \ N) by ;
EqSegm (MV,(Seg (m -' n)),((Seg m) \ N)) = 1. (K,(m -' n)) by ;
then m -' n <= the_rank_of MV by ;
then A27: the_rank_of MV = m -' n by ;
A28: the carrier of c= the carrier of (Lin (lines MV))
proof
set SN = (Seg m) \ N;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of or y in the carrier of (Lin (lines MV)) )
assume y in the carrier of ; :: thesis: y in the carrier of (Lin (lines MV))
then y in Solutions_of (A,((len A) |-> (0. K))) by ;
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 ;
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 A35: dom M = Seg (m -' n) by ;
reconsider M = M as FinSequence of the carrier of () by ;
reconsider M1 = FinS2MX M as Matrix of m -' n,m,K by A33;
now :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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); :: thesis: Line (M1,i) = a * (Line (MV,i))
thus Line (M1,i) = M1 . i by
.= a * (Line (MV,i)) by ; :: thesis: verum
end;
then consider L being Linear_Combination of lines MV such that
A37: L (#) (MX2FinS MV) = M1 by ;
reconsider SumL = Sum L, f = f as Element of m -tuples_on the carrier of K by ;
now :: thesis: for i being Nat st i in Seg m holds
SumL . i = f . i
let i be Nat; :: thesis: ( i in Seg m implies SumL . i = f . i )
assume A38: i in Seg m ; :: thesis: SumL . i = f . i
A39: (Seg m) \ N c= Seg m by XBOOLE_1:36;
A40: now :: thesis: Sum (Col (M1,i)) = f . i
per cases ( i in N or not i in N ) ;
suppose A41: i in N ; :: thesis: Sum (Col (M1,i)) = f . i
consider 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 ;
reconsider F = f as Element of () -tuples_on the carrier of K by ;
A46: rng (Sgm (Seg (m -' n))) = Seg (m -' n) by FINSEQ_1:def 13;
A47: rng (Sgm N) = N by ;
then consider x being object such that
A48: x in dom (Sgm N) and
A49: (Sgm N) . x = i by ;
reconsider x = x as Element of NAT by A48;
set L = Line (A,x);
A50: dom (mlt ((Line (A,x)),F)) = Seg m by ;
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 ;
A54: dom (Sgm N) = Seg (card N) by ;
then A55: dom mN = Seg n by ;
Indices (1. (K,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A56: [x,x] in Indices (1. (K,n)) by ;
A57: (Sgm N) . x in N by ;
then A58: ( F . ((Sgm N) . x) = F /. ((Sgm N) . x) & (Line (A,x)) . ((Sgm N) . x) = A * (x,((Sgm N) . x)) ) by ;
A59: x = () . x by
.= (Sgm (Seg n)) . x by FINSEQ_3:48 ;
now :: thesis: for j being Nat st j in dom mN & j <> x holds
mN . j = 0. K
let j be Nat; :: thesis: ( j in dom mN & j <> x implies mN . j = 0. K )
assume that
A60: j in dom mN and
A61: j <> x ; :: thesis: 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 ;
A63: (Sgm N) . j in N by ;
then A64: ( F . ((Sgm N) . j) = F /. ((Sgm N) . j) & (Line (A,x)) . ((Sgm N) . j) = A * (x,((Sgm N) . j)) ) by ;
thus mN . j = (mlt ((Line (A,x)),F)) . ((Sgm N) . j) by
.= (F /. ((Sgm N) . j)) * (A * (((Sgm (Seg n)) . x),((Sgm N) . j))) by
.= (F /. ((Sgm N) . j)) * ((1. (K,n)) * (x,j)) by
.= (F /. ((Sgm N) . j)) * (0. K) by
.= 0. K ; :: thesis: verum
end;
then Sum mN = mN . x by ;
then A65: Sum mN = (mlt ((Line (A,x)),F)) . ((Sgm N) . x) by
.= (F /. ((Sgm N) . x)) * (A * (((Sgm (Seg n)) . x),((Sgm N) . x))) by
.= (F /. ((Sgm N) . x)) * ((1. (K,n)) * (x,x)) by
.= (F /. ((Sgm N) . x)) * (1_ K) by
.= F /. i by A49
.= f . i by ;
A66: dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N)) by ;
A67: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by ;
then dom mSN = Seg (m -' n) by ;
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 ;
then A70: [x,1] in Indices (0. (K,(len A),1)) by ;
then A71: 0. K = (ColVec2Mx ((len A) |-> (0. K))) * (x,1) by
.= (Line (A,x)) "*" (Col (X,1)) by
.= Sum (mlt ((Line (A,x)),(Col (X,1)))) ;
reconsider mSN = mSN as Element of (m -' n) -tuples_on the carrier of K by ;
A72: width M1 = m by ;
now :: thesis: for j being Nat st j in Seg (m -' n) holds
(Col (M1,i)) . j = (- mSN) . j
let j be Nat; :: thesis: ( j in Seg (m -' n) implies (Col (M1,i)) . j = (- mSN) . j )
assume A73: j in Seg (m -' n) ; :: thesis: (Col (M1,i)) . j = (- mSN) . j
A74: j = (idseq (m -' n)) . j by
.= (Sgm (Seg (m -' n))) . j by FINSEQ_3:48 ;
A75: Line (M1,j) = M1 . j by
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (Line (MV,j)) by ;
A76: (Sgm ((Seg m) \ N)) . j in (Seg m) \ N by ;
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 ;
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
.= mSN . j by ;
A78: x = () . x by
.= (Sgm (Seg n)) . x by FINSEQ_3:48 ;
A79: [:(Seg (m -' n)),N:] c= Indices MV by ;
[j,i] in Indices MV by ;
then A80: [j,x] in Indices (Segm (MV,(Seg (m -' n)),N)) by ;
then A81: [j,x] in Indices ((Segm (A,(Seg n),((Seg m) \ N))) @) by ;
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
.= (- ((Segm (A,(Seg n),((Seg m) \ N))) @)) * (j,x) by
.= - (((Segm (A,(Seg n),((Seg m) \ N))) @) * (j,x)) by
.= - ((Segm (A,(Seg n),((Seg m) \ N))) * (x,j)) by
.= - (A * (x,((Sgm ((Seg m) \ N)) . j))) by ;
dom M1 = Seg (m -' n) by ;
hence (Col (M1,i)) . j = M1 * (j,i) by
.= (Line (M1,j)) . i by
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (- (A * (x,((Sgm ((Seg m) \ N)) . j)))) by
.= - ((f /. ((Sgm ((Seg m) \ N)) . j)) * (A * (x,((Sgm ((Seg m) \ N)) . j)))) by VECTSP_1:8
.= (- mSN) . j by ;
:: thesis: verum
end;
then Col (M1,i) = - mSN by ;
hence Sum (Col (M1,i)) = - (Sum mSN) by FVSUM_1:75
.= (- (Sum mSN)) + ((Sum mSN) + (Sum mN)) by
.= ((- (Sum mSN)) + (Sum mSN)) + (Sum mN) by RLVECT_1:def 3
.= (0. K) + (Sum mN) by VECTSP_1:19
.= f . i by ;
:: thesis: verum
end;
suppose A84: not i in N ; :: thesis: Sum (Col (M1,i)) = f . i
A85: rng (Sgm ((Seg m) \ N)) = (Seg m) \ N by ;
i in (Seg m) \ N by ;
then consider x being object such that
A86: x in dom (Sgm ((Seg m) \ N)) and
A87: (Sgm ((Seg m) \ N)) . x = i by ;
reconsider x = x as Element of NAT by A86;
A88: dom (Sgm ((Seg m) \ N)) = Seg (card ((Seg m) \ N)) by ;
then A89: Line (M1,x) = M1 . x by
.= (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 ;
then A90: [x,x] in Indices (1. (K,(m -' n))) by MATRIX_0:24;
x = (idseq (m -' n)) . x by
.= (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
.= (1. (K,(m -' n))) * (x,x) by
.= 1_ K by ;
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 ;
A95: width M1 = m by ;
A96: now :: thesis: for j being Nat st j in dom (Col (M1,i)) & x <> j holds
(Col (M1,i)) . j = 0. K
let j be Nat; :: thesis: ( 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 ; :: thesis: (Col (M1,i)) . j = 0. K
A99: Line (M1,j) = M1 . j by
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (Line (MV,j)) by A34, A92, A93, A97 ;
[j,x] in [:(Seg (m -' n)),(Seg (m -' n)):] by ;
then A100: [j,x] in Indices (1. (K,(m -' n))) by MATRIX_0:24;
j = (idseq (m -' n)) . j by
.= (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
.= (1. (K,(m -' n))) * (j,x) by
.= 0. K by ;
thus (Col (M1,i)) . j = M1 * (j,i) by
.= ((f /. ((Sgm ((Seg m) \ N)) . j)) * (Line (MV,j))) . i by
.= (f /. ((Sgm ((Seg m) \ N)) . j)) * (0. K) by
.= 0. K ; :: thesis: verum
end;
(Col (M1,i)) . x = M1 * (x,i) by
.= (Line (M1,x)) . i by
.= (f /. ((Sgm ((Seg m) \ N)) . x)) * (1_ K) by
.= f /. i by A87
.= f . i by ;
hence Sum (Col (M1,i)) = f . i by ; :: thesis: verum
end;
end;
end;
Carrier L c= lines MV by VECTSP_6:def 4;
hence SumL . i = f . i by ; :: thesis: 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 ; :: thesis: verum
end;
take MV ; :: thesis: ( 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 by ;
then the carrier of (Lin (lines MV)) c= the carrier of by ;
then the carrier of (Lin (lines MV)) = the carrier of 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 ; :: thesis: verum