let m, i, n, j, k, l 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_1:def 8;
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:133;
then
(a * qK) + pK is
Element of
(width M) -tuples_on the
carrier of
K
by A4, FINSEQ_2:140;
then A11:
len ((a * qK) + pK) = width M
by FINSEQ_1:def 18;
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:28
.=
(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_1:def 8
.=
(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:133;
then
(a * qK) + pK is Element of (width M) -tuples_on the carrier of K
by A4, FINSEQ_2:140;
then
len ((a * qK) + pK) = width M
by FINSEQ_1:def 18;
then
width M1 = width M
by A6, MATRIX11:def 3;
hence M1 * i,j =
(Line M1,i) . j
by A2, MATRIX_1:def 8
.=
(Line M,i) . j
by A1, A6, A13, MATRIX11:28
.=
M * i,j
by A2, MATRIX_1:def 8
;
verum