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