let n, m be Nat; :: thesis: 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 one-to-one & 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; :: thesis: for M being Matrix of n,m,K
for i, j being Nat
for a being Element of K st M is one-to-one & 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; :: thesis: for i, j being Nat
for a being Element of K st M is one-to-one & 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; :: thesis: for a being Element of K st M is one-to-one & 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; :: thesis: ( M is one-to-one & 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 one-to-one & j in dom M )
and
A2:
( i = j implies a <> - (1_ K) )
; :: thesis: Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))
A3:
( dom M = Seg (len M) & len M = n )
by FINSEQ_1:def 3, MATRIX_1:def 3;
set L = (Line M,i) + (a * (Line M,j));
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 A4:
i in dom M
;
:: thesis: Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))reconsider L' =
(Line M,i) + (a * (Line M,j)) as
Element of the
carrier of
K * by FINSEQ_1:def 11;
reconsider LL =
L' as
set ;
n <> 0
by A3, A4;
then
n > 0
;
then A5:
width M = m
by MATRIX_1:24;
then reconsider Li =
Line M,
i,
Lj =
Line M,
j as
Vector of
(m -VectSp_over K) by MATRIX13:102;
set iL =
{i} --> L';
len ((Line M,i) + (a * (Line M,j))) = width M
by FINSEQ_1:def 18;
then A6:
RLine M,
i,
((Line M,i) + (a * (Line M,j))) =
M +* i,
LL
by MATRIX11:29
.=
M +* (i .--> LL)
by A4, FUNCT_7:def 3
.=
M +* ({i} --> L')
by FUNCOP_1:def 9
;
a * Lj = a * (Line M,j)
by A5, MATRIX13:102;
then A7:
(Line M,i) + (a * (Line M,j)) = Li + (a * Lj)
by A5, MATRIX13:102;
M .: ((dom M) \ (dom ({i} --> L'))) =
(M .: (dom M)) \ (M .: (dom ({i} --> L')))
by A1, FUNCT_1:123
.=
(rng M) \ (M .: (dom ({i} --> L')))
by RELAT_1:146
.=
(rng M) \ (Im M,i)
by FUNCOP_1:19
.=
(rng M) \ {(M . i)}
by A4, FUNCT_1:117
.=
(rng M) \ {(Line M,i)}
by A4, A3, MATRIX_2:10
;
then A8:
lines (RLine M,i,((Line M,i) + (a * (Line M,j)))) =
((lines M) \ {(Line M,i)}) \/ (rng ({i} --> L'))
by A6, FRECHET:12
.=
((lines M) \ {(Line M,i)}) \/ {((Line M,i) + (a * (Line M,j)))}
by FUNCOP_1:14
;
A9:
(
Li in lines M &
Lj in lines M )
by A1, A3, A4, MATRIX13:103;
( not
Li = Lj or
a <> - (1_ K) or
Li = 0. (m -VectSp_over K) )
hence
Lin (lines M) = Lin (lines (RLine M,i,((Line M,i) + (a * (Line M,j)))))
by A7, A8, A9, Th14;
:: thesis: verum end;