let K be Field; :: thesis: for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds

(B + C) * A = (B * A) + (C * A)

let A, B, C be Matrix of K; :: thesis: ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 implies (B + C) * A = (B * A) + (C * A) )

assume that

A1: len B = len C and

A2: width B = width C and

A3: len A = width B and

A4: len B > 0 and

A5: len A > 0 ; :: thesis: (B + C) * A = (B * A) + (C * A)

A6: width (B + C) = width B by MATRIX_3:def 3;

then A7: width ((B + C) * A) = width A by A3, MATRIX_3:def 4;

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

then A8: len ((B + C) * A) = len B by A3, A6, MATRIX_3:def 4;

then reconsider M1 = (B + C) * A as Matrix of len B, width A,K by A4, A7, MATRIX_0:20;

A9: len (B * A) = len B by A3, MATRIX_3:def 4;

A10: width (B * A) = width A by A3, MATRIX_3:def 4;

then A11: Indices M1 = Indices (B * A) by A8, A7, A9, Th55;

A12: ( len ((B * A) + (C * A)) = len (B * A) & width ((B * A) + (C * A)) = width (B * A) ) by MATRIX_3:def 3;

then reconsider M2 = (B * A) + (C * A) as Matrix of len B, width A,K by A4, A9, A10, MATRIX_0:20;

( len (C * A) = len C & width (C * A) = width A ) by A2, A3, MATRIX_3:def 4;

then A13: Indices M1 = Indices (C * A) by A1, A8, A7, Th55;

for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = M2 * (i,j)

(B + C) * A = (B * A) + (C * A)

let A, B, C be Matrix of K; :: thesis: ( len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 implies (B + C) * A = (B * A) + (C * A) )

assume that

A1: len B = len C and

A2: width B = width C and

A3: len A = width B and

A4: len B > 0 and

A5: len A > 0 ; :: thesis: (B + C) * A = (B * A) + (C * A)

A6: width (B + C) = width B by MATRIX_3:def 3;

then A7: width ((B + C) * A) = width A by A3, MATRIX_3:def 4;

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

then A8: len ((B + C) * A) = len B by A3, A6, MATRIX_3:def 4;

then reconsider M1 = (B + C) * A as Matrix of len B, width A,K by A4, A7, MATRIX_0:20;

A9: len (B * A) = len B by A3, MATRIX_3:def 4;

A10: width (B * A) = width A by A3, MATRIX_3:def 4;

then A11: Indices M1 = Indices (B * A) by A8, A7, A9, Th55;

A12: ( len ((B * A) + (C * A)) = len (B * A) & width ((B * A) + (C * A)) = width (B * A) ) by MATRIX_3:def 3;

then reconsider M2 = (B * A) + (C * A) as Matrix of len B, width A,K by A4, A9, A10, MATRIX_0:20;

( len (C * A) = len C & width (C * A) = width A ) by A2, A3, MATRIX_3:def 4;

then A13: Indices M1 = Indices (C * A) by A1, A8, A7, Th55;

for i, j being Nat st [i,j] in Indices M1 holds

M1 * (i,j) = M2 * (i,j)

proof

hence
(B + C) * A = (B * A) + (C * A)
by A8, A7, A9, A10, A12, MATRIX_0:21; :: thesis: verum
let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )

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

then A14: len (Col (A,j)) = len (Line (B,i)) by MATRIX_0:def 7;

reconsider q1 = Line (B,i), q2 = Line (C,i), q3 = Col (A,j) as Element of (len A) -tuples_on the carrier of K by A2, A3;

A15: len (mlt ((Line (B,i)),(Col (A,j)))) = len (mlt (q1,q3))

.= len A by CARD_1:def 7

.= len (mlt (q2,q3)) by CARD_1:def 7

.= len (mlt ((Line (C,i)),(Col (A,j)))) ;

1 + 0 <= width B by A3, A5, NAT_1:13;

then A16: 1 in Seg (width B) by FINSEQ_1:1;

len (Col (A,j)) = width C by A2, A3, MATRIX_0:def 8;

then A17: len (Col (A,j)) = len (Line (C,i)) by MATRIX_0:def 7;

assume A18: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)

then A19: M2 * (i,j) = ((B * A) * (i,j)) + ((C * A) * (i,j)) by A11, MATRIX_3:def 3

.= ((Line (B,i)) "*" (Col (A,j))) + ((C * A) * (i,j)) by A3, A11, A18, MATRIX_3:def 4

