let n, m be Nat; for K being Field
for a being Element of K
for l being Nat
for M, M1 being Matrix of n,m,K
for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line (M,l) & M1 = RLine (M,l,(a * pK)) holds
( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let K be Field; for a being Element of K
for l being Nat
for M, M1 being Matrix of n,m,K
for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line (M,l) & M1 = RLine (M,l,(a * pK)) holds
( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let a be Element of K; for l being Nat
for M, M1 being Matrix of n,m,K
for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line (M,l) & M1 = RLine (M,l,(a * pK)) holds
( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let l be Nat; for M, M1 being Matrix of n,m,K
for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line (M,l) & M1 = RLine (M,l,(a * pK)) holds
( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let M, M1 be Matrix of n,m,K; for pK being FinSequence of K
for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line (M,l) & M1 = RLine (M,l,(a * pK)) holds
( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let pK be FinSequence of K; for i, j being Nat st i in Seg n & j in Seg (width M) & pK = Line (M,l) & M1 = RLine (M,l,(a * pK)) holds
( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let i, j be Nat; ( i in Seg n & j in Seg (width M) & pK = Line (M,l) & M1 = RLine (M,l,(a * pK)) implies ( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) ) )
assume that
A1:
i in Seg n
and
A2:
j in Seg (width M)
and
A3:
pK = Line (M,l)
and
A4:
M1 = RLine (M,l,(a * pK))
; ( ( i = l implies M1 * (i,j) = a * (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
thus
( i = l implies M1 * (i,j) = a * (M * (l,j)) )
( i <> l implies M1 * (i,j) = M * (i,j) )proof
assume A5:
i = l
;
M1 * (i,j) = a * (M * (l,j))
len M = n
by MATRIX_0:def 2;
then A6:
l in dom M
by A1, A5, FINSEQ_1:def 3;
A7:
len (a * (Line (M,l))) = width M
by CARD_1:def 7;
then
width M1 = width M
by A3, A4, MATRIX11:def 3;
then M1 * (
i,
j) =
(Line (M1,i)) . j
by A2, MATRIX_0:def 7
.=
(a * (Line (M,l))) . j
by A1, A3, A4, A5, A7, MATRIX11:28
.=
a * (M * (l,j))
by A2, A6, Th3
;
hence
M1 * (
i,
j)
= a * (M * (l,j))
;
verum
end;
assume A8:
i <> l
; M1 * (i,j) = M * (i,j)
len (a * (Line (M,l))) = width M
by CARD_1:def 7;
then
width M1 = width M
by A3, A4, MATRIX11:def 3;
hence M1 * (i,j) =
(Line (M1,i)) . j
by A2, MATRIX_0:def 7
.=
(Line (M,i)) . j
by A1, A4, A8, MATRIX11:28
.=
M * (i,j)
by A2, MATRIX_0:def 7
;
verum