let K be Field; :: thesis: for A being Matrix of K
for b being FinSequence of K st not Solutions_of (A,b) is empty holds
Solutions_of (A,b) is Coset of Space_of_Solutions_of A

let A be Matrix of K; :: thesis: for b being FinSequence of K st not Solutions_of (A,b) is empty holds
Solutions_of (A,b) is Coset of Space_of_Solutions_of A

let b be FinSequence of K; :: thesis: ( not Solutions_of (A,b) is empty implies Solutions_of (A,b) is Coset of Space_of_Solutions_of A )
set V = () -VectSp_over K;
reconsider B = b as Element of (len b) -tuples_on the carrier of K by FINSEQ_2:92;
set CB = ColVec2Mx B;
assume not Solutions_of (A,b) is empty ; :: thesis: Solutions_of (A,b) is Coset of Space_of_Solutions_of A
then consider x being object such that
A1: x in Solutions_of (A,B) ;
consider f being FinSequence of K such that
x = f and
A2: ColVec2Mx f in Solutions_of (A,()) by A1;
set Cf = ColVec2Mx f;
A3: len f = width A by ;
then reconsider f = f as Element of () -tuples_on the carrier of K by FINSEQ_2:92;
reconsider F = f as Element of (() -VectSp_over K) by MATRIX13:102;
A4: ( len () = len B & len A = len () ) by ;
( width A = 0 implies len A = 0 ) by ;
then A5: the carrier of = Solutions_of (A,((len A) |-> (0. K))) by Def5;
A6: Solutions_of (A,b) c= F +
proof
( len B = len ((- (1_ K)) * B) & (- (1_ K)) * () = ColVec2Mx ((- (1_ K)) * B) ) by ;
then A7: () + ((- (1_ K)) * ()) = ColVec2Mx (B + ((- (1_ K)) * B)) by Th28
.= ColVec2Mx (B + (- B)) by FVSUM_1:59
.= ColVec2Mx ((len A) |-> (0. K)) by ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Solutions_of (A,b) or y in F + )
assume y in Solutions_of (A,b) ; :: thesis: y in F +
then consider g being FinSequence of K such that
A8: y = g and
A9: ColVec2Mx g in Solutions_of (A,()) ;
len g = width A by ;
then reconsider g = g as Element of () -tuples_on the carrier of K by FINSEQ_2:92;
set Cg = ColVec2Mx g;
reconsider GF = g + ((- (1_ K)) * f) as Element of (() -VectSp_over K) by MATRIX13:102;
A10: len f = len ((- (1_ K)) * f) by ;
( width () = width ((- (1_ K)) * ()) & (- (1_ K)) * () in Solutions_of (A,((- (1_ K)) * ())) ) by ;
then A11: (ColVec2Mx g) + ((- (1_ K)) * ()) in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) by A9, A7, Th37;
() + ((- (1_ K)) * ()) = () + (ColVec2Mx ((- (1_ K)) * f)) by Th30
.= ColVec2Mx (g + ((- (1_ K)) * f)) by A3, A9, A10, Th28, Th59 ;
then g + ((- (1_ K)) * f) in Solutions_of (A,((len A) |-> (0. K))) by A11;
then A12: GF in Space_of_Solutions_of A by ;
f + (g + ((- (1_ K)) * f)) = f + (((- (1_ K)) * f) + g) by FINSEQOP:33
.= f + ((- f) + g) by FVSUM_1:59
.= (f + (- f)) + g by FINSEQOP:28
.= (() |-> (0. K)) + g by FVSUM_1:26
.= g by FVSUM_1:21 ;
then F + GF = g by MATRIX13:102;
hence y in F + by ; :: thesis: verum
end;
F + c= Solutions_of (A,b)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in F + or y in Solutions_of (A,b) )
A13: ( len A = 0 or len A <> 0 ) ;
len ((len A) |-> (0. K)) = len A by CARD_1:def 7;
then A14: ( ( width () = 1 & width (ColVec2Mx ((len A) |-> (0. K))) = 1 ) or ( width () = 0 & width (ColVec2Mx ((len A) |-> (0. K))) = 0 ) ) by ;
ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;
then A15: (ColVec2Mx B) + (ColVec2Mx ((len A) |-> (0. K))) = ColVec2Mx B by ;
assume y in F + ; :: thesis: y in Solutions_of (A,b)
then consider U being Element of (() -VectSp_over K) such that
A16: U in Space_of_Solutions_of A and
A17: y = F + U by VECTSP_4:42;
reconsider u = U as Element of () -tuples_on the carrier of K by MATRIX13:102;
u in Solutions_of (A,((len A) |-> (0. K))) by ;
then consider g being FinSequence of K such that
A18: u = g and
A19: ColVec2Mx g in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) ;
width A = len g by ;
then ColVec2Mx (f + g) = () + () by ;
then ColVec2Mx (f + g) in Solutions_of (A,()) by A2, A19, A14, A15, Th37;
then f + g in Solutions_of (A,b) ;
hence y in Solutions_of (A,b) by ; :: thesis: verum
end;
then F + = Solutions_of (A,b) by A6;
hence Solutions_of (A,b) is Coset of Space_of_Solutions_of A by VECTSP_4:def 6; :: thesis: verum