let i be Nat; for K being Field
for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let K be Field; for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let a be Element of K; for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))
let M be Matrix of K; ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) )
assume A1:
( 1 <= i & i <= width M )
; Col ((a * M),i) = a * (Col (M,i))
A2:
Seg (len (a * M)) = dom (a * M)
by FINSEQ_1:def 3;
A3:
len (a * M) = len M
by MATRIX_3:def 5;
then A4:
dom M = dom (a * M)
by FINSEQ_3:29;
A5:
( len (a * (Col (M,i))) = len (Col (M,i)) & len (Col (M,i)) = len M )
by Th16, MATRIX_0:def 8;
then A6:
dom (a * (Col (M,i))) = Seg (len (a * M))
by A3, FINSEQ_1:def 3;
for j being Nat st j in dom (a * M) holds
(a * (Col (M,i))) . j = (a * M) * (j,i)
proof
let j be
Nat;
( j in dom (a * M) implies (a * (Col (M,i))) . j = (a * M) * (j,i) )
assume A7:
j in dom (a * M)
;
(a * (Col (M,i))) . j = (a * M) * (j,i)
i in Seg (width M)
by A1, FINSEQ_1:1;
then
[j,i] in Indices M
by A4, A7, ZFMISC_1:87;
then A8:
(a * M) * (
j,
i)
= a * (M * (j,i))
by MATRIX_3:def 5;
(Col (M,i)) . j = M * (
j,
i)
by A4, A7, MATRIX_0:def 8;
hence
(a * (Col (M,i))) . j = (a * M) * (
j,
i)
by A6, A2, A7, A8, FVSUM_1:50;
verum
end;
hence
Col ((a * M),i) = a * (Col (M,i))
by A5, A3, MATRIX_0:def 8; verum