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

for j being Nat

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

Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

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

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

Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

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

Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

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

assume that

A1: width A = width B and

A2: ex j being Nat st [i,j] in Indices A ; :: thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

reconsider wA = width A as Element of NAT by ORDINAL1:def 12;

reconsider a = Line (A,i), b = Line (B,i) as Element of wA -tuples_on the carrier of K by A1;

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

i in dom A by A2, ZFMISC_1:87;

then A4: i in Seg (len A) by FINSEQ_1:def 3;

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

then A6: Indices (A + B) = Indices A by A3, Th55;

A7: for k being Nat st 1 <= k & k <= len (Line ((A + B),i)) holds

(Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k

.= width A by CARD_1:def 7 ;

len (Line ((A + B),i)) = width A by A3, MATRIX_0:def 7;

hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A16, A7, FINSEQ_1:14; :: thesis: verum

for j being Nat

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

Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

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

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

Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

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

Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

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

assume that

A1: width A = width B and

A2: ex j being Nat st [i,j] in Indices A ; :: thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

reconsider wA = width A as Element of NAT by ORDINAL1:def 12;

reconsider a = Line (A,i), b = Line (B,i) as Element of wA -tuples_on the carrier of K by A1;

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

i in dom A by A2, ZFMISC_1:87;

then A4: i in Seg (len A) by FINSEQ_1:def 3;

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

then A6: Indices (A + B) = Indices A by A3, Th55;

A7: for k being Nat st 1 <= k & k <= len (Line ((A + B),i)) holds

(Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k

proof

A16: len ((Line (A,i)) + (Line (B,i))) =
len (a + b)
let k be Nat; :: thesis: ( 1 <= k & k <= len (Line ((A + B),i)) implies (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k )

assume A8: ( 1 <= k & k <= len (Line ((A + B),i)) ) ; :: thesis: (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k

A9: len (Line ((A + B),i)) = width A by A3, MATRIX_0:def 7;

then A10: k in Seg (width (A + B)) by A3, A8, FINSEQ_1:1;

len (Line (B,i)) = width B by MATRIX_0:def 7;

then k in Seg (len (Line (B,i))) by A1, A8, A9, FINSEQ_1:1;

then k in dom (Line (B,i)) by FINSEQ_1:def 3;

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

i in dom (A + B) by A5, A4, FINSEQ_1:def 3;

then A11: [i,k] in Indices (A + B) by A10, ZFMISC_1:87;

A12: (Line ((A + B),i)) . k = (A + B) * (i,k) by A10, MATRIX_0:def 7

.= (A * (i,k)) + (B * (i,k)) by A6, A11, MATRIX_3:def 3 ;

A13: len (Line (A,i)) = width A by MATRIX_0:def 7;

then A14: k in Seg (len (Line (A,i))) by A8, A9, FINSEQ_1:1;

then k in dom (Line (A,i)) by FINSEQ_1:def 3;

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

len ((Line (A,i)) + (Line (B,i))) = len (a + b)

.= width A by CARD_1:def 7

.= len (Line (A,i)) by CARD_1:def 7 ;

then k in dom ((Line (A,i)) + (Line (B,i))) by A14, FINSEQ_1:def 3;

then A15: ((Line (A,i)) + (Line (B,i))) . k = d + e by FVSUM_1:17;

(Line (A,i)) . k = A * (i,k) by A13, A14, MATRIX_0:def 7;

hence (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k by A1, A13, A12, A14, A15, MATRIX_0:def 7; :: thesis: verum

end;assume A8: ( 1 <= k & k <= len (Line ((A + B),i)) ) ; :: thesis: (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k

A9: len (Line ((A + B),i)) = width A by A3, MATRIX_0:def 7;

then A10: k in Seg (width (A + B)) by A3, A8, FINSEQ_1:1;

len (Line (B,i)) = width B by MATRIX_0:def 7;

then k in Seg (len (Line (B,i))) by A1, A8, A9, FINSEQ_1:1;

then k in dom (Line (B,i)) by FINSEQ_1:def 3;

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

i in dom (A + B) by A5, A4, FINSEQ_1:def 3;

then A11: [i,k] in Indices (A + B) by A10, ZFMISC_1:87;

A12: (Line ((A + B),i)) . k = (A + B) * (i,k) by A10, MATRIX_0:def 7

.= (A * (i,k)) + (B * (i,k)) by A6, A11, MATRIX_3:def 3 ;

A13: len (Line (A,i)) = width A by MATRIX_0:def 7;

then A14: k in Seg (len (Line (A,i))) by A8, A9, FINSEQ_1:1;

then k in dom (Line (A,i)) by FINSEQ_1:def 3;

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

len ((Line (A,i)) + (Line (B,i))) = len (a + b)

.= width A by CARD_1:def 7

.= len (Line (A,i)) by CARD_1:def 7 ;

then k in dom ((Line (A,i)) + (Line (B,i))) by A14, FINSEQ_1:def 3;

then A15: ((Line (A,i)) + (Line (B,i))) . k = d + e by FVSUM_1:17;

(Line (A,i)) . k = A * (i,k) by A13, A14, MATRIX_0:def 7;

hence (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k by A1, A13, A12, A14, A15, MATRIX_0:def 7; :: thesis: verum

.= width A by CARD_1:def 7 ;

len (Line ((A + B),i)) = width A by A3, MATRIX_0:def 7;

hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A16, A7, FINSEQ_1:14; :: thesis: verum