let m, n be Nat; for K being Field
for a being Element of K
for A9 being Matrix of m,n,K
for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A9 = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))
let K be Field; for a being Element of K
for A9 being Matrix of m,n,K
for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A9 = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))
let a be Element of K; for A9 being Matrix of m,n,K
for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A9 = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))
let A9 be Matrix of m,n,K; for i, j being Nat st j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) holds
Space_of_Solutions_of A9 = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))
let i, j be Nat; ( j in Seg m & n > 0 & ( i = j implies a <> - (1_ K) ) implies Space_of_Solutions_of A9 = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) )
assume that
A1:
j in Seg m
and
A2:
n > 0
and
A3:
( i = j implies a <> - (1_ K) )
; Space_of_Solutions_of A9 = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))
set L = (len A9) |-> (0. K);
set R = RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))));
A4:
m <> 0
by A1;
then A5:
width (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = n
by MATRIX_0:23;
len ((len A9) |-> (0. K)) = len A9
by CARD_1:def 7;
then
len ((len A9) |-> (0. K)) = m
by MATRIX_0:def 2;
then reconsider C = ColVec2Mx ((len A9) |-> (0. K)) as Matrix of m,1,K ;
set RC = RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))));
A6:
C = 0. (K,(len A9),1)
by Th32;
now for i9, j9 being Nat st [i9,j9] in Indices C holds
C * (i9,j9) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (i9,j9)let i9,
j9 be
Nat;
( [i9,j9] in Indices C implies C * (i9,j9) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (i9,j9) )assume A7:
[i9,j9] in Indices C
;
C * (i9,j9) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (i9,j9)reconsider I =
i9,
J =
j9 as
Element of
NAT by ORDINAL1:def 12;
A8:
len ((Line (C,i)) + (a * (Line (C,j)))) = width C
by CARD_1:def 7;
now C * (I,J) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (I,J)per cases
( i9 = i or i <> i9 )
;
suppose A9:
i9 = i
;
C * (I,J) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (I,J)A10:
1
= width C
by A4, MATRIX_0:23;
then A11:
j9 in Seg 1
by A7, ZFMISC_1:87;
then
(Line (C,j)) . j9 = C * (
j,
j9)
by A10, MATRIX_0:def 7;
then A12:
(a * (Line (C,j))) . j9 = a * (C * (j,j9))
by A10, A11, FVSUM_1:51;
Indices C = [:(Seg m),(Seg 1):]
by A4, MATRIX_0:23;
then A13:
[j,j9] in Indices C
by A1, A11, ZFMISC_1:87;
(Line (C,i)) . j9 = C * (
i,
j9)
by A10, A11, MATRIX_0:def 7;
then ((Line (C,i)) + (a * (Line (C,j)))) . j9 =
(C * (i,j9)) + (a * (C * (j,j9)))
by A10, A11, A12, FVSUM_1:18
.=
(0. K) + (a * (C * (j,j9)))
by A6, A7, A9, MATRIX_3:1
.=
(0. K) + (a * (0. K))
by A6, A13, MATRIX_3:1
.=
(0. K) + (0. K)
.=
0. K
by RLVECT_1:def 4
.=
C * (
i9,
j9)
by A6, A7, MATRIX_3:1
;
hence
C * (
I,
J)
= (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (
I,
J)
by A7, A8, A9, MATRIX11:def 3;
verum end; end; end; hence
C * (
i9,
j9)
= (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (
i9,
j9)
;
verum end;
then
RLine (C,i,((Line (C,i)) + (a * (Line (C,j))))) = C
by MATRIX_0:27;
then A14:
Solutions_of (A9,C) = Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),C)
by A1, A3, Th40;
set SR = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))));
( len A9 = m & len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = m )
by A4, MATRIX_0:23;
then A15:
the carrier of (Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))) = Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),((len A9) |-> (0. K)))
by A2, A5, Def5;
set SA = Space_of_Solutions_of A9;
A16:
width A9 = n
by A4, MATRIX_0:23;
then
the carrier of (Space_of_Solutions_of A9) = Solutions_of (A9,((len A9) |-> (0. K)))
by A2, Def5;
hence
Space_of_Solutions_of A9 = Space_of_Solutions_of (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))
by A16, A5, A14, A15, VECTSP_4:29; verum