let K be Field; :: thesis: for j being Nat

for A, B being Matrix of K st len A = len B & ex i being Nat st [i,j] in Indices A holds

Col ((A + B),j) = (Col (A,j)) + (Col (B,j))

let j be Nat; :: thesis: for A, B being Matrix of K st len A = len B & ex i being Nat st [i,j] in Indices A holds

Col ((A + B),j) = (Col (A,j)) + (Col (B,j))

let A, B be Matrix of K; :: thesis: ( len A = len B & ex i being Nat st [i,j] in Indices A implies Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) )

A1: len (A + B) = len A by MATRIX_3:def 3;

assume A2: len A = len B ; :: thesis: ( for i being Nat holds not [i,j] in Indices A or Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) )

then reconsider a = Col (A,j), b = Col (B,j) as Element of (len A) -tuples_on the carrier of K ;

given i being Nat such that A3: [i,j] in Indices A ; :: thesis: Col ((A + B),j) = (Col (A,j)) + (Col (B,j))

A4: width (A + B) = width A by MATRIX_3:def 3;

then A5: Indices (A + B) = Indices A by A1, Th55;

A6: for k being Nat st 1 <= k & k <= len (Col ((A + B),j)) holds

(Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k

.= len A by CARD_1:def 7 ;

len (Col ((A + B),j)) = len A by A1, MATRIX_0:def 8;

hence Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) by A17, A6, FINSEQ_1:14; :: thesis: verum

for A, B being Matrix of K st len A = len B & ex i being Nat st [i,j] in Indices A holds

Col ((A + B),j) = (Col (A,j)) + (Col (B,j))

let j be Nat; :: thesis: for A, B being Matrix of K st len A = len B & ex i being Nat st [i,j] in Indices A holds

Col ((A + B),j) = (Col (A,j)) + (Col (B,j))

let A, B be Matrix of K; :: thesis: ( len A = len B & ex i being Nat st [i,j] in Indices A implies Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) )

A1: len (A + B) = len A by MATRIX_3:def 3;

assume A2: len A = len B ; :: thesis: ( for i being Nat holds not [i,j] in Indices A or Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) )

then reconsider a = Col (A,j), b = Col (B,j) as Element of (len A) -tuples_on the carrier of K ;

given i being Nat such that A3: [i,j] in Indices A ; :: thesis: Col ((A + B),j) = (Col (A,j)) + (Col (B,j))

A4: width (A + B) = width A by MATRIX_3:def 3;

then A5: Indices (A + B) = Indices A by A1, Th55;

A6: for k being Nat st 1 <= k & k <= len (Col ((A + B),j)) holds

(Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k

proof

A17: len ((Col (A,j)) + (Col (B,j))) =
len (a + b)
let k be Nat; :: thesis: ( 1 <= k & k <= len (Col ((A + B),j)) implies (Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k )

assume A7: ( 1 <= k & k <= len (Col ((A + B),j)) ) ; :: thesis: (Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k

A8: len (Col ((A + B),j)) = len A by A1, MATRIX_0:def 8;

then k in Seg (len A) by A7, FINSEQ_1:1;

then A9: k in dom (A + B) by A1, FINSEQ_1:def 3;

len (Col (B,j)) = len B by MATRIX_0:def 8;

then k in Seg (len (Col (B,j))) by A2, A7, A8, FINSEQ_1:1;

then k in dom (Col (B,j)) by FINSEQ_1:def 3;

then reconsider e = (Col (B,j)) . k as Element of K by FINSEQ_2:11;

A10: dom A = Seg (len A) by FINSEQ_1:def 3

.= dom B by A2, FINSEQ_1:def 3 ;

A11: len (Col (A,j)) = len A by MATRIX_0:def 8;

then A12: k in Seg (len (Col (A,j))) by A7, A8, FINSEQ_1:1;

then k in dom (Col (A,j)) by FINSEQ_1:def 3;

then reconsider d = (Col (A,j)) . k as Element of K by FINSEQ_2:11;

len ((Col (A,j)) + (Col (B,j))) = len (a + b)

.= len A by CARD_1:def 7

.= len (Col (A,j)) by CARD_1:def 7 ;

then k in dom ((Col (A,j)) + (Col (B,j))) by A12, FINSEQ_1:def 3;

then A13: ((Col (A,j)) + (Col (B,j))) . k = d + e by FVSUM_1:17;

j in Seg (width (A + B)) by A3, A4, ZFMISC_1:87;

then A14: [k,j] in Indices (A + B) by A9, ZFMISC_1:87;

A15: (Col ((A + B),j)) . k = (A + B) * (k,j) by A9, MATRIX_0:def 8

.= (A * (k,j)) + (B * (k,j)) by A5, A14, MATRIX_3:def 3 ;

A16: k in dom A by A11, A12, FINSEQ_1:def 3;

then (Col (A,j)) . k = A * (k,j) by MATRIX_0:def 8;

hence (Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k by A15, A13, A10, A16, MATRIX_0:def 8; :: thesis: verum

end;assume A7: ( 1 <= k & k <= len (Col ((A + B),j)) ) ; :: thesis: (Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k

A8: len (Col ((A + B),j)) = len A by A1, MATRIX_0:def 8;

then k in Seg (len A) by A7, FINSEQ_1:1;

then A9: k in dom (A + B) by A1, FINSEQ_1:def 3;

len (Col (B,j)) = len B by MATRIX_0:def 8;

then k in Seg (len (Col (B,j))) by A2, A7, A8, FINSEQ_1:1;

then k in dom (Col (B,j)) by FINSEQ_1:def 3;

then reconsider e = (Col (B,j)) . k as Element of K by FINSEQ_2:11;

A10: dom A = Seg (len A) by FINSEQ_1:def 3

.= dom B by A2, FINSEQ_1:def 3 ;

A11: len (Col (A,j)) = len A by MATRIX_0:def 8;

then A12: k in Seg (len (Col (A,j))) by A7, A8, FINSEQ_1:1;

then k in dom (Col (A,j)) by FINSEQ_1:def 3;

then reconsider d = (Col (A,j)) . k as Element of K by FINSEQ_2:11;

len ((Col (A,j)) + (Col (B,j))) = len (a + b)

.= len A by CARD_1:def 7

.= len (Col (A,j)) by CARD_1:def 7 ;

then k in dom ((Col (A,j)) + (Col (B,j))) by A12, FINSEQ_1:def 3;

then A13: ((Col (A,j)) + (Col (B,j))) . k = d + e by FVSUM_1:17;

j in Seg (width (A + B)) by A3, A4, ZFMISC_1:87;

then A14: [k,j] in Indices (A + B) by A9, ZFMISC_1:87;

A15: (Col ((A + B),j)) . k = (A + B) * (k,j) by A9, MATRIX_0:def 8

.= (A * (k,j)) + (B * (k,j)) by A5, A14, MATRIX_3:def 3 ;

A16: k in dom A by A11, A12, FINSEQ_1:def 3;

then (Col (A,j)) . k = A * (k,j) by MATRIX_0:def 8;

hence (Col ((A + B),j)) . k = ((Col (A,j)) + (Col (B,j))) . k by A15, A13, A10, A16, MATRIX_0:def 8; :: thesis: verum

.= len A by CARD_1:def 7 ;

len (Col ((A + B),j)) = len A by A1, MATRIX_0:def 8;

hence Col ((A + B),j) = (Col (A,j)) + (Col (B,j)) by A17, A6, FINSEQ_1:14; :: thesis: verum