let i be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) )

assume A1: ( 1 <= i & i <= width M ) ; :: thesis: 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)

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 1 <= i & i <= width M implies Col ((a * M),i) = a * (Col (M,i)) )

assume A1: ( 1 <= i & i <= width M ) ; :: thesis: 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

hence
Col ((a * M),i) = a * (Col (M,i))
by A5, A3, MATRIX_0:def 8; :: thesis: verum
let j be Nat; :: thesis: ( j in dom (a * M) implies (a * (Col (M,i))) . j = (a * M) * (j,i) )

assume A7: j in dom (a * M) ; :: thesis: (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; :: thesis: verum

end;assume A7: j in dom (a * M) ; :: thesis: (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; :: thesis: verum