let i, j, k, m, n be Nat; :: thesis: for K being Field
for a being Element of K
for X being Matrix of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let K be Field; :: thesis: for a being Element of K
for X being Matrix of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let a be Element of K; :: thesis: for X being Matrix of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let X be Matrix of K; :: thesis: for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let A9 be Matrix of m,n,K; :: thesis: for B9 being Matrix of m,k,K st X in Solutions_of (A9,B9) & j in Seg m holds
X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))

let B9 be Matrix of m,k,K; :: thesis: ( X in Solutions_of (A9,B9) & j in Seg m implies X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) )
assume that
A1: X in Solutions_of (A9,B9) and
A2: j in Seg m ; :: thesis: X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
consider X1 being Matrix of K such that
A3: X = X1 and
A4: len X1 = width A9 and
A5: width X1 = width B9 and
A6: A9 * X1 = B9 by A1;
set LAj = Line (A9,j);
set LAi = Line (A9,i);
set RA = RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))));
A7: len ((Line (A9,i)) + (a * (Line (A9,j)))) = width A9 by CARD_1:def 7;
then A8: len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = len A9 by MATRIX11:def 3;
set RX = (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1;
A9: width (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) = width A9 by ;
then A10: ( len ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) & width ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = width X1 ) by ;
A11: len A9 = len B9 by ;
then dom B9 = Seg (len (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j))))))) by ;
then A12: Indices ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) = Indices B9 by ;
set LBj = Line (B9,j);
set LBi = Line (B9,i);
set RB = RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))));
A13: Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = Indices B9 by MATRIX_0:26;
A14: len ((Line (B9,i)) + (a * (Line (B9,j)))) = width B9 by CARD_1:def 7;
then A15: width (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = width B9 by MATRIX11:def 3;
A16: ( len (a * (Line (A9,j))) = width A9 & len (Line (A9,i)) = width A9 ) by CARD_1:def 7;
A17: now :: thesis: for o, p being Nat st [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) holds
(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p)
A18: rng (a * (Line (B9,j))) c= the carrier of K by FINSEQ_1:def 4;
let o, p be Nat; :: thesis: ( [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) implies (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) )
assume A19: [o,p] in Indices (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) ; :: thesis: (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p)
A20: o in dom B9 by ;
A21: B9 * (o,p) = (Line (A9,o)) "*" (Col (X1,p)) by ;
reconsider CX = Col (X1,p) as Element of (width A9) -tuples_on the carrier of K by A4;
A22: len (Col (X1,p)) = width A9 by ;
A23: p in Seg (width B9) by ;
then ( B9 * (o,p) = (Line (B9,o)) . p & B9 * (j,p) = (Line (B9,j)) . p ) by MATRIX_0:def 7;
then reconsider LBop = (Line (B9,o)) . p, LBjp = (Line (B9,j)) . p as Element of the carrier of K ;
p in dom (a * (Line (B9,j))) by ;
then (a * (Line (B9,j))) . p in rng (a * (Line (B9,j))) by FUNCT_1:def 3;
then reconsider aLBjp = (a * (Line (B9,j))) . p as Element of K by A18;
len B9 = m by MATRIX_0:def 2;
then A24: dom B9 = Seg m by FINSEQ_1:def 3;
then [j,p] in Indices B9 by ;
then A25: B9 * (j,p) = (Line (A9,j)) "*" (Col (X1,p)) by ;
now :: thesis: ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p)
per cases ( o = i or o <> i ) ;
suppose A26: o = i ; :: thesis: ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p)
then Line ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),o) = (Line (A9,i)) + (a * (Line (A9,j))) by ;
hence ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = ((Line (A9,i)) + (a * (Line (A9,j)))) "*" CX by
.= Sum ((mlt ((Line (A9,i)),CX)) + (mlt ((a * (Line (A9,j))),CX))) by
.= Sum ((mlt ((Line (A9,i)),CX)) + (a * (mlt ((Line (A9,j)),CX)))) by FVSUM_1:68
.= (Sum (mlt ((Line (A9,i)),CX))) + (Sum (a * (mlt ((Line (A9,j)),CX)))) by FVSUM_1:76
.= (B9 * (o,p)) + (a * (B9 * (j,p))) by
.= LBop + (a * (B9 * (j,p))) by
.= LBop + (a * LBjp) by
.= LBop + aLBjp by
.= ((Line (B9,i)) + (a * (Line (B9,j)))) . p by
.= (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) by ;
:: thesis: verum
end;
suppose A27: o <> i ; :: thesis: ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p)
then Line ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),o) = Line (A9,o) by ;
hence ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) = (Line (A9,o)) "*" (Col (X1,p)) by
.= B9 * (o,p) by
.= (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) by ;
:: thesis: verum
end;
end;
end;
hence (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) * (o,p) = ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1) * (o,p) ; :: thesis: verum
end;
len (RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))) = len B9 by ;
then (RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))) * X1 = RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))) by ;
hence X in Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j))))))) by A3, A4, A5, A9, A15; :: thesis: verum