let k, l, n, m, i be Nat; for K being Field
for a being Element of K
for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) holds
( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )
let K be Field; for a being Element of K
for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) holds
( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )
let a be Element of K; for M, M1 being Matrix of n,m,K st l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) holds
( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )
let M, M1 be Matrix of n,m,K; ( l in dom M & k in dom M & i in dom M & M1 = RlineXScalar (M,l,k,a) implies ( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) ) )
assume that
A1:
l in dom M
and
A2:
k in dom M
and
A3:
i in dom M
and
A4:
M1 = RlineXScalar (M,l,k,a)
; ( ( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) ) & ( i <> l implies Line (M1,i) = Line (M,i) ) )
thus
( i = l implies Line (M1,i) = (a * (Line (M,k))) + (Line (M,l)) )
( i <> l implies Line (M1,i) = Line (M,i) )proof
A5:
len ((a * (Line (M,k))) + (Line (M,l))) = width M
by CARD_1:def 7;
A6:
len (Line (M1,i)) = width M1
by MATRIX_0:def 7;
A7:
width M1 = width M
by Th1;
assume A8:
i = l
;
Line (M1,i) = (a * (Line (M,k))) + (Line (M,l))
now for j being Nat st 1 <= j & j <= len (Line (M1,i)) holds
(Line (M1,i)) . j = ((a * (Line (M,k))) + (Line (M,l))) . jlet j be
Nat;
( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = ((a * (Line (M,k))) + (Line (M,l))) . j )assume A9:
( 1
<= j &
j <= len (Line (M1,i)) )
;
(Line (M1,i)) . j = ((a * (Line (M,k))) + (Line (M,l))) . jA10:
j in Seg (width M1)
by A6, A9;
then A11:
(Line (M,l)) . j = M * (
l,
j)
by A7, MATRIX_0:def 7;
then consider a2 being
Element of
K such that A12:
a2 = (Line (M,l)) . j
;
(a * (Line (M,k))) . j = a * (M * (k,j))
by A2, A7, A10, Th3;
then consider a1 being
Element of
K such that A13:
a1 = (a * (Line (M,k))) . j
;
j in dom ((a * (Line (M,k))) + (Line (M,l)))
by A7, A5, A10, FINSEQ_1:def 3;
then A14:
((a * (Line (M,k))) + (Line (M,l))) . j =
the
addF of
K . (
a1,
a2)
by A13, A12, FUNCOP_1:22
.=
(a * (M * (k,j))) + (M * (l,j))
by A2, A7, A10, A11, A13, A12, Th3
;
thus (Line (M1,i)) . j =
M1 * (
i,
j)
by A10, MATRIX_0:def 7
.=
((a * (Line (M,k))) + (Line (M,l))) . j
by A1, A2, A4, A8, A7, A10, A14, Def3
;
verum end;
hence
Line (
M1,
i)
= (a * (Line (M,k))) + (Line (M,l))
by A6, A5, Th1;
verum
end;
thus
( i <> l implies Line (M1,i) = Line (M,i) )
verumproof
A15:
width M1 = width M
by Th1;
A16:
len (Line (M1,i)) = width M1
by MATRIX_0:def 7;
assume A17:
i <> l
;
Line (M1,i) = Line (M,i)
A18:
now for j being Nat st 1 <= j & j <= len (Line (M1,i)) holds
(Line (M1,i)) . j = (Line (M,i)) . jlet j be
Nat;
( 1 <= j & j <= len (Line (M1,i)) implies (Line (M1,i)) . j = (Line (M,i)) . j )assume A19:
( 1
<= j &
j <= len (Line (M1,i)) )
;
(Line (M1,i)) . j = (Line (M,i)) . jA20:
j in Seg (width M1)
by A16, A19;
hence (Line (M1,i)) . j =
M1 * (
i,
j)
by MATRIX_0:def 7
.=
M * (
i,
j)
by A2, A3, A4, A17, A15, A20, Def3
.=
(Line (M,i)) . j
by A15, A20, MATRIX_0:def 7
;
verum end;
len (Line (M,i)) = width M
by MATRIX_0:def 7;
hence
Line (
M1,
i)
= Line (
M,
i)
by A16, A18, Th1;
verum
end;