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 = (width A) -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,(ColVec2Mx B)) by A1;

set Cf = ColVec2Mx f;

A3: len f = width A by A2, Th59;

then reconsider f = f as Element of (width A) -tuples_on the carrier of K by FINSEQ_2:92;

reconsider F = f as Element of ((width A) -VectSp_over K) by MATRIX13:102;

A4: ( len (ColVec2Mx B) = len B & len A = len (ColVec2Mx B) ) by A2, Th33, MATRIX_0:def 2;

( width A = 0 implies len A = 0 ) by A1, Th60;

then A5: the carrier of (Space_of_Solutions_of A) = Solutions_of (A,((len A) |-> (0. K))) by Def5;

A6: Solutions_of (A,b) c= F + (Space_of_Solutions_of A)

hence Solutions_of (A,b) is Coset of Space_of_Solutions_of A by VECTSP_4:def 6; :: thesis: verum

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 = (width A) -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,(ColVec2Mx B)) by A1;

set Cf = ColVec2Mx f;

A3: len f = width A by A2, Th59;

then reconsider f = f as Element of (width A) -tuples_on the carrier of K by FINSEQ_2:92;

reconsider F = f as Element of ((width A) -VectSp_over K) by MATRIX13:102;

A4: ( len (ColVec2Mx B) = len B & len A = len (ColVec2Mx B) ) by A2, Th33, MATRIX_0:def 2;

( width A = 0 implies len A = 0 ) by A1, Th60;

then A5: the carrier of (Space_of_Solutions_of A) = Solutions_of (A,((len A) |-> (0. K))) by Def5;

A6: Solutions_of (A,b) c= F + (Space_of_Solutions_of A)

proof

F + (Space_of_Solutions_of A) c= Solutions_of (A,b)
( len B = len ((- (1_ K)) * B) & (- (1_ K)) * (ColVec2Mx B) = ColVec2Mx ((- (1_ K)) * B) )
by Th30, CARD_1:def 7;

then A7: (ColVec2Mx B) + ((- (1_ K)) * (ColVec2Mx B)) = ColVec2Mx (B + ((- (1_ K)) * B)) by Th28

.= ColVec2Mx (B + (- B)) by FVSUM_1:59

.= ColVec2Mx ((len A) |-> (0. K)) by A4, FVSUM_1:26 ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Solutions_of (A,b) or y in F + (Space_of_Solutions_of A) )

assume y in Solutions_of (A,b) ; :: thesis: y in F + (Space_of_Solutions_of A)

then consider g being FinSequence of K such that

A8: y = g and

A9: ColVec2Mx g in Solutions_of (A,(ColVec2Mx B)) ;

len g = width A by A9, Th59;

then reconsider g = g as Element of (width A) -tuples_on the carrier of K by FINSEQ_2:92;

set Cg = ColVec2Mx g;

reconsider GF = g + ((- (1_ K)) * f) as Element of ((width A) -VectSp_over K) by MATRIX13:102;

A10: len f = len ((- (1_ K)) * f) by A3, CARD_1:def 7;

( width (ColVec2Mx B) = width ((- (1_ K)) * (ColVec2Mx B)) & (- (1_ K)) * (ColVec2Mx f) in Solutions_of (A,((- (1_ K)) * (ColVec2Mx B))) ) by A2, Th35, MATRIX_3:def 5;

then A11: (ColVec2Mx g) + ((- (1_ K)) * (ColVec2Mx f)) in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) by A9, A7, Th37;

(ColVec2Mx g) + ((- (1_ K)) * (ColVec2Mx f)) = (ColVec2Mx g) + (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 A5, STRUCT_0:def 5;

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

.= ((width A) |-> (0. K)) + g by FVSUM_1:26

.= g by FVSUM_1:21 ;

then F + GF = g by MATRIX13:102;

hence y in F + (Space_of_Solutions_of A) by A8, A12; :: thesis: verum

end;then A7: (ColVec2Mx B) + ((- (1_ K)) * (ColVec2Mx B)) = ColVec2Mx (B + ((- (1_ K)) * B)) by Th28

.= ColVec2Mx (B + (- B)) by FVSUM_1:59

.= ColVec2Mx ((len A) |-> (0. K)) by A4, FVSUM_1:26 ;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Solutions_of (A,b) or y in F + (Space_of_Solutions_of A) )

assume y in Solutions_of (A,b) ; :: thesis: y in F + (Space_of_Solutions_of A)

then consider g being FinSequence of K such that

