let K be Field; 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; 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; ( 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
; 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
(
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 ;
TARSKI:def 3 ( not y in Solutions_of (A,b) or y in F + (Space_of_Solutions_of A) )
assume
y in Solutions_of (
A,
b)
;
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;
verum
end;
F + (Space_of_Solutions_of A) c= Solutions_of (A,b)
proof
let y be
object ;
TARSKI:def 3 ( 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)
;
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;
verum
end;
then
F + (Space_of_Solutions_of A) = Solutions_of (A,b)
by A6;
hence
Solutions_of (A,b) is Coset of Space_of_Solutions_of A
by VECTSP_4:def 6; verum