let m, n be Nat; for K being Field
for M being Matrix of n,m,K
for i, j being Nat
for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))
let K be Field; for M being Matrix of n,m,K
for i, j being Nat
for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))
let M be Matrix of n,m,K; for i, j being Nat
for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))
let i, j be Nat; for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))
let a be Element of K; ( M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) implies Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))))) )
assume that
A1:
M is without_repeated_line
and
A2:
j in dom M
and
A3:
( i = j implies a <> - (1_ K) )
; Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))
A4:
len M = n
by MATRIX_0:def 2;
set L = (Line (M,i)) + (a * (Line (M,j)));
A5:
dom M = Seg (len M)
by FINSEQ_1:def 3;
set R = RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))));
per cases
( not i in dom M or i in dom M )
;
suppose A6:
i in dom M
;
Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))then
n <> 0
by A5, A4;
then A7:
width M = m
by MATRIX_0:23;
then reconsider Li =
Line (
M,
i),
Lj =
Line (
M,
j) as
Vector of
(m -VectSp_over K) by MATRIX13:102;
a * Lj = a * (Line (M,j))
by A7, MATRIX13:102;
then A8:
(Line (M,i)) + (a * (Line (M,j))) = Li + (a * Lj)
by A7, MATRIX13:102;
A9:
( not
Li = Lj or
a <> - (1_ K) or
Li = 0. (m -VectSp_over K) )
reconsider L9 =
(Line (M,i)) + (a * (Line (M,j))) as
Element of the
carrier of
K * by FINSEQ_1:def 11;
reconsider LL =
L9 as
set ;
set iL =
{i} --> L9;
len ((Line (M,i)) + (a * (Line (M,j)))) = width M
by CARD_1:def 7;
then A11:
RLine (
M,
i,
((Line (M,i)) + (a * (Line (M,j))))) =
M +* (
i,
LL)
by MATRIX11:29
.=
M +* (i .--> LL)
by A6, FUNCT_7:def 3
.=
M +* ({i} --> L9)
by FUNCOP_1:def 9
;
M .: ((dom M) \ (dom ({i} --> L9))) =
(M .: (dom M)) \ (M .: (dom ({i} --> L9)))
by A1, FUNCT_1:64
.=
(rng M) \ (M .: (dom ({i} --> L9)))
by RELAT_1:113
.=
(rng M) \ (Im (M,i))
.=
(rng M) \ {(M . i)}
by A6, FUNCT_1:59
.=
(rng M) \ {(Line (M,i))}
by A5, A4, A6, MATRIX_0:52
;
then A12:
lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) =
((lines M) \ {(Line (M,i))}) \/ (rng ({i} --> L9))
by A11, FRECHET:12
.=
((lines M) \ {(Line (M,i))}) \/ {((Line (M,i)) + (a * (Line (M,j))))}
by FUNCOP_1:8
;
A13:
Lj in lines M
by A2, A5, A4, MATRIX13:103;
Li in lines M
by A5, A4, A6, MATRIX13:103;
hence
Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))
by A8, A12, A13, A9, Th14;
verum end; end;