A5:
width M = m
by A3, MATRIX_0:23;
then A6:
len (M @) = m
by A4, MATRIX_0:54;
A7:
len M = n
by A3, MATRIX_0:23;
then
width (M @) = n
by A4, A5, MATRIX_0:54;
then
M @ is Matrix of m,n,K
by A4, A6, MATRIX_0:20;
then consider M1 being Matrix of m,n,K such that
A8:
M1 = M @
;
A9:
width (RlineXScalar (M1,l,k,a)) = n
by A4, MATRIX_0:23;
then A10:
len ((RlineXScalar (M1,l,k,a)) @) = n
by A3, MATRIX_0:54;
len (RlineXScalar (M1,l,k,a)) = m
by A4, MATRIX_0:23;
then
width ((RlineXScalar (M1,l,k,a)) @) = m
by A3, A9, MATRIX_0:54;
then
(RlineXScalar (M1,l,k,a)) @ is Matrix of n,m,K
by A3, A10, MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A11:
M2 = (RlineXScalar (M1,l,k,a)) @
;
take
M2
; ( len M2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) ) )
for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) )
proof
let i,
j be
Nat;
( i in dom M & j in Seg (width M) implies ( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) )
assume that A12:
i in dom M
and A13:
j in Seg (width M)
;
( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) )
A14:
[i,j] in Indices M
by A12, A13, ZFMISC_1:87;
then A15:
[j,i] in Indices M1
by A8, MATRIX_0:def 6;
then A16:
i in Seg (width M1)
by ZFMISC_1:87;
A17:
len M1 = width M
by A8, MATRIX_0:def 6;
then A18:
k in dom M1
by A2, FINSEQ_1:def 3;
dom (RlineXScalar (M1,l,k,a)) =
Seg (len (RlineXScalar (M1,l,k,a)))
by FINSEQ_1:def 3
.=
Seg (len M1)
by A18, Def3
.=
dom M1
by FINSEQ_1:def 3
;
then A19:
[j,i] in Indices (RlineXScalar (M1,l,k,a))
by A15, Th1;
A20:
l in dom M1
by A1, A17, FINSEQ_1:def 3;
thus
(
j = l implies
M2 * (
i,
j)
= (a * (M * (i,k))) + (M * (i,l)) )
( j <> l implies M2 * (i,j) = M * (i,j) )proof
A21:
[i,k] in Indices M
by A2, A12, ZFMISC_1:87;
A22:
[i,l] in Indices M
by A1, A12, ZFMISC_1:87;
assume A23:
j = l
;
M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l))
M2 * (
i,
j) =
(RlineXScalar (M1,l,k,a)) * (
j,
i)
by A11, A19, MATRIX_0:def 6
.=
(a * (M1 * (k,i))) + (M1 * (l,i))
by A20, A18, A16, A23, Def3
.=
(a * (M * (i,k))) + (M1 * (l,i))
by A8, A21, MATRIX_0:def 6
.=
(a * (M * (i,k))) + (M * (i,l))
by A8, A22, MATRIX_0:def 6
;
hence
M2 * (
i,
j)
= (a * (M * (i,k))) + (M * (i,l))
;
verum
end;
A24:
j in dom M1
by A15, ZFMISC_1:87;
thus
(
j <> l implies
M2 * (
i,
j)
= M * (
i,
j) )
verumproof
assume A25:
j <> l
;
M2 * (i,j) = M * (i,j)
M2 * (
i,
j) =
(RlineXScalar (M1,l,k,a)) * (
j,
i)
by A11, A19, MATRIX_0:def 6
.=
M1 * (
j,
i)
by A18, A24, A16, A25, Def3
.=
M * (
i,
j)
by A8, A14, MATRIX_0:def 6
;
hence
M2 * (
i,
j)
= M * (
i,
j)
;
verum
end;
end;
hence
( len M2 = len M & ( for i, j being Nat st i in dom M & j in Seg (width M) holds
( ( j = l implies M2 * (i,j) = (a * (M * (i,k))) + (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) ) )
by A3, A7, MATRIX_0:23; verum