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

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

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

assume that

A1: len B = len C and

A2: width B = width C and

A3: width A = len B and

A4: len A > 0 and

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

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

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

A8: ( width (B + C) = width B & width (A * (B + C)) = width (B + C) ) by A3, A6, MATRIX_3:def 3, MATRIX_3:def 4;

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

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

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

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

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

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

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

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

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

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

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

assume that

A1: len B = len C and

A2: width B = width C and

A3: width A = len B and

A4: len A > 0 and

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

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

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

A8: ( width (B + C) = width B & width (A * (B + C)) = width (B + C) ) by A3, A6, MATRIX_3:def 3, MATRIX_3:def 4;

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

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

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

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

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

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

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

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

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

proof

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

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

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

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

A14: len (mlt ((Line (A,i)),(Col (B,j)))) = len (mlt (q1,q2))

.= len B by CARD_1:def 7

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

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

( dom B = Seg (len B) & 1 + 0 <= len B ) by A5, FINSEQ_1:def 3, NAT_1:13;

then A15: 1 in dom B by FINSEQ_1:1;

len (Line (A,i)) = len C by A1, A3, MATRIX_0:def 7;

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

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

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

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

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

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

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

j in Seg (width B) by A8, A17, ZFMISC_1:87;

then A19: [1,j] in Indices B by A15, ZFMISC_1:87;

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

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

.= Sum (mlt ((Line (A,i)),((Col (B,j)) + (Col (C,j))))) by A1, A19, Th60

.= Sum ((mlt ((Line (A,i)),(Col (B,j)))) + (mlt ((Line (A,i)),(Col (C,j))))) by A13, A16, Th57

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

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

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

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

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

A14: len (mlt ((Line (A,i)),(Col (B,j)))) = len (mlt (q1,q2))

.= len B by CARD_1:def 7

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

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

( dom B = Seg (len B) & 1 + 0 <= len B ) by A5, FINSEQ_1:def 3, NAT_1:13;

then A15: 1 in dom B by FINSEQ_1:1;

len (Line (A,i)) = len C by A1, A3, MATRIX_0:def 7;

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

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

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

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

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

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

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

j in Seg (width B) by A8, A17, ZFMISC_1:87;

then A19: [1,j] in Indices B by A15, ZFMISC_1:87;

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

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

.= Sum (mlt ((Line (A,i)),((Col (B,j)) + (Col (C,j))))) by A1, A19, Th60

.= Sum ((mlt ((Line (A,i)),(Col (B,j)))) + (mlt ((Line (A,i)),(Col (C,j))))) by A13, A16, Th57

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

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