A4:
width M = m
by A2, MATRIX_0:23;
then A5:
len (M @) = m
by A3, MATRIX_0:54;
A6:
len M = n
by A2, MATRIX_0:23;
then
width (M @) = n
by A3, A4, MATRIX_0:54;
then
M @ is Matrix of m,n,K
by A3, A5, MATRIX_0:20;
then consider M1 being Matrix of m,n,K such that
A7:
M1 = M @
;
A8:
width (ScalarXLine (M1,l,a)) = n
by A3, MATRIX_0:23;
then A9:
len ((ScalarXLine (M1,l,a)) @) = n
by A2, MATRIX_0:54;
len (ScalarXLine (M1,l,a)) = m
by A3, MATRIX_0:23;
then
width ((ScalarXLine (M1,l,a)) @) = m
by A2, A8, MATRIX_0:54;
then
(ScalarXLine (M1,l,a)) @ is Matrix of n,m,K
by A2, A9, MATRIX_0:20;
then consider M2 being Matrix of n,m,K such that
A10:
M2 = (ScalarXLine (M1,l,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,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,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,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) )
assume that A11:
i in dom M
and A12:
j in Seg (width M)
;
( ( j = l implies M2 * (i,j) = a * (M * (i,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) )
A13:
[i,j] in Indices M
by A11, A12, ZFMISC_1:87;
then A14:
[j,i] in Indices M1
by A7, MATRIX_0:def 6;
dom (ScalarXLine (M1,l,a)) =
Seg (len (ScalarXLine (M1,l,a)))
by FINSEQ_1:def 3
.=
Seg (len M1)
by Def2
.=
dom M1
by FINSEQ_1:def 3
;
then A15:
[j,i] in Indices (ScalarXLine (M1,l,a))
by A14, Th1;
A16:
(
j in dom M1 &
i in Seg (width M1) )
by A14, ZFMISC_1:87;
thus
(
j = l implies
M2 * (
i,
j)
= a * (M * (i,l)) )
( j <> l implies M2 * (i,j) = M * (i,j) )proof
A17:
[i,l] in Indices M
by A1, A11, ZFMISC_1:87;
assume A18:
j = l
;
M2 * (i,j) = a * (M * (i,l))
M2 * (
i,
j) =
(ScalarXLine (M1,l,a)) * (
j,
i)
by A10, A15, MATRIX_0:def 6
.=
a * (M1 * (l,i))
by A16, A18, Def2
.=
a * (M * (i,l))
by A7, A17, MATRIX_0:def 6
;
hence
M2 * (
i,
j)
= a * (M * (i,l))
;
verum
end;
thus
(
j <> l implies
M2 * (
i,
j)
= M * (
i,
j) )
verumproof
assume A19:
j <> l
;
M2 * (i,j) = M * (i,j)
M2 * (
i,
j) =
(ScalarXLine (M1,l,a)) * (
j,
i)
by A10, A15, MATRIX_0:def 6
.=
M1 * (
j,
i)
by A16, A19, Def2
.=
M * (
i,
j)
by A7, A13, 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,l)) ) & ( j <> l implies M2 * (i,j) = M * (i,j) ) ) ) )
by A2, A6, MATRIX_0:23; verum