let m, n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: 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 :: thesis: 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; :: thesis: ( [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 ; :: thesis: 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 :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
suppose i <> i9 ; :: thesis: C * (I,J) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (I,J)
hence C * (I,J) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (I,J) by A7, A8, MATRIX11:def 3; :: thesis: verum
end;
end;
end;
hence C * (i9,j9) = (RLine (C,i,((Line (C,i)) + (a * (Line (C,j)))))) * (i9,j9) ; :: thesis: 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; :: thesis: verum