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:110;
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 set such that
A1:
x in Solutions_of A,B
by XBOOLE_0:def 1;
consider f being FinSequence of K such that
A2:
( x = f & 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:110;
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_1:def 3;
( 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
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in Solutions_of A,b or y in F + (Space_of_Solutions_of A) )
assume A7:
y in Solutions_of A,
b
;
:: thesis: y in F + (Space_of_Solutions_of A)
consider g being
FinSequence of
K such that A8:
(
y = g &
ColVec2Mx g in Solutions_of A,
(ColVec2Mx B) )
by A7;
len g = width A
by A8, Th59;
then reconsider g =
g as
Element of
(width A) -tuples_on the
carrier of
K by FINSEQ_2:110;
reconsider GF =
g + ((- (1_ K)) * f) as
Element of
((width A) -VectSp_over K) by MATRIX13:102;
set Cg =
ColVec2Mx g;
A9:
width (ColVec2Mx B) = width ((- (1_ K)) * (ColVec2Mx B))
by MATRIX_3:def 5;
A10:
(
len B = len ((- (1_ K)) * B) &
len f = len ((- (1_ K)) * f) )
by A3, FINSEQ_1:def 18;
(- (1_ K)) * (ColVec2Mx B) = ColVec2Mx ((- (1_ K)) * B)
by Th30;
then A11:
(ColVec2Mx B) + ((- (1_ K)) * (ColVec2Mx B)) =
ColVec2Mx (B + ((- (1_ K)) * B))
by Th28, A10
.=
ColVec2Mx (B + (- B))
by FVSUM_1:72
.=
ColVec2Mx ((len A) |-> (0. K))
by A4, FVSUM_1:35
;
A12:
(ColVec2Mx g) + ((- (1_ K)) * (ColVec2Mx f)) =
(ColVec2Mx g) + (ColVec2Mx ((- (1_ K)) * f))
by Th30
.=
ColVec2Mx (g + ((- (1_ K)) * f))
by A3, Th28, A10, A8, Th59
;
f + (g + ((- (1_ K)) * f)) =
f + (((- (1_ K)) * f) + g)
by FINSEQOP:34
.=
f + ((- f) + g)
by FVSUM_1:72
.=
(f + (- f)) + g
by FINSEQOP:29
.=
((width A) |-> (0. K)) + g
by FVSUM_1:35
.=
g
by FVSUM_1:28
;
then A13:
F + GF = g
by MATRIX13:102;
(- (1_ K)) * (ColVec2Mx f) in Solutions_of A,
((- (1_ K)) * (ColVec2Mx B))
by A2, Th35;
then
(ColVec2Mx g) + ((- (1_ K)) * (ColVec2Mx f)) in Solutions_of A,
(ColVec2Mx ((len A) |-> (0. K)))
by A8, A11, A9, Th37;
then
g + ((- (1_ K)) * f) in Solutions_of A,
((len A) |-> (0. K))
by A12;
then
GF in Space_of_Solutions_of A
by A5, STRUCT_0:def 5;
hence
y in F + (Space_of_Solutions_of A)
by A8, A13;
:: thesis: verum
end;
F + (Space_of_Solutions_of A) c= Solutions_of A,b
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in F + (Space_of_Solutions_of A) or y in Solutions_of A,b )
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 A14:
(
U in Space_of_Solutions_of A &
y = F + U )
by VECTSP_4:57;
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 A14, A5, STRUCT_0:def 5;
then consider g being
FinSequence of
K such that A15:
(
u = g &
ColVec2Mx g in Solutions_of A,
(ColVec2Mx ((len A) |-> (0. K))) )
;
width A = len g
by A15, Th59;
then A16:
ColVec2Mx (f + g) = (ColVec2Mx f) + (ColVec2Mx g)
by A2, Th59, Th28;
(
len ((len A) |-> (0. K)) = len A & (
len A = 0 or
len A <> 0 ) )
by FINSEQ_1:def 18;
then A17:
( (
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, Th26, MATRIX_1:23;
ColVec2Mx ((len A) |-> (0. K)) = 0. K,
(len A),1
by Th32;
then
(ColVec2Mx B) + (ColVec2Mx ((len A) |-> (0. K))) = ColVec2Mx B
by A4, MATRIX_3:6;
then
ColVec2Mx (f + g) in Solutions_of A,
(ColVec2Mx B)
by A2, A15, A16, A17, Th37;
then
f + g in Solutions_of A,
b
;
hence
y in Solutions_of A,
b
by A14, A15, MATRIX13:102;
:: thesis: verum
end;
then
F + (Space_of_Solutions_of A) = Solutions_of A,b
by A6, XBOOLE_0:def 10;
hence
Solutions_of A,b is Coset of Space_of_Solutions_of A
by VECTSP_4:def 6; :: thesis: verum