let j, 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
for pK, qK being FinSequence of K st i in Seg n & j in Seg (width M) & k in dom M & pK = Line (M,l) & qK = Line (M,k) & M1 = RLine (M,l,((a * qK) + pK)) holds
( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let K be Field; for a being Element of K
for M, M1 being Matrix of n,m,K
for pK, qK being FinSequence of K st i in Seg n & j in Seg (width M) & k in dom M & pK = Line (M,l) & qK = Line (M,k) & M1 = RLine (M,l,((a * qK) + pK)) holds
( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let a be Element of K; for M, M1 being Matrix of n,m,K
for pK, qK being FinSequence of K st i in Seg n & j in Seg (width M) & k in dom M & pK = Line (M,l) & qK = Line (M,k) & M1 = RLine (M,l,((a * qK) + pK)) holds
( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let M, M1 be Matrix of n,m,K; for pK, qK being FinSequence of K st i in Seg n & j in Seg (width M) & k in dom M & pK = Line (M,l) & qK = Line (M,k) & M1 = RLine (M,l,((a * qK) + pK)) holds
( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
let pK, qK be FinSequence of K; ( i in Seg n & j in Seg (width M) & k in dom M & pK = Line (M,l) & qK = Line (M,k) & M1 = RLine (M,l,((a * qK) + pK)) implies ( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (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:
k in dom M
and
A4:
pK = Line (M,l)
and
A5:
qK = Line (M,k)
and
A6:
M1 = RLine (M,l,((a * qK) + pK))
; ( ( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) ) & ( i <> l implies M1 * (i,j) = M * (i,j) ) )
thus
( i = l implies M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j)) )
( i <> l implies M1 * (i,j) = M * (i,j) )proof
(a * (Line (M,k))) . j = a * (M * (k,j))
by A2, A3, Th3;
then consider a1 being
Element of
K such that A7:
a1 = (a * (Line (M,k))) . j
;
assume A8:
i = l
;
M1 * (i,j) = (a * (M * (k,j))) + (M * (l,j))
A9:
(Line (M,l)) . j = M * (
l,
j)
by A2, MATRIX_0:def 7;
then consider a2 being
Element of
K such that A10:
a2 = (Line (M,l)) . j
;
a * qK is
Element of
(width M) -tuples_on the
carrier of
K
by A5, FINSEQ_2:113;
then
(a * qK) + pK is
Element of
(width M) -tuples_on the
carrier of
K
by A4, FINSEQ_2:120;
then A11:
len ((a * qK) + pK) = width M
by CARD_1:def 7;
then
j in dom ((a * qK) + pK)
by A2, FINSEQ_1:def 3;
then A12:
((a * qK) + pK) . j =
the
addF of
K . (
a1,
a2)
by A4, A5, A7, A10, FUNCOP_1:22
.=
(a * (M * (k,j))) + (M * (l,j))
by A2, A3, A9, A7, A10, Th3
;
width M1 = width M
by A6, A11, MATRIX11:def 3;
then M1 * (
i,
j) =
(Line (M1,i)) . j
by A2, MATRIX_0:def 7
.=
(a * (M * (k,j))) + (M * (l,j))
by A1, A6, A8, A11, A12, MATRIX11:28
;
hence
M1 * (
i,
j)
= (a * (M * (k,j))) + (M * (l,j))
;
verum
end;
assume A13:
i <> l
; M1 * (i,j) = M * (i,j)
a * qK is Element of (width M) -tuples_on the carrier of K
by A5, FINSEQ_2:113;
then
(a * qK) + pK is Element of (width M) -tuples_on the carrier of K
by A4, FINSEQ_2:120;
then
len ((a * qK) + pK) = width M
by CARD_1:def 7;
then
width M1 = width M
by A6, MATRIX11:def 3;
hence M1 * (i,j) =
(Line (M1,i)) . j
by A2, MATRIX_0:def 7
.=
(Line (M,i)) . j
by A1, A6, A13, MATRIX11:28
.=
M * (i,j)
by A2, MATRIX_0:def 7
;
verum