let i, j, k, m, n be Nat; for K being Field
for a being Element of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
Solutions_of (A9,B9) = 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; for a being Element of K
for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
Solutions_of (A9,B9) = 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; for A9 being Matrix of m,n,K
for B9 being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
Solutions_of (A9,B9) = 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; for B9 being Matrix of m,k,K st j in Seg m & ( i = j implies a <> - (1_ K) ) holds
Solutions_of (A9,B9) = 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; ( j in Seg m & ( i = j implies a <> - (1_ K) ) implies Solutions_of (A9,B9) = 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:
j in Seg m
and
A2:
( i = j implies a <> - (1_ K) )
; Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
per cases
( i <> j or i = j )
;
suppose
i <> j
;
Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))hence
Solutions_of (
A9,
B9)
= Solutions_of (
(RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),
(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))
by A1, Lm5;
verum end; suppose A3:
i = j
;
Solutions_of (A9,B9) = Solutions_of ((RLine (A9,i,((Line (A9,i)) + (a * (Line (A9,j)))))),(RLine (B9,i,((Line (B9,i)) + (a * (Line (B9,j)))))))A4:
(1_ K) + a <> 0. K
set LB =
Line (
B9,
i);
set LA =
Line (
A9,
i);
A5:
(Line (B9,i)) + (a * (Line (B9,i))) =
((1_ K) * (Line (B9,i))) + (a * (Line (B9,i)))
by FVSUM_1:57
.=
((1_ K) + a) * (Line (B9,i))
by FVSUM_1:55
;
(Line (A9,i)) + (a * (Line (A9,i))) =
((1_ K) * (Line (A9,i))) + (a * (Line (A9,i)))
by FVSUM_1:57
.=
((1_ K) + a) * (Line (A9,i))
by FVSUM_1:55
;
hence
Solutions_of (
A9,
B9)
= 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, Lm4;
verum end; end;