A8: y = g and

A9: ColVec2Mx g in Solutions_of (A,(ColVec2Mx B)) ;

len g = width A by A9, Th59;

then reconsider g = g as Element of (width A) -tuples_on the carrier of K by FINSEQ_2:92;

set Cg = ColVec2Mx g;

reconsider GF = g + ((- (1_ K)) * f) as Element of ((width A) -VectSp_over K) by MATRIX13:102;

A10: len f = len ((- (1_ K)) * f) by A3, CARD_1:def 7;

( width (ColVec2Mx B) = width ((- (1_ K)) * (ColVec2Mx B)) & (- (1_ K)) * (ColVec2Mx f) in Solutions_of (A,((- (1_ K)) * (ColVec2Mx B))) ) by A2, Th35, MATRIX_3:def 5;

then A11: (ColVec2Mx g) + ((- (1_ K)) * (ColVec2Mx f)) in Solutions_of (A,(ColVec2Mx ((len A) |-> (0. K)))) by A9, A7, Th37;

(ColVec2Mx g) + ((- (1_ K)) * (ColVec2Mx f)) = (ColVec2Mx g) + (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 A5, STRUCT_0:def 5;

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

.= ((width A) |-> (0. K)) + g by FVSUM_1:26

.= g by FVSUM_1:21 ;

then F + GF = g by MATRIX13:102;

hence y in F + (Space_of_Solutions_of A) by A8, A12; :: thesis: verum

proof

then
F + (Space_of_Solutions_of A) = Solutions_of (A,b)
by A6;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in F + (Space_of_Solutions_of A) 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 (ColVec2Mx B) = 1 & width (ColVec2Mx ((len A) |-> (0. K))) = 1 ) or ( width (ColVec2Mx B) = 0 & width (ColVec2Mx ((len A) |-> (0. K))) = 0 ) ) by A4, A13, Th26, MATRIX_0:22;

ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;

then A15: (ColVec2Mx B) + (ColVec2Mx ((len A) |-> (0. K))) = ColVec2Mx B by A4, MATRIX_3:4;

assume y in F + (Space_of_Solutions_of A) ; :: thesis: y in Solutions_of (A,b)

then consider U being Element of ((width A) -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 (width A) -tuples_on the carrier of K by MATRIX13:102;

u in Solutions_of (A,((len A) |-> (0. K))) by A5, A16, STRUCT_0:def 5;

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 A19, Th59;

then ColVec2Mx (f + g) = (ColVec2Mx f) + (ColVec2Mx g) by A2, Th28, Th59;

then ColVec2Mx (f + g) in Solutions_of (A,(ColVec2Mx B)) by A2, A19, A14, A15, Th37;

then f + g in Solutions_of (A,b) ;

hence y in Solutions_of (A,b) by A17, A18, MATRIX13:102; :: thesis: verum

end;A13: ( len A = 0 or len A <> 0 ) ;

len ((len A) |-> (0. K)) = len A by CARD_1:def 7;

then A14: ( ( width (ColVec2Mx B) = 1 & width (ColVec2Mx ((len A) |-> (0. K))) = 1 ) or ( width (ColVec2Mx B) = 0 & width (ColVec2Mx ((len A) |-> (0. K))) = 0 ) ) by A4, A13, Th26, MATRIX_0:22;

ColVec2Mx ((len A) |-> (0. K)) = 0. (K,(len A),1) by Th32;

then A15: (ColVec2Mx B) + (ColVec2Mx ((len A) |-> (0. K))) = ColVec2Mx B by A4, MATRIX_3:4;

assume y in F + (Space_of_Solutions_of A) ; :: thesis: y in Solutions_of (A,b)

then consider U being Element of ((width A) -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 (width A) -tuples_on the carrier of K by MATRIX13:102;

u in Solutions_of (A,((len A) |-> (0. K))) by A5, A16, STRUCT_0:def 5;

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 A19, Th59;

then ColVec2Mx (f + g) = (ColVec2Mx f) + (ColVec2Mx g) by A2, Th28, Th59;

then ColVec2Mx (f + g) in Solutions_of (A,(ColVec2Mx B)) by A2, A19, A14, A15, Th37;

then f + g in Solutions_of (A,b) ;

hence y in Solutions_of (A,b) by A17, A18, MATRIX13:102; :: thesis: verum

hence Solutions_of (A,b) is Coset of Space_of_Solutions_of A by VECTSP_4:def 6; :: thesis: verum