.= ((Line (B,i)) "*" (Col (A,j))) + ((Line (C,i)) "*" (Col (A,j))) by A2, A3, A13, A18, MATRIX_3:def 4

.= ((Line (B,i)) "*" (Col (A,j))) + (Sum (mlt ((Line (C,i)),(Col (A,j))))) by FVSUM_1:def 9

.= (Sum (mlt ((Line (B,i)),(Col (A,j))))) + (Sum (mlt ((Line (C,i)),(Col (A,j))))) by FVSUM_1:def 9 ;

i in dom (B * A) by A11, A18, ZFMISC_1:87;

then i in Seg (len B) by A9, FINSEQ_1:def 3;

then i in dom B by FINSEQ_1:def 3;

then A20: [i,1] in Indices B by A16, ZFMISC_1:87;

M1 * (i,j) = (Line ((B + C),i)) "*" (Col (A,j)) by A3, A6, A18, MATRIX_3:def 4

.= Sum (mlt ((Line ((B + C),i)),(Col (A,j)))) by FVSUM_1:def 9

.= Sum (mlt (((Line (B,i)) + (Line (C,i))),(Col (A,j)))) by A2, A20, Th59

.= Sum ((mlt ((Line (B,i)),(Col (A,j)))) + (mlt ((Line (C,i)),(Col (A,j))))) by A14, A17, Th56

.= (Sum (mlt ((Line (B,i)),(Col (A,j))))) + (Sum (mlt ((Line (C,i)),(Col (A,j))))) by A15, Th61 ;

hence M1 * (i,j) = M2 * (i,j) by A19; :: thesis: verum

end;len (Col (A,j)) = width B by A3, MATRIX_0:def 8;

then A14: len (Col (A,j)) = len (Line (B,i)) by MATRIX_0:def 7;

reconsider q1 = Line (B,i), q2 = Line (C,i), q3 = Col (A,j) as Element of (len A) -tuples_on the carrier of K by A2, A3;

A15: len (mlt ((Line (B,i)),(Col (A,j)))) = len (mlt (q1,q3))

.= len A by CARD_1:def 7

.= len (mlt (q2,q3)) by CARD_1:def 7

.= len (mlt ((Line (C,i)),(Col (A,j)))) ;

1 + 0 <= width B by A3, A5, NAT_1:13;

then A16: 1 in Seg (width B) by FINSEQ_1:1;

len (Col (A,j)) = width C by A2, A3, MATRIX_0:def 8;

then A17: len (Col (A,j)) = len (Line (C,i)) by MATRIX_0:def 7;

assume A18: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)

then A19: M2 * (i,j) = ((B * A) * (i,j)) + ((C * A) * (i,j)) by A11, MATRIX_3:def 3

.= ((Line (B,i)) "*" (Col (A,j))) + ((C * A) * (i,j)) by A3, A11, A18, MATRIX_3:def 4

.= ((Line (B,i)) "*" (Col (A,j))) + ((Line (C,i)) "*" (Col (A,j))) by A2, A3, A13, A18, MATRIX_3:def 4

.= ((Line (B,i)) "*" (Col (A,j))) + (Sum (mlt ((Line (C,i)),(Col (A,j))))) by FVSUM_1:def 9

.= (Sum (mlt ((Line (B,i)),(Col (A,j))))) + (Sum (mlt ((Line (C,i)),(Col (A,j))))) by FVSUM_1:def 9 ;

i in dom (B * A) by A11, A18, ZFMISC_1:87;

then i in Seg (len B) by A9, FINSEQ_1:def 3;

then i in dom B by FINSEQ_1:def 3;

then A20: [i,1] in Indices B by A16, ZFMISC_1:87;

M1 * (i,j) = (Line ((B + C),i)) "*" (Col (A,j)) by A3, A6, A18, MATRIX_3:def 4

.= Sum (mlt ((Line ((B + C),i)),(Col (A,j)))) by FVSUM_1:def 9

.= Sum (mlt (((Line (B,i)) + (Line (C,i))),(Col (A,j)))) by A2, A20, Th59

.= Sum ((mlt ((Line (B,i)),(Col (A,j)))) + (mlt ((Line (C,i)),(Col (A,j))))) by A14, A17, Th56

.= (Sum (mlt ((Line (B,i)),(Col (A,j))))) + (Sum (mlt ((Line (C,i)),(Col (A,j))))) by A15, Th61 ;

hence M1 * (i,j) = M2 * (i,j) by A19; :: thesis: